From 4abe760cc90cdfd389fc59ee10f160ebfc5773cf Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 3 Jul 2019 11:02:53 +0100 Subject: [PATCH] Update type on delayed rewrite Like in delayed ambiguity resolution, we need to reevaluate the target type because it might have changed - and that's why we delayed in the first place! --- libs/base/Data/Strings.idr | 3 +++ libs/base/Data/Vect.idr | 16 ++++++++-------- src/TTImp/Elab/Ambiguity.idr | 23 ++++++++++++++++++++--- src/TTImp/Elab/App.idr | 1 + src/TTImp/Elab/Check.idr | 1 + src/TTImp/Elab/Rewrite.idr | 20 ++++++++++++++------ 6 files changed, 47 insertions(+), 17 deletions(-) diff --git a/libs/base/Data/Strings.idr b/libs/base/Data/Strings.idr index 3189e64..42abcda 100644 --- a/libs/base/Data/Strings.idr +++ b/libs/base/Data/Strings.idr @@ -72,3 +72,6 @@ public export break : (Char -> Bool) -> String -> (String, String) break p = span (not . p) +export +stringToNatOrZ : String -> Nat +stringToNatOrZ = fromInteger . prim__cast_StringInteger diff --git a/libs/base/Data/Vect.idr b/libs/base/Data/Vect.idr index 540f3f9..9c447a1 100644 --- a/libs/base/Data/Vect.idr +++ b/libs/base/Data/Vect.idr @@ -807,13 +807,13 @@ exactLength {m} len xs with (decEq m len) ||| at least that length in its type, otherwise return Nothing ||| @len the required length ||| @xs the vector with the desired length --- overLength : {m : Nat} -> -- expected at run-time --- (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a) --- overLength {m} n xs with (cmp m n) --- overLength {m = m} (plus m (S y)) xs | (CmpLT y) = Nothing --- overLength {m = m} m xs | CmpEQ --- = Just (0 ** xs) --- overLength {m = plus n (S x)} n xs | (CmpGT x) --- = Just (S x ** rewrite plusCommutative (S x) n in xs) +overLength : {m : Nat} -> -- expected at run-time + (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a) +overLength {m} n xs with (cmp m n) + overLength {m = m} (plus m (S y)) xs | (CmpLT y) = Nothing + overLength {m = m} m xs | CmpEQ + = Just (0 ** xs) + overLength {m = plus n (S x)} n xs | (CmpGT x) + = Just (S x ** rewrite plusCommutative (S x) n in xs) diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index 491c149..2f4e8f8 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/src/TTImp/Elab/Ambiguity.idr @@ -177,6 +177,11 @@ couldBe {vars} defs ty@(NPrimVal _ _) app Concrete => pure $ Just (True, app) Poly => pure $ Just (False, app) NoMatch => pure Nothing +couldBe {vars} defs ty@(NType _) app + = case !(couldBeFn {vars} defs ty (getFn app)) of + Concrete => pure $ Just (True, app) + Poly => pure $ Just (False, app) + NoMatch => pure Nothing couldBe defs ty app = pure $ Just (False, app) @@ -257,18 +262,30 @@ checkAlternative rig elabinfo nest env fc (UniqueDefault def) alts mexpected do solveConstraints solvemode Normal defs <- get Ctxt alts' <- pruneByType !(getNF expected) alts + + -- We can't just use the old NF on the second attempt, + -- because we might know more now, so recalculate it + exp <- getTerm expected + let exp' = if delayed + then gnf env exp + else expected + + logGlueNF 5 ("Ambiguous elaboration " ++ show alts' ++ + " at " ++ show fc ++ + "\nWith default. Target type ") env exp' if delayed -- use the default if there's still ambiguity then try (exactlyOne fc env (map (\t => (getName t, checkImp rig elabinfo nest env t - (Just expected))) alts')) - (checkImp rig elabinfo nest env def (Just expected)) + (Just exp'))) alts')) + (do log 5 "All failed, running default" + checkImp rig elabinfo nest env def (Just exp')) else exactlyOne fc env (map (\t => (getName t, - checkImp rig elabinfo nest env t (Just expected))) + checkImp rig elabinfo nest env t (Just exp'))) alts')) checkAlternative rig elabinfo nest env fc uniq alts mexpected = do expected <- maybe (do nm <- genName "altTy" diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index aa63c83..dba7b82 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -214,6 +214,7 @@ mutual needsDelayExpr True (IUpdate _ _ _) = pure True needsDelayExpr True (IAlternative _ _ _) = pure True needsDelayExpr True (ISearch _ _) = pure True + needsDelayExpr True (IRewrite _ _ _) = pure True needsDelayExpr True _ = pure False -- On the LHS, for any concrete thing, we need to make sure we know diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr index c998fa8..734d070 100644 --- a/src/TTImp/Elab/Check.idr +++ b/src/TTImp/Elab/Check.idr @@ -406,6 +406,7 @@ successful ((tm, elab) :: elabs) md <- get MD defs <- branch catch (do -- Run the elaborator + log 5 $ "Running " ++ show tm res <- elab -- Record post-elaborator state ust' <- get UST diff --git a/src/TTImp/Elab/Rewrite.idr b/src/TTImp/Elab/Rewrite.idr index b49b28d..ea2877c 100644 --- a/src/TTImp/Elab/Rewrite.idr +++ b/src/TTImp/Elab/Rewrite.idr @@ -58,7 +58,7 @@ elabRewrite : {vars : _} -> {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> FC -> Env Term vars -> - (expected : Glued vars) -> + (expected : Term vars) -> (rulety : Term vars) -> Core (Name, Term vars, Term vars) elabRewrite loc env expected rulety @@ -68,20 +68,27 @@ elabRewrite loc env expected rulety (lt, rt, lty) <- getRewriteTerms loc defs tynf (NotRewriteRule loc env rulety) lemn <- findRewriteLemma loc rulety - rwexp_sc <- replace defs env lt (Ref loc Bound parg) - !(getNF expected) + -- Need to normalise again, since we might have been delayed and + -- the metavariables might have been updated + expnf <- nf defs env expected + + logNF 5 "Rewriting" env lt + logNF 5 "Rewriting in" env expnf + rwexp_sc <- replace defs env lt (Ref loc Bound parg) expnf + logTerm 5 "Rewritten to" rwexp_sc + empty <- clearDefs defs let pred = Bind loc parg (Lam RigW Explicit !(quote empty env lty)) (refsToLocals (Add parg parg None) rwexp_sc) gpredty <- getType env pred predty <- getTerm gpredty - exptm <- getTerm expected + exptm <- quote defs env expected -- if the rewritten expected type converts with the original, -- then the rewrite did nothing, which is an error when !(convert defs env rwexp_sc exptm) $ - throw (RewriteNoChange loc env rulety exptm) + throw (RewriteNoChange loc env rulety exptm) pure (lemn, pred, predty) export @@ -101,7 +108,8 @@ checkRewrite {vars} rigc elabinfo nest env fc rule tm (Just expected) do (rulev, grulet) <- check Rig0 elabinfo nest env rule Nothing rulet <- getTerm grulet expTy <- getTerm expected - (lemma, pred, predty) <- elabRewrite fc env expected rulet + when delayed $ log 5 "Retrying rewrite" + (lemma, pred, predty) <- elabRewrite fc env expTy rulet rname <- genVarName "_" pname <- genVarName "_"