diff options
Diffstat (limited to 'plugins/firstorder/sequent.ml')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 62 |
1 files changed, 30 insertions, 32 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 50cf14a9..2f7f21e4 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -1,18 +1,18 @@ (************************************************************************) (* 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 Formula open Unify open Tacmach -open Names -open Libnames +open Globnames open Pp let newcnt ()= @@ -48,8 +48,6 @@ let priority = (* pure heuristics, <=0 for non reversible *) | LLexists (_,_) -> 50 | LLarrow (_,_,_) -> -10 -let left_reversible lpat=(priority lpat)>0 - module OrderedFormula= struct type t=Formula.t @@ -69,12 +67,14 @@ module Hitem= struct type t = h_item let compare (id1,co1) (id2,co2)= - (Libnames.RefOrdered.compare - =? (fun oc1 oc2 -> - match oc1,oc2 with - Some (m1,c1),Some (m2,c2) -> - ((-) =? OrderedConstr.compare) m1 m2 c1 c2 - | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2 + let c = Globnames.RefOrdered.compare id1 id2 in + if c = 0 then + let cmp (i1, c1) (i2, c2) = + let c = Int.compare i1 i2 in + if c = 0 then OrderedConstr.compare c1 c2 else c + in + Option.compare cmp co1 co2 + else c end module CM=Map.Make(OrderedConstr) @@ -90,7 +90,7 @@ let cm_add typ nam cm= let cm_remove typ nam cm= try let l=CM.find typ cm in - let l0=List.filter (fun id->id<>nam) l in + let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in match l0 with []->CM.remove typ cm | _ ->CM.add typ l0 cm @@ -120,10 +120,10 @@ let lookup item seq= let p (id2,o)= match o with None -> false - | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in + | Some ((m2,t2) as c2)-> Globnames.eq_gr id id2 && m2>m && more_general c2 c in History.exists p seq.history -let rec add_formula side nam t seq gl= +let add_formula side nam t seq gl= match build_formula side nam t gl seq.cnt with Left f-> begin @@ -163,8 +163,6 @@ let find_left t seq=List.hd (CM.find t seq.context) left_reversible lpat with Heap.EmptyHeap -> false *) -let no_formula seq= - seq.redexes=HP.empty let rec take_formula seq= let hd=HP.maximum seq.redexes @@ -191,36 +189,36 @@ let empty_seq depth= depth=depth} let expand_constructor_hints = - list_map_append (function + List.map_append (function | IndRef ind -> - list_tabulate (fun i -> ConstructRef (ind,i+1)) - (Inductiveops.nconstructors ind) + List.init (Inductiveops.nconstructors ind) + (fun i -> ConstructRef (ind,i+1)) | gr -> [gr]) -let extend_with_ref_list l seq gl= +let extend_with_ref_list l seq gl = let l = expand_constructor_hints l in - let f gr seq= - let c=constr_of_global gr in + let f gr (seq,gl) = + let gl, c = pf_eapply Evd.fresh_global gl gr in let typ=(pf_type_of gl c) in - add_formula Hyp gr typ seq gl in - List.fold_right f l seq + (add_formula Hyp gr typ seq gl,gl) in + List.fold_right f l (seq,gl) -open Auto +open Hints let extend_with_auto_hints l seq gl= let seqref=ref seq in let f p_a_t = match p_a_t.code with - Res_pf (c,_) | Give_exact c + Res_pf (c,_) | Give_exact (c,_) | Res_pf_THEN_trivial_fail (c,_) -> (try - let gr=global_of_constr c in + let gr = global_of_constr c in let typ=(pf_type_of gl c) in seqref:=add_formula Hint gr typ !seqref gl with Not_found->()) | _-> () in - let g _ l = List.iter f l in + let g _ _ l = List.iter f l in let h dbname= let hdb= try @@ -229,18 +227,18 @@ let extend_with_auto_hints l seq gl= error ("Firstorder: "^dbname^" : No such Hint database") in Hint_db.iter g hdb in List.iter h l; - !seqref + !seqref, gl (*FIXME: forgetting about universes*) let print_cmap map= let print_entry c l s= - let xc=Constrextern.extern_constr false (Global.env ()) c in + let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty c in str "| " ++ - Util.prlist Printer.pr_global l ++ + prlist Printer.pr_global l ++ str " : " ++ Ppconstr.pr_constr_expr xc ++ cut () ++ s in - msgnl (v 0 + (v 0 (str "-----" ++ cut () ++ CM.fold print_entry map (mt ()) ++ |