diff options
Diffstat (limited to 'vernac/command.ml')
| -rw-r--r-- | vernac/command.ml | 95 |
1 files changed, 45 insertions, 50 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index 8a9bbb8846..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 = @@ -382,7 +380,7 @@ type structured_inductive_expr = local_binder_expr list * structured_one_inductive_expr list let minductive_message warn = function - | [] -> error "No inductive definition." + | [] -> user_err Pp.(str "No inductive definition.") | [x] -> (pr_id x ++ str " is defined" ++ if warn then str " as a non-primitive record" else mt()) | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ @@ -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,10 +672,10 @@ 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 error - "Parameters should be syntactically the same for each inductive type."; + 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."); params let extract_inductive indl = @@ -715,9 +713,9 @@ let declare_mutual_inductive_with_eliminations mie pl impls = begin match mie.mind_entry_finite with | BiFinite when is_recursive mie -> if Option.has_some mie.mind_entry_record then - error "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command." + user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") else - error ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.") + user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")) | _ -> () end; let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in @@ -906,23 +904,26 @@ let subtac_dir = [contrib_name] let fixsub_module = subtac_dir @ ["Wf"] let tactics_module = subtac_dir @ ["Tactics"] -let init_reference dir s () = Coqlib.gen_reference "Command" dir s -let init_constant dir s () = EConstr.of_constr (Coqlib.gen_constant "Command" dir s) +let init_reference dir s () = 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 @@ -934,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))) @@ -946,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 = @@ -975,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 @@ -1003,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 = @@ -1011,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 |]) @@ -1032,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 @@ -1058,10 +1055,10 @@ 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)) wf_proof; + ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof; prop |]) in let def = Typing.e_solve_evars env evdref def in @@ -1074,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 @@ -1096,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 @@ -1122,7 +1117,7 @@ let interp_recursive isfix fixl notations = | x , None -> x | Some ls , Some us -> if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then - error "(co)-recursive definitions should all have the same universe binders"; + user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); Some us) fixl None in let ctx = Evd.make_evar_universe_context env all_universes in let evdref = ref (Evd.from_ctx ctx) in @@ -1142,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 @@ -1262,8 +1257,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let extract_decreasing_argument limit = function | (na,CStructRec) -> na | (na,_) when not limit -> na - | _ -> error - "Only structural decreasing is supported for a non-Program Fixpoint" + | _ -> user_err Pp.(str + "Only structural decreasing is supported for a non-Program Fixpoint") let extract_fixpoint_components limit l = let fixl, ntnl = List.split l in @@ -1282,7 +1277,7 @@ let extract_cofixpoint_components l = let out_def = function | Some def -> def - | None -> error "Program Fixpoint needs defined bodies." + | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.") let collect_evars_of_term evd c ty = let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in @@ -1302,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 = |