diff options
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 41 | ||||
| -rw-r--r-- | plugins/cc/ccalgo.mli | 101 | ||||
| -rw-r--r-- | plugins/cc/ccproof.ml | 4 | ||||
| -rw-r--r-- | plugins/cc/ccproof.mli | 4 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 43 | ||||
| -rw-r--r-- | plugins/cc/cctac.mli | 4 | ||||
| -rw-r--r-- | plugins/cc/g_congruence.mlg | 4 |
7 files changed, 52 insertions, 149 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 500f464ea7..74043d6bc8 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -33,7 +33,6 @@ let debug x = let () = let gdopt= { optdepr=false; - optname="Congruence Verbose"; optkey=["Congruence";"Verbose"]; optread=(fun ()-> !cc_verbose); optwrite=(fun b -> cc_verbose := b)} @@ -492,7 +491,7 @@ let rec add_term state t= Not_found -> let b=next uf in let trm = constr_of_term t in - let typ = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr trm) in + let typ = Retyping.get_type_of state.env state.sigma (EConstr.of_constr trm) in let typ = canonize_name state.sigma typ in let new_node= match t with @@ -809,23 +808,23 @@ let new_state_var typ state = let complete_one_class state i= match (get_representative state.uf i).inductive_status with - Partial pac -> - let rec app t typ n = - if n<=0 then t else - let _,etyp,rest= destProd typ in - let id = new_state_var (EConstr.of_constr etyp) state in - app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in - let _c = Typing.unsafe_type_of state.env state.sigma - (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in - let _c = EConstr.Unsafe.to_constr _c in - let _args = - List.map (fun i -> constr_of_term (term state.uf i)) - pac.args in - let typ = Term.prod_applist _c (List.rev _args) in - let ct = app (term state.uf i) typ pac.arity in - state.uf.epsilons <- pac :: state.uf.epsilons; - ignore (add_term state ct) - | _ -> anomaly (Pp.str "wrong incomplete class.") + | Partial pac -> + let rec app t typ n = + if n<=0 then t else + let _,etyp,rest= destProd typ in + let id = new_state_var (EConstr.of_constr etyp) state in + app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in + let c = Retyping.get_type_of state.env state.sigma + (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in + let c = EConstr.Unsafe.to_constr c in + let args = + List.map (fun i -> constr_of_term (term state.uf i)) + pac.args in + let typ = Term.prod_applist c (List.rev args) in + let ct = app (term state.uf i) typ pac.arity in + state.uf.epsilons <- pac :: state.uf.epsilons; + ignore (add_term state ct) + | _ -> anomaly (Pp.str "wrong incomplete class.") let complete state = Int.Set.iter (complete_one_class state) state.pa_classes diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 3dc934b426..3270f74479 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -1,14 +1,13 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * 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 Util open Constr open Names @@ -156,102 +155,6 @@ val subterms : forest -> int -> int * int val join_path : forest -> int -> int -> ((int * int) * equality) list * ((int * int) * equality) list -val make_fun_table : state -> Int.Set.t PafMap.t - -val do_match : state -> - (quant_eq * int array) list ref -> matching_problem Stack.t -> unit - -val init_pb_stack : state -> matching_problem Stack.t - -val paf_of_patt : int Termhash.t -> ccpattern -> pa_fun - -val find_instances : state -> (quant_eq * int array) list - val execute : bool -> state -> explanation option val pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t - -val empty_forest: unit -> forest - - - - - - - - - - -(*type pa_constructor - - -module PacMap:CSig.MapS with type key=pa_constructor - -type term = - Symb of Term.constr - | Eps - | Appli of term * term - | Constructor of Names.constructor*int*int - -type rule = - Congruence - | Axiom of Names.Id.t - | Injection of int*int*int*int - -type equality = - {lhs : int; - rhs : int; - rule : rule} - -module ST : -sig - type t - val empty : unit -> t - val enter : int -> int * int -> t -> unit - val query : int * int -> t -> int - val delete : int -> t -> unit - val delete_list : int list -> t -> unit -end - -module UF : -sig - type t - exception Discriminable of int * int * int * int * t - val empty : unit -> t - val find : t -> int -> int - val size : t -> int -> int - val get_constructor : t -> int -> Names.constructor - val pac_arity : t -> int -> int * int -> int - val mem_node_pac : t -> int -> int * int -> int - val add_pacs : t -> int -> pa_constructor PacMap.t -> - int list * equality list - val term : t -> int -> term - val subterms : t -> int -> int * int - val add : t -> term -> int - val union : t -> int -> int -> equality -> int list * equality list - val join_path : t -> int -> int -> - ((int*int)*equality) list* - ((int*int)*equality) list -end - - -val combine_rec : UF.t -> int list -> equality list -val process_rec : UF.t -> equality list -> int list - -val cc : UF.t -> unit - -val make_uf : - (Names.Id.t * (term * term)) list -> UF.t - -val add_one_diseq : UF.t -> (term * term) -> int * int - -val add_disaxioms : - UF.t -> (Names.Id.t * (term * term)) list -> - (Names.Id.t * (int * int)) list - -val check_equal : UF.t -> int * int -> bool - -val find_contradiction : UF.t -> - (Names.Id.t * (int * int)) list -> - (Names.Id.t * (int * int)) -*) diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index f82a55fe71..53d8c5bdd9 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index 88c45afc2f..0a2de9816c 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 556e6b48e6..0c305d09e8 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -90,14 +90,13 @@ let rec decompose_term env sigma t= if closed0 sigma t then Symb (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) else raise Not_found (* decompose equality in members and type *) -open Termops let atom_of_constr env sigma term = let wh = whd_delta env sigma term in let kot = EConstr.kind sigma wh in match kot with App (f,args)-> - if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3 + if isRefX sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3 then `Eq (args.(0), decompose_term env sigma args.(1), decompose_term env sigma args.(2)) @@ -132,7 +131,7 @@ let non_trivial = function let patterns_of_constr env sigma nrels term= let f,args= try destApp sigma (whd_delta env sigma term) with DestKO -> raise Not_found in - if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3 + if isRefX sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3 then let patt1,rels1 = pattern_of_constr env sigma args.(1) and patt2,rels2 = pattern_of_constr env sigma args.(2) in @@ -153,7 +152,7 @@ let patterns_of_constr env sigma nrels term= let rec quantified_atom_of_constr env sigma nrels term = match EConstr.kind sigma (whd_delta env sigma term) with Prod (id,atom,ff) -> - if is_global sigma (Lazy.force _False) ff then + if isRefX sigma (Lazy.force _False) ff then let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else @@ -165,7 +164,7 @@ let rec quantified_atom_of_constr env sigma nrels term = let litteral_of_constr env sigma term= match EConstr.kind sigma (whd_delta env sigma term) with | Prod (id,atom,ff) -> - if is_global sigma (Lazy.force _False) ff then + if isRefX sigma (Lazy.force _False) ff then match (atom_of_constr env sigma atom) with `Eq(t,a,b) -> `Neq(t,a,b) | `Other(p) -> `Nother(p) @@ -277,10 +276,12 @@ let refresh_type env evm ty = Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true (Some false) env evm ty -let refresh_universes ty k = +let type_and_refresh c k = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let evm = Tacmach.New.project gl in + (* XXX is get_type_of enough? *) + let evm, ty = Typing.type_of env evm c in let evm, ty = refresh_type env evm ty in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k ty) end @@ -289,7 +290,6 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c) let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> - let type_of t = Tacmach.New.pf_unsafe_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with Ax c -> exact_check (EConstr.of_constr c) @@ -297,17 +297,17 @@ let rec proof_tac p : unit Proofview.tactic = let c = EConstr.of_constr c in let l=constr_of_term p.p_lhs and r=constr_of_term p.p_rhs in - refresh_universes (type_of l) (fun typ -> + type_and_refresh l (fun typ -> app_global _sym_eq [|typ;r;l;c|] exact_check) | Refl t -> let lr = constr_of_term t in - refresh_universes (type_of lr) (fun typ -> + type_and_refresh lr (fun typ -> app_global _refl_equal [|typ;constr_of_term t|] exact_check) | Trans (p1,p2)-> let t1 = constr_of_term p1.p_lhs and t2 = constr_of_term p1.p_rhs and t3 = constr_of_term p2.p_rhs in - refresh_universes (type_of t2) (fun typ -> + type_and_refresh t2 (fun typ -> let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in Tacticals.New.tclTHENS prf [(proof_tac p1);(proof_tac p2)]) | Congr (p1,p2)-> @@ -315,9 +315,9 @@ let rec proof_tac p : unit Proofview.tactic = and tx1=constr_of_term p2.p_lhs and tf2=constr_of_term p1.p_rhs and tx2=constr_of_term p2.p_rhs in - refresh_universes (type_of tf1) (fun typf -> - refresh_universes (type_of tx1) (fun typx -> - refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx -> + type_and_refresh tf1 (fun typf -> + type_and_refresh tx1 (fun typx -> + type_and_refresh (mkApp (tf1,[|tx1|])) (fun typfx -> let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in let appx1 = mkLambda(make_annot (Name id) Sorts.Relevant,typf,mkApp(mkRel 1,[|tx1|])) in let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in @@ -341,8 +341,8 @@ let rec proof_tac p : unit Proofview.tactic = let tj=constr_of_term prf.p_rhs in let default=constr_of_term p.p_lhs in let special=mkRel (1+nargs-argind) in - refresh_universes (type_of ti) (fun intype -> - refresh_universes (type_of default) (fun outtype -> + type_and_refresh ti (fun intype -> + type_and_refresh default (fun outtype -> let sigma, proj = build_projection intype cstr special default gl in @@ -362,7 +362,7 @@ let refute_tac c t1 t2 p = let neweq= app_global _eq [|intype;tt1;tt2|] in Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] - in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k + in type_and_refresh tt1 k end let refine_exact_check c = @@ -382,7 +382,7 @@ let convert_to_goal_tac c t1 t2 p = let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) [proof_tac p; endt refine_exact_check] - in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k + in type_and_refresh tt2 k end let convert_to_hyp_tac c1 t1 c2 t2 p = @@ -401,7 +401,8 @@ let discriminate_tac cstru p = let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in let env = Proofview.Goal.env gl in let evm = Tacmach.New.project gl in - let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl lhs) in + let evm, intype = Typing.type_of env evm lhs in + let evm, intype = refresh_type env evm intype in let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in let neweq=app_global _eq [|intype;lhs;rhs|] in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) @@ -515,7 +516,7 @@ let f_equal = in Proofview.tclORELSE begin match EConstr.kind sigma concl with - | App (r,[|_;t;t'|]) when is_global sigma (Lazy.force _eq) r -> + | App (r,[|_;t;t'|]) when isRefX sigma (Lazy.force _eq) r -> begin match EConstr.kind sigma t, EConstr.kind sigma t' with | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') -> let rec cuts i = diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index 5648b45a9e..52fc3acb6f 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/cc/g_congruence.mlg b/plugins/cc/g_congruence.mlg index 66a5c16a90..3920e3da75 100644 --- a/plugins/cc/g_congruence.mlg +++ b/plugins/cc/g_congruence.mlg @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |