git.iko.soy/Idris-dev
on master help sign in
Add conversion checking to Elab
e947d69David Raymond Christiansen
libs/prelude/Language/Reflection/Elab.idr+16
compare with master
unifiedsplit
@@ -139,6 +139,7 @@ data Elab : Type -> Type where
139 prim__Compute : Elab ()
139 prim__Compute : Elab ()
140 prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT
140 prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT
141 prim__Whnf : TT -> Elab TT
141 prim__Whnf : TT -> Elab TT
142+ prim__Converts : (List (TTName, Binder TT)) -> TT -> TT -> Elab ()
142
143
143 prim__DeclareType : TyDecl -> Elab ()
144 prim__DeclareType : TyDecl -> Elab ()
144 prim__DefineFunction : FunDefn -> Elab ()
145 prim__DefineFunction : FunDefn -> Elab ()
@@ -373,6 +374,21 @@ namespace Tactics
373 whnf : (term : TT) -> Elab TT
374 whnf : (term : TT) -> Elab TT
374 whnf term = prim__Whnf term
375 whnf term = prim__Whnf term
375
376
377+ ||| Check that two terms are convertable in the current context and environment
378+ |||
379+ ||| @ env a lexical environment to compare the terms in (see `getEnv`)
380+ ||| @ term1 the first term to convert
381+ ||| @ term2 the second term to convert
382+ convertsInEnv : (env : List (TTName, Binder TT)) -> (term1, term2 : TT) -> Elab ()
383+ convertsInEnv env term1 term2 = prim__Converts env term1 term2
384+
385+ ||| Check that two terms are convertable in the current context and environment
386+ |||
387+ ||| @ term1 the first term to convert
388+ ||| @ term2 the second term to convert
389+ converts : (term1, term2 : TT) -> Elab ()
390+ converts term1 term2 = convertsInEnv !getEnv term1 term2
391+
376 ||| Find the source context for the elaboration script
392 ||| Find the source context for the elaboration script
377 getSourceLocation : Elab SourceLocation
393 getSourceLocation : Elab SourceLocation
378 getSourceLocation = prim__SourceLocation
394 getSourceLocation = prim__SourceLocation
src/Idris/Elab/Term.hs+7
@@ -1963,6 +1963,13 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1963 = do tm' <- reifyTT tm
1963 = do tm' <- reifyTT tm
1964 ctxt <- get_context
1964 ctxt <- get_context
1965 fmap fst . checkClosed . reflect $ whnf ctxt tm'
1965 fmap fst . checkClosed . reflect $ whnf ctxt tm'
1966+ | n == tacN "prim__Converts", [env, tm1, tm2] <- args
1967+ = do env' <- reifyEnv env
1968+ tm1' <- reifyTT tm1
1969+ tm2' <- reifyTT tm2
1970+ ctxt <- get_context
1971+ lift $ converts ctxt env' tm1' tm2'
1972+ returnUnit
1966 | n == tacN "prim__DeclareType", [decl] <- args
1973 | n == tacN "prim__DeclareType", [decl] <- args
1967 = do (RDeclare n args res) <- reifyTyDecl decl
1974 = do (RDeclare n args res) <- reifyTyDecl decl
1968 ctxt <- get_context
1975 ctxt <- get_context