f96ccde · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2367 from david-christiansen/wip/tactical

f96ccdeDavid Christiansen11 years ago

libs/base/Language/Reflection/Utils.idr+7−3

compare with master

unifiedsplit

@@ -328,10 +328,14 @@ pure = id

328--------------------------------------

329-- Instances for definition reflection

330--------------------------------------

331+instance Show Erasure where

332+ show Erased = "Erased"

333+ show NotErased = "NotErased"

334+

331instance Show Arg where

335instance Show Arg where

332− show (Explicit n t) = "(Explicit " ++ show n ++ " " ++ show t ++ ")"

336+ show (Explicit n e t) = "(Explicit " ++ show n ++ " " ++ show e ++ " " ++ show t ++ ")"

333− show (Implicit n t) = "(Implicit " ++ show n ++ " " ++ show t ++ ")"

337+ show (Implicit n e t) = "(Implicit " ++ show n ++ " " ++ show e ++ " " ++ show t ++ ")"

334− show (Constraint n t) = "(Constraint " ++ show n ++ " " ++ show t ++ ")"

338+ show (Constraint n e t) = "(Constraint " ++ show n ++ " " ++ show e ++ " " ++ show t ++ ")"

335

339

336instance Show TyDecl where

340instance Show TyDecl where

337 show (Declare fn args ret) = "(Declare " ++ show fn ++ " " ++

341 show (Declare fn args ret) = "(Declare " ++ show fn ++ " " ++

libs/prelude/Language/Reflection/Elab.idr+17−8

@@ -13,17 +13,21 @@ import Prelude.Maybe

13import Prelude.Monad

14import Language.Reflection

16+||| Erasure annotations reflect Idris's idea of what is intended to be

17+||| erased.

18+data Erasure = Erased | NotErased

19+

16||| Arguments, with plicity.

20||| Arguments, with plicity.

17data Arg : Type where

21data Arg : Type where

18 ||| An explicit argument

22 ||| An explicit argument

19− Explicit : TTName -> Raw -> Arg

23+ Explicit : TTName -> Erasure -> Raw -> Arg

21 ||| An implicit argument, to be solved by unification

25 ||| An implicit argument, to be solved by unification

22− Implicit : TTName -> Raw -> Arg

26+ Implicit : TTName -> Erasure -> Raw -> Arg

24 ||| A type-class constraint argument, to be solved by type class

28 ||| A type-class constraint argument, to be solved by type class

25 ||| resolution

29 ||| resolution

26− Constraint : TTName -> Raw -> Arg

30+ Constraint : TTName -> Erasure -> Raw -> Arg

28||| A type declaration

32||| A type declaration

29data TyDecl : Type where

33data TyDecl : Type where

@@ -41,7 +45,6 @@ data TyDecl : Type where

41||| A single pattern-matching clause

45||| A single pattern-matching clause

42data FunClause : Type where

46data FunClause : Type where

43 MkFunClause : (lhs, rhs : Raw) -> FunClause

47 MkFunClause : (lhs, rhs : Raw) -> FunClause

44− MkImpossibleClause : (lhs : Raw) -> FunClause

46||| A reflected function definition.

49||| A reflected function definition.

47data FunDefn : Type where

50data FunDefn : Type where

@@ -50,10 +53,10 @@ data FunDefn : Type where

50||| An argument to a type constructor.

53||| An argument to a type constructor.

51data TyConArg : Type where

54data TyConArg : Type where

52 ||| Parameters are consistent across all constructors of the type

55 ||| Parameters are consistent across all constructors of the type

53− Parameter : TTName -> Raw -> TyConArg

56+ Parameter : TTName -> Erasure -> Raw -> TyConArg

55 ||| Indices are allowed to vary across constructors

58 ||| Indices are allowed to vary across constructors

56− Index : TTName -> Raw -> TyConArg

59+ Index : TTName -> Erasure -> Raw -> TyConArg

58||| A reflected datatype definition

61||| A reflected datatype definition

59data Datatype : Type where

62data Datatype : Type where

