0 | module TTImp.Elab.Rewrite
  1 |
  2 | import Core.Env
  3 | import Core.GetType
  4 | import Core.Metadata
  5 | import Core.Unify
  6 | import Core.Value
  7 |
  8 | import Idris.REPL.Opts
  9 | import Idris.Syntax
 10 |
 11 | import TTImp.Elab.Check
 12 | import TTImp.Elab.Delayed
 13 | import TTImp.TTImp
 14 |
 15 | import Libraries.Data.List.SizeOf
 16 |
 17 | %default covering
 18 |
 19 | -- TODO: Later, we'll get the name of the lemma from the type, if it's one
 20 | -- that's generated for a dependent type. For now, always return the default
 21 | findRewriteLemma : {auto c : Ref Ctxt Defs} ->
 22 |                    FC -> (rulety : Term vars) ->
 23 |                    Core Name
 24 | findRewriteLemma loc rulety
 25 |    = case !getRewrite of
 26 |           Nothing => throw (GenericMsg loc "No rewrite lemma defined")
 27 |           Just n => pure n
 28 |
 29 | getRewriteTerms : {vars : _} ->
 30 |                   {auto c : Ref Ctxt Defs} ->
 31 |                   FC -> Defs -> NF vars -> Error ->
 32 |                   Core (NF vars, NF vars, NF vars)
 33 | getRewriteTerms loc defs (NTCon nfc eq a args) err
 34 |     = if !(isEqualTy eq)
 35 |          then case reverse $ map snd args of
 36 |                    (rhs :: lhs :: rhsty :: lhsty :: _) =>
 37 |                         pure (!(evalClosure defs lhs),
 38 |                               !(evalClosure defs rhs),
 39 |                               !(evalClosure defs lhsty))
 40 |                    _ => throw err
 41 |          else throw err
 42 | getRewriteTerms loc defs ty err
 43 |     = throw err
 44 |
 45 | rewriteErr : Error -> Bool
 46 | rewriteErr (NotRewriteRule {}) = True
 47 | rewriteErr (RewriteNoChange {}) = True
 48 | rewriteErr (InType _ _ err) = rewriteErr err
 49 | rewriteErr (InCon _ err) = rewriteErr err
 50 | rewriteErr (InLHS _ _ err) = rewriteErr err
 51 | rewriteErr (InRHS _ _ err) = rewriteErr err
 52 | rewriteErr (WhenUnifying _ _ _ _ _ err) = rewriteErr err
 53 | rewriteErr _ = False
 54 |
 55 | record Lemma vars where
 56 |   constructor MkLemma
 57 |   ||| The name of the rewriting lemma
 58 |   name : Name
 59 |   ||| The predicate (\ v => lhs === rhs) to pass to it
 60 |   pred : Term vars
 61 |   ||| The type ((v : ?) -> Type) of the predicate
 62 |   predTy : Term vars
 63 |
 64 | elabRewrite : {vars : _} ->
 65 |               {auto c : Ref Ctxt Defs} ->
 66 |               {auto u : Ref UST UState} ->
 67 |               FC -> Env Term vars ->
 68 |               (expected : Term vars) ->
 69 |               (rulety : Term vars) ->
 70 |               Core (Lemma vars)
 71 | elabRewrite loc env expected rulety
 72 |     = do defs <- get Ctxt
 73 |          parg <- genVarName "rwarg"
 74 |          tynf <- nf defs env rulety
 75 |          (lt, rt, lty) <- getRewriteTerms loc defs tynf (NotRewriteRule loc env rulety)
 76 |          lemn <- findRewriteLemma loc rulety
 77 |
 78 |          -- Need to normalise again, since we might have been delayed and
 79 |          -- the metavariables might have been updated
 80 |          expnf <- nf defs env expected
 81 |
 82 |          logNF "elab.rewrite" 5 "Rewriting" env lt
 83 |          logNF "elab.rewrite" 5 "Rewriting in" env expnf
 84 |          rwexp_sc <- replace defs env lt (Ref loc Bound parg) expnf
 85 |          logTerm "elab.rewrite" 5 "Rewritten to" rwexp_sc
 86 |
 87 |          empty <- clearDefs defs
 88 |          let pred = Bind loc parg (Lam loc top Explicit
 89 |                           !(quote empty env lty))
 90 |                           (refsToLocals (Add parg parg None) rwexp_sc)
 91 |          gpredty <- getType env pred
 92 |          predty <- getTerm gpredty
 93 |          exptm <- quote defs env expected
 94 |
 95 |          -- if the rewritten expected type converts with the original,
 96 |          -- then the rewrite did nothing, which is an error
 97 |          when !(convert defs env rwexp_sc exptm) $
 98 |              throw (RewriteNoChange loc env rulety exptm)
 99 |          pure (MkLemma lemn pred predty)
100 |
101 | export
102 | checkRewrite : {vars : _} ->
103 |                {auto c : Ref Ctxt Defs} ->
104 |                {auto m : Ref MD Metadata} ->
105 |                {auto u : Ref UST UState} ->
106 |                {auto e : Ref EST (EState vars)} ->
107 |                {auto s : Ref Syn SyntaxInfo} ->
108 |                {auto o : Ref ROpts REPLOpts} ->
109 |                RigCount -> ElabInfo ->
110 |                NestedNames vars -> Env Term vars ->
111 |                FC -> RawImp -> RawImp -> Maybe (Glued vars) ->
112 |                Core (Term vars, Glued vars)
113 | checkRewrite rigc elabinfo nest env fc rule tm Nothing
114 |     = throw (GenericMsg fc "Can't infer a type for rewrite")
115 | checkRewrite {vars} rigc elabinfo nest env ifc rule tm (Just expected)
116 |     = delayOnFailure ifc rigc env (Just expected) rewriteErr Rewrite $ \delayed =>
117 |         do let vfc = virtualiseFC ifc
118 |
119 |            constart <- getNextEntry
120 |            (rulev, grulet) <- check erased elabinfo nest env rule Nothing
121 |            solveConstraintsAfter constart inTerm Normal
122 |
123 |            rulet <- getTerm grulet
124 |            expTy <- getTerm expected
125 |            when delayed $ log "elab.rewrite" 5 "Retrying rewrite"
126 |            lemma <- elabRewrite vfc env expTy rulet
127 |
128 |            rname <- genVarName "_"
129 |            pname <- genVarName "_"
130 |
131 |            let pbind = Let vfc erased lemma.pred lemma.predTy
132 |            let rbind = Let vfc erased (weaken rulev) (weaken rulet)
133 |
134 |            let env' = rbind :: pbind :: env
135 |
136 |            -- Nothing we do in this last part will affect the EState,
137 |            -- we're only doing the application this way to make sure the
138 |            -- implicits for the rewriting lemma are in the right place. But,
139 |            -- we still need the right type for the EState, so weaken it once
140 |            -- for each of the let bindings above.
141 |            (rwtm, grwty) <-
142 |               inScope vfc (pbind :: env) $ \e' =>
143 |                 inScope {e=e'} vfc env' $ \e'' =>
144 |                   let offset = mkSizeOf [rname, pname] in
145 |                   check {e = e''} rigc elabinfo (weakenNs offset nest) env'
146 |                     (apply (IVar vfc lemma.name)
147 |                       [ IVar vfc pname
148 |                       , IVar vfc rname
149 |                       , tm ])
150 |                     (Just (gnf env' (weakenNs offset expTy)))
151 |            rwty <- getTerm grwty
152 |            let binding = Bind vfc pname pbind . Bind vfc rname rbind
153 |            pure (binding rwtm, gnf env (binding rwty))
154 |