diff options
54 files changed, 407 insertions, 407 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 4f4cc5560..7800dff01 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -28,7 +28,7 @@ let check_constant_declaration env kn cb = (* let env = add_constraints cb.const_constraints env in*) (match cb.const_type with ty -> - let env' = add_constraints cb.const_constraints env in + let env' = add_constraints (Future.force cb.const_constraints) env in let _ = infer_type env' ty in (match body_of_constant cb with | Some bd -> @@ -69,13 +69,13 @@ let rec check_module env mp mb = {typ_mp=mp; typ_expr=sign; typ_expr_alg=None; - typ_constraints=Univ.empty_constraint; + typ_constraints=Univ.Constraint.empty; typ_delta = mb.mod_delta;} and mtb2 = {typ_mp=mp; typ_expr=mb.mod_type; typ_expr_alg=None; - typ_constraints=Univ.empty_constraint; + typ_constraints=Univ.Constraint.empty; typ_delta = mb.mod_delta;} in let env = add_module_type mp mtb1 env in diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 857f75ed6..ed6ded8e1 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -448,7 +448,7 @@ type vernac_type = | VtStm of vernac_control * vernac_part_of_script | VtUnknown and vernac_qed_type = VtKeep | VtDrop (* Qed/Admitted, Abort *) -and vernac_start = string * opacity_guarantee * Id.t list +and vernac_start = string * opacity_guarantee * Id.t list * polymorphic and vernac_sideff_type = Id.t list and vernac_is_alias = bool and vernac_part_of_script = bool diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 7d49e452c..35577239b 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -193,7 +193,8 @@ type constraints_addition = let add_constraints cst senv = match cst with - | Later fc -> {senv with future_cst = fc :: senv.future_cst} + | Later fc -> + {senv with future_cst = fc :: senv.future_cst} | Now cst -> { senv with env = Environ.add_constraints cst senv.env; diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 352ef40d9..a7f2125a7 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -24,7 +24,7 @@ open Entries open Typeops open Fast_typeops -let debug = false +let debug = true let prerr_endline = if debug then prerr_endline else fun _ -> () diff --git a/library/declare.ml b/library/declare.ml index 41f50753f..820e72369 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -253,7 +253,10 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) = let cd = (* We deal with side effects of non-opaque constants *) match cd with | Entries.DefinitionEntry ({ - const_entry_opaque = false; const_entry_body = bo } as de) -> + const_entry_opaque = false; const_entry_body = bo } as de) + | Entries.DefinitionEntry ({ + const_entry_polymorphic = true; const_entry_body = bo } as de) + -> let pt, seff = Future.force bo in if Declareops.side_effects_is_empty seff then cd else begin diff --git a/library/global.ml b/library/global.ml index c56bc9e77..16b07db25 100644 --- a/library/global.ml +++ b/library/global.ml @@ -160,6 +160,30 @@ let type_of_global_unsafe r = let inst = Univ.UContext.instance mib.Declarations.mind_universes in Inductive.type_of_constructor (cstr,inst) specif +let type_of_global_in_context env r = + let open Declarations in + match r with + | VarRef id -> Environ.named_type id env, Univ.UContext.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + let univs = + if cb.const_polymorphic then Future.force cb.const_universes + else Univ.UContext.empty + in cb.Declarations.const_type, univs + | IndRef ind -> + let (mib, oib) = Inductive.lookup_mind_specif env ind in + let univs = + if mib.mind_polymorphic then mib.mind_universes + else Univ.UContext.empty + in oib.Declarations.mind_arity.Declarations.mind_user_arity, univs + | ConstructRef cstr -> + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + let univs = + if mib.mind_polymorphic then mib.mind_universes + else Univ.UContext.empty + in + let inst = Univ.UContext.instance univs in + Inductive.type_of_constructor (cstr,inst) specif, univs let is_polymorphic r = let env = env() in diff --git a/library/global.mli b/library/global.mli index b6825ffa5..410be961b 100644 --- a/library/global.mli +++ b/library/global.mli @@ -108,7 +108,8 @@ val join_safe_environment : unit -> unit val is_polymorphic : Globnames.global_reference -> bool -(* val type_of_global : Globnames.global_reference -> types Univ.in_universe_context_set *) +val type_of_global_in_context : Environ.env -> + Globnames.global_reference -> Constr.types Univ.in_universe_context val type_of_global_unsafe : Globnames.global_reference -> Constr.types (** {6 Retroknowledge } *) diff --git a/library/universes.ml b/library/universes.ml index 79286792d..c7009b400 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -60,7 +60,7 @@ let fresh_instance_from ctx = let fresh_constant_instance env c = let cb = lookup_constant c env in if cb.Declarations.const_polymorphic then - let (inst,_), ctx = fresh_instance_from (Future.join cb.Declarations.const_universes) in + let (inst,_), ctx = fresh_instance_from (Future.force cb.Declarations.const_universes) in ((c, inst), ctx) else ((c,Instance.empty), ContextSet.empty) @@ -94,7 +94,20 @@ let fresh_global_instance env gr = let constr_of_global gr = let c, ctx = fresh_global_instance (Global.env ()) gr in - Global.push_context_set ctx; c + if not (Univ.ContextSet.is_empty ctx) then + if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then + (* Should be an error as we might forget constraints, allow for now + to make firstorder work with "using" clauses *) + c + else raise (Invalid_argument + ("constr_of_global: globalization of polymorphic reference " ^ + Pp.string_of_ppcmds (Nametab.pr_global_env Id.Set.empty gr) ^ + " would forget universes.")) + else c + +let unsafe_constr_of_global gr = + let c, ctx = fresh_global_instance (Global.env ()) gr in + c let constr_of_global_univ (gr,u) = match gr with @@ -132,7 +145,7 @@ let type_of_reference env r = | ConstRef c -> let cb = Environ.lookup_constant c env in if cb.const_polymorphic then - let (inst, subst), ctx = fresh_instance_from (Future.join cb.const_universes) in + let (inst, subst), ctx = fresh_instance_from (Future.force cb.const_universes) in Vars.subst_univs_constr subst cb.const_type, ctx else cb.const_type, ContextSet.empty diff --git a/library/universes.mli b/library/universes.mli index 47876269a..fb662d7a3 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -136,12 +136,19 @@ val normalize_universe_opt_subst : universe_opt_subst ref -> val normalize_universe_subst : universe_subst ref -> (universe -> universe) -(** Create a fresh global in the global environment, shouldn't be done while - building polymorphic values as the constraints are added to the global - environment already. *) +(** Create a fresh global in the global environment, without side effects. + BEWARE: this raises an ANOMALY on polymorphic constants/inductives: + the constraints should be properly added to an evd. + See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for + the proper way to get a fresh copy of a global reference. *) val constr_of_global : Globnames.global_reference -> constr +(** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic + reference by building a "dummy" universe instance that is not recorded + anywhere. The constraints are forgotten as well. DO NOT USE in new code. *) +val unsafe_constr_of_global : Globnames.global_reference -> constr + val type_of_global : Globnames.global_reference -> types in_universe_context_set (** Full universes substitutions into terms *) diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4 index 2354aa332..061f7ba5d 100644 --- a/parsing/g_obligations.ml4 +++ b/parsing/g_obligations.ml4 @@ -54,7 +54,7 @@ GEXTEND Gram open Obligations -let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater) +let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[],false), VtLater) VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl | [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] -> diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 563148872..9ae8fcbf6 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -78,7 +78,8 @@ let gen_ground_tac flag taco ids bases gl= | None-> snd (default_solver ()) in let startseq gl= let seq=empty_seq !ground_depth in - extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in + let seq,gl = extend_with_ref_list ids seq gl in + extend_with_auto_hints bases seq gl in let result=ground_tac (Proofview.V82.of_tactic solver) startseq gl in qflag:=backup;result with reraise -> qflag:=backup;raise reraise diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index e0f4fa95f..3faf7f802 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -119,5 +119,6 @@ let ground_tac solver startseq gl= end with Heap.EmptyHeap->solver end gl in - wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl + let seq, gl' = startseq gl in + wrap (List.length (pf_hyps gl)) true (toptac []) seq gl' diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli index 8b2ba20c1..f4a6ff48a 100644 --- a/plugins/firstorder/ground.mli +++ b/plugins/firstorder/ground.mli @@ -7,5 +7,5 @@ (************************************************************************) val ground_tac: Tacmach.tactic -> - (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic + (Proof_type.goal Tacmach.sigma -> Sequent.t * Proof_type.goal Tacmach.sigma) -> Tacmach.tactic diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index c6db6a49f..11b120c41 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -101,14 +101,12 @@ 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 mk_open_instance id idc gl m t= let env=pf_env gl in let evmap=Refiner.project gl in let var_id= if id==dummy_id then dummy_bvid else - let typ=pf_type_of gl (constr_of_global id) in + let typ=pf_type_of gl idc in (* since we know we will get a product, reduction is not too expensive *) let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in @@ -146,9 +144,10 @@ let left_instance_tac (inst,id) continue seq= tclTHENS (Proofview.V82.of_tactic (cut dom)) [tclTHENLIST [Proofview.V82.of_tactic introf; + pf_constr_of_global id (fun idc -> (fun gls->generalize - [mkApp(constr_of_global id, - [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls); + [mkApp(idc, + [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls)); Proofview.V82.of_tactic introf; tclSOLVE [wrap 1 false continue (deepen (record (id,None) seq))]]; @@ -159,14 +158,16 @@ let left_instance_tac (inst,id) continue seq= else let special_generalize= if m>0 then - fun gl-> - let (rc,ot)= mk_open_instance id gl m t in - let gt= - it_mkLambda_or_LetIn - (mkApp(constr_of_global id,[|ot|])) rc in - generalize [gt] gl + pf_constr_of_global id (fun idc -> + fun gl-> + let (rc,ot) = mk_open_instance id idc gl m t in + let gt= + it_mkLambda_or_LetIn + (mkApp(idc,[|ot|])) rc in + generalize [gt] gl) else - generalize [mkApp(constr_of_global id,[|t|])] + pf_constr_of_global id (fun idc -> + generalize [mkApp(idc,[|t|])]) in tclTHENLIST [special_generalize; diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 31a1e6cb0..996deb8c5 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -53,19 +53,19 @@ let clear_global=function VarRef id->clear [id] | _->tclIDTAC -let constr_of_global = Universes.constr_of_global (* connection rules *) let axiom_tac t seq= - try exact_no_check (constr_of_global (find_left t seq)) + try pf_constr_of_global (find_left t seq) exact_no_check with Not_found->tclFAIL 0 (Pp.str "No axiom link") let ll_atom_tac a backtrack id continue seq= tclIFTHENELSE (try tclTHENLIST - [generalize [mkApp(constr_of_global id, - [|constr_of_global (find_left a seq)|])]; + [pf_constr_of_global (find_left a seq) (fun left -> + pf_constr_of_global id (fun id -> + generalize [mkApp(id, [|left|])])); clear_global id; Proofview.V82.of_tactic intro] with Not_found->tclFAIL 0 (Pp.str "No link")) @@ -92,7 +92,7 @@ let left_and_tac ind backtrack id continue seq gls= let n=(construct_nhyps ind gls).(0) in tclIFTHENELSE (tclTHENLIST - [Proofview.V82.of_tactic (simplest_elim (constr_of_global id)); + [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim); clear_global id; tclDO n (Proofview.V82.of_tactic intro)]) (wrap n false continue seq) @@ -106,12 +106,12 @@ let left_or_tac ind backtrack id continue seq gls= tclDO n (Proofview.V82.of_tactic intro); wrap n false continue seq] in tclIFTHENSVELSE - (Proofview.V82.of_tactic (simplest_elim (constr_of_global id))) + (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)) (Array.map f v) backtrack gls let left_false_tac id= - Proofview.V82.of_tactic (simplest_elim (constr_of_global id)) + Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim) (* left arrow connective rules *) @@ -120,29 +120,28 @@ let left_false_tac id= 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= + (* construire le terme H->B, le generaliser etc *) + let myterm idc i= let rc=rcs.(i) in let p=List.length rc 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 - it_mkLambda_or_LetIn head rc in + let head=mkApp ((lift p idc),[|capply|]) in + it_mkLambda_or_LetIn head rc in let lp=Array.length rcs in - let newhyps=List.init lp myterm in + let newhyps idc =List.init lp (myterm idc) in tclIFTHENELSE (tclTHENLIST - [generalize newhyps; + [pf_constr_of_global id (fun idc -> generalize (newhyps idc)); clear_global id; tclDO lp (Proofview.V82.of_tactic intro)]) (wrap lp false continue seq) backtrack gl let ll_arrow_tac a b c backtrack id continue seq= let cc=mkProd(Anonymous,a,(lift 1 b)) in - let d=mkLambda (Anonymous,b, - mkApp ((constr_of_global id), - [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in + let d idc =mkLambda (Anonymous,b, + mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in tclORELSE (tclTHENS (Proofview.V82.of_tactic (cut c)) [tclTHENLIST @@ -150,9 +149,9 @@ let ll_arrow_tac a b c backtrack id continue seq= clear_global id; wrap 1 false continue seq]; tclTHENS (Proofview.V82.of_tactic (cut cc)) - [exact_no_check (constr_of_global id); + [pf_constr_of_global id exact_no_check; tclTHENLIST - [generalize [d]; + [pf_constr_of_global id (fun idc -> generalize [d idc]); clear_global id; Proofview.V82.of_tactic introf; Proofview.V82.of_tactic introf; @@ -175,7 +174,7 @@ let forall_tac backtrack continue seq= let left_exists_tac ind backtrack id continue seq gls= let n=(construct_nhyps ind gls).(0) in tclIFTHENELSE - (Proofview.V82.of_tactic (simplest_elim (constr_of_global id))) + (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)) (tclTHENLIST [clear_global id; tclDO n (Proofview.V82.of_tactic intro); (wrap (n-1) false continue seq)]) @@ -187,10 +186,11 @@ let ll_forall_tac prod backtrack id continue seq= (tclTHENS (Proofview.V82.of_tactic (cut prod)) [tclTHENLIST [Proofview.V82.of_tactic intro; + pf_constr_of_global id (fun idc -> (fun gls-> let id0=pf_nth_hyp_id gls 1 in - let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in - tclTHEN (generalize [term]) (clear [id0]) gls); + let term=mkApp(idc,[|mkVar(id0)|]) in + tclTHEN (generalize [term]) (clear [id0]) gls)); clear_global id; Proofview.V82.of_tactic intro; tclCOMPLETE (wrap 1 false continue (deepen seq))]; diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index c0e5c7e58..43bb6dbbf 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -196,13 +196,13 @@ let expand_constructor_hints = | gr -> [gr]) -let extend_with_ref_list l seq gl= +let extend_with_ref_list l seq gl = let l = expand_constructor_hints l in - let f gr seq= - let c=Universes.constr_of_global gr in + let f gr (seq,gl) = + let gl, c = pf_eapply Evd.fresh_global gl gr in let typ=(pf_type_of gl c) in - add_formula Hyp gr typ seq gl in - List.fold_right f l seq + (add_formula Hyp gr typ seq gl,gl) in + List.fold_right f l (seq,gl) open Auto @@ -227,7 +227,7 @@ let extend_with_auto_hints l seq gl= error ("Firstorder: "^dbname^" : No such Hint database") in Hint_db.iter g hdb in List.iter h l; - !seqref + !seqref, gl (*FIXME: forgetting about universes*) let print_cmap map= let print_entry c l s= diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 536ee7cc3..40aa169ab 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -54,9 +54,9 @@ val take_formula : t -> Formula.t * t val empty_seq : int -> t val extend_with_ref_list : global_reference list -> - t -> Proof_type.goal sigma -> t + t -> Proof_type.goal sigma -> t * Proof_type.goal sigma val extend_with_auto_hints : Auto.hint_db_name list -> - t -> Proof_type.goal sigma -> t + t -> Proof_type.goal sigma -> t * Proof_type.goal sigma val print_cmap: global_reference list CM.t -> Pp.std_ppcmds diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 88693c196..05cdd288c 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -645,7 +645,7 @@ let build_case_scheme fa = (* Constrintern.global_reference id *) (* in *) let funs = (fun (_,f,_) -> - try Universes.constr_of_global (Nametab.global f) + try Universes.unsafe_constr_of_global (Nametab.global f) with Not_found -> Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in let first_fun,u = destConst funs in diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 3802aa365..90282fcf7 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -163,7 +163,7 @@ VERNAC COMMAND EXTEND Function (Vernacexpr.VernacFixpoint(None, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> - Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) + Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids, false), VtLater) | x -> x ] -> [ do_generate_principle false (List.map snd recsl) ] END diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d98f824e8..d6ad5575b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -181,6 +181,7 @@ let is_rec names = let rec lookup names = function | GVar(_,id) -> check_id id names | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false + | GProj (loc, p, c) -> lookup names c | GCast(_,b,_) -> lookup names b | GProj _ -> error "GProj not handled" | GRec _ -> error "GRec not handled" diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8cccb0bed..5d9c226b7 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -166,7 +166,7 @@ let save with_clean id const (locality,_,kind) hook = let cook_proof _ = - let (id,(entry,strength)) = Pfedit.cook_proof () in + let (id,(entry,_,strength)) = Pfedit.cook_proof () in (id,(entry,strength)) let get_proof_clean do_reduce = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 96bf4c921..50e7507f4 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -75,7 +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 constr_of_global = Universes.unsafe_constr_of_global let constant sl s = constr_of_global (find_reference sl s) @@ -1016,7 +1016,7 @@ let compute_terminate_type nb_args func = delayed_force nat, (mkProd (Name k_id, delayed_force nat, mkArrow cond result))))|])in - let value = mkApp(delayed_force coq_sig, + let value = mkApp(constr_of_global (delayed_force coq_sig_ref), [|b; (mkLambda (Name v_id, b, nb_iter))|]) in compose_prod rev_args value diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 2b9dce1b0..de308c296 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -113,6 +113,28 @@ Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c =? c')%coef. Proof. generalize (CRmorph.(morph_eq) c c'). destruct (c =? c')%coef; auto. +<<<<<<< HEAD +======= +||||||| merged common ancestors +destruct (c ?= c')%coef; auto. +======= +destruct (c ?= c')%coef; auto. +<<<<<<< HEAD +======= +intros. +generalize (fun h => X (morph_eq CRmorph _ _ h)). +case (ceqb c1 c2); auto. +>>>>>>> .merge_file_U4r9lJ +>>>>>>> This commit adds full universe polymorphism and fast projections to Coq. +||||||| merged common ancestors +======= +intros. +generalize (fun h => X (morph_eq CRmorph _ _ h)). +case (ceqb c1 c2); auto. +>>>>>>> .merge_file_U4r9lJ +======= +>>>>>>> Correct rebase on STM code. Thanks to E. Tassi for help on dealing with +>>>>>>> Correct rebase on STM code. Thanks to E. Tassi for help on dealing with Qed. (* Power coefficients : Cpow *) @@ -279,6 +301,7 @@ apply radd_ext. [ ring | now rewrite rdiv_simpl ]. Qed. +<<<<<<< HEAD Theorem rdiv3 r1 r2 r3 r4 : ~ r2 == 0 -> ~ r4 == 0 -> @@ -294,6 +317,8 @@ f_equiv. transitivity (r1 * r4 + - (r3 * r2)); auto. Qed. +======= +>>>>>>> Correct rebase on STM code. Thanks to E. Tassi for help on dealing with Theorem rdiv5 a b : - (a / b) == - a / b. Proof. now rewrite !rdiv_def, ropp_mul_l. @@ -712,7 +737,6 @@ 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. @@ -725,32 +749,6 @@ 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. @@ -1004,7 +1002,6 @@ 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 @@ -1015,20 +1012,6 @@ 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. @@ -1148,7 +1131,6 @@ 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. @@ -1171,93 +1153,6 @@ 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 (*************************************************************************** @@ -1648,21 +1543,11 @@ 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) := diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index ae05fbdc3..8df061870 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -51,8 +51,17 @@ let tag_arg tag_rec map subs i c = | Prot -> mk_atom c | Rec -> if Int.equal i (-1) then mk_clos subs c else tag_rec c +let global_head_of_constr c = + let f, args = decompose_app c in + try global_of_constr f + with Not_found -> anomaly (str "global_head_of_constr") + +let global_of_constr_nofail c = + try global_of_constr c + with Not_found -> VarRef (Id.of_string "dummy") + let rec mk_clos_but f_map subs t = - match f_map t with + match f_map (global_of_constr_nofail t) with | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t | None -> (match kind_of_term t with @@ -65,7 +74,7 @@ and mk_clos_app_but f_map subs f args n = else let fargs, args' = Array.chop n args in let f' = mkApp(f,fargs) in - match f_map f' with + match f_map (global_of_constr_nofail f') with Some map -> mk_clos_deep (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s')) @@ -74,7 +83,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_nounivs t l) with Not_found -> None + try Some(List.assoc_f eq_gr 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 @@ -219,14 +228,12 @@ 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" -let coq_nil = coq_constant "nil" -let coq_None = coq_constant "None" -let coq_Some = coq_constant "Some" +let coq_None = coq_reference "None" +let coq_Some = coq_reference "Some" let coq_eq = coq_constant "eq" -let coq_pcons = coq_reference "cons" -let coq_pnil = coq_reference "nil" +let coq_cons = coq_reference "cons" +let coq_nil = coq_reference "nil" let lapp f args = mkApp(Lazy.force f,args) @@ -274,7 +281,7 @@ let znew_ring_path = let zltac s = lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s)) -let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);; +let mk_cst l s = lazy (Coqlib.gen_reference "newring" l s);; let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; (* Ring theory *) @@ -319,9 +326,12 @@ let coq_hypo = my_reference "hypo" let map_with_eq arg_map c = let (req,_,_) = dest_rel c in interp_map - ((req,(function -1->Prot|_->Rec)):: + ((global_head_of_constr req,(function -1->Prot|_->Rec)):: List.map (fun (c,map) -> (Lazy.force c,map)) arg_map) +let map_without_eq arg_map _ = + interp_map (List.map (fun (c,map) -> (Lazy.force c,map)) arg_map) + let _ = add_map "ring" (map_with_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); @@ -618,8 +628,8 @@ 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|]) + (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH + (plapp evd coq_nil [|carrier|]) in let l' = Typing.solve_evars env evd l in Evarutil.nf_evars_universes !evd l' @@ -629,7 +639,7 @@ let interp_power env evd pow = match pow with | None -> let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in - (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), lapp coq_None [|carrier|]) + (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), plapp evd coq_None [|carrier|]) | Some (tac, spec) -> let tac = match tac with @@ -637,24 +647,24 @@ let interp_power env evd pow = | Closed lc -> closed_term_ast (List.map Smartlocate.global_with_alias lc) in let spec = make_hyp env evd (ic_unsafe spec) in - (tac, lapp coq_Some [|carrier; spec|]) + (tac, plapp evd coq_Some [|carrier; spec|]) 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|] + | None -> plapp evd coq_None [|carrier|] | Some spec -> let spec = make_hyp env evd (ic_unsafe spec) in - lapp coq_Some [|carrier;spec|] + plapp evd coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) 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|] + | None -> plapp evd coq_None [|carrier|] | Some spec -> let spec = make_hyp env evd (ic_unsafe spec) in - lapp coq_Some [|carrier;spec|] + plapp evd coq_Some [|carrier;spec|] (* Same remark on ill-typed terms ... *) let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div = @@ -788,8 +798,8 @@ let make_args_list rl t = 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|]) + (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl + (plapp evd coq_nil [|carrier|]) in Typing.solve_evars env evd l let ltac_ring_structure e = @@ -844,9 +854,9 @@ let _ = add_map "field" coq_nil, (function -1->Eval|_ -> Prot); (* display_linear: evaluate polynomials and coef operations, protect field operations and make recursive call on the var map *) - my_constant "display_linear", + my_reference "display_linear", (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot); - my_constant "display_pow_linear", + my_reference "display_pow_linear", (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) @@ -858,15 +868,15 @@ let _ = add_map "field" pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot); (* FEeval: evaluate morphism, protect field operations and make recursive call on the var map *) - my_constant "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);; + my_reference "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);; let _ = add_map "field_cond" - (map_with_eq + (map_without_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); coq_nil, (function -1->Eval|_ -> Prot); (* PCond: evaluate morphism and denum list, protect ring operations and make recursive call on the var map *) - my_constant "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);; + my_reference "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);; (* (function -1|9|11->Eval|10->Rec|_->Prot)]);;*) @@ -875,9 +885,9 @@ 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 afield_theory = my_reference "almost_field_theory" +let field_theory = my_reference "field_theory" +let sfield_theory = my_reference "semi_field_theory" let af_ar = my_reference"AF_AR" let f_r = my_reference"F_R" let sf_sr = my_reference"SF_SR" @@ -885,18 +895,18 @@ 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_nounivs f (Lazy.force afield_theory) -> + when is_global (Lazy.force afield_theory) f -> 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_nounivs f (Lazy.force field_theory) -> + when is_global (Lazy.force field_theory) f -> let rth = 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_nounivs f (Lazy.force sfield_theory) -> + when is_global (Lazy.force sfield_theory) f -> 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) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 1db3fac52..b56d5947c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1923,11 +1923,12 @@ let eq_id avoid id = let hid' = next_ident_away hid avoid in hid' -let mk_eq typ x y = mkApp (delayed_force coq_eq_ind, [| typ; x ; y |]) -let mk_eq_refl typ x = mkApp (delayed_force coq_eq_refl, [| typ; x |]) -let mk_JMeq typ x typ' y = - mkApp (delayed_force coq_JMeq_ind, [| typ; x ; typ'; y |]) -let mk_JMeq_refl typ x = mkApp (delayed_force coq_JMeq_refl, [| typ; x |]) +let mk_eq evdref typ x y = papp evdref coq_eq_ind [| typ; x ; y |] +let mk_eq_refl evdref typ x = papp evdref coq_eq_refl [| typ; x |] +let mk_JMeq evdref typ x typ' y = + papp evdref coq_JMeq_ind [| typ; x ; typ'; y |] +let mk_JMeq_refl evdref typ x = + papp evdref coq_JMeq_refl [| typ; x |] let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true), None) @@ -1987,7 +1988,7 @@ let constr_of_pat env evdref arsign pat avoid = let env = push_rel_context sign env in evdref := the_conv_x_leq (push_rel_context sign env) (lift (succ m) ty) (lift 1 apptype) !evdref; - let eq_t = mk_eq (lift (succ m) ty) + let eq_t = mk_eq evdref (lift (succ m) ty) (mkRel 1) (* alias *) (lift 1 app) (* aliased term *) in @@ -2048,7 +2049,7 @@ let rec is_included x y = Hence pats is already typed in its full signature. However prevpatterns are in the original one signature per pattern form. *) -let build_ineqs prevpatterns pats liftsign = +let build_ineqs evdref prevpatterns pats liftsign = let _tomatchs = List.length pats in let diffs = List.fold_left @@ -2070,11 +2071,11 @@ let build_ineqs prevpatterns pats liftsign = lift_rel_context len ppat_sign @ sign, len', succ n, (* nth pattern *) - mkApp (delayed_force coq_eq_ind, - [| lift (len' + liftsign) curpat_ty; - liftn (len + liftsign) (succ lens) ppat_c ; - lift len' curpat_c |]) :: - List.map (lift lens (* Jump over this prevpat signature *)) c) + (papp evdref coq_eq_ind + [| lift (len' + liftsign) curpat_ty; + liftn (len + liftsign) (succ lens) ppat_c ; + lift len' curpat_c |]) :: + List.map (lift lens (* Jump over this prevpat signature *)) c) in Some acc else None) (Some ([], 0, 0, [])) eqnpats pats @@ -2122,7 +2123,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = (s, List.map (lift n) args), p) :: pats, len + n)) ([], 0) pats in - let ineqs = build_ineqs prevpatterns pats signlen in + let ineqs = build_ineqs evdref prevpatterns pats signlen in let rhs_rels' = rels_of_patsign rhs_rels in let _signenv = push_rel_context rhs_rels' env in let arity = @@ -2203,7 +2204,7 @@ let abstract_tomatch env tomatchs tycon = ([], [], [], tycon) tomatchs in List.rev prev, ctx, tycon -let build_dependent_signature env evars avoid tomatchs arsign = +let build_dependent_signature env evdref avoid tomatchs arsign = let avoid = ref avoid in let arsign = List.rev arsign in let allnames = List.rev_map (List.map pi1) arsign in @@ -2227,19 +2228,19 @@ let build_dependent_signature env evars avoid tomatchs arsign = let env', nargeqs, argeqs, refl_args, slift, argsign' = List.fold_left2 (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg (name, b, t) -> - let argt = Retyping.get_type_of env evars arg in + let argt = Retyping.get_type_of env !evdref arg in let eq, refl_arg = - if Reductionops.is_conv env evars argt t then - (mk_eq (lift (nargeqs + slift) argt) + if Reductionops.is_conv env !evdref argt t then + (mk_eq evdref (lift (nargeqs + slift) argt) (mkRel (nargeqs + slift)) (lift (nargeqs + nar) arg), - mk_eq_refl argt arg) + mk_eq_refl evdref argt arg) else - (mk_JMeq (lift (nargeqs + slift) t) + (mk_JMeq evdref (lift (nargeqs + slift) t) (mkRel (nargeqs + slift)) (lift (nargeqs + nar) argt) (lift (nargeqs + nar) arg), - mk_JMeq_refl argt arg) + mk_JMeq_refl evdref argt arg) in let previd, id = let name = @@ -2256,13 +2257,13 @@ let build_dependent_signature env evars avoid tomatchs arsign = (Name id, b, t) :: argsign')) (env, neqs, [], [], slift, []) args argsign in - let eq = mk_JMeq + let eq = mk_JMeq evdref (lift (nargeqs + slift) appt) (mkRel (nargeqs + slift)) (lift (nargeqs + nar) ty) (lift (nargeqs + nar) tm) in - let refl_eq = mk_JMeq_refl ty tm in + let refl_eq = mk_JMeq_refl evdref ty tm in let previd, id = make_prime avoid appn in (((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs, succ nargeqs, @@ -2276,11 +2277,11 @@ let build_dependent_signature env evars avoid tomatchs arsign = let arsign' = (Name id, b, typ) in let tomatch_ty = type_of_tomatch ty in let eq = - mk_eq (lift nar tomatch_ty) + mk_eq evdref (lift nar tomatch_ty) (mkRel slift) (lift nar tm) in ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs, - (mk_eq_refl tomatch_ty tm) :: refl_args, + (mk_eq_refl evdref tomatch_ty tm) :: refl_args, pred slift, (arsign' :: []) :: arsigns)) ([], 0, [], nar, []) tomatchs arsign in @@ -2317,7 +2318,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env (* Build the dependent arity signature, the equalities which makes the first part of the predicate and their instantiations. *) let avoid = [] in - build_dependent_signature env ( !evdref) avoid tomatchs arsign + build_dependent_signature env evdref avoid tomatchs arsign in let tycon, arity = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 43af6ec62..c7173c2d1 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -28,6 +28,7 @@ open Evarutil open Evarconv open Evd open Termops +open Globnames (* Typing operations dealing with coercions *) exception NoCoercion @@ -84,7 +85,7 @@ let disc_subset x = Ind (i,_) -> let len = Array.length l in let sigty = delayed_force sig_typ in - if Int.equal len 2 && eq_ind i (fst (Term.destInd sigty)) + if Int.equal len 2 && eq_ind i (Globnames.destIndRef sigty) then let (a, b) = pair_of_array l in Some (a, b) @@ -113,8 +114,7 @@ let mu env evdref t = let p = hnf_nodelta env !evdref p in (Some (fun x -> app_opt env evdref - f (mkApp (delayed_force sig_proj1, - [| u; p; x |]))), + f (papp evdref sig_proj1 [| u; p; x |])), ct) | None -> (None, v) in aux t @@ -158,10 +158,11 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) in let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in - let eq = mkApp (delayed_force coq_eq_ind, [| eqT; hdx; hdy |]) in + let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in let evar = make_existential loc env evdref eq in - let eq_app x = mkApp (delayed_force coq_eq_rect, - [| eqT; hdx; pred; x; hdy; evar|]) in + let eq_app x = papp evdref coq_eq_rect + [| eqT; hdx; pred; x; hdy; evar|] + in aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) else Some co @@ -204,9 +205,9 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let prod = delayed_force prod_typ in (* Sigma types *) if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i' - && (eq_ind i (fst (Term.destInd sigT)) || eq_ind i (fst (Term.destInd prod))) + && (eq_ind i (destIndRef sigT) || eq_ind i (destIndRef prod)) then - if eq_ind i (fst (Term.destInd sigT)) + if eq_ind i (destIndRef sigT) then begin let (a, pb), (a', pb') = @@ -238,12 +239,12 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) Some (fun x -> let x, y = - app_opt env' evdref c1 (mkApp (delayed_force sigT_proj1, - [| a; pb; x |])), - app_opt env' evdref c2 (mkApp (delayed_force sigT_proj2, - [| a; pb; x |])) + app_opt env' evdref c1 (papp evdref sigT_proj1 + [| a; pb; x |]), + app_opt env' evdref c2 (papp evdref sigT_proj2 + [| a; pb; x |]) in - mkApp (delayed_force sigT_intro, [| a'; pb'; x ; y |])) + papp evdref sigT_intro [| a'; pb'; x ; y |]) end else begin @@ -258,12 +259,12 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) Some (fun x -> let x, y = - app_opt env evdref c1 (mkApp (delayed_force prod_proj1, - [| a; b; x |])), - app_opt env evdref c2 (mkApp (delayed_force prod_proj2, - [| a; b; x |])) + app_opt env evdref c1 (papp evdref prod_proj1 + [| a; b; x |]), + app_opt env evdref c2 (papp evdref prod_proj2 + [| a; b; x |]) in - mkApp (delayed_force prod_intro, [| a'; b'; x ; y |])) + papp evdref prod_intro [| a'; b'; x ; y |]) end else if eq_ind i i' && Int.equal len (Array.length l') then @@ -294,8 +295,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) Some (u, p) -> let c = coerce_unify env u y in let f x = - app_opt env evdref c (mkApp (delayed_force sig_proj1, - [| u; p; x |])) + app_opt env evdref c (papp evdref sig_proj1 [| u; p; x |]) in Some f | None -> match disc_subset y with @@ -306,9 +306,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let cx = app_opt env evdref c x in let evar = make_existential loc env evdref (mkApp (p, [| cx |])) in - (mkApp - (delayed_force sig_intro, - [| u; p; cx; evar |]))) + (papp evdref sig_intro [| u; p; cx; evar |])) | None -> raise NoSubtacCoercion in coerce_unify env x y diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index b3c65ebaf..306116d76 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1082,10 +1082,16 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar let evi2 = Evd.find evd evk2 in let evi2env = Evd.evar_env evi2 in let ctx', j = Reduction.dest_arity evi2env evi2.evar_concl in - if i == j || Evd.check_eq evd (univ_of_sort i) (univ_of_sort j) + let ui, uj = univ_of_sort i, univ_of_sort j in + if i == j || Evd.check_eq evd ui uj then (* Shortcut, i = j *) solve_evar_evar ~force f g env evd pbty ev1 ev2 - else + (* Avoid looping if postponing happened on previous evar/evar problem *) + else if Evd.check_leq evd ui uj then + solve_evar_evar ~force f g env evd None ev1 ev2 + else if Evd.check_leq evd uj ui then + solve_evar_evar ~force f g env evd None ev2 ev1 + else let evd, k = Evd.new_sort_variable univ_flexible_alg evd in let evd, ev3 = Evarutil.new_pure_evar evd (Evd.evar_hyps evi) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 0776988d7..ae16fbebe 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1005,14 +1005,6 @@ let fresh_constructor_instance env evd c = with_context_set univ_flexible evd (Universes.fresh_constructor_instance env c) let fresh_global ?(rigid=univ_flexible) env evd gr = - (* match gr with *) - (* | ConstructRef c -> let evd, c = fresh_constructor_instance env evd c in *) - (* evd, mkConstructU c *) - (* | IndRef c -> let evd, c = fresh_inductive_instance env evd c in *) - (* evd, mkIndU c *) - (* | ConstRef c -> let evd, c = fresh_constant_instance env evd c in *) - (* evd, mkConstU c *) - (* | VarRef i -> evd, mkVar i *) with_context_set rigid evd (Universes.fresh_global_instance env gr) let whd_sort_variable evd t = t @@ -1420,6 +1412,9 @@ type 'a sigma = { let sig_it x = x.it let sig_sig x = x.sigma +let on_sig s f = + let sigma', v = f s.sigma in + { s with sigma = sigma' }, v (*******************************************************************) (* The state monad with state an evar map. *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 18d68bebf..e44e8e906 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -226,7 +226,8 @@ val instantiate_evar_array : evar_info -> constr -> constr array -> constr val subst_evar_defs_light : substitution -> evar_map -> evar_map (** Assume empty universe constraints in [evar_map] and [conv_pbs] *) -val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> evar_map -> evar_map -> evar_map +val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> + evar_map -> evar_map -> evar_map (** spiwack: this function seems to somewhat break the abstraction. *) (** {6 Misc} *) @@ -283,12 +284,14 @@ type 'a sigma = { val sig_it : 'a sigma -> 'a val sig_sig : 'a sigma -> evar_map +val on_sig : 'a sigma -> (evar_map -> evar_map * 'b) -> 'a sigma * 'b (** {5 The state monad with state an evar map} *) module MonadR : Monad.S with type +'a t = evar_map -> evar_map * 'a module Monad : Monad.S with type +'a t = evar_map -> 'a * evar_map + (** {5 Meta machinery} These functions are almost deprecated. They were used before the @@ -478,7 +481,8 @@ val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstan val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor -val fresh_global : ?rigid:rigid -> env -> evar_map -> Globnames.global_reference -> evar_map * constr +val fresh_global : ?rigid:rigid -> env -> evar_map -> + Globnames.global_reference -> evar_map * constr (******************************************************************** Conversion w.r.t. an evar map: might generate universe unifications diff --git a/pretyping/program.ml b/pretyping/program.ml index 67bb3bd2a..a0ecfb1f9 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -26,27 +26,31 @@ let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr let init_constant dir s () = coq_constant "Program" dir s let init_reference dir s () = coq_reference "Program" dir s -let sig_typ = init_constant ["Init"; "Specif"] "sig" -let sig_intro = init_constant ["Init"; "Specif"] "exist" -let sig_proj1 = init_constant ["Init"; "Specif"] "proj1_sig" +let papp evdref r args = + let gr = delayed_force r in + mkApp (Evarutil.e_new_global evdref gr, args) -let sigT_typ = init_constant ["Init"; "Specif"] "sigT" -let sigT_intro = init_constant ["Init"; "Specif"] "existT" -let sigT_proj1 = init_constant ["Init"; "Specif"] "projT1" -let sigT_proj2 = init_constant ["Init"; "Specif"] "projT2" +let sig_typ = init_reference ["Init"; "Specif"] "sig" +let sig_intro = init_reference ["Init"; "Specif"] "exist" +let sig_proj1 = init_reference ["Init"; "Specif"] "proj1_sig" -let prod_typ = init_constant ["Init"; "Datatypes"] "prod" -let prod_intro = init_constant ["Init"; "Datatypes"] "pair" -let prod_proj1 = init_constant ["Init"; "Datatypes"] "fst" -let prod_proj2 = init_constant ["Init"; "Datatypes"] "snd" +let sigT_typ = init_reference ["Init"; "Specif"] "sigT" +let sigT_intro = init_reference ["Init"; "Specif"] "existT" +let sigT_proj1 = init_reference ["Init"; "Specif"] "projT1" +let sigT_proj2 = init_reference ["Init"; "Specif"] "projT2" -let coq_eq_ind = init_constant ["Init"; "Logic"] "eq" -let coq_eq_refl = init_constant ["Init"; "Logic"] "eq_refl" +let prod_typ = init_reference ["Init"; "Datatypes"] "prod" +let prod_intro = init_reference ["Init"; "Datatypes"] "pair" +let prod_proj1 = init_reference ["Init"; "Datatypes"] "fst" +let prod_proj2 = init_reference ["Init"; "Datatypes"] "snd" + +let coq_eq_ind = init_reference ["Init"; "Logic"] "eq" +let coq_eq_refl = init_reference ["Init"; "Logic"] "eq_refl" let coq_eq_refl_ref = init_reference ["Init"; "Logic"] "eq_refl" -let coq_eq_rect = init_constant ["Init"; "Logic"] "eq_rect" +let coq_eq_rect = init_reference ["Init"; "Logic"] "eq_rect" -let coq_JMeq_ind = init_constant ["Logic";"JMeq"] "JMeq" -let coq_JMeq_refl = init_constant ["Logic";"JMeq"] "JMeq_refl" +let coq_JMeq_ind = init_reference ["Logic";"JMeq"] "JMeq" +let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl" let coq_not = init_constant ["Init";"Logic"] "not" let coq_and = init_constant ["Init";"Logic"] "and" diff --git a/pretyping/program.mli b/pretyping/program.mli index 0572a93a0..5b40b2e71 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -7,29 +7,33 @@ (************************************************************************) open Term +open Globnames (** A bunch of Coq constants used by Progam *) -val sig_typ : unit -> constr -val sig_intro : unit -> constr -val sig_proj1 : unit -> constr -val sigT_typ : unit -> constr -val sigT_intro : unit -> constr -val sigT_proj1 : unit -> constr -val sigT_proj2 : unit -> constr +val sig_typ : unit -> global_reference +val sig_intro : unit -> global_reference +val sig_proj1 : unit -> global_reference +val sigT_typ : unit -> global_reference +val sigT_intro : unit -> global_reference +val sigT_proj1 : unit -> global_reference +val sigT_proj2 : unit -> global_reference -val prod_typ : unit -> constr -val prod_intro : unit -> constr -val prod_proj1 : unit -> constr -val prod_proj2 : unit -> constr +val prod_typ : unit -> global_reference +val prod_intro : unit -> global_reference +val prod_proj1 : unit -> global_reference +val prod_proj2 : unit -> global_reference -val coq_eq_ind : unit -> constr -val coq_eq_refl : unit -> constr -val coq_eq_refl_ref : unit -> Globnames.global_reference -val coq_eq_rect : unit -> constr +val coq_eq_ind : unit -> global_reference +val coq_eq_refl : unit -> global_reference +val coq_eq_refl_ref : unit -> global_reference +val coq_eq_rect : unit -> global_reference -val coq_JMeq_ind : unit -> constr -val coq_JMeq_refl : unit -> constr +val coq_JMeq_ind : unit -> global_reference +val coq_JMeq_refl : unit -> global_reference val mk_coq_and : constr list -> constr val mk_coq_not : constr -> constr + +(** Polymorphic application of delayed references *) +val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index fac73670b..fdcce914d 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -255,8 +255,10 @@ let build_subclasses ~check env sigma glob pri = (fun () -> incr i; Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i)) in - let rec aux pri c path = - let ty = Evarutil.nf_evar sigma (Retyping.get_type_of env sigma c) in + let ty, ctx = Global.type_of_global_in_context env glob in + let sigma = Evd.merge_context_set Evd.univ_rigid sigma (Univ.ContextSet.of_context ctx) in + let rec aux pri c ty path = + let ty = Evarutil.nf_evar sigma ty in match class_of_constr ty with | None -> [] | Some (rels, ((tc,u), args)) -> @@ -284,10 +286,15 @@ let build_subclasses ~check env sigma glob pri = in let declare_proj hints (cref, pri, body) = let path' = cref :: path in - let rest = aux pri body path' in + let ty = Retyping.get_type_of env sigma body in + let rest = aux pri body ty path' in hints @ (path', pri, body) :: rest in List.fold_left declare_proj [] projs - in aux pri (Universes.constr_of_global glob) [glob] + in + let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in + (*FIXME subclasses should now get substituted for each particular instance of + the polymorphic superclass *) + aux pri term ty [glob] (* * instances persistent object diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 3fc01c0bc..1b329dbc4 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -36,8 +36,8 @@ let start_proof (id : Id.t) str hyps c ?init_tac terminator = let cook_this_proof p = match p with - | { Proof_global.id;entries=[constr];persistence } -> - (id,(constr,persistence)) + | { Proof_global.id;entries=[constr];persistence;constraints } -> + (id,(constr,constraints,persistence)) | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") let cook_proof () = @@ -123,7 +123,7 @@ let build_constant_by_tactic id sign ?(goal_kind = Global, false, Proof Theorem) start_proof id goal_kind sign typ (fun _ -> ()); try let status = by tac in - let _,(const,_) = cook_proof () in + let _,(const,_,_) = cook_proof () in delete_current_proof (); const, status, !substref with reraise -> diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 877b7c858..b99bbe872 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -69,11 +69,11 @@ val start_proof : val cook_this_proof : Proof_global.proof_object -> (Id.t * - (Entries.definition_entry * goal_kind)) + (Entries.definition_entry * Univ.constraints * goal_kind)) val cook_proof : unit -> (Id.t * - (Entries.definition_entry * goal_kind)) + (Entries.definition_entry * Univ.constraints * goal_kind)) (** {6 ... } *) (** [get_pftreestate ()] returns the current focused pending proof. diff --git a/proofs/proof.mli b/proofs/proof.mli index 30b65d0ce..f2b64fb18 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -53,7 +53,7 @@ val proof : proof -> val start : Evd.evar_map -> (Environ.env * Term.types Univ.in_universe_context_set) list -> proof val dependent_start : Evd.evar_map -> Proofview.telescope -> proof -val initial_goals : proof -> (Term.constr * Term.types) list +val initial_goals : proof -> (Term.constr * Term.types Univ.in_universe_context_set) list (* Returns [true] if the considered proof is completed, that is if no goal remain to be considered (this does not require that all evars have been solved). *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f7548b6ca..c11a26fb2 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -68,6 +68,7 @@ type proof_object = { id : Names.Id.t; entries : Entries.definition_entry list; persistence : Decl_kinds.goal_kind; + constraints : Univ.constraints; } type proof_ending = @@ -271,7 +272,7 @@ let close_proof ?feedback_id ~now fpl = let initial_goals = Proof.initial_goals proof in let fpl, univs = Future.split2 fpl in let () = if poly || now then ignore (Future.compute univs) in - let entries = Future.map2 (fun p (c, t) -> + let entries = Future.map2 (fun p (c, (t, octx)) -> let compute_univs (usubst, uctx) = let nf = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst in let compute_c_t (c, eff) = @@ -290,19 +291,33 @@ let close_proof ?feedback_id ~now fpl = let t = Future.chain ~pure:true ans (fun (_, x, _) -> x) in let univs = Future.chain ~pure:true ans (fun (_, _, x) -> x) in let t = Future.force t in - { Entries. - const_entry_body = p; - const_entry_secctx = section_vars; - const_entry_type = Some t; - const_entry_feedback = feedback_id; - const_entry_inline_code = false; - const_entry_opaque = true; - const_entry_universes = univs; - const_entry_polymorphic = pi2 strength; - const_entry_proj = None}) fpl initial_goals in - if now then - List.iter (fun x -> ignore(Future.force x.Entries.const_entry_body)) entries; - { id = pid; entries = entries; persistence = strength }, + { Entries. + const_entry_body = p; + const_entry_secctx = section_vars; + const_entry_type = Some t; + const_entry_inline_code = false; + const_entry_opaque = true; + const_entry_universes = univs; + const_entry_feedback = None; + const_entry_polymorphic = pi2 strength; + const_entry_proj = None}) fpl initial_goals in + let globaluctx = + if not poly then + List.fold_left (fun acc (c, (t, octx)) -> + Univ.ContextSet.union octx acc) + Univ.ContextSet.empty initial_goals + else Univ.ContextSet.empty + in + let _ = + if now then + List.iter (fun x -> ignore(Future.compute x.Entries.const_entry_body)) entries + in +(* let hook = Option.map (fun f -> + if poly || now then f (Future.join univs) + else f (Univ.LMap.empty,Univ.UContext.empty)) + hook + in*) (* FIXME *) + { id = pid; entries = entries; persistence = strength; constraints = Univ.ContextSet.constraints globaluctx }, Ephemeron.get terminator type closed_proof_output = Entries.proof_output list * @@ -330,8 +345,8 @@ let return_proof () = (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) - let goals = List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals in - goals, (subst, ctx) + let proofs = List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals in + proofs, (subst, ctx) let close_future_proof ~feedback_id proof = close_proof ~feedback_id ~now:false proof @@ -493,8 +508,10 @@ let _ = module V82 = struct let get_current_initial_conclusions () = - let { pid; strength; proof } = cur_pstate () in - pid, (List.map snd (Proof.initial_goals proof), strength) + let { pid; strength; proof } = cur_pstate () in + let initial = Proof.initial_goals proof in + let goals = List.map (fun (o, (c, ctx)) -> c) initial in + pid, (goals, strength) end type state = pstate list diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index f10e991ea..6c11ee9b4 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -61,6 +61,8 @@ type proof_object = { id : Names.Id.t; entries : Entries.definition_entry list; persistence : Decl_kinds.goal_kind; + constraints : Univ.constraints; + (** guards : lemma_possible_guards; *) } type proof_ending = diff --git a/proofs/proofview.ml b/proofs/proofview.ml index d0a477431..291da4a98 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -26,7 +26,7 @@ open Util type proofview = Proofview_monad.proofview open Proofview_monad -type entry = (Term.constr * Term.types) list +type entry = (Term.constr * Term.types Univ.in_universe_context_set) list let proofview p = p.comb , p.solution @@ -42,7 +42,7 @@ let init sigma = let (e, _) = Term.destEvar econstr in let new_defs = Evd.merge_context_set Evd.univ_rigid new_defs ctx in let gl = Goal.build e in - let entry = (econstr, typ) :: ret in + let entry = (econstr, (typ, ctx)) :: ret in entry, { solution = new_defs; comb = gl::comb; } in fun l -> @@ -52,17 +52,18 @@ let init sigma = type telescope = | TNil - | TCons of Environ.env*Term.types*(Term.constr -> telescope) + | TCons of Environ.env * Term.types Univ.in_universe_context_set * (Term.constr -> telescope) let dependent_init = let rec aux sigma = function | TNil -> [], { solution = sigma; comb = []; } - | TCons (env, typ, t) -> + | TCons (env, (typ, ctx), t) -> let (sigma, econstr ) = Evarutil.new_evar sigma env typ in + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in let ret, { solution = sol; comb = comb } = aux sigma (t econstr) in let (e, _) = Term.destEvar econstr in let gl = Goal.build e in - let entry = (econstr, typ) :: ret in + let entry = (econstr, (typ, ctx)) :: ret in entry, { solution = sol; comb = gl :: comb; } in fun sigma t -> diff --git a/proofs/proofview.mli b/proofs/proofview.mli index bfb88c897..dddf9b1c2 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -41,7 +41,7 @@ val init : Evd.evar_map -> (Environ.env * Term.types Univ.in_universe_context_se type telescope = | TNil - | TCons of Environ.env*Term.types*(Term.constr -> telescope) + | TCons of Environ.env * Term.types Univ.in_universe_context_set * (Term.constr -> telescope) (* Like [init], but goals are allowed to be depedenent on one another. Dependencies between goals is represented with the type @@ -57,7 +57,7 @@ val finished : proofview -> bool val return : proofview -> Evd.evar_map val partial_proof : entry -> proofview -> constr list -val initial_goals : entry -> (constr * types) list +val initial_goals : entry -> (constr * types Univ.in_universe_context_set) list val emit_side_effects : Declareops.side_effects -> proofview -> proofview (*** Focusing operations ***) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 2faf18355..695e8ab6e 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -75,6 +75,8 @@ let pf_reduction_of_red_expr gls re c = (fst (reduction_of_red_expr (pf_env gls) re)) (pf_env gls) (project gls) c let pf_apply f gls = f (pf_env gls) (project gls) +let pf_eapply f gls x = + on_sig gls (fun evm -> f (pf_env gls) evm x) let pf_reduce = pf_apply let pf_whd_betadeltaiota = pf_reduce whd_betadeltaiota diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 326d14bf6..cd4e796d5 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -54,6 +54,8 @@ val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a +val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) -> + goal sigma -> 'a -> goal sigma * 'b val pf_reduce : (env -> evar_map -> constr -> constr) -> goal sigma -> constr -> constr diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 13194eb89..9e7bcc8b0 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -296,11 +296,11 @@ let set_start_hook = (:=) start_hook let get_proof proof do_guard hook opacity = - let (id,(const,persistence)) = + let (id,(const,cstrs,persistence)) = Pfedit.cook_this_proof proof in (** FIXME *) - id,{const with const_entry_opaque = opacity},Univ.Constraint.empty,do_guard,persistence,hook + id,{const with const_entry_opaque = opacity},cstrs,do_guard,persistence,hook let standard_proof_terminator compute_guard hook = let open Proof_global in function diff --git a/stm/stm.ml b/stm/stm.ml index 3496a3e4f..69e73089e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -79,7 +79,7 @@ type branch_type = | `Proof of proof_mode * depth | `Edit of proof_mode * Stateid.t * Stateid.t ] type cmd_t = ast * Id.t list -type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list +type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list * Decl_kinds.polymorphic type qed_t = { qast : ast; keep : vernac_qed_type; @@ -245,7 +245,7 @@ end = struct let print_dag vcs () = let fname = "stm_" ^ process_id () in let string_of_transaction = function - | Cmd (t, _) | Fork (t, _,_,_) -> + | Cmd (t, _) | Fork (t, _,_,_,_) -> (try string_of_ppcmds (pr_ast t) with _ -> "ERR") | Sideff (Some t) -> sprintf "Sideff(%s)" @@ -777,7 +777,7 @@ end = struct | Some (_, cur) -> match VCS.visit cur with | { step = `Cmd ( { loc }, _) } - | { step = `Fork ( { loc }, _, _, _) } + | { step = `Fork ( { loc }, _, _, _, _) } | { step = `Qed ( { qast = { loc } }, _) } | { step = `Sideff (`Ast ( { loc }, _)) } -> let start, stop = Loc.unloc loc in @@ -1182,11 +1182,11 @@ let collect_proof cur hd brkind id = match last, view.step with | _, `Cmd (x, _) -> collect (Some (id,x)) (id::accn) view.next | _, `Alias _ -> `Sync (no_name,`Alias) - | _, `Fork(_,_,_,_::_::_)-> `Sync (no_name,`MutualProofs) - | _, `Fork(_,_,Doesn'tGuaranteeOpacity,_) -> + | _, `Fork(_,_,_,_::_::_,_)-> `Sync (no_name,`MutualProofs) + | _, `Fork(_,_,Doesn'tGuaranteeOpacity,_,_) -> `Sync (no_name,`Doesn'tGuaranteeOpacity) | Some (parent, ({ expr = VernacProof(_,Some _)} as v)), - `Fork (_, hd', GuaranteesOpacity, ids) -> + `Fork (_, hd', GuaranteesOpacity, ids,_) -> let name = name ids in let time = get_hint_bp_time name in assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); @@ -1194,7 +1194,7 @@ let collect_proof cur hd brkind id = then `ASync (parent,Some v,accn,name) else `Sync (name,`Policy) | Some (parent, ({ expr = VernacProof(t,None)} as v)), - `Fork (_, hd', GuaranteesOpacity, ids) when + `Fork (_, hd', GuaranteesOpacity, ids, _) when not (State.is_cached parent) && !Flags.compilation_mode = Flags.BuildVi -> (try @@ -1206,7 +1206,7 @@ let collect_proof cur hd brkind id = then `ASync (parent,Some v,accn,name) else `Sync (name,`Policy) with Not_found -> `Sync (no_name,`NoHint)) - | Some (parent, _), `Fork (_, hd', GuaranteesOpacity, ids) -> + | Some (parent, _), `Fork (_, hd', GuaranteesOpacity, ids, _) -> assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in let time = get_hint_bp_time name in @@ -1274,7 +1274,7 @@ let known_state ?(redefine_qed=false) ~cache id = | `Cmd (x,_) -> (fun () -> reach view.next; vernac_interp id x ), cache - | `Fork (x,_,_,_) -> (fun () -> + | `Fork (x,_,_,_,_) -> (fun () -> reach view.next; vernac_interp id x; wall_clock_last_fork := Unix.gettimeofday () ), `Yes @@ -1422,7 +1422,7 @@ end = struct let ids = if id = Stateid.initial || id = Stateid.dummy then [] else match VCS.visit id with - | { step = `Fork (_,_,_,l) } -> l + | { step = `Fork (_,_,_,l,_) } -> l | { step = `Cmd (_,l) } -> l | _ -> [] in match f acc (id, vcs, ids) with @@ -1712,11 +1712,11 @@ let process_transaction ~tty verbose c (loc, expr) = anomaly(str"classifier: VtQuery + VtLater must imply part_of_script") (* Proof *) - | VtStartProof (mode, guarantee, names), w -> + | VtStartProof (mode, guarantee, names, poly), w -> let id = VCS.new_node () in let bname = VCS.mk_branch_name x in VCS.checkout VCS.Branch.master; - VCS.commit id (Fork (x, bname, guarantee, names)); + VCS.commit id (Fork (x, bname, guarantee, names, poly)); VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode mode; Backtrack.record (); if w == VtNow then finish (); `Ok @@ -1773,7 +1773,7 @@ let process_transaction ~tty verbose c (loc, expr) = Proof_global.there_are_pending_proofs () then begin let bname = VCS.mk_branch_name x in - VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[])); + VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[],false)); VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode "Classic"; end else begin @@ -1995,7 +1995,7 @@ let get_script prf = Stateid.equal id Stateid.dummy then acc else let view = VCS.visit id in match view.step with - | `Fork (_,_,_,ns) when test ns -> acc + | `Fork (_,_,_,ns,_) when test ns -> acc | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof | `Sideff (`Ast (x,_)) -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 94268e020..76ef10e85 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -46,6 +46,11 @@ let elide_part_of_script_and_now (a, _) = | VtStm (x, _) -> VtStm (x, false), VtNow | x -> x, VtNow +let make_polymorphic (a, b as x) = + match a with + | VtStartProof (x, y, ids, _) -> (VtStartProof (x, y, ids, true), b) + | _ -> x + let undo_classifier = ref (fun _ -> assert false) let set_undo_classifier f = undo_classifier := f @@ -68,7 +73,7 @@ let rec classify_vernac e = | VernacLocal (_,e) -> classify_vernac e | VernacPolymorphic (b, e) -> if b || Flags.is_universe_polymorphism () (* Ok or not? *) then - fst (classify_vernac e), VtNow + make_polymorphic (classify_vernac e) else classify_vernac e | VernacTimeout (_,e) -> classify_vernac e | VernacTime e -> classify_vernac e @@ -88,8 +93,8 @@ let rec classify_vernac e = | VernacProof _ | VernacBullet _ | VernacFocus _ | VernacUnfocus - | VernacSubproof _ | VernacEndSubproof - | VernacSolve _ | VernacError _ + | VernacSubproof _ | VernacEndSubproof + | VernacSolve _ | VernacCheckGuard | VernacUnfocused | VernacSolveExistential _ -> VtProofStep, VtLater @@ -98,23 +103,23 @@ let rec classify_vernac e = | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) | VernacDefinition (_,(_,i),ProveBody _) -> - VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater + VtStartProof("Classic",GuaranteesOpacity,[i], false), VtLater | VernacStartTheoremProof (_,l,_) -> let ids = CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in - VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater - | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater + VtStartProof ("Classic",GuaranteesOpacity,ids, false), VtLater + | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[],false), VtLater | VernacFixpoint (_,l) -> let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in - if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater + if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids, false), VtLater else VtSideff ids, VtLater | VernacCoFixpoint (_,l) -> let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,p),_) -> id::l, b || p = None) ([],false) l in - if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater + if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids,false), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> @@ -182,6 +187,7 @@ let rec classify_vernac e = | VernacToplevelControl _ | VernacRestoreState _ | VernacWriteState _ -> VtUnknown, VtNow + | VernacError _ -> assert false (* Plugins should classify their commands *) | VernacExtend (s,l) -> try List.assoc s !classifiers l () diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index d00626d32..779070f80 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -254,11 +254,11 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ] -> [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ] | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] + => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n], false), VtLater) ] -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ] | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] + => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n], false), VtLater) ] -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ] END diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index d75eb384f..ba62fa7fd 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -125,7 +125,6 @@ Proof. intros x y z H; revert z; induction H; auto. inversion 1; subst; auto. invlist eqlistA; eauto with *. Qed. - (** Moreover, [eqlistA] implies [equivlistA]. A reverse result will be proved later for sorted list without duplicates. *) diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v index 4a4fc23f9..76f8a55a4 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -42,8 +42,8 @@ intros A B. apply (dependent_unique_choice A (fun _ => B)). Qed. -(** The following proof comes from [[ChicliPottierSimpson02]] *) +(** The following proof comes from [[ChicliPottierSimpson02]] *) Require Import Setoid. Theorem classic_set_in_prop_context : @@ -78,7 +78,7 @@ destruct (f P). right. destruct HfP as [[_ Hfalse]| [Hna _]]. discriminate. - assumption. + assumption. Qed. Corollary not_not_classic_set : diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 3142d97ca..6164e6e93 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -962,7 +962,8 @@ Proof. firstorder. Qed. Lemma eq_Leq : forall s s', eq s s' <-> L.eq (elements s) (elements s'). Proof. unfold eq, Equal, L.eq; intros. - setoid_rewrite elements_spec1; firstorder. + do 2 setoid_rewrite elements_spec1. (*FIXME due to regression in rewrite *) + firstorder. Qed. Definition lt (s1 s2 : tree) : Prop := diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index b444d443d..acc9fd5d6 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -812,7 +812,7 @@ Hint Resolve Rinv_involutive: real. Lemma Rinv_mult_distr : forall r1 r2, r1 <> 0 -> r2 <> 0 -> / (r1 * r2) = / r1 * / r2. Proof. - intros; field; auto. + intros; field; auto. Qed. (*********) diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index a89b90238..5b52c6ec9 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -69,7 +69,7 @@ Section defs. (forall a l, Sorted l -> P l -> HdRel a l -> P (a :: l)) -> forall l:list A, Sorted l -> P l. Proof. - induction l; firstorder using Sorted_inv. + induction l. firstorder using Sorted_inv. firstorder using Sorted_inv. Qed. Lemma Sorted_LocallySorted_iff : forall l, Sorted l <-> LocallySorted l. diff --git a/toplevel/classes.ml b/toplevel/classes.ml index cf47abf44..45dd6f1ec 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -55,7 +55,7 @@ let declare_class g = (** TODO: add subinstances *) let existing_instance glob g pri = let c = global g in - let instance = Typing.type_of (Global.env ()) Evd.empty (Universes.constr_of_global c) in + let instance = Global.type_of_global_unsafe c in let _, r = decompose_prod_assum instance in match class_of_constr r with | Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob @@ -356,7 +356,7 @@ let context l = let impl = List.exists test impls in let decl = (Discharge, (Flags.use_polymorphic_flag ()), Definitional) in let nstatus = - snd (Command.declare_assumption false decl (t, uctx) [] impl + pi3 (Command.declare_assumption false decl (t, uctx) [] impl Vernacexpr.NoInline (Loc.ghost, id)) in status && nstatus diff --git a/toplevel/command.ml b/toplevel/command.ml index e8d2eda8a..3f2a51888 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -202,7 +202,7 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma let r = VarRef ident in let () = Typeclasses.declare_instance None true r in let () = if is_coe then Class.try_add_new_coercion r ~local:true false in - (r,true) + (r,Univ.Instance.empty,true) | Global | Local | Discharge -> let local = get_locality ident local in @@ -219,7 +219,7 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma let () = assumption_message ident in let () = Typeclasses.declare_instance None false gr in let () = if is_coe then Class.try_add_new_coercion gr local p in - (gr,Lib.is_modtype_strict ()) + (gr,Univ.UContext.instance ctx,Lib.is_modtype_strict ()) let declare_assumptions_hook = ref ignore let set_declare_assumptions_hook = (:=) declare_assumptions_hook @@ -234,8 +234,8 @@ let interp_assumption evdref env bl c = let declare_assumptions idl is_coe k c imps impl_is_on nl = let refs, status = List.fold_left (fun (refs,status) id -> - let ref',status' = declare_assumption is_coe k c imps impl_is_on nl id in - ref'::refs, status' && status) ([],true) idl in + let ref',u',status' = declare_assumption is_coe k c imps impl_is_on nl id in + (ref',u')::refs, status' && status) ([],true) idl in List.rev refs, status let do_assumptions kind nl l = @@ -251,8 +251,11 @@ let do_assumptions kind nl l = snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) -> let t = replace_vars subst t in let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) imps false nl in - let subst' = List.map2 (fun (_,id) c -> (id,Universes.constr_of_global c)) idl refs in - (subst'@subst, status' && status)) ([],true) l) + let subst' = List.map2 + (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) (*FIXME incorrect should also enrich the context of the current assumption with c's context *) + idl refs + in + (subst'@subst, status' && status)) ([],true) l) (* 3a| Elimination schemes for mutual inductive definitions *) diff --git a/toplevel/command.mli b/toplevel/command.mli index b2ba23ef2..d2e601edd 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -52,7 +52,7 @@ val declare_assumption : coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> Impargs.manual_implicits -> bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> - global_reference * bool + global_reference * Univ.Instance.t * bool val do_assumptions : locality * polymorphic * assumption_object_kind -> Vernacexpr.inline -> simple_binder with_coercion list -> bool diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2e9bfedc7..02e59a227 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -835,7 +835,7 @@ let vernac_set_end_tac tac = let vernac_set_used_variables e = let tys = - List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in + List.map fst (Proof.initial_goals (Proof_global.give_me_the_proof ())) in let l = Proof_using.process_expr (Global.env ()) e tys in let vars = Environ.named_context (Global.env ()) in List.iter (fun id -> |