@@ -65,7 +68,7 @@ data Datatype : Type where

65 ||| @ constrs the constructors, with their types

68 ||| @ constrs the constructors, with their types

66 MkDatatype : (familyName : TTName) ->

69 MkDatatype : (familyName : TTName) ->

67 (tyConArgs : List TyConArg) -> (tyConRes : Raw) ->

70 (tyConArgs : List TyConArg) -> (tyConRes : Raw) ->

68− (constrs : List (TTName, Raw)) ->

71+ (constrs : List (TTName, List Arg, Raw)) ->

69 Datatype

72 Datatype

71||| A reflected elaboration script.

74||| A reflected elaboration script.

@@ -120,7 +123,7 @@ data Elab : Type -> Type where

120 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)

123 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)

121

124

122 prim__Debug : {a : Type} -> List ErrorReportPart -> Elab a

125 prim__Debug : {a : Type} -> List ErrorReportPart -> Elab a

123−

126+ prim__Metavar : TTName -> Elab ()

124

127

125-------------

128-------------

126-- Public API

129-- Public API

@@ -350,6 +353,12 @@ namespace Tactics

350 debugMessage : (msg : List ErrorReportPart) -> Elab a

353 debugMessage : (msg : List ErrorReportPart) -> Elab a

351 debugMessage msg = prim__Debug msg

354 debugMessage msg = prim__Debug msg

352

355

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+

353 ||| Recursively invoke the reflected elaborator with some goal.

362 ||| Recursively invoke the reflected elaborator with some goal.

354 |||

363 |||

355 ||| The result is the final term and its type.

364 ||| The result is the final term and its type.

src/Idris/AbsSyntax.hs+9−8

@@ -1336,7 +1336,7 @@ addUsingImpls syn n fc t

1336 bindFree (n:ns) tm

1337 | elem n (map iname uimpls) = bindFree ns tm

1338 | 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)

1340

1341 getArgnames (PPi _ n _ c sc)

1342 = n : getArgnames sc

@@ -1376,8 +1376,9 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

1376-- argument position.

1377

1378-- 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

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

1380−-- a couple of places which use it. Clean them up!

1381+-- it. Clean them up!

1381--

1382--

1382-- Issue 1739 in the issue tracker

1383-- Issue 1739 in the issue tracker

1383-- https://github.com/idris-lang/Idris-dev/issues/1739

1384-- https://github.com/idris-lang/Idris-dev/issues/1739

@@ -1512,9 +1513,10 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1512 pibind using [] sc = sc

1513 pibind using [] sc = sc

1513 pibind using (n:ns) sc

1514 pibind using (n:ns) sc

1514 = case lookup n using of

1515 = case lookup n using of

1515− Just ty -> PPi (Imp [] Dynamic False Nothing) n NoFC ty (pibind using ns sc)

1516+ Just ty -> PPi (Imp [] Dynamic False Nothing)

1517+ n NoFC ty (pibind using ns sc)

1516− Nothing -> PPi (Imp [] Dynamic False Nothing) n NoFC Placeholder

1518+ Nothing -> PPi (Imp [InaccessibleArg] Dynamic False Nothing)

1517− (pibind using ns sc)

1519+ n NoFC Placeholder (pibind using ns sc)

1518

1520

1519-- Add implicit arguments in function calls

1521-- Add implicit arguments in function calls

1520addImplPat :: IState -> PTerm -> PTerm

1522addImplPat :: IState -> PTerm -> PTerm

@@ -2091,9 +2093,8 @@ shadow n n' t = sm t where

2091 sm (PNoImplicits x) = PNoImplicits (sm x)

2093 sm (PNoImplicits x) = PNoImplicits (sm x)

2092 sm x = x

2094 sm x = x

2093

2095

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

2095-- about with shadowing anywhere else).

2097-- about with shadowing anywhere else).

2096−

2097mkUniqueNames :: [Name] -> PTerm -> PTerm

2098mkUniqueNames :: [Name] -> PTerm -> PTerm

2098mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

2099mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

