d9b5682 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

d9b5682David Christiansen11 years ago

libs/base/Language/Reflection/Utils.idr+18−4

compare with master

unifiedsplit

@@ -242,6 +242,12 @@ instance Eq TT where

242 equalp (TType u) (TType u') = u == u'

243 equalp x y = False

244

245+instance Eq Universe where

246+ Reflection.NullType == Reflection.NullType = True

247+ Reflection.UniqueType == Reflection.UniqueType = True

248+ Reflection.AllTypes == Reflection.AllTypes = True

249+ _ == _ = False

250+

245total

251total

246forget : TT -> Maybe Raw

252forget : TT -> Maybe Raw

247forget tm = fe [] tm

253forget tm = fe [] tm

@@ -333,10 +339,18 @@ instance Show Erasure where

333 show Erased = "Erased"

339 show Erased = "Erased"

334 show NotErased = "NotErased"

340 show NotErased = "NotErased"

335

341

336−instance Show Arg where

342+instance Show Plicity where

337− showPrec d (Explicit n e t) = showCon d "Explicit" $ showArg n ++ showArg e ++ showArg t

343+ show Explicit = "Explicit"

344+ show Implicit = "Implicit"

345+ show Constraint = "Constraint"

346+

347+instance Show FunArg where

338− showPrec d (Implicit n e t) = showCon d "Implicit" $ showArg n ++ showArg e ++ showArg t

348+ showPrec d (MkFunArg n ty plic era) = showCon d "MkFunArg" $ showArg n ++

349+ showArg ty ++ showArg plic ++ showArg era

350+

351+instance Show CtorArg where

339− showPrec d (Constraint n e t) = showCon d "Constraint" $ showArg n ++ showArg e ++ showArg t

352+ showPrec d (CtorParameter fa) = showCon d "CtorParameter" $ showArg fa

353+ showPrec d (CtorField fa) = showCon d "CtorField" $ showArg fa

340

354

341instance Show TyDecl where

355instance Show TyDecl where

342 showPrec d (Declare fn args ret) = showCon d "Declare" $ showArg fn ++

356 showPrec d (Declare fn args ret) = showCon d "Declare" $ showArg fn ++

libs/prelude/Language/Reflection.idr+50−21

@@ -579,33 +579,62 @@ mutual

579 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))

580

581mutual

582− quoteRaw : Raw -> TT

582+ quoteRawTT : Raw -> TT

583− quoteRaw (Var n) = `(Var ~(quote n))

583+ quoteRawTT (Var n) = `(Var ~(quote n))

584− quoteRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinder b) ~(quoteRaw tm))

584+ quoteRawTT (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinderTT b) ~(quoteRawTT tm))

585− quoteRaw (RApp tm tm') = `(RApp ~(quoteRaw tm) ~(quoteRaw tm'))

585+ quoteRawTT (RApp tm tm') = `(RApp ~(quoteRawTT tm) ~(quoteRawTT tm'))

586− quoteRaw RType = `(RType)

586+ quoteRawTT RType = `(RType)

587− quoteRaw (RUType u) = `(RUType ~(quote u))

587+ quoteRawTT (RUType u) = `(RUType ~(quote u))

588− quoteRaw (RForce tm) = `(RForce ~(quoteRaw tm))

588+ quoteRawTT (RForce tm) = `(RForce ~(quoteRawTT tm))

589− quoteRaw (RConstant c) = `(RConstant ~(quote c))

589+ quoteRawTT (RConstant c) = `(RConstant ~(quote c))

590−

590+

591− quoteRawBinder : Binder Raw -> TT

591+ quoteRawBinderTT : Binder Raw -> TT

592− quoteRawBinder (Lam x) = `(Lam {a=Raw} ~(quoteRaw x))

592+ quoteRawBinderTT (Lam x) = `(Lam {a=Raw} ~(quoteRawTT x))

593− quoteRawBinder (Pi x k) = `(Pi {a=Raw} ~(quoteRaw x) ~(quoteRaw k))

593+ quoteRawBinderTT (Pi x k) = `(Pi {a=Raw} ~(quoteRawTT x) ~(quoteRawTT k))

594− quoteRawBinder (Let x y) = `(Let {a=Raw} ~(quoteRaw x) ~(quoteRaw y))

594+ quoteRawBinderTT (Let x y) = `(Let {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))

595− quoteRawBinder (NLet x y) = `(NLet {a=Raw} ~(quoteRaw x) ~(quoteRaw y))

595+ quoteRawBinderTT (NLet x y) = `(NLet {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))

596− quoteRawBinder (Hole x) = `(Hole {a=Raw} ~(quoteRaw x))

596+ quoteRawBinderTT (Hole x) = `(Hole {a=Raw} ~(quoteRawTT x))

597− quoteRawBinder (GHole x) = `(GHole {a=Raw} ~(quoteRaw x))

597+ quoteRawBinderTT (GHole x) = `(GHole {a=Raw} ~(quoteRawTT x))

598− quoteRawBinder (Guess x y) = `(Guess {a=Raw} ~(quoteRaw x) ~(quoteRaw y))

598+ quoteRawBinderTT (Guess x y) = `(Guess {a=Raw} ~(quoteRawTT x) ~(quoteRawTT y))

599− quoteRawBinder (PVar x) = `(PVar {a=Raw} ~(quoteRaw x))

599+ quoteRawBinderTT (PVar x) = `(PVar {a=Raw} ~(quoteRawTT x))

600− quoteRawBinder (PVTy x) = `(PVTy {a=Raw} ~(quoteRaw x))

600+ quoteRawBinderTT (PVTy x) = `(PVTy {a=Raw} ~(quoteRawTT x))

601

602instance Quotable Raw TT where

603 quotedTy = `(Raw)

604− quote = quoteRaw

604+ quote = quoteRawTT

605

606instance Quotable (Binder Raw) TT where

607 quotedTy = `(Binder Raw)

608− quote = quoteRawBinder

608+ quote = quoteRawBinderTT

609+

610+mutual

611+ quoteRawRaw : Raw -> Raw

612+ quoteRawRaw (Var n) = `(Var ~(quote n))

613+ quoteRawRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinderRaw b) ~(quoteRawRaw tm))

614+ quoteRawRaw (RApp tm tm') = `(RApp ~(quoteRawRaw tm) ~(quoteRawRaw tm'))

615+ quoteRawRaw RType = `(RType)

616+ quoteRawRaw (RUType u) = `(RUType ~(quote u))

617+ quoteRawRaw (RForce tm) = `(RForce ~(quoteRawRaw tm))

618+ quoteRawRaw (RConstant c) = `(RConstant ~(quote c))

619+

620+ quoteRawBinderRaw : Binder Raw -> Raw

621+ quoteRawBinderRaw (Lam x) = `(Lam {a=Raw} ~(quoteRawRaw x))

622+ quoteRawBinderRaw (Pi x k) = `(Pi {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw k))

623+ quoteRawBinderRaw (Let x y) = `(Let {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))

624+ quoteRawBinderRaw (NLet x y) = `(NLet {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))

625+ quoteRawBinderRaw (Hole x) = `(Hole {a=Raw} ~(quoteRawRaw x))

626+ quoteRawBinderRaw (GHole x) = `(GHole {a=Raw} ~(quoteRawRaw x))

627+ quoteRawBinderRaw (Guess x y) = `(Guess {a=Raw} ~(quoteRawRaw x) ~(quoteRawRaw y))

628+ quoteRawBinderRaw (PVar x) = `(PVar {a=Raw} ~(quoteRawRaw x))

629+ quoteRawBinderRaw (PVTy x) = `(PVTy {a=Raw} ~(quoteRawRaw x))

630+

631+instance Quotable Raw Raw where

632+ quotedTy = `(Raw)

633+ quote = quoteRawRaw

634+

635+instance Quotable (Binder Raw) Raw where

636+ quotedTy = `(Binder Raw)

637+ quote = quoteRawBinderRaw

609

638

610instance Quotable ErrorReportPart TT where

639instance Quotable ErrorReportPart TT where

611 quotedTy = `(ErrorReportPart)

640 quotedTy = `(ErrorReportPart)

libs/prelude/Language/Reflection/Elab.idr+68−28

@@ -7,6 +7,7 @@ module Language.Reflection.Elab

8import Builtins

9import Prelude.Applicative

10+import Prelude.Basics

10import Prelude.Bool

11import Prelude.Bool

11import Prelude.Functor

12import Prelude.Functor

12import Prelude.List

13import Prelude.List

@@ -18,17 +19,36 @@ import Language.Reflection

18||| erased.

19||| erased.

19data Erasure = Erased | NotErased

20data Erasure = Erased | NotErased

21−||| Arguments, with plicity.

22+||| How an argument is provided in high-level Idris

22−data Arg : Type where

23+data Plicity =

23− ||| An explicit argument

24+ ||| The argument is directly provided at the application site

24− Explicit : TTName -> Erasure -> Raw -> Arg

25+ Explicit |

26+ ||| The argument is found by Idris at the application site

27+ Implicit |

28+ ||| The argument is solved using type class resolution

29+ Constraint

26− ||| An implicit argument, to be solved by unification

31+||| Function arguments

27− Implicit : TTName -> Erasure -> Raw -> Arg

32+|||

28−

33+||| These are the simplest representation of argument lists, and are

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

34+||| used for functions.

30− ||| resolution

35+record FunArg where

31− Constraint : TTName -> Erasure -> Raw -> Arg

36+ constructor MkFunArg

37+ argName : TTName

38+ argTy : Raw

39+ plicity : Plicity

40+ erasure : Erasure

41+

42+||| Type constructor arguments

43+|||

44+||| Each argument is identified as being either a parameter that is

45+||| consistent in all constructors, or an index that varies based on

46+||| which constructor is selected.

47+data TyConArg =

48+ ||| Parameters are uniform across the constructors

49+ TyConParameter FunArg |

50+ ||| Indices are not uniform

51+ TyConIndex FunArg

33||| A type declaration

53||| A type declaration

34data TyDecl : Type where

54data TyDecl : Type where

@@ -41,7 +61,7 @@ data TyDecl : Type where

41 ||| @ fn the name to be declared, fully-qualified

61 ||| @ fn the name to be declared, fully-qualified

42 ||| @ args the arguments to the function

62 ||| @ args the arguments to the function

43 ||| @ ret the final return type

63 ||| @ ret the final return type

44− Declare : (fn : TTName) -> (args : List Arg) -> (ret : Raw) -> TyDecl

64+ Declare : (fn : TTName) -> (args : List FunArg) -> (ret : Raw) -> TyDecl

46||| A single pattern-matching clause

66||| A single pattern-matching clause

47data FunClause : Type where

67data FunClause : Type where

@@ -51,26 +71,24 @@ data FunClause : Type where

51data FunDefn : Type where

71data FunDefn : Type where

52 DefineFun : TTName -> List FunClause -> FunDefn

72 DefineFun : TTName -> List FunClause -> FunDefn

54−||| An argument to a type constructor.

55−data TyConArg : Type where

56− ||| Parameters are consistent across all constructors of the type

57− Parameter : TTName -> Erasure -> Raw -> TyConArg

59− ||| Indices are allowed to vary across constructors

75+data CtorArg = CtorParameter FunArg | CtorField FunArg

60− Index : TTName -> Erasure -> Raw -> TyConArg

62||| A reflected datatype definition

77||| A reflected datatype definition

63−data Datatype : Type where

78+record Datatype where

64− ||| A reflected datatype definition

79+ constructor MkDatatype

65− |||

80+

66− ||| @ familyName the name of the type constructor

81+ ||| The name of the type constructor

82+ familyName : TTName

83+

67− ||| @ tyConArgs the arguments to the type constructor

84+ ||| The arguments to the type constructor

68− ||| @ tyConRes the result of the type constructor

69− ||| @ constrs the constructors, with their types

70− MkDatatype : (familyName : TTName) ->

71− (tyConArgs : List TyConArg) -> (tyConRes : Raw) ->

85+ tyConArgs : List TyConArg

86+

87+ ||| The result of the type constructor

88+ tyConRes : Raw

89+

90+ ||| The constructors for the family

72− (constrs : List (TTName, List Arg, Raw)) ->

91+ constructors : List (TTName, List CtorArg, Raw)

73− Datatype

75||| A reflected elaboration script.

93||| A reflected elaboration script.

76abstract

94abstract

@@ -113,8 +131,11 @@ data Elab : Type -> Type where

113 prim__Forall : TTName -> Raw -> Elab ()

131 prim__Forall : TTName -> Raw -> Elab ()

114 prim__PatVar : TTName -> Elab ()

132 prim__PatVar : TTName -> Elab ()

115 prim__PatBind : TTName -> Elab ()

133 prim__PatBind : TTName -> Elab ()

134+ -- TODO: letbind

116

135

117 prim__Compute : Elab ()

136 prim__Compute : Elab ()

137+ prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT

138+ prim__Whnf : TT -> Elab TT

118

139

119 prim__DeclareType : TyDecl -> Elab ()

140 prim__DeclareType : TyDecl -> Elab ()

120 prim__DefineFunction : FunDefn -> Elab ()

141 prim__DefineFunction : FunDefn -> Elab ()

@@ -204,6 +225,12 @@ namespace Tactics

204 forgetTypes : TT -> Elab Raw

225 forgetTypes : TT -> Elab Raw

205 forgetTypes tt = prim__Forget tt

226 forgetTypes tt = prim__Forget tt

206

227

228+ ||| Get the goal type as a Raw term

229+ goalType : Elab Raw

230+ goalType = do g <- getGoal

231+ forgetTypes (snd g)

232+

233+

207 ||| Generate a unique name based on some hint.

234 ||| Generate a unique name based on some hint.

208 |||

235 |||

209 ||| **NB**: the generated name is unique _for this run of the

236 ||| **NB**: the generated name is unique _for this run of the

@@ -316,6 +343,19 @@ namespace Tactics

316 compute : Elab ()

343 compute : Elab ()

317 compute = prim__Compute

344 compute = prim__Compute

318

345

346+ ||| Normalise a term in some lexical environment

347+ |||

348+ ||| @ env the environment in which to compute (get one of these from `getEnv`)

349+ ||| @ term the term to normalise

350+ normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT

351+ normalise env term = prim__Normalise env term

352+

353+ ||| Reduce a closed term to weak-head normal form

354+ |||

355+ ||| @ term the term to reduce

356+ whnf : (term : TT) -> Elab TT

357+ whnf term = prim__Whnf term

358+

319 ||| Find the source context for the elaboration script

359 ||| Find the source context for the elaboration script

320 getSourceLocation : Elab SourceLocation

360 getSourceLocation : Elab SourceLocation

321 getSourceLocation = prim__SourceLocation

361 getSourceLocation = prim__SourceLocation

src/Idris/Elab/Term.hs+16−3

@@ -17,6 +17,7 @@ import Idris.Core.Evaluate

17import Idris.Core.Unify

18import Idris.Core.ProofTerm (getProofTerm)

19import Idris.Core.Typecheck (check, recheck, converts, isType)

20+import Idris.Core.WHNF (whnf)

20import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)

21import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)

21import Idris.ErrReverse (errReverse)

22import Idris.ErrReverse (errReverse)

22import Idris.ElabQuasiquote (extractUnquotes)

23import Idris.ElabQuasiquote (extractUnquotes)

@@ -2050,8 +2051,10 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

2050 returnUnit

2051 returnUnit

2051 | n == tacN "prim__Focus", [what] <- args

2052 | n == tacN "prim__Focus", [what] <- args

2052 = do n' <- reifyTTName what

2053 = do n' <- reifyTTName what

2053− focus n'

2054+ hs <- get_holes

2055+ if elem n' hs

2054− returnUnit

2056+ then focus n' >> returnUnit

2057+ else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"

2055 | n == tacN "prim__Unfocus", [what] <- args

2058 | n == tacN "prim__Unfocus", [what] <- args

2056 = do n' <- reifyTTName what

2059 = do n' <- reifyTTName what

2057 movelast n'

2060 movelast n'

@@ -2077,6 +2080,16 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

2077 returnUnit

2080 returnUnit

2078 | n == tacN "prim__Compute", [] <- args

2081 | n == tacN "prim__Compute", [] <- args

2079 = do compute ; returnUnit

2082 = do compute ; returnUnit

2083+ | n == tacN "prim__Normalise", [env, tm] <- args

2084+ = do env' <- reifyEnv env

2085+ tm' <- reifyTT tm

2086+ ctxt <- get_context

2087+ let out = normaliseAll ctxt env' (finalise tm')

2088+ fmap fst . checkClosed $ reflect out

2089+ | n == tacN "prim__Whnf", [tm] <- args

2090+ = do tm' <- reifyTT tm

2091+ ctxt <- get_context

2092+ fmap fst . checkClosed . reflect $ whnf ctxt tm'

2080 | n == tacN "prim__DeclareType", [decl] <- args

2093 | n == tacN "prim__DeclareType", [decl] <- args

2081 = do (RDeclare n args res) <- reifyTyDecl decl

2094 = do (RDeclare n args res) <- reifyTyDecl decl

2082 ctxt <- get_context

2095 ctxt <- get_context

@@ -2097,7 +2110,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

2097 let decl = TyDecl Ref checked

2110 let decl = TyDecl Ref checked

2098 ctxt' = addCtxtDef n decl ctxt

2111 ctxt' = addCtxtDef n decl ctxt

2099 set_context ctxt'

2112 set_context ctxt'

2100− updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rArgToPArg args) checked) :

2113+ updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :

2101 new_tyDecls e }

2114 new_tyDecls e }

2102 aux <- getAux

2115 aux <- getAux

2103 returnUnit

2116 returnUnit

src/Idris/Reflection.hs+102−67

@@ -6,9 +6,9 @@ quoters and unquoters along with some supporting datatypes.

6module Idris.Reflection where

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

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

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

10import Data.Maybe (catMaybes)

11−import Data.List ((\\))

11+import Data.List ((\\), findIndex)

12import qualified Data.Text as T

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

@@ -23,27 +23,33 @@ import Idris.Delaborate (delab)

24data RErasure = RErased | RNotErased deriving Show

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

26+data RPlicity = RExplicit | RImplicit | RConstraint deriving Show

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

27+

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

28+data RFunArg = RFunArg { argName :: Name

29+ , argTy :: Raw

30+ , argPlicity :: RPlicity

31+ , erasure :: RErasure

32+ }

29 deriving Show

33 deriving Show

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

35+data RTyDecl = RDeclare Name [RFunArg] Raw deriving Show

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

37+data RTyConArg = RParameter RFunArg

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

38+ | RIndex RFunArg

35 deriving Show

39 deriving Show

41+data RCtorArg = RCtorParameter RFunArg | RCtorField RFunArg deriving Show

42+

37−data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RArg], Raw)] deriving Show

43+data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RCtorArg], Raw)] deriving Show

39rArgOpts :: RErasure -> [ArgOpt]

45rArgOpts :: RErasure -> [ArgOpt]

40rArgOpts RErased = [InaccessibleArg]

46rArgOpts RErased = [InaccessibleArg]

41rArgOpts _ = []

47rArgOpts _ = []

43−rArgToPArg :: RArg -> PArg

49+rFunArgToPArg :: RFunArg -> PArg

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

50+rFunArgToPArg (RFunArg n _ RExplicit e) = PExp 0 (rArgOpts e) n Placeholder

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

51+rFunArgToPArg (RFunArg n _ RImplicit e) = PImp 0 False (rArgOpts e) n Placeholder

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

52+rFunArgToPArg (RFunArg n _ RConstraint e) = PConstraint 0 (rArgOpts e) n Placeholder

48data RFunClause = RMkFunClause Raw Raw

54data RFunClause = RMkFunClause Raw Raw

49 | RMkImpossibleClause Raw

55 | RMkImpossibleClause Raw

@@ -795,6 +801,9 @@ reflectEnv = foldr consToEnvList emptyEnvList

795 emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))

801 emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))

796 [envTupleType]

802 [envTupleType]

797

803

804+reifyEnv :: Term -> ElabD Env

805+reifyEnv = reifyList (reifyPair reifyTTName (reifyTTBinder reifyTT (reflm "TT")))

806+

798-- | Reflect an error into the internal datatype of Idris -- TODO

807-- | Reflect an error into the internal datatype of Idris -- TODO

799rawBool :: Bool -> Raw

808rawBool :: Bool -> Raw

800rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])

809rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])

@@ -977,29 +986,31 @@ reifyErasure (P (DCon _ _ _) n _)

977 | n == tacN "NotErased" = return RNotErased

986 | n == tacN "NotErased" = return RNotErased

978reifyErasure tm = fail $ "Can't reify " ++ show tm ++ " as erasure info."

987reifyErasure tm = fail $ "Can't reify " ++ show tm ++ " as erasure info."

979

988

989+reifyPlicity :: Term -> ElabD RPlicity

990+reifyPlicity (P (DCon _ _ _) n _)

991+ | n == tacN "Explicit" = return RExplicit

992+ | n == tacN "Implicit" = return RImplicit

993+ | n == tacN "Constraint" = return RConstraint

994+reifyPlicity tm = fail $ "Couldn't reify " ++ show tm ++ " as RPlicity."

995+

996+reifyRFunArg :: Term -> ElabD RFunArg

997+reifyRFunArg (App _ (App _ (App _ (App _ (P (DCon _ _ _) n _) argN) argTy) argPl) argE)

998+ | n == tacN "MkFunArg" = liftM4 RFunArg

999+ (reifyTTName argN)

1000+ (reifyRaw argTy)

1001+ (reifyPlicity argPl)

1002+ (reifyErasure argE)

1003+reifyRFunArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."

1004+

980reifyTyDecl :: Term -> ElabD RTyDecl

1005reifyTyDecl :: Term -> ElabD RTyDecl

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

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

982 | n == tacN "Declare" =

1007 | n == tacN "Declare" =

983 do tyN' <- reifyTTName tyN

1008 do tyN' <- reifyTTName tyN

984 args' <- case unList args of

1009 args' <- case unList args of

985 Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."

1010 Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."

986− Just xs -> mapM reifyRArg xs

1011+ Just xs -> mapM reifyRFunArg xs

987 ret' <- reifyRaw ret

1012 ret' <- reifyRaw ret

988 return $ RDeclare tyN' args' ret'

1013 return $ RDeclare tyN' args' ret'

989− where reifyRArg :: Term -> ElabD RArg

990− reifyRArg (App _ (App _ (App _ (P (DCon _ _ _) n _) argN) argE) argTy)

991− | n == tacN "Explicit" = liftM3 RExplicit

992− (reifyTTName argN)

993− (reifyErasure argE)

994− (reifyRaw argTy)

995− | n == tacN "Implicit" = liftM3 RImplicit

996− (reifyTTName argN)

997− (reifyErasure argE)

998− (reifyRaw argTy) | n == tacN "Constraint" = liftM3 RConstraint

999− (reifyTTName argN)

1000− (reifyErasure argE)

1001− (reifyRaw argTy)

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

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

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

1004

1015

1005reifyFunDefn :: Term -> ElabD RFunDefn

1016reifyFunDefn :: Term -> ElabD RFunDefn

@@ -1028,19 +1039,25 @@ envTupleType

1028

1039

1029-- | Apply Idris's implicit info to get a signature. The [PArg] should

1040-- | Apply Idris's implicit info to get a signature. The [PArg] should

1030-- come from a lookup in idris_implicits on IState.

1041-- come from a lookup in idris_implicits on IState.

1031−getArgs :: [PArg] -> Raw -> ([RArg], Raw)

1042+getArgs :: [PArg] -> Raw -> ([RFunArg], Raw)

1032getArgs [] r = ([], r)

1043getArgs [] r = ([], r)

1033getArgs (a:as) (RBind n (Pi _ ty _) sc) =

1044getArgs (a:as) (RBind n (Pi _ ty _) sc) =

1034 let (args, res) = getArgs as sc

1045 let (args, res) = getArgs as sc

1035 erased = if InaccessibleArg `elem` argopts a then RErased else RNotErased

1046 erased = if InaccessibleArg `elem` argopts a then RErased else RNotErased

1036 arg' = case a of

1047 arg' = case a of

1037− PImp {} -> RImplicit n erased ty

1048+ PImp {} -> RFunArg n ty RImplicit erased

1038− PExp {} -> RExplicit n erased ty

1049+ PExp {} -> RFunArg n ty RExplicit erased

1039− PConstraint {} -> RConstraint n erased ty

1050+ PConstraint {} -> RFunArg n ty RConstraint erased

1040− PTacImplicit {} -> RImplicit n erased ty -- TODO?

1051+ PTacImplicit {} -> RFunArg n ty RImplicit erased

1041 in (arg':args, res)

1052 in (arg':args, res)

1042getArgs _ r = ([], r)

1053getArgs _ r = ([], r)

1043

1054

1055+unApplyRaw :: Raw -> (Raw, [Raw])

1056+unApplyRaw tm = ua [] tm

1057+ where

1058+ ua args (RApp f a) = ua (a:args) f

1059+ ua args t = (t, args)

1060+

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

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

1045-- a provided unqualified name

1062-- a provided unqualified name

1046buildDatatypes :: IState -> Name -> [RDatatype]

1063buildDatatypes :: IState -> Name -> [RDatatype]

@@ -1052,44 +1069,62 @@ buildDatatypes ist n =

1052 ctxt = tt_ctxt ist

1069 ctxt = tt_ctxt ist

1053 impls = idris_implicits ist

1070 impls = idris_implicits ist

1054

1071

1055− ctorSig cn = do cty <- fmap forget (lookupTyExact cn ctxt)

1072+ ctorSig params cn = do cty <- fmap forget (lookupTyExact cn ctxt)

1056− argInfo <- lookupCtxtExact cn impls

1073+ argInfo <- lookupCtxtExact cn impls

1057− let (args, res) = getArgs argInfo cty

1074+ let (args, res) = getArgs argInfo cty

1058− return (cn, args, res)

1075+ return (cn, ctorArgsStatus args res params, res)

1076+

1077+ argPos n [] res = findPos n res

1078+ where findPos n app = case unApplyRaw app of

1079+ (_, argL) -> findIndex (== Var n) argL

1080+ argPos n (arg:args) res = if n == argName arg

1081+ then Nothing

1082+ else argPos n args res

1083+

1084+ ctorArgsStatus :: [RFunArg] -> Raw -> [Int] -> [RCtorArg]

1085+ ctorArgsStatus [] _ _ = []

1086+ ctorArgsStatus (arg:args) res params =

1087+ case argPos (argName arg) args res of

1088+ Nothing -> RCtorField arg : ctorArgsStatus args res params

1089+ Just i -> if i `elem` params

1090+ then RCtorParameter arg : ctorArgsStatus args res params

1091+ else RCtorField arg : ctorArgsStatus args res params

1059

1092

1060 mkDataType name (TI {param_pos = params, con_names = constrs}) =

1093 mkDataType name (TI {param_pos = params, con_names = constrs}) =

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

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

1062 implInfo <- lookupCtxtExact name impls

1095 implInfo <- lookupCtxtExact name impls

1063− let (tcargs, tcres) = getTCArgs params implInfo (forget ty) 0

1096+ let (tcargs, tcres) = getTCArgs params implInfo (forget ty)

1064− ctors <- mapM ctorSig constrs

1097+ ctors <- mapM (ctorSig params) constrs

1065 return $ RDatatype name tcargs tcres ctors

1098 return $ RDatatype name tcargs tcres ctors

1066

1099

1067− getTCArgs params implInfo (RBind an (Pi _ ty _) body) i =

1100+ getTCArgs :: [Int] -> [PArg] -> Raw -> ([RTyConArg], Raw)

1068− let (erased, implInfo') = case implInfo of

1101+ getTCArgs params implInfo tcTy =

1069− [] -> (RNotErased, [])

1070− (a:as) -> (if InaccessibleArg `elem` argopts a

1071− then RErased

1072− else RNotErased,

1073− as)

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

1102+ let (args, res) = getArgs implInfo tcTy

1075− in if i `elem` params

1103+ in (tcArg args 0, res)

1076− then (RParameter an erased ty : args, res )

1104+ where tcArg [] _ = []

1077− else (RIndex an erased ty : args, res)

1105+ tcArg (arg:args) i | i `elem` params = RParameter arg : tcArg args (i+1)

1078− getTCArgs _ implInfo tm _ = ([], tm)

1106+ | otherwise = RIndex arg : tcArg args (i+1)

1107+

1079

1108

1080reflectErasure :: RErasure -> Raw

1109reflectErasure :: RErasure -> Raw

1081reflectErasure RErased = Var (tacN "Erased")

1110reflectErasure RErased = Var (tacN "Erased")

1082reflectErasure RNotErased = Var (tacN "NotErased")

1111reflectErasure RNotErased = Var (tacN "NotErased")

1083

1112

1084−reflectArg :: RArg -> Raw

1113+reflectPlicity :: RPlicity -> Raw

1085−reflectArg arg =

1086− RApp (RApp (RApp (Var con) (reflectName $ argName arg))

1087− (reflectErasure $ argErased arg))

1088− (reflectRaw $ argTy arg)

1089− where con = case arg of

1090− RExplicit{} -> tacN "Explicit"

1114+reflectPlicity RExplicit = Var (tacN "Explicit")

1091− RImplicit{} -> tacN "Implicit"

1115+reflectPlicity RImplicit = Var (tacN "Implicit")

1092− RConstraint{} -> tacN "Constraint"

1116+reflectPlicity RConstraint = Var (tacN "Constraint")

1117+

1118+reflectArg :: RFunArg -> Raw

1119+reflectArg (RFunArg n ty plic erasure) =

1120+ RApp (RApp (RApp (RApp (Var $ tacN "MkFunArg") (reflectName n))

1121+ (reflectRaw ty))

1122+ (reflectPlicity plic))

1123+ (reflectErasure erasure)

1124+

1125+reflectCtorArg :: RCtorArg -> Raw

1126+reflectCtorArg (RCtorParameter arg) = RApp (Var $ tacN "CtorParameter") (reflectArg arg)

1127+reflectCtorArg (RCtorField arg) = RApp (Var $ tacN "CtorField") (reflectArg arg)

1093

1128

1094reflectDatatype :: RDatatype -> Raw

1129reflectDatatype :: RDatatype -> Raw

1095reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =

1130reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =

@@ -1097,18 +1132,18 @@ reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =

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

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

1098 , reflectRaw tyConRes

1133 , reflectRaw tyConRes

1099 , rawList (rawTripleTy (Var $ reflm "TTName")

1134 , rawList (rawTripleTy (Var $ reflm "TTName")

1100− (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "Arg"))

1135+ (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "CtorArg"))

1101 (Var $ reflm "Raw"))

1136 (Var $ reflm "Raw"))

1102 [ rawTriple ((Var $ reflm "TTName"),

1137 [ rawTriple ((Var $ reflm "TTName"),

1103− (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "Arg")),

1138+ (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "CtorArg")),

1104 (Var $ reflm "Raw"))

1139 (Var $ reflm "Raw"))

1105 (reflectName cn,

1140 (reflectName cn,

1106− rawList (Var $ tacN "Arg") (map reflectArg cargs),

1141+ rawList (Var $ tacN "CtorArg") (map reflectCtorArg cargs),

1107 reflectRaw cty)

1142 reflectRaw cty)

1108 | (cn, cargs, cty) <- constrs

1143 | (cn, cargs, cty) <- constrs

1109 ]

1144 ]

1110 ]

1145 ]

1111− where reflectConArg (RParameter n e t) =

1146+ where reflectConArg (RParameter a) =

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

1147+ RApp (Var $ tacN "TyConParameter") (reflectArg a)

1113− reflectConArg (RIndex n e t) =

1148+ reflectConArg (RIndex a) =

1114− raw_apply (Var $ tacN "Index") [reflectName n, reflectErasure e, reflectRaw t]

1149+ RApp (Var $ tacN "TyConIndex") (reflectArg a)

test/meta001/Finite.idr+16−16

@@ -28,7 +28,7 @@ mkFin (S k) (S j) = do i <- mkFin k j

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

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

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

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

32 Elab FunClause

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

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

@@ -37,7 +37,7 @@ mkToClause fn size i (n, _, ty) =

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

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

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

41 Elab FunClause

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

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

@@ -45,7 +45,7 @@ mkFromClause fn size i (n, _, ty) =

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

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

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

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

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

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

@@ -53,7 +53,7 @@ mkOk1Clause fn size i (n, _, ty) =

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

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

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

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

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

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

@@ -62,9 +62,9 @@ mkOk2Clause fn size i (n, _, ty) =

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

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

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

66mkToClauses fn size xs = mkToClauses' Z xs

67− where mkToClauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)

67+ where mkToClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

68 mkToClauses' k [] = return []

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

70 clause <- mkToClause fn size k x

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

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

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

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

96mkFromClauses fn ty size xs = mkFromClauses' Z xs

97− where mkFromClauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)

97+ where mkFromClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

98 mkFromClauses' k [] =

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

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

101 clause <- mkFromClause fn size k x

102 return $ clause :: rest

103

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

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

105mkOk1Clauses fn size xs = mkOk1Clauses' Z xs

106− where mkOk1Clauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)

106+ where mkOk1Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

107 mkOk1Clauses' k [] = return []

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

109 clause <- mkOk1Clause fn size k x

110 return $ clause :: rest

111

112−mkOk2Clauses : TTName -> Nat -> List (TTName, List Arg, Raw) -> (Raw -> Raw) -> Elab (List FunClause)

112+mkOk2Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> (Raw -> Raw) -> Elab (List FunClause)

113mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs

114− where mkOk2Clauses' : Nat -> List (TTName, List Arg, Raw) -> Elab (List FunClause)

114+ where mkOk2Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

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

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

117 clause <- mkOk2Clause fn size k x

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

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

124 let size = length constrs

125 argn <- gensym "arg"

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

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

127 `(Fin ~(quote size))

128 toClauses <- mkToClauses to size constrs

129 defineFunction $ DefineFun to toClauses

130

131 argn' <- gensym "arg"

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

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

133 (Var ty)

134 fromClauses <- mkFromClauses from ty size constrs

135 defineFunction $ DefineFun from fromClauses

136

137 argn'' <- gensym "arg"

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

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

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

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

141 ~(Var argn''))

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

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

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

150 ~n))

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

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

152 (ok2ResTy (Var argn'''))

153 ok2Clauses <- mkOk2Clauses ok2 size constrs ok2ResTy

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") NotErased `(Nat)]

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

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

38 fill `(() : ())

39 solve)