aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/first-order
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/first-order')
-rw-r--r--contrib/first-order/formula.ml95
-rw-r--r--contrib/first-order/formula.mli4
-rw-r--r--contrib/first-order/g_ground.ml496
-rw-r--r--contrib/first-order/ground.ml (renamed from contrib/first-order/ground.ml4)84
-rw-r--r--contrib/first-order/ground.mli13
-rw-r--r--contrib/first-order/instances.ml26
-rw-r--r--contrib/first-order/rules.ml40
-rw-r--r--contrib/first-order/rules.mli4
-rw-r--r--contrib/first-order/sequent.ml3
9 files changed, 173 insertions, 192 deletions
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 3cf099773..bce1ef24e 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -63,25 +63,19 @@ let ind_hyps nevar ind largs=
fst (Sign.decompose_prod_assum t2) in
Array.init lp myhyps
-let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
-
-let id_not=lazy (destConst (constant "not"))
-let id_iff=lazy (destConst (constant "iff"))
-
let match_with_evaluable gl t=
let env=pf_env gl in
+ let hd=
match kind_of_term t with
- App (hd,b)->
- (match kind_of_term hd with
- Const cst->
- if (*Environ.evaluable_constant cst env*)
- cst=(Lazy.force id_not) ||
- cst=(Lazy.force id_iff) then
- Some(EvalConstRef cst,t)
- else None
- | _-> None)
+ App (head,_) -> head
+ | _ -> t in
+ match kind_of_term hd with
+ Const cst->
+ if Environ.evaluable_constant cst env
+ then Some (EvalConstRef cst,t)
+ else None
| _-> None
-
+
type kind_of_formula=
Arrow of constr*constr
| False of inductive*constr list
@@ -90,7 +84,6 @@ type kind_of_formula=
| Exists of inductive*constr list
| Forall of constr*constr
| Atom of constr
- | Evaluable of evaluable_global_reference*constr
let rec kind_of_formula gl term =
let cciterm=whd_betaiotazeta term in
@@ -116,8 +109,14 @@ let rec kind_of_formula gl term =
Some (i,l)-> Exists((destInd i),l)
|_->
match match_with_evaluable gl cciterm with
- Some (ec,t)->Evaluable (ec,t)
- | None ->Atom cciterm
+ Some (ec,t)->
+ let nt=Tacred.unfoldn [[1],ec]
+ (pf_env gl)
+ (Refiner.sig_sig gl) t in
+ kind_of_formula gl nt
+ | None ->Atom (nf_betadeltaiota
+ (pf_env gl)
+ (Refiner.sig_sig gl) cciterm)
type atoms = {positive:constr list;negative:constr list}
@@ -161,10 +160,6 @@ let build_atoms gl metagen polarity cciterm =
positive:= unsigned :: !positive
else
negative:= unsigned :: !negative
- | Evaluable(ec,t)->
- let nt=Tacred.unfoldn [[1],ec] (Lazy.force pfenv)
- (Refiner.sig_sig gl) t in
- build_rec env polarity nt
in
build_rec [] polarity cciterm;
(!trivial,
@@ -179,7 +174,6 @@ type right_pattern =
| Rfalse
| Rforall
| Rexists of metavariable*constr*bool
- | Revaluable of evaluable_global_reference
type left_arrow_pattern=
LLatom
@@ -189,7 +183,6 @@ type left_arrow_pattern=
| LLforall of constr
| LLexists of inductive*constr list
| LLarrow of constr*constr*constr
- | LLevaluable of evaluable_global_reference
type left_pattern=
Lfalse
@@ -197,7 +190,6 @@ type left_pattern=
| Lor of inductive
| Lforall of metavariable*constr*bool
| Lexists of inductive
- | Levaluable of evaluable_global_reference
| LA of constr*left_arrow_pattern
type t={id:global_reference;
@@ -224,8 +216,7 @@ let build_formula side nam typ gl metagen=
let (_,_,d)=list_last (ind_hyps 0 i l).(0) in
Rexists(m,d,trivial)
| Forall (_,a) -> Rforall
- | Arrow (a,b) -> Rarrow
- | Evaluable (egc,_)->Revaluable egc in
+ | Arrow (a,b) -> Rarrow in
Right pat
else
let pat=
@@ -237,44 +228,22 @@ let build_formula side nam typ gl metagen=
| Exists (ind,_) -> Lexists ind
| Forall (d,_) ->
Lforall(m,d,trivial)
- | Evaluable (egc,_) ->Levaluable egc
- | Arrow (a,b) ->LA (a,
- match kind_of_formula gl a with
- False(i,l)-> LLfalse(i,l)
- | Atom t-> LLatom
- | And(i,l)-> LLand(i,l)
- | Or(i,l)-> LLor(i,l)
- | Arrow(a,c)-> LLarrow(a,c,b)
- | Exists(i,l)->LLexists(i,l)
- | Forall(_,_)->LLforall a
- | Evaluable (egc,_)-> LLevaluable egc) in
+ | Arrow (a,b) ->
+ let nfa=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) a in
+ LA (nfa,
+ match kind_of_formula gl a with
+ False(i,l)-> LLfalse(i,l)
+ | Atom t-> LLatom
+ | And(i,l)-> LLand(i,l)
+ | Or(i,l)-> LLor(i,l)
+ | Arrow(a,c)-> LLarrow(a,c,b)
+ | Exists(i,l)->LLexists(i,l)
+ | Forall(_,_)->LLforall a) in
Left pat
in
Left {id=nam;
- constr=typ;
+ constr=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) typ;
pat=pattern;
atoms=atoms}
- with Is_atom a-> Right a
-(*
-let build_right_entry typ gl metagen=
- try
- let m=meta_succ(metagen false) in
- let trivial,atoms=
- if !qflag then
- build_atoms gl metagen true typ
- else no_atoms in
- let pattern=
- match kind_of_formula gl typ with
- False(_,_) -> raise (Is_atom typ)
- | Atom a -> raise (Is_atom a)
- | And(_,_) -> Rand
- | Or(_,_) -> Ror
- | Exists (i,l) ->
- let (_,_,d)=list_last (ind_hyps 0 i l).(0) in
- Rexists(m,d,trivial)
- | Forall (_,a) -> Rforall
- | Arrow (a,b) -> Rarrow
- | Evaluable (egc,_)->Revaluable egc in
- Complex(pattern,typ,atoms)
- with Is_atom a-> Atomic a
-*)
+ with Is_atom a-> Right a (* already in nf *)
+
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index 815657f54..cbf3dc152 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -39,7 +39,6 @@ type kind_of_formula =
| Exists of inductive*constr list
| Forall of constr*constr
| Atom of constr
- | Evaluable of Names.evaluable_global_reference * Term.constr
val kind_of_formula : Proof_type.goal Tacmach.sigma ->
constr -> kind_of_formula
@@ -58,7 +57,6 @@ type right_pattern =
| Rfalse
| Rforall
| Rexists of metavariable*constr*bool
- | Revaluable of Names.evaluable_global_reference
type left_arrow_pattern=
LLatom
@@ -68,7 +66,6 @@ type left_arrow_pattern=
| LLforall of constr
| LLexists of inductive*constr list
| LLarrow of constr*constr*constr
- | LLevaluable of Names.evaluable_global_reference
type left_pattern=
Lfalse
@@ -76,7 +73,6 @@ type left_pattern=
| Lor of inductive
| Lforall of metavariable*constr*bool
| Lexists of inductive
- | Levaluable of Names.evaluable_global_reference
| LA of constr*left_arrow_pattern
type t={id: global_reference;
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
new file mode 100644
index 000000000..059ca69a6
--- /dev/null
+++ b/contrib/first-order/g_ground.ml4
@@ -0,0 +1,96 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Formula
+open Sequent
+open Ground
+open Goptions
+open Tactics
+open Tacticals
+open Term
+open Names
+
+(* declaring search depth as a global option *)
+
+let ground_depth=ref 5
+
+let _=
+ let gdopt=
+ { optsync=false;
+ optname="ground_depth";
+ optkey=SecondaryTable("Ground","Depth");
+ optread=(fun ()->Some !ground_depth);
+ optwrite=
+ (function
+ None->ground_depth:=5
+ | Some i->ground_depth:=(max i 0))}
+ in
+ declare_int_option gdopt
+
+let default_solver=(Tacinterp.interp <:tactic<Auto with *>>)
+
+let fail_solver=tclFAIL 0 "GTauto failed"
+
+let gen_ground_tac flag taco l gl=
+ let backup= !qflag in
+ try
+ qflag:=flag;
+ let solver=
+ match taco with
+ Some tac->tac
+ | None-> default_solver in
+ let startseq=create_with_ref_list l !ground_depth in
+ let result=ground_tac solver startseq gl in
+ qflag:=backup;result
+ with e ->qflag:=backup;raise e
+
+(* special for compatibility with old Intuition *)
+
+let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
+
+let defined_connectives=lazy
+ [[],EvalConstRef (destConst (constant "not"));
+ [],EvalConstRef (destConst (constant "iff"))]
+
+let normalize_evaluables=
+ onAllClauses
+ (function
+ None->unfold_in_concl (Lazy.force defined_connectives)
+ | Some id->
+ unfold_in_hyp (Lazy.force defined_connectives)
+ (Tacexpr.InHypType id))
+
+TACTIC EXTEND Ground
+ | [ "Ground" tactic(t) "with" ne_reference_list(l) ] ->
+ [ gen_ground_tac true (Some (snd t)) l ]
+ | [ "Ground" tactic(t) ] ->
+ [ gen_ground_tac true (Some (snd t)) [] ]
+ | [ "Ground" "with" ne_reference_list(l) ] ->
+ [ gen_ground_tac true None l ]
+ | [ "Ground" ] ->
+ [ gen_ground_tac true None [] ]
+END
+
+TACTIC EXTEND GTauto
+ [ "GTauto" ] ->
+ [ gen_ground_tac false (Some fail_solver) [] ]
+END
+
+TACTIC EXTEND GIntuition
+ ["GIntuition" tactic(t)] ->
+ [ gen_ground_tac false
+ (Some(tclTHEN normalize_evaluables (snd t))) [] ]
+| [ "GIntuition" ] ->
+ [ gen_ground_tac false
+ (Some (tclTHEN normalize_evaluables default_solver)) [] ]
+END
+
diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml
index 69f70d590..cc63b4afc 100644
--- a/contrib/first-order/ground.ml4
+++ b/contrib/first-order/ground.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
(* $Id$ *)
open Formula
@@ -18,40 +16,18 @@ open Term
open Tacmach
open Tactics
open Tacticals
-open Libnames
-open Util
-open Goptions
-
-(* declaring search depth as a global option *)
-
-let ground_depth=ref 5
-
-let set_qflag b= qflag:=b
-
-let _=
- let gdopt=
- { optsync=false;
- optname="ground_depth";
- optkey=SecondaryTable("Ground","Depth");
- optread=(fun ()->Some !ground_depth);
- optwrite=
- (function
- None->ground_depth:=5
- | Some i->ground_depth:=(max i 0))}
- in
- declare_int_option gdopt
let ground_tac solver startseq gl=
- let rec toptac ctx seq gl=
+ let rec toptac skipped seq gl=
if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
then Pp.msgnl (Proof_trees.pr_goal (sig_it gl));
tclORELSE (axiom_tac seq.gl seq)
begin
try
let (hd,seq1)=take_formula seq
- and re_add s=re_add_formula_list ctx s in
+ and re_add s=re_add_formula_list skipped s in
let continue=toptac []
- and backtrack=toptac (hd::ctx) seq1 in
+ and backtrack=toptac (hd::skipped) seq1 in
match hd.pat with
Right rpat->
begin
@@ -62,8 +38,6 @@ let ground_tac solver startseq gl=
forall_tac continue (re_add seq1)
| Rarrow->
arrow_tac continue (re_add seq1)
- | Revaluable egr->
- evaluable_tac egr continue (re_add seq1)
| Ror->
tclORELSE
(or_tac continue (re_add seq1))
@@ -71,7 +45,7 @@ let ground_tac solver startseq gl=
| Rfalse->backtrack
| Rexists(i,dom,triv)->
let (lfp,seq2)=collect_quantified seq in
- let backtrack2=toptac (lfp@ctx) seq2 in
+ let backtrack2=toptac (lfp@skipped) seq2 in
tclORELSE
(if seq.depth<=0 || not !qflag then
tclFAIL 0 "max depth"
@@ -90,7 +64,7 @@ let ground_tac solver startseq gl=
left_or_tac ind hd.id continue (re_add seq1)
| Lforall (_,_,_)->
let (lfp,seq2)=collect_quantified seq in
- let backtrack2=toptac (lfp@ctx) seq2 in
+ let backtrack2=toptac (lfp@skipped) seq2 in
tclORELSE
(if seq.depth<=0 || not !qflag then
tclFAIL 0 "max depth"
@@ -101,8 +75,6 @@ let ground_tac solver startseq gl=
if !qflag then
left_exists_tac ind hd.id continue (re_add seq1)
else backtrack
- | Levaluable egr->
- left_evaluable_tac egr hd.id continue (re_add seq1)
| LA (typ,lap)->
tclORELSE
(ll_atom_tac typ hd.id continue (re_add seq1))
@@ -132,54 +104,8 @@ let ground_tac solver startseq gl=
(ll_arrow_tac a b c hd.id continue
(re_add seq1))
backtrack
- | LLevaluable egr->
- left_evaluable_tac egr hd.id continue
- (re_add seq1)
end
end
with Heap.EmptyHeap->solver
end gl in
wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl
-
-let default_solver=(Tacinterp.interp <:tactic<Auto with *>>)
-
-let fail_solver=tclFAIL 0 "GroundTauto failed"
-
-let gen_ground_tac flag taco l gl=
- let backup= !qflag in
- try
- set_qflag flag;
- let solver=
- match taco with
- Some tac->tac
- | None-> default_solver in
- let startseq=create_with_ref_list l !ground_depth in
- let result=ground_tac solver startseq gl in
- set_qflag backup;result
- with e -> set_qflag backup;raise e
-
-TACTIC EXTEND Ground
- | [ "Ground" tactic(t) "with" ne_reference_list(l) ] ->
- [ gen_ground_tac true (Some (snd t)) l ]
- | [ "Ground" tactic(t) ] ->
- [ gen_ground_tac true (Some (snd t)) [] ]
- | [ "Ground" "with" ne_reference_list(l) ] ->
- [ gen_ground_tac true None l ]
- | [ "Ground" ] ->
- [ gen_ground_tac true None [] ]
-END
-
-TACTIC EXTEND GTauto
- [ "GTauto" ] ->
- [ gen_ground_tac false (Some fail_solver) [] ]
-END
-
-TACTIC EXTEND GIntuition
- ["GIntuition" tactic(t)] ->
- [ gen_ground_tac false
- (Some(tclTHEN normalize_evaluables (snd t))) [] ]
-| [ "GIntuition" ] ->
- [ gen_ground_tac false
- (Some (tclTHEN normalize_evaluables default_solver)) [] ]
-END
-
diff --git a/contrib/first-order/ground.mli b/contrib/first-order/ground.mli
new file mode 100644
index 000000000..fff45816a
--- /dev/null
+++ b/contrib/first-order/ground.mli
@@ -0,0 +1,13 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+val ground_tac: Tacmach.tactic ->
+ (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
+
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index 41a4078cc..e75ee8fb8 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -115,41 +115,47 @@ let left_instance_tac (inst,id) tacrec seq=
else
tclTHENS (cut dom)
[tclTHENLIST
- [intro;
+ [introf;
(fun gls->generalize
[mkApp(constr_of_reference id,
[|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
- intro;
+ introf;
tclSOLVE [wrap 1 false tacrec
(deepen (record (id,None) seq))]];
tclTRY assumption]
- | Real((m,t) as c,_)->
- if lookup (id,Some c) seq || m>0 then
+ | Real((0,t) as c,_)->
+ if lookup (id,Some c) seq then
tclFAIL 0 "already done"
else
tclTHENLIST
[generalize [mkApp(constr_of_reference id,[|t|])];
- intro;
+ introf;
tclSOLVE
[wrap 1 false tacrec
(deepen (record (id,Some c) seq))]]
+ | Real((m,t) as c,_)->
+ if lookup (id,Some c) seq then
+ tclFAIL 0 "already done"
+ else
+ tclFAIL 0 "not implemented ... yet"
+
let right_instance_tac inst tacrec seq=
match inst with
Phantom dom ->
tclTHENS (cut dom)
[tclTHENLIST
- [intro;
+ [introf;
(fun gls->
split (Rawterm.ImplicitBindings
[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
tclSOLVE [wrap 0 false tacrec (deepen seq)]];
tclTRY assumption]
+ | Real ((0,t),_) ->
+ (tclTHEN (split (Rawterm.ImplicitBindings [t]))
+ (tclSOLVE [wrap 0 true tacrec (deepen seq)]))
| Real ((m,t),_) ->
- if m>0 then tclFAIL 0 "not implemented ... yes"
- else
- tclTHEN (split (Rawterm.ImplicitBindings [t]))
- (tclSOLVE [wrap 0 true tacrec (deepen seq)])
+ tclFAIL 0 "not implemented ... yet"
let instance_tac inst=
if (snd inst)==dummy_id then
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index e7b71f54f..3ee0871de 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -15,7 +15,6 @@ open Tacmach
open Tactics
open Tacticals
open Termops
-open Reductionops
open Declarations
open Formula
open Sequent
@@ -65,27 +64,10 @@ let ll_atom_tac a id tacrec seq=
[generalize [mkApp(constr_of_reference id,
[|constr_of_reference (find_left a seq)|])];
clear_global id;
- intro;
+ introf;
wrap 1 false tacrec seq]
with Not_found->tclFAIL 0 "No link"
-(* evaluation rules *)
-
-let evaluable_tac ec tacrec seq gl=
- tclTHEN
- (unfold_in_concl [[1],ec])
- (wrap 0 true tacrec seq) gl
-
-let left_evaluable_tac ec id tacrec seq gl=
- tclTHENLIST
- [generalize [constr_of_reference id];
- clear_global id;
- intro;
- (fun gls->
- let nid=(Tacmach.pf_nth_hyp_id gls 1) in
- unfold_in_hyp [[1],ec] (Tacexpr.InHypType nid) gls);
- wrap 1 false tacrec seq] gl
-
(* right connectives rules *)
let and_tac tacrec seq=
@@ -95,7 +77,7 @@ let or_tac tacrec seq=
any_constructor (Some (tclSOLVE [wrap 0 true tacrec seq]))
let arrow_tac tacrec seq=
- tclTHEN intro (wrap 1 true tacrec seq)
+ tclTHEN introf (wrap 1 true tacrec seq)
(* left connectives rules *)
@@ -104,7 +86,7 @@ let left_and_tac ind id tacrec seq=
tclTHENLIST
[simplest_elim (constr_of_reference id);
clear_global id;
- tclDO n intro;
+ tclDO n introf;
wrap n false tacrec seq]
let left_or_tac ind id tacrec seq=
@@ -112,7 +94,7 @@ let left_or_tac ind id tacrec seq=
let f n=
tclTHENLIST
[clear_global id;
- tclDO n intro;
+ tclDO n introf;
wrap n false tacrec seq] in
tclTHENSV
(simplest_elim (constr_of_reference id))
@@ -143,7 +125,7 @@ let ll_ind_tac ind largs id tacrec seq gl=
tclTHENLIST
[generalize newhyps;
clear_global id;
- tclDO lp intro;
+ tclDO lp introf;
wrap lp false tacrec seq]
with Invalid_argument _ ->tclFAIL 0 "") gl
@@ -154,40 +136,40 @@ let ll_arrow_tac a b c id tacrec seq=
[|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
tclTHENS (cut c)
[tclTHENLIST
- [intro;
+ [introf;
clear_global id;
wrap 1 false tacrec seq];
tclTHENS (cut cc)
[exact_no_check (constr_of_reference id);
tclTHENLIST
[generalize [d];
- intro;
+ introf;
clear_global id;
tclSOLVE [wrap 1 true tacrec seq]]]]
(* quantifier rules (easy side) *)
let forall_tac tacrec seq=
- tclTHEN intro (wrap 0 true tacrec seq)
+ tclTHEN introf (wrap 0 true tacrec seq)
let left_exists_tac ind id tacrec seq=
let n=(construct_nhyps ind).(0) in
tclTHENLIST
[simplest_elim (constr_of_reference id);
clear_global id;
- tclDO n intro;
+ tclDO n introf;
(wrap (n-1) false tacrec seq)]
let ll_forall_tac prod id tacrec seq=
tclTHENS (cut prod)
[tclTHENLIST
- [intro;
+ [introf;
(fun gls->
let id0=pf_nth_hyp_id gls 1 in
let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in
tclTHEN (generalize [term]) (clear [id0]) gls);
clear_global id;
- intro;
+ introf;
tclSOLVE [wrap 1 false tacrec (deepen seq)]];
tclSOLVE [wrap 0 true tacrec (deepen seq)]]
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index 10ffe863d..afccfcd1b 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -27,10 +27,6 @@ val axiom_tac : constr -> Sequent.t -> tactic
val ll_atom_tac : constr -> lseqtac
-val evaluable_tac : evaluable_global_reference -> seqtac
-
-val left_evaluable_tac : evaluable_global_reference -> lseqtac
-
val and_tac : seqtac
val or_tac : seqtac
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 4942503c6..4c18090b9 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -31,7 +31,6 @@ let priority = (* pure heuristics, <=0 for non reversible *)
| Ror -> -15
| Rfalse -> -50 (* dead end for sure *)
| Rforall -> 100
- | Revaluable _ -> 100
| Rexists (_,_,_) -> -30
end
| Left lf ->
@@ -41,7 +40,6 @@ let priority = (* pure heuristics, <=0 for non reversible *)
| Lor _ -> 40
| Lforall (_,_,_) -> -30 (* must stay at lowest priority *)
| Lexists _ -> 60
- | Levaluable _ -> 100
| LA(_,lap) ->
match lap with
LLatom -> 0
@@ -51,7 +49,6 @@ let priority = (* pure heuristics, <=0 for non reversible *)
| LLforall _ -> -20
| LLexists (_,_) -> 50
| LLarrow (_,_,_) -> -10
- | LLevaluable _ -> 100
let left_reversible lpat=(priority lpat)>0
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-06 11:35:17 +0000