2099 inScope :: S.Set Name

2100 inScope :: S.Set Name

src/Idris/AbsSyntaxTree.hs+4

@@ -1675,6 +1675,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1675 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"

1676 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t

1677 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

1678

1682

1679 prettySe d p bnd _ = text "missing pretty-printer for term"

1683 prettySe d p bnd _ = text "missing pretty-printer for term"

1680

1684

src/Idris/Elab/Term.hs+24−12

@@ -881,15 +881,11 @@ elab ist info emode opts fn tm

881 -- names which have been used elsewhere in the term, since we

882 -- won't be able to use them in the resulting application.

883 let unique_used = getUniqueUsed (tt_ctxt ist) ptm

884− let n' = mkN n

884+ let n' = metavarName (namespace info) n

885 attack

886 defer unique_used n'

887 solve

888 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

893 elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts

889 elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts

894 elab' ina fc (PTactics ts)

890 elab' ina fc (PTactics ts)

895 | not pattern = do mapM_ (runTac False ist fc fn) ts

891 | not pattern = do mapM_ (runTac False ist fc fn) ts

@@ -1149,7 +1145,7 @@ elab ist info emode opts fn tm

1149 focus n

1145 focus n

1150 elab' ina (Just fc') tm

1146 elab' ina (Just fc') tm

1151 env <- get_env

1147 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

1153 solve

1149 solve

1154 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1150 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1155

1151

@@ -1696,10 +1692,15 @@ case_ ind autoSolve ist fn tm = do

1696 else casetac (forget val)

1692 else casetac (forget val)

1697 when autoSolve solveAll

1693 when autoSolve solveAll

1698

1694

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

1699

1700

1700−runTactical :: IState -> FC -> Env -> Term -> [String] -> ElabD Term

1701+runElabAction :: IState -> FC -> Env -> Term -> [String] -> ElabD Term

1701−runTactical ist fc env tm ns = do tm' <- eval tm

1702+runElabAction ist fc env tm ns = do tm' <- eval tm

1702− runTacTm tm'

1703+ runTacTm tm'

1703

1704

1704 where

1705 where

1705 eval tm = do ctxt <- get_context

1706 eval tm = do ctxt <- get_context

@@ -1809,7 +1810,7 @@ runTactical ist fc env tm ns = do tm' <- eval tm

1809 ctxt <- get_context

1810 ctxt <- get_context

1810 fmap fst . checkClosed $

1811 fmap fst . checkClosed $

1811 rawList (Var (tacN "Datatype"))

1812 rawList (Var (tacN "Datatype"))

