Added named holes

Unlike in blodwen, it is okay for a named hole to be solved by
unification. (Is this the right choice?)

src/Core/Binary.idr

@@ -139,7 +139,7 @@ readTTCFile modns as r b
            gam' <- updateEntries (gamma defs) modns as 0 (max r) r
            setCtxt gam' 
            holes <- fromBuf r b
-           coreLift $ putStrLn $ "Read " ++ show holes ++ " holes"
+           coreLift $ putStrLn $ "Read " ++ show (length holes) ++ " holes"
            guesses <- fromBuf r b
            coreLift $ putStrLn $ "Read " ++ show (length guesses) ++ " guesses"
            constraints <- the (Core (List (Int, Constraint))) $ fromBuf r b

src/Core/Context.idr

@@ -420,9 +420,9 @@ TTC GlobalDef where
                  toBuf b (multiplicity gdef)
                  toBuf b (visibility gdef)
                  toBuf b (totality gdef)
+                 toBuf b (flags gdef)
                  toBuf b (map fst (toList (refersTo gdef)))
                  toBuf b (noCycles gdef)
-                 toBuf b (flags gdef)
 
   fromBuf r b 
       = do name <- fromBuf r b
@@ -431,7 +431,8 @@ TTC GlobalDef where
               then do loc <- fromBuf r b; 
                       ty <- fromBuf r b; mul <- fromBuf r b
                       vis <- fromBuf r b; tot <- fromBuf r b
-                      refsList <- fromBuf r b; fl <- fromBuf r b
+                      fl <- fromBuf r b
+                      refsList <- fromBuf r b; 
                       let refs = fromList (map (\x => (x, ())) refsList)
                       c <- fromBuf r b
                       pure (MkGlobalDef loc name ty mul vis tot fl refs c def)

src/Core/Env.idr

@@ -109,3 +109,9 @@ abstractFullEnvType fc (b :: env) tm
     = abstractFullEnvType fc env (Bind fc _ 
 						(Pi (multiplicity b) Explicit (binderType b)) tm)
 
+export
+letToLam : Env Term vars -> Env Term vars
+letToLam [] = []
+letToLam (Let c val ty :: env) = Lam c Explicit ty :: letToLam env
+letToLam (b :: env) = b :: letToLam env
+

src/TTImp/Elab/App.idr

@@ -195,8 +195,8 @@ mutual
                   InLHS _ => -- reset hole and redo it with the unexpanded definition
                      do updateDef (Resolved idx) (const (Just (Hole False)))
                         convert fc elabinfo env 
-                                   (gnfOpts withHoles (noLet env) metaval) 
-                                   (gnfOpts withHoles (noLet env) argv)
+                                   (gnfOpts withHoles (letToLam env) metaval) 
+                                   (gnfOpts withHoles (letToLam env) argv)
                         pure ()
                   _ => pure ()
              removeHoleName nm
@@ -216,12 +216,6 @@ mutual
              fnty <- sc defs (toClosure defaultOpts env argv)
              checkAppWith rig elabinfo nest env fc
                           fntm fnty expargs impargs kr expty
-    where
-      noLet : Env Term vs -> Env Term vs
-      noLet [] = []
-      noLet (Let c v t :: env) = Lam c Explicit t :: noLet env
-      noLet (b :: env) = b :: noLet env
-
 
   -- Check an application of 'fntm', with type 'fnty' to the given list
   -- of explicit and implicit arguments.

src/TTImp/Elab/Hole.idr

@@ -0,0 +1,38 @@
+module TTImp.Elab.As
+
+import Core.Context
+import Core.Core
+import Core.Env
+import Core.Normalise
+import Core.Unify
+import Core.TT
+import Core.Value
+
+import TTImp.Elab.Check
+import TTImp.TTImp
+
+%default covering
+
+export
+checkHole : {vars : _} ->
+            {auto c : Ref Ctxt Defs} ->
+            {auto u : Ref UST UState} ->
+            {auto e : Ref EST (EState vars)} ->
+            RigCount -> ElabInfo ->
+            NestedNames vars -> Env Term vars -> 
+            FC -> String -> Maybe (Glued vars) ->
+            Core (Term vars, Glued vars)
+checkHole rig elabinfo nest env fc n_in (Just gexpty)
+    = do nm <- inCurrentNS (UN n_in)
+         expty <- getTerm gexpty
+         let env' = letToLam env -- we want all the names to appear in the
+                                 -- hole type
+         metaval <- metaVar fc rig env' nm expty
+         pure (metaval, gexpty)
+checkHole rig elabinfo nest env fc n_in exp
+    = do nmty <- genName "holeTy"
+         ty <- metaVar fc Rig0 env nmty (TType fc)
+         nm <- inCurrentNS (UN n_in)
+         let env' = letToLam env
+         metaval <- metaVar fc rig env' nm ty
+         pure (metaval, gnf env ty)

src/TTImp/Elab/Term.idr

@@ -14,6 +14,7 @@ import TTImp.Elab.As
 import TTImp.Elab.Binders
 import TTImp.Elab.Case
 import TTImp.Elab.Check
+import TTImp.Elab.Hole
 import TTImp.Elab.ImplicitBind
 import TTImp.Elab.Local
 import TTImp.Elab.Prim
