From 6887a5f95f09d56c37149dd1967f6a0ecd463896 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 3 Mar 2021 13:49:32 +0000 Subject: [PATCH] Record local hints in delayed elaborators We might not have set up search problems yet when delaying an elaborator, so we need to know what the local hints were at the point of delay. --- src/Core/UnifyState.idr | 3 +- src/TTImp/Elab/Delayed.idr | 21 +++-- tests/Main.idr | 2 +- tests/idris2/interface024/EH.idr | 138 +++++++++++++++++++++++++++++ tests/idris2/interface024/expected | 1 + tests/idris2/interface024/run | 3 + 6 files changed, 159 insertions(+), 9 deletions(-) create mode 100644 tests/idris2/interface024/EH.idr create mode 100644 tests/idris2/interface024/expected create mode 100644 tests/idris2/interface024/run diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr index 1303643f2..dbee31dd9 100644 --- a/src/Core/UnifyState.idr +++ b/src/Core/UnifyState.idr @@ -84,12 +84,13 @@ record UState where dotConstraints : List (Name, DotReason, Constraint) -- dot pattern constraints nextName : Int nextConstraint : Int - delayedElab : List (Nat, Int, Core ClosedTerm) + delayedElab : List (Nat, Int, NameMap (), Core ClosedTerm) -- Elaborators which we need to try again later, because -- we didn't have enough type information to elaborate -- successfully yet. -- 'Nat' is the priority (lowest first) -- The 'Int' is the resolved name. + -- NameMap () is the set of local hints at the point of delay logging : Bool export diff --git a/src/TTImp/Elab/Delayed.idr b/src/TTImp/Elab/Delayed.idr index 2bf8f65db..261ca2038 100644 --- a/src/TTImp/Elab/Delayed.idr +++ b/src/TTImp/Elab/Delayed.idr @@ -15,6 +15,7 @@ import TTImp.Elab.Check import TTImp.TTImp import Libraries.Data.IntMap +import Libraries.Data.NameMap import Data.List %default covering @@ -81,8 +82,10 @@ delayOnFailure fc rig env expected pred pri elab " for") env expected log "elab.delay" 10 ("Due to error " ++ show err) ust <- get UST + defs <- get Ctxt put UST (record { delayedElab $= - ((pri, ci, mkClosedElab fc env (deeper (elab True))) :: ) } + ((pri, ci, localHints defs, + mkClosedElab fc env (deeper (elab True))) :: ) } ust) pure (dtm, expected) else throw err) @@ -106,8 +109,9 @@ delayElab {vars} fc rig env exp pri elab logGlueNF "elab.delay" 5 ("Postponing elaborator " ++ show nm ++ " for") env expected ust <- get UST + defs <- get Ctxt put UST (record { delayedElab $= - ((pri, ci, mkClosedElab fc env elab) :: ) } + ((pri, ci, localHints defs, mkClosedElab fc env elab) :: ) } ust) pure (dtm, expected) where @@ -208,11 +212,11 @@ retryDelayed' : {vars : _} -> {auto u : Ref UST UState} -> {auto e : Ref EST (EState vars)} -> RetryError -> - List (Nat, Int, Core ClosedTerm) -> - List (Nat, Int, Core ClosedTerm) -> - Core (List (Nat, Int, Core ClosedTerm)) + List (Nat, Int, NameMap (), Core ClosedTerm) -> + List (Nat, Int, NameMap (), Core ClosedTerm) -> + Core (List (Nat, Int, NameMap (), Core ClosedTerm)) retryDelayed' errmode acc [] = pure (reverse acc) -retryDelayed' errmode acc (d@(_, i, elab) :: ds) +retryDelayed' errmode acc (d@(_, i, hints, elab) :: ds) = do defs <- get Ctxt Just Delayed <- lookupDefExact (Resolved i) (gamma defs) | _ => retryDelayed' errmode acc ds @@ -222,6 +226,9 @@ retryDelayed' errmode acc (d@(_, i, elab) :: ds) -- elab itself might have delays internally, so keep track of them ust <- get UST put UST (record { delayedElab = [] } ust) + defs <- get Ctxt + put Ctxt (record { localHints = hints } defs) + tm <- elab ust <- get UST let ds' = reverse (delayedElab ust) ++ ds @@ -247,7 +254,7 @@ retryDelayed : {vars : _} -> {auto m : Ref MD Metadata} -> {auto u : Ref UST UState} -> {auto e : Ref EST (EState vars)} -> - List (Nat, Int, Core ClosedTerm) -> + List (Nat, Int, NameMap (), Core ClosedTerm) -> Core () retryDelayed ds = do est <- get EST diff --git a/tests/Main.idr b/tests/Main.idr index c91d1d80f..951b08ea5 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -90,7 +90,7 @@ idrisTestsInterface = MkTestPool [] "interface009", "interface010", "interface011", "interface012", "interface013", "interface014", "interface015", "interface016", "interface017", "interface018", "interface019", "interface020", - "interface021", "interface022", "interface023"] + "interface021", "interface022", "interface023", "interface024"] idrisTestsLinear : TestPool idrisTestsLinear = MkTestPool [] diff --git a/tests/idris2/interface024/EH.idr b/tests/idris2/interface024/EH.idr new file mode 100644 index 000000000..5affe35db --- /dev/null +++ b/tests/idris2/interface024/EH.idr @@ -0,0 +1,138 @@ +import Syntax.PreorderReasoning + +-------- some notation ---------- +infixr 6 .+.,:+: +infixr 7 .*.,:*: + +interface Additive a where + constructor MkAdditive + (.+.) : a -> a -> a + O : a + +interface Additive2 a where + constructor MkAdditive2 + (:+:) : a -> a -> a + O2 : a + +interface Multiplicative a where + constructor MkMultiplicative + (.*.) : a -> a -> a + I : a + +record MonoidOver U where + constructor WithStruct + Unit : U + Mult : U -> U -> U + lftUnit : (x : U) -> Unit `Mult` x = x + rgtUnit : (x : U) -> x `Mult` Unit = x + assoc : (x,y,z : U) + -> x `Mult` (y `Mult` z) = (x `Mult` y) `Mult` z + +record Monoid where + constructor MkMonoid + U : Type + Struct : MonoidOver U + +AdditiveStruct : (m : MonoidOver a) -> Additive a +AdditiveStruct m = MkAdditive (Mult $ m) + (Unit $ m) +AdditiveStruct2 : (m : MonoidOver a) -> Additive2 a +AdditiveStruct2 m = MkAdditive2 (Mult $ m) + (Unit $ m) +AdditiveStructs : (ma : MonoidOver a) -> (mb : MonoidOver b) + -> (Additive a, Additive2 b) +AdditiveStructs ma mb = (AdditiveStruct ma, AdditiveStruct2 mb) + +getAdditive : (m : Monoid) -> Additive (U m) +getAdditive m = AdditiveStruct (Struct m) + +MultiplicativeStruct : (m : Monoid) -> Multiplicative (U m) +MultiplicativeStruct m = MkMultiplicative (Mult $ Struct m) + (Unit $ Struct m) +----------------------------------------------------- + +Commutative : MonoidOver a -> Type +Commutative m = (x,y : a) -> let _ = AdditiveStruct m in + x .+. y = y .+. x + +Commute : (Additive a, Additive2 a) => Type +Commute = + (x11,x12,x21,x22 : a) -> + ((x11 :+: x12) .+. (x21 :+: x22)) + = + ((x11 .+. x21) :+: (x12 .+. x22)) + +product : (ma, mb : Monoid) -> Monoid +product ma mb = + let + %hint aStruct : Additive (U ma) + aStruct = getAdditive ma + %hint bStruct : Additive (U mb) + bStruct = getAdditive mb + + in MkMonoid (U ma, U mb) $ WithStruct + (O, O) + (\(x1,y1), (x2, y2) => (x1 .+. x2, y1 .+. y2)) + (\(x,y) => rewrite lftUnit (Struct ma) x in + rewrite lftUnit (Struct mb) y in + Refl) + (\(x,y) => rewrite rgtUnit (Struct ma) x in + rewrite rgtUnit (Struct mb) y in + Refl) + (\(x1,y1),(x2,y2),(x3,y3) => + rewrite assoc (Struct ma) x1 x2 x3 in + rewrite assoc (Struct mb) y1 y2 y3 in + Refl) + +EckmannHilton : forall a . (ma,mb : MonoidOver a) + -> let ops = AdditiveStructs ma mb in + Commute @{ops} + -> (Commutative ma, (x,y : a) -> x .+. y = x :+: y) +EckmannHilton ma mb prf = + let %hint first : Additive a + first = AdditiveStruct ma + %hint second : Additive2 a + second = AdditiveStruct2 mb in + let SameUnits : (the a O === O2) + SameUnits = Calc $ + |~ O + ~~ O .+. O ...(sym $ lftUnit ma O) + ~~ (O :+: O2) .+. (O2 :+: O) ...(sym $ cong2 (.+.) + (rgtUnit mb O) + (lftUnit mb O)) + ~~ (O .+. O2) :+: (O2 .+. O) ...(prf O O2 O2 O) + ~~ O2 :+: O2 ...(cong2 (:+:) + (lftUnit ma O2) + (rgtUnit ma O2)) + ~~ O2 ...(lftUnit mb O2) + + SameMults : (x,y : a) -> (x .+. y) === (x :+: y) + SameMults x y = Calc $ + |~ x .+. y + ~~ (x :+: O2) .+. (O2 :+: y) ...(sym $ cong2 (.+.) + (rgtUnit mb x) + (lftUnit mb y)) + ~~ (x .+. O2) :+: (O2 .+. y) ...(prf x O2 O2 y) + ~~ (x .+. O ) :+: (O .+. y) ...(cong (\u => + (x .+. u) :+: (u .+. y)) + (sym SameUnits)) + ~~ x :+: y ...(cong2 (:+:) + (rgtUnit ma x) + (lftUnit ma y)) + + Commutativity : Commutative ma + Commutativity x y = Calc $ + |~ x .+. y + ~~ (O2 :+: x) .+. (y :+: O2) ...(sym $ cong2 (.+.) + (lftUnit mb x) + (rgtUnit mb y)) + ~~ (O2 .+. y) :+: (x .+. O2) ...(prf O2 x y O2) + ~~ (O .+. y) :+: (x .+. O ) ...(cong (\u => + (u .+. y) :+: (x .+. u)) + (sym SameUnits)) + ~~ y :+: x ...(cong2 (:+:) + (lftUnit ma y) + (rgtUnit ma x)) + ~~ y .+. x ...(sym $ SameMults y x) + in (Commutativity, SameMults) + diff --git a/tests/idris2/interface024/expected b/tests/idris2/interface024/expected new file mode 100644 index 000000000..86f94457a --- /dev/null +++ b/tests/idris2/interface024/expected @@ -0,0 +1 @@ +1/1: Building EH (EH.idr) diff --git a/tests/idris2/interface024/run b/tests/idris2/interface024/run new file mode 100644 index 000000000..df18ab570 --- /dev/null +++ b/tests/idris2/interface024/run @@ -0,0 +1,3 @@ +$1 --no-banner --no-color --check EH.idr -p contrib + +rm -rf build