1812− (map reflectDatatype (buildDatatypes ctxt datatypes n'))

1813+ (map reflectDatatype (buildDatatypes ist n'))

1813 | n == tacN "prim__SourceLocation", [] <- args

1814 | n == tacN "prim__SourceLocation", [] <- args

1814 = fmap fst . checkClosed $

1815 = fmap fst . checkClosed $

1815 reflectFC fc

1816 reflectFC fc

@@ -1964,8 +1965,8 @@ runTactical ist fc env tm ns = do tm' <- eval tm

1964 datatypes <- get_datatypes

1965 datatypes <- get_datatypes

1965 env <- get_env

1966 env <- get_env

1966 (_, ES (p, aux') _ _) <-

1967 (_, ES (p, aux') _ _) <-

1967− lift $ runElab aux (runTactical ist fc [] script ns)

1968+ lift $ runElab aux (runElabAction ist fc [] script ns)

1968− (newProof recH ctxt datatypes goalTT)

1969+ (newProof recH ctxt datatypes goalTT)

1969 let tm_out = getProofTerm (pterm p)

1970 let tm_out = getProofTerm (pterm p)

1970 updateAux $ const aux'

1971 updateAux $ const aux'

1971 env' <- get_env

1972 env' <- get_env

@@ -1974,6 +1975,17 @@ runTactical ist fc env tm ns = do tm' <- eval tm

1974 fmap fst . checkClosed $

1975 fmap fst . checkClosed $

1975 rawPair (Var $ reflm "TT", Var $ reflm "TT")

1976 rawPair (Var $ reflm "TT", Var $ reflm "TT")

1976 (tm', ty')

1977 (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

1977 | n == tacN "prim__Debug", [ty, msg] <- args

1989 | n == tacN "prim__Debug", [ty, msg] <- args

1978 = do msg' <- eval msg

1990 = do msg' <- eval msg

1979 parts <- reifyReportParts msg

1991 parts <- reifyReportParts msg

src/Idris/Prover.hs+10−2

@@ -1,6 +1,14 @@

1{-# LANGUAGE PatternGuards #-}

2module Idris.Prover (prover, showProof, showRunElab) where

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+

4import Idris.Core.Elaborate hiding (Tactic(..))

12import Idris.Core.Elaborate hiding (Tactic(..))

5import Idris.Core.TT

13import Idris.Core.TT

6import Idris.Core.Evaluate

14import Idris.Core.Evaluate

@@ -335,7 +343,7 @@ elabloop fn d prompt prf e prev h env

335 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)

343 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)

336 (_, e') <- elabStep e saveState -- enable :undo

344 (_, e') <- elabStep e saveState -- enable :undo

337 (res, e'') <- elabStep e' $

345 (res, e'') <- elabStep e' $

338− runTactical ist NoFC [] tm ["Shell"]

346+ runElabAction ist NoFC [] tm ["Shell"]

339 ctxt <- getContext

347 ctxt <- getContext

340 (v, vty) <- tclift $ check ctxt [] (forget res)

348 (v, vty) <- tclift $ check ctxt [] (forget res)

341 let v' = normaliseAll ctxt [] v

349 let v' = normaliseAll ctxt [] v

@@ -346,7 +354,7 @@ elabloop fn d prompt prf e prev h env

346 -- TODO: call elaborator with Elab () as goal here

354 -- TODO: call elaborator with Elab () as goal here

347 (_, e') <- elabStep e saveState -- enable :undo

355 (_, e') <- elabStep e saveState -- enable :undo

348 (_, e'') <- elabStep e' $

356 (_, e'') <- elabStep e' $

349− runTactical ist NoFC [] tm ["Shell"]

357+ runElabAction ist NoFC [] tm ["Shell"]

350 return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))

358 return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))

351 (\err -> return (False, prev, e, False, prf, env, Left err))

359 (\err -> return (False, prev, e, False, prf, env, Left err))

352 idemodePutSExp "write-proof-state" (prf', length prf')

360 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.

6module Idris.Reflection where

8import Control.Applicative ((<$>), (<*>), pure)

9−import Control.Monad (liftM, liftM2)

9+import Control.Monad (liftM, liftM2, liftM3)

10import Data.Maybe (catMaybes)

11import Data.List ((\\))

12import qualified Data.Text as T

14import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,

15 movelast, runElab, solve)

16−import Idris.Core.Evaluate (Context, Def(TyDecl), initContext, lookupDefExact, lookupTyExact)

16+import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact, lookupTyExact)

17import Idris.Core.TT

19+import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes),

19−import Idris.AbsSyntaxTree (ElabD, IState, PArg'(..), PArg, PTactic, PTactic'(..),

20+ PArg'(..), PArg, PTactic, PTactic'(..), PTerm(..),

20− PTerm(..), initEState, pairCon, pairTy)

21+ initEState, pairCon, pairTy)

21import Idris.Delaborate (delab)

22import Idris.Delaborate (delab)

24+data RErasure = RErased | RNotErased deriving Show

25+

23−data RArg = RExplicit { argName :: Name, argTy :: Raw }

26+data RArg = RExplicit { argName :: Name, argErased :: RErasure, argTy :: Raw }

24− | RImplicit { argName :: Name, argTy :: Raw }

27+ | RImplicit { argName :: Name, argErased :: RErasure, argTy :: Raw }

25− | RConstraint { argName :: Name, argTy :: Raw }

28+ | RConstraint { argName :: Name, argErased :: RErasure, argTy :: Raw }

26 deriving Show

29 deriving Show

28data RTyDecl = RDeclare Name [RArg] Raw deriving Show

31data RTyDecl = RDeclare Name [RArg] Raw deriving Show

30−data RTyConArg = RParameter { tcArgName :: Name, tcArgTy :: Raw }

33+data RTyConArg = RParameter { tcArgName :: Name, tcArgErased :: RErasure, tcArgTy :: Raw }

31− | RIndex { tcArgName :: Name, tcArgTy :: Raw }

34+ | RIndex { tcArgName :: Name, tcArgErased :: RErasure, tcArgTy :: Raw }

32 deriving Show

35 deriving Show

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 _ = []

36rArgToPArg :: RArg -> PArg

43rArgToPArg :: RArg -> PArg

37−rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder

44+rArgToPArg (RExplicit n e _) = PExp 0 (rArgOpts e) n Placeholder

38−rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder

45+rArgToPArg (RImplicit n e _) = PImp 0 False (rArgOpts e) n Placeholder

39−rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder

46+rArgToPArg (RConstraint n e _) = PConstraint 0 (rArgOpts e) n Placeholder

41data RFunClause = RMkFunClause Raw Raw

48data RFunClause = RMkFunClause Raw Raw

42 | RMkImpossibleClause Raw

49 | RMkImpossibleClause Raw

@@ -154,8 +161,16 @@ reifyTTApp t [t', Constant (I i)]

154 return $ Proj t'' i

161 return $ Proj t'' i

155reifyTTApp t [tt]

162reifyTTApp t [tt]

156 | t == reflm "TType" = liftM TType (reifyTTUExp tt)

163 | t == reflm "TType" = liftM TType (reifyTTUExp tt)

164+reifyTTApp t [tt]

165+ | t == reflm "UType" = liftM UType (reifyUniverse tt)

157reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))

166reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))

158

167

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+

159-- | Reify raw terms from their reflected representation

174-- | Reify raw terms from their reflected representation

160reifyRaw :: Term -> ElabD Raw

175reifyRaw :: Term -> ElabD Raw

161reifyRaw t@(App _ _ _)

176reifyRaw t@(App _ _ _)

@@ -780,6 +795,13 @@ rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]

780rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw

795rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw

781rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]

796rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]

782

797

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+

783reflectCtxt :: [(Name, Type)] -> Raw

805reflectCtxt :: [(Name, Type)] -> Raw

784reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))

806reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))

785 (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")

807 (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")

@@ -929,6 +951,12 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

929 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

951 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

930reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

952reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

931

953

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+

932reifyTyDecl :: Term -> ElabD RTyDecl

960reifyTyDecl :: Term -> ElabD RTyDecl

933reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)

961reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)

934 | n == tacN "Declare" =

962 | n == tacN "Declare" =

@@ -939,14 +967,17 @@ reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)

939 ret' <- reifyRaw ret

967 ret' <- reifyRaw ret

940 return $ RDeclare tyN' args' ret'

968 return $ RDeclare tyN' args' ret'

941 where reifyRArg :: Term -> ElabD RArg

969 where reifyRArg :: Term -> ElabD RArg

942− reifyRArg (App _ (App _ (P (DCon _ _ _) n _) argN) argTy)

970+ reifyRArg (App _ (App _ (App _ (P (DCon _ _ _) n _) argN) argE) argTy)

943− | n == tacN "Explicit" = liftM2 RExplicit

971+ | n == tacN "Explicit" = liftM3 RExplicit

944 (reifyTTName argN)

972 (reifyTTName argN)

973+ (reifyErasure argE)

945 (reifyRaw argTy)

974 (reifyRaw argTy)

946− | n == tacN "Implicit" = liftM2 RImplicit

975+ | n == tacN "Implicit" = liftM3 RImplicit

947 (reifyTTName argN)

976 (reifyTTName argN)

977+ (reifyErasure argE)

