Add parameters blocks

idris2.ipkg

@@ -103,6 +103,7 @@ modules =
     TTImp.ProcessData,
     TTImp.ProcessDecls,
     TTImp.ProcessDef,
+    TTImp.ProcessParams,
     TTImp.ProcessRecord,
     TTImp.ProcessType,
     TTImp.TTImp,

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

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)

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')

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} ->

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 " ++ 
+               _ => throw (BadUnboundImplicit fc env f y)
-                               show f ++ " " ++ show xnf ++ " : " ++ show ynf))
     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 " ++ 
+               _ => throw (BadUnboundImplicit fc env f y)
-                               show f ++ " " ++ show xnf ++ " : " ++ show ynf))
 
     dropTop : (Var (n :: vs)) -> Maybe (Var vs)
     dropTop (MkVar First) = Nothing

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)

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))

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",

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

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!

tests/idris2/basic023/input

@@ -0,0 +1,8 @@
+:t Dict
+:t MkDict
+:t lookup
+:t lookupK
+testDict
+lookupK _ 1 testDict
+lookupK _ 2 testDict
+:q

tests/idris2/basic023/run

@@ -0,0 +1,3 @@
+$1 Params.idr < input
+
+rm -rf build