@@ -16,12 +16,14 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
1616 Def(..), CaseInfo(..), CaseDefs(..),
1717 Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),
1818 Context, initContext, ctxtAlist, next_tvar,
19− addToCtxt, setAccess, setInjective, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
19+ addToCtxt, setAccess, setInjective, setTotal, setRigCount,
20+ setMetaInformation, addCtxtDef, addTyDecl,
2021 addDatatype, addCasedef, simplifyCasedef, addOperator,
2122 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
2223 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
2324 mapDefCtxt, tcReducible,
2425 lookupTotal, lookupTotalExact, lookupInjectiveExact,
26+ lookupRigCount, lookupRigCountExact,
2527 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,
2628 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,
2729 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
@@ -866,9 +868,11 @@ data MetaInformation =
866868
867869-- | Contexts used for global definitions and for proof state. They contain
868870-- universe constraints and existing definitions.
871+-- Also store maximum RigCount of the name (can't bind a name at multiplicity
872+-- 1 in a RigW, for example)
869873data Context = MkContext {
870874 next_tvar :: Int,
871− definitions :: Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation)
875+ definitions :: Ctxt (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)
872876 } deriving (Show, Generic)
873877
874878
@@ -878,53 +882,59 @@ initContext = MkContext 0 emptyContext
878882
879883mapDefCtxt :: (Def -> Def) -> Context -> Context
880884mapDefCtxt f (MkContext t !defs) = MkContext t (mapCtxt f' defs)
881− where f' (!d, i, a, t, m) = f' (f d, i, a, t, m)
885+ where f' (!d, r, i, a, t, m) = f' (f d, r, i, a, t, m)
882886
883887-- | Get the definitions from a context
884888ctxtAlist :: Context -> [(Name, Def)]
885−ctxtAlist ctxt = map (\(n, (d, i, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)
889+ctxtAlist ctxt = map (\(n, (d, r, i, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)
886890
887891veval ctxt env t = evalState (eval False ctxt [] env t []) initEval
888892
889893addToCtxt :: Name -> Term -> Type -> Context -> Context
890894addToCtxt n tm ty uctxt
891895 = let ctxt = definitions uctxt
892− !ctxt' = addDef n (Function ty tm, False, Public, Unchecked, EmptyMI) ctxt in
896+ !ctxt' = addDef n (Function ty tm, RigW, False, Public, Unchecked, EmptyMI) ctxt in
893897 uctxt { definitions = ctxt' }
894898
895899setAccess :: Name -> Accessibility -> Context -> Context
896900setAccess n a uctxt
897901 = let ctxt = definitions uctxt
898− !ctxt' = updateDef n (\ (d, i, _, t, m) -> (d, i, a, t, m)) ctxt in
902+ !ctxt' = updateDef n (\ (d, r, i, _, t, m) -> (d, r, i, a, t, m)) ctxt in
899903 uctxt { definitions = ctxt' }
900904
901905setInjective :: Name -> Injectivity -> Context -> Context
902906setInjective n i uctxt
903907 = let ctxt = definitions uctxt
904− !ctxt' = updateDef n (\ (d, _, a, t, m) -> (d, i, a, t, m)) ctxt in
908+ !ctxt' = updateDef n (\ (d, r, _, a, t, m) -> (d, r, i, a, t, m)) ctxt in
905909 uctxt { definitions = ctxt' }
906910
907911setTotal :: Name -> Totality -> Context -> Context
908912setTotal n t uctxt
909913 = let ctxt = definitions uctxt
910− !ctxt' = updateDef n (\ (d, i, a, _, m) -> (d, i, a, t, m)) ctxt in
914+ !ctxt' = updateDef n (\ (d, r, i, a, _, m) -> (d, r, i, a, t, m)) ctxt in
915+ uctxt { definitions = ctxt' }
916+
917+setRigCount :: Name -> RigCount -> Context -> Context
918+setRigCount n rc uctxt
919+ = let ctxt = definitions uctxt
920+ !ctxt' = updateDef n (\ (d, _, i, a, t, m) -> (d, rc, i, a, t, m)) ctxt in
911921 uctxt { definitions = ctxt' }
912922
913923setMetaInformation :: Name -> MetaInformation -> Context -> Context
914924setMetaInformation n m uctxt
915925 = let ctxt = definitions uctxt
916− !ctxt' = updateDef n (\ (d, i, a, t, _) -> (d, i, a, t, m)) ctxt in
926+ !ctxt' = updateDef n (\ (d, r, i, a, t, _) -> (d, r, i, a, t, m)) ctxt in
917927 uctxt { definitions = ctxt' }
918928
919929addCtxtDef :: Name -> Def -> Context -> Context
920930addCtxtDef n d c = let ctxt = definitions c
921− !ctxt' = addDef n (d, False, Public, Unchecked, EmptyMI) $! ctxt in
931+ !ctxt' = addDef n (d, RigW, False, Public, Unchecked, EmptyMI) $! ctxt in
922932 c { definitions = ctxt' }
923933
924934addTyDecl :: Name -> NameType -> Type -> Context -> Context
925935addTyDecl n nt ty uctxt
926936 = let ctxt = definitions uctxt
927− !ctxt' = addDef n (TyDecl nt ty, False, Public, Unchecked, EmptyMI) ctxt in
937+ !ctxt' = addDef n (TyDecl nt ty, RigW, False, Public, Unchecked, EmptyMI) ctxt in
928938 uctxt { definitions = ctxt' }
929939
930940addDatatype :: Datatype Name -> Context -> Context
@@ -932,14 +942,14 @@ addDatatype (Data n tag ty unique cons) uctxt
932942 = let ctxt = definitions uctxt
933943 ty' = normalise uctxt [] ty
934944 !ctxt' = addCons 0 cons (addDef n
935− (TyDecl (TCon tag (arity ty')) ty, True, Public, Unchecked, EmptyMI) ctxt) in
945+ (TyDecl (TCon tag (arity ty')) ty, RigW, True, Public, Unchecked, EmptyMI) ctxt) in
936946 uctxt { definitions = ctxt' }
937947 where
938948 addCons tag [] ctxt = ctxt
939949 addCons tag ((n, ty) : cons) ctxt
940950 = let ty' = normalise uctxt [] ty in
941951 addCons (tag+1) cons (addDef n
942− (TyDecl (DCon tag (arity ty') unique) ty, True, Public, Unchecked, EmptyMI) ctxt)
952+ (TyDecl (DCon tag (arity ty') unique) ty, RigW, True, Public, Unchecked, EmptyMI) ctxt)
943953
944954-- FIXME: Too many arguments! Refactor all these Bools.
945955--
@@ -973,7 +983,7 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)
973983 (args_rt, sc_rt)
974984 op = (CaseOp (ci { case_inlinable = inlc })
975985 ty argtys ps_in ps_ct cdef,
976− False, access, Unchecked, EmptyMI)
986+ RigW, False, access, Unchecked, EmptyMI)
977987 in return $ addDef n op ctxt
978988-- other -> tfail (Msg $ "Error adding case def: " ++ show other)
979989 return uctxt { definitions = ctxt' }
@@ -986,15 +996,15 @@ simplifyCasedef :: Name -> ErasureInfo -> Context -> TC Context
986996simplifyCasedef n ei uctxt
987997 = do let ctxt = definitions uctxt
988998 ctxt' <- case lookupCtxt n ctxt of
989− [(CaseOp ci ty atys [] ps _, inj, acc, tot, metainf)] ->
999+ [(CaseOp ci ty atys [] ps _, rc, inj, acc, tot, metainf)] ->
9901000 return ctxt -- nothing to simplify (or already done...)
991− [(CaseOp ci ty atys ps_in ps cd, inj, acc, tot, metainf)] ->
1001+ [(CaseOp ci ty atys ps_in ps cd, rc, inj, acc, tot, metainf)] ->
9921002 do let ps_in' = map simpl ps_in
9931003 pdef = map debind ps_in'
9941004 CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei
9951005 return $ addDef n (CaseOp ci
9961006 ty atys ps_in' ps (cd { cases_compiletime = (args, sc) }),
997− inj, acc, tot, metainf) ctxt
1007+ rc, inj, acc, tot, metainf) ctxt
9981008
9991009 _ -> return ctxt
10001010 return uctxt { definitions = ctxt' }
@@ -1014,10 +1024,10 @@ addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
10141024 Context -> Context
10151025addOperator n ty a op uctxt
10161026 = let ctxt = definitions uctxt
1017− ctxt' = addDef n (Operator ty a op, False, Public, Unchecked, EmptyMI) ctxt in
1027+ ctxt' = addDef n (Operator ty a op, RigW, False, Public, Unchecked, EmptyMI) ctxt in
10181028 uctxt { definitions = ctxt' }
10191029
1020−tfst (a, _, _, _, _) = a
1030+tfst (a, _, _, _, _, _) = a
10211031
10221032lookupNames :: Name -> Context -> [Name]
10231033lookupNames n ctxt
@@ -1103,10 +1113,10 @@ lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]
11031113lookupP_all all exact n ctxt
11041114 = do (n', def) <- names
11051115 p <- case def of
1106− (Function ty tm, inj, a, _, _) -> return (P Ref n' ty, a)
1107− (TyDecl nt ty, _, a, _, _) -> return (P nt n' ty, a)
1108− (CaseOp _ ty _ _ _ _, inj, a, _, _) -> return (P Ref n' ty, a)
1109− (Operator ty _ _, inj, a, _, _) -> return (P Ref n' ty, a)
1116+ (Function ty tm, _, inj, a, _, _) -> return (P Ref n' ty, a)
1117+ (TyDecl nt ty, _, _, a, _, _) -> return (P nt n' ty, a)
1118+ (CaseOp _ ty _ _ _ _, _, inj, a, _, _) -> return (P Ref n' ty, a)
1119+ (Operator ty _ _, _, inj, a, _, _) -> return (P Ref n' ty, a)
11101120 case snd p of
11111121 Hidden -> if all then return (fst p) else []
11121122 Private -> if all then return (fst p) else []
@@ -1133,28 +1143,36 @@ lookupDefAcc :: Name -> Bool -> Context ->
11331143lookupDefAcc n mkpublic ctxt
11341144 = map mkp $ lookupCtxt n (definitions ctxt)
11351145 -- io_bind a special case for REPL prettiness
1136− where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))
1137− then (d, Public) else (d, a)
1146+ where mkp (d, _, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))
1147+ then (d, Public) else (d, a)
11381148
11391149lookupDefAccExact :: Name -> Bool -> Context ->
11401150 Maybe (Def, Accessibility)
11411151lookupDefAccExact n mkpublic ctxt
11421152 = fmap mkp $ lookupCtxtExact n (definitions ctxt)
11431153 -- io_bind a special case for REPL prettiness
1144− where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))
1145− then (d, Public) else (d, a)
1154+ where mkp (d, _, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))
1155+ then (d, Public) else (d, a)
11461156
11471157lookupTotal :: Name -> Context -> [Totality]
11481158lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
1149− where mkt (d, inj, a, t, m) = t
1159+ where mkt (d, _, inj, a, t, m) = t
11501160
11511161lookupTotalExact :: Name -> Context -> Maybe Totality
11521162lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)
1153− where mkt (d, inj, a, t, m) = t
1163+ where mkt (d, _, inj, a, t, m) = t
1164+
1165+lookupRigCount :: Name -> Context -> [Totality]
1166+lookupRigCount n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
1167+ where mkt (d, _, inj, a, t, m) = t
1168+
1169+lookupRigCountExact :: Name -> Context -> Maybe RigCount
1170+lookupRigCountExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)
1171+ where mkt (d, rc, inj, a, t, m) = rc
11541172
11551173lookupInjectiveExact :: Name -> Context -> Maybe Injectivity
11561174lookupInjectiveExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)
1157− where mkt (d, inj, a, t, m) = inj
1175+ where mkt (d, _, inj, a, t, m) = inj
11581176
11591177-- Check if a name is reducible in the type checker. Partial definitions
11601178-- are not reducible (so treated as a constant)
@@ -1166,10 +1184,10 @@ tcReducible n ctxt = case lookupTotalExact n ctxt of
11661184
11671185lookupMetaInformation :: Name -> Context -> [MetaInformation]
11681186lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)
1169− where mkm (d, inj, a, t, m) = m
1187+ where mkm (d, _, inj, a, t, m) = m
11701188
11711189lookupNameTotal :: Name -> Context -> [(Name, Totality)]
1172−lookupNameTotal n = map (\(n, (_, _, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions
1190+lookupNameTotal n = map (\(n, (_, _, _, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions
11731191
11741192
11751193lookupVal :: Name -> Context -> [Value]