948− (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint

978+ (reifyRaw argTy) | n == tacN "Constraint" = liftM3 RConstraint

949 (reifyTTName argN)

979 (reifyTTName argN)

980+ (reifyErasure argE)

950 (reifyRaw argTy)

981 (reifyRaw argTy)

951 reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."

982 reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."

952reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

983reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

@@ -975,38 +1006,89 @@ envTupleType

975 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))

1006 , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))

976 ]

1007 ]

977

1008

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+

978-- | Build the reflected datatype definition(s) that correspond(s) to

1024-- | Build the reflected datatype definition(s) that correspond(s) to

979-- a provided unqualified name

1025-- a provided unqualified name

980−buildDatatypes :: Context -> Ctxt TypeInfo -> Name -> [RDatatype]

1026+buildDatatypes :: IState -> Name -> [RDatatype]

981−buildDatatypes ctxt datatypes n =

1027+buildDatatypes ist n =

982 catMaybes [ mkDataType dn ti

1028 catMaybes [ mkDataType dn ti

983 | (dn, ti) <- lookupCtxtName n datatypes

1029 | (dn, ti) <- lookupCtxtName n datatypes

984 ]

1030 ]

985− where mkDataType name (TI {param_pos = params, con_names = constrs}) =

1031+ where datatypes = idris_datatypes ist

986− do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt

1032+ ctxt = tt_ctxt ist

987− let (tcargs, tcres) = getArgs params (forget ty) 0

1033+ impls = idris_implicits ist

988− conTys <- mapM (fmap forget . flip lookupTyExact ctxt) constrs

989− return $ RDatatype name tcargs tcres $ zip constrs conTys

990

1034

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+

991− getArgs params (RBind an (Pi _ ty _) body) i =

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)

992− let (args, res) = getArgs params body (i+1)

1054+ (args, res) = getTCArgs params implInfo' body (i+1)

993 in if i `elem` params

1055 in if i `elem` params

994− then (RParameter an ty : args, res )

1056+ then (RParameter an erased ty : args, res )

995− else (RIndex an ty : args, res)

1057+ else (RIndex an erased ty : args, res)

996− getArgs _ tm _ = ([], tm)

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"

997

1073

998reflectDatatype :: RDatatype -> Raw

1074reflectDatatype :: RDatatype -> Raw

999reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =

1075reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =

1000 raw_apply (Var $ tacN "MkDatatype") [ reflectName tyn

1076 raw_apply (Var $ tacN "MkDatatype") [ reflectName tyn

1001 , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)

1077 , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)

1002 , reflectRaw tyConRes

1078 , reflectRaw tyConRes

1003− , rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "Raw"))

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")),

1004− [ rawPair ((Var $ reflm "TTName"), (Var $ reflm "Raw"))

1084+ (Var $ reflm "Raw"))

1005− (reflectName cn, reflectRaw cty)

1085+ (reflectName cn,

1086+ rawList (Var $ tacN "Arg") (map reflectArg cargs),

1087+ reflectRaw cty)

1006− | (cn, cty) <- constrs

1088+ | (cn, cargs, cty) <- constrs

1007 ]

1089 ]

1008 ]

1090 ]

1009− where reflectConArg (RParameter n t) =

1091+ where reflectConArg (RParameter n e t) =

1010− raw_apply (Var $ tacN "Parameter") [reflectName n, reflectRaw t]

1092+ raw_apply (Var $ tacN "Parameter") [reflectName n, reflectErasure e, reflectRaw t]

1011− reflectConArg (RIndex n t) =

1093+ reflectConArg (RIndex n e t) =

1012− raw_apply (Var $ tacN "Index") [reflectName n, reflectRaw 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)})

27mkFin (S k) (S j) = do i <- mkFin k j

