diff options
Diffstat (limited to 'plugins')
61 files changed, 1081 insertions, 751 deletions
diff --git a/plugins/Derive/derive.ml b/plugins/Derive/derive.ml index c6a96b31a..906f5e383 100644 --- a/plugins/Derive/derive.ml +++ b/plugins/Derive/derive.ml @@ -7,14 +7,14 @@ (************************************************************************) let interp_init_def_and_relation env sigma init_def r = - let init_def = Constrintern.interp_constr sigma env init_def in + let init_def, _ = Constrintern.interp_constr sigma env init_def in let init_type = Typing.type_of env sigma init_def in let r_type = let open Term in mkProd (Names.Anonymous,init_type, mkProd (Names.Anonymous,init_type,mkProp)) in - let r = Constrintern.interp_casted_constr sigma env r r_type in + let r, _ = Constrintern.interp_casted_constr sigma env r r_type in init_def , init_type , r @@ -23,7 +23,7 @@ let interp_init_def_and_relation env sigma init_def r = [lemma] as the proof. *) let start_deriving f init_def r lemma = let env = Global.env () in - let kind = Decl_kinds.(Global,DefinitionBody Definition) in + let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in let ( init_def , init_type , r ) = interp_init_def_and_relation env Evd.empty init_def r in diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index a515deefd..795211c20 100644 --- a/plugins/btauto/Algebra.v +++ b/plugins/btauto/Algebra.v @@ -8,11 +8,37 @@ repeat match goal with apply <- andb_true_iff; split end. +Arguments decide P /H. + Hint Extern 5 => progress bool. Ltac define t x H := set (x := t) in *; assert (H : t = x) by reflexivity; clearbody x. +Lemma Decidable_sound : forall P (H : Decidable P), + decide P = true -> P. +Proof. +intros P H Hp; apply -> Decidable_spec; assumption. +Qed. + +Lemma Decidable_complete : forall P (H : Decidable P), + P -> decide P = true. +Proof. +intros P H Hp; apply <- Decidable_spec; assumption. +Qed. + +Lemma Decidable_sound_alt : forall P (H : Decidable P), + ~ P -> decide P = false. +Proof. +intros P [wit spec] Hd; destruct wit; simpl; tauto. +Qed. + +Lemma Decidable_complete_alt : forall P (H : Decidable P), + decide P = false -> ~ P. +Proof. + intros P [wit spec] Hd Hc; simpl in *; intuition congruence. +Qed. + Ltac try_rewrite := repeat match goal with | [ H : ?P |- _ ] => rewrite H @@ -142,6 +168,7 @@ end. Program Instance Decidable_eq_poly : forall (p q : poly), Decidable (eq p q) := { Decidable_witness := beq_poly p q }. + Next Obligation. split. revert q; induction p; intros [] ?; simpl in *; bool; try_decide; @@ -185,8 +212,8 @@ Program Instance Decidable_valid : forall n p, Decidable (valid n p) := { }. Next Obligation. split. - revert n; induction p; simpl in *; intuition; bool; try_decide; auto. - intros H; induction H; simpl in *; bool; try_decide; auto. + revert n; induction p; unfold valid_dec in *; intuition; bool; try_decide; auto. + intros H; induction H; unfold valid_dec in *; bool; try_decide; auto. Qed. (** Basic algebra *) diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index b81821a2e..6a0f4d852 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -3,7 +3,7 @@ let contrib_name = "btauto" let init_constant dir s = let find_constant contrib dir s = - Globnames.constr_of_global (Coqlib.find_reference contrib dir s) + Universes.constr_of_global (Coqlib.find_reference contrib dir s) in find_constant contrib_name dir s diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 046ecf775..c726fd5de 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -123,7 +123,7 @@ module PacMap=Map.Make(PacOrd) module PafMap=Map.Make(PafOrd) type cinfo= - {ci_constr: constructor; (* inductive type *) + {ci_constr: pconstructor; (* inductive type *) ci_arity: int; (* # args *) ci_nhyps: int} (* # projectable args *) @@ -142,13 +142,13 @@ type term= let rec term_equal t1 t2 = match t1, t2 with - | Symb c1, Symb c2 -> eq_constr c1 c2 + | Symb c1, Symb c2 -> eq_constr_nounivs c1 c2 | Product (s1, t1), Product (s2, t2) -> family_eq s1 s2 && family_eq t1 t2 | Eps i1, Eps i2 -> Id.equal i1 i2 | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2 - | Constructor {ci_constr=c1; ci_arity=i1; ci_nhyps=j1}, - Constructor {ci_constr=c2; ci_arity=i2; ci_nhyps=j2} -> - Int.equal i1 i2 && Int.equal j1 j2 && eq_constructor c1 c2 + | Constructor {ci_constr=(c1,u1); ci_arity=i1; ci_nhyps=j1}, + Constructor {ci_constr=(c2,u2); ci_arity=i2; ci_nhyps=j2} -> + Int.equal i1 i2 && Int.equal j1 j2 && eq_constructor c1 c2 (* FIXME check eq? *) | _ -> false open Hashset.Combine @@ -163,7 +163,7 @@ let rec hash_term = function | Product (s1, s2) -> combine3 2 (hash_sorts_family s1) (hash_sorts_family s2) | Eps i -> combine 3 (Id.hash i) | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2) - | Constructor {ci_constr=c; ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j + | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j type ccpattern = PApp of term * ccpattern list (* arguments are reversed *) @@ -234,7 +234,7 @@ type node = module Constrhash = Hashtbl.Make (struct type t = constr - let equal = eq_constr + let equal = eq_constr_nounivs let hash = hash_constr end) module Typehash = Constrhash @@ -404,32 +404,50 @@ let _B_ = Name (Id.of_string "A") let _body_ = mkProd(Anonymous,mkRel 2,mkRel 2) let cc_product s1 s2 = - mkLambda(_A_,mkSort(Termops.new_sort_in_family s1), - mkLambda(_B_,mkSort(Termops.new_sort_in_family s2),_body_)) + mkLambda(_A_,mkSort(Universes.new_sort_in_family s1), + mkLambda(_B_,mkSort(Universes.new_sort_in_family s2),_body_)) let rec constr_of_term = function - Symb s->s + Symb s-> applist_projection s [] | Product(s1,s2) -> cc_product s1 s2 | Eps id -> mkVar id - | Constructor cinfo -> mkConstruct cinfo.ci_constr + | Constructor cinfo -> mkConstructU cinfo.ci_constr | Appli (s1,s2)-> make_app [(constr_of_term s2)] s1 and make_app l=function Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1 - | other -> applistc (constr_of_term other) l + | other -> + applist_proj other l +and applist_proj c l = + match c with + | Symb s -> applist_projection s l + | _ -> applistc (constr_of_term c) l +and applist_projection c l = + match kind_of_term c with + | Const c when Environ.is_projection (fst c) (Global.env()) -> + (match l with + | [] -> (* Expand the projection *) + let kn = fst c in + let ty,_ = Typeops.type_of_constant (Global.env ()) c in + let pb = Environ.lookup_projection kn (Global.env()) in + let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in + it_mkLambda_or_LetIn (mkProj(kn,mkRel 1)) ctx + | hd :: tl -> + applistc (mkProj (fst c, hd)) tl) + | _ -> applistc c l let rec canonize_name c = let func = canonize_name in match kind_of_term c with - | Const kn -> + | Const (kn,u) -> let canon_const = constant_of_kn (canonical_con kn) in - (mkConst canon_const) - | Ind (kn,i) -> + (mkConstU (canon_const,u)) + | Ind ((kn,i),u) -> let canon_mind = mind_of_kn (canonical_mind kn) in - (mkInd (canon_mind,i)) - | Construct ((kn,i),j) -> + (mkIndU ((canon_mind,i),u)) + | Construct (((kn,i),j),u) -> let canon_mind = mind_of_kn (canonical_mind kn) in - mkConstruct ((canon_mind,i),j) + mkConstructU (((canon_mind,i),j),u) | Prod (na,t,ct) -> mkProd (na,func t, func ct) | Lambda (na,t,ct) -> @@ -438,6 +456,9 @@ let rec canonize_name c = mkLetIn (na, func b,func t,func ct) | App (ct,l) -> mkApp (func ct,Array.smartmap func l) + | Proj(kn,c) -> + let canon_const = constant_of_kn (canonical_con kn) in + (mkProj (canon_const, func c)) | _ -> c (* rebuild a term from a pattern and a substitution *) @@ -469,7 +490,7 @@ let rec add_term state t= try Termhash.find uf.syms t with Not_found -> let b=next uf in - let trm = Termops.refresh_universes (constr_of_term t) in + let trm = constr_of_term t in let typ = pf_type_of state.gls trm in let typ = canonize_name typ in let new_node= diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 5d286c732..0c5d6ca1f 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -11,7 +11,7 @@ open Term open Names type cinfo = - {ci_constr: constructor; (* inductive type *) + {ci_constr: pconstructor; (* inductive type *) ci_arity: int; (* # args *) ci_nhyps: int} (* # projectable args *) diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 5244dcf17..4e1806f5a 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -20,7 +20,7 @@ type rule= | Refl of term | Trans of proof*proof | Congr of proof*proof - | Inject of proof*constructor*int*int + | Inject of proof*pconstructor*int*int and proof = {p_lhs:term;p_rhs:term;p_rule:rule} diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index b8a8d229a..50e3624d0 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -16,7 +16,7 @@ type rule= | Refl of term | Trans of proof*proof | Congr of proof*proof - | Inject of proof*constructor*int*int + | Inject of proof*pconstructor*int*int and proof = private {p_lhs:term;p_rhs:term;p_rule:rule} diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index ac148fe18..783abc5d8 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -23,21 +23,17 @@ open Pp open Errors open Util -let constant dir s = lazy (Coqlib.gen_constant "CC" dir s) - -let _f_equal = constant ["Init";"Logic"] "f_equal" - -let _eq_rect = constant ["Init";"Logic"] "eq_rect" - -let _refl_equal = constant ["Init";"Logic"] "eq_refl" - -let _sym_eq = constant ["Init";"Logic"] "eq_sym" - -let _trans_eq = constant ["Init";"Logic"] "eq_trans" - -let _eq = constant ["Init";"Logic"] "eq" - -let _False = constant ["Init";"Logic"] "False" +let reference dir s = Coqlib.gen_reference "CC" dir s + +let _f_equal = reference ["Init";"Logic"] "f_equal" +let _eq_rect = reference ["Init";"Logic"] "eq_rect" +let _refl_equal = reference ["Init";"Logic"] "eq_refl" +let _sym_eq = reference ["Init";"Logic"] "eq_sym" +let _trans_eq = reference ["Init";"Logic"] "eq_trans" +let _eq = reference ["Init";"Logic"] "eq" +let _False = reference ["Init";"Logic"] "False" +let _True = reference ["Init";"Logic"] "True" +let _I = reference ["Init";"Logic"] "I" let whd env= let infos=Closure.create_clos_infos Closure.betaiotazeta env in @@ -64,32 +60,36 @@ let rec decompose_term env sigma t= Appli(Appli(Product (sort_a,sort_b) , decompose_term env sigma a), decompose_term env sigma b) - | Construct c-> - let (mind,i_ind),i_con = c in + | Construct c -> + let (((mind,i_ind),i_con),u)= c in let canon_mind = mind_of_kn (canonical_mind mind) in let canon_ind = canon_mind,i_ind in let (oib,_)=Global.lookup_inductive (canon_ind) in let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in - Constructor {ci_constr= (canon_ind,i_con); + Constructor {ci_constr= ((canon_ind,i_con),u); ci_arity=nargs; ci_nhyps=nargs-oib.mind_nparams} | Ind c -> - let mind,i_ind = c in + let (mind,i_ind),u = c in let canon_mind = mind_of_kn (canonical_mind mind) in - let canon_ind = canon_mind,i_ind in (Symb (mkInd canon_ind)) - | Const c -> + let canon_ind = canon_mind,i_ind in (Symb (mkIndU (canon_ind,u))) + | Const (c,u) -> let canon_const = constant_of_kn (canonical_con c) in - (Symb (mkConst canon_const)) + (Symb (mkConstU (canon_const,u))) + | Proj (p, c) -> + let canon_const = constant_of_kn (canonical_con p) in + (Appli (Symb (mkConst canon_const), decompose_term env sigma c)) | _ ->if closed0 t then (Symb t) else raise Not_found (* decompose equality in members and type *) +open Globnames let atom_of_constr env sigma term = let wh = (whd_delta env term) in let kot = kind_of_term wh in match kot with App (f,args)-> - if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3 + if is_global _eq f && Int.equal (Array.length args) 3 then `Eq (args.(0), decompose_term env sigma args.(1), decompose_term env sigma args.(2)) @@ -124,7 +124,7 @@ let non_trivial = function let patterns_of_constr env sigma nrels term= let f,args= try destApp (whd_delta env term) with DestKO -> raise Not_found in - if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3 + if is_global _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 @@ -145,7 +145,7 @@ let patterns_of_constr env sigma nrels term= let rec quantified_atom_of_constr env sigma nrels term = match kind_of_term (whd_delta env term) with Prod (id,atom,ff) -> - if eq_constr ff (Lazy.force _False) then + if is_global _False ff then let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else @@ -157,7 +157,7 @@ let rec quantified_atom_of_constr env sigma nrels term = let litteral_of_constr env sigma term= match kind_of_term (whd_delta env term) with | Prod (id,atom,ff) -> - if eq_constr ff (Lazy.force _False) then + if is_global _False ff then match (atom_of_constr env sigma atom) with `Eq(t,a,b) -> `Neq(t,a,b) | `Other(p) -> `Nother(p) @@ -218,13 +218,13 @@ let make_prb gls depth additionnal_terms = (* indhyps builds the array of arrays of constructor hyps for (ind largs) *) -let build_projection intype outtype (cstr:constructor) special default gls= +let build_projection intype outtype (cstr:pconstructor) special default gls= let env=pf_env gls in let (h,argv) = try destApp intype with DestKO -> (intype,[||]) in - let ind=destInd h in - let types=Inductiveops.arities_of_constructors env ind in + let ind,u=destInd h in + let types=Inductiveops.arities_of_constructors env (ind,u) in let lp=Array.length types in - let ci=pred (snd cstr) in + let ci=pred (snd(fst cstr)) in let branch i= let ti= prod_appvect types.(i) argv in let rc=fst (decompose_prod_assum ti) in @@ -243,60 +243,67 @@ let build_projection intype outtype (cstr:constructor) special default gls= let _M =mkMeta +let app_global f args k = + Tacticals.pf_constr_of_global f (fun fc -> k (mkApp (fc, args))) + +let new_app_global f args k = + Tacticals.New.pf_constr_of_global f (fun fc -> k (mkApp (fc, args))) + +let new_exact_check c = Proofview.V82.tactic (exact_check c) +let new_refine c = Proofview.V82.tactic (refine c) + let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> let type_of = Tacmach.New.pf_type_of gl in + try (* type_of can raise exceptions *) match p.p_rule with - Ax c -> Proofview.V82.tactic (exact_check c) + Ax c -> new_exact_check c | SymAx c -> Proofview.V82.tactic begin fun gls -> - let l=constr_of_term p.p_lhs and - r=constr_of_term p.p_rhs in - let typ = Termops.refresh_universes (pf_type_of gls l) in - exact_check - (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls + let l=constr_of_term p.p_lhs and + r=constr_of_term p.p_rhs in + let typ = (* Termops.refresh_universes *)pf_type_of gls l in + (app_global _sym_eq [|typ;r;l;c|] exact_check) gls end | Refl t -> Proofview.V82.tactic begin fun gls -> - let lr = constr_of_term t in - let typ = Termops.refresh_universes (pf_type_of gls lr) in - exact_check - (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls + let lr = constr_of_term t in + let typ = (* Termops.refresh_universes *) (pf_type_of gls lr) in + (app_global _refl_equal [|typ;constr_of_term t|] exact_check) gls end | 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 - let typ = Termops.refresh_universes (type_of t2) in - let prf = - mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in - Tacticals.New.tclTHENS (Proofview.V82.tactic (refine prf)) [(proof_tac p1);(proof_tac p2)] + let typ = (* Termops.refresh_universes *) (type_of t2) in + let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in + Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)] | Congr (p1,p2)-> let tf1=constr_of_term p1.p_lhs 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 - let typf = Termops.refresh_universes (type_of tf1) in - let typx = Termops.refresh_universes (type_of tx1) in - let typfx = Termops.refresh_universes (type_of (mkApp (tf1,[|tx1|]))) in + let typf = (* Termops.refresh_universes *)(type_of tf1) in + let typx = (* Termops.refresh_universes *) (type_of tx1) in + let typfx = (* Termops.refresh_universes *) (type_of (mkApp (tf1,[|tx1|]))) in let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in let lemma1 = - mkApp(Lazy.force _f_equal, - [|typf;typfx;appx1;tf1;tf2;_M 1|]) in + app_global _f_equal + [|typf;typfx;appx1;tf1;tf2;_M 1|] in let lemma2= - mkApp(Lazy.force _f_equal, - [|typx;typfx;tf2;tx1;tx2;_M 1|]) in + app_global _f_equal + [|typx;typfx;tf2;tx1;tx2;_M 1|] in let prf = - mkApp(Lazy.force _trans_eq, + app_global _trans_eq [|typfx; mkApp(tf1,[|tx1|]); mkApp(tf2,[|tx1|]); - mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in - Tacticals.New.tclTHENS (Proofview.V82.tactic (refine prf)) - [Tacticals.New.tclTHEN (Proofview.V82.tactic (refine lemma1)) (proof_tac p1); + mkApp(tf2,[|tx2|]);_M 2;_M 3|] in + Tacticals.New.tclTHENS (Proofview.V82.tactic (prf refine)) + [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma1 refine)) (proof_tac p1); Tacticals.New.tclFIRST - [Tacticals.New.tclTHEN (Proofview.V82.tactic (refine lemma2)) (proof_tac p2); + [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2); reflexivity; Proofview.tclZERO (UserError ("Congruence" , (Pp.str @@ -305,46 +312,48 @@ let rec proof_tac p : unit Proofview.tactic = let ti=constr_of_term prf.p_lhs in let tj=constr_of_term prf.p_rhs in let default=constr_of_term p.p_lhs in - let intype = Termops.refresh_universes (type_of ti) in - let outtype = Termops.refresh_universes (type_of default) in + let intype = (* Termops.refresh_universes *) (type_of ti) in + let outtype = (* Termops.refresh_universes *) (type_of default) in let special=mkRel (1+nargs-argind) in let proj = Tacmach.New.of_old (build_projection intype outtype cstr special default) gl in let injt= - mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in - Tacticals.New.tclTHEN (Proofview.V82.tactic (refine injt)) (proof_tac prf) + app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in + Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end let refute_tac c t1 t2 p = Proofview.Goal.enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let intype = - Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt1)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl in - let neweq= - mkApp(Lazy.force _eq, - [|intype;tt1;tt2|]) in + let neweq= new_app_global _eq [|intype;tt1;tt2|] in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in let false_t=mkApp (c,[|mkVar hid|]) in - Tacticals.New.tclTHENS (assert_tac (Name hid) neweq) + Tacticals.New.tclTHENS (neweq (assert_tac (Name hid))) [proof_tac p; simplest_elim false_t] end +let refine_exact_check c gl = + let evm, _ = pf_apply e_type_of gl c in + Tacticals.tclTHEN (Refiner.tclEVARS evm) (exact_check c) gl + let convert_to_goal_tac c t1 t2 p = Proofview.Goal.enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let sort = - Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt2)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl in - let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in + let neweq= new_app_global _eq [|sort;tt1;tt2|] in let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in let identity=mkLambda (Name x,sort,mkRel 1) in - let endt=mkApp (Lazy.force _eq_rect, - [|sort;tt1;identity;c;tt2;mkVar e|]) in - Tacticals.New.tclTHENS (assert_tac (Name e) neweq) - [proof_tac p; Proofview.V82.tactic (exact_check endt)] + let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in + Tacticals.New.tclTHENS (neweq (assert_tac (Name e))) + [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] end let convert_to_hyp_tac c1 t1 c2 t2 p = @@ -357,29 +366,36 @@ let convert_to_hyp_tac c1 t1 c2 t2 p = simplest_elim false_t] end -let discriminate_tac cstr p = +let discriminate_tac (cstr,u as cstru) p = Proofview.Goal.enter begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in let intype = - Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl in let concl = Proofview.Goal.concl gl in - let outsort = mkType (Termops.new_univ ()) in + (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in *) + (* let outsort = mkSort outsort in *) let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in - let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in - let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in - let trivial = Tacmach.New.of_old (fun gls -> pf_type_of gls identity) gl in - let outtype = mkType (Termops.new_univ ()) in + (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *) + (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *) + let identity = Universes.constr_of_global _I in + (* let trivial=pf_type_of gls identity in *) + let trivial = Universes.constr_of_global _True in + let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in + let outtype = mkSort outtype in let pred=mkLambda(Name xid,outtype,mkRel 1) in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in - let proj = Tacmach.New.of_old (build_projection intype outtype cstr trivial concl) gl in - let injt=mkApp (Lazy.force _f_equal, - [|intype;outtype;proj;t1;t2;mkVar hid|]) in - let endt=mkApp (Lazy.force _eq_rect, - [|outtype;trivial;pred;identity;concl;injt|]) in - let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in - Tacticals.New.tclTHENS (assert_tac (Name hid) neweq) - [proof_tac p; Proofview.V82.tactic (exact_check endt)] + let proj = Tacmach.New.of_old (build_projection intype outtype cstru trivial concl) gl in + let injt=app_global _f_equal + [|intype;outtype;proj;t1;t2;mkVar hid|] in + let endt k = + injt (fun injt -> + app_global _eq_rect + [|outtype;trivial;pred;identity;concl;injt|] k) in + let neweq=new_app_global _eq [|intype;t1;t2|] in + Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evm) + (Tacticals.New.tclTHENS (neweq (assert_tac (Name hid))) + [proof_tac p; Proofview.V82.tactic (endt exact_check)]) end (* wrap everything *) @@ -389,7 +405,7 @@ let build_term_to_complete uf meta pac = let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in let dummy_args = List.rev (List.init pac.arity meta) in let all_args = List.rev_append real_args dummy_args in - applistc (mkConstruct cinfo.ci_constr) all_args + applistc (mkConstructU cinfo.ci_constr) all_args let cc_tactic depth additionnal_terms = Proofview.Goal.enter begin fun gl -> @@ -457,7 +473,7 @@ let congruence_tac depth l = might be slow now, let's rather do something equivalent to a "simple apply refl_equal" *) -let simple_reflexivity () = apply (Lazy.force _refl_equal) +let simple_reflexivity () = apply (Universes.constr_of_global _refl_equal) (* The [f_equal] tactic. @@ -472,15 +488,17 @@ let f_equal = let type_of = Tacmach.New.pf_type_of gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) - let ty = Termops.refresh_universes (type_of c1) in - Tacticals.New.tclTRY (Tacticals.New.tclTHEN - (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) - (Tacticals.New.tclTRY (Proofview.V82.tactic (simple_reflexivity ())))) + let ty = (* Termops.refresh_universes *) (type_of c1) in + if eq_constr_nounivs c1 c2 then Proofview.tclUNIT () + else + Tacticals.New.tclTRY (Tacticals.New.tclTHEN + ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut) + (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) (fun c -> Proofview.V82.tactic (apply c))))) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE begin match kind_of_term concl with - | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) -> + | App (r,[|_;t;t'|]) when Globnames.is_global _eq r -> begin match kind_of_term t, kind_of_term 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 a022a07da..7c1d9f1c0 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -1,3 +1,4 @@ + (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 505d7dba5..e0aee15e6 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -144,26 +144,26 @@ let intern_proof_instr globs instr= (* INTERP *) let interp_justification_items sigma env = - Option.map (List.map (fun c ->understand sigma env (fst c))) + Option.map (List.map (fun c -> fst (*FIXME*)(understand sigma env (fst c)))) let interp_constr check_sort sigma env c = if check_sort then - understand sigma env ~expected_type:IsType (fst c) + fst (understand sigma env ~expected_type:IsType (fst c) (* FIXME *)) else - understand sigma env (fst c) + fst (understand sigma env (fst c)) let special_whd env = let infos=Closure.create_clos_infos Closure.betadeltaiota env in (fun t -> Closure.whd_val infos (Closure.inject t)) -let _eq = Globnames.constr_of_global (Coqlib.glob_eq) +let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq)) let decompose_eq env id = let typ = Environ.named_type id env in let whd = special_whd env typ in match kind_of_term whd with App (f,args)-> - if eq_constr f _eq && Int.equal (Array.length args) 3 + if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3 then args.(0) else error "Previous step is not an equality." | _ -> error "Previous step is not an equality." @@ -173,7 +173,7 @@ let get_eq_typ info env = typ let interp_constr_in_type typ sigma env c = - understand sigma env (fst c) ~expected_type:(OfType typ) + fst (understand sigma env (fst c) ~expected_type:(OfType typ))(*FIXME*) let interp_statement interp_it sigma env st = {st_label=st.st_label; @@ -213,7 +213,7 @@ let rec match_hyps blend names constr = function qhyp::rhyps,head let interp_hyps_gen inject blend sigma env hyps head = - let constr=understand sigma env (glob_constr_of_hyps inject hyps head) in + let constr= fst(*FIXME*) (understand sigma env (glob_constr_of_hyps inject hyps head)) in match_hyps blend [] constr hyps let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps glob_prop) @@ -246,7 +246,7 @@ let rec glob_of_pat = add_params (pred n) (GHole(Loc.ghost, Evar_kinds.TomatchTypeParameter(ind,n), None)::q) in let args = List.map glob_of_pat lpat in - glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr), + glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr,None), add_params mind.Declarations.mind_nparams args) let prod_one_hyp = function @@ -333,7 +333,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++ str "expected.") in let app_ind = - let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind) in + let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind,None) in let rparams = List.map detype_ground pinfo.per_params in let rparams_rec = List.map @@ -365,7 +365,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let term3=List.fold_right let_in_one_alias aliases term2 in let term4=List.fold_right prod_one_id loc_ids term3 in let term5=List.fold_right prod_one_hyp params term4 in - let constr = understand sigma env term5 in + let constr = fst (understand sigma env term5)(*FIXME*) in let tparams,nam4,rest4 = match_args destProd [] constr params in let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in @@ -409,7 +409,7 @@ let interp_suffices_clause sigma env (hyps,cot)= nenv,res let interp_casee sigma env = function - Real c -> Real (understand sigma env (fst c)) + Real c -> Real (fst (understand sigma env (fst c)))(*FIXME*) | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) sigma env cut) let abstract_one_arg = function @@ -425,7 +425,7 @@ let glob_constr_of_fun args body = List.fold_right abstract_one_arg args (fst body) let interp_fun sigma env args body = - let constr=understand sigma env (glob_constr_of_fun args body) in + let constr=fst (*FIXME*) (understand sigma env (glob_constr_of_fun args body)) in match_args destLambda [] constr args let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = function @@ -448,7 +448,7 @@ let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = fu let tparams,tpat,thyps = interp_cases info sigma env params pat hyps in Pcase (tparams,tpat,thyps) | Ptake witl -> - Ptake (List.map (fun c -> understand sigma env (fst c)) witl) + Ptake (List.map (fun c -> fst (*FIXME*) (understand sigma env (fst c))) witl) | Pconsider (c,hyps) -> Pconsider (interp_constr false sigma env c, interp_hyps sigma env hyps) | Pper (et,c) -> Pper (et,interp_casee sigma env c) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index de57330ec..8647ca676 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -292,13 +292,13 @@ let rec replace_in_list m l = function let enstack_subsubgoals env se stack gls= let hd,params = decompose_app (special_whd gls se.se_type) in match kind_of_term hd with - Ind ind when is_good_inductive env ind -> + Ind (ind,u as indu) when is_good_inductive env ind -> (* MS: FIXME *) let mib,oib= Inductive.lookup_mind_specif env ind in let gentypes= - Inductive.arities_of_constructors ind (mib,oib) in + Inductive.arities_of_constructors indu (mib,oib) in let process i gentyp = - let constructor = mkConstruct(ind,succ i) + let constructor = mkConstructU ((ind,succ i),u) (* constructors numbering*) in let appterm = applist (constructor,params) in let apptype = prod_applist gentyp params in @@ -357,7 +357,7 @@ let find_subsubgoal c ctyp skip submetas gls = try let unifier = Unification.w_unify env se.se_evd Reduction.CUMUL - ~flags:Unification.elim_flags ctyp se.se_type in + ~flags:(Unification.elim_flags ()) ctyp se.se_type in if n <= 0 then {se with se_evd=meta_assign se.se_meta @@ -488,14 +488,14 @@ let instr_cut mkstat _thus _then cut gls0 = (* iterated equality *) -let _eq = Globnames.constr_of_global (Coqlib.glob_eq) +let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq)) let decompose_eq id gls = let typ = pf_get_hyp_typ gls id in let whd = (special_whd gls typ) in match kind_of_term whd with App (f,args)-> - if eq_constr f _eq && Int.equal (Array.length args) 3 + if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3 then (args.(0), args.(1), args.(2)) @@ -530,14 +530,14 @@ let instr_rew _thus rew_side cut gls0 = else tclIDTAC gls in match rew_side with Lhs -> - let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in + let new_eq = mkApp(Lazy.force _eq,[|typ;cut.cut_stat.st_it;rhs|]) in tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq)) [tclTHEN tcl_erase_info (tclTHENS (Proofview.V82.of_tactic (transitivity lhs)) [just_tac;exact_check (mkVar last_id)]); thus_tac new_eq] gls0 | Rhs -> - let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in + let new_eq = mkApp(Lazy.force _eq,[|typ;lhs;cut.cut_stat.st_it|]) in tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq)) [tclTHEN tcl_erase_info (tclTHENS (Proofview.V82.of_tactic (transitivity rhs)) @@ -663,11 +663,11 @@ let conjunction_arity id gls = let hd,params = decompose_app (special_whd gls typ) in let env =pf_env gls in match kind_of_term hd with - Ind ind when is_good_inductive env ind -> + Ind (ind,u as indu) when is_good_inductive env ind -> let mib,oib= Inductive.lookup_mind_specif env ind in let gentypes= - Inductive.arities_of_constructors ind (mib,oib) in + Inductive.arities_of_constructors indu (mib,oib) in let _ = if not (Int.equal (Array.length gentypes) 1) then raise Not_found in let apptype = prod_applist gentypes.(0) params in let rc,_ = Reduction.dest_prod env apptype in @@ -832,7 +832,7 @@ let build_per_info etype casee gls = let ctyp=pf_type_of gls casee in let is_dep = dependent casee concl in let hd,args = decompose_app (special_whd gls ctyp) in - let ind = + let (ind,u as indu) = try destInd hd with DestKO -> @@ -1031,7 +1031,7 @@ let rec st_assoc id = function let thesis_for obj typ per_info env= let rc,hd1=decompose_prod typ in let cind,all_args=decompose_app typ in - let ind = destInd cind in + let ind,u = destInd cind in let _ = if not (eq_ind ind per_info.per_ind) then errorlabstrm "thesis_for" ((Printer.pr_constr_env env obj) ++ spc () ++ @@ -1166,7 +1166,7 @@ let hrec_for fix_id per_info gls obj_id = let typ=pf_get_hyp_typ gls obj_id in let rc,hd1=decompose_prod typ in let cind,all_args=decompose_app typ in - let ind = destInd cind in assert (eq_ind ind per_info.per_ind); + let ind,u = destInd cind in assert (eq_ind ind per_info.per_ind); let params,args= List.chop per_info.per_nparams all_args in assert begin try List.for_all2 eq_constr params per_info.per_params with @@ -1205,7 +1205,8 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let env=pf_env gls in let ctyp=pf_type_of gls casee in let hd,all_args = decompose_app (special_whd gls ctyp) in - let _ = assert (eq_ind (destInd hd) ind) in (* just in case *) + let ind', u = destInd hd in + let _ = assert (eq_ind ind' ind) in (* just in case *) let params,real_args = List.chop nparams all_args in let abstract_obj c body = let typ=pf_type_of gls c in @@ -1213,7 +1214,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let elim_pred = List.fold_right abstract_obj real_args (lambda_create env (ctyp,subst_term casee concl)) in let case_info = Inductiveops.make_case_info env ind RegularStyle in - let gen_arities = Inductive.arities_of_constructors ind spec in + let gen_arities = Inductive.arities_of_constructors (ind,u) spec in let f_ids typ = let sign = (prod_assum (prod_applist typ params)) in diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 7c9ef3c2a..36abb86cc 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -176,7 +176,7 @@ GLOBAL: proof_instr; statement : [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c} | i=ident -> {st_label=Anonymous; - st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i))} + st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i), None)} | c=constr -> {st_label=Anonymous;st_it=c} ]]; constr_or_thesis : @@ -189,7 +189,7 @@ GLOBAL: proof_instr; | [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot} | i=ident -> {st_label=Anonymous; - st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i)))} + st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i), None))} | c=constr -> {st_label=Anonymous;st_it=This c} ] ]; diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 791294902..74de31368 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -131,7 +131,7 @@ end exception Impossible let check_arity env cb = - let t = Typeops.type_of_constant_type env cb.const_type in + let t = cb.const_type in if Reduction.is_arity env t then raise Impossible let check_fix env cb i = diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 3927ad328..5b79f6d78 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -203,27 +203,28 @@ let oib_equal o1 o2 = Id.equal o1.mind_typename o2.mind_typename && List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt && begin match o1.mind_arity, o2.mind_arity with - | Monomorphic {mind_user_arity=c1; mind_sort=s1}, - Monomorphic {mind_user_arity=c2; mind_sort=s2} -> + (* | Monomorphic {mind_user_arity=c1; mind_sort=s1}, *) + (* Monomorphic {mind_user_arity=c2; mind_sort=s2} -> *) + (* eq_constr c1 c2 && Sorts.equal s1 s2 *) + (* | ma1, ma2 -> Pervasives.(=) ma1 ma2 (\** FIXME: this one is surely wrong *\) end && *) + (* Array.equal Id.equal o1.mind_consnames o2.mind_consnames *) + | {mind_user_arity=c1; mind_sort=s1}, + {mind_user_arity=c2; mind_sort=s2} -> eq_constr c1 c2 && Sorts.equal s1 s2 - | Polymorphic p1, Polymorphic p2 -> - let eq o1 o2 = Option.equal Univ.Universe.equal o1 o2 in - List.equal eq p1.poly_param_levels p2.poly_param_levels && - Univ.Universe.equal p1.poly_level p2.poly_level - | Monomorphic _, Polymorphic _ | Polymorphic _, Monomorphic _ -> false end && Array.equal Id.equal o1.mind_consnames o2.mind_consnames let mib_equal m1 m2 = Array.equal oib_equal m1.mind_packets m1.mind_packets && - (m1.mind_record : bool) == m2.mind_record && + (m1.mind_record) = m2.mind_record && (*FIXME*) (m1.mind_finite : bool) == m2.mind_finite && Int.equal m1.mind_ntypes m2.mind_ntypes && List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps && Int.equal m1.mind_nparams m2.mind_nparams && Int.equal m1.mind_nparams_rec m2.mind_nparams_rec && List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt && - Univ.eq_constraint m1.mind_constraints m2.mind_constraints + Pervasives.(=) m1.mind_universes m2.mind_universes (** FIXME *) + (* m1.mind_universes = m2.mind_universes *) (*S Extraction of a type. *) @@ -278,10 +279,10 @@ let rec extract_type env db j c args = if n > List.length db then Tunknown else let n' = List.nth db (n-1) in if Int.equal n' 0 then Tunknown else Tvar n') - | Const kn -> + | Const (kn,u as c) -> let r = ConstRef kn in let cb = lookup_constant kn env in - let typ = Typeops.type_of_constant_type env cb.const_type in + let typ,_ = Typeops.type_of_constant env c in (match flag_of_type env typ with | (Logic,_) -> assert false (* Cf. logical cases above *) | (Info, TypeScheme) -> @@ -306,7 +307,7 @@ let rec extract_type env db j c args = (* We try to reduce. *) let newc = applist (Mod_subst.force_constr lbody, args) in extract_type env db j newc [])) - | Ind (kn,i) -> + | Ind ((kn,i),u) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in extract_type_app env db (IndRef (kn,i),s) args | Case _ | Fix _ | CoFix _ -> Tunknown @@ -388,8 +389,10 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let packets = Array.mapi (fun i mip -> - let ar = Inductive.type_of_inductive env (mib,mip) in - let info = (fst (flag_of_type env ar) == Info) in + let (ind,u), ctx = + Universes.fresh_inductive_instance env (kn,i) in + let ar = Inductive.type_of_inductive env ((mib,mip),u) in + let info = (fst (flag_of_type env ar) = Info) in let s,v = if info then type_sign_vl env ar else [],[] in let t = Array.make (Array.length mip.mind_nf_lc) [] in { ip_typename = mip.mind_typename; @@ -397,21 +400,21 @@ and extract_ind env kn = (* kn is supposed to be in long form *) ip_logical = not info; ip_sign = s; ip_vars = v; - ip_types = t }) + ip_types = t }, u) mib.mind_packets in add_ind kn mib {ind_kind = Standard; ind_nparams = npar; - ind_packets = packets; + ind_packets = Array.map fst packets; ind_equiv = equiv }; (* Second pass: we extract constructors *) for i = 0 to mib.mind_ntypes - 1 do - let p = packets.(i) in + let p,u = packets.(i) in if not p.ip_logical then - let types = arities_of_constructors env (kn,i) in + let types = arities_of_constructors env ((kn,i),u) in for j = 0 to Array.length types - 1 do let t = snd (decompose_prod_n npar types.(j)) in let prods,head = dest_prod epar t in @@ -433,7 +436,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) if is_custom r then raise (I Standard); if not mib.mind_finite then raise (I Coinductive); if not (Int.equal mib.mind_ntypes 1) then raise (I Standard); - let p = packets.(0) in + let p,u = packets.(0) in if p.ip_logical then raise (I Standard); if not (Int.equal (Array.length p.ip_types) 1) then raise (I Standard); let typ = p.ip_types.(0) in @@ -442,7 +445,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l)) then raise (I Singleton); if List.is_empty l then raise (I Standard); - if not mib.mind_record then raise (I Standard); + if Option.is_empty mib.mind_record then raise (I Standard); (* Now we're sure it's a record. *) (* First, we find its field names. *) let rec names_prod t = match kind_of_term t with @@ -476,7 +479,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) (* If so, we use this information. *) begin try let n = nb_default_params env - (Inductive.type_of_inductive env (mib,mip0)) + (Inductive.type_of_inductive env ((mib,mip0),u)) in let check_proj kn = if Cset.mem kn !projs then add_projection n kn in List.iter (Option.iter check_proj) (lookup_projections ip) @@ -487,7 +490,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) in let i = {ind_kind = ind_info; ind_nparams = npar; - ind_packets = packets; + ind_packets = Array.map fst packets; ind_equiv = equiv } in add_ind kn mib i; @@ -522,7 +525,7 @@ and mlt_env env r = match r with | _ -> None with Not_found -> let cb = Environ.lookup_constant kn env in - let typ = Typeops.type_of_constant_type env cb.const_type in + let typ = cb.const_type (* FIXME not sure if we should instantiate univs here *) in match cb.const_body with | Undef _ | OpaqueDef _ -> None | Def l_body -> @@ -550,7 +553,7 @@ let record_constant_type env kn opt_typ = lookup_type kn with Not_found -> let typ = match opt_typ with - | None -> Typeops.type_of_constant env kn + | None -> (lookup_constant kn env).const_type | Some typ -> typ in let mlt = extract_type env [] 1 typ [] in let schema = (type_maxvar mlt, mlt) @@ -605,10 +608,12 @@ let rec extract_term env mle mlt c args = with NotDefault d -> let mle' = Mlenv.push_std_type mle (Tdummy d) in ast_pop (extract_term env' mle' mlt c2 args')) - | Const kn -> - extract_cst_app env mle mlt kn args - | Construct cp -> - extract_cons_app env mle mlt cp args + | Const (kn,u) -> + extract_cst_app env mle mlt kn u args + | Construct (cp,u) -> + extract_cons_app env mle mlt cp u args + | Proj (p, c) -> + extract_cst_app env mle mlt p Univ.Instance.empty (c :: args) | Rel n -> (* As soon as the expected [mlt] for the head is known, *) (* we unify it with an fresh copy of the stored type of [Rel n]. *) @@ -656,7 +661,7 @@ and make_mlargs env e s args typs = (*s Extraction of a constant applied to arguments. *) -and extract_cst_app env mle mlt kn args = +and extract_cst_app env mle mlt kn u args = (* First, the [ml_schema] of the constant, in expanded version. *) let nb,t = record_constant_type env kn None in let schema = nb, expand env t in @@ -729,7 +734,7 @@ and extract_cst_app env mle mlt kn args = they are fixed, and thus are not used for the computation. \end{itemize} *) -and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = +and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args = (* First, we build the type of the constructor, stored in small pieces. *) let mi = extract_ind env kn in let params_nb = mi.ind_nparams in @@ -971,7 +976,7 @@ let extract_fixpoint env vkn (fi,ti,ci) = let extract_constant env kn cb = let r = ConstRef kn in - let typ = Typeops.type_of_constant_type env cb.const_type in + let typ = cb.const_type in let warn_info () = if not (is_custom r) then add_info_axiom r in let warn_log () = if not (constant_has_body cb) then add_log_axiom r in @@ -1018,7 +1023,7 @@ let extract_constant env kn cb = let extract_constant_spec env kn cb = let r = ConstRef kn in - let typ = Typeops.type_of_constant_type env cb.const_type in + let typ = cb.const_type in match flag_of_type env typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) | (Logic, Default) -> Sval (r, Tdummy Kother) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index ba21c6cbf..133f4ada9 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -645,7 +645,7 @@ let implicits_of_global r = try Refmap'.find r !implicits_table with Not_found -> [] let add_implicits r l = - let typ = Global.type_of_global r in + let typ = Global.type_of_global_unsafe r in let rels,_ = decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in let names = List.rev_map fst rels in @@ -816,7 +816,7 @@ let extract_constant_inline inline r ids s = match g with | ConstRef kn -> let env = Global.env () in - let typ = Typeops.type_of_constant env kn in + let typ = (Environ.lookup_constant kn env).const_type in let typ = Reduction.whd_betadeltaiota env typ in if Reduction.is_arity env typ then begin diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 03a832e90..430b549d9 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -43,7 +43,7 @@ let rec nb_prod_after n c= | _ -> 0 let construct_nhyps ind gls = - let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in + let nparams = (fst (Global.lookup_inductive (fst ind))).mind_nparams in let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in let hyp = nb_prod_after nparams in Array.map hyp constr_types @@ -67,10 +67,10 @@ let special_whd gl= type kind_of_formula= Arrow of constr*constr - | False of inductive*constr list - | And of inductive*constr list*bool - | Or of inductive*constr list*bool - | Exists of inductive*constr list + | False of pinductive*constr list + | And of pinductive*constr list*bool + | Or of pinductive*constr list*bool + | Exists of pinductive*constr list | Forall of constr*constr | Atom of constr @@ -85,11 +85,11 @@ let kind_of_formula gl term = |_-> match match_with_nodep_ind cciterm with Some (i,l,n)-> - let ind=destInd i in + let ind,u=destInd i in let (mib,mip) = Global.lookup_inductive ind in let nconstr=Array.length mip.mind_consnames in if Int.equal nconstr 0 then - False(ind,l) + False((ind,u),l) else let has_realargs=(n>0) in let is_trivial= @@ -102,9 +102,9 @@ let kind_of_formula gl term = Atom cciterm else if Int.equal nconstr 1 then - And(ind,l,is_trivial) + And((ind,u),l,is_trivial) else - Or(ind,l,is_trivial) + Or((ind,u),l,is_trivial) | _ -> match match_with_sigma_type cciterm with Some (i,l)-> Exists((destInd i),l) @@ -186,19 +186,19 @@ type right_pattern = type left_arrow_pattern= LLatom - | LLfalse of inductive*constr list - | LLand of inductive*constr list - | LLor of inductive*constr list + | LLfalse of pinductive*constr list + | LLand of pinductive*constr list + | LLor of pinductive*constr list | LLforall of constr - | LLexists of inductive*constr list + | LLexists of pinductive*constr list | LLarrow of constr*constr*constr type left_pattern= Lfalse - | Land of inductive - | Lor of inductive + | Land of pinductive + | Lor of pinductive | Lforall of metavariable*constr*bool - | Lexists of inductive + | Lexists of pinductive | LA of constr*left_arrow_pattern type t={id:global_reference; diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 59b363393..d12b106cc 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -25,9 +25,9 @@ type ('a,'b) sum = Left of 'a | Right of 'b type counter = bool -> metavariable -val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array +val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array -val ind_hyps : int -> inductive -> constr list -> +val ind_hyps : int -> pinductive -> constr list -> Proof_type.goal Tacmach.sigma -> rel_context array type atoms = {positive:constr list;negative:constr list} @@ -49,19 +49,19 @@ type right_pattern = type left_arrow_pattern= LLatom - | LLfalse of inductive*constr list - | LLand of inductive*constr list - | LLor of inductive*constr list + | LLfalse of pinductive*constr list + | LLand of pinductive*constr list + | LLor of pinductive*constr list | LLforall of constr - | LLexists of inductive*constr list + | LLexists of pinductive*constr list | LLarrow of constr*constr*constr type left_pattern= Lfalse - | Land of inductive - | Lor of inductive + | Land of pinductive + | Lor of pinductive | Lforall of metavariable*constr*bool - | Lexists of inductive + | Lexists of pinductive | LA of constr*left_arrow_pattern type t={id: global_reference; diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 6c1709140..e0f4fa95f 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -18,7 +18,7 @@ let update_flags ()= let predref=ref Names.Cpred.empty in let f coe= try - let kn=destConst (Classops.get_coercion_value coe) in + let kn= fst (destConst (Classops.get_coercion_value coe)) in predref:=Names.Cpred.add kn !predref with DestKO -> () in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index fe22708a0..c6db6a49f 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -101,6 +101,8 @@ let dummy_constr=mkMeta (-1) let dummy_bvid=Id.of_string "x" +let constr_of_global = Universes.constr_of_global + let mk_open_instance id gl m t= let env=pf_env gl in let evmap=Refiner.project gl in @@ -128,7 +130,7 @@ let mk_open_instance id gl m t= GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,None),t1) | _-> anomaly (Pp.str "can't happen") in let ntt=try - Pretyping.understand evmap env (raux m rawt) + fst (Pretyping.understand evmap env (raux m rawt))(*FIXME*) with e when Errors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in decompose_lam_n_assum m ntt diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 6d9af2bbf..31a1e6cb0 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -53,7 +53,7 @@ let clear_global=function VarRef id->clear [id] | _->tclIDTAC - +let constr_of_global = Universes.constr_of_global (* connection rules *) let axiom_tac t seq= @@ -117,14 +117,14 @@ let left_false_tac id= (* We use this function for false, and, or, exists *) -let ll_ind_tac ind largs backtrack id continue seq gl= - let rcs=ind_hyps 0 ind largs gl in +let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl= + let rcs=ind_hyps 0 indu largs gl in let vargs=Array.of_list largs in (* construire le terme H->B, le generaliser etc *) let myterm i= let rc=rcs.(i) in let p=List.length rc in - let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in + let cstr=mkApp ((mkConstructU ((ind,(i+1)),u)),vargs) in let vars=Array.init p (fun j->mkRel (p-j)) in let capply=mkApp ((lift p cstr),vars) in let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in @@ -204,8 +204,8 @@ let ll_forall_tac prod backtrack id continue seq= let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str let defined_connectives=lazy - [AllOccurrences,EvalConstRef (destConst (constant "not")); - AllOccurrences,EvalConstRef (destConst (constant "iff"))] + [AllOccurrences,EvalConstRef (fst (destConst (constant "not"))); + AllOccurrences,EvalConstRef (fst (destConst (constant "iff")))] let normalize_evaluables= onAllHypsAndConcl diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index bfebbaaf8..180f6f5da 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -33,19 +33,19 @@ val or_tac : seqtac with_backtracking val arrow_tac : seqtac with_backtracking -val left_and_tac : inductive -> lseqtac with_backtracking +val left_and_tac : pinductive -> lseqtac with_backtracking -val left_or_tac : inductive -> lseqtac with_backtracking +val left_or_tac : pinductive -> lseqtac with_backtracking val left_false_tac : global_reference -> tactic -val ll_ind_tac : inductive -> constr list -> lseqtac with_backtracking +val ll_ind_tac : pinductive -> constr list -> lseqtac with_backtracking val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking val forall_tac : seqtac with_backtracking -val left_exists_tac : inductive -> lseqtac with_backtracking +val left_exists_tac : pinductive -> lseqtac with_backtracking val ll_forall_tac : types -> lseqtac with_backtracking diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 72bde18f4..c0e5c7e58 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -199,7 +199,7 @@ let expand_constructor_hints = 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 c=Universes.constr_of_global gr in let typ=(pf_type_of gl c) in add_formula Hyp gr typ seq gl in List.fold_right f l seq @@ -210,10 +210,10 @@ 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->()) diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 2556460f5..f7ee9fdad 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -78,7 +78,7 @@ let unif t1 t2= for i=0 to l-1 do Queue.add (va.(i),vb.(i)) bige done - | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2)) + | _->if not (eq_constr_nounivs nt1 nt2) then raise (UFAIL (nt1,nt2)) done; assert false (* this place is unreachable but needed for the sake of typing *) diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index aeb07fc3a..d34d50364 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -87,7 +87,7 @@ let string_of_R_constant kn = let rec string_of_R_constr c = match kind_of_term c with Cast (c,_,_) -> string_of_R_constr c - |Const c -> string_of_R_constant c + |Const (c,_) -> string_of_R_constant c | _ -> "not_of_constant" exception NoRational @@ -114,7 +114,7 @@ let rec rational_of_constr c = rminus (rational_of_constr args.(0)) (rational_of_constr args.(1)) | _ -> raise NoRational) - | Const kn -> + | Const (kn,_) -> (match (string_of_R_constant kn) with "R1" -> r1 |"R0" -> r0 @@ -160,7 +160,7 @@ let rec flin_of_constr c = with NoRational -> flin_add (flin_zero()) args.(0) (rinv b)) |_-> raise NoLinear) - | Const c -> + | Const (c,_) -> (match (string_of_R_constant c) with "R1" -> flin_one () |"R0" -> flin_zero () @@ -194,7 +194,7 @@ let ineq1_of_constr (h,t) = match (kind_of_term t) with | App (f,args) -> (match kind_of_term f with - | Const c when Array.length args = 2 -> + | Const (c,_) when Array.length args = 2 -> let t1= args.(0) in let t2= args.(1) in (match (string_of_R_constant c) with @@ -227,13 +227,13 @@ let ineq1_of_constr (h,t) = (flin_of_constr t1); hstrict=false}] |_-> raise NoIneq) - | Ind (kn,i) -> + | Ind ((kn,i),_) -> if not (eq_gr (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq; let t0= args.(0) in let t1= args.(1) in let t2= args.(2) in (match (kind_of_term t0) with - | Const c -> + | Const (c,_) -> (match (string_of_R_constant c) with | "R"-> [{hname=h; @@ -609,8 +609,9 @@ let rec fourier gl= [tclORELSE (* TODO : Ring.polynom []*) tclIDTAC tclIDTAC; - (tclTHEN (apply (get coq_sym_eqT)) - (apply (get coq_Rinv_1)))] + pf_constr_of_global (get coq_sym_eqT) (fun symeq -> + (tclTHEN (apply symeq) + (apply (get coq_Rinv_1))))] ) ])); diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f06d8fa53..a3af23dcd 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -124,11 +124,13 @@ let finish_proof dynamic_infos g = let refine c = - Tacmach.refine_no_check c + Tacmach.refine c let thin l = Tacmach.thin_no_check l +let eq_constr u v = eq_constr_nounivs u v + let is_trivial_eq t = let res = try begin @@ -205,7 +207,7 @@ let prove_trivial_eq h_id context (constructor,type_of_term,term) = let find_rectype env c = - let (t, l) = decompose_app (Reduction.whd_betaiotazeta c) in + let (t, l) = decompose_app (Reduction.whd_betaiotazeta env c) in match kind_of_term t with | Ind ind -> (t, l) | Construct _ -> (t,l) @@ -233,7 +235,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = failwith "NoChange"; end in - let eq_constr = Reductionops.is_conv env sigma in + let eq_constr = Evarconv.e_conv env (ref sigma) in if not (noccurn 1 end_of_type) then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *) if not (isApp t) then nochange "not an equality"; @@ -325,7 +327,8 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = let all_ids = pf_ids_of_hyps g in let new_ids,_ = list_chop ctxt_size all_ids in let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in - refine to_refine g + let evm, _ = pf_apply Typing.e_type_of g to_refine in + tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g ) in let simpl_eq_tac = @@ -633,8 +636,11 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = ( (* we instanciate the hyp if possible *) fun g -> let prov_hid = pf_get_new_id hid g in + let c = mkApp(mkVar hid,args) in + let evm, _ = pf_apply Typing.e_type_of g c in tclTHENLIST[ - Proofview.V82.of_tactic (pose_proof (Name prov_hid) (mkApp(mkVar hid,args))); + Refiner.tclEVARS evm; + Proofview.V82.of_tactic (pose_proof (Name prov_hid) c); thin [hid]; rename_hyp [prov_hid,hid] ] g @@ -757,6 +763,7 @@ let build_proof begin match kind_of_term f with | App _ -> assert false (* we have collected all the app in decompose_app *) + | Proj _ -> assert false (*FIXME*) | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ -> let new_infos = { dyn_infos with @@ -764,7 +771,7 @@ let build_proof } in build_proof_args do_finalize new_infos g - | Const c when not (List.mem_f Constant.equal c fnames) -> + | Const (c,_) when not (List.mem_f Constant.equal c fnames) -> let new_infos = { dyn_infos with info = (f,args) @@ -809,6 +816,7 @@ let build_proof | Fix _ | CoFix _ -> error ( "Anonymous local (co)fixpoints are not handled yet") + | Proj _ -> error "Prod" | Prod _ -> error "Prod" | LetIn _ -> let new_infos = @@ -938,7 +946,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (* observe (str "nb_args := " ++ str (string_of_int nb_args)); *) (* observe (str "nb_params := " ++ str (string_of_int nb_params)); *) (* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *) - let f_def = Global.lookup_constant (destConst f) in + let f_def = Global.lookup_constant (fst (destConst f)) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in let f_body = Option.get (body_of_constant f_def) in @@ -956,10 +964,10 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args) - (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in + ((*FIXME*)f_def.const_type) in let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in - let f_id = Label.to_id (con_label (destConst f)) in + let f_id = Label.to_id (con_label (fst (destConst f))) in let prove_replacement = tclTHENSEQ [ @@ -978,8 +986,8 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = Ensures by: obvious i*) (mk_equation_id f_id) - (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) - lemma_type + (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) + (lemma_type, (*FIXME*) Univ.ContextSet.empty) (fun _ _ -> ()); ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); Lemmas.save_proof (Vernacexpr.Proved(false,None)) @@ -990,10 +998,10 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = let equation_lemma = try - let finfos = find_Function_infos (destConst f) in + let finfos = find_Function_infos (fst (destConst f)) (*FIXME*) in mkConst (Option.get finfos.equation_lemma) with (Not_found | Option.IsNone as e) -> - let f_id = Label.to_id (con_label (destConst f)) in + let f_id = Label.to_id (con_label (fst (destConst f))) in (*i The next call to mk_equation_id is valid since we will construct the lemma Ensures by: obvious i*) @@ -1002,7 +1010,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = let _ = match e with | Option.IsNone -> - let finfos = find_Function_infos (destConst f) in + let finfos = find_Function_infos (fst (destConst f)) in update_Function {finfos with equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with @@ -1306,7 +1314,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in tclTHENSEQ - [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef fname)]; + [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]; let do_prove = build_proof interactive_proof diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d6f21fb86..2adc82505 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -106,14 +106,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in let is_dom c = match kind_of_term c with - | Ind((u,_)) -> MutInd.equal u rel_as_kn - | Construct((u,_),_) -> MutInd.equal u rel_as_kn + | Ind((u,_),_) -> MutInd.equal u rel_as_kn + | Construct(((u,_),_),_) -> MutInd.equal u rel_as_kn | _ -> false in let get_fun_num c = match kind_of_term c with - | Ind(_,num) -> num - | Construct((_,num),_) -> num + | Ind((_,num),_) -> num + | Construct(((_,num),_),_) -> num | _ -> assert false in let dummy_var = mkVar (Id.of_string "________") in @@ -251,8 +251,10 @@ let change_property_sort toSort princ princName = let princ_info = compute_elim_sig princ in let change_sort_in_predicate (x,v,t) = (x,None, - let args,_ = decompose_prod t in - compose_prod args (mkSort toSort) + let args,ty = decompose_prod t in + let s = destSort ty in + Global.add_constraints (Univ.enforce_leq (univ_of_sort toSort) (univ_of_sort s) Univ.Constraint.empty); + compose_prod args (mkSort toSort) ) in let princName_as_constr = Constrintern.global_reference princName in @@ -292,8 +294,8 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro begin Lemmas.start_proof new_princ_name - (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) - new_principle_type + (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) + (new_principle_type, (*FIXME*) Univ.ContextSet.empty) hook ; (* let _tim1 = System.get_time () in *) @@ -315,7 +317,7 @@ let generate_functional_principle try let f = funs.(i) in - let type_sort = Termops.new_sort_in_family InType in + let type_sort = Universes.new_sort_in_family InType in let new_sorts = match sorts with | None -> Array.make (Array.length funs) (type_sort) @@ -334,18 +336,23 @@ let generate_functional_principle then (* let id_of_f = Label.to_id (con_label f) in *) let register_with_sort fam_sort = - let s = Termops.new_sort_in_family fam_sort in + let s = Universes.new_sort_in_family fam_sort in let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in let value = change_property_sort s new_principle_type new_princ_name in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = { - const_entry_body = Future.from_val (value,Declareops.no_seff); - const_entry_secctx = None; - const_entry_type = None; - const_entry_opaque = false; - const_entry_inline_code = false; - const_entry_feedback = None; - } in + let ce = + { const_entry_body = + Future.from_val (value,Declareops.no_seff); + const_entry_secctx = None; + const_entry_type = None; + const_entry_polymorphic = false; + const_entry_universes = Univ.UContext.empty (*FIXME*); + const_entry_proj = None; + const_entry_opaque = false; + const_entry_feedback = None; + const_entry_inline_code = false + } + in ignore( Declare.declare_constant name @@ -488,19 +495,20 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis List.map (fun (idx) -> let ind = first_fun_kn,idx in - ind,true,prop_sort + (ind,Univ.Instance.empty)(*FIXME*),true,prop_sort ) funs_indexes in + let sigma, schemes = + Indrec.build_mutual_induction_scheme env sigma ind_list + in let l_schemes = - List.map - (Typing.type_of env sigma) - (Indrec.build_mutual_induction_scheme env sigma ind_list) + List.map (Typing.type_of env sigma) schemes in let i = ref (-1) in let sorts = List.rev_map (fun (_,x) -> - Termops.new_sort_in_family (Pretyping.interp_elimination_sort x) + Universes.new_sort_in_family (Pretyping.interp_elimination_sort x) ) fas in @@ -649,10 +657,10 @@ let build_case_scheme fa = (* Constrintern.global_reference id *) (* in *) let funs = (fun (_,f,_) -> - try Globnames.constr_of_global (Nametab.global f) + try Universes.constr_of_global (Nametab.global f) with Not_found -> Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in - let first_fun = destConst funs in + let first_fun,u = destConst funs in let funs_mp,funs_dp,_ = Names.repr_con first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in @@ -664,16 +672,18 @@ let build_case_scheme fa = let prop_sort = InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in - List.assoc_f Constant.equal (destConst funs) this_block_funs_indexes + List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes in let ind_fun = let ind = first_fun_kn,funs_indexes in - ind,prop_sort + (ind,Univ.Instance.empty)(*FIXME*),prop_sort in - let scheme_type = (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun) in + let sigma, scheme = + (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun in + let scheme_type = (Typing.type_of env sigma ) scheme in let sorts = (fun (_,_,x) -> - Termops.new_sort_in_family (Pretyping.interp_elimination_sort x) + Universes.new_sort_in_family (Pretyping.interp_elimination_sort x) ) fa in @@ -690,6 +700,6 @@ let build_case_scheme fa = (Some princ_name) this_block_funs 0 - (prove_princ_for_struct false 0 [|destConst funs|]) + (prove_princ_for_struct false 0 [|fst (destConst funs)|]) in () diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 2dd78d890..3802aa365 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -307,8 +307,11 @@ let rec hdMatchSub inu (test: constr -> bool) : fapp_info list = max_rel = max_rel; onlyvars = List.for_all isVar args } ::subres +let make_eq () = +(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ()) + let mkEq typ c1 c2 = - mkApp (Coqlib.build_coq_eq(),[| typ; c1; c2|]) + mkApp (make_eq(),[| typ; c1; c2|]) let poseq_unsafe idunsafe cstr gl = @@ -463,10 +466,10 @@ VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")" "with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] -> [ - let f1 = Constrintern.interp_constr Evd.empty (Global.env()) - (CRef (Libnames.Ident (Loc.ghost,id1))) in - let f2 = Constrintern.interp_constr Evd.empty (Global.env()) - (CRef (Libnames.Ident (Loc.ghost,id2))) in + let f1,ctx = Constrintern.interp_constr Evd.empty (Global.env()) + (CRef (Libnames.Ident (Loc.ghost,id1),None)) in + let f2,ctx' = Constrintern.interp_constr Evd.empty (Global.env()) + (CRef (Libnames.Ident (Loc.ghost,id2),None)) in let f1type = Typing.type_of (Global.env()) Evd.empty f1 in let f2type = Typing.type_of (Global.env()) Evd.empty f2 in let ar1 = List.length (fst (decompose_prod f1type)) in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index dd02dfe8d..4544f736c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -333,8 +333,8 @@ let raw_push_named (na,raw_value,raw_typ) env = match na with | Anonymous -> env | Name id -> - let value = Option.map (Pretyping.understand Evd.empty env) raw_value in - let typ = Pretyping.understand Evd.empty env ~expected_type:Pretyping.IsType raw_typ in + let value = Option.map (fun x-> fst (Pretyping.understand Evd.empty env x)) raw_value in + let typ,ctx = Pretyping.understand Evd.empty env ~expected_type:Pretyping.IsType raw_typ in Environ.push_named (id,value,typ) env @@ -350,7 +350,7 @@ let add_pat_variables pat typ env : Environ.env = with Not_found -> assert false in let constructors = Inductiveops.get_constructors env indf in - let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c cs.Inductiveops.cs_cstr) (Array.to_list constructors) in + let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in List.fold_left2 add_pat_variables env patl (List.rev cs_args_types) in @@ -397,7 +397,7 @@ let rec pattern_to_term_and_type env typ = function with Not_found -> assert false in let constructors = Inductiveops.get_constructors env indf in - let constructor = List.find (fun cs -> eq_constructor cs.Inductiveops.cs_cstr constr) (Array.to_list constructors) in + let constructor = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in let _,cstl = Inductiveops.dest_ind_family indf in let csta = Array.of_list cstl in @@ -486,7 +486,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = a pseudo value "v1 ... vn". The "value" of this branch is then simply [res] *) - let rt_as_constr = Pretyping.understand Evd.empty env rt in + let rt_as_constr,ctx = Pretyping.understand Evd.empty env rt in let rt_typ = Typing.type_of env Evd.empty rt_as_constr in let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in let res = fresh_id args_res.to_avoid "_res" in @@ -559,6 +559,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) build_entry_lc env funnames avoid (mkGApp(b,args)) | GRec _ -> error "Not handled GRec" + | GProj _ -> error "Not handled GProj" | GProd _ -> error "Cannot apply a type" end (* end of the application treatement *) @@ -594,7 +595,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = and combine the two result *) let v_res = build_entry_lc env funnames avoid v in - let v_as_constr = Pretyping.understand Evd.empty env v in + let v_as_constr,ctx = Pretyping.understand Evd.empty env v in let v_type = Typing.type_of env Evd.empty v_as_constr in let new_env = match n with @@ -610,7 +611,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let make_discr = make_discr_match brl in build_entry_lc_from_case env funnames make_discr el brl avoid | GIf(_,b,(na,e_option),lhs,rhs) -> - let b_as_constr = Pretyping.understand Evd.empty env b in + let b_as_constr,ctx = Pretyping.understand Evd.empty env b in let b_typ = Typing.type_of env Evd.empty b_as_constr in let (ind,_) = try Inductiveops.find_inductive env Evd.empty b_typ @@ -619,7 +620,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = Printer.pr_glob_constr b ++ str " in " ++ Printer.pr_glob_constr rt ++ str ". try again with a cast") in - let case_pats = build_constructors_of_type ind [] in + let case_pats = build_constructors_of_type (fst ind) [] in assert (Int.equal (Array.length case_pats) 2); let brl = List.map_i @@ -642,7 +643,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = ) nal in - let b_as_constr = Pretyping.understand Evd.empty env b in + let b_as_constr,ctx = Pretyping.understand Evd.empty env b in let b_typ = Typing.type_of env Evd.empty b_as_constr in let (ind,_) = try Inductiveops.find_inductive env Evd.empty b_typ @@ -651,7 +652,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = Printer.pr_glob_constr b ++ str " in " ++ Printer.pr_glob_constr rt ++ str ". try again with a cast") in - let case_pats = build_constructors_of_type ind nal_as_glob_constr in + let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in assert (Int.equal (Array.length case_pats) 1); let br = (Loc.ghost,[],[case_pats.(0)],e) @@ -661,6 +662,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = end | GRec _ -> error "Not handled GRec" + | GProj _ -> error "Not handled GProj" | GCast(_,b,_) -> build_entry_lc env funnames avoid b and build_entry_lc_from_case env funname make_discr @@ -689,7 +691,7 @@ and build_entry_lc_from_case env funname make_discr in let types = List.map (fun (case_arg,_) -> - let case_arg_as_constr = Pretyping.understand Evd.empty env case_arg in + let case_arg_as_constr,ctx = Pretyping.understand Evd.empty env case_arg in Typing.type_of env Evd.empty case_arg_as_constr ) el in @@ -844,7 +846,7 @@ let is_res id = let same_raw_term rt1 rt2 = match rt1,rt2 with - | GRef(_,r1), GRef (_,r2) -> Globnames.eq_gr r1 r2 + | GRef(_,r1,_), GRef (_,r2,_) -> Globnames.eq_gr r1 r2 | GHole _, GHole _ -> true | _ -> false let decompose_raw_eq lhs rhs = @@ -894,7 +896,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let new_t = mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt]) in - let t' = Pretyping.understand Evd.empty env new_t in + let t',ctx = Pretyping.understand Evd.empty env new_t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -907,14 +909,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> (* the first args is the name of the function! *) assert false end - | GApp(loc1,GRef(loc2,eq_as_ref),[ty;GVar(loc3,id);rt]) + | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;GVar(loc3,id);rt]) when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin try observe (str "computing new type for eq : " ++ pr_glob_constr rt); let t' = - try Pretyping.understand Evd.empty env t + try fst (Pretyping.understand Evd.empty env t)(*FIXME*) with e when Errors.noncritical e -> raise Continue in let is_in_b = is_free_in id b in @@ -936,17 +938,17 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = in mkGProd(n,t,new_b),id_to_exclude with Continue -> - let jmeq = Globnames.IndRef (destInd (jmeq ())) in - let ty' = Pretyping.understand Evd.empty env ty in + let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in + let ty',ctx = Pretyping.understand Evd.empty env ty in let ind,args' = Inductive.find_inductive env ty' in - let mib,_ = Global.lookup_inductive ind in + let mib,_ = Global.lookup_inductive (fst ind) in let nparam = mib.Declarations.mind_nparams in let params,arg' = ((Util.List.chop nparam args')) in let rt_typ = GApp(Loc.ghost, - GRef (Loc.ghost,Globnames.IndRef ind), + GRef (Loc.ghost,Globnames.IndRef (fst ind),None), (List.map (fun p -> Detyping.detype false [] (Termops.names_of_rel_context env) @@ -956,10 +958,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (mkGHole ())))) in let eq' = - GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;rt]) + GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt]) in observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); - let eq'_as_constr = Pretyping.understand Evd.empty env eq' in + let eq'_as_constr,ctx = Pretyping.understand Evd.empty env eq' in observe (str " computing new type for jmeq : done") ; let new_args = match kind_of_term eq'_as_constr with @@ -1007,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = if is_in_b then b else replace_var_by_term id rt b in let new_env = - let t' = Pretyping.understand Evd.empty env eq' in + let t',ctx = Pretyping.understand Evd.empty env eq' in Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = @@ -1024,7 +1026,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGProd(n,t,new_b),id_to_exclude else new_b, Id.Set.add id id_to_exclude *) - | GApp(loc1,GRef(loc2,eq_as_ref),[ty;rt1;rt2]) + | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;rt1;rt2]) when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin @@ -1045,7 +1047,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = else raise Continue with Continue -> observe (str "computing new type for prod : " ++ pr_glob_constr rt); - let t' = Pretyping.understand Evd.empty env t in + let t',ctx = Pretyping.understand Evd.empty env t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1061,7 +1063,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = end | _ -> observe (str "computing new type for prod : " ++ pr_glob_constr rt); - let t' = Pretyping.understand Evd.empty env t in + let t',ctx = Pretyping.understand Evd.empty env t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1080,7 +1082,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in observe (str "computing new type for lambda : " ++ pr_glob_constr rt); - let t' = Pretyping.understand Evd.empty env t in + let t',ctx = Pretyping.understand Evd.empty env t in match n with | Name id -> let new_env = Environ.push_rel (n,None,t') env in @@ -1102,7 +1104,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | GLetIn(_,n,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in - let t' = Pretyping.understand Evd.empty env t in + let t',ctx = Pretyping.understand Evd.empty env t in let type_t' = Typing.type_of env Evd.empty t' in let new_env = Environ.push_rel (n,Some t',type_t') env in let new_b,id_to_exclude = @@ -1127,7 +1129,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = args (crossed_types) depth t in - let t' = Pretyping.understand Evd.empty env new_t in + let t',ctx = Pretyping.understand Evd.empty env new_t in let new_env = Environ.push_rel (na,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1179,7 +1181,7 @@ let rec compute_cst_params relnames params = function discriminitation ones *) | GSort _ -> params | GHole _ -> params - | GIf _ | GRec _ | GCast _ -> + | GIf _ | GRec _ | GCast _ | GProj _-> raise (UserError("compute_cst_params", str "Not handled case")) and compute_cst_params_from_app acc (params,rtl) = match params,rtl with @@ -1267,12 +1269,12 @@ let do_build_inductive (fun (n,t,is_defined) acc -> if is_defined then - Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t, + Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, acc) else Constrexpr.CProdN (Loc.ghost, - [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t], + [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], acc ) ) @@ -1285,7 +1287,8 @@ let do_build_inductive *) let rel_arities = Array.mapi rel_arity funsargs in Util.Array.fold_left2 (fun env rel_name rel_ar -> - Environ.push_named (rel_name,None, Constrintern.interp_constr Evd.empty env rel_ar) env) env relnames rel_arities + Environ.push_named (rel_name,None, + fst (with_full_print (Constrintern.interp_constr Evd.empty env) rel_ar)) env) env relnames rel_arities in (* and of the real constructors*) let constr i res = @@ -1333,12 +1336,12 @@ let do_build_inductive (fun (n,t,is_defined) acc -> if is_defined then - Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t, + Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, acc) else Constrexpr.CProdN (Loc.ghost, - [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t], + [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], acc ) ) @@ -1366,8 +1369,7 @@ let do_build_inductive Array.map (List.map (fun (id,t) -> false,((Loc.ghost,id), - Flags.with_option - Flags.raw_print + with_full_print (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) t) ) )) @@ -1403,7 +1405,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds)) true + with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false)) true with | UserError(s,msg) as e -> let _time3 = System.get_time () in diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 6a7f326e6..5efaf7954 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -10,7 +10,7 @@ open Misctypes Some basic functions to rebuild glob_constr In each of them the location is Loc.ghost *) -let mkGRef ref = GRef(Loc.ghost,ref) +let mkGRef ref = GRef(Loc.ghost,ref,None) let mkGVar id = GVar(Loc.ghost,id) let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl) let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b) @@ -180,6 +180,7 @@ let change_vars = | GRec _ -> error "Local (co)fixes are not supported" | GSort _ -> rt | GHole _ -> rt + | GProj _ -> error "Native projections are not supported" (** FIXME *) | GCast(loc,b,c) -> GCast(loc,change_vars mapping b, Miscops.map_cast_type (change_vars mapping) c) @@ -357,6 +358,7 @@ let rec alpha_rt excluded rt = alpha_rt excluded rhs ) | GRec _ -> error "Not handled GRec" + | GProj _ -> error "Native projections are not supported" (** FIXME *) | GSort _ -> rt | GHole _ -> rt | GCast (loc,b,c) -> @@ -407,6 +409,7 @@ let is_free_in id = | GIf(_,cond,_,br1,br2) -> is_free_in cond || is_free_in br1 || is_free_in br2 | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GProj _ -> error "Native projections are not supported" (** FIXME *) | GSort _ -> false | GHole _ -> false | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t @@ -503,6 +506,7 @@ let replace_var_by_term x_id term = replace_var_by_pattern rhs ) | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GProj _ -> error "Native projections are not supported" (** FIXME *) | GSort _ -> rt | GHole _ -> rt | GCast(loc,b,c) -> @@ -598,6 +602,7 @@ let ids_of_glob_constr c = | GCases (loc,sty,rtntypopt,tml,brchl) -> List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl) | GRec _ -> failwith "Fix inside a constructor branch" + | GProj _ -> error "Native projections are not supported" (** FIXME *) | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> [] in (* build the set *) @@ -656,6 +661,7 @@ let zeta_normalize = zeta_normalize_term rhs ) | GRec _ -> raise (UserError("",str "Not handled GRec")) + | GProj _ -> error "Native projections are not supported" (** FIXME *) | GSort _ -> rt | GHole _ -> rt | GCast(loc,b,c) -> @@ -698,6 +704,7 @@ let expand_as = GIf(loc,expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) | GRec _ -> error "Not handled GRec" + | GProj _ -> error "Native projections are not supported" (** FIXME *) | GCast(loc,b,c) -> GCast(loc,expand_as map b, Miscops.map_cast_type (expand_as map) c) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 661e5e486..d98f824e8 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -38,7 +38,7 @@ let functional_induction with_clean c princl pat = | None -> (* No principle is given let's find the good one *) begin match kind_of_term f with - | Const c' -> + | Const (c',u) -> let princ_option = let finfo = (* we first try to find out a graph on f *) try find_Function_infos c' @@ -148,7 +148,7 @@ let build_newrecursive List.fold_left (fun (env,impls) ((_,recname),bl,arityc,_) -> let arityc = Constrexpr_ops.prod_constr_expr arityc bl in - let arity = Constrintern.interp_type sigma env0 arityc in + let arity,ctx = Constrintern.interp_type sigma env0 arityc in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in (Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls)) (env0,Constrintern.empty_internalization_env) lnameargsardef in @@ -182,6 +182,7 @@ let is_rec names = | GVar(_,id) -> check_id id names | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false | GCast(_,b,_) -> lookup names b + | GProj _ -> error "GProj not handled" | GRec _ -> error "GRec not handled" | GIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) @@ -222,7 +223,7 @@ let derive_inversion fix_names = try (* we first transform the fix_names identifier into their corresponding constant *) let fix_names_as_constant = - List.map (fun id -> destConst (Constrintern.global_reference id)) fix_names + List.map (fun id -> fst (destConst (Constrintern.global_reference id))) fix_names in (* Then we check that the graphs have been defined @@ -239,7 +240,7 @@ let derive_inversion fix_names = Ensures by : register_built i*) (List.map - (fun id -> destInd (Constrintern.global_reference (mk_rel_id id))) + (fun id -> fst (destInd (Constrintern.global_reference (mk_rel_id id)))) fix_names ) with e when Errors.noncritical e -> @@ -326,9 +327,8 @@ let generate_principle on_error let _ = List.map_i (fun i x -> - let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in - let princ_type = Typeops.type_of_constant (Global.env()) princ - in + let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in + let princ_type = Global.type_of_global_unsafe princ in Functional_principles_types.generate_functional_principle interactive_proof princ_type @@ -351,10 +351,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp match fixpoint_exprl with | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in - Command.do_definition fname (Decl_kinds.Global,Decl_kinds.Definition) + Command.do_definition fname (Decl_kinds.Global,(*FIXME*)false,Decl_kinds.Definition) bl None body (Some ret_type) (fun _ _ -> ()) | _ -> - Command.do_fixpoint Global fixpoint_exprl + Command.do_fixpoint Global false(*FIXME*) fixpoint_exprl let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation @@ -385,7 +385,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas let f_app_args = Constrexpr.CAppExpl (Loc.ghost, - (None,(Ident (Loc.ghost,fname))) , + (None,(Ident (Loc.ghost,fname)),None) , (List.map (function | _,Anonymous -> assert false @@ -399,7 +399,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.prod_constr_expr unbounded_eq args in - let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type + let hook (f_ref,_) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type nb_args relation = try pre_hook @@ -536,7 +536,7 @@ let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),_) = Command.interp_fixpoint fixl ntns in + let ((_,_,typel),_,_) = Command.interp_fixpoint fixl ntns in let constr_expr_typel = with_full_print (List.map (Constrextern.extern_constr false (Global.env ()))) typel in let fixpoint_exprl_with_new_bl = @@ -631,10 +631,10 @@ let do_generate_principle on_error register_built interactive_proof let rec add_args id new_args b = match b with - | CRef r -> + | CRef (r,_) -> begin match r with | Libnames.Ident(loc,fname) when Id.equal fname id -> - CAppExpl(Loc.ghost,(None,r),new_args) + CAppExpl(Loc.ghost,(None,r,None),new_args) | _ -> b end | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo") @@ -648,12 +648,12 @@ let rec add_args id new_args b = add_args id new_args b1) | CLetIn(loc,na,b1,b2) -> CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2) - | CAppExpl(loc,(pf,r),exprl) -> + | CAppExpl(loc,(pf,r,us),exprl) -> begin match r with | Libnames.Ident(loc,fname) when Id.equal fname id -> - CAppExpl(loc,(pf,r),new_args@(List.map (add_args id new_args) exprl)) - | _ -> CAppExpl(loc,(pf,r),List.map (add_args id new_args) exprl) + CAppExpl(loc,(pf,r,us),new_args@(List.map (add_args id new_args) exprl)) + | _ -> CAppExpl(loc,(pf,r,us),List.map (add_args id new_args) exprl) end | CApp(loc,(pf,b),bl) -> CApp(loc,(pf,add_args id new_args b), @@ -767,11 +767,10 @@ let make_graph (f_ref:global_reference) = | Some body -> let env = Global.env () in let extern_body,extern_type = - with_full_print - (fun () -> + with_full_print (fun () -> (Constrextern.extern_constr false env body, Constrextern.extern_type false env - (Typeops.type_of_constant_type env c_body.const_type) + ((*FIXNE*) c_body.const_type) ) ) () @@ -792,7 +791,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.LocalRawAssum (nal,_,_) -> List.map (fun (loc,n) -> - CRef(Libnames.Ident(loc, Nameops.out_name n))) + CRef(Libnames.Ident(loc, Nameops.out_name n),None)) nal ) nal_tas diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 5c37dcec3..8cccb0bed 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -114,7 +114,7 @@ let const_of_id id = let def_of_const t = match (Term.kind_of_term t) with Term.Const sp -> - (try (match Declareops.body_of_constant (Global.lookup_constant sp) with + (try (match Environ.constant_opt_value_in (Global.env()) sp with | Some c -> c | _ -> assert false) with Not_found -> assert false) @@ -146,7 +146,7 @@ let get_locality = function | Local -> true | Global -> false -let save with_clean id const (locality,kind) hook = +let save with_clean id const (locality,_,kind) hook = let l,r = match locality with | Discharge when Lib.sections_are_opened () -> let k = Kindops.logical_kind_of_goal_kind kind in @@ -177,7 +177,8 @@ let get_proof_clean do_reduce = let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () - and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in + and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () + in let old_rawprint = !Flags.raw_print in Flags.raw_print := true; Impargs.make_implicit_args false; @@ -259,8 +260,8 @@ let cache_Function (_,finfos) = let load_Function _ = cache_Function let subst_Function (subst,finfos) = - let do_subst_con c = fst (Mod_subst.subst_con subst c) - and do_subst_ind (kn,i) = (Mod_subst.subst_ind subst kn,i) + let do_subst_con c = Mod_subst.subst_constant subst c + and do_subst_ind i = Mod_subst.subst_ind subst i in let function_constant' = do_subst_con finfos.function_constant in let graph_ind' = do_subst_ind finfos.graph_ind in @@ -336,7 +337,7 @@ let pr_info f_info = str "function_constant_type := " ++ (try Printer.pr_lconstr - (Global.type_of_global (ConstRef f_info.function_constant)) + (Global.type_of_global_unsafe (ConstRef f_info.function_constant)) with e when Errors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 0e8b22deb..6e8b79a6b 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -58,7 +58,7 @@ val get_proof_clean : bool -> -(* [with_full_print f a] applies [f] to [a] in full printing environment +(* [with_full_print f a] applies [f] to [a] in full printing environment. This function preserves the print settings *) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 7c8f5714e..897c8765b 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -112,7 +112,9 @@ let id_to_constr id = let generate_type g_to_f f graph i = (*i we deduce the number of arguments of the function and its returned type from the graph i*) - let graph_arity = Inductive.type_of_inductive (Global.env()) (Global.lookup_inductive (destInd graph)) in + let gr,u = destInd graph in + let graph_arity = Inductive.type_of_inductive (Global.env()) + (Global.lookup_inductive gr, u) in let ctxt,_ = decompose_prod_assum graph_arity in let fun_ctxt,res_type = match ctxt with @@ -138,8 +140,11 @@ let generate_type g_to_f f graph i = the hypothesis [res = fv] can then be computed We will need to lift it by one in order to use it as a conclusion i*) + let make_eq () = +(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ()) + in let res_eq_f_of_args = - mkApp(Coqlib.build_coq_eq (),[|lift 2 res_type;mkRel 1;mkRel 2|]) + mkApp(make_eq (),[|lift 2 res_type;mkRel 1;mkRel 2|]) in (*i The hypothesis [graph\ x_1\ldots x_n\ res] can then be computed @@ -166,7 +171,7 @@ let generate_type g_to_f f graph i = WARNING: while convertible, [type_of body] and [type] can be non equal *) let find_induction_principle f = - let f_as_constant = match kind_of_term f with + let f_as_constant,u = match kind_of_term f with | Const c' -> c' | _ -> error "Must be used with a function" in @@ -205,6 +210,11 @@ let rec generate_fresh_id x avoid i = let id = Namegen.next_ident_away_in_goal x avoid in id::(generate_fresh_id x (id::avoid) (pred i)) +let make_eq () = +(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ()) +let make_eq_refl () = +(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ()) + (* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ] is the tactic used to prove correctness lemma. @@ -237,7 +247,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem \[fun (x_1:t_1)\ldots(x_n:t_n)=> fun fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\] *) (* we the get the definition of the graphs block *) - let graph_ind = destInd graphs_constr.(i) in + let graph_ind,u = destInd graphs_constr.(i) in let kn = fst graph_ind in let mib,_ = Global.lookup_inductive graph_ind in (* and the principle to use in this lemma in $\zeta$ normal form *) @@ -267,8 +277,8 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem branches in (* before building the full intro pattern for the principle *) - let eq_ind = Coqlib.build_coq_eq () in - let eq_construct = mkConstruct((destInd eq_ind),1) in + let eq_ind = make_eq () in + let eq_construct = mkConstructUi (destInd eq_ind, 1) in (* The next to referencies will be used to find out which constructor to apply in each branch *) let ind_number = ref 0 and min_constr_number = ref 0 in @@ -731,7 +741,7 @@ let rec intros_with_rewrite g = observe_tac "intros_with_rewrite" intros_with_rewrite_aux g and intros_with_rewrite_aux : tactic = fun g -> - let eq_ind = Coqlib.build_coq_eq () in + let eq_ind = make_eq () in match kind_of_term (pf_concl g) with | Prod(_,t,t') -> begin @@ -830,7 +840,7 @@ let rec reflexivity_with_destruct_cases g = | _ -> Proofview.V82.of_tactic reflexivity with e when Errors.noncritical e -> Proofview.V82.of_tactic reflexivity in - let eq_ind = Coqlib.build_coq_eq () in + let eq_ind = make_eq () in let discr_inject = Tacticals.onAllHypsAndConcl ( fun sc g -> @@ -936,7 +946,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = let rewrite_tac j ids : tactic = let graph_def = graphs.(j) in let infos = - try find_Function_infos (destConst funcs.(j)) + try find_Function_infos (fst (destConst funcs.(j))) with Not_found -> error "No graph found" in if infos.is_general @@ -962,7 +972,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = thin ids ] else - unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (destConst f))] + unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))] in (* The proof of each branche itself *) let ind_number = ref 0 in @@ -1026,7 +1036,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g let lemmas_types_infos = Util.Array.map2_i (fun i f_constr graph -> - let const_of_f = destConst f_constr in + let const_of_f,u = destConst f_constr in let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = generate_type false const_of_f graph i in @@ -1065,22 +1075,22 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g i*) let lem_id = mk_correct_id f_id in Lemmas.start_proof lem_id - (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) - (fst lemmas_types_infos.(i)) + (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem)) + (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty) (fun _ _ -> ()); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i)))); do_save (); let finfo = find_Function_infos f_as_constant in - let lem_cst = destConst (Constrintern.global_reference lem_id) in + let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in update_Function {finfo with correctness_lemma = Some lem_cst} ) funs; let lemmas_types_infos = Util.Array.map2_i (fun i f_constr graph -> - let const_of_f = destConst f_constr in + let const_of_f = fst (destConst f_constr) in let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = generate_type true const_of_f graph i in @@ -1092,19 +1102,21 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g funs_constr graphs_constr in - let kn,_ as graph_ind = destInd graphs_constr.(0) in + let kn,_ as graph_ind = fst (destInd graphs_constr.(0)) in let mib,mip = Global.lookup_inductive graph_ind in - let schemes = - Array.of_list + let sigma, scheme = (Indrec.build_mutual_induction_scheme (Global.env ()) Evd.empty (Array.to_list (Array.mapi - (fun i _ -> (kn,i),true,InType) + (fun i _ -> ((kn,i),Univ.Instance.empty)(*FIXME*),true,InType) mib.Declarations.mind_packets ) ) ) in + let schemes = + Array.of_list scheme + in let proving_tac = prove_fun_complete funs_constr mib.Declarations.mind_packets schemes lemmas_types_infos in @@ -1116,15 +1128,12 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g i*) let lem_id = mk_complete_id f_id in Lemmas.start_proof lem_id - (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) - (fst lemmas_types_infos.(i)) + (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem)) + (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty) (fun _ _ -> ()); - ignore (Pfedit.by - (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") - (proving_tac i)))); do_save (); let finfo = find_Function_infos f_as_constant in - let lem_cst = destConst (Constrintern.global_reference lem_id) in + let lem_cst,u = destConst (Constrintern.global_reference lem_id) in update_Function {finfo with completeness_lemma = Some lem_cst} ) funs) @@ -1142,7 +1151,7 @@ let revert_graph kn post_tac hid g = let typ = pf_type_of g (mkVar hid) in match kind_of_term typ with | App(i,args) when isInd i -> - let ((kn',num) as ind') = destInd i in + let ((kn',num) as ind'),u = destInd i in if MutInd.equal kn kn' then (* We have generated a graph hypothesis so that we must change it if we can *) let info = @@ -1192,7 +1201,7 @@ let functional_inversion kn hid fconst f_correct : tactic = let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in let type_of_h = pf_type_of g (mkVar hid) in match kind_of_term type_of_h with - | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) -> + | App(eq,args) when eq_constr eq (make_eq ()) -> let pre_tac,f_args,res = match kind_of_term args.(1),kind_of_term args.(2) with | App(f,f_args),_ when eq_constr f fconst -> @@ -1244,12 +1253,12 @@ let invfun qhyp f g = (fun hid -> Proofview.V82.tactic begin fun g -> let hyp_typ = pf_type_of g (mkVar hid) in match kind_of_term hyp_typ with - | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) -> + | App(eq,args) when eq_constr eq (make_eq ()) -> begin let f1,_ = decompose_app args.(1) in try if not (isConst f1) then failwith ""; - let finfos = find_Function_infos (destConst f1) in + let finfos = find_Function_infos (fst (destConst f1)) in let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in @@ -1258,7 +1267,7 @@ let invfun qhyp f g = try let f2,_ = decompose_app args.(2) in if not (isConst f2) then failwith ""; - let finfos = find_Function_infos (destConst f2) in + let finfos = find_Function_infos (fst (destConst f2)) in let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index ac54e44cc..d0497f6f6 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -70,7 +70,7 @@ let isVarf f x = in global environment. *) let ident_global_exist id = try - let ans = CRef (Libnames.Ident (Loc.ghost,id)) in + let ans = CRef (Libnames.Ident (Loc.ghost,id), None) in let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in true with e when Errors.noncritical e -> false @@ -134,16 +134,12 @@ let prNamedRLDecl s lc = let showind (id:Id.t) = let cstrid = Constrintern.global_reference id in let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in - let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in + let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in List.iter (fun (nm, optcstr, tp) -> print_string (string_of_name nm^":"); prconstr tp; print_string "\n") ib1.mind_arity_ctxt; - (match ib1.mind_arity with - | Monomorphic x -> - Printf.printf "arity :"; prconstr x.mind_user_arity - | Polymorphic x -> - Printf.printf "arity : universe?"); + Printf.printf "arity :"; prconstr ib1.mind_arity.mind_user_arity; Array.iteri (fun i x -> Printf.printf"type constr %d :" i ; prconstr x) ib1.mind_user_lc @@ -888,7 +884,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in + let mie,impls = Command.interp_mutual_inductive indl [] false (*FIXMEnon-poly *) true (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls) @@ -961,7 +957,7 @@ let funify_branches relinfo nfuns branch = | _ -> assert false in let is_dom c = match kind_of_term c with - | Ind((u,_)) | Construct((u,_),_) -> MutInd.equal u mut_induct + | Ind(((u,_),_)) | Construct(((u,_),_),_) -> MutInd.equal u mut_induct | _ -> false in let _dom_i c = assert (is_dom c); diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 614886073..96bf4c921 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -52,29 +52,21 @@ let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in locate (make_qualid dp (Id.of_string s)) -let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) = - fun f_id kind value -> - let ce = {const_entry_body = Future.from_val - (value, Declareops.no_seff); - const_entry_secctx = None; - const_entry_type = None; - const_entry_opaque = false; - const_entry_inline_code = false; - const_entry_feedback = None; - } in - ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; +let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value = + let ce = definition_entry ~univs:ctx value (*FIXME *) in + ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None)) let def_of_const t = match (kind_of_term t) with Const sp -> - (try (match body_of_constant (Global.lookup_constant sp) with + (try (match constant_opt_value_in (Global.env ()) sp with | Some c -> c | _ -> raise Not_found) with Not_found -> anomaly (str "Cannot find definition of constant " ++ - (Id.print (Label.to_id (con_label sp)))) + (Id.print (Label.to_id (con_label (fst sp))))) ) |_ -> assert false @@ -83,6 +75,7 @@ let type_of_const t = Const sp -> Typeops.type_of_constant (Global.env()) sp |_ -> assert false +let constr_of_global = Universes.constr_of_global let constant sl s = constr_of_global (find_reference sl s) @@ -188,7 +181,7 @@ let (value_f:constr list -> global_reference -> constr) = let glob_body = GCases (d0,RegularStyle,None, - [GApp(d0, GRef(d0,fterm), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l), + [GApp(d0, GRef(d0,fterm,None), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l), (Anonymous,None)], [d0, [v_id], [PatCstr(d0,(destIndRef (delayed_force coq_sig_ref),1), @@ -197,7 +190,7 @@ let (value_f:constr list -> global_reference -> constr) = Anonymous)], GVar(d0,v_id)]) in - let body = understand Evd.empty env glob_body in + let body = fst (understand Evd.empty env glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) = @@ -302,6 +295,7 @@ let check_not_nested forbidden e = | Lambda(_,t,b) -> check_not_nested t;check_not_nested b | LetIn(_,v,t,b) -> check_not_nested t;check_not_nested b;check_not_nested v | App(f,l) -> check_not_nested f;Array.iter check_not_nested l + | Proj (p,c) -> check_not_nested c | Const _ -> () | Ind _ -> () | Construct _ -> () @@ -412,6 +406,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = match kind_of_term expr_info.info with | CoFix _ | Fix _ -> error "Function cannot treat local fixpoint or cofixpoint" + | Proj _ -> error "Function cannot treat projections" | LetIn(na,b,t,e) -> begin let new_continuation_tac = @@ -640,7 +635,16 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info = in continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} +let pf_type c tac gl = + let evars, ty = Typing.e_type_of (pf_env gl) (project gl) c in + tclTHEN (Refiner.tclEVARS evars) (tac ty) gl +let pf_typel l tac = + let rec aux tys l = + match l with + | [] -> tac (List.rev tys) + | hd :: tl -> pf_type hd (fun ty -> aux (ty::tys) tl) + in aux [] l (* This is like the previous one except that it also rewrite on all hypotheses except the ones given in the first argument. All the @@ -660,12 +664,13 @@ let mkDestructEq : let type_of_expr = pf_type_of g expr in let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|]):: to_revert_constr in + pf_typel new_hyps (fun _ -> tclTHENLIST [Simple.generalize new_hyps; (fun g2 -> change_in_concl None (pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2); - Proofview.V82.of_tactic (simplest_case expr)], to_revert + Proofview.V82.of_tactic (simplest_case expr)]), to_revert let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = @@ -1167,7 +1172,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let get_current_subgoals_types () = let p = Proof_global.give_me_the_proof () in let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in - List.map (Goal.V82.abstract_type sigma) sgs + sigma, List.map (Goal.V82.abstract_type sigma) sgs let build_and_l l = let and_constr = Coqlib.build_coq_and () in @@ -1225,12 +1230,12 @@ let clear_goals = let build_new_goal_type () = - let sub_gls_types = get_current_subgoals_types () in - (* Pp.msgnl (str "sub_gls_types1 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) + let sigma, sub_gls_types = get_current_subgoals_types () in + (* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) let sub_gls_types = clear_goals sub_gls_types in (* Pp.msgnl (str "sub_gls_types2 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) let res = build_and_l sub_gls_types in - res + sigma, res let is_opaque_constant c = let cb = Global.lookup_constant c in @@ -1239,7 +1244,7 @@ let is_opaque_constant c = | Declarations.Undef _ -> true | Declarations.Def _ -> false -let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = +let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) let current_proof_name = get_current_proof_name () in let name = match goal_name with @@ -1265,7 +1270,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ let lid = ref [] in let h_num = ref (-1) in Proof_global.discard_all (); - build_proof + build_proof (Univ.ContextSet.empty) ( fun gls -> let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in tclTHENSEQ @@ -1312,8 +1317,8 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ in Lemmas.start_proof na - (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma) - gls_type + (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) + (gls_type, ctx) hook; if Indfun_common.is_strict_tcc () then @@ -1330,7 +1335,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ (fun c -> tclTHENSEQ [Proofview.V82.of_tactic intros; - Simple.apply (interp_constr Evd.empty (Global.env()) c); + Simple.apply (fst (interp_constr Evd.empty (Global.env()) c)) (*FIXME*); tclCOMPLETE (Proofview.V82.of_tactic Auto.default_auto) ] ) @@ -1354,22 +1359,24 @@ let com_terminate relation rec_arg_num thm_name using_lemmas - nb_args + nb_args ctx hook = - let start_proof (tac_start:tactic) (tac_end:tactic) = + let ctx = Univ.ContextSet.of_context ctx in + let start_proof ctx (tac_start:tactic) (tac_end:tactic) = let (evmap, env) = Lemmas.get_current_context() in Lemmas.start_proof thm_name - (Global, Proof Lemma) ~sign:(Environ.named_context_val env) - (compute_terminate_type nb_args fonctional_ref) hook; + (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) + (compute_terminate_type nb_args fonctional_ref, ctx) hook; ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start))); ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref input_type relation rec_arg_num )))) in - start_proof tclIDTAC tclIDTAC; + start_proof ctx tclIDTAC tclIDTAC; try - let new_goal_type = build_new_goal_type () in - open_new_goal start_proof using_lemmas tcc_lemma_ref + let sigma, new_goal_type = build_new_goal_type () in + open_new_goal start_proof (Evd.get_universe_context_set sigma) + using_lemmas tcc_lemma_ref (Some tcc_lemma_name) (new_goal_type); with Failure "empty list of subgoals!" -> @@ -1384,7 +1391,7 @@ let start_equation (f:global_reference) (term_f:global_reference) (cont_tactic:Id.t list -> tactic) g = let ids = pf_ids_of_hyps g in let terminate_constr = constr_of_global term_f in - let nargs = nb_prod (type_of_const terminate_constr) in + let nargs = nb_prod (fst (type_of_const terminate_constr)) (*FIXME*) in let x = n_x_id ids nargs in tclTHENLIST [ h_intros x; @@ -1406,8 +1413,8 @@ let (com_eqn : int -> Id.t -> let (evmap, env) = Lemmas.get_current_context() in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - (Lemmas.start_proof eq_name (Global, Proof Lemma) - ~sign:(Environ.named_context_val env) equation_lemma_type (fun _ _ -> ()); + (Lemmas.start_proof eq_name (Global, false, Proof Lemma) + ~sign:(Environ.named_context_val env) (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty) (fun _ _ -> ()); ignore (by (Proofview.V82.tactic (start_equation f_ref terminate_ref (fun x -> @@ -1445,13 +1452,15 @@ let (com_eqn : int -> Id.t -> let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : unit = - let function_type = interp_constr Evd.empty (Global.env()) type_of_f in - let env = push_named (function_name,None,function_type) (Global.env()) in + let env = Global.env() in + let evd = ref (Evd.from_env env) in + let function_type = interp_type_evars evd env type_of_f in + let env = push_named (function_name,None,function_type) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) - let equation_lemma_type = - nf_betaiotazeta - (interp_constr Evd.empty env ~impls:rec_impls eq) - in + let ty = interp_type_evars evd env ~impls:rec_impls eq in + let evm, nf = Evarutil.nf_evars_and_universes !evd in + let equation_lemma_type = nf_betaiotazeta (nf ty) in + let function_type = nf function_type in (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) let res_vars,eq' = decompose_prod equation_lemma_type in let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in @@ -1471,13 +1480,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_id = add_suffix function_name "_equation" in let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in - let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) res in + let ctx = Evd.universe_context evm in + let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in let relation = - interp_constr + fst (*FIXME*)(interp_constr Evd.empty env_with_pre_rec_args - r + r) in let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref None in @@ -1524,6 +1534,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num term_id using_lemmas (List.length res_vars) - hook) + ctx hook) () - diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index 2ef685203..f60eedbe6 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -12,9 +12,9 @@ bool -> Constrintern.internalization_env -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> - int -> Constrexpr.constr_expr -> (Names.constant -> + int -> Constrexpr.constr_expr -> (Term.pconstant -> Term.constr option ref -> - Names.constant -> - Names.constant -> int -> Term.types -> int -> Term.constr -> 'a) -> Constrexpr.constr_expr list -> unit + Term.pconstant -> + Term.pconstant -> int -> Term.types -> int -> Term.constr -> 'a) -> Constrexpr.constr_expr list -> unit diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v index b260feab1..2246af64d 100644 --- a/plugins/micromega/OrderedRing.v +++ b/plugins/micromega/OrderedRing.v @@ -85,9 +85,9 @@ Notation "x < y" := (rlt x y). Add Relation R req - reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _ ) - symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _ ) - transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _ ) + reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _) + symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _) + transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _) as sor_setoid. diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 68add5b3d..fb16c55c2 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -57,7 +57,7 @@ Variables ceqb cleb : C -> C -> bool. Variable phi : C -> R. (* Power coefficients *) -Variable E : Set. (* the type of exponents *) +Variable E : Type. (* the type of exponents *) Variable pow_phi : N -> E. Variable rpow : R -> E -> R. @@ -78,9 +78,9 @@ Record SORaddon := mk_SOR_addon { Variable addon : SORaddon. Add Relation R req - reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _ ) - symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _ ) - transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _ ) + reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _) + symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _) + transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _) as micomega_sor_setoid. Add Morphism rplus with signature req ==> req ==> req as rplus_morph. @@ -414,7 +414,7 @@ Proof. simpl ; intros. destruct (nth_in_or_default n l (Pc cO, Equal)). (* index is in bounds *) - apply H ; congruence. + apply H. congruence. (* index is out-of-bounds *) inversion H0. rewrite e. simpl. diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index d8ab6fd30..78837d4cd 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -317,7 +317,7 @@ Qed. Require Import QArith. -Inductive ZArithProof : Type := +Inductive ZArithProof := | DoneProof | RatProof : ZWitness -> ZArithProof -> ZArithProof | CutProof : ZWitness -> ZArithProof -> ZArithProof diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 9515c5de9..d11454b27 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -536,10 +536,10 @@ struct let get_left_construct term = match Term.kind_of_term term with - | Term.Construct(_,i) -> (i,[| |]) + | Term.Construct((_,i),_) -> (i,[| |]) | Term.App(l,rst) -> (match Term.kind_of_term l with - | Term.Construct(_,i) -> (i,rst) + | Term.Construct((_,i),_) -> (i,rst) | _ -> raise ParseError ) | _ -> raise ParseError @@ -833,8 +833,8 @@ struct let parse_zop (op,args) = match kind_of_term op with - | Const x -> (assoc_const op zop_table, args.(0) , args.(1)) - | Ind(n,0) -> + | Const (x,_) -> (assoc_const op zop_table, args.(0) , args.(1)) + | Ind((n,0),_) -> if Constr.equal op (Lazy.force coq_Eq) && Constr.equal args.(0) (Lazy.force coq_Z) then (Mc.OpEq, args.(1), args.(2)) else raise ParseError @@ -842,8 +842,8 @@ struct let parse_rop (op,args) = match kind_of_term op with - | Const x -> (assoc_const op rop_table, args.(0) , args.(1)) - | Ind(n,0) -> + | Const (x,_) -> (assoc_const op rop_table, args.(0) , args.(1)) + | Ind((n,0),_) -> if Constr.equal op (Lazy.force coq_Eq) && Constr.equal args.(0) (Lazy.force coq_R) then (Mc.OpEq, args.(1), args.(2)) else raise ParseError diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 9b851447c..9b12c5eb3 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -170,7 +170,7 @@ let hide_constr,find_constr,clear_constr_tables,dump_tables = let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in (fun h id eg b -> l := (h,(id,eg,b)):: !l), (fun h -> - try List.assoc_f Constr.equal h !l with Not_found -> failwith "find_contr"), + try List.assoc_f eq_constr_nounivs h !l with Not_found -> failwith "find_contr"), (fun () -> l := []), (fun () -> !l) @@ -350,7 +350,7 @@ let coq_iff = lazy (constant "iff") (* For unfold *) let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with - | Const kn when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) -> + | Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) -> EvalConstRef kn | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant")) @@ -367,15 +367,16 @@ let mk_var v = mkVar (Id.of_string v) let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |]) let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |]) let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |]) -let mk_eq t1 t2 = mkApp (build_coq_eq (), [| Lazy.force coq_Z; t1; t2 |]) +let mk_eq t1 t2 = mkApp (Universes.constr_of_global (build_coq_eq ()), + [| Lazy.force coq_Z; t1; t2 |]) let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |]) let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |]) let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |]) let mk_and t1 t2 = mkApp (build_coq_and (), [| t1; t2 |]) let mk_or t1 t2 = mkApp (build_coq_or (), [| t1; t2 |]) let mk_not t = mkApp (build_coq_not (), [| t |]) -let mk_eq_rel t1 t2 = mkApp (build_coq_eq (), - [| Lazy.force coq_comparison; t1; t2 |]) +let mk_eq_rel t1 t2 = mkApp (Universes.constr_of_global (build_coq_eq ()), + [| Lazy.force coq_comparison; t1; t2 |]) let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |]) let mk_integer n = @@ -419,7 +420,7 @@ type result = let destructurate_prop t = let c, args = decompose_app t in match kind_of_term c, args with - | _, [_;_;_] when eq_constr c (build_coq_eq ()) -> Kapp (Eq,args) + | _, [_;_;_] when eq_constr c (Universes.constr_of_global (build_coq_eq ())) -> Kapp (Eq,args) | _, [_;_] when eq_constr c (Lazy.force coq_neq) -> Kapp (Neq,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zne) -> Kapp (Zne,args) | _, [_;_] when eq_constr c (Lazy.force coq_Zle) -> Kapp (Zle,args) @@ -436,11 +437,11 @@ let destructurate_prop t = | _, [_;_] when eq_constr c (Lazy.force coq_lt) -> Kapp (Lt,args) | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args) | _, [_;_] when eq_constr c (Lazy.force coq_gt) -> Kapp (Gt,args) - | Const sp, args -> + | Const (sp,_), args -> Kapp (Other (string_of_path (path_of_global (ConstRef sp))),args) - | Construct csp , args -> + | Construct (csp,_) , args -> Kapp (Other (string_of_path (path_of_global (ConstructRef csp))), args) - | Ind isp, args -> + | Ind (isp,_), args -> Kapp (Other (string_of_path (path_of_global (IndRef isp))),args) | Var id,[] -> Kvar id | Prod (Anonymous,typ,body), [] -> Kimp(typ,body) @@ -1081,7 +1082,8 @@ let replay_history tactic_normalisation = let p_initial = [P_APP 2;P_TYPE] in let tac = shuffle_cancel p_initial e1.body in let solve_le = - let not_sup_sup = mkApp (build_coq_eq (), [| + let not_sup_sup = mkApp (Universes.constr_of_global (build_coq_eq ()), + [| Lazy.force coq_comparison; Lazy.force coq_Gt; Lazy.force coq_Gt |]) diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 9ee16a582..ea459e551 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -196,9 +196,9 @@ let coerce_meta_in n = let compute_lhs typ i nargsi = match kind_of_term typ with - | Ind(sp,0) -> + | Ind((sp,0),u) -> let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in - mkApp (mkConstruct ((sp,0),i+1), argsi) + mkApp (mkConstructU (((sp,0),i+1),u), argsi) | _ -> i_can't_do_that () (*s This function builds the pattern from the RHS. Recursive calls are @@ -221,7 +221,7 @@ let compute_rhs bodyi index_of_f = let compute_ivs f cs gl = let cst = try destConst f with DestKO -> i_can't_do_that () in - let body = Environ.constant_value (Global.env()) cst in + let body = Environ.constant_value_in (Global.env()) cst in match decomp_term body with | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> let (args3, body3) = decompose_lam body2 in diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index ab424c223..7e4475d40 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -1284,7 +1284,7 @@ Qed. (* Extraire une hypothèse de la liste *) Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm. - +Unset Printing Notations. Theorem nth_valid : forall (ep : list Prop) (e : list int) (i : nat) (l : hyps), interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l). diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 5416e936c..689462704 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -30,11 +30,11 @@ let string_of_global r = let destructurate t = let c, args = Term.decompose_app t in match Term.kind_of_term c, args with - | Term.Const sp, args -> + | Term.Const (sp,_), args -> Kapp (string_of_global (Globnames.ConstRef sp), args) - | Term.Construct csp , args -> + | Term.Construct (csp,_) , args -> Kapp (string_of_global (Globnames.ConstructRef csp), args) - | Term.Ind isp, args -> + | Term.Ind (isp,_), args -> Kapp (string_of_global (Globnames.IndRef isp), args) | Term.Var id,[] -> Kvar(Names.Id.to_string id) | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) @@ -48,9 +48,9 @@ let dest_const_apply t = let f,args = Term.decompose_app t in let ref = match Term.kind_of_term f with - | Term.Const sp -> Globnames.ConstRef sp - | Term.Construct csp -> Globnames.ConstructRef csp - | Term.Ind isp -> Globnames.IndRef isp + | Term.Const (sp,_) -> Globnames.ConstRef sp + | Term.Construct (csp,_) -> Globnames.ConstructRef csp + | Term.Ind (isp,_) -> Globnames.IndRef isp | _ -> raise Destruct in Nametab.basename_of_global ref, args @@ -210,19 +210,26 @@ let rec mk_nat = function (* Lists *) -let coq_cons = lazy (constant "cons") -let coq_nil = lazy (constant "nil") +let mkListConst c u = + Term.mkConstructU (Globnames.destConstructRef + (Coqlib.gen_reference "" ["Init";"Datatypes"] c), + Univ.Instance.of_array [|u|]) -let mk_list typ l = +let coq_cons univ typ = Term.mkApp (mkListConst "cons" univ, [|typ|]) +let coq_nil univ typ = Term.mkApp (mkListConst "nil" univ, [|typ|]) + +let mk_list univ typ l = let rec loop = function - | [] -> - Term.mkApp (Lazy.force coq_nil, [|typ|]) + | [] -> coq_nil univ typ | (step :: l) -> - Term.mkApp (Lazy.force coq_cons, [|typ; step; loop l |]) in + Term.mkApp (coq_cons univ typ, [| step; loop l |]) in loop l -let mk_plist l = mk_list Term.mkProp l +let mk_plist = + let type1lev = Universes.new_univ_level (Global.current_dirpath ()) in + fun l -> mk_list type1lev Term.mkProp l +let mk_list = mk_list Univ.Level.set let mk_shuffle_list l = mk_list (Lazy.force coq_t_fusion) l diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index b8db71e40..4ae1cb94c 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -117,6 +117,7 @@ val do_seq : Term.constr -> Term.constr -> Term.constr val do_list : Term.constr list -> Term.constr val mk_nat : int -> Term.constr +(** Precondition: the type of the list is in Set *) val mk_list : Term.constr -> Term.constr list -> Term.constr val mk_plist : Term.types list -> Term.types val mk_shuffle_list : Term.constr list -> Term.constr diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 98dd257d5..16081ffe1 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -198,7 +198,7 @@ Theorem get_Full_Gt : forall S, Full S -> 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/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 96758788a..bff574a06 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -104,20 +104,20 @@ 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 Names.eq_ind 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 Int.equal (Array.length argv) 2 -> begin try - let ind = destInd hd in - if Names.eq_ind 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 Names.eq_ind 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) diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 3622c7fe9..2b9dce1b0 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -10,6 +10,7 @@ Require Ring. Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List Morphisms. Require Import ZArith_base. Set Implicit Arguments. +(* Set Universe Polymorphism. *) Section MakeFieldPol. @@ -278,6 +279,21 @@ apply radd_ext. [ ring | now rewrite rdiv_simpl ]. Qed. +Theorem rdiv3 r1 r2 r3 r4 : + ~ r2 == 0 -> + ~ r4 == 0 -> + r1 / r2 - r3 / r4 == (r1 * r4 - r3 * r2) / (r2 * r4). +Proof. +intros H2 H4. +assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial). +transitivity (r1 / r2 + - (r3 / r4)); auto. +transitivity (r1 / r2 + - r3 / r4); auto. +transitivity ((r1 * r4 + - r3 * r2) / (r2 * r4)). +apply rdiv2; auto. +f_equiv. +transitivity (r1 * r4 + - (r3 * r2)); auto. +Qed. + Theorem rdiv5 a b : - (a / b) == - a / b. Proof. now rewrite !rdiv_def, ropp_mul_l. @@ -696,6 +712,7 @@ Fixpoint PEsimp (e : PExpr C) : PExpr C := | _ => e end%poly. +<<<<<<< .merge_file_5Z3Qpn Theorem PEsimp_ok e : (PEsimp e === e)%poly. Proof. induction e; simpl. @@ -708,6 +725,32 @@ induction e; simpl. - rewrite NPEmul_ok. now f_equiv. - rewrite NPEopp_ok. now f_equiv. - rewrite NPEpow_ok. now f_equiv. +======= +Theorem PExpr_simp_correct: + forall l e, NPEeval l (PExpr_simp e) == NPEeval l e. +clear eq_sym. +intros l e; elim e; simpl; auto. +intros e1 He1 e2 He2. +transitivity (NPEeval l (PEadd (PExpr_simp e1) (PExpr_simp e2))); auto. +apply NPEadd_correct. +simpl; auto. +intros e1 He1 e2 He2. +transitivity (NPEeval l (PEsub (PExpr_simp e1) (PExpr_simp e2))). auto. +apply NPEsub_correct. +simpl; auto. +intros e1 He1 e2 He2. +transitivity (NPEeval l (PEmul (PExpr_simp e1) (PExpr_simp e2))); auto. +apply NPEmul_correct. +simpl; auto. +intros e1 He1. +transitivity (NPEeval l (PEopp (PExpr_simp e1))); auto. +apply NPEopp_correct. +simpl; auto. +intros e1 He1 n;simpl. +rewrite NPEpow_correct;simpl. +repeat rewrite pow_th.(rpow_pow_N). +rewrite He1;auto. +>>>>>>> .merge_file_U4r9lJ Qed. @@ -961,6 +1004,7 @@ Fixpoint split_aux e1 p e2 {struct e1}: rsplit := end end%poly. +<<<<<<< .merge_file_5Z3Qpn Lemma split_aux_ok1 e1 p e2 : (let res := match isIn e1 p e2 1 with | Some (N0,e3) => mk_rsplit 1 (e1 ^^ Npos p) e3 @@ -971,6 +1015,20 @@ Lemma split_aux_ok1 e1 p e2 : e1 ^ Npos p === left res * common res /\ e2 === right res * common res)%poly. Proof. +======= +Lemma split_aux_correct_1 : forall l e1 p e2, + let res := match isIn e1 p e2 xH with + | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3 + | Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3 + | None => mk_rsplit (NPEpow e1 (Npos p)) (PEc cI) e2 + end in + NPEeval l (PEpow e1 (Npos p)) == NPEeval l (NPEmul (left res) (common res)) + /\ + NPEeval l e2 == NPEeval l (NPEmul (right res) (common res)). +Proof. + intros. unfold res. clear res; generalize (isIn_correct l e1 p e2 xH). + destruct (isIn e1 p e2 1). destruct p0. +>>>>>>> .merge_file_U4r9lJ Opaque NPEpow NPEmul. intros. unfold res;clear res; generalize (isIn_ok e1 p e2 xH). destruct (isIn e1 p e2 1) as [([|p'],e')|]; simpl. @@ -1090,6 +1148,7 @@ Eval compute Theorem Pcond_Fnorm l e : PCond l (condition (Fnorm e)) -> ~ (denum (Fnorm e))@l == 0. Proof. +<<<<<<< .merge_file_5Z3Qpn induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl denum; intros (Hc1,Hc2) || intros Hc; rewrite ?NPEmul_ok. - simpl. rewrite phi_1; exact rI_neq_rO. @@ -1112,6 +1171,93 @@ induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app; + apply split_nz_r, Hc1. - rewrite NPEpow_ok. apply PEpow_nz, IHe, Hc. Qed. +======= + induction p;simpl. + intro Hp;assert (H1 := @rmul_reg_l _ (pow_pos rmul x p * pow_pos rmul x p) 0 H). + apply IHp. + rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). + reflexivity. + rewrite H1. ring. rewrite Hp;ring. + intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). + reflexivity. rewrite Hp;ring. trivial. +Qed. + +Theorem Pcond_Fnorm: + forall l e, + PCond l (condition (Fnorm e)) -> ~ NPEeval l ((Fnorm e).(denum)) == 0. +intros l e; elim e. + simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO. + simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO. + intros e1 Hrec1 e2 Hrec2 Hcond. + simpl in Hcond. + simpl @denum. + rewrite NPEmul_correct. + simpl. + apply field_is_integral_domain. + intros HH; case Hrec1; auto. + apply PCond_app_inv_l with (1 := Hcond). + rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))). + rewrite NPEmul_correct; simpl; rewrite HH; ring. + intros HH; case Hrec2; auto. + apply PCond_app_inv_r with (1 := Hcond). + rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto. + intros e1 Hrec1 e2 Hrec2 Hcond. + simpl @condition in Hcond. + simpl @denum. + rewrite NPEmul_correct. + simpl. + apply field_is_integral_domain. + intros HH; case Hrec1; auto. + apply PCond_app_inv_l with (1 := Hcond). + rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))). + rewrite NPEmul_correct; simpl; rewrite HH; ring. + intros HH; case Hrec2; auto. + apply PCond_app_inv_r with (1 := Hcond). + rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto. + intros e1 Hrec1 e2 Hrec2 Hcond. + simpl in Hcond. + simpl @denum. + rewrite NPEmul_correct. + simpl. + apply field_is_integral_domain. + intros HH; apply Hrec1. + apply PCond_app_inv_l with (1 := Hcond). + rewrite (split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))). + rewrite NPEmul_correct; simpl; rewrite HH; ring. + intros HH; apply Hrec2. + apply PCond_app_inv_r with (1 := Hcond). + rewrite (split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2))). + rewrite NPEmul_correct; simpl; rewrite HH; ring. + intros e1 Hrec1 Hcond. + simpl in Hcond. + simpl @denum. + auto. + intros e1 Hrec1 Hcond. + simpl in Hcond. + simpl @denum. + apply PCond_cons_inv_l with (1:=Hcond). + intros e1 Hrec1 e2 Hrec2 Hcond. + simpl in Hcond. + simpl @denum. + rewrite NPEmul_correct. + simpl. + apply field_is_integral_domain. + intros HH; apply Hrec1. + specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1. + apply PCond_app_inv_l with (1 := Hcond1). + rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))). + rewrite NPEmul_correct; simpl; rewrite HH; ring. + intros HH; apply PCond_cons_inv_l with (1:=Hcond). + rewrite (split_correct_r l (num (Fnorm e1)) (num (Fnorm e2))). + rewrite NPEmul_correct; simpl; rewrite HH; ring. + simpl;intros e1 Hrec1 n Hcond. + rewrite NPEpow_correct. + simpl;rewrite pow_th.(rpow_pow_N). + destruct n;simpl;intros. + apply AFth.(AF_1_neq_0). apply pow_pos_not_0;auto. +Qed. +Hint Resolve Pcond_Fnorm. +>>>>>>> .merge_file_U4r9lJ (*************************************************************************** @@ -1502,11 +1648,21 @@ Hypothesis ceqb_complete : forall c1 c2, [c1] == [c2] -> ceqb c1 c2 = true. Lemma ceqb_spec' c1 c2 : Bool.reflect ([c1] == [c2]) (ceqb c1 c2). Proof. +<<<<<<< .merge_file_5Z3Qpn assert (H := morph_eq CRmorph c1 c2). assert (H' := @ceqb_complete c1 c2). destruct (ceqb c1 c2); constructor. - now apply H. - intro E. specialize (H' E). discriminate. +======= +intros. +generalize (fun h => X (morph_eq CRmorph _ _ h)). +generalize (@ceqb_complete c1 c2). +case (c1 ?=! c2); auto; intros. +apply X0. +red; intro. +absurd (false = true); auto; discriminate. +>>>>>>> .merge_file_U4r9lJ Qed. Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) := @@ -1766,4 +1922,4 @@ End Field. End Complete. Arguments FEO [C]. -Arguments FEI [C].
\ No newline at end of file +Arguments FEI [C]. diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index ca178dd38..07f49cc4f 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -15,6 +15,7 @@ Require Import Ring_polynom. Import List. Set Implicit Arguments. +(* Set Universe Polymorphism. *) Import RingSyntax. diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 6ffa54866..5ec73950b 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -6,12 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) + Set Implicit Arguments. -Require Import Setoid Morphisms BinList BinPos BinNat BinInt. +Require Import Setoid Morphisms. +Require Import BinList BinPos BinNat BinInt. Require Export Ring_theory. - Local Open Scope positive_scope. Import RingSyntax. +(* Set Universe Polymorphism. *) Section MakeRingPol. @@ -678,7 +680,7 @@ Section MakeRingPol. - add_permut. - destruct p; simpl; rewrite ?jump_pred_double; add_permut. - - destr_pos_sub; intros ->;Esimpl. + - destr_pos_sub; intros ->; Esimpl. + rewrite IHP';rsimpl. add_permut. + rewrite IHP', pow_pos_add;simpl;Esimpl. add_permut. + rewrite IHP1, pow_pos_add;rsimpl. add_permut. @@ -796,9 +798,9 @@ Section MakeRingPol. P@l == Q@l + [c] * R@l. Proof. revert l. - induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl. - - assert (H := div_th.(div_eucl_th) c0 c). - destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. + induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl. + - assert (H := div_th.(div_eucl_th) c0 c). + destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. - destr_factor. Esimpl. - destr_factor. Esimpl. add_permut. Qed. @@ -807,11 +809,12 @@ Section MakeRingPol. let (c,M) := cM in let (Q,R) := MFactor P c M in P@l == Q@l + [c] * M@@l * R@l. - Proof. + Proof. destruct cM as (c,M). revert M l. - induction P; destruct M; intros l; simpl; auto; + induction P; destruct M; intros l; simpl; auto; try (case ceqb_spec; intro He); - try (case Pos.compare_spec; intros He); rewrite ?He; + try (case Pos.compare_spec; intros He); + rewrite ?He; destr_factor; simpl; Esimpl. - assert (H := div_th.(div_eucl_th) c0 c). destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. @@ -869,9 +872,9 @@ Section MakeRingPol. Lemma PSubstL1_ok n LM1 P1 l : MPcond LM1 l -> P1@l == (PSubstL1 P1 LM1 n)@l. Proof. - revert P1; induction LM1 as [|(M2,P2) LM2 IH]; simpl; intros. - - reflexivity. - - rewrite <- IH by intuition. now apply PNSubst1_ok. + revert P1; induction LM1 as [|(M2,P2) LM2 IH]; simpl; intros. + - reflexivity. + - rewrite <- IH by intuition; now apply PNSubst1_ok. Qed. Lemma PSubstL_ok n LM1 P1 P2 l : @@ -1483,4 +1486,4 @@ Qed. End MakeRingPol. Arguments PEO [C]. -Arguments PEI [C].
\ No newline at end of file +Arguments PEI [C]. diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 42ce4edca..d56f50bec 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -28,6 +28,8 @@ Reserved Notation "x == y" (at level 70, no associativity). End RingSyntax. Import RingSyntax. +(* Set Universe Polymorphism. *) + Section Power. Variable R:Type. Variable rI : R. @@ -252,6 +254,7 @@ Section ALMOST_RING. Section SEMI_RING. Variable SReqe : sring_eq_ext radd rmul req. + Add Morphism radd : radd_ext1. exact (SRadd_ext SReqe). Qed. Add Morphism rmul : rmul_ext1. exact (SRmul_ext SReqe). Qed. Variable SRth : semi_ring_theory 0 1 radd rmul req. @@ -503,7 +506,6 @@ Qed. End ALMOST_RING. - Section AddRing. (* Variable R : Type. @@ -528,7 +530,6 @@ Inductive ring_kind : Type := (_ : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi). - End AddRing. diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 235ee8d72..7ed8e03a9 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -74,7 +74,7 @@ and mk_clos_app_but f_map subs f args n = | None -> mk_clos_app_but f_map subs f args (n+1) let interp_map l t = - try Some(List.assoc_f eq_constr t l) with Not_found -> None + try Some(List.assoc_f eq_constr_nounivs t l) with Not_found -> None let protect_maps = ref String.Map.empty let add_map s m = protect_maps := String.Map.add s m !protect_maps @@ -104,7 +104,7 @@ END;; (****************************************************************************) let closed_term t l = - let l = List.map constr_of_global l in + let l = List.map Universes.constr_of_global l in let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt()) ;; @@ -141,15 +141,24 @@ let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" let ic c = let env = Global.env() and sigma = Evd.empty in - Constrintern.interp_constr sigma env c + Constrintern.interp_open_constr sigma env c + +let ic_unsafe c = (*FIXME remove *) + let env = Global.env() and sigma = Evd.empty in + fst (Constrintern.interp_constr sigma env c) let ty c = Typing.type_of (Global.env()) Evd.empty c -let decl_constant na c = +let decl_constant na ctx c = + let vars = Universes.universes_of_constr c in + let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in mkConst(declare_constant (Id.of_string na) (DefinitionEntry - { const_entry_body = c; + { const_entry_body = Future.from_val (c, Declareops.no_seff); const_entry_secctx = None; const_entry_type = None; + const_entry_polymorphic = false; + const_entry_universes = Univ.ContextSet.to_context ctx; + const_entry_proj = None; const_entry_opaque = true; const_entry_inline_code = false; const_entry_feedback = None; @@ -182,7 +191,11 @@ let dummy_goal env = Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Evd.Store.empty in {Evd.it = gl; Evd.sigma = sigma} -let exec_tactic env n f args = +let constr_of v = match Value.to_constr v with + | Some c -> c + | None -> failwith "Ring.exec_tactic: anomaly" + +let exec_tactic env evd n f args = let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in let res = ref [||] in let get_res ist = @@ -192,13 +205,14 @@ let exec_tactic env n f args = let getter = Tacexp(TacFun(List.map(fun id -> Some id) lid, Tacintern.glob_tactic(tacticIn get_res))) in - let _ = - Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter]))) (dummy_goal env) in - !res - -let constr_of v = match Value.to_constr v with - | Some c -> c - | None -> failwith "Ring.exec_tactic: anomaly" + let gls = + (fun gl -> + let sigma = gl.Evd.sigma in + tclTHEN (Refiner.tclEVARS (Evd.merge sigma evd)) + (Proofview.V82.of_tactic (Tacinterp.eval_tactic(ltac_call f (args@[getter])))) gl) + (dummy_goal env) in + let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in + Array.map (fun x -> nf (constr_of x)) !res, Evd.universe_context evd let stdlib_modules = [["Coq";"Setoids";"Setoid"]; @@ -209,6 +223,8 @@ let stdlib_modules = let coq_constant c = lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c) +let coq_reference c = + lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c) let coq_mk_Setoid = coq_constant "Build_Setoid_Theory" let coq_cons = coq_constant "cons" @@ -217,8 +233,15 @@ let coq_None = coq_constant "None" let coq_Some = coq_constant "Some" let coq_eq = coq_constant "eq" +let coq_pcons = coq_reference "cons" +let coq_pnil = coq_reference "nil" + let lapp f args = mkApp(Lazy.force f,args) +let plapp evd f args = + let fc = Evarutil.e_new_global evd (Lazy.force f) in + mkApp(fc,args) + let dest_rel0 t = match kind_of_term t with | App(f,args) when Array.length args >= 2 -> @@ -247,6 +270,8 @@ let plugin_modules = let my_constant c = lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c) +let my_reference c = + lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) let new_ring_path = DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"]) @@ -266,9 +291,9 @@ let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; let coq_almost_ring_theory = my_constant "almost_ring_theory" (* setoid and morphism utilities *) -let coq_eq_setoid = my_constant "Eqsth" -let coq_eq_morph = my_constant "Eq_ext" -let coq_eq_smorph = my_constant "Eq_s_ext" +let coq_eq_setoid = my_reference "Eqsth" +let coq_eq_morph = my_reference "Eq_ext" +let coq_eq_smorph = my_reference "Eq_s_ext" (* ring -> almost_ring utilities *) let coq_ring_theory = my_constant "ring_theory" @@ -295,8 +320,8 @@ let ltac_inv_morph_nothing = zltac"inv_morph_nothing" let coq_pow_N_pow_N = my_constant "pow_N_pow_N" (* hypothesis *) -let coq_mkhypo = my_constant "mkhypo" -let coq_hypo = my_constant "hypo" +let coq_mkhypo = my_reference "mkhypo" +let coq_hypo = my_reference "hypo" (* Equality: do not evaluate but make recursive call on both sides *) let map_with_eq arg_map c = @@ -415,14 +440,14 @@ let theory_to_obj : ring_info -> obj = classify_function = (fun x -> Substitute x)} -let setoid_of_relation env a r = - let evm = Evd.empty in +let setoid_of_relation env evd a r = try - lapp coq_mk_Setoid - [|a ; r ; - Rewrite.get_reflexive_proof env evm a r ; - Rewrite.get_symmetric_proof env evm a r ; - Rewrite.get_transitive_proof env evm a r |] + let evm = !evd, Int.Set.empty in + let evm, refl = Rewrite.PropGlobal.get_reflexive_proof env evm a r in + let evm, sym = Rewrite.PropGlobal.get_symmetric_proof env evm a r in + let evm, trans = Rewrite.PropGlobal.get_transitive_proof env evm a r in + evd := fst evm; + lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |] with Not_found -> error "cannot find setoid relation" @@ -435,7 +460,7 @@ let op_smorph r add mul req m1 m2 = (* let default_ring_equality (r,add,mul,opp,req) = *) (* let is_setoid = function *) (* {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *) -(* eq_constr req rel (\* Qu: use conversion ? *\) *) +(* eq_constr_nounivs req rel (\* Qu: use conversion ? *\) *) (* | _ -> false in *) (* match default_relation_for_carrier ~filter:is_setoid r with *) (* Leibniz _ -> *) @@ -450,7 +475,7 @@ let op_smorph r add mul req m1 m2 = (* let is_endomorphism = function *) (* { args=args } -> List.for_all *) (* (function (var,Relation rel) -> *) -(* var=None && eq_constr req rel *) +(* var=None && eq_constr_nounivs req rel *) (* | _ -> false) args in *) (* let add_m = *) (* try default_morphism ~filter:is_endomorphism add *) @@ -485,17 +510,19 @@ let op_smorph r add mul req m1 m2 = (* op_smorph r add mul req add_m.lem mul_m.lem) in *) (* (setoid,op_morph) *) -let ring_equality (r,add,mul,opp,req) = +let ring_equality env evd (r,add,mul,opp,req) = match kind_of_term req with - | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) -> - let setoid = lapp coq_eq_setoid [|r|] in + | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) -> + let setoid = plapp evd coq_eq_setoid [|r|] in let op_morph = match opp with - Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] - | None -> lapp coq_eq_smorph [|r;add;mul|] in + Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|] + | None -> plapp evd coq_eq_smorph [|r;add;mul|] in + let setoid = Typing.solve_evars env evd setoid in + let op_morph = Typing.solve_evars env evd op_morph in (setoid,op_morph) | _ -> - let setoid = setoid_of_relation (Global.env ()) r req in + let setoid = setoid_of_relation (Global.env ()) evd r req in let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in let add_m, add_m_lem = try Rewrite.default_morphism signature add @@ -532,22 +559,22 @@ let ring_equality (r,add,mul,opp,req) = op_smorph r add mul req add_m_lem mul_m_lem) in (setoid,op_morph) -let build_setoid_params r add mul opp req eqth = +let build_setoid_params env evd r add mul opp req eqth = match eqth with Some th -> th - | None -> ring_equality (r,add,mul,opp,req) + | None -> ring_equality env evd (r,add,mul,opp,req) let dest_ring env sigma th_spec = let th_typ = Retyping.get_type_of env sigma th_spec in match kind_of_term th_typ with App(f,[|r;zero;one;add;mul;sub;opp;req|]) - when eq_constr f (Lazy.force coq_almost_ring_theory) -> + when eq_constr_nounivs f (Lazy.force coq_almost_ring_theory) -> (None,r,zero,one,add,mul,Some sub,Some opp,req) | App(f,[|r;zero;one;add;mul;req|]) - when eq_constr f (Lazy.force coq_semi_ring_theory) -> + when eq_constr_nounivs f (Lazy.force coq_semi_ring_theory) -> (Some true,r,zero,one,add,mul,None,None,req) | App(f,[|r;zero;one;add;mul;sub;opp;req|]) - when eq_constr f (Lazy.force coq_ring_theory) -> + when eq_constr_nounivs f (Lazy.force coq_ring_theory) -> (Some false,r,zero,one,add,mul,Some sub,Some opp,req) | _ -> error "bad ring structure" @@ -557,10 +584,10 @@ let dest_morph env sigma m_spec = match kind_of_term m_typ with App(f,[|r;zero;one;add;mul;sub;opp;req; c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|]) - when eq_constr f (Lazy.force coq_ring_morph) -> + when eq_constr_nounivs f (Lazy.force coq_ring_morph) -> (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi) | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|]) - when eq_constr f (Lazy.force coq_semi_morph) -> + when eq_constr_nounivs f (Lazy.force coq_semi_morph) -> (c,czero,cone,cadd,cmul,None,None,ceqb,phi) | _ -> error "bad morphism structure" @@ -591,18 +618,22 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morph_nothing) in TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])) -let make_hyp env c = - let t = Retyping.get_type_of env Evd.empty c in - lapp coq_mkhypo [|t;c|] - -let make_hyp_list env lH = - let carrier = Lazy.force coq_hypo in - List.fold_right - (fun c l -> lapp coq_cons [|carrier; (make_hyp env c); l|]) lH - (lapp coq_nil [|carrier|]) - -let interp_power env pow = - let carrier = Lazy.force coq_hypo in +let make_hyp env evd c = + let t = Retyping.get_type_of env !evd c in + plapp evd coq_mkhypo [|t;c|] + +let make_hyp_list env evd lH = + let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in + let l = + List.fold_right + (fun c l -> plapp evd coq_pcons [|carrier; (make_hyp env evd c); l|]) lH + (plapp evd coq_pnil [|carrier|]) + in + let l' = Typing.solve_evars env evd l in + Evarutil.nf_evars_universes !evd l' + +let interp_power env evd pow = + let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in match pow with | None -> let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in @@ -613,47 +644,47 @@ let interp_power env pow = | CstTac t -> Tacintern.glob_tactic t | Closed lc -> closed_term_ast (List.map Smartlocate.global_with_alias lc) in - let spec = make_hyp env (ic spec) in + let spec = make_hyp env evd (ic_unsafe spec) in (tac, lapp coq_Some [|carrier; spec|]) -let interp_sign env sign = - let carrier = Lazy.force coq_hypo in +let interp_sign env evd sign = + let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in match sign with | None -> lapp coq_None [|carrier|] | Some spec -> - let spec = make_hyp env (ic spec) in + let spec = make_hyp env evd (ic_unsafe spec) in lapp coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) -let interp_div env div = - let carrier = Lazy.force coq_hypo in +let interp_div env evd div = + let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in match div with | None -> lapp coq_None [|carrier|] | Some spec -> - let spec = make_hyp env (ic spec) in + let spec = make_hyp env evd (ic_unsafe spec) in lapp coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) -let add_theory name rth eqth morphth cst_tac (pre,post) power sign div = +let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div = check_required_library (cdir@["Ring_base"]); let env = Global.env() in - let sigma = Evd.empty in let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in - let (sth,ext) = build_setoid_params r add mul opp req eqth in - let (pow_tac, pspec) = interp_power env power in - let sspec = interp_sign env sign in - let dspec = interp_div env div in + let evd = ref sigma in + let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in + let (pow_tac, pspec) = interp_power env evd power in + let sspec = interp_sign env evd sign in + let dspec = interp_div env evd div in let rk = reflect_coeff morphth in - let params = - exec_tactic env 5 (zltac "ring_lemmas") + let params,ctx = + exec_tactic env !evd 5 (zltac "ring_lemmas") (List.map carg[sth;ext;rth;pspec;sspec;dspec;rk]) in - let lemma1 = constr_of params.(3) in - let lemma2 = constr_of params.(4) in + let lemma1 = params.(3) in + let lemma2 = params.(4) in let lemma1 = - decl_constant (Id.to_string name^"_ring_lemma1") (Future.from_val ( lemma1,Declareops.no_seff)) in + decl_constant (Id.to_string name^"_ring_lemma1") ctx (Future.from_val ( lemma1,Declareops.no_seff)) in let lemma2 = - decl_constant (Id.to_string name^"_ring_lemma2") (Future.from_val ( lemma2,Declareops.no_seff)) in + decl_constant (Id.to_string name^"_ring_lemma2") ctx (Future.from_val ( lemma2,Declareops.no_seff)) in let cst_tac = interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = @@ -670,9 +701,9 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div = { ring_carrier = r; ring_req = req; ring_setoid = sth; - ring_ext = constr_of params.(1); - ring_morph = constr_of params.(2); - ring_th = constr_of params.(0); + ring_ext = params.(1); + ring_morph = params.(2); + ring_th = params.(0); ring_cst_tac = cst_tac; ring_pow_tac = pow_tac; ring_lemma1 = lemma1; @@ -692,16 +723,11 @@ type 'constr ring_mod = | Sign_spec of Constrexpr.constr_expr | Div_spec of Constrexpr.constr_expr -let ic_coeff_spec = function - | Computational t -> Computational (ic t) - | Morphism t -> Morphism (ic t) - | Abstract -> Abstract - VERNAC ARGUMENT EXTEND ring_mod - | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ] + | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational (ic_unsafe eq_test)) ] | [ "abstract" ] -> [ Ring_kind Abstract ] - | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ] + | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism (ic_unsafe morph)) ] | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ] | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ] | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ] @@ -732,11 +758,11 @@ let process_ring_mods l = | Const_tac t -> set_once "tactic recognizing constants" cst_tac t | Pre_tac t -> set_once "preprocess tactic" pre t | Post_tac t -> set_once "postprocess tactic" post t - | Setoid(sth,ext) -> set_once "setoid" set (ic sth,ic ext) + | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext) | Pow_spec(t,spec) -> set_once "power" power (t,spec) | Sign_spec t -> set_once "sign" sign t | Div_spec t -> set_once "div" div t) l; - let k = match !kind with Some k -> ic_coeff_spec k | None -> Abstract in + let k = match !kind with Some k -> k | None -> Abstract in (k, !set, !cst_tac, !pre, !post, !power, !sign, !div) VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF @@ -762,10 +788,11 @@ let make_args_list rl t = | [] -> let (_,t1,t2) = dest_rel0 t in [t1;t2] | _ -> rl -let make_term_list carrier rl = - List.fold_right - (fun x l -> lapp coq_cons [|carrier;x;l|]) rl - (lapp coq_nil [|carrier|]) +let make_term_list env evd carrier rl = + let l = List.fold_right + (fun x l -> plapp evd coq_pcons [|carrier;x;l|]) rl + (plapp evd coq_pnil [|carrier|]) + in Typing.solve_evars env evd l let ltac_ring_structure e = let req = carg e.ring_req in @@ -786,12 +813,15 @@ let ring_lookup (f:glob_tactic_expr) lH rl t = Proofview.Goal.raw_enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let rl = make_args_list rl t in - let e = find_ring_structure env sigma rl in - let rl = carg (make_term_list e.ring_carrier rl) in - let lH = carg (make_hyp_list env lH) in - let ring = ltac_ring_structure e in - ltac_apply f (ring@[lH;rl]) + try (* find_ring_strucure can raise an exception *) + let evdref = ref sigma in + let rl = make_args_list rl t in + let e = find_ring_structure env sigma rl in + let rl = carg (make_term_list env evdref e.ring_carrier rl) in + let lH = carg (make_hyp_list env evdref lH) in + let ring = ltac_ring_structure e in + Proofview.tclTHEN (Proofview.V82.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl])) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end TACTIC EXTEND ring_lookup @@ -850,26 +880,26 @@ let _ = Redexpr.declare_reduction "simpl_field_expr" let afield_theory = my_constant "almost_field_theory" let field_theory = my_constant "field_theory" let sfield_theory = my_constant "semi_field_theory" -let af_ar = my_constant"AF_AR" -let f_r = my_constant"F_R" -let sf_sr = my_constant"SF_SR" -let dest_field env sigma th_spec = - let th_typ = Retyping.get_type_of env sigma th_spec in +let af_ar = my_reference"AF_AR" +let f_r = my_reference"F_R" +let sf_sr = my_reference"SF_SR" +let dest_field env evd th_spec = + let th_typ = Retyping.get_type_of env !evd th_spec in match kind_of_term th_typ with | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when eq_constr f (Lazy.force afield_theory) -> - let rth = lapp af_ar + when eq_constr_nounivs f (Lazy.force afield_theory) -> + let rth = plapp evd af_ar [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when eq_constr f (Lazy.force field_theory) -> + when eq_constr_nounivs f (Lazy.force field_theory) -> let rth = - lapp f_r + plapp evd f_r [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;div;inv;req|]) - when eq_constr f (Lazy.force sfield_theory) -> - let rth = lapp sf_sr + when eq_constr_nounivs f (Lazy.force sfield_theory) -> + let rth = plapp evd sf_sr [|r;zero;one;add;mul;div;inv;req;th_spec|] in (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth) | _ -> error "bad field structure" @@ -960,12 +990,12 @@ let ftheory_to_obj : field_info -> obj = subst_function = subst_th; classify_function = (fun x -> Substitute x) } -let field_equality r inv req = +let field_equality evd r inv req = match kind_of_term req with - | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) -> - mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|]) + | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) -> + mkApp(Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr,[|r;r;inv|]) | _ -> - let _setoid = setoid_of_relation (Global.env ()) r req in + let _setoid = setoid_of_relation (Global.env ()) evd r req in let signature = [Some (r,Some req)],Some(r,Some req) in let inv_m, inv_m_lem = try Rewrite.default_morphism signature inv @@ -973,36 +1003,41 @@ let field_equality r inv req = error "field inverse should be declared as a morphism" in inv_m_lem -let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odiv = +let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power sign odiv = check_required_library (cdir@["Field_tac"]); let env = Global.env() in - let sigma = Evd.empty in + let evd = ref sigma in let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) = - dest_field env sigma fth in - let (sth,ext) = build_setoid_params r add mul opp req eqth in + dest_field env evd fth in + let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in let eqth = Some(sth,ext) in - let _ = add_theory name rth eqth morphth cst_tac (None,None) power sign odiv in - let (pow_tac, pspec) = interp_power env power in - let sspec = interp_sign env sign in - let dspec = interp_div env odiv in - let inv_m = field_equality r inv req in + let _ = add_theory name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in + let (pow_tac, pspec) = interp_power env evd power in + let sspec = interp_sign env evd sign in + let dspec = interp_div env evd odiv in + let inv_m = field_equality evd r inv req in let rk = reflect_coeff morphth in - let params = - exec_tactic env 9 (field_ltac"field_lemmas") + let params,ctx = + exec_tactic env !evd 9 (field_ltac"field_lemmas") (List.map carg[sth;ext;inv_m;fth;pspec;sspec;dspec;rk]) in - let lemma1 = constr_of params.(3) in - let lemma2 = constr_of params.(4) in - let lemma3 = constr_of params.(5) in - let lemma4 = constr_of params.(6) in + let lemma1 = params.(3) in + let lemma2 = params.(4) in + let lemma3 = params.(5) in + let lemma4 = params.(6) in let cond_lemma = match inj with | Some thm -> mkApp(constr_of params.(8),[|thm|]) | None -> constr_of params.(7) in - let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") (Future.from_val (lemma1,Declareops.no_seff)) in - let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") (Future.from_val (lemma2,Declareops.no_seff)) in - let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") (Future.from_val (lemma3,Declareops.no_seff)) in - let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") (Future.from_val (lemma4,Declareops.no_seff)) in - let cond_lemma = decl_constant (Id.to_string name^"_lemma5") (Future.from_val (cond_lemma,Declareops.no_seff)) in + let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") + ctx (Future.from_val (lemma1,Declareops.no_seff)) in + let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") + ctx (Future.from_val (lemma2,Declareops.no_seff)) in + let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") + ctx (Future.from_val (lemma3,Declareops.no_seff)) in + let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") + ctx (Future.from_val (lemma4,Declareops.no_seff)) in + let cond_lemma = decl_constant (Id.to_string name^"_lemma5") + ctx (Future.from_val (cond_lemma,Declareops.no_seff)) in let cst_tac = interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = @@ -1053,12 +1088,12 @@ let process_field_mods l = set_once "tactic recognizing constants" cst_tac t | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t - | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic sth,ic ext) + | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext) | Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec) | Ring_mod(Sign_spec t) -> set_once "sign" sign t | Ring_mod(Div_spec t) -> set_once "div" div t - | Inject i -> set_once "infinite property" inj (ic i)) l; - let k = match !kind with Some k -> ic_coeff_spec k | None -> Abstract in + | Inject i -> set_once "infinite property" inj (ic_unsafe i)) l; + let k = match !kind with Some k -> k | None -> Abstract in (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div) VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF @@ -1094,12 +1129,15 @@ let field_lookup (f:glob_tactic_expr) lH rl t = Proofview.Goal.raw_enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let rl = make_args_list rl t in - let e = find_field_structure env sigma rl in - let rl = carg (make_term_list e.field_carrier rl) in - let lH = carg (make_hyp_list env lH) in - let field = ltac_field_structure e in - ltac_apply f (field@[lH;rl]) + try + let evdref = ref sigma in + let rl = make_args_list rl t in + let e = find_field_structure env sigma rl in + let rl = carg (make_term_list env evdref e.field_carrier rl) in + let lH = carg (make_hyp_list env evdref lH) in + let field = ltac_field_structure e in + Proofview.tclTHEN (Proofview.V82.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 790e1970b..5c060c3d6 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -37,9 +37,9 @@ let interp_ascii dloc p = let rec aux n p = if Int.equal n 0 then [] else let mp = p mod 2 in - GRef (dloc,if Int.equal mp 0 then glob_false else glob_true) + GRef (dloc,if Int.equal mp 0 then glob_false else glob_true,None) :: (aux (n-1) (p/2)) in - GApp (dloc,GRef(dloc,force glob_Ascii), aux 8 p) + GApp (dloc,GRef(dloc,force glob_Ascii,None), aux 8 p) let interp_ascii_string dloc s = let p = @@ -55,12 +55,12 @@ let interp_ascii_string dloc s = let uninterp_ascii r = let rec uninterp_bool_list n = function | [] when Int.equal n 0 -> 0 - | GRef (_,k)::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | GRef (_,k)::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l) + | GRef (_,k,_)::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l) + | GRef (_,k,_)::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l) | _ -> raise Non_closed_ascii in try let aux = function - | GApp (_,GRef (_,k),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l + | GApp (_,GRef (_,k,_),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l | _ -> raise Non_closed_ascii in Some (aux r) with @@ -76,4 +76,4 @@ let _ = Notation.declare_string_interpreter "char_scope" (ascii_path,ascii_module) interp_ascii_string - ([GRef (Loc.ghost,static_glob_Ascii)], uninterp_ascii_string, true) + ([GRef (Loc.ghost,static_glob_Ascii,None)], uninterp_ascii_string, true) diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index c3dad0a10..bad099d4f 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -30,8 +30,8 @@ let nat_of_int dloc n = strbrk "working with large numbers in nat (observed threshold " ++ strbrk "may vary from 5000 to 70000 depending on your system " ++ strbrk "limits and on the command executed)."); - let ref_O = GRef (dloc, glob_O) in - let ref_S = GRef (dloc, glob_S) in + let ref_O = GRef (dloc, glob_O, None) in + let ref_S = GRef (dloc, glob_S, None) in let rec mk_nat acc n = if n <> zero then mk_nat (GApp (dloc,ref_S, [acc])) (sub_1 n) @@ -50,8 +50,8 @@ let nat_of_int dloc n = exception Non_closed_number let rec int_of_nat = function - | GApp (_,GRef (_,s),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) - | GRef (_,z) when Globnames.eq_gr z glob_O -> zero + | GApp (_,GRef (_,s,_),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) + | GRef (_,z,_) when Globnames.eq_gr z glob_O -> zero | _ -> raise Non_closed_number let uninterp_nat p = @@ -67,4 +67,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,datatypes_module_name) nat_of_int - ([GRef (Loc.ghost,glob_S); GRef (Loc.ghost,glob_O)], uninterp_nat, true) + ([GRef (Loc.ghost,glob_S,None); GRef (Loc.ghost,glob_O,None)], uninterp_nat, true) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index 8e09c974a..a6b3d9038 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -83,9 +83,9 @@ exception Non_closed (* parses a *non-negative* integer (from bigint.ml) into an int31 wraps modulo 2^31 *) let int31_of_pos_bigint dloc n = - let ref_construct = GRef (dloc, int31_construct) in - let ref_0 = GRef (dloc, int31_0) in - let ref_1 = GRef (dloc, int31_1) in + let ref_construct = GRef (dloc, int31_construct, None) in + let ref_0 = GRef (dloc, int31_0, None) in + let ref_1 = GRef (dloc, int31_1, None) in let rec args counter n = if counter <= 0 then [] @@ -110,12 +110,12 @@ let bigint_of_int31 = let rec args_parsing args cur = match args with | [] -> cur - | (GRef (_,b))::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur) - | (GRef (_,b))::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur)) + | (GRef (_,b,_))::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur) + | (GRef (_,b,_))::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur)) | _ -> raise Non_closed in function - | GApp (_, GRef (_, c), args) when eq_gr c int31_construct -> args_parsing args zero + | GApp (_, GRef (_, c, _), args) when eq_gr c int31_construct -> args_parsing args zero | _ -> raise Non_closed let uninterp_int31 i = @@ -128,7 +128,7 @@ let uninterp_int31 i = let _ = Notation.declare_numeral_interpreter int31_scope (int31_path, int31_module) interp_int31 - ([GRef (Loc.ghost, int31_construct)], + ([GRef (Loc.ghost, int31_construct, None)], uninterp_int31, true) @@ -159,8 +159,8 @@ let height bi = (* n must be a non-negative integer (from bigint.ml) *) let word_of_pos_bigint dloc hght n = - let ref_W0 = GRef (dloc, zn2z_W0) in - let ref_WW = GRef (dloc, zn2z_WW) in + let ref_W0 = GRef (dloc, zn2z_W0, None) in + let ref_WW = GRef (dloc, zn2z_WW, None) in let rec decomp hgt n = if hgt <= 0 then int31_of_pos_bigint dloc n @@ -176,7 +176,7 @@ let word_of_pos_bigint dloc hght n = let bigN_of_pos_bigint dloc n = let h = height n in - let ref_constructor = GRef (dloc, bigN_constructor h) in + let ref_constructor = GRef (dloc, bigN_constructor h, None) in let word = word_of_pos_bigint dloc h n in let args = if h < n_inlined then [word] @@ -199,14 +199,14 @@ let interp_bigN dloc n = let bigint_of_word = let rec get_height rc = match rc with - | GApp (_,GRef(_,c), [_;lft;rght]) when eq_gr c zn2z_WW -> + | GApp (_,GRef(_,c,_), [_;lft;rght]) when eq_gr c zn2z_WW -> 1+max (get_height lft) (get_height rght) | _ -> 0 in let rec transform hght rc = match rc with - | GApp (_,GRef(_,c),_) when eq_gr c zn2z_W0-> zero - | GApp (_,GRef(_,c), [_;lft;rght]) when eq_gr c zn2z_WW-> + | GApp (_,GRef(_,c,_),_) when eq_gr c zn2z_W0-> zero + | GApp (_,GRef(_,c,_), [_;lft;rght]) when eq_gr c zn2z_WW-> let new_hght = hght-1 in add (mult (rank new_hght) (transform new_hght lft)) @@ -236,7 +236,7 @@ let uninterp_bigN rc = let bigN_list_of_constructors = let rec build i = if i < n_inlined+1 then - GRef (Loc.ghost, bigN_constructor i)::(build (i+1)) + GRef (Loc.ghost, bigN_constructor i,None)::(build (i+1)) else [] in @@ -253,8 +253,8 @@ let _ = Notation.declare_numeral_interpreter bigN_scope (*** Parsing for bigZ in digital notation ***) let interp_bigZ dloc n = - let ref_pos = GRef (dloc, bigZ_pos) in - let ref_neg = GRef (dloc, bigZ_neg) in + let ref_pos = GRef (dloc, bigZ_pos, None) in + let ref_neg = GRef (dloc, bigZ_neg, None) in if is_pos_or_zero n then GApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n]) else @@ -262,8 +262,8 @@ let interp_bigZ dloc n = (* pretty printing functions for bigZ *) let bigint_of_bigZ = function - | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigZ_pos -> bigint_of_bigN one_arg - | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigZ_neg -> + | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigZ_pos -> bigint_of_bigN one_arg + | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigZ_neg -> let opp_val = bigint_of_bigN one_arg in if equal opp_val zero then raise Non_closed @@ -282,19 +282,19 @@ let uninterp_bigZ rc = let _ = Notation.declare_numeral_interpreter bigZ_scope (bigZ_path, bigZ_module) interp_bigZ - ([GRef (Loc.ghost, bigZ_pos); - GRef (Loc.ghost, bigZ_neg)], + ([GRef (Loc.ghost, bigZ_pos, None); + GRef (Loc.ghost, bigZ_neg, None)], uninterp_bigZ, true) (*** Parsing for bigQ in digital notation ***) let interp_bigQ dloc n = - let ref_z = GRef (dloc, bigQ_z) in + let ref_z = GRef (dloc, bigQ_z, None) in GApp (dloc, ref_z, [interp_bigZ dloc n]) let uninterp_bigQ rc = try match rc with - | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigQ_z -> + | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigQ_z -> Some (bigint_of_bigZ one_arg) | _ -> None (* we don't pretty-print yet fractions *) with Non_closed -> None @@ -303,5 +303,5 @@ let uninterp_bigQ rc = let _ = Notation.declare_numeral_interpreter bigQ_scope (bigQ_path, bigQ_module) interp_bigQ - ([GRef (Loc.ghost, bigQ_z)], uninterp_bigQ, + ([GRef (Loc.ghost, bigQ_z, None)], uninterp_bigQ, true) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 545f205db..dac70c673 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -42,24 +42,24 @@ let four = mult_2 two (* Unary representation of strictly positive numbers *) let rec small_r dloc n = - if equal one n then GRef (dloc, glob_R1) - else GApp(dloc,GRef (dloc,glob_Rplus), - [GRef (dloc, glob_R1);small_r dloc (sub_1 n)]) + if equal one n then GRef (dloc, glob_R1, None) + else GApp(dloc,GRef (dloc,glob_Rplus, None), + [GRef (dloc, glob_R1, None);small_r dloc (sub_1 n)]) let r_of_posint dloc n = - let r1 = GRef (dloc, glob_R1) in + let r1 = GRef (dloc, glob_R1, None) in let r2 = small_r dloc two in let rec r_of_pos n = if less_than n four then small_r dloc n else let (q,r) = div2_with_rest n in - let b = GApp(dloc,GRef(dloc,glob_Rmult),[r2;r_of_pos q]) in - if r then GApp(dloc,GRef(dloc,glob_Rplus),[r1;b]) else b in - if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0) + let b = GApp(dloc,GRef(dloc,glob_Rmult,None),[r2;r_of_pos q]) in + if r then GApp(dloc,GRef(dloc,glob_Rplus,None),[r1;b]) else b in + if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0,None) let r_of_int dloc z = if is_strictly_neg z then - GApp (dloc, GRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)]) + GApp (dloc, GRef(dloc,glob_Ropp,None), [r_of_posint dloc (neg z)]) else r_of_posint dloc z @@ -71,33 +71,33 @@ let bignat_of_r = (* for numbers > 1 *) let rec bignat_of_pos = function (* 1+1 *) - | GApp (_,GRef (_,p), [GRef (_,o1); GRef (_,o2)]) + | GApp (_,GRef (_,p,_), [GRef (_,o1,_); GRef (_,o2,_)]) when Globnames.eq_gr p glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 -> two (* 1+(1+1) *) - | GApp (_,GRef (_,p1), [GRef (_,o1); - GApp(_,GRef (_,p2),[GRef(_,o2);GRef(_,o3)])]) + | GApp (_,GRef (_,p1,_), [GRef (_,o1,_); + GApp(_,GRef (_,p2,_),[GRef(_,o2,_);GRef(_,o3,_)])]) when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 && Globnames.eq_gr o3 glob_R1 -> three (* (1+1)*b *) - | GApp (_,GRef (_,p), [a; b]) when Globnames.eq_gr p glob_Rmult -> + | GApp (_,GRef (_,p,_), [a; b]) when Globnames.eq_gr p glob_Rmult -> if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number; mult_2 (bignat_of_pos b) (* 1+(1+1)*b *) - | GApp (_,GRef (_,p1), [GRef (_,o); GApp (_,GRef (_,p2),[a;b])]) + | GApp (_,GRef (_,p1,_), [GRef (_,o,_); GApp (_,GRef (_,p2,_),[a;b])]) when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rmult && Globnames.eq_gr o glob_R1 -> if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number; add_1 (mult_2 (bignat_of_pos b)) | _ -> raise Non_closed_number in let bignat_of_r = function - | GRef (_,a) when Globnames.eq_gr a glob_R0 -> zero - | GRef (_,a) when Globnames.eq_gr a glob_R1 -> one + | GRef (_,a,_) when Globnames.eq_gr a glob_R0 -> zero + | GRef (_,a,_) when Globnames.eq_gr a glob_R1 -> one | r -> bignat_of_pos r in bignat_of_r let bigint_of_r = function - | GApp (_,GRef (_,o), [a]) when Globnames.eq_gr o glob_Ropp -> + | GApp (_,GRef (_,o,_), [a]) when Globnames.eq_gr o glob_Ropp -> let n = bignat_of_r a in if Bigint.equal n zero then raise Non_closed_number; neg n @@ -109,11 +109,12 @@ let uninterp_r p = with Non_closed_number -> None +let mkGRef gr = GRef (Loc.ghost,gr,None) + let _ = Notation.declare_numeral_interpreter "R_scope" (r_path,["Coq";"Reals";"Rdefinitions"]) r_of_int - ([GRef(Loc.ghost,glob_Ropp);GRef(Loc.ghost,glob_R0); - GRef(Loc.ghost,glob_Rplus);GRef(Loc.ghost,glob_Rmult); - GRef(Loc.ghost,glob_R1)], + (List.map mkGRef + [glob_Ropp;glob_R0;glob_Rplus;glob_Rmult;glob_R1], uninterp_r, false) diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index 54206b453..2e696f391 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -32,8 +32,8 @@ open Lazy let interp_string dloc s = let le = String.length s in let rec aux n = - if n = le then GRef (dloc, force glob_EmptyString) else - GApp (dloc,GRef (dloc, force glob_String), + if n = le then GRef (dloc, force glob_EmptyString, None) else + GApp (dloc,GRef (dloc, force glob_String, None), [interp_ascii dloc (int_of_char s.[n]); aux (n+1)]) in aux 0 @@ -41,11 +41,11 @@ let uninterp_string r = try let b = Buffer.create 16 in let rec aux = function - | GApp (_,GRef (_,k),[a;s]) when eq_gr k (force glob_String) -> + | GApp (_,GRef (_,k,_),[a;s]) when eq_gr k (force glob_String) -> (match uninterp_ascii a with | Some c -> Buffer.add_char b (Char.chr c); aux s | _ -> raise Non_closed_string) - | GRef (_,z) when eq_gr z (force glob_EmptyString) -> + | GRef (_,z,_) when eq_gr z (force glob_EmptyString) -> Some (Buffer.contents b) | _ -> raise Non_closed_string @@ -57,6 +57,6 @@ let _ = Notation.declare_string_interpreter "string_scope" (string_path,["Coq";"Strings";"String"]) interp_string - ([GRef (Loc.ghost,static_glob_String); - GRef (Loc.ghost,static_glob_EmptyString)], + ([GRef (Loc.ghost,static_glob_String,None); + GRef (Loc.ghost,static_glob_EmptyString,None)], uninterp_string, true) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 67e54c017..5131a5f38 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -41,9 +41,9 @@ let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH let pos_of_bignat dloc x = - let ref_xI = GRef (dloc, glob_xI) in - let ref_xH = GRef (dloc, glob_xH) in - let ref_xO = GRef (dloc, glob_xO) in + let ref_xI = GRef (dloc, glob_xI, None) in + let ref_xH = GRef (dloc, glob_xH, None) in + let ref_xO = GRef (dloc, glob_xO, None) in let rec pos_of x = match div2_with_rest x with | (q,false) -> GApp (dloc, ref_xO,[pos_of q]) @@ -65,9 +65,9 @@ let interp_positive dloc n = (**********************************************************************) let rec bignat_of_pos = function - | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) - | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (_, a) when Globnames.eq_gr a glob_xH -> Bigint.one + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) + | GRef (_, a, _) when Globnames.eq_gr a glob_xH -> Bigint.one | _ -> raise Non_closed_number let uninterp_positive p = @@ -83,9 +83,9 @@ let uninterp_positive p = let _ = Notation.declare_numeral_interpreter "positive_scope" (positive_path,binnums) interp_positive - ([GRef (Loc.ghost, glob_xI); - GRef (Loc.ghost, glob_xO); - GRef (Loc.ghost, glob_xH)], + ([GRef (Loc.ghost, glob_xI, None); + GRef (Loc.ghost, glob_xO, None); + GRef (Loc.ghost, glob_xH, None)], uninterp_positive, true) @@ -104,9 +104,9 @@ let n_path = make_path binnums "N" let n_of_binnat dloc pos_or_neg n = if not (Bigint.equal n zero) then - GApp(dloc, GRef (dloc,glob_Npos), [pos_of_bignat dloc n]) + GApp(dloc, GRef (dloc,glob_Npos,None), [pos_of_bignat dloc n]) else - GRef (dloc, glob_N0) + GRef (dloc, glob_N0, None) let error_negative dloc = user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".") @@ -120,8 +120,8 @@ let n_of_int dloc n = (**********************************************************************) let bignat_of_n = function - | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a - | GRef (_, a) when Globnames.eq_gr a glob_N0 -> Bigint.zero + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a + | GRef (_, a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero | _ -> raise Non_closed_number let uninterp_n p = @@ -134,8 +134,8 @@ let uninterp_n p = let _ = Notation.declare_numeral_interpreter "N_scope" (n_path,binnums) n_of_int - ([GRef (Loc.ghost, glob_N0); - GRef (Loc.ghost, glob_Npos)], + ([GRef (Loc.ghost, glob_N0, None); + GRef (Loc.ghost, glob_Npos, None)], uninterp_n, true) @@ -157,18 +157,18 @@ let z_of_int dloc n = if not (Bigint.equal n zero) then let sgn, n = if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - GApp(dloc, GRef (dloc,sgn), [pos_of_bignat dloc n]) + GApp(dloc, GRef (dloc,sgn,None), [pos_of_bignat dloc n]) else - GRef (dloc, glob_ZERO) + GRef (dloc, glob_ZERO, None) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) let bigint_of_z = function - | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a - | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) - | GRef (_, a) when Globnames.eq_gr a glob_ZERO -> Bigint.zero + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) + | GRef (_, a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number let uninterp_z p = @@ -182,8 +182,8 @@ let uninterp_z p = let _ = Notation.declare_numeral_interpreter "Z_scope" (z_path,binnums) z_of_int - ([GRef (Loc.ghost, glob_ZERO); - GRef (Loc.ghost, glob_POS); - GRef (Loc.ghost, glob_NEG)], + ([GRef (Loc.ghost, glob_ZERO, None, None); + GRef (Loc.ghost, glob_POS, None, None); + GRef (Loc.ghost, glob_NEG, None, None)], uninterp_z, true) diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index bf46065d0..bbaef1e70 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -190,6 +190,7 @@ module CPropRetyping = let typeur sigma metamap = let rec type_of env cstr= match Term.kind_of_term cstr with + | T.Proj _ -> assert false | T.Meta n -> (try T.strip_outer_cast (Int.List.assoc n metamap) with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term")) @@ -202,9 +203,7 @@ let typeur sigma metamap = ty with Not_found -> Errors.anomaly ~label:"type_of" (str "variable " ++ Id.print id ++ str " unbound")) - | T.Const c -> - let cb = Environ.lookup_constant c env in - Typeops.type_of_constant_type env (cb.Declarations.const_type) + | T.Const c -> Typeops.type_of_constant_in env c | T.Evar ev -> Evd.existential_type sigma ev | T.Ind ind -> Inductiveops.type_of_inductive env ind | T.Construct cstr -> Inductiveops.type_of_constructor env cstr @@ -355,7 +354,7 @@ Pp.msg_debug (Pp.(++) (Pp.str "BUG: this subterm was not visited during the doub {DoubleTypeInference.synthesized = Reductionops.nf_beta evar_map (CPropRetyping.get_type_of env evar_map - (Termops.refresh_universes tt)) ; + ((* Termops.refresh_universes *) tt)) ; DoubleTypeInference.expected = None} in let innersort = @@ -484,7 +483,8 @@ print_endline "PASSATO" ; flush stdout ; (* Now that we have all the auxiliary functions we *) (* can finally proceed with the main case analysis. *) match Term.kind_of_term tt with - Term.Rel n -> + | Term.Proj _ -> assert false + | Term.Rel n -> let id = match List.nth (Environ.rel_context env) (n - 1) with (Names.Name id,_,_) -> id @@ -670,7 +670,7 @@ print_endline "PASSATO" ; flush stdout ; explicit_substitute_and_eta_expand_if_required h (Array.to_list t) t' compute_result_if_eta_expansion_not_required - | Term.Const kn -> + | Term.Const (kn,u) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort && expected_available then add_inner_type fresh_id'' ; @@ -681,7 +681,7 @@ print_endline "PASSATO" ; flush stdout ; explicit_substitute_and_eta_expand_if_required tt [] (List.map snd subst') compute_result_if_eta_expansion_not_required - | Term.Ind (kn,i) -> + | Term.Ind ((kn,i),u) -> let compute_result_if_eta_expansion_not_required _ _ = Acic.AInd (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i) in @@ -689,7 +689,7 @@ print_endline "PASSATO" ; flush stdout ; explicit_substitute_and_eta_expand_if_required tt [] (List.map snd subst') compute_result_if_eta_expansion_not_required - | Term.Construct ((kn,i),j) -> + | Term.Construct (((kn,i),j),u) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort && expected_available then add_inner_type fresh_id'' ; diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index d54308165..c8717e008 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -64,7 +64,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = T.Meta n -> Errors.error "DoubleTypeInference.double_type_of: found a non-instanciated goal" - + | T.Proj _ -> assert false | T.Evar ((n,l) as ev) -> let ty = Unshare.unshare (Evd.existential_type sigma ev) in let jty = execute env sigma ty None in @@ -99,7 +99,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = Typeops.judge_of_variable env id | T.Const c -> - E.make_judge cstr (Typeops.type_of_constant env c) + E.make_judge cstr (fst (Typeops.type_of_constant env c)) | T.Ind ind -> E.make_judge cstr (Inductiveops.type_of_inductive env ind) @@ -112,15 +112,14 @@ let double_type_of env sigma cstr expectedty subterms_to_types = Reduction.whd_betadeltaiota env (Retyping.get_type_of env sigma c) in let cj = execute env sigma c (Some expectedtype) in let pj = execute env sigma p None in - let (expectedtypes,_,_) = + let (expectedtypes,_) = let indspec = Inductive.find_rectype env cj.Environ.uj_type in Inductive.type_case_branches env indspec pj cj.Environ.uj_val in let lfj = execute_array env sigma lf (Array.map (function x -> Some x) expectedtypes) in - let (j,_) = Typeops.judge_of_case env ci pj cj lfj in - j + Typeops.judge_of_case env ci pj cj lfj | T.Fix ((vn,i as vni),recdef) -> let (_,tys,_ as recdef') = execute_recdef env sigma recdef in @@ -141,10 +140,10 @@ let double_type_of env sigma cstr expectedty subterms_to_types = (*CSC: again once Judicael will introduce his non-bugged algebraic *) (*CSC: universes. *) (try - Typeops.judge_of_type u + (*FIXME*) (Typeops.judge_of_type u) with _ -> (* Successor of a non universe-variable universe anomaly *) Pp.msg_warning (Pp.str "Universe refresh performed!!!"); - Typeops.judge_of_type (Termops.new_univ ()) + (*FIXME*) (Typeops.judge_of_type (Universes.new_univ Names.empty_dirpath)) ) | T.App (f,args) -> @@ -165,7 +164,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = Array.of_list (aux j.Environ.uj_type (Array.to_list args)) in let jl = execute_array env sigma args expected_args in - let (j,_) = Typeops.judge_of_apply env j jl in + let j = Typeops.judge_of_apply env j jl in j | T.Lambda (name,c1,c2) -> @@ -212,7 +211,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = let cj = execute env sigma c (Some (Reductionops.nf_beta sigma t)) in let tj = execute env sigma t None in let tj = type_judgment env sigma tj in - let j, _ = Typeops.judge_of_cast env cj k tj in + let j = Typeops.judge_of_cast env cj k tj in j in let synthesized = E.j_type judgement in diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 5f26e2bac..3d655920b 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -175,16 +175,17 @@ let find_hyps t = | Term.Meta _ | Term.Evar _ | Term.Sort _ -> l + | Term.Proj _ -> ignore(Errors.todo "Proj in find_hyps"); assert false | Term.Cast (te,_, ty) -> aux (aux l te) ty | Term.Prod (_,s,t) -> aux (aux l s) t | Term.Lambda (_,s,t) -> aux (aux l s) t | Term.LetIn (_,s,_,t) -> aux (aux l s) t | Term.App (he,tl) -> Array.fold_left (fun i x -> aux i x) (aux l he) tl - | Term.Const con -> + | Term.Const (con, _) -> let hyps = (Global.lookup_constant con).Declarations.const_hyps in map_and_filter l hyps @ l - | Term.Ind ind - | Term.Construct (ind,_) -> + | Term.Ind (ind,_) + | Term.Construct ((ind,_),_) -> let hyps = (fst (Global.lookup_inductive ind)).Declarations.mind_hyps in map_and_filter l hyps @ l | Term.Case (_,t1,t2,b) -> @@ -243,8 +244,8 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite = let {Declarations.mind_consnames=consnames ; Declarations.mind_typename=typename } = p in - let arity = Inductive.type_of_inductive (Global.env()) (mib,p) in - let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in + let arity = Inductive.type_of_inductive (Global.env()) ((mib,p),Univ.Instance.empty)(*FIXME*) in + let lc = Inductiveops.arities_of_constructors (Global.env ()) ((sp,!tyno),Univ.Instance.empty)(*FIXME*) in let cons = (Array.fold_right (fun (name,lc) i -> (name,lc)::i) (Array.mapi @@ -379,7 +380,7 @@ let print internal glob_ref kind xml_library_root = let val0 = Declareops.body_of_constant cb in let typ = cb.Declarations.const_type in let hyps = cb.Declarations.const_hyps in - let typ = Typeops.type_of_constant_type (Global.env()) typ in + let typ = (* Typeops.type_of_constant_type (Global.env()) *) typ in Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps | Globnames.IndRef (kn,_) -> let mib = Global.lookup_mind kn in |