diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /plugins/rtauto/proof_search.ml | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'plugins/rtauto/proof_search.ml')
-rw-r--r-- | plugins/rtauto/proof_search.ml | 127 |
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: " ++ |