summaryrefslogtreecommitdiff
path: root/plugins/rtauto/proof_search.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/rtauto/proof_search.ml')
-rw-r--r--plugins/rtauto/proof_search.ml127
1 files changed, 71 insertions, 56 deletions
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 2ace38bd..23510117 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Term
+open Errors
open Util
open Goptions
@@ -62,20 +62,35 @@ type form=
| Conjunct of form * form
| Disjunct of form * form
-type tag=int
-
-let decomp_form=function
- Atom i -> Some (i,[])
- | Arrow (f1,f2) -> Some (-1,[f1;f2])
- | Bot -> Some (-2,[])
- | Conjunct (f1,f2) -> Some (-3,[f1;f2])
- | Disjunct (f1,f2) -> Some (-4,[f1;f2])
-
-module Fmap=Map.Make(struct type t=form let compare=compare end)
+module FOrd = struct
+ type t = form
+ let rec compare x y =
+ match x, y with
+ | Bot, Bot -> 0
+ | Bot, _ -> -1
+ | Atom _, Bot -> 1
+ | Atom a1, Atom a2 -> Int.compare a1 a2
+ | Atom _, _ -> -1
+ | Arrow _, (Bot | Atom _) -> 1
+ | Arrow (f1, g1), Arrow (f2, g2) ->
+ let cmp = compare f1 f2 in
+ if cmp = 0 then compare g1 g2 else cmp
+ | Arrow _, _ -> -1
+ | Conjunct _, (Bot | Atom _ | Arrow _) -> 1
+ | Conjunct (f1, g1), Conjunct (f2, g2) ->
+ let cmp = compare f1 f2 in
+ if cmp = 0 then compare g1 g2 else cmp
+ | Conjunct _, _ -> -1
+ | Disjunct _, (Bot | Atom _ | Arrow _ | Conjunct _) -> 1
+ | Disjunct (f1, g1), Disjunct (f2, g2) ->
+ let cmp = compare f1 f2 in
+ if cmp = 0 then compare g1 g2 else cmp
+end
+module Fmap = Map.Make(FOrd)
type sequent =
- {rev_hyps: form Intmap.t;
- norev_hyps: form Intmap.t;
+ {rev_hyps: form Int.Map.t;
+ norev_hyps: form Int.Map.t;
size:int;
left:int Fmap.t;
right:(int*form) list Fmap.t;
@@ -131,21 +146,21 @@ let add_step s sub =
| SI_Or_r,[p] -> I_Or_r p
| SE_Or i,[p1;p2] -> E_Or(i,p1,p2)
| SD_Or i,[p] -> D_Or(i,p)
- | _,_ -> anomaly "add_step: wrong arity"
+ | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity")
type 'a with_deps =
{dep_it:'a;
dep_goal:bool;
- dep_hyps:Intset.t}
+ dep_hyps:Int.Set.t}
type slice=
{proofs_done:proof list;
proofs_todo:sequent with_deps list;
step:rule;
needs_goal:bool;
- needs_hyps:Intset.t;
+ needs_hyps:Int.Set.t;
changes_goal:bool;
- creates_hyps:Intset.t}
+ creates_hyps:Int.Set.t}
type state =
Complete of proof
@@ -153,7 +168,7 @@ type state =
let project = function
Complete prf -> prf
- | Incomplete (_,_) -> anomaly "not a successful state"
+ | Incomplete (_,_) -> anomaly (Pp.str "not a successful state")
let pop n prf =
let nprf=
@@ -168,27 +183,27 @@ let rec fill stack proof =
| slice::super ->
if
!pruning &&
- slice.proofs_done=[] &&
+ List.is_empty slice.proofs_done &&
not (slice.changes_goal && proof.dep_goal) &&
- not (Intset.exists
- (fun i -> Intset.mem i proof.dep_hyps)
+ not (Int.Set.exists
+ (fun i -> Int.Set.mem i proof.dep_hyps)
slice.creates_hyps)
then
begin
s_info.pruned_steps<-s_info.pruned_steps+1;
s_info.pruned_branches<- s_info.pruned_branches +
List.length slice.proofs_todo;
- let created_here=Intset.cardinal slice.creates_hyps in
+ let created_here=Int.Set.cardinal slice.creates_hyps in
s_info.pruned_hyps<-s_info.pruned_hyps+
List.fold_left
- (fun sum dseq -> sum + Intset.cardinal dseq.dep_hyps)
+ (fun sum dseq -> sum + Int.Set.cardinal dseq.dep_hyps)
created_here slice.proofs_todo;
- fill super (pop (Intset.cardinal slice.creates_hyps) proof)
+ fill super (pop (Int.Set.cardinal slice.creates_hyps) proof)
end
else
let dep_hyps=
- Intset.union slice.needs_hyps
- (Intset.diff proof.dep_hyps slice.creates_hyps) in
+ Int.Set.union slice.needs_hyps
+ (Int.Set.diff proof.dep_hyps slice.creates_hyps) in
let dep_goal=
slice.needs_goal ||
((not slice.changes_goal) && proof.dep_goal) in
@@ -235,7 +250,7 @@ let append stack (step,subgoals) =
let embed seq=
{dep_it=seq;
dep_goal=false;
- dep_hyps=Intset.empty}
+ dep_hyps=Int.Set.empty}
let change_goal seq gl=
{seq with
@@ -270,7 +285,7 @@ let add_hyp seqwd f=
cnx=cnx}
| Conjunct (_,_) | Disjunct (_,_) ->
{seq with
- rev_hyps=Intmap.add num f seq.rev_hyps;
+ rev_hyps=Int.Map.add num f seq.rev_hyps;
size=num;
left=left;
right=right;
@@ -285,14 +300,14 @@ let add_hyp seqwd f=
match f1 with
Conjunct (_,_) | Disjunct (_,_) ->
{seq with
- rev_hyps=Intmap.add num f seq.rev_hyps;
+ rev_hyps=Int.Map.add num f seq.rev_hyps;
size=num;
left=left;
right=nright;
cnx=ncnx}
| Arrow(_,_) ->
{seq with
- norev_hyps=Intmap.add num f seq.norev_hyps;
+ norev_hyps=Int.Map.add num f seq.norev_hyps;
size=num;
left=left;
right=nright;
@@ -305,13 +320,13 @@ let add_hyp seqwd f=
cnx=ncnx} in
{seqwd with
dep_it=nseq;
- dep_hyps=Intset.add num seqwd.dep_hyps}
+ dep_hyps=Int.Set.add num seqwd.dep_hyps}
exception Here_is of (int*form)
let choose m=
try
- Intmap.iter (fun i f -> raise (Here_is (i,f))) m;
+ Int.Map.iter (fun i f -> raise (Here_is (i,f))) m;
raise Not_found
with
Here_is (i,f) -> (i,f)
@@ -322,11 +337,11 @@ let search_or seq=
Disjunct (f1,f2) ->
[{dep_it = SI_Or_l;
dep_goal = true;
- dep_hyps = Intset.empty},
+ dep_hyps = Int.Set.empty},
[change_goal (embed seq) f1];
{dep_it = SI_Or_r;
dep_goal = true;
- dep_hyps = Intset.empty},
+ dep_hyps = Int.Set.empty},
[change_goal (embed seq) f2]]
| _ -> []
@@ -336,19 +351,19 @@ let search_norev seq=
match f with
Arrow (Arrow (f1,f2),f3) ->
let nseq =
- {seq with norev_hyps=Intmap.remove i seq.norev_hyps} in
+ {seq with norev_hyps=Int.Map.remove i seq.norev_hyps} in
goals:=
({dep_it=SD_Arrow(i);
dep_goal=false;
- dep_hyps=Intset.singleton i},
+ dep_hyps=Int.Set.singleton i},
[add_hyp
(add_hyp
(change_goal (embed nseq) f2)
(Arrow(f2,f3)))
f1;
add_hyp (embed nseq) f3]):: !goals
- | _ -> anomaly "search_no_rev: can't happen" in
- Intmap.iter add_one seq.norev_hyps;
+ | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen") in
+ Int.Map.iter add_one seq.norev_hyps;
List.rev !goals
let search_in_rev_hyps seq=
@@ -357,8 +372,8 @@ let search_in_rev_hyps seq=
let make_step step=
{dep_it=step;
dep_goal=false;
- dep_hyps=Intset.singleton i} in
- let nseq={seq with rev_hyps=Intmap.remove i seq.rev_hyps} in
+ dep_hyps=Int.Set.singleton i} in
+ let nseq={seq with rev_hyps=Int.Map.remove i seq.rev_hyps} in
match f with
Conjunct (f1,f2) ->
[make_step (SE_And(i)),
@@ -372,7 +387,7 @@ let search_in_rev_hyps seq=
| Arrow (Disjunct (f1,f2),f0) ->
[make_step (SD_Or(i)),
[add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]]
- | _ -> anomaly "search_in_rev_hyps: can't happen"
+ | _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen")
with
Not_found -> search_norev seq
@@ -383,27 +398,27 @@ let search_rev seq=
match f1 with
Conjunct (_,_) | Disjunct (_,_) ->
{seq with cnx=next;
- rev_hyps=Intmap.remove j seq.rev_hyps}
+ rev_hyps=Int.Map.remove j seq.rev_hyps}
| Arrow (_,_) ->
{seq with cnx=next;
- norev_hyps=Intmap.remove j seq.norev_hyps}
+ norev_hyps=Int.Map.remove j seq.norev_hyps}
| _ ->
{seq with cnx=next} in
[{dep_it=SE_Arrow(i,j);
dep_goal=false;
- dep_hyps=Intset.add i (Intset.singleton j)},
+ dep_hyps=Int.Set.add i (Int.Set.singleton j)},
[add_hyp (embed nseq) f2]]
| [] ->
match seq.gl with
Arrow (f1,f2) ->
[{dep_it=SI_Arrow;
dep_goal=true;
- dep_hyps=Intset.empty},
+ dep_hyps=Int.Set.empty},
[add_hyp (change_goal (embed seq) f2) f1]]
| Conjunct (f1,f2) ->
[{dep_it=SI_And;
dep_goal=true;
- dep_hyps=Intset.empty},[change_goal (embed seq) f1;
+ dep_hyps=Int.Set.empty},[change_goal (embed seq) f1;
change_goal (embed seq) f2]]
| _ -> search_in_rev_hyps seq
@@ -412,18 +427,18 @@ let search_all seq=
Some i ->
[{dep_it=SE_False (i);
dep_goal=false;
- dep_hyps=Intset.singleton i},[]]
+ dep_hyps=Int.Set.singleton i},[]]
| None ->
try
let ax = Fmap.find seq.gl seq.left in
[{dep_it=SAx (ax);
dep_goal=true;
- dep_hyps=Intset.singleton ax},[]]
+ dep_hyps=Int.Set.singleton ax},[]]
with Not_found -> search_rev seq
let bare_sequent = embed
- {rev_hyps=Intmap.empty;
- norev_hyps=Intmap.empty;
+ {rev_hyps=Int.Map.empty;
+ norev_hyps=Int.Map.empty;
size=0;
left=Fmap.empty;
right=Fmap.empty;
@@ -442,7 +457,7 @@ let success= function
let branching = function
Incomplete (seq,stack) ->
- check_for_interrupt ();
+ Control.check_for_interrupt ();
let successors = search_all seq in
let _ =
match successors with
@@ -450,7 +465,7 @@ let branching = function
| _::next ->
s_info.nd_branching<-s_info.nd_branching+List.length next in
List.map (append stack) successors
- | Complete prf -> anomaly "already succeeded"
+ | Complete prf -> anomaly (Pp.str "already succeeded")
open Pp
@@ -471,11 +486,11 @@ and pp_atom= function
| Atom n -> int n
| f -> str "(" ++ hv 2 (pp_form f) ++ str ")"
-let pr_form f = msg (pp_form f)
+let pr_form f = pp_form f
let pp_intmap map =
let pp=ref (str "") in
- Intmap.iter (fun i obj -> pp:= (!pp ++
+ Int.Map.iter (fun i obj -> pp:= (!pp ++
pp_form obj ++ cut ())) map;
str "{ " ++ v 0 (!pp) ++ str " }"
@@ -532,7 +547,7 @@ let pp_info () =
int s_info.created_branches ++ str " created" ++ fnl () ++
str "Hypotheses : " ++
int s_info.created_hyps ++ str " created" ++ fnl () in
- msgnl
+ msg_info
( str "Proof-search statistics :" ++ fnl () ++
count_info ++
str "Branch ends: " ++
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 00:57:00 +0000