diff options
Diffstat (limited to 'vernac/command.ml')
| -rw-r--r-- | vernac/command.ml | 72 |
1 files changed, 33 insertions, 39 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index 25dd724af8..b1425d7034 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -35,7 +35,6 @@ open Evarconv open Indschemes open Misctypes open Vernacexpr -open Sigma.Notations open Context.Rel.Declaration open Entries @@ -78,8 +77,7 @@ let red_constant_entry n ce sigma = function let env = Global.env () in let (redfun, _) = reduction_of_red_expr env red in let redfun env sigma c = - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (c, _, _) = redfun.e_redfun env sigma c in + let (_, c) = redfun env sigma c in EConstr.Unsafe.to_constr c in { ce with const_entry_body = Future.chain ~pure:true proof_out @@ -211,7 +209,7 @@ let do_definition ident k pl bl red_option c ctypopt hook = assert(Univ.ContextSet.is_empty ctx); let typ = match ce.const_entry_type with | Some t -> t - | None -> EConstr.Unsafe.to_constr (Retyping.get_type_of env evd (EConstr.of_constr c)) + | None -> EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr c)) in Obligations.check_evars env evd; let obls, _, c, cty = @@ -411,8 +409,8 @@ let mk_mltype_data evdref env assums arity indname = (is_ml_type,indname,assums) let prepare_param = function - | LocalAssum (na,t) -> out_name na, LocalAssumEntry t - | LocalDef (na,b,_) -> out_name na, LocalDefEntry b + | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t + | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b (** Make the arity conclusion flexible to avoid generating an upper bound universe now, only if the universe does not appear anywhere else. @@ -582,7 +580,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = let pl = (List.hd indl).ind_univs in let ctx = Evd.make_evar_universe_context env0 pl in let evdref = ref Evd.(from_ctx ctx) in - let _, ((env_params, ctx_params), userimpls) = + let impls, ((env_params, ctx_params), userimpls) = interp_context_evars env0 evdref paramsl in let ctx_params = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx_params in @@ -590,7 +588,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = (* Names of parameters as arguments of the inductive type (defs removed) *) let assums = List.filter is_local_assum ctx_params in - let params = List.map (RelDecl.get_name %> out_name) assums in + let params = List.map (RelDecl.get_name %> Name.get_id) assums in (* Interpret the arities *) let arities = List.map (interp_ind_arity env_params evdref) indl in @@ -603,7 +601,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = let indimpls = List.map (fun (_, _, impls) -> userimpls @ lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in - let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in + let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in let implsforntn = compute_internalization_env env0 Variable indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in @@ -674,7 +672,7 @@ let extract_coercions indl = let extract_params indl = let paramsl = List.map (fun (_,params,_,_) -> params) indl in match paramsl with - | [] -> anomaly (Pp.str "empty list of inductive types") + | [] -> anomaly (Pp.str "empty list of inductive types.") | params::paramsl -> if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str "Parameters should be syntactically the same for each inductive type."); @@ -907,23 +905,25 @@ let fixsub_module = subtac_dir @ ["Wf"] let tactics_module = subtac_dir @ ["Tactics"] let init_reference dir s () = Coqlib.coq_reference "Command" dir s -let init_constant dir s () = EConstr.of_constr @@ Universes.constr_of_global (Coqlib.coq_reference "Command" dir s) +let init_constant dir s evdref = + let (sigma, c) = Evarutil.new_global !evdref (Coqlib.coq_reference "Command" dir s) + in evdref := sigma; c let make_ref l s = init_reference l s let fix_proto = init_constant tactics_module "fix_proto" let fix_sub_ref = make_ref fixsub_module "Fix_sub" let measure_on_R_ref = make_ref fixsub_module "MR" let well_founded = init_constant ["Init"; "Wf"] "well_founded" -let mkSubset name typ prop = +let mkSubset evdref name typ prop = let open EConstr in - mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).typ), + mkApp (Evarutil.e_new_global evdref (delayed_force build_sigma).typ, [| typ; mkLambda (name, typ, prop) |]) let sigT = Lazy.from_fun build_sigma_type let make_qref s = Qualid (Loc.tag @@ qualid_of_string s) let lt_ref = make_qref "Init.Peano.lt" -let rec telescope l = +let rec telescope evdref l = let open EConstr in let open Vars in match l with @@ -935,10 +935,8 @@ let rec telescope l = (fun (ty, tys, (k, constr)) decl -> let t = RelDecl.get_type decl in let pred = mkLambda (RelDecl.get_name decl, t, ty) in - let ty = Universes.constr_of_global (Lazy.force sigT).typ in - let ty = EConstr.of_constr ty in - let intro = Universes.constr_of_global (Lazy.force sigT).intro in - let intro = EConstr.of_constr intro in + let ty = Evarutil.e_new_global evdref (Lazy.force sigT).typ in + let intro = Evarutil.e_new_global evdref (Lazy.force sigT).intro in let sigty = mkApp (ty, [|t; pred|]) in let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in (sigty, pred :: tys, (succ k, intro))) @@ -947,17 +945,15 @@ let rec telescope l = let (last, subst) = List.fold_right2 (fun pred decl (prev, subst) -> let t = RelDecl.get_type decl in - let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in - let p1 = EConstr.of_constr p1 in - let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in - let p2 = EConstr.of_constr p2 in + let p1 = Evarutil.e_new_global evdref (Lazy.force sigT).proj1 in + let p2 = Evarutil.e_new_global evdref (Lazy.force sigT).proj2 in let proj1 = applist (p1, [t; pred; prev]) in let proj2 = applist (p2, [t; pred; prev]) in (lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst)) (List.rev tys) tl (mkRel 1, []) in ty, (LocalDef (n, last, t) :: subst), constr - | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope tl in + | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope evdref tl in ty, (LocalDef (n, b, t) :: subst), lift 1 term let nf_evar_context sigma ctx = @@ -976,7 +972,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let top_env = push_rel_context binders_rel env in let top_arity = interp_type_evars top_env evdref arityc in let full_arity = it_mkProd_or_LetIn top_arity binders_rel in - let argtyp, letbinders, make = telescope binders_rel in + let argtyp, letbinders, make = telescope evdref binders_rel in let argname = Id.of_string "recarg" in let arg = LocalAssum (Name argname, argtyp) in let binders = letbinders @ [arg] in @@ -1004,7 +1000,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = it_mkLambda_or_LetIn measure letbinders, it_mkLambda_or_LetIn measure binders in - let comb = EConstr.of_constr (Universes.constr_of_global (delayed_force measure_on_R_ref)) in + let comb = Evarutil.e_new_global evdref (delayed_force measure_on_R_ref) in let relargty = EConstr.of_constr relargty in let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in let wf_rel_fun x y = @@ -1012,15 +1008,15 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = subst1 y measure_body |]) in wf_rel, wf_rel_fun, measure in - let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in + let wf_proof = mkApp (well_founded evdref, [| argtyp ; wf_rel |]) in let argid' = Id.of_string (Id.to_string argname ^ "'") in let wfarg len = LocalAssum (Name argid', - mkSubset (Name argid') argtyp + mkSubset evdref (Name argid') argtyp (wf_rel_fun (mkRel 1) (mkRel (len + 1)))) in let intern_bl = wfarg 1 :: [arg] in let _intern_env = push_rel_context intern_bl env in - let proj = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.proj1) in + let proj = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.proj1 in let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in let projection = (* in wfarg :: arg :: before *) mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |]) @@ -1033,7 +1029,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in let curry_fun = let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in - let intro = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro) in + let intro = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.intro in let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in let rcurry = mkApp (rel, [| measure; lift len measure |]) in @@ -1059,7 +1055,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in let prop = mkLambda (Name argname, argtyp, top_arity_let) in let def = - mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)), + mkApp (Evarutil.e_new_global evdref (delayed_force fix_sub_ref), [| argtyp ; wf_rel ; Evarutil.e_new_evar env evdref ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof; @@ -1075,12 +1071,12 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in let hook l gr _ = - let body = it_mkLambda_or_LetIn (mkApp (EConstr.of_constr (Universes.constr_of_global gr), [|make|])) binders_rel in + let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ty = EConstr.Unsafe.to_constr ty in let pl, univs = Evd.universe_context ?names:pl !evdref in (*FIXME poly? *) - let ce = definition_entry ~poly ~types:ty ~univs (EConstr.Unsafe.to_constr (Evarutil.nf_evar !evdref body)) in + let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in @@ -1097,10 +1093,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = in hook, recname, typ in let hook = Lemmas.mk_hook hook in - let fullcoqc = Evarutil.nf_evar !evdref def in - let fullctyp = Evarutil.nf_evar !evdref typ in - let fullcoqc = EConstr.Unsafe.to_constr fullcoqc in - let fullctyp = EConstr.Unsafe.to_constr fullctyp in + let fullcoqc = EConstr.to_constr !evdref def in + let fullctyp = EConstr.to_constr !evdref typ in Obligations.check_evars env !evdref; let evars, _, evars_def, evars_typ = Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp @@ -1143,7 +1137,7 @@ let interp_recursive isfix fixl notations = let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in let fixprot = try - let app = mkApp (delayed_force fix_proto, [|sort; t|]) in + let app = mkApp (fix_proto evdref, [|sort; t|]) in Typing.e_solve_evars env evdref app with e when CErrors.noncritical e -> t in @@ -1303,9 +1297,9 @@ let do_program_recursive local p fixkind fixl ntns = let collect_evars id def typ imps = (* Generalize by the recursive prototypes *) let def = - EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)) + EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign) and typ = - EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)) + EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = |