git.iko.soy/Idris-dev
on master help sign in
Indicate constructor fields vs parameters in Elab

All reasonable uses of datatype declarations for generic programming that I could find needed to first split constructor arguments beteween parameters and other arguments, so I added it to the base representation.

commit3b905592fcd7574eb8866e74525313bd821589f2 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 24 Jul 2015, 15:59 (11 years ago) parent7a2dc7b
4 files changed+154−101
compare with master
unifiedsplit
libs/base/Language/Reflection/Utils.idr+8−4 libs/prelude/Language/Reflection/Elab.idr+46−29 src/Idris/Elab/Term.hs+1−1 src/Idris/Reflection.hs+99−67
libs/base/Language/Reflection/Utils.idr+8−4
@@ -333,10 +333,14 @@ instance Show Erasure where
333333 show Erased = "Erased"
334334 show NotErased = "NotErased"
335335
336−instance Show Arg where
337− showPrec d (Explicit n e t) = showCon d "Explicit" $ showArg n ++ showArg e ++ showArg t
338− showPrec d (Implicit n e t) = showCon d "Implicit" $ showArg n ++ showArg e ++ showArg t
339− showPrec d (Constraint n e t) = showCon d "Constraint" $ showArg n ++ showArg e ++ showArg t
336+instance Show Plicity where
337+ show Explicit = "Explicit"
338+ show Implicit = "Implicit"
339+ show Constraint = "Constraint"
340+
341+instance Show FunArg where
342+ showPrec d (MkFunArg n ty plic era) = showCon d "MkFunArg" $ showArg n ++
343+ showArg ty ++ showArg plic ++ showArg era
340344
341345instance Show TyDecl where
342346 showPrec d (Declare fn args ret) = showCon d "Declare" $ showArg fn ++
libs/prelude/Language/Reflection/Elab.idr+46−29
@@ -18,17 +18,36 @@ import Language.Reflection
1818||| erased.
1919data Erasure = Erased | NotErased
2020
21−||| Arguments, with plicity.
22−data Arg : Type where
23− ||| An explicit argument
24− Explicit : TTName -> Erasure -> Raw -> Arg
25−
26− ||| An implicit argument, to be solved by unification
27− Implicit : TTName -> Erasure -> Raw -> Arg
28−
29− ||| A type-class constraint argument, to be solved by type class
30− ||| resolution
31− Constraint : TTName -> Erasure -> Raw -> Arg
21+||| How an argument is provided in high-level Idris
22+data Plicity =
23+ ||| The argument is directly provided at the application site
24+ Explicit |
25+ ||| The argument is found by Idris at the application site
26+ Implicit |
27+ ||| The argument is solved using type class resolution
28+ Constraint
29+
30+||| Function arguments
31+|||
32+||| These are the simplest representation of argument lists, and are
33+||| used for functions.
34+record FunArg where
35+ constructor MkFunArg
36+ argName : TTName
37+ argTy : Raw
38+ plicity : Plicity
39+ erasure : Erasure
40+
41+||| Type constructor arguments
42+|||
43+||| Each argument is identified as being either a parameter that is
44+||| consistent in all constructors, or an index that varies based on
45+||| which constructor is selected.
46+data TyConArg =
47+ ||| Parameters are uniform across the constructors
48+ TyConParameter FunArg |
49+ ||| Indices are not uniform
50+ TyConIndex FunArg
3251
3352||| A type declaration
3453data TyDecl : Type where
@@ -41,7 +60,7 @@ data TyDecl : Type where
4160 ||| @ fn the name to be declared, fully-qualified
4261 ||| @ args the arguments to the function
4362 ||| @ ret the final return type
44− Declare : (fn : TTName) -> (args : List Arg) -> (ret : Raw) -> TyDecl
63+ Declare : (fn : TTName) -> (args : List FunArg) -> (ret : Raw) -> TyDecl
4564
4665||| A single pattern-matching clause
4766data FunClause : Type where
@@ -51,26 +70,24 @@ data FunClause : Type where
5170data FunDefn : Type where
5271 DefineFun : TTName -> List FunClause -> FunDefn
5372
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
5873
59− ||| Indices are allowed to vary across constructors
60− Index : TTName -> Erasure -> Raw -> TyConArg
74+data CtorArg = CtorParameter FunArg | CtorField FunArg
6175
6276||| A reflected datatype definition
63−data Datatype : Type where
64− ||| A reflected datatype definition
65− |||
66− ||| @ familyName the name of the type constructor
67− ||| @ tyConArgs 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) ->
72− (constrs : List (TTName, List Arg, Raw)) ->
73− Datatype
77+record Datatype where
78+ constructor MkDatatype
79+
80+ ||| The name of the type constructor
81+ familyName : TTName
82+
83+ ||| The arguments to the type constructor
84+ tyConArgs : List TyConArg
85+
86+ ||| The result of the type constructor
87+ tyConRes : Raw
88+
89+ ||| The constructors for the family
90+ constructors : List (TTName, List CtorArg, Raw)
7491
7592||| A reflected elaboration script.
7693abstract
src/Idris/Elab/Term.hs+1−1
@@ -2100,7 +2100,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
21002100 let decl = TyDecl Ref checked
21012101 ctxt' = addCtxtDef n decl ctxt
21022102 set_context ctxt'
2103− updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rArgToPArg args) checked) :
2103+ updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
21042104 new_tyDecls e }
21052105 aux <- getAux
21062106 returnUnit
src/Idris/Reflection.hs+99−67
@@ -6,9 +6,9 @@ quoters and unquoters along with some supporting datatypes.
66module Idris.Reflection where
77
88import Control.Applicative ((<$>), (<*>), pure)
9−import Control.Monad (liftM, liftM2, liftM3)
9+import Control.Monad (liftM, liftM2, liftM4)
1010import Data.Maybe (catMaybes)
11−import Data.List ((\\))
11+import Data.List ((\\), findIndex)
1212import qualified Data.Text as T
1313
1414import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,
@@ -23,27 +23,33 @@ import Idris.Delaborate (delab)
2323
2424data RErasure = RErased | RNotErased deriving Show
2525
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 }
26+data RPlicity = RExplicit | RImplicit | RConstraint deriving Show
27+
28+data RFunArg = RFunArg { argName :: Name
29+ , argTy :: Raw
30+ , argPlicity :: RPlicity
31+ , erasure :: RErasure
32+ }
2933 deriving Show
3034
31−data RTyDecl = RDeclare Name [RArg] Raw deriving Show
35+data RTyDecl = RDeclare Name [RFunArg] Raw deriving Show
3236
33−data RTyConArg = RParameter { tcArgName :: Name, tcArgErased :: RErasure, tcArgTy :: Raw }
34− | RIndex { tcArgName :: Name, tcArgErased :: RErasure, tcArgTy :: Raw }
37+data RTyConArg = RParameter RFunArg
38+ | RIndex RFunArg
3539 deriving Show
3640
37−data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RArg], Raw)] deriving Show
41+data RCtorArg = RCtorParameter RFunArg | RCtorField RFunArg deriving Show
42+
43+data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RCtorArg], Raw)] deriving Show
3844
3945rArgOpts :: RErasure -> [ArgOpt]
4046rArgOpts RErased = [InaccessibleArg]
4147rArgOpts _ = []
4248
43−rArgToPArg :: RArg -> PArg
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
49+rFunArgToPArg :: RFunArg -> PArg
50+rFunArgToPArg (RFunArg n _ RExplicit e) = PExp 0 (rArgOpts e) n Placeholder
51+rFunArgToPArg (RFunArg n _ RImplicit e) = PImp 0 False (rArgOpts e) n Placeholder
52+rFunArgToPArg (RFunArg n _ RConstraint e) = PConstraint 0 (rArgOpts e) n Placeholder
4753
4854data RFunClause = RMkFunClause Raw Raw
4955 | RMkImpossibleClause Raw
@@ -977,29 +983,31 @@ reifyErasure (P (DCon _ _ _) n _)
977983 | n == tacN "NotErased" = return RNotErased
978984reifyErasure tm = fail $ "Can't reify " ++ show tm ++ " as erasure info."
979985
986+reifyPlicity :: Term -> ElabD RPlicity
987+reifyPlicity (P (DCon _ _ _) n _)
988+ | n == tacN "Explicit" = return RExplicit
989+ | n == tacN "Implicit" = return RImplicit
990+ | n == tacN "Constraint" = return RConstraint
991+reifyPlicity tm = fail $ "Couldn't reify " ++ show tm ++ " as RPlicity."
992+
993+reifyRFunArg :: Term -> ElabD RFunArg
994+reifyRFunArg (App _ (App _ (App _ (App _ (P (DCon _ _ _) n _) argN) argTy) argPl) argE)
995+ | n == tacN "MkFunArg" = liftM4 RFunArg
996+ (reifyTTName argN)
997+ (reifyRaw argTy)
998+ (reifyPlicity argPl)
999+ (reifyErasure argE)
1000+reifyRFunArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
1001+
9801002reifyTyDecl :: Term -> ElabD RTyDecl
9811003reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
9821004 | n == tacN "Declare" =
9831005 do tyN' <- reifyTTName tyN
9841006 args' <- case unList args of
9851007 Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."
986− Just xs -> mapM reifyRArg xs
1008+ Just xs -> mapM reifyRFunArg xs
9871009 ret' <- reifyRaw ret
9881010 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."
10031011reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
10041012
10051013reifyFunDefn :: Term -> ElabD RFunDefn
@@ -1028,19 +1036,25 @@ envTupleType
10281036
10291037-- | Apply Idris's implicit info to get a signature. The [PArg] should
10301038-- come from a lookup in idris_implicits on IState.
1031−getArgs :: [PArg] -> Raw -> ([RArg], Raw)
1039+getArgs :: [PArg] -> Raw -> ([RFunArg], Raw)
10321040getArgs [] r = ([], r)
10331041getArgs (a:as) (RBind n (Pi _ ty _) sc) =
10341042 let (args, res) = getArgs as sc
10351043 erased = if InaccessibleArg `elem` argopts a then RErased else RNotErased
10361044 arg' = case a of
1037− PImp {} -> RImplicit n erased ty
1038− PExp {} -> RExplicit n erased ty
1039− PConstraint {} -> RConstraint n erased ty
1040− PTacImplicit {} -> RImplicit n erased ty -- TODO?
1045+ PImp {} -> RFunArg n ty RImplicit erased
1046+ PExp {} -> RFunArg n ty RExplicit erased
1047+ PConstraint {} -> RFunArg n ty RConstraint erased
1048+ PTacImplicit {} -> RFunArg n ty RImplicit erased
10411049 in (arg':args, res)
10421050getArgs _ r = ([], r)
10431051
1052+unApplyRaw :: Raw -> (Raw, [Raw])
1053+unApplyRaw tm = ua [] tm
1054+ where
1055+ ua args (RApp f a) = ua (a:args) f
1056+ ua args t = (t, args)
1057+
10441058-- | Build the reflected datatype definition(s) that correspond(s) to
10451059-- a provided unqualified name
10461060buildDatatypes :: IState -> Name -> [RDatatype]
@@ -1052,44 +1066,62 @@ buildDatatypes ist n =
10521066 ctxt = tt_ctxt ist
10531067 impls = idris_implicits ist
10541068
1055− ctorSig cn = do cty <- fmap forget (lookupTyExact cn ctxt)
1056− argInfo <- lookupCtxtExact cn impls
1057− let (args, res) = getArgs argInfo cty
1058− return (cn, args, res)
1069+ ctorSig params cn = do cty <- fmap forget (lookupTyExact cn ctxt)
1070+ argInfo <- lookupCtxtExact cn impls
1071+ let (args, res) = getArgs argInfo cty
1072+ return (cn, ctorArgsStatus args res params, res)
1073+
1074+ argPos n [] res = findPos n res
1075+ where findPos n app = case unApplyRaw app of
1076+ (_, argL) -> findIndex (== Var n) argL
1077+ argPos n (arg:args) res = if n == argName arg
1078+ then Nothing
1079+ else argPos n args res
1080+
1081+ ctorArgsStatus :: [RFunArg] -> Raw -> [Int] -> [RCtorArg]
1082+ ctorArgsStatus [] _ _ = []
1083+ ctorArgsStatus (arg:args) res params =
1084+ case argPos (argName arg) args res of
1085+ Nothing -> RCtorField arg : ctorArgsStatus args res params
1086+ Just i -> if i `elem` params
1087+ then RCtorParameter arg : ctorArgsStatus args res params
1088+ else RCtorField arg : ctorArgsStatus args res params
10591089
10601090 mkDataType name (TI {param_pos = params, con_names = constrs}) =
10611091 do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt
10621092 implInfo <- lookupCtxtExact name impls
1063− let (tcargs, tcres) = getTCArgs params implInfo (forget ty) 0
1064− ctors <- mapM ctorSig constrs
1093+ let (tcargs, tcres) = getTCArgs params implInfo (forget ty)
1094+ ctors <- mapM (ctorSig params) constrs
10651095 return $ RDatatype name tcargs tcres ctors
10661096
1067− getTCArgs params implInfo (RBind an (Pi _ ty _) body) i =
1068− let (erased, implInfo') = case implInfo of
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)
1075− in if i `elem` params
1076− then (RParameter an erased ty : args, res )
1077− else (RIndex an erased ty : args, res)
1078− getTCArgs _ implInfo tm _ = ([], tm)
1097+ getTCArgs :: [Int] -> [PArg] -> Raw -> ([RTyConArg], Raw)
1098+ getTCArgs params implInfo tcTy =
1099+ let (args, res) = getArgs implInfo tcTy
1100+ in (tcArg args 0, res)
1101+ where tcArg [] _ = []
1102+ tcArg (arg:args) i | i `elem` params = RParameter arg : tcArg args (i+1)
1103+ | otherwise = RIndex arg : tcArg args (i+1)
1104+
10791105
10801106reflectErasure :: RErasure -> Raw
10811107reflectErasure RErased = Var (tacN "Erased")
10821108reflectErasure RNotErased = Var (tacN "NotErased")
10831109
1084−reflectArg :: RArg -> 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"
1091− RImplicit{} -> tacN "Implicit"
1092− RConstraint{} -> tacN "Constraint"
1110+reflectPlicity :: RPlicity -> Raw
1111+reflectPlicity RExplicit = Var (tacN "Explicit")
1112+reflectPlicity RImplicit = Var (tacN "Implicit")
1113+reflectPlicity RConstraint = Var (tacN "Constraint")
1114+
1115+reflectArg :: RFunArg -> Raw
1116+reflectArg (RFunArg n ty plic erasure) =
1117+ RApp (RApp (RApp (RApp (Var $ tacN "MkFunArg") (reflectName n))
1118+ (reflectRaw ty))
1119+ (reflectPlicity plic))
1120+ (reflectErasure erasure)
1121+
1122+reflectCtorArg :: RCtorArg -> Raw
1123+reflectCtorArg (RCtorParameter arg) = RApp (Var $ tacN "CtorParameter") (reflectArg arg)
1124+reflectCtorArg (RCtorField arg) = RApp (Var $ tacN "CtorField") (reflectArg arg)
10931125
10941126reflectDatatype :: RDatatype -> Raw
10951127reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
@@ -1097,18 +1129,18 @@ reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
10971129 , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)
10981130 , reflectRaw tyConRes
10991131 , rawList (rawTripleTy (Var $ reflm "TTName")
1100− (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "Arg"))
1132+ (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "CtorArg"))
11011133 (Var $ reflm "Raw"))
11021134 [ rawTriple ((Var $ reflm "TTName"),
1103− (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "Arg")),
1135+ (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "CtorArg")),
11041136 (Var $ reflm "Raw"))
11051137 (reflectName cn,
1106− rawList (Var $ tacN "Arg") (map reflectArg cargs),
1138+ rawList (Var $ tacN "CtorArg") (map reflectCtorArg cargs),
11071139 reflectRaw cty)
11081140 | (cn, cargs, cty) <- constrs
11091141 ]
11101142 ]
1111− where reflectConArg (RParameter n e t) =
1112− raw_apply (Var $ tacN "Parameter") [reflectName n, reflectErasure e, reflectRaw t]
1113− reflectConArg (RIndex n e t) =
1114− raw_apply (Var $ tacN "Index") [reflectName n, reflectErasure e, reflectRaw t]
1143+ where reflectConArg (RParameter a) =
1144+ RApp (Var $ tacN "TyConParameter") (reflectArg a)
1145+ reflectConArg (RIndex a) =
1146+ RApp (Var $ tacN "TyConIndex") (reflectArg a)