git.iko.soy/Idris-dev
on master help sign in
Repaired effects library, less attacks in applyTactic
6440a7bJan Bessai
config.mk+1−1
compare with master
unifiedsplit
@@ -5,5 +5,5 @@ CABAL :=cabal
5## Enable Java RTS:
5## Enable Java RTS:
6#CABALFLAGS :=-f Java
6#CABALFLAGS :=-f Java
7## Disable building of Effects
7## Disable building of Effects
8−CABALFLAGS :=-f NoEffects
8+#CABALFLAGS :=-f NoEffects
9
9
effects/Effects.idr+10−10
@@ -59,19 +59,19 @@ rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
59---- The Effect EDSL itself ----
59---- The Effect EDSL itself ----
60
60
61-- some proof automation
61-- some proof automation
62−findEffElem : Nat -> Tactic -- Nat is maximum search depth
62+findEffElem : Nat -> List (TTName, Binder TT) -> Tactic -- Nat is maximum search depth
63−findEffElem O = Refine "Here" `Seq` Solve
63+findEffElem O ctxt = Refine "Here" `Seq` Solve
64−findEffElem (S n) = GoalType "EffElem"
64+findEffElem (S n) ctxt = GoalType "EffElem"
65 (Try (Refine "Here" `Seq` Solve)
65 (Try (Refine "Here" `Seq` Solve)
66− (Refine "There" `Seq` (Solve `Seq` findEffElem n)))
66+ (Refine "There" `Seq` (Solve `Seq` findEffElem n ctxt)))
67
67
68−findSubList : Nat -> Tactic
68+findSubList : Nat -> List (TTName, Binder TT) -> Tactic
69−findSubList O = Refine "SubNil" `Seq` Solve
69+findSubList O ctxt = Refine "SubNil" `Seq` Solve
70−findSubList (S n)
70+findSubList (S n) ctxt
71 = GoalType "SubList"
71 = GoalType "SubList"
72 (Try (Refine "subListId" `Seq` Solve)
72 (Try (Refine "subListId" `Seq` Solve)
73 ((Try (Refine "Keep" `Seq` Solve)
73 ((Try (Refine "Keep" `Seq` Solve)
74− (Refine "Drop" `Seq` Solve)) `Seq` findSubList n))
74+ (Refine "Drop" `Seq` Solve)) `Seq` findSubList n ctxt))
75
75
76updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->
76updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->
77 List EFFECT
77 List EFFECT
@@ -116,14 +116,14 @@ data EffM : (m : Type -> Type) ->
116-- Eff : List (EFFECT m) -> Type -> Type
116-- Eff : List (EFFECT m) -> Type -> Type
117
117
118implicit
118implicit
119−lift' : {default tactics { reflect findSubList 100; solve; }
119+lift' : {default tactics { applyTactic findSubList 100; solve; }
120 prf : SubList ys xs} ->
120 prf : SubList ys xs} ->
121 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
121 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
122lift' {prf} e = lift prf e
122lift' {prf} e = lift prf e
123
123
124implicit
124implicit
125effect' : {a, b: _} -> {e : Effect} ->
125effect' : {a, b: _} -> {e : Effect} ->
126− {default tactics { reflect findEffElem 100; solve; }
126+ {default tactics { applyTactic findEffElem 100; solve; }
127 prf : EffElem e a xs} ->
127 prf : EffElem e a xs} ->
128 (eff : e a b t) ->
128 (eff : e a b t) ->
129 EffM m xs (updateResTy xs prf eff) t
129 EffM m xs (updateResTy xs prf eff) t
src/Idris/ElabTerm.hs+2−2
@@ -788,7 +788,7 @@ runTac autoSolve ist tac = do env <- get_env
788 ctxt <- get_context
788 ctxt <- get_context
789 env <- get_env
789 env <- get_env
790 let tm'' = normalise ctxt env tm'
790 let tm'' = normalise ctxt env tm'
791− attack -- let x : List (TTName, Binder TT) = reflectEnv in ...
791+ -- let x : List (TTName, Binder TT) = reflectEnv in ...
792 envval <- unique_hole (MN 0 "letval")
792 envval <- unique_hole (MN 0 "letval")
793 claim envval (RApp listTy envTupleType)
793 claim envval (RApp listTy envTupleType)
794 letn <- unique_hole (MN 0 "letvar")
794 letn <- unique_hole (MN 0 "letvar")
@@ -800,7 +800,7 @@ runTac autoSolve ist tac = do env <- get_env
800 ctxt <- get_context
800 ctxt <- get_context
801 env <- get_env
801 env <- get_env
802 let env'' = normalise ctxt env env'
802 let env'' = normalise ctxt env env'
803− attack -- let z : Tactic = f x
803+ -- let z : Tactic = f x
804 restac <- unique_hole (MN 0 "letval")
804 restac <- unique_hole (MN 0 "letval")
805 claim restac tacticTy
805 claim restac tacticTy
806 letn <- unique_hole (MN 0 "letvar")
806 letn <- unique_hole (MN 0 "letvar")