git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2367 from david-christiansen/wip/tactical

Elab reflection progress

commitf96ccde7a3ffffbe4e770c610d0a8b6890059952 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 12 Jun 2015, 14:25 (11 years ago) parent8ed6000b2dc1fc
9 files changed+217−95
compare with master
unifiedsplit
libs/base/Language/Reflection/Utils.idr+7−3 libs/prelude/Language/Reflection/Elab.idr+17−8 src/Idris/AbsSyntax.hs+9−8 src/Idris/AbsSyntaxTree.hs+4 src/Idris/Elab/Term.hs+24−12 src/Idris/Prover.hs+10−2 src/Idris/Reflection.hs+119−37 test/meta001/Finite.idr+26−24 test/tactics001/Tactics.idr+1−1
libs/base/Language/Reflection/Utils.idr+7−3
@@ -328,10 +328,14 @@ pure = id
328328--------------------------------------
329329-- Instances for definition reflection
330330--------------------------------------
331+instance Show Erasure where
332+ show Erased = "Erased"
333+ show NotErased = "NotErased"
334+
331335instance Show Arg where
332− show (Explicit n t) = "(Explicit " ++ show n ++ " " ++ show t ++ ")"
333− show (Implicit n t) = "(Implicit " ++ show n ++ " " ++ show t ++ ")"
334− show (Constraint n t) = "(Constraint " ++ show n ++ " " ++ show t ++ ")"
336+ show (Explicit n e t) = "(Explicit " ++ show n ++ " " ++ show e ++ " " ++ show t ++ ")"
337+ show (Implicit n e t) = "(Implicit " ++ show n ++ " " ++ show e ++ " " ++ show t ++ ")"
338+ show (Constraint n e t) = "(Constraint " ++ show n ++ " " ++ show e ++ " " ++ show t ++ ")"
335339
336340instance Show TyDecl where
337341 show (Declare fn args ret) = "(Declare " ++ show fn ++ " " ++
libs/prelude/Language/Reflection/Elab.idr+17−8
@@ -13,17 +13,21 @@ import Prelude.Maybe
1313import Prelude.Monad
1414import Language.Reflection
1515
16+||| Erasure annotations reflect Idris's idea of what is intended to be
17+||| erased.
18+data Erasure = Erased | NotErased
19+
1620||| Arguments, with plicity.
1721data Arg : Type where
1822 ||| An explicit argument
19− Explicit : TTName -> Raw -> Arg
23+ Explicit : TTName -> Erasure -> Raw -> Arg
2024
2125 ||| An implicit argument, to be solved by unification
22− Implicit : TTName -> Raw -> Arg
26+ Implicit : TTName -> Erasure -> Raw -> Arg
2327
2428 ||| A type-class constraint argument, to be solved by type class
2529 ||| resolution
26− Constraint : TTName -> Raw -> Arg
30+ Constraint : TTName -> Erasure -> Raw -> Arg
2731
2832||| A type declaration
2933data TyDecl : Type where
@@ -41,7 +45,6 @@ data TyDecl : Type where
4145||| A single pattern-matching clause
4246data FunClause : Type where
4347 MkFunClause : (lhs, rhs : Raw) -> FunClause
44− MkImpossibleClause : (lhs : Raw) -> FunClause
4548
4649||| A reflected function definition.
4750data FunDefn : Type where
@@ -50,10 +53,10 @@ data FunDefn : Type where
5053||| An argument to a type constructor.
5154data TyConArg : Type where
5255 ||| Parameters are consistent across all constructors of the type
53− Parameter : TTName -> Raw -> TyConArg
56+ Parameter : TTName -> Erasure -> Raw -> TyConArg
5457
5558 ||| Indices are allowed to vary across constructors
56− Index : TTName -> Raw -> TyConArg
59+ Index : TTName -> Erasure -> Raw -> TyConArg
5760
5861||| A reflected datatype definition
5962data Datatype : Type where
@@ -65,7 +68,7 @@ data Datatype : Type where
6568 ||| @ constrs the constructors, with their types
6669 MkDatatype : (familyName : TTName) ->
6770 (tyConArgs : List TyConArg) -> (tyConRes : Raw) ->
68− (constrs : List (TTName, Raw)) ->
71+ (constrs : List (TTName, List Arg, Raw)) ->
6972 Datatype
7073
7174||| A reflected elaboration script.
@@ -120,7 +123,7 @@ data Elab : Type -> Type where
120123 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)
121124
122125 prim__Debug : {a : Type} -> List ErrorReportPart -> Elab a
123−
126+ prim__Metavar : TTName -> Elab ()
124127
125128-------------
126129-- Public API
@@ -350,6 +353,12 @@ namespace Tactics
350353 debugMessage : (msg : List ErrorReportPart) -> Elab a
351354 debugMessage msg = prim__Debug msg
352355
356+ ||| Create a new top-level metavariable to solve the current hole.
357+ |||
358+ ||| @ name the name for the top-level variable
359+ metavar : (name : TTName) -> Elab ()
360+ metavar name = prim__Metavar name
361+
353362 ||| Recursively invoke the reflected elaborator with some goal.
354363 |||
355364 ||| The result is the final term and its type.
src/Idris/AbsSyntax.hs+9−8
@@ -1336,7 +1336,7 @@ addUsingImpls syn n fc t
13361336 bindFree (n:ns) tm
13371337 | elem n (map iname uimpls) = bindFree ns tm
13381338 | otherwise
1339− = PPi (Imp [] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)
1339+ = PPi (Imp [InaccessibleArg] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)
13401340
13411341 getArgnames (PPi _ n _ c sc)
13421342 = n : getArgnames sc
@@ -1376,8 +1376,9 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)
13761376-- argument position.
13771377
13781378-- This has become a right mess already. Better redo it some time...
1379−-- TODO: This is obsoleted by the new way of elaborating types, but there's still
1380−-- a couple of places which use it. Clean them up!
1379+-- TODO: This is obsoleted by the new way of elaborating types, (which
1380+-- calls addUsingImpls) but there's still a couple of places which use
1381+-- it. Clean them up!
13811382--
13821383-- Issue 1739 in the issue tracker
13831384-- https://github.com/idris-lang/Idris-dev/issues/1739
@@ -1512,9 +1513,10 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
15121513 pibind using [] sc = sc
15131514 pibind using (n:ns) sc
15141515 = case lookup n using of
1515− Just ty -> PPi (Imp [] Dynamic False Nothing) n NoFC ty (pibind using ns sc)
1516− Nothing -> PPi (Imp [] Dynamic False Nothing) n NoFC Placeholder
1517− (pibind using ns sc)
1516+ Just ty -> PPi (Imp [] Dynamic False Nothing)
1517+ n NoFC ty (pibind using ns sc)
1518+ Nothing -> PPi (Imp [InaccessibleArg] Dynamic False Nothing)
1519+ n NoFC Placeholder (pibind using ns sc)
15181520
15191521-- Add implicit arguments in function calls
15201522addImplPat :: IState -> PTerm -> PTerm
@@ -2091,9 +2093,8 @@ shadow n n' t = sm t where
20912093 sm (PNoImplicits x) = PNoImplicits (sm x)
20922094 sm x = x
20932095
2094−-- Rename any binders which are repeated (so that we don't have to mess
2096+-- | Rename any binders which are repeated (so that we don't have to mess
20952097-- about with shadowing anywhere else).
2096−
20972098mkUniqueNames :: [Name] -> PTerm -> PTerm
20982099mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
20992100 inScope :: S.Set Name
src/Idris/AbsSyntaxTree.hs+4
@@ -1675,6 +1675,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
16751675 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
16761676 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
16771677 prettySe d p bnd (PQuoteName n) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
1678+ prettySe d p bnd (PRunElab _ tm _) =
1679+ bracket p funcAppPrec . group . align . hang 2 $
1680+ text "%runElab" <$>
1681+ prettySe (decD d) funcAppPrec bnd tm
16781682
16791683 prettySe d p bnd _ = text "missing pretty-printer for term"
16801684
src/Idris/Elab/Term.hs+24−12
@@ -881,15 +881,11 @@ elab ist info emode opts fn tm
881881 -- names which have been used elsewhere in the term, since we
882882 -- won't be able to use them in the resulting application.
883883 let unique_used = getUniqueUsed (tt_ctxt ist) ptm
884− let n' = mkN n
884+ let n' = metavarName (namespace info) n
885885 attack
886886 defer unique_used n'
887887 solve
888888 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)
889− where mkN n@(NS _ _) = n
890− mkN n = case namespace info of
891− Just xs@(_:_) -> sNS n xs
892− _ -> n
893889 elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts
894890 elab' ina fc (PTactics ts)
895891 | not pattern = do mapM_ (runTac False ist fc fn) ts
@@ -1149,7 +1145,7 @@ elab ist info emode opts fn tm
11491145 focus n
11501146 elab' ina (Just fc') tm
11511147 env <- get_env
1152− runTactical ist (maybe fc' id fc) env (P Bound n' Erased) ns
1148+ runElabAction ist (maybe fc' id fc) env (P Bound n' Erased) ns
11531149 solve
11541150 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
11551151
@@ -1696,10 +1692,15 @@ case_ ind autoSolve ist fn tm = do
16961692 else casetac (forget val)
16971693 when autoSolve solveAll
16981694
1695+-- | Compute the appropriate name for a top-level metavariable
1696+metavarName :: Maybe [String] -> Name -> Name
1697+metavarName _ n@(NS _ _) = n
1698+metavarName (Just (ns@(_:_))) n = sNS n ns
1699+metavarName _ n = n
16991700
1700−runTactical :: IState -> FC -> Env -> Term -> [String] -> ElabD Term
1701−runTactical ist fc env tm ns = do tm' <- eval tm
1702− runTacTm tm'
1701+runElabAction :: IState -> FC -> Env -> Term -> [String] -> ElabD Term
1702+runElabAction ist fc env tm ns = do tm' <- eval tm
1703+ runTacTm tm'
17031704
17041705 where
17051706 eval tm = do ctxt <- get_context
@@ -1809,7 +1810,7 @@ runTactical ist fc env tm ns = do tm' <- eval tm
18091810 ctxt <- get_context
18101811 fmap fst . checkClosed $
18111812 rawList (Var (tacN "Datatype"))
1812− (map reflectDatatype (buildDatatypes ctxt datatypes n'))
1813+ (map reflectDatatype (buildDatatypes ist n'))
18131814 | n == tacN "prim__SourceLocation", [] <- args
18141815 = fmap fst . checkClosed $
18151816 reflectFC fc
@@ -1964,8 +1965,8 @@ runTactical ist fc env tm ns = do tm' <- eval tm
19641965 datatypes <- get_datatypes
19651966 env <- get_env
19661967 (_, ES (p, aux') _ _) <-
1967− lift $ runElab aux (runTactical ist fc [] script ns)
1968− (newProof recH ctxt datatypes goalTT)
1968+ lift $ runElab aux (runElabAction ist fc [] script ns)
1969+ (newProof recH ctxt datatypes goalTT)
19691970 let tm_out = getProofTerm (pterm p)
19701971 updateAux $ const aux'
19711972 env' <- get_env
@@ -1974,6 +1975,17 @@ runTactical ist fc env tm ns = do tm' <- eval tm
19741975 fmap fst . checkClosed $
19751976 rawPair (Var $ reflm "TT", Var $ reflm "TT")
19761977 (tm', ty')
1978+ | n == tacN "prim__Metavar", [n] <- args
1979+ = do n' <- reifyTTName n
1980+ ctxt <- get_context
1981+ ptm <- get_term
1982+ -- See documentation above in the elab case for PMetavar
1983+ let unique_used = getUniqueUsed ctxt ptm
1984+ let mvn = metavarName (Just ns) n'
1985+ attack
1986+ defer unique_used mvn
1987+ solve
1988+ returnUnit
19771989 | n == tacN "prim__Debug", [ty, msg] <- args
19781990 = do msg' <- eval msg
19791991 parts <- reifyReportParts msg
src/Idris/Prover.hs+10−2
@@ -1,6 +1,14 @@
11{-# LANGUAGE PatternGuards #-}
22module Idris.Prover (prover, showProof, showRunElab) where
33
4+-- Hack for GHC 7.10 and earlier compat without CPP or warnings
5+-- This exludes (<$>) as fmap, because wl-pprint uses it for newline
6+import Prelude (Eq(..), Show(..),
7+ Bool(..), Either(..), Maybe(..), String,
8+ (.), ($), (++),
9+ concatMap, id, elem, error, fst, flip, foldl, foldr, init,
10+ length, lines, map, not, null, repeat, reverse, tail, zip)
11+
412import Idris.Core.Elaborate hiding (Tactic(..))
513import Idris.Core.TT
614import Idris.Core.Evaluate
@@ -335,7 +343,7 @@ elabloop fn d prompt prf e prev h env
335343 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
336344 (_, e') <- elabStep e saveState -- enable :undo
337345 (res, e'') <- elabStep e' $
338− runTactical ist NoFC [] tm ["Shell"]
346+ runElabAction ist NoFC [] tm ["Shell"]
339347 ctxt <- getContext
340348 (v, vty) <- tclift $ check ctxt [] (forget res)
341349 let v' = normaliseAll ctxt [] v
@@ -346,7 +354,7 @@ elabloop fn d prompt prf e prev h env
346354 -- TODO: call elaborator with Elab () as goal here
347355 (_, e') <- elabStep e saveState -- enable :undo
348356 (_, e'') <- elabStep e' $
349− runTactical ist NoFC [] tm ["Shell"]
357+ runElabAction ist NoFC [] tm ["Shell"]
350358 return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))
351359 (\err -> return (False, prev, e, False, prf, env, Left err))
352360 idemodePutSExp "write-proof-state" (prf', length prf')
src/Idris/Reflection.hs+119−37
@@ -6,37 +6,44 @@ quoters and unquoters along with some supporting datatypes.
66module Idris.Reflection where
77
88import Control.Applicative ((<$>), (<*>), pure)
9−import Control.Monad (liftM, liftM2)
9+import Control.Monad (liftM, liftM2, liftM3)
1010import Data.Maybe (catMaybes)
1111import Data.List ((\\))
1212import qualified Data.Text as T
1313
1414import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,
1515 movelast, runElab, solve)
16−import Idris.Core.Evaluate (Context, Def(TyDecl), initContext, lookupDefExact, lookupTyExact)
16+import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact, lookupTyExact)
1717import Idris.Core.TT
1818
19−import Idris.AbsSyntaxTree (ElabD, IState, PArg'(..), PArg, PTactic, PTactic'(..),
20− PTerm(..), initEState, pairCon, pairTy)
19+import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes),
20+ PArg'(..), PArg, PTactic, PTactic'(..), PTerm(..),
21+ initEState, pairCon, pairTy)
2122import Idris.Delaborate (delab)
2223
23−data RArg = RExplicit { argName :: Name, argTy :: Raw }
24− | RImplicit { argName :: Name, argTy :: Raw }
25− | RConstraint { argName :: Name, argTy :: Raw }
24+data RErasure = RErased | RNotErased deriving Show
25+
26+data RArg = RExplicit { argName :: Name, argErased :: RErasure, argTy :: Raw }
27+ | RImplicit { argName :: Name, argErased :: RErasure, argTy :: Raw }
28+ | RConstraint { argName :: Name, argErased :: RErasure, argTy :: Raw }
2629 deriving Show
2730
2831data RTyDecl = RDeclare Name [RArg] Raw deriving Show
2932
30−data RTyConArg = RParameter { tcArgName :: Name, tcArgTy :: Raw }
31− | RIndex { tcArgName :: Name, tcArgTy :: Raw }
33+data RTyConArg = RParameter { tcArgName :: Name, tcArgErased :: RErasure, tcArgTy :: Raw }
34+ | RIndex { tcArgName :: Name, tcArgErased :: RErasure, tcArgTy :: Raw }
3235 deriving Show
3336
34−data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, Raw)] deriving Show
37+data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RArg], Raw)] deriving Show
38+
39+rArgOpts :: RErasure -> [ArgOpt]
40+rArgOpts RErased = [InaccessibleArg]
41+rArgOpts _ = []
3542
3643rArgToPArg :: RArg -> PArg
37−rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder
38−rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder
39−rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder
44+rArgToPArg (RExplicit n e _) = PExp 0 (rArgOpts e) n Placeholder
45+rArgToPArg (RImplicit n e _) = PImp 0 False (rArgOpts e) n Placeholder
46+rArgToPArg (RConstraint n e _) = PConstraint 0 (rArgOpts e) n Placeholder
4047
4148data RFunClause = RMkFunClause Raw Raw
4249 | RMkImpossibleClause Raw
@@ -154,8 +161,16 @@ reifyTTApp t [t', Constant (I i)]
154161 return $ Proj t'' i
155162reifyTTApp t [tt]
156163 | t == reflm "TType" = liftM TType (reifyTTUExp tt)
164+reifyTTApp t [tt]
165+ | t == reflm "UType" = liftM UType (reifyUniverse tt)
157166reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
158167
168+reifyUniverse :: Term -> ElabD Universe
169+reifyUniverse (P _ n _) | n == reflm "AllTypes" = return AllTypes
170+ | n == reflm "UniqueType" = return UniqueType
171+ | n == reflm "NullType" = return NullType
172+reifyUniverse tm = fail ("Unknown reflection universe: " ++ show tm)
173+
159174-- | Reify raw terms from their reflected representation
160175reifyRaw :: Term -> ElabD Raw
161176reifyRaw t@(App _ _ _)
@@ -780,6 +795,13 @@ rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
780795rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
781796rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
782797
798+-- | Idris tuples nest to the right
799+rawTripleTy :: Raw -> Raw -> Raw -> Raw
800+rawTripleTy a b c = rawPairTy a (rawPairTy b c)
801+
802+rawTriple :: (Raw, Raw, Raw) -> (Raw, Raw, Raw) -> Raw
803+rawTriple (a, b, c) (x, y, z) = rawPair (a, rawPairTy b c) (x, rawPair (b, c) (y, z))
804+
783805reflectCtxt :: [(Name, Type)] -> Raw
784806reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
785807 (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
@@ -929,6 +951,12 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
929951 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
930952reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
931953
954+reifyErasure :: Term -> ElabD RErasure
955+reifyErasure (P (DCon _ _ _) n _)
956+ | n == tacN "Erased" = return RErased
957+ | n == tacN "NotErased" = return RNotErased
958+reifyErasure tm = fail $ "Can't reify " ++ show tm ++ " as erasure info."
959+
932960reifyTyDecl :: Term -> ElabD RTyDecl
933961reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
934962 | n == tacN "Declare" =
@@ -939,14 +967,17 @@ reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
939967 ret' <- reifyRaw ret
940968 return $ RDeclare tyN' args' ret'
941969 where reifyRArg :: Term -> ElabD RArg
942− reifyRArg (App _ (App _ (P (DCon _ _ _) n _) argN) argTy)
943− | n == tacN "Explicit" = liftM2 RExplicit
970+ reifyRArg (App _ (App _ (App _ (P (DCon _ _ _) n _) argN) argE) argTy)
971+ | n == tacN "Explicit" = liftM3 RExplicit
944972 (reifyTTName argN)
973+ (reifyErasure argE)
945974 (reifyRaw argTy)
946− | n == tacN "Implicit" = liftM2 RImplicit
975+ | n == tacN "Implicit" = liftM3 RImplicit
947976 (reifyTTName argN)
948− (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint
977+ (reifyErasure argE)
978+ (reifyRaw argTy) | n == tacN "Constraint" = liftM3 RConstraint
949979 (reifyTTName argN)
980+ (reifyErasure argE)
950981 (reifyRaw argTy)
951982 reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
952983reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
@@ -975,38 +1006,89 @@ envTupleType
9751006 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
9761007 ]
9771008
1009+-- | Apply Idris's implicit info to get a signature. The [PArg] should
1010+-- come from a lookup in idris_implicits on IState.
1011+getArgs :: [PArg] -> Raw -> ([RArg], Raw)
1012+getArgs [] r = ([], r)
1013+getArgs (a:as) (RBind n (Pi _ ty _) sc) =
1014+ let (args, res) = getArgs as sc
1015+ erased = if InaccessibleArg `elem` argopts a then RErased else RNotErased
1016+ arg' = case a of
1017+ PImp {} -> RImplicit n erased ty
1018+ PExp {} -> RExplicit n erased ty
1019+ PConstraint {} -> RConstraint n erased ty
1020+ PTacImplicit {} -> RImplicit n erased ty -- TODO?
1021+ in (arg':args, res)
1022+getArgs _ r = ([], r)
1023+
9781024-- | Build the reflected datatype definition(s) that correspond(s) to
9791025-- a provided unqualified name
980−buildDatatypes :: Context -> Ctxt TypeInfo -> Name -> [RDatatype]
981−buildDatatypes ctxt datatypes n =
1026+buildDatatypes :: IState -> Name -> [RDatatype]
1027+buildDatatypes ist n =
9821028 catMaybes [ mkDataType dn ti
9831029 | (dn, ti) <- lookupCtxtName n datatypes
9841030 ]
985− where mkDataType name (TI {param_pos = params, con_names = constrs}) =
986− do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt
987− let (tcargs, tcres) = getArgs params (forget ty) 0
988− conTys <- mapM (fmap forget . flip lookupTyExact ctxt) constrs
989− return $ RDatatype name tcargs tcres $ zip constrs conTys
1031+ where datatypes = idris_datatypes ist
1032+ ctxt = tt_ctxt ist
1033+ impls = idris_implicits ist
9901034
991− getArgs params (RBind an (Pi _ ty _) body) i =
992− let (args, res) = getArgs params body (i+1)
1035+ ctorSig cn = do cty <- fmap forget (lookupTyExact cn ctxt)
1036+ argInfo <- lookupCtxtExact cn impls
1037+ let (args, res) = getArgs argInfo cty
1038+ return (cn, args, res)
1039+
1040+ mkDataType name (TI {param_pos = params, con_names = constrs}) =
1041+ do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt
1042+ implInfo <- lookupCtxtExact name impls
1043+ let (tcargs, tcres) = getTCArgs params implInfo (forget ty) 0
1044+ ctors <- mapM ctorSig constrs
1045+ return $ RDatatype name tcargs tcres ctors
1046+
1047+ getTCArgs params implInfo (RBind an (Pi _ ty _) body) i =
1048+ let (erased, implInfo') = case implInfo of
1049+ [] -> (RNotErased, [])
1050+ (a:as) -> (if InaccessibleArg `elem` argopts a
1051+ then RErased
1052+ else RNotErased,
1053+ as)
1054+ (args, res) = getTCArgs params implInfo' body (i+1)
9931055 in if i `elem` params
994− then (RParameter an ty : args, res )
995− else (RIndex an ty : args, res)
996− getArgs _ tm _ = ([], tm)
1056+ then (RParameter an erased ty : args, res )
1057+ else (RIndex an erased ty : args, res)
1058+ getTCArgs _ implInfo tm _ = ([], tm)
1059+
1060+reflectErasure :: RErasure -> Raw
1061+reflectErasure RErased = Var (tacN "Erased")
1062+reflectErasure RNotErased = Var (tacN "NotErased")
1063+
1064+reflectArg :: RArg -> Raw
1065+reflectArg arg =
1066+ RApp (RApp (RApp (Var con) (reflectName $ argName arg))
1067+ (reflectErasure $ argErased arg))
1068+ (reflectRaw $ argTy arg)
1069+ where con = case arg of
1070+ RExplicit{} -> tacN "Explicit"
1071+ RImplicit{} -> tacN "Implicit"
1072+ RConstraint{} -> tacN "Constraint"
9971073
9981074reflectDatatype :: RDatatype -> Raw
9991075reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
10001076 raw_apply (Var $ tacN "MkDatatype") [ reflectName tyn
10011077 , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)
10021078 , reflectRaw tyConRes
1003− , rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "Raw"))
1004− [ rawPair ((Var $ reflm "TTName"), (Var $ reflm "Raw"))
1005− (reflectName cn, reflectRaw cty)
1006− | (cn, cty) <- constrs
1079+ , rawList (rawTripleTy (Var $ reflm "TTName")
1080+ (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "Arg"))
1081+ (Var $ reflm "Raw"))
1082+ [ rawTriple ((Var $ reflm "TTName"),
1083+ (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "Arg")),
1084+ (Var $ reflm "Raw"))
1085+ (reflectName cn,
1086+ rawList (Var $ tacN "Arg") (map reflectArg cargs),
1087+ reflectRaw cty)
1088+ | (cn, cargs, cty) <- constrs
10071089 ]
10081090 ]
1009− where reflectConArg (RParameter n t) =
1010− raw_apply (Var $ tacN "Parameter") [reflectName n, reflectRaw t]
1011− reflectConArg (RIndex n t) =
1012− raw_apply (Var $ tacN "Index") [reflectName n, reflectRaw t]
1091+ where reflectConArg (RParameter n e t) =
1092+ raw_apply (Var $ tacN "Parameter") [reflectName n, reflectErasure e, reflectRaw t]
1093+ reflectConArg (RIndex n e t) =
1094+ raw_apply (Var $ tacN "Index") [reflectName n, reflectErasure e, reflectRaw t]
test/meta001/Finite.idr+26−24
@@ -27,42 +27,44 @@ mkFin (S k) Z = return `(FZ {k=~(quote k)})
2727mkFin (S k) (S j) = do i <- mkFin k j
2828 return `(FS {k=~(quote k)} ~i)
2929
30−mkToClause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
31−mkToClause fn size i (n, Var ty) =
30+mkToClause : TTName -> (size, i : Nat) ->
31+ (constr : (TTName, List Arg, Raw)) ->
32+ Elab FunClause
33+mkToClause fn size i (n, [], Var ty) =
3234 MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i
33−mkToClause fn size i (n, ty) =
35+mkToClause fn size i (n, _, ty) =
3436 fail [TextPart "unsupported constructor", NamePart n]
3537
3638
3739mkFromClause : TTName -> (size, i : Nat) ->
38− (constr : (TTName, Raw)) ->
40+ (constr : (TTName, List Arg, Raw)) ->
3941 Elab FunClause
40−mkFromClause fn size i (n, Var ty) =
42+mkFromClause fn size i (n, [], Var ty) =
4143 return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)
42−mkFromClause fn size i (n, ty) =
44+mkFromClause fn size i (n, _, ty) =
4345 fail [TextPart "unsupported constructor", NamePart n]
4446
4547
46−mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
47−mkOk1Clause fn size i (n, Var ty) =
48+mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List Arg, Raw)) -> Elab FunClause
49+mkOk1Clause fn size i (n, [], Var ty) =
4850 return $ MkFunClause (RApp (Var fn) (Var n))
4951 [| (Var (UN "Refl")) (Var ty) (Var n) |]
50−mkOk1Clause fn size i (n, ty) =
52+mkOk1Clause fn size i (n, _, ty) =
5153 fail [TextPart "unsupported constructor", NamePart n]
5254
5355
54−mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause
55−mkOk2Clause fn size i (n, Var ty) =
56+mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List Arg, Raw)) -> Elab FunClause
57+mkOk2Clause fn size i (n, [], Var ty) =
5658 return $ MkFunClause (RApp (Var fn) !(mkFin size i))
5759 [| (Var "Refl") `(Fin ~(quote size))
5860 !(mkFin size i) |]
59−mkOk2Clause fn size i (n, ty) =
61+mkOk2Clause fn size i (n, _, ty) =
6062 fail [TextPart "unsupported constructor", NamePart n]
6163
6264
63−mkToClauses : TTName -> Nat -> List (TTName, Raw) -> Elab (List FunClause)
65+mkToClauses : TTName -> Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
6466mkToClauses fn size xs = mkToClauses' Z xs
65− where mkToClauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
67+ where mkToClauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
6668 mkToClauses' k [] = return []
6769 mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs
6870 clause <- mkToClause fn size k x
@@ -90,26 +92,26 @@ mkAbsurdFinClause fn goal size =
9092
9193
9294mkFromClauses : TTName -> TTName -> Nat ->
93− List (TTName, Raw) -> Elab (List FunClause)
95+ List (TTName, List Arg, Raw) -> Elab (List FunClause)
9496mkFromClauses fn ty size xs = mkFromClauses' Z xs
95− where mkFromClauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
97+ where mkFromClauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
9698 mkFromClauses' k [] =
9799 return [!(mkAbsurdFinClause fn (const (Var ty)) size)]
98100 mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs
99101 clause <- mkFromClause fn size k x
100102 return $ clause :: rest
101103
102−mkOk1Clauses : TTName -> Nat -> List (TTName, Raw) -> Elab (List FunClause)
104+mkOk1Clauses : TTName -> Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
103105mkOk1Clauses fn size xs = mkOk1Clauses' Z xs
104− where mkOk1Clauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
106+ where mkOk1Clauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
105107 mkOk1Clauses' k [] = return []
106108 mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs
107109 clause <- mkOk1Clause fn size k x
108110 return $ clause :: rest
109111
110−mkOk2Clauses : TTName -> Nat -> List (TTName, Raw) -> (Raw -> Raw) -> Elab (List FunClause)
112+mkOk2Clauses : TTName -> Nat -> List (TTName, List Arg, Raw) -> (Raw -> Raw) -> Elab (List FunClause)
111113mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs
112− where mkOk2Clauses' : Nat -> List (TTName, Raw) -> Elab (List FunClause)
114+ where mkOk2Clauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)
113115 mkOk2Clauses' k [] = return [!(mkAbsurdFinClause fn resTy size)]
114116 mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs
115117 clause <- mkOk2Clause fn size k x
@@ -121,19 +123,19 @@ genToFin to from ok1 ok2 ty =
121123 do (MkDatatype famn tcargs tcres constrs) <- lookupDatatypeExact ty
122124 let size = length constrs
123125 argn <- gensym "arg"
124− declareType $ Declare to [Explicit argn (Var ty)]
126+ declareType $ Declare to [Explicit argn NotErased (Var ty)]
125127 `(Fin ~(quote size))
126128 toClauses <- mkToClauses to size constrs
127129 defineFunction $ DefineFun to toClauses
128130
129131 argn' <- gensym "arg"
130− declareType $ Declare from [Explicit argn' `(Fin ~(quote size))]
132+ declareType $ Declare from [Explicit argn' NotErased `(Fin ~(quote size))]
131133 (Var ty)
132134 fromClauses <- mkFromClauses from ty size constrs
133135 defineFunction $ DefineFun from fromClauses
134136
135137 argn'' <- gensym "arg"
136− declareType $ Declare ok1 [Explicit argn'' (Var ty)]
138+ declareType $ Declare ok1 [Explicit argn'' NotErased (Var ty)]
137139 `((=) {A=~(Var ty)} {B=~(Var ty)}
138140 ~(RApp (Var from) (RApp (Var to) (Var argn'')))
139141 ~(Var argn''))
@@ -146,7 +148,7 @@ genToFin to from ok1 ok2 ty =
146148 (\n => `((=) {A=~fty} {B=~fty}
147149 ~(RApp (Var to) (RApp (Var from) n))
148150 ~n))
149− declareType $ Declare ok2 [Explicit argn''' fty]
151+ declareType $ Declare ok2 [Explicit argn''' NotErased fty]
150152 (ok2ResTy (Var argn'''))
151153 ok2Clauses <- mkOk2Clauses ok2 size constrs ok2ResTy
152154 defineFunction $ DefineFun ok2 ok2Clauses
test/tactics001/Tactics.idr+1−1
@@ -33,7 +33,7 @@ plusSuccRightSuccNew (S j) k =
3333
3434mkDecl : ()
3535mkDecl = %runElab (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])
36− [Implicit (UN "z") `(Nat)]
36+ [Implicit (UN "z") NotErased `(Nat)]
3737 `(Vect ~(Var (UN "z")) ())
3838 fill `(() : ())
3939 solve)