From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- plugins/rtauto/Bintree.v | 16 ++--- plugins/rtauto/Rtauto.v | 2 +- plugins/rtauto/g_rtauto.ml4 | 8 ++- plugins/rtauto/proof_search.ml | 127 ++++++++++++++++++++++------------------ plugins/rtauto/proof_search.mli | 4 +- plugins/rtauto/refl_tauto.ml | 59 ++++++++----------- plugins/rtauto/refl_tauto.mli | 6 +- 7 files changed, 115 insertions(+), 107 deletions(-) (limited to 'plugins/rtauto') diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index fbfa1bfd..267cd472 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Proof. intros S W;induction W. unfold empty,index,get,contents;intros;apply Tget_Tempty. -unfold index,get,push;simpl contents. +unfold index,get,push. simpl @contents. intros i e;rewrite Tget_Tadd. rewrite (Gt_Psucc _ _ e). unfold get in IHW. @@ -209,7 +209,7 @@ Theorem get_Full_Eq : forall S, Full S -> get (index S) S = PNone. intros [index0 contents0] F. case F. unfold empty,index,get,contents;intros;apply Tget_Tempty. -unfold index,get,push;simpl contents. +unfold push,index,get;simpl @contents. intros a S. rewrite Tget_Tadd. rewrite Psucc_Gt. @@ -231,12 +231,12 @@ Proof. intros i a S F. case_eq (i ?= index S). intro e;rewrite (Pos.compare_eq _ _ e). -destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd. +destruct S;unfold get,push,index;simpl @contents;rewrite Tget_Tadd. rewrite Pos.compare_refl;reflexivity. -intros;destruct S;unfold get,push,index;simpl contents;rewrite Tget_Tadd. -simpl index in H;rewrite H;reflexivity. +intros;destruct S;unfold get,push,index;simpl @contents;rewrite Tget_Tadd. +simpl @index in H;rewrite H;reflexivity. intro H;generalize H;clear H. -unfold get,push;simpl index;simpl contents. +unfold get,push;simpl. rewrite Tget_Tadd;intro e;rewrite e. change (get i S=PNone). apply get_Full_Gt;auto. @@ -260,7 +260,7 @@ Qed. Lemma Full_index_one_empty : forall S, Full S -> index S = 1 -> S=empty. intros [ind cont] F one; inversion F. reflexivity. -simpl index in one;assert (h:=Pos.succ_not_1 (index S)). +simpl @index in one;assert (h:=Pos.succ_not_1 (index S)). congruence. Qed. diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index f823cf74..61a160b2 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [ Refl_tauto.rtauto_tac ] + [ "rtauto" ] -> [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ] END 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 *) -(* 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: " ++ diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli index 1aaafbe6..86a2fb66 100644 --- a/plugins/rtauto/proof_search.mli +++ b/plugins/rtauto/proof_search.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* bool val pp: state -> Pp.std_ppcmds -val pr_form : form -> unit +val pr_form : form -> Pp.std_ppcmds val reset_info : unit -> unit diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 7dedb44e..4ffc1f33 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* if not (Termops.dependent (mkRel 1) b) && Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) a = InProp + (pf_env gls) (Tacmach.project gls) a == InProp then let fa=make_form atom_env gls a in let fb=make_form atom_env gls b in @@ -112,25 +104,25 @@ let rec make_form atom_env gls term = make_atom atom_env (normalize term) | Cast(a,_,_) -> make_form atom_env gls a - | Ind ind -> - if ind = Lazy.force li_False then + | Ind (ind, _) -> + if Names.eq_ind ind (fst (Lazy.force li_False)) then Bot else make_atom atom_env (normalize term) - | App(hd,argv) when Array.length argv = 2 -> + | App(hd,argv) when Int.equal (Array.length argv) 2 -> begin try - let ind = destInd hd in - if ind = Lazy.force li_and then + let ind, _ = destInd hd in + if Names.eq_ind ind (fst (Lazy.force li_and)) then let fa=make_form atom_env gls argv.(0) in let fb=make_form atom_env gls argv.(1) in Conjunct (fa,fb) - else if ind = Lazy.force li_or then + else if Names.eq_ind ind (fst (Lazy.force li_or)) then let fa=make_form atom_env gls argv.(0) in let fb=make_form atom_env gls argv.(1) in Disjunct (fa,fb) else make_atom atom_env (normalize term) - with Invalid_argument _ -> make_atom atom_env (normalize term) + with DestKO -> make_atom atom_env (normalize term) end | _ -> make_atom atom_env (normalize term) @@ -143,7 +135,7 @@ let rec make_hyps atom_env gls lenv = function make_hyps atom_env gls (typ::lenv) rest in if List.exists (Termops.dependent (mkVar id)) lenv || (Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) typ <> InProp) + (pf_env gls) (Tacmach.project gls) typ != InProp) then hrec else @@ -151,7 +143,7 @@ let rec make_hyps atom_env gls lenv = function let rec build_pos n = if n<=1 then force node_count l_xH - else if n land 1 = 0 then + else if Int.equal (n land 1) 0 then mkApp (force node_count l_xO,[|build_pos (n asr 1)|]) else mkApp (force node_count l_xI,[|build_pos (n asr 1)|]) @@ -269,22 +261,21 @@ let rtauto_tac gls= let gl=pf_concl gls in let _= if Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) gl <> InProp + (pf_env gls) (Tacmach.project gls) gl != InProp then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in let glf=make_form gamma gls gl in let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in let formula= List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in - let search_fun = - if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then - Search.debug_depth_first - else - Search.depth_first in + let search_fun = match Tacinterp.get_debug() with + | Tactic_debug.DebugOn 0 -> Search.debug_depth_first + | _ -> Search.depth_first + in let _ = begin reset_info (); if !verbose then - msgnl (str "Starting proof-search ..."); + msg_info (str "Starting proof-search ..."); end in let search_start_time = System.get_time () in let prf = @@ -294,10 +285,10 @@ let rtauto_tac gls= let search_end_time = System.get_time () in let _ = if !verbose then begin - msgnl (str "Proof tree found in " ++ + msg_info (str "Proof tree found in " ++ System.fmt_time_difference search_start_time search_end_time); pp_info (); - msgnl (str "Building proof term ... ") + msg_info (str "Building proof term ... ") end in let build_start_time=System.get_time () in let _ = step_count := 0; node_count := 0 in @@ -306,11 +297,11 @@ let rtauto_tac gls= build_form formula; build_proof [] 0 prf|]) in let term= - Term.applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in + applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in let build_end_time=System.get_time () in let _ = if !verbose then begin - msgnl (str "Proof term built in " ++ + msg_info (str "Proof term built in " ++ System.fmt_time_difference build_start_time build_end_time ++ fnl () ++ str "Proof size : " ++ int !step_count ++ @@ -322,14 +313,14 @@ let rtauto_tac gls= let tac_start_time = System.get_time () in let result= if !check then - Tactics.exact_check term gls + Proofview.V82.of_tactic (Tactics.exact_check term) gls else Tactics.exact_no_check term gls in let tac_end_time = System.get_time () in let _ = - if !check then msgnl (str "Proof term type-checking is on"); + if !check then msg_info (str "Proof term type-checking is on"); if !verbose then - msgnl (str "Internal tactic executed in " ++ + msg_info (str "Internal tactic executed in " ++ System.fmt_time_difference tac_start_time tac_end_time) in result diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index 9f7db593..45fb50dc 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Proof_type.goal Tacmach.sigma -> Term.types list -> - (Names.identifier * Term.types option * Term.types) list -> - (Names.identifier * Proof_search.form) list + (Names.Id.t * Term.types option * Term.types) list -> + (Names.Id.t * Proof_search.form) list val rtauto_tac : Proof_type.tactic -- cgit v1.2.3