From 9a0c61b81a2d9c0024b20a6c7ad8af01026739b0 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Dec 2012 10:56:41 +0000 Subject: Moved Intset and Intmap to Int namespace. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/rtauto/proof_search.ml | 70 +++++++++++++++++++++--------------------- 1 file changed, 35 insertions(+), 35 deletions(-) (limited to 'plugins/rtauto/proof_search.ml') diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 20ec17269..5cb97d4bd 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -65,8 +65,8 @@ type form= module Fmap=Map.Make(struct type t=form let compare=compare end) 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; @@ -127,16 +127,16 @@ let add_step s sub = 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 @@ -161,25 +161,25 @@ let rec fill stack proof = !pruning && 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 @@ -226,7 +226,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 @@ -261,7 +261,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; @@ -276,14 +276,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; @@ -296,13 +296,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) @@ -313,11 +313,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]] | _ -> [] @@ -327,11 +327,11 @@ 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) @@ -339,7 +339,7 @@ let search_norev seq= f1; add_hyp (embed nseq) f3]):: !goals | _ -> anomaly "search_no_rev: can't happen" in - Intmap.iter add_one seq.norev_hyps; + Int.Map.iter add_one seq.norev_hyps; List.rev !goals let search_in_rev_hyps seq= @@ -348,8 +348,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)), @@ -374,27 +374,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 @@ -403,18 +403,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; @@ -466,7 +466,7 @@ 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 " }" -- cgit v1.2.3