@@ -142,7 +143,7 @@ checkTerm rig elabinfo nest env (IType fc) exp
     = checkExp rig elabinfo env fc (TType fc) (gType fc) exp
 
 checkTerm rig elabinfo nest env (IHole fc str) exp
-    = throw (InternalError "holes not implemented")
+    = checkHole rig elabinfo nest env fc str exp
 checkTerm rig elabinfo nest env (Implicit fc b) (Just gexpty)
     = do nm <- genName "imp"
          expty <- getTerm gexpty

src/TTImp/Parser.idr

@@ -45,6 +45,10 @@ atom fname
          x <- unqualifiedName
          end <- location
          pure (IBindVar (MkFC fname start end) x)
+  <|> do start <- location
+         x <- holeName
+         end <- location
+         pure (IHole (MkFC fname start end) x)
 
 visibility : EmptyRule Visibility
 visibility

src/TTImp/ProcessDef.idr

@@ -154,7 +154,7 @@ checkClause mult hashit n nest env (PatClause fc lhs_in rhs)
          -- Normalise the LHS to get any functions or let bindings evaluated
          -- (this might be allowed, e.g. for 'fromInteger')
          defs <- get Ctxt
-         lhstm <- normaliseLHS defs (noLet env) lhstm
+         lhstm <- normaliseLHS defs (letToLam env) lhstm
          lhsty <- normaliseHoles defs env lhsty
          linvars_in <- findLinear True 0 Rig1 lhstm
          log 5 $ "Linearity of names in " ++ show n ++ ": " ++ 
@@ -174,11 +174,6 @@ checkClause mult hashit n nest env (PatClause fc lhs_in rhs)
 
          logTerm 5 "RHS term" rhstm
          pure (Just (MkClause env' lhstm' rhstm))
-  where
-    noLet : Env Term vs -> Env Term vs
-    noLet [] = []
-    noLet (Let c v t :: env) = Lam c Explicit t :: noLet env
-    noLet (b :: env) = b :: noLet env
 
 toPats : Clause -> (vs ** (Env Term vs, Term vs, Term vs))
 toPats (MkClause {vars} env lhs rhs) 

tests/Main.idr

@@ -7,7 +7,7 @@ import System
 ttimpTests : List String
 ttimpTests 
     = ["basic001", "basic002", "basic003", "basic004", "basic005",
-       "basic006",
+       "basic006", "basic007",
        "eta001", "eta002",
        "nest001", "nest002",
        "perf001", "perf002", "perf003"]

tests/ttimp/basic001/expected

@@ -4,7 +4,7 @@ Yaffle> (Main.S (Main.S (Main.S (Main.S Main.Z))))
 Yaffle> (Main.S (Main.S (Main.S (Main.S (Main.S Main.Z)))))
 Yaffle> Bye for now!
 Processing as TTC
-Read [] holes
+Read 0 holes
 Read 0 guesses
 Read 31 constraints
 Read TTC

tests/ttimp/basic007/Hole.yaff

@@ -0,0 +1,15 @@
+data Nat : Type where
+     Z : Nat
+     S : Nat -> Nat
+
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z $a
+     Cons : $a -> Vect $k $a -> Vect (S $k) $a
+
+plus : Nat -> Nat -> Nat
+plus Z $y = y
+plus (S $k) $y = S (plus k y)
+
+append : Vect $n $a -> Vect $m $a -> Vect (plus $n $m) $a
+append Nil $ys = ys
+append (Cons $x $xs) $ys = Cons $x ?foo

tests/ttimp/basic007/expected

@@ -0,0 +1,11 @@
+Processing as TTImp
+Written TTC
+Yaffle> (%pi Rig0 Explicit Just {m:39} Main.Nat (%pi Rig0 Explicit Just {a:38} %type (%pi Rig0 Explicit Just {k:37} Main.Nat (%pi RigW Explicit Nothing {a:38} (%pi RigW Explicit Nothing ((Main.Vect {k:37}) {a:38}) (%pi RigW Explicit Nothing ((Main.Vect {m:39}) {a:38}) ((Main.Vect ((Main.plus {k:37}) {m:39})) {a:38})))))))
+Yaffle> Bye for now!
+Processing as TTC
+Read 2 holes
+Read 0 guesses
+Read 0 constraints
+Read TTC
+Yaffle> (%pi Rig0 Explicit Just {m:39} Main.Nat (%pi Rig0 Explicit Just {a:38} %type (%pi Rig0 Explicit Just {k:37} Main.Nat (%pi RigW Explicit Nothing {a:38} (%pi RigW Explicit Nothing ((Main.Vect {k:37}) {a:38}) (%pi RigW Explicit Nothing ((Main.Vect {m:39}) {a:38}) ((Main.Vect ((Main.plus {k:37}) {m:39})) {a:38})))))))
+Yaffle> Bye for now!

tests/ttimp/basic007/input

@@ -0,0 +1,2 @@
+:t foo
+:q

tests/ttimp/basic007/run

@@ -0,0 +1,4 @@
+$1 Hole.yaff < input
+$1 build/Hole.ttc < input
+
+rm -rf build

yaffle.ipkg

@@ -45,6 +45,7 @@ modules =
     TTImp.Elab.As,
     TTImp.Elab.Binders,
     TTImp.Elab.Check,
+    TTImp.Elab.Hole,
     TTImp.Elab.ImplicitBind,
     TTImp.Elab.Local,
     TTImp.Elab.Prim,