From ae777b8dcbab63fc6c0c17149042af0c5e6312db Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sat, 29 Jun 2019 23:55:17 +0100 Subject: [PATCH] Add parameters blocks --- idris2.ipkg | 1 + src/Core/Core.idr | 5 +++ src/Core/Env.idr | 2 + src/Idris/Error.idr | 3 ++ src/TTImp/Elab.idr | 1 - src/TTImp/Elab/Check.idr | 8 ++-- src/TTImp/ProcessDecls.idr | 3 +- src/TTImp/ProcessParams.idr | 64 ++++++++++++++++++++++++++++++++ tests/Main.idr | 2 +- tests/idris2/basic023/Params.idr | 20 ++++++++++ tests/idris2/basic023/expected | 10 +++++ tests/idris2/basic023/input | 8 ++++ tests/idris2/basic023/run | 3 ++ 13 files changed, 122 insertions(+), 8 deletions(-) create mode 100644 src/TTImp/ProcessParams.idr create mode 100644 tests/idris2/basic023/Params.idr create mode 100644 tests/idris2/basic023/expected create mode 100644 tests/idris2/basic023/input create mode 100755 tests/idris2/basic023/run diff --git a/idris2.ipkg b/idris2.ipkg index 6e38e08..f74f86e 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -103,6 +103,7 @@ modules = TTImp.ProcessData, TTImp.ProcessDecls, TTImp.ProcessDef, + TTImp.ProcessParams, TTImp.ProcessRecord, TTImp.ProcessType, TTImp.TTImp, diff --git a/src/Core/Core.idr b/src/Core/Core.idr index b257255..e4b0d55 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -53,6 +53,7 @@ data Error | IncompatibleFieldUpdate FC (List String) | InvalidImplicits FC (Env Term vars) (List (Maybe Name)) (Term vars) | TryWithImplicits FC (Env Term vars) (List (Name, Term vars)) + | BadUnboundImplicit FC (Env Term vars) Name (Term vars) | CantSolveGoal FC (Env Term vars) (Term vars) | DeterminingArg FC Name Int (Env Term vars) (Term vars) | UnsolvedHoles (List (FC, Name)) @@ -175,6 +176,9 @@ Show Error where = show fc ++ ":Need to bind implicits " ++ showSep "," (map (\x => show (fst x) ++ " : " ++ show (snd x)) imps) ++ "\n(The front end should probably have done this for you. Please report!)" + show (BadUnboundImplicit fc env n ty) + = show fc ++ ":Can't bind name " ++ nameRoot n ++ + " with type " ++ show ty show (CantSolveGoal fc env g) = show fc ++ ":Can't solve goal " ++ assert_total (show g) show (DeterminingArg fc n i env g) @@ -271,6 +275,7 @@ getErrorLoc (NotRecordType loc _) = Just loc getErrorLoc (IncompatibleFieldUpdate loc _) = Just loc getErrorLoc (InvalidImplicits loc _ y tm) = Just loc getErrorLoc (TryWithImplicits loc _ _) = Just loc +getErrorLoc (BadUnboundImplicit loc _ _ _) = Just loc getErrorLoc (CantSolveGoal loc _ tm) = Just loc getErrorLoc (DeterminingArg loc n y env tm) = Just loc getErrorLoc (UnsolvedHoles ((loc, _) :: xs)) = Just loc diff --git a/src/Core/Env.idr b/src/Core/Env.idr index 46e9093..bd79aad 100644 --- a/src/Core/Env.idr +++ b/src/Core/Env.idr @@ -87,6 +87,8 @@ abstractEnvType : FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm abstractEnvType fc [] tm = tm abstractEnvType fc (Let c val ty :: env) tm = abstractEnvType fc env (Bind fc _ (Let c val ty) tm) +abstractEnvType fc (Pi c e ty :: env) tm + = abstractEnvType fc env (Bind fc _ (Pi c e ty) tm) abstractEnvType fc (b :: env) tm = abstractEnvType fc env (Bind fc _ (Pi (multiplicity b) Explicit (binderType b)) tm) diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 18e10c7..c26d7bb 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -150,6 +150,9 @@ perror (TryWithImplicits _ env imps) where tshow : Env Term vars -> (Name, Term vars) -> Core String tshow env (n, ty) = pure $ show n ++ " : " ++ !(pshow env ty) +perror (BadUnboundImplicit _ env n ty) + = pure $ "Can't bind name " ++ nameRoot n ++ " with type " ++ !(pshow env ty) + ++ " here. Try binding explicitly." perror (CantSolveGoal _ env g) = let (_ ** (env', g')) = dropPis env g in pure $ "Can't find an implementation for " ++ !(pshow env' g') diff --git a/src/TTImp/Elab.idr b/src/TTImp/Elab.idr index 0676731..4454c3f 100644 --- a/src/TTImp/Elab.idr +++ b/src/TTImp/Elab.idr @@ -217,7 +217,6 @@ checkTermSub defining mode opts nest env env' sub tm ty = pure $ IPi loc Rig0 Implicit (Just n) !(unelabNoSugar env ty) !(bindImps loc env ntys sc) - export checkTerm : {vars : _} -> {auto c : Ref Ctxt Defs} -> diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr index b4755e8..fb47786 100644 --- a/src/TTImp/Elab/Check.idr +++ b/src/TTImp/Elab/Check.idr @@ -202,18 +202,16 @@ strengthenedEState {n} {vars} c e fc env case (removeArg xnf, shrinkTerm ynf (DropCons SubRefl)) of (Just x', Just y') => pure (f, NameBinding c x' y') - _ => throw (GenericMsg fc ("Invalid unbound implicit " ++ - show f ++ " " ++ show xnf ++ " : " ++ show ynf)) + _ => throw (BadUnboundImplicit fc env f y) strTms defs (f, AsBinding c x y z) = do xnf <- normaliseHoles defs env x ynf <- normaliseHoles defs env y - znf <- normaliseHoles defs env y + znf <- normaliseHoles defs env z case (shrinkTerm xnf (DropCons SubRefl), shrinkTerm ynf (DropCons SubRefl), shrinkTerm znf (DropCons SubRefl)) of (Just x', Just y', Just z') => pure (f, AsBinding c x' y' z') - _ => throw (GenericMsg fc ("Invalid as binding " ++ - show f ++ " " ++ show xnf ++ " : " ++ show ynf)) + _ => throw (BadUnboundImplicit fc env f y) dropTop : (Var (n :: vs)) -> Maybe (Var vs) dropTop (MkVar First) = Nothing diff --git a/src/TTImp/ProcessDecls.idr b/src/TTImp/ProcessDecls.idr index 1899c1b..7d393e7 100644 --- a/src/TTImp/ProcessDecls.idr +++ b/src/TTImp/ProcessDecls.idr @@ -12,6 +12,7 @@ import TTImp.Elab.Check import TTImp.Parser import TTImp.ProcessData import TTImp.ProcessDef +import TTImp.ProcessParams import TTImp.ProcessRecord import TTImp.ProcessType import TTImp.TTImp @@ -30,7 +31,7 @@ process eopts nest env (IData fc vis ddef) process eopts nest env (IDef fc fname def) = processDef eopts nest env fc fname def process eopts nest env (IParameters fc ps decls) - = throw (InternalError "Parameters blocks not yet implemented") + = processParams nest env fc ps decls process eopts nest env (IRecord fc vis rec) = processRecord eopts nest env vis rec process eopts nest env (INamespace fc ns decls) diff --git a/src/TTImp/ProcessParams.idr b/src/TTImp/ProcessParams.idr new file mode 100644 index 0000000..718f15a --- /dev/null +++ b/src/TTImp/ProcessParams.idr @@ -0,0 +1,64 @@ +module TTImp.ProcessParams + +import Core.Context +import Core.Env +import Core.TT +import Core.Unify +import Core.Metadata +import Core.Normalise + +import TTImp.BindImplicits +import TTImp.Elab +import TTImp.Elab.Check +import TTImp.TTImp + +%default covering + +extend : Env Term extvs -> SubVars vs extvs -> + NestedNames extvs -> + Term extvs -> + (vars' ** (SubVars vs vars', Env Term vars', NestedNames vars')) +extend env p nest (Bind fc n (Pi c e ty) sc) + = extend (Pi c e ty :: env) (DropCons p) (weaken nest) sc +extend env p nest tm = (_ ** (p, env, nest)) + +export +processParams : {vars : _} -> + {auto c : Ref Ctxt Defs} -> + {auto m : Ref MD Metadata} -> + {auto u : Ref UST UState} -> + NestedNames vars -> + Env Term vars -> + FC -> List (Name, RawImp) -> List ImpDecl -> + Core () +processParams {vars} {c} {m} {u} nest env fc ps ds + = do -- Turn the parameters into a function type, (x : ps) -> Type, + -- then read off the environment from the elaborated type. This way + -- we'll get all the implicit names we need + let pty_raw = mkParamTy ps + pty_imp <- bindTypeNames vars (IBindHere fc (PI Rig0) pty_raw) + log 10 $ "Checking " ++ show pty_imp + pty <- checkTerm (-1) InType [] + nest env pty_imp (gType fc) + let (vs ** (prf, env', nest')) = extend env SubRefl nest pty + + -- Treat the names in the block as 'nested names' so that we expand + -- the applications as we need to + defNames <- traverse inCurrentNS (definedInBlock ds) + names' <- traverse (applyEnv env') defNames + let nestBlock = record { names $= (names' ++) } nest' + traverse (processDecl [] nestBlock env') ds + pure () + where + mkParamTy : List (Name, RawImp) -> RawImp + mkParamTy [] = IType fc + mkParamTy ((n, ty) :: ps) + = IPi fc RigW Explicit (Just n) ty (mkParamTy ps) + + applyEnv : Env Term vs -> Name -> + Core (Name, (Maybe Name, FC -> NameType -> Term vs)) + applyEnv env n + = do n' <- resolveName n -- it'll be Resolved by expandAmbigName + pure (Resolved n', (Nothing, + \fc, nt => applyTo fc + (Ref fc nt (Resolved n')) env)) diff --git a/tests/Main.idr b/tests/Main.idr index f884df1..a5e3c8a 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -27,7 +27,7 @@ idrisTests "basic006", "basic007", "basic008", "basic009", "basic010", "basic011", "basic012", "basic013", "basic014", "basic015", "basic016", "basic017", "basic018", "basic019", "basic020", - "basic021", "basic022", + "basic021", "basic022", "basic023", "coverage001", "coverage002", "coverage003", "coverage004", "error001", "error002", "error003", "error004", "error005", "error006", diff --git a/tests/idris2/basic023/Params.idr b/tests/idris2/basic023/Params.idr new file mode 100644 index 0000000..ce275a8 --- /dev/null +++ b/tests/idris2/basic023/Params.idr @@ -0,0 +1,20 @@ +parameters (eq : a -> a -> Bool) + lookup : a -> List (a, b) -> Maybe b + lookup x [] = Nothing + lookup x ((k, v) :: ys) + = if eq x k + then Just v + else lookup x ys + + data Dict : Type -> Type where + MkDict : List (a, b) -> Dict b + + lookupK : a -> Dict b -> Maybe b + lookupK k (MkDict xs) = lookup k xs + +testDict : Dict {a=Int} (==) String +testDict = MkDict _ [(0, "foo"), (1, "bar")] + +parameters (y : ?) -- test that the type of 'y' can be inferred + foo : (x : Int) -> x = y -> Int + foo x@_ Refl = 42 diff --git a/tests/idris2/basic023/expected b/tests/idris2/basic023/expected new file mode 100644 index 0000000..a3862a7 --- /dev/null +++ b/tests/idris2/basic023/expected @@ -0,0 +1,10 @@ +1/1: Building Params (Params.idr) +Welcome to Idris 2 version 0.0. Enjoy yourself! +Main> Main.Dict : (a -> a -> Bool) -> Type -> Type +Main> Main.MkDict : (eq : (a -> a -> Bool)) -> List (a, b) -> Dict eq b +Main> Main.lookup : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b +Main> Main.lookupK : (eq : (a -> a -> Bool)) -> a -> Dict eq b -> Maybe b +Main> MkDict (\{arg:0} => (\{arg:1} => (intToBool (prim__eq_Int arg arg)))) [(0, "foo"), (1, "bar")] +Main> Just "bar" +Main> Nothing +Main> Bye for now! diff --git a/tests/idris2/basic023/input b/tests/idris2/basic023/input new file mode 100644 index 0000000..dc51de7 --- /dev/null +++ b/tests/idris2/basic023/input @@ -0,0 +1,8 @@ +:t Dict +:t MkDict +:t lookup +:t lookupK +testDict +lookupK _ 1 testDict +lookupK _ 2 testDict +:q diff --git a/tests/idris2/basic023/run b/tests/idris2/basic023/run new file mode 100755 index 0000000..ceacfe1 --- /dev/null +++ b/tests/idris2/basic023/run @@ -0,0 +1,3 @@ +$1 Params.idr < input + +rm -rf build