28 return `(FS {k=~(quote k)} ~i)

30−mkToClause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause

30+mkToClause : TTName -> (size, i : Nat) ->

31+ (constr : (TTName, List Arg, Raw)) ->

32+ Elab FunClause

31−mkToClause fn size i (n, Var ty) =

33+mkToClause fn size i (n, [], Var ty) =

32 MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i

34 MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i

33−mkToClause fn size i (n, ty) =

35+mkToClause fn size i (n, _, ty) =

34 fail [TextPart "unsupported constructor", NamePart n]

36 fail [TextPart "unsupported constructor", NamePart n]

37mkFromClause : TTName -> (size, i : Nat) ->

39mkFromClause : TTName -> (size, i : Nat) ->

38− (constr : (TTName, Raw)) ->

40+ (constr : (TTName, List Arg, Raw)) ->

39 Elab FunClause

41 Elab FunClause

40−mkFromClause fn size i (n, Var ty) =

42+mkFromClause fn size i (n, [], Var ty) =

41 return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)

43 return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)

42−mkFromClause fn size i (n, ty) =

44+mkFromClause fn size i (n, _, ty) =

43 fail [TextPart "unsupported constructor", NamePart n]

45 fail [TextPart "unsupported constructor", NamePart n]

46−mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause

48+mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List Arg, Raw)) -> Elab FunClause

47−mkOk1Clause fn size i (n, Var ty) =

49+mkOk1Clause fn size i (n, [], Var ty) =

48 return $ MkFunClause (RApp (Var fn) (Var n))

50 return $ MkFunClause (RApp (Var fn) (Var n))

49 [| (Var (UN "Refl")) (Var ty) (Var n) |]

51 [| (Var (UN "Refl")) (Var ty) (Var n) |]

50−mkOk1Clause fn size i (n, ty) =

52+mkOk1Clause fn size i (n, _, ty) =

51 fail [TextPart "unsupported constructor", NamePart n]

53 fail [TextPart "unsupported constructor", NamePart n]

54−mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, Raw)) -> Elab FunClause

56+mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List Arg, Raw)) -> Elab FunClause

55−mkOk2Clause fn size i (n, Var ty) =

57+mkOk2Clause fn size i (n, [], Var ty) =

56 return $ MkFunClause (RApp (Var fn) !(mkFin size i))

58 return $ MkFunClause (RApp (Var fn) !(mkFin size i))

57 [| (Var "Refl") `(Fin ~(quote size))

59 [| (Var "Refl") `(Fin ~(quote size))

58 !(mkFin size i) |]

60 !(mkFin size i) |]

59−mkOk2Clause fn size i (n, ty) =

61+mkOk2Clause fn size i (n, _, ty) =

60 fail [TextPart "unsupported constructor", NamePart n]

62 fail [TextPart "unsupported constructor", NamePart n]

63−mkToClauses : TTName -> Nat -> List (TTName, Raw) -> Elab (List FunClause)

65+mkToClauses : TTName -> Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)

64mkToClauses fn size xs = mkToClauses' Z xs

66mkToClauses 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)

66 mkToClauses' k [] = return []

68 mkToClauses' k [] = return []

67 mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs

69 mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs

68 clause <- mkToClause fn size k x

70 clause <- mkToClause fn size k x

@@ -90,26 +92,26 @@ mkAbsurdFinClause fn goal size =

92mkFromClauses : TTName -> TTName -> Nat ->

94mkFromClauses : TTName -> TTName -> Nat ->

93− List (TTName, Raw) -> Elab (List FunClause)

95+ List (TTName, List Arg, Raw) -> Elab (List FunClause)

94mkFromClauses fn ty size xs = mkFromClauses' Z xs

96mkFromClauses 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)

96 mkFromClauses' k [] =

98 mkFromClauses' k [] =

97 return [!(mkAbsurdFinClause fn (const (Var ty)) size)]

99 return [!(mkAbsurdFinClause fn (const (Var ty)) size)]

98 mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs

100 mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs

99 clause <- mkFromClause fn size k x

101 clause <- mkFromClause fn size k x

100 return $ clause :: rest

102 return $ clause :: rest

101

103

102−mkOk1Clauses : TTName -> Nat -> List (TTName, Raw) -> Elab (List FunClause)

104+mkOk1Clauses : TTName -> Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)

103mkOk1Clauses fn size xs = mkOk1Clauses' Z xs

105mkOk1Clauses 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)

105 mkOk1Clauses' k [] = return []

107 mkOk1Clauses' k [] = return []

106 mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs

108 mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs

107 clause <- mkOk1Clause fn size k x

109 clause <- mkOk1Clause fn size k x

108 return $ clause :: rest

110 return $ clause :: rest

109

111

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)

111mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs

113mkOk2Clauses 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)

113 mkOk2Clauses' k [] = return [!(mkAbsurdFinClause fn resTy size)]

115 mkOk2Clauses' k [] = return [!(mkAbsurdFinClause fn resTy size)]

114 mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs

116 mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs

115 clause <- mkOk2Clause fn size k x

117 clause <- mkOk2Clause fn size k x

@@ -121,19 +123,19 @@ genToFin to from ok1 ok2 ty =

121 do (MkDatatype famn tcargs tcres constrs) <- lookupDatatypeExact ty

123 do (MkDatatype famn tcargs tcres constrs) <- lookupDatatypeExact ty

122 let size = length constrs

124 let size = length constrs

123 argn <- gensym "arg"

125 argn <- gensym "arg"

124− declareType $ Declare to [Explicit argn (Var ty)]

126+ declareType $ Declare to [Explicit argn NotErased (Var ty)]

125 `(Fin ~(quote size))

127 `(Fin ~(quote size))

126 toClauses <- mkToClauses to size constrs

128 toClauses <- mkToClauses to size constrs

127 defineFunction $ DefineFun to toClauses

129 defineFunction $ DefineFun to toClauses

128

130

129 argn' <- gensym "arg"

131 argn' <- gensym "arg"

130− declareType $ Declare from [Explicit argn' `(Fin ~(quote size))]

