[ re #2041 ] better runtime error for holey expression (#2045)

.github/workflows/ci-idris2.yml

@@ -337,6 +337,7 @@ jobs:
   ubuntu-self-host-racket:
     needs: ubuntu-bootstrap-racket
     runs-on: ubuntu-latest
+    if: false
     env:
       IDRIS2_CG: racket
     steps:

src/Compiler/Common.idr

@@ -120,7 +120,6 @@ execute {c} cg tm
          let tmpDir = execBuildDir d
          ensureDirectoryExists tmpDir
          executeExpr cg c tmpDir tm
-         pure ()
 
 export
 incCompile : {auto c : Ref Ctxt Defs} ->
@@ -166,7 +165,8 @@ getAllDesc (n@(Resolved i) :: rest) arr defs
   = do Nothing <- coreLift $ readArray arr i
            | Just _ => getAllDesc rest arr defs
        case !(lookupContextEntry n (gamma defs)) of
-            Nothing => getAllDesc rest arr defs
+            Nothing => do log "compile.execute" 20 $ "Couldn't find " ++ show n
+                          getAllDesc rest arr defs
             Just (_, entry) =>
               do (def, bin) <- getMinimalDef entry
                  ignore $ addDef n def
@@ -176,9 +176,13 @@ getAllDesc (n@(Resolved i) :: rest) arr defs
                             let refs = refersToRuntime def
                             refs' <- traverse toResolvedNames (keys refs)
                             getAllDesc (refs' ++ rest) arr defs
-                    else getAllDesc rest arr defs
+                    else do log "compile.execute" 20
+                               $ "Dropping " ++ show n ++ " because it's erased"
+                            getAllDesc rest arr defs
 getAllDesc (n :: rest) arr defs
-  = getAllDesc rest arr defs
+  = do log "compile.execute" 20 $
+         "Ignoring " ++ show n ++ " because it's not a Resolved name"
+       getAllDesc rest arr defs
 
 warnIfHole : Name -> NamedDef -> Core ()
 warnIfHole n (MkNmError _)
@@ -236,27 +240,61 @@ export
 getCompileData : {auto c : Ref Ctxt Defs} -> (doLazyAnnots : Bool) ->
                  UsePhase -> ClosedTerm -> Core CompileData
 getCompileData doLazyAnnots phase_in tm_in
-    = do defs <- get Ctxt
+    = do log "compile.execute" 10 $ "Getting compiled data for: " ++ show tm_in
          sopts <- getSession
          let phase = foldl {t=List} (flip $ maybe id max) phase_in $
-                         [Cases <$ dumpcases sopts, Lifted <$ dumplifted sopts, ANF <$ dumpanf sopts, VMCode <$ dumpvmcode sopts]
-         let ns = getRefs (Resolved (-1)) tm_in
+                       [ Cases <$ dumpcases sopts
+                       , Lifted <$ dumplifted sopts
+                       , ANF <$ dumpanf sopts
+                       , VMCode <$ dumpvmcode sopts
+                       ]
+
+         -- When we compile a REPL expression, there may be leftovers holes in it.
+         -- Turn these into runtime errors.
+         let metas = addMetas True empty tm_in
+         for_ (keys metas) $ \ metanm =>
+             do defs <- get Ctxt
+                Just gdef <- lookupCtxtExact metanm (gamma defs)
+                  | Nothing => log "compile.execute" 50 $ unwords
+                                    [ "Couldn't find"
+                                    , show metanm
+                                    , "(probably impossible)"]
+                let Hole _ _ = definition gdef
+                  | _ => pure ()
+                let fulln = fullname gdef
+                let cexp = MkError $ CCrash emptyFC
+                         $ "Encountered unimplemented hole " ++ show fulln
+                ignore $ addDef metanm ({ compexpr := Just cexp
+                                        , namedcompexpr := Just (forgetDef cexp)
+                                        } gdef)
+
+         let refs  = getRefs (Resolved (-1)) tm_in
+         let ns = mergeWith const metas refs
+         log "compile.execute" 70 $
+           "Found names: " ++ concat (intersperse ", " $ map show $ keys ns)
          tm <- toFullNames tm_in
          natHackNames' <- traverse toResolvedNames natHackNames
          -- make an array of Bools to hold which names we've found (quicker
          -- to check than a NameMap!)
          asize <- getNextEntry
          arr <- coreLift $ newArray asize
+
+         defs <- get Ctxt
          logTime "++ Get names" $ getAllDesc (natHackNames' ++ keys ns) arr defs
 
          let entries = catMaybes !(coreLift (toList arr))
          let allNs = map (Resolved . fst) entries
          cns <- traverse toFullNames allNs
+         log "compile.execute" 30 $
+           "All names: " ++ concat (intersperse ", " $ map show $ zip allNs cns)
 
          -- Do a round of merging/arity fixing for any names which were
          -- unknown due to cyclic modules (i.e. declared in one, defined in
          -- another)
          rcns <- filterM nonErased cns
+         log "compile.execute" 40 $
+           "Kept: " ++ concat (intersperse ", " $ map show rcns)
+
          logTime "++ Merge lambda" $ traverse_ mergeLamDef rcns
          logTime "++ Fix arity" $ traverse_ fixArityDef rcns
          compiledtm <- fixArityExp !(compileExp tm)

src/Compiler/Opts/CSE.idr

@@ -302,9 +302,11 @@ analyzeName :  Ref Sts St
 analyzeName fn = do
     defs <- get Ctxt
     Just def <- lookupCtxtExact fn (gamma defs)
-        | Nothing => pure Nothing
+        | Nothing => do log "compile.execute" 50 $ "Couldn't find " ++ show fn
+                        pure Nothing
     let Just cexp = compexpr def
-        | Nothing => pure Nothing
+        | Nothing => do log "compile.execute" 50 $ "Couldn't compile " ++ show fn
+                        pure Nothing
     cexp' <- analyzeDef cexp
     pure $ Just (fn, location def, cexp')
 
@@ -473,7 +475,7 @@ cse :  Ref Ctxt Defs
 cse defs me = do
   log "compiler.cse" 10 $ "Analysing " ++ show (length defs) ++ " names"
   s            <- newRef Sts $ MkSt empty 0
-  analyzedDefs <- mapMaybe id <$> traverse analyzeName defs
+  analyzedDefs <- catMaybes <$> traverse analyzeName defs
   MkSt um _    <- get Sts
   srep         <- newRef ReplaceMap $ toReplaceMap um
   replacedDefs <- traverse replaceDef analyzedDefs

src/Compiler/Scheme/Chez.idr

@@ -461,7 +461,6 @@ compileToSS c prof appdir tm outfile
          Right () <- coreLift $ writeFile outfile scm
             | Left err => throw (FileErr outfile err)
          coreLift_ $ chmodRaw outfile 0o755
-         pure ()
 
 ||| Compile a Chez Scheme source file to an executable, daringly with runtime checks off.
 compileToSO : {auto c : Ref Ctxt Defs} ->
@@ -591,7 +590,6 @@ executeExpr c tmpDir tm
     = do Just sh <- compileExpr False c tmpDir tmpDir tm "_tmpchez"
             | Nothing => throw (InternalError "compileExpr returned Nothing")
          coreLift_ $ system sh
-         pure ()
 
 incCompile : Ref Ctxt Defs ->
              (sourceFile : String) -> Core (Maybe (String, List String))

src/Core/Case/CaseTree.idr

@@ -282,7 +282,7 @@ addRefs at ns = getNames (addRefs False at) ns
 
 export
 getMetas : CaseTree vars -> NameMap Bool
-getMetas = getNames addMetas empty
+getMetas = getNames (addMetas False) empty
 
 export
 mkTerm : (vars : List Name) -> Pat -> Term vars

src/Core/Context.idr

@@ -379,8 +379,11 @@ HasNames (Term vars) where
       = do Just gdef <- lookupCtxtExact (Resolved i) gam
                 | Nothing => pure (Ref fc x (Resolved i))
            pure (Ref fc x (fullname gdef))
-  full gam (Meta fc x y xs)
-      = pure (Meta fc x y !(traverse (full gam) xs))
+  full gam (Meta fc x i xs)
+      = do xs <- traverse (full gam) xs
+           pure $ case !(lookupCtxtExact (Resolved i) gam) of
+             Nothing => Meta fc x i xs
+             Just gdef => Meta fc (fullname gdef) i xs
   full gam (Bind fc x b scope)
       = pure (Bind fc x !(traverse (full gam) b) !(full gam scope))
   full gam (App fc fn arg)

src/Core/Options/Log.idr

@@ -43,6 +43,7 @@ knownTopics = [
     ("builtin.Natural", Just "Log each encountered %builtin Natural declaration."),
     ("builtin.NaturalToInteger", Just "Log each encountered %builtin NaturalToInteger declaration."),
     ("builtin.IntegerToNatural", Just "Log each encountered %builtin IntegerToNatural declaration."),
+    ("compile.execute", Nothing),
     ("compile.casetree", Nothing),
     ("compile.casetree.clauses", Nothing),
     ("compile.casetree.getpmdef", Nothing),

src/Core/SchemeEval/Evaluate.idr

@@ -72,7 +72,7 @@ seval mode env tm
          -- since we last evaluated a name, and we might have evaluated the
          -- name in a different mode
          let ms = getRefs (MN "" 0) tm
-         let rs = addMetas ms tm
+         let rs = addMetas False ms tm
          names <- getAllNames empty (keys rs)
          traverse_ (compileDef mode) (keys names)
 

src/Core/TT.idr

@@ -1641,33 +1641,34 @@ substName x new (TForce fc r y)
 substName x new tm = tm
 
 export
-addMetas : NameMap Bool -> Term vars -> NameMap Bool
-addMetas ns (Local fc x idx y) = ns
-addMetas ns (Ref fc x name) = ns
-addMetas ns (Meta fc n i xs) = addMetaArgs (insert n False ns) xs
+addMetas : (usingResolved : Bool) -> NameMap Bool -> Term vars -> NameMap Bool
+addMetas res ns (Local fc x idx y) = ns
+addMetas res ns (Ref fc x name) = ns
+addMetas res ns (Meta fc n i xs)
+  = addMetaArgs (insert (ifThenElse res (Resolved i) n) False ns) xs
   where
     addMetaArgs : NameMap Bool -> List (Term vars) -> NameMap Bool
     addMetaArgs ns [] = ns
-    addMetaArgs ns (t :: ts) = addMetaArgs (addMetas ns t) ts
-addMetas ns (Bind fc x (Let _ c val ty) scope)
-    = addMetas (addMetas (addMetas ns val) ty) scope
-addMetas ns (Bind fc x b scope)
-    = addMetas (addMetas ns (binderType b)) scope
-addMetas ns (App fc fn arg)
-    = addMetas (addMetas ns fn) arg
-addMetas ns (As fc s as tm) = addMetas ns tm
-addMetas ns (TDelayed fc x y) = addMetas ns y
-addMetas ns (TDelay fc x t y)
-    = addMetas (addMetas ns t) y
-addMetas ns (TForce fc r x) = addMetas ns x
-addMetas ns (PrimVal fc c) = ns
-addMetas ns (Erased fc i) = ns
-addMetas ns (TType fc) = ns
+    addMetaArgs ns (t :: ts) = addMetaArgs (addMetas res ns t) ts
+addMetas res ns (Bind fc x (Let _ c val ty) scope)
+    = addMetas res (addMetas res (addMetas res ns val) ty) scope
+addMetas res ns (Bind fc x b scope)
+    = addMetas res (addMetas res ns (binderType b)) scope
+addMetas res ns (App fc fn arg)
+    = addMetas res (addMetas res ns fn) arg
+addMetas res ns (As fc s as tm) = addMetas res ns tm
+addMetas res ns (TDelayed fc x y) = addMetas res ns y
+addMetas res ns (TDelay fc x t y)
+    = addMetas res (addMetas res ns t) y
+addMetas res ns (TForce fc r x) = addMetas res ns x
+addMetas res ns (PrimVal fc c) = ns
+addMetas res ns (Erased fc i) = ns
+addMetas res ns (TType fc) = ns
 
 -- Get the metavariable names in a term
 export
 getMetas : Term vars -> NameMap Bool
-getMetas tm = addMetas empty tm
+getMetas tm = addMetas False empty tm
 
 export
 addRefs : (underAssert : Bool) -> (aTotal : Name) ->
@@ -1706,6 +1707,7 @@ export
 getRefs : (aTotal : Name) -> Term vars -> NameMap Bool
 getRefs at tm = addRefs False at empty tm
 
+
 export
 nameAt : {vars : _} -> {idx : Nat} -> (0 p : IsVar n idx vars) -> Name
 nameAt {vars = n :: ns} First     = n

src/Idris/REPL.idr

@@ -627,11 +627,11 @@ execExp : {auto c : Ref Ctxt Defs} ->
           {auto o : Ref ROpts REPLOpts} ->
           PTerm -> Core REPLResult
 execExp ctm
-    = do tm_erased <- prepareExp ctm
-         Just cg <- findCG
-              | Nothing =>
-                   do iputStrLn (reflow "No such code generator available")
-                      pure CompilationFailed
+    = do Just cg <- findCG
+           | Nothing =>
+              do iputStrLn (reflow "No such code generator available")
+                 pure CompilationFailed
+         tm_erased <- prepareExp ctm
          logTimeWhen !getEvalTiming "Execution" $
            execute cg tm_erased
          pure $ Executed ctm
@@ -662,11 +662,11 @@ compileExp : {auto c : Ref Ctxt Defs} ->
              {auto o : Ref ROpts REPLOpts} ->
              PTerm -> String -> Core REPLResult
 compileExp ctm outfile
-    = do tm_erased <- prepareExp ctm
-         Just cg <- findCG
+    = do Just cg <- findCG
               | Nothing =>
                    do iputStrLn (reflow "No such code generator available")
                       pure CompilationFailed
+         tm_erased <- prepareExp ctm
          ok <- compile cg tm_erased outfile
          maybe (pure CompilationFailed)
                (pure . Compiled)

src/Parser/Rule/Source.idr

@@ -175,10 +175,7 @@ pragma : String -> Rule ()
 pragma n =
   terminal ("Expected pragma " ++ n) $
     \case
-      Pragma s =>
-        if s == n
-          then Just ()
-          else Nothing
+      Pragma s => guard (s == n)
       _ => Nothing
 
 export

tests/Main.idr

@@ -157,7 +157,7 @@ idrisTestsEvaluator = MkTestPool "Evaluation" [] Nothing
        "evaluator001", "evaluator002", "evaluator003",
        -- Miscellaneous REPL
        "interpreter001", "interpreter002", "interpreter003", "interpreter004",
-       "interpreter005", "interpreter006", "interpreter007"]
+       "interpreter005", "interpreter006", "interpreter007", "interpreter008"]
 
 idrisTestsAllBackends : Requirement -> TestPool
 idrisTestsAllBackends cg = MkTestPool

tests/idris2/interpreter008/Issue2041.idr

@@ -0,0 +1,5 @@
+ex : {n : Nat} -> String
+ex {n} = "hello" ++ show n
+
+main : IO ()
+main = putStrLn ex

tests/idris2/interpreter008/expected

@@ -0,0 +1,17 @@
+1/1: Building Issue2041 (Issue2041.idr)
+Error: Unsolved holes:
+Main.{n:377} introduced at: 
+Issue2041:5:17--5:19
+ 1 | ex : {n : Nat} -> String
+ 2 | ex {n} = "hello" ++ show n
+ 3 | 
+ 4 | main : IO ()
+ 5 | main = putStrLn ex
+                     ^^
+
+Main> Encountered unimplemented hole Main.{n:377}
+Warning: compiling hole Main.{n:377}
+Main> Encountered unimplemented hole Main.{n:4}
+Warning: compiling hole Main.{n:4}
+Main> 
+Bye for now!

tests/idris2/interpreter008/input

@@ -0,0 +1,3 @@
+:exec main
+:exec putStrLn ex
+:q

tests/idris2/interpreter008/run

@@ -0,0 +1 @@
+$1 --no-color --console-width 0 --no-banner Issue2041.idr < input