0 | module TTImp.Elab.Quote
5 | import Core.UnifyState
7 | import Idris.REPL.Opts
10 | import TTImp.Elab.Check
11 | import TTImp.Reflect
17 | data Unq : Type where
22 | getUnquote : {auto c : Ref Ctxt Defs} ->
23 | {auto q : Ref Unq (List (Name, FC, RawImp))} ->
24 | {auto u : Ref UST UState} ->
27 | getUnquote (IPi fc c p n arg ret)
28 | = pure $
IPi fc c p n !(getUnquote arg) !(getUnquote ret)
29 | getUnquote (ILam fc c p n arg sc)
30 | = pure $
ILam fc c p n !(getUnquote arg) !(getUnquote sc)
31 | getUnquote (ILet fc lhsFC c n ty val sc)
32 | = pure $
ILet fc lhsFC c n !(getUnquote ty) !(getUnquote val) !(getUnquote sc)
33 | getUnquote (ICase fc opts sc ty cs)
34 | = pure $
ICase fc opts
35 | !(getUnquote sc) !(getUnquote ty)
36 | !(traverse getUnquoteClause cs)
37 | getUnquote (ILocal fc ds sc)
38 | = pure $
ILocal fc !(traverse getUnquoteDecl ds) !(getUnquote sc)
39 | getUnquote (IUpdate fc ds sc)
40 | = pure $
IUpdate fc !(traverse getUnquoteUpdate ds) !(getUnquote sc)
41 | getUnquote (IApp fc f a)
42 | = pure $
IApp fc !(getUnquote f) !(getUnquote a)
43 | getUnquote (IAutoApp fc f a)
44 | = pure $
IAutoApp fc !(getUnquote f) !(getUnquote a)
45 | getUnquote (INamedApp fc f n a)
46 | = pure $
INamedApp fc !(getUnquote f) n !(getUnquote a)
47 | getUnquote (IWithApp fc f a)
48 | = pure $
IWithApp fc !(getUnquote f) !(getUnquote a)
49 | getUnquote (IAlternative fc at as)
50 | = pure $
IAlternative fc at !(traverse getUnquote as)
51 | getUnquote (IRewrite fc f a)
52 | = pure $
IRewrite fc !(getUnquote f) !(getUnquote a)
53 | getUnquote (ICoerced fc t)
54 | = pure $
ICoerced fc !(getUnquote t)
55 | getUnquote (IBindHere fc m t)
56 | = pure $
IBindHere fc m !(getUnquote t)
57 | getUnquote (IAs fc nameFC u nm t)
58 | = pure $
IAs fc nameFC u nm !(getUnquote t)
59 | getUnquote (IMustUnify fc r t)
60 | = pure $
IMustUnify fc r !(getUnquote t)
61 | getUnquote (IDelayed fc r t)
62 | = pure $
IDelayed fc r !(getUnquote t)
63 | getUnquote (IDelay fc t)
64 | = pure $
IDelay fc !(getUnquote t)
65 | getUnquote (IForce fc t)
66 | = pure $
IForce fc !(getUnquote t)
67 | getUnquote (IQuote fc t)
68 | = pure $
IQuote fc !(getUnquote t)
69 | getUnquote (IUnquote fc tm)
70 | = do qv <- genVarName "q"
71 | update Unq ((qv, fc, tm) ::)
72 | pure (IUnquote fc (IVar fc qv))
73 | getUnquote tm = pure tm
75 | getUnquoteClause : {auto c : Ref Ctxt Defs} ->
76 | {auto q : Ref Unq (List (Name, FC, RawImp))} ->
77 | {auto u : Ref UST UState} ->
80 | getUnquoteClause (PatClause fc l r)
81 | = pure $
PatClause fc !(getUnquote l) !(getUnquote r)
82 | getUnquoteClause (WithClause fc l rig w prf flags cs)
90 | !(traverse getUnquoteClause cs)
91 | getUnquoteClause (ImpossibleClause fc l)
92 | = pure $
ImpossibleClause fc !(getUnquote l)
94 | getUnquoteUpdate : {auto c : Ref Ctxt Defs} ->
95 | {auto q : Ref Unq (List (Name, FC, RawImp))} ->
96 | {auto u : Ref UST UState} ->
99 | getUnquoteUpdate (ISetField p t) = pure $
ISetField p !(getUnquote t)
100 | getUnquoteUpdate (ISetFieldApp p t) = pure $
ISetFieldApp p !(getUnquote t)
102 | getUnquoteRecord : {auto c : Ref Ctxt Defs} ->
103 | {auto q : Ref Unq (List (Name, FC, RawImp))} ->
104 | {auto u : Ref UST UState} ->
105 | ImpRecordData Name ->
106 | Core (ImpRecordData Name)
107 | getUnquoteRecord (MkImpRecord header body)
109 | = pure $
MkImpRecord !(traverse (traverse (traverse (traverse getUnquote))) header)
110 | !(traverse (traverse (traverse (traverse getUnquote))) body)
112 | getUnquoteData : {auto c : Ref Ctxt Defs} ->
113 | {auto q : Ref Unq (List (Name, FC, RawImp))} ->
114 | {auto u : Ref UST UState} ->
117 | getUnquoteData (MkImpData fc n tc opts cs)
118 | = pure $
MkImpData fc n !(traverseOpt getUnquote tc) opts
119 | !(traverse (traverse getUnquote) cs)
120 | getUnquoteData (MkImpLater fc n tc)
121 | = pure $
MkImpLater fc n !(getUnquote tc)
123 | getUnquoteDecl : {auto c : Ref Ctxt Defs} ->
124 | {auto q : Ref Unq (List (Name, FC, RawImp))} ->
125 | {auto u : Ref UST UState} ->
128 | getUnquoteDecl (IClaim (MkWithData fc (MkIClaimData c v opts ty)))
129 | = pure $
IClaim (MkWithData fc (MkIClaimData c v opts !(traverse getUnquote ty)))
130 | getUnquoteDecl (IData fc v mbt d)
131 | = pure $
IData fc v mbt !(getUnquoteData d)
132 | getUnquoteDecl (IDef fc v d)
133 | = pure $
IDef fc v !(traverse getUnquoteClause d)
134 | getUnquoteDecl (IParameters fc ps ds)
135 | = pure $
IParameters fc
136 | !(traverseList1 (traverse (traverse getUnquote)) ps)
137 | !(traverse getUnquoteDecl ds)
138 | getUnquoteDecl (IRecord fc ns v mbt d)
139 | = pure $
IRecord fc ns v mbt !(traverse getUnquoteRecord d)
140 | getUnquoteDecl (INamespace fc ns ds)
141 | = pure $
INamespace fc ns !(traverse getUnquoteDecl ds)
142 | getUnquoteDecl (ITransform fc n l r)
143 | = pure $
ITransform fc n !(getUnquote l) !(getUnquote r)
144 | getUnquoteDecl d = pure d
146 | bindUnqs : {vars : _} ->
147 | {auto c : Ref Ctxt Defs} ->
148 | {auto m : Ref MD Metadata} ->
149 | {auto u : Ref UST UState} ->
150 | {auto e : Ref EST (EState vars)} ->
151 | {auto s : Ref Syn SyntaxInfo} ->
152 | {auto o : Ref ROpts REPLOpts} ->
153 | List (Name, FC, RawImp) ->
154 | RigCount -> ElabInfo -> NestedNames vars -> Env Term vars ->
157 | bindUnqs [] _ _ _ _ tm = pure tm
158 | bindUnqs ((qvar, fc, esctm) :: qs) rig elabinfo nest env tm
159 | = do defs <- get Ctxt
160 | Just (idx, gdef) <- lookupCtxtExactI (reflectionttimp "TTImp") (gamma defs)
161 | | _ => throw (UndefinedName fc (reflectionttimp "TTImp"))
162 | (escv, escty) <- check rig elabinfo nest env esctm
163 | (Just (gnf env (Ref fc (TyCon 0)
165 | sc <- bindUnqs qs rig elabinfo nest env tm
166 | pure (Bind fc qvar (Let fc (rigMult top rig) escv !(getTerm escty))
167 | (refToLocal qvar qvar sc))
169 | onLHS : ElabMode -> Bool
170 | onLHS (InLHS _) = True
174 | checkQuote : {vars : _} ->
175 | {auto c : Ref Ctxt Defs} ->
176 | {auto m : Ref MD Metadata} ->
177 | {auto u : Ref UST UState} ->
178 | {auto e : Ref EST (EState vars)} ->
179 | {auto s : Ref Syn SyntaxInfo} ->
180 | {auto o : Ref ROpts REPLOpts} ->
181 | RigCount -> ElabInfo ->
182 | NestedNames vars -> Env Term vars ->
183 | FC -> RawImp -> Maybe (Glued vars) ->
184 | Core (Term vars, Glued vars)
185 | checkQuote rig elabinfo nest env fc tm exp
186 | = do defs <- get Ctxt
188 | tm' <- getUnquote tm
189 | qtm <- reflect fc defs (onLHS (elabMode elabinfo)) env tm'
191 | qty <- getCon fc defs (reflectionttimp "TTImp")
192 | qtm <- bindUnqs unqs rig elabinfo nest env qtm
193 | fullqtm <- normalise defs env qtm
194 | checkExp rig elabinfo env fc fullqtm (gnf env qty) exp
197 | checkQuoteName : {vars : _} ->
198 | {auto c : Ref Ctxt Defs} ->
199 | {auto u : Ref UST UState} ->
200 | RigCount -> ElabInfo ->
201 | NestedNames vars -> Env Term vars ->
202 | FC -> Name -> Maybe (Glued vars) ->
203 | Core (Term vars, Glued vars)
204 | checkQuoteName rig elabinfo nest env fc n exp
205 | = do defs <- get Ctxt
206 | qnm <- reflect fc defs (onLHS (elabMode elabinfo)) env n
207 | qty <- getCon fc defs (reflectiontt "Name")
208 | checkExp rig elabinfo env fc qnm (gnf env qty) exp
211 | checkQuoteDecl : {vars : _} ->
212 | {auto c : Ref Ctxt Defs} ->
213 | {auto m : Ref MD Metadata} ->
214 | {auto u : Ref UST UState} ->
215 | {auto e : Ref EST (EState vars)} ->
216 | {auto s : Ref Syn SyntaxInfo} ->
217 | {auto o : Ref ROpts REPLOpts} ->
218 | RigCount -> ElabInfo ->
219 | NestedNames vars -> Env Term vars ->
220 | FC -> List ImpDecl -> Maybe (Glued vars) ->
221 | Core (Term vars, Glued vars)
222 | checkQuoteDecl rig elabinfo nest env fc ds exp
223 | = do defs <- get Ctxt
225 | ds' <- traverse getUnquoteDecl ds
226 | qds <- reflect fc defs (onLHS (elabMode elabinfo)) env ds'
228 | qd <- getCon fc defs (reflectionttimp "Decl")
229 | qty <- appCon fc defs (basics "List") [qd]
230 | checkExp rig elabinfo env fc
231 | !(bindUnqs unqs rig elabinfo nest env qds)