132+ declareType $ Declare from [Explicit argn' NotErased `(Fin ~(quote size))]

131 (Var ty)

133 (Var ty)

132 fromClauses <- mkFromClauses from ty size constrs

134 fromClauses <- mkFromClauses from ty size constrs

133 defineFunction $ DefineFun from fromClauses

135 defineFunction $ DefineFun from fromClauses

134

136

135 argn'' <- gensym "arg"

137 argn'' <- gensym "arg"

136− declareType $ Declare ok1 [Explicit argn'' (Var ty)]

138+ declareType $ Declare ok1 [Explicit argn'' NotErased (Var ty)]

137 `((=) {A=~(Var ty)} {B=~(Var ty)}

139 `((=) {A=~(Var ty)} {B=~(Var ty)}

138 ~(RApp (Var from) (RApp (Var to) (Var argn'')))

140 ~(RApp (Var from) (RApp (Var to) (Var argn'')))

139 ~(Var argn''))

141 ~(Var argn''))

@@ -146,7 +148,7 @@ genToFin to from ok1 ok2 ty =

146 (\n => `((=) {A=~fty} {B=~fty}

148 (\n => `((=) {A=~fty} {B=~fty}

147 ~(RApp (Var to) (RApp (Var from) n))

149 ~(RApp (Var to) (RApp (Var from) n))

148 ~n))

150 ~n))

149− declareType $ Declare ok2 [Explicit argn''' fty]

151+ declareType $ Declare ok2 [Explicit argn''' NotErased fty]

150 (ok2ResTy (Var argn'''))

152 (ok2ResTy (Var argn'''))

151 ok2Clauses <- mkOk2Clauses ok2 size constrs ok2ResTy

153 ok2Clauses <- mkOk2Clauses ok2 size constrs ok2ResTy

152 defineFunction $ DefineFun ok2 ok2Clauses

154 defineFunction $ DefineFun ok2 ok2Clauses

test/tactics001/Tactics.idr+1−1

@@ -33,7 +33,7 @@ plusSuccRightSuccNew (S j) k =

34mkDecl : ()

35mkDecl = %runElab (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])

36− [Implicit (UN "z") `(Nat)]

36+ [Implicit (UN "z") NotErased `(Nat)]

37 `(Vect ~(Var (UN "z")) ())

38 fill `(() : ())

39 solve)