diff options
Diffstat (limited to 'plugins/firstorder/sequent.ml')
-rw-r--r-- | plugins/firstorder/sequent.ml | 83 |
1 files changed, 40 insertions, 43 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 1248b60a..28599179 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -1,17 +1,18 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Term +open EConstr open CErrors open Util open Formula open Unify -open Tacmach open Globnames open Pp @@ -55,13 +56,7 @@ struct (priority e1.pat) - (priority e2.pat) end -module OrderedConstr= -struct - type t=constr - let compare=constr_ord -end - -type h_item = global_reference * (int*constr) option +type h_item = global_reference * (int*Constr.t) option module Hitem= struct @@ -71,23 +66,25 @@ struct 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 + if c = 0 then Constr.compare c1 c2 else c in Option.compare cmp co1 co2 else c end -module CM=Map.Make(OrderedConstr) +module CM=Map.Make(Constr) module History=Set.Make(Hitem) -let cm_add typ nam cm= +let cm_add sigma typ nam cm= + let typ = EConstr.to_constr sigma typ in try let l=CM.find typ cm in CM.add typ (nam::l) cm with Not_found->CM.add typ [nam] cm -let cm_remove typ nam cm= +let cm_remove sigma typ nam cm= + let typ = EConstr.to_constr sigma typ in try let l=CM.find typ cm in let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in @@ -112,19 +109,19 @@ let deepen seq={seq with depth=seq.depth-1} let record item seq={seq with history=History.add item seq.history} -let lookup item seq= +let lookup sigma item seq= History.mem item seq.history || match item with (_,None)->false - | (id,Some ((m,t) as c))-> + | (id,Some (m, t))-> let p (id2,o)= match o with None -> false - | Some ((m2,t2) as c2)-> Globnames.eq_gr id id2 && m2>m && more_general c2 c in + | Some (m2, t2)-> Globnames.eq_gr id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in History.exists p seq.history -let add_formula side nam t seq gl= - match build_formula side nam t gl seq.cnt with +let add_formula env sigma side nam t seq = + match build_formula env sigma side nam t seq.cnt with Left f-> begin match side with @@ -136,7 +133,7 @@ let add_formula side nam t seq gl= | _ -> {seq with redexes=HP.add f seq.redexes; - context=cm_add f.constr nam seq.context} + context=cm_add sigma f.constr nam seq.context} end | Right t-> match side with @@ -144,18 +141,18 @@ let add_formula side nam t seq gl= {seq with gl=t;glatom=Some t} | _ -> {seq with - context=cm_add t nam seq.context; + context=cm_add sigma t nam seq.context; latoms=t::seq.latoms} -let re_add_formula_list lf seq= +let re_add_formula_list sigma lf seq= let do_one f cm= if f.id == dummy_id then cm - else cm_add f.constr f.id cm in + else cm_add sigma f.constr f.id cm in {seq with redexes=List.fold_right HP.add lf seq.redexes; context=List.fold_right do_one lf seq.context} -let find_left t seq=List.hd (CM.find t seq.context) +let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr sigma t) seq.context) (*let rev_left seq= try @@ -164,7 +161,7 @@ let find_left t seq=List.hd (CM.find t seq.context) with Heap.EmptyHeap -> false *) -let rec take_formula seq= +let rec take_formula sigma seq= let hd=HP.maximum seq.redexes and hp=HP.remove seq.redexes in if hd.id == dummy_id then @@ -172,11 +169,11 @@ let rec take_formula seq= if seq.gl==hd.constr then hd,nseq else - take_formula nseq (* discarding deprecated goal *) + take_formula sigma nseq (* discarding deprecated goal *) else hd,{seq with redexes=hp; - context=cm_remove hd.constr hd.id seq.context} + context=cm_remove sigma hd.constr hd.id seq.context} let empty_seq depth= {redexes=HP.empty; @@ -196,17 +193,17 @@ let expand_constructor_hints = | gr -> [gr]) -let extend_with_ref_list l seq gl = +let extend_with_ref_list env sigma l seq = let l = expand_constructor_hints l in - let f gr (seq,gl) = - let gl, c = pf_eapply Evd.fresh_global gl gr in - let typ=(pf_unsafe_type_of gl c) in - (add_formula Hyp gr typ seq gl,gl) in - List.fold_right f l (seq,gl) + let f gr (seq, sigma) = + let sigma, c = Evd.fresh_global env sigma gr in + let sigma, typ= Typing.type_of env sigma (EConstr.of_constr c) in + (add_formula env sigma Hyp gr typ seq, sigma) in + List.fold_right f l (seq, sigma) open Hints -let extend_with_auto_hints l seq gl= +let extend_with_auto_hints env sigma l seq = let seqref=ref seq in let f p_a_t = match repr_hint p_a_t.code with @@ -214,9 +211,9 @@ let extend_with_auto_hints l seq gl= | Res_pf_THEN_trivial_fail (c,_) -> let (c, _, _) = c in (try - let gr = global_of_constr c in - let typ=(pf_unsafe_type_of gl c) in - seqref:=add_formula Hint gr typ !seqref gl + let (gr, _) = Termops.global_of_constr sigma c in + let typ=(Typing.unsafe_type_of env sigma c) in + seqref:=add_formula env sigma Hint gr typ !seqref with Not_found->()) | _-> () in let g _ _ l = List.iter f l in @@ -225,14 +222,14 @@ let extend_with_auto_hints l seq gl= try searchtable_map dbname with Not_found-> - error ("Firstorder: "^dbname^" : No such Hint database") in + user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database")) in Hint_db.iter g hdb in List.iter h l; - !seqref, gl (*FIXME: forgetting about universes*) + !seqref, sigma (*FIXME: forgetting about universes*) let print_cmap map= let print_entry c l s= - let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty c in + let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty (EConstr.of_constr c) in str "| " ++ prlist Printer.pr_global l ++ str " : " ++ |