git.iko.soy/Idris-dev
on master help sign in
Indicate constructor fields vs parameters in Elab
3b90559David Raymond Christiansen
libs/base/Language/Reflection/Utils.idr+8−4
compare with master
unifiedsplit
@@ -333,10 +333,14 @@ instance Show Erasure where
333 show Erased = "Erased"
333 show Erased = "Erased"
334 show NotErased = "NotErased"
334 show NotErased = "NotErased"
335
335
336−instance Show Arg where
336+instance Show Plicity where
337− showPrec d (Explicit n e t) = showCon d "Explicit" $ showArg n ++ showArg e ++ showArg t
337+ show Explicit = "Explicit"
338− showPrec d (Implicit n e t) = showCon d "Implicit" $ showArg n ++ showArg e ++ showArg t
338+ show Implicit = "Implicit"
339+ show Constraint = "Constraint"
340+
341+instance Show FunArg where
339− showPrec d (Constraint n e t) = showCon d "Constraint" $ showArg n ++ showArg e ++ showArg t
342+ showPrec d (MkFunArg n ty plic era) = showCon d "MkFunArg" $ showArg n ++
343+ showArg ty ++ showArg plic ++ showArg era
340
344
341instance Show TyDecl where
345instance Show TyDecl where
342 showPrec d (Declare fn args ret) = showCon d "Declare" $ showArg fn ++
346 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
18||| erased.
18||| erased.
19data Erasure = Erased | NotErased
19data Erasure = Erased | NotErased
20
20
21−||| Arguments, with plicity.
21+||| How an argument is provided in high-level Idris
22−data Arg : Type where
22+data Plicity =
23− ||| An explicit argument
23+ ||| The argument is directly provided at the application site
24− Explicit : TTName -> Erasure -> Raw -> Arg
24+ Explicit |
25−
25+ ||| The argument is found by Idris at the application site
26− ||| An implicit argument, to be solved by unification
27− Implicit : TTName -> Erasure -> Raw -> Arg
26+ Implicit |
28−
29− ||| A type-class constraint argument, to be solved by type class
27+ ||| The argument is solved using type class resolution
30− ||| resolution
31− Constraint : TTName -> Erasure -> Raw -> Arg
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
32
51
33||| A type declaration
52||| A type declaration
34data TyDecl : Type where
53data TyDecl : Type where
@@ -41,7 +60,7 @@ data TyDecl : Type where
41 ||| @ fn the name to be declared, fully-qualified
60 ||| @ fn the name to be declared, fully-qualified
42 ||| @ args the arguments to the function
61 ||| @ args the arguments to the function
43 ||| @ ret the final return type
62 ||| @ 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
45
64
46||| A single pattern-matching clause
65||| A single pattern-matching clause
47data FunClause : Type where
66data FunClause : Type where
@@ -51,26 +70,24 @@ data FunClause : Type where
51data FunDefn : Type where
70data FunDefn : Type where
52 DefineFun : TTName -> List FunClause -> FunDefn
71 DefineFun : TTName -> List FunClause -> FunDefn
53
72
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
58
73
59− ||| Indices are allowed to vary across constructors
74+data CtorArg = CtorParameter FunArg | CtorField FunArg
60− Index : TTName -> Erasure -> Raw -> TyConArg
61
75
62||| A reflected datatype definition
76||| A reflected datatype definition
63−data Datatype : Type where
77+record Datatype where
64− ||| A reflected datatype definition
78+ constructor MkDatatype
65− |||
79+
66− ||| @ familyName the name of the type constructor
80+ ||| The name of the type constructor
81+ familyName : TTName
82+
67− ||| @ tyConArgs the arguments to the type constructor
83+ ||| 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) ->
84+ tyConArgs : List TyConArg
85+
86+ ||| The result of the type constructor
87+ tyConRes : Raw
88+
89+ ||| The constructors for the family
72− (constrs : List (TTName, List Arg, Raw)) ->
90+ constructors : List (TTName, List CtorArg, Raw)
73− Datatype
74
91
75||| A reflected elaboration script.
92||| A reflected elaboration script.
76abstract
93abstract
src/Idris/Elab/Term.hs+1−1
@@ -2100,7 +2100,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2100 let decl = TyDecl Ref checked
2100 let decl = TyDecl Ref checked
2101 ctxt' = addCtxtDef n decl ctxt
2101 ctxt' = addCtxtDef n decl ctxt
2102 set_context ctxt'
2102 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) :
2104 new_tyDecls e }
2104 new_tyDecls e }
2105 aux <- getAux
2105 aux <- getAux
2106 returnUnit
2106 returnUnit
src/Idris/Reflection.hs+99−67
@@ -6,9 +6,9 @@ quoters and unquoters along with some supporting datatypes.
6module Idris.Reflection where
6module Idris.Reflection where
7
7
8import Control.Applicative ((<$>), (<*>), pure)
8import Control.Applicative ((<$>), (<*>), pure)
9−import Control.Monad (liftM, liftM2, liftM3)
9+import Control.Monad (liftM, liftM2, liftM4)
10import Data.Maybe (catMaybes)
10import Data.Maybe (catMaybes)
11−import Data.List ((\\))
11+import Data.List ((\\), findIndex)
12import qualified Data.Text as T
12import qualified Data.Text as T
13
13
14import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,
14import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,
@@ -23,27 +23,33 @@ import Idris.Delaborate (delab)
23
23
24data RErasure = RErased | RNotErased deriving Show
24data RErasure = RErased | RNotErased deriving Show
25
25
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
30
34
31−data RTyDecl = RDeclare Name [RArg] Raw deriving Show
35+data RTyDecl = RDeclare Name [RFunArg] Raw deriving Show
32
36
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
36
40
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
38
44
39rArgOpts :: RErasure -> [ArgOpt]
45rArgOpts :: RErasure -> [ArgOpt]
40rArgOpts RErased = [InaccessibleArg]
46rArgOpts RErased = [InaccessibleArg]
41rArgOpts _ = []
47rArgOpts _ = []
42
48
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
47
53
48data RFunClause = RMkFunClause Raw Raw
54data RFunClause = RMkFunClause Raw Raw
49 | RMkImpossibleClause Raw
55 | RMkImpossibleClause Raw
@@ -977,29 +983,31 @@ reifyErasure (P (DCon _ _ _) n _)
977 | n == tacN "NotErased" = return RNotErased
983 | n == tacN "NotErased" = return RNotErased
978reifyErasure tm = fail $ "Can't reify " ++ show tm ++ " as erasure info."
984reifyErasure tm = fail $ "Can't reify " ++ show tm ++ " as erasure info."
979
985
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+
980reifyTyDecl :: Term -> ElabD RTyDecl
1002reifyTyDecl :: Term -> ElabD RTyDecl
981reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
1003reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
982 | n == tacN "Declare" =
1004 | n == tacN "Declare" =
983 do tyN' <- reifyTTName tyN
1005 do tyN' <- reifyTTName tyN
984 args' <- case unList args of
1006 args' <- case unList args of
985 Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."
1007 Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."
986− Just xs -> mapM reifyRArg xs
1008+ Just xs -> mapM reifyRFunArg xs
987 ret' <- reifyRaw ret
1009 ret' <- reifyRaw ret
988 return $ RDeclare tyN' args' ret'
1010 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."
1011reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
1004
1012
1005reifyFunDefn :: Term -> ElabD RFunDefn
1013reifyFunDefn :: Term -> ElabD RFunDefn
@@ -1028,19 +1036,25 @@ envTupleType
1028
1036
1029-- | Apply Idris's implicit info to get a signature. The [PArg] should
1037-- | Apply Idris's implicit info to get a signature. The [PArg] should
1030-- come from a lookup in idris_implicits on IState.
1038-- come from a lookup in idris_implicits on IState.
1031−getArgs :: [PArg] -> Raw -> ([RArg], Raw)
1039+getArgs :: [PArg] -> Raw -> ([RFunArg], Raw)
1032getArgs [] r = ([], r)
1040getArgs [] r = ([], r)
1033getArgs (a:as) (RBind n (Pi _ ty _) sc) =
1041getArgs (a:as) (RBind n (Pi _ ty _) sc) =
1034 let (args, res) = getArgs as sc
1042 let (args, res) = getArgs as sc
1035 erased = if InaccessibleArg `elem` argopts a then RErased else RNotErased
1043 erased = if InaccessibleArg `elem` argopts a then RErased else RNotErased
1036 arg' = case a of
1044 arg' = case a of
1037− PImp {} -> RImplicit n erased ty
1045+ PImp {} -> RFunArg n ty RImplicit erased
1038− PExp {} -> RExplicit n erased ty
1046+ PExp {} -> RFunArg n ty RExplicit erased
1039− PConstraint {} -> RConstraint n erased ty
1047+ PConstraint {} -> RFunArg n ty RConstraint erased
1040− PTacImplicit {} -> RImplicit n erased ty -- TODO?
1048+ PTacImplicit {} -> RFunArg n ty RImplicit erased
1041 in (arg':args, res)
1049 in (arg':args, res)
1042getArgs _ r = ([], r)
1050getArgs _ r = ([], r)
1043
1051
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+
1044-- | Build the reflected datatype definition(s) that correspond(s) to
1058-- | Build the reflected datatype definition(s) that correspond(s) to
1045-- a provided unqualified name
1059-- a provided unqualified name
1046buildDatatypes :: IState -> Name -> [RDatatype]
1060buildDatatypes :: IState -> Name -> [RDatatype]
@@ -1052,44 +1066,62 @@ buildDatatypes ist n =
1052 ctxt = tt_ctxt ist
1066 ctxt = tt_ctxt ist
1053 impls = idris_implicits ist
1067 impls = idris_implicits ist
1054
1068
1055− ctorSig cn = do cty <- fmap forget (lookupTyExact cn ctxt)
1069+ ctorSig params cn = do cty <- fmap forget (lookupTyExact cn ctxt)
1056− argInfo <- lookupCtxtExact cn impls
1070+ argInfo <- lookupCtxtExact cn impls
1057− let (args, res) = getArgs argInfo cty
1071+ let (args, res) = getArgs argInfo cty
1058− return (cn, args, res)
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
1059
1089
1060 mkDataType name (TI {param_pos = params, con_names = constrs}) =
1090 mkDataType name (TI {param_pos = params, con_names = constrs}) =
1061 do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt
1091 do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt
1062 implInfo <- lookupCtxtExact name impls
1092 implInfo <- lookupCtxtExact name impls
1063− let (tcargs, tcres) = getTCArgs params implInfo (forget ty) 0
1093+ let (tcargs, tcres) = getTCArgs params implInfo (forget ty)
1064− ctors <- mapM ctorSig constrs
1094+ ctors <- mapM (ctorSig params) constrs
1065 return $ RDatatype name tcargs tcres ctors
1095 return $ RDatatype name tcargs tcres ctors
1066
1096
1067− getTCArgs params implInfo (RBind an (Pi _ ty _) body) i =
1097+ getTCArgs :: [Int] -> [PArg] -> Raw -> ([RTyConArg], Raw)
1068− let (erased, implInfo') = case implInfo of
1098+ 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)
1099+ let (args, res) = getArgs implInfo tcTy
1075− in if i `elem` params
1100+ in (tcArg args 0, res)
1076− then (RParameter an erased ty : args, res )
1101+ where tcArg [] _ = []
1077− else (RIndex an erased ty : args, res)
1102+ tcArg (arg:args) i | i `elem` params = RParameter arg : tcArg args (i+1)
1078− getTCArgs _ implInfo tm _ = ([], tm)
1103+ | otherwise = RIndex arg : tcArg args (i+1)
1104+
1079
1105
1080reflectErasure :: RErasure -> Raw
1106reflectErasure :: RErasure -> Raw
1081reflectErasure RErased = Var (tacN "Erased")
1107reflectErasure RErased = Var (tacN "Erased")
1082reflectErasure RNotErased = Var (tacN "NotErased")
1108reflectErasure RNotErased = Var (tacN "NotErased")
1083
1109
1084−reflectArg :: RArg -> Raw
1110+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"
1111+reflectPlicity RExplicit = Var (tacN "Explicit")
1091− RImplicit{} -> tacN "Implicit"
1112+reflectPlicity RImplicit = Var (tacN "Implicit")
1092− RConstraint{} -> tacN "Constraint"
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)
1093
1125
1094reflectDatatype :: RDatatype -> Raw
1126reflectDatatype :: RDatatype -> Raw
1095reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
1127reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
@@ -1097,18 +1129,18 @@ reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
1097 , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)
1129 , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)
1098 , reflectRaw tyConRes
1130 , reflectRaw tyConRes
1099 , rawList (rawTripleTy (Var $ reflm "TTName")
1131 , 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"))
1101 (Var $ reflm "Raw"))
1133 (Var $ reflm "Raw"))
1102 [ rawTriple ((Var $ reflm "TTName"),
1134 [ 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")),
1104 (Var $ reflm "Raw"))
1136 (Var $ reflm "Raw"))
1105 (reflectName cn,
1137 (reflectName cn,
1106− rawList (Var $ tacN "Arg") (map reflectArg cargs),
1138+ rawList (Var $ tacN "CtorArg") (map reflectCtorArg cargs),
1107 reflectRaw cty)
1139 reflectRaw cty)
1108 | (cn, cargs, cty) <- constrs
1140 | (cn, cargs, cty) <- constrs
1109 ]
1141 ]
1110 ]
1142 ]
1111− where reflectConArg (RParameter n e t) =
1143+ where reflectConArg (RParameter a) =
1112− raw_apply (Var $ tacN "Parameter") [reflectName n, reflectErasure e, reflectRaw t]
1144+ RApp (Var $ tacN "TyConParameter") (reflectArg a)
1113− reflectConArg (RIndex n e t) =
1145+ reflectConArg (RIndex a) =
1114− raw_apply (Var $ tacN "Index") [reflectName n, reflectErasure e, reflectRaw t]
1146+ RApp (Var $ tacN "TyConIndex") (reflectArg a)