From eaff52a6e1400f47fbae731a43ca7333654762a7 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sat, 11 May 2019 22:21:03 +0100 Subject: [PATCH] Use updated NF for delayed elaborators Since the NF might refer to hole names, and those hole names might be possible to evaluate now, we'll need to recalculate the expected type's normal form before rerunning the delayed elaborator --- src/Core/Normalise.idr | 14 ++++++++++++++ src/TTImp/Elab/Ambiguity.idr | 23 +++++++++++++++-------- src/TTImp/Elab/App.idr | 3 ++- src/TTImp/Elab/Delayed.idr | 5 +++-- tests/ttimp/basic005/Ambig.yaff | 13 +++++++++++++ tests/ttimp/basic005/expected | 1 + tests/ttimp/basic005/input | 1 + 7 files changed, 49 insertions(+), 11 deletions(-) diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr index a636efa..ecb506d 100644 --- a/src/Core/Normalise.idr +++ b/src/Core/Normalise.idr @@ -678,4 +678,18 @@ logGlue lvl msg env gtm ++ ": " ++ show tm' else pure () +export +logGlueNF : {auto c : Ref Ctxt Defs} -> + Nat -> Lazy String -> Env Term vars -> Glued vars -> Core () +logGlueNF lvl msg env gtm + = do opts <- getOpts + if logLevel opts >= lvl + then do defs <- get Ctxt + tm <- getTerm gtm + tmnf <- normaliseHoles defs env tm + tm' <- toFullNames tmnf + coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg + ++ ": " ++ show tm' + else pure () + diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index 8dd01b7..7ed1f21 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/src/TTImp/Elab/Ambiguity.idr @@ -137,23 +137,30 @@ checkAlternative rig elabinfo env fc uniq alts mexpected InLHS c => InLHS _ => InTerm solveConstraints solvemode Normal - defs <- get Ctxt delayOnFailure fc rig env expected ambiguous $ (\delayed => do defs <- get Ctxt - -- If we don't know the target type, try again later + exp <- getTerm expected + -- If we don't know the target type on the first attempt, + -- delay when (not delayed && - !(holeIn (gamma defs) !(getTerm expected))) $ + !(holeIn (gamma defs) exp)) $ throw (AllFailed []) - let alts' = alts -- pruneByType defs expected alts TODO - logGlue 5 ("Ambiguous elaboration " ++ show alts' ++ - "\nTarget type ") env expected + -- We can't just used the old NF on the second attempt, + -- because we might know more now, so recalculate it + let exp' = if delayed + then gnf env exp + else expected + + let alts' = alts -- pruneByType defs !(getNF exp') alts TODO + logGlueNF 5 ("Ambiguous elaboration " ++ show alts' ++ + "\nTarget type ") env exp' let tryall = case uniq of FirstSuccess => anyOne fc _ => exactlyOne fc env tryall (map (\t => (getName t, - do res <- checkImp rig elabinfo env t (Just expected) + do res <- checkImp rig elabinfo env t (Just exp') -- Do it twice for interface resolution; -- first pass gets the determining argument -- (maybe rethink this, there should be a better @@ -168,7 +175,7 @@ checkAlternative rig elabinfo env fc uniq alts mexpected = case getFn tm of Meta _ _ idx _ => do Just (Hole _) <- lookupDefExact (Resolved idx) gam - | Nothing => pure False + | _ => pure False pure True _ => pure False diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index ff2f53d..6b89abe 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -304,7 +304,8 @@ checkApp rig elabinfo env fc (IVar fc' n) expargs impargs exp fnty <- quote defs env nty exptyt <- maybe (pure Nothing) (\t => do ety <- getTerm t - pure (Just !(toFullNames ety))) + etynf <- normaliseHoles defs env ety + pure (Just !(toFullNames etynf))) exp pure ("Checking application of " ++ show n ++ " to " ++ show expargs ++ "\n\tFunction type " ++ diff --git a/src/TTImp/Elab/Delayed.idr b/src/TTImp/Elab/Delayed.idr index c153acb..a15d64d 100644 --- a/src/TTImp/Elab/Delayed.idr +++ b/src/TTImp/Elab/Delayed.idr @@ -57,8 +57,9 @@ delayOnFailure fc rig env expected pred elab then do nm <- genName "delayed" (ci, dtm) <- newDelayed fc rig env nm !(getTerm expected) - logGlue 5 ("Postponing elaborator " ++ show nm ++ - " for") env expected + logGlueNF 5 ("Postponing elaborator " ++ show nm ++ + " for") env expected + log 10 ("Due to error " ++ show err) ust <- get UST put UST (record { delayedElab $= insert ci (mkClosedElab fc env (elab True)) } diff --git a/tests/ttimp/basic005/Ambig.yaff b/tests/ttimp/basic005/Ambig.yaff index 2d4a9da..3f707fb 100644 --- a/tests/ttimp/basic005/Ambig.yaff +++ b/tests/ttimp/basic005/Ambig.yaff @@ -29,4 +29,17 @@ testList = Cons 1 (Cons 2 (Cons 3 Nil)) testVect : Vect ? Integer testVect = Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))) +data IsType : $a -> Type -> Type where + ItIs : {x : $a} -> IsType x $a + +foo : IsType 5 Integer +foo = ItIs + +revapply : $arg -> ($arg -> $b) -> $b +revapply $x $f = f x + +-- Testing delayed elaborationg; we can't check the list until we know +-- whether it's List or Vect, which we work out from the second argument +test : Integer -> Nat +test $x = revapply (Cons x (Cons x Nil)) Vect.length diff --git a/tests/ttimp/basic005/expected b/tests/ttimp/basic005/expected index cd5a663..e0cd23d 100644 --- a/tests/ttimp/basic005/expected +++ b/tests/ttimp/basic005/expected @@ -2,4 +2,5 @@ Processing as TTImp Written TTC Yaffle> (Main.S (Main.S (Main.S Main.Z))) Yaffle> (Main.S (Main.S (Main.S (Main.S Main.Z)))) +Yaffle> (Main.S (Main.S Main.Z)) Yaffle> Bye for now! diff --git a/tests/ttimp/basic005/input b/tests/ttimp/basic005/input index 618d2ed..df72873 100644 --- a/tests/ttimp/basic005/input +++ b/tests/ttimp/basic005/input @@ -1,3 +1,4 @@ length testList length testVect +test 94 :q