diff options
Diffstat (limited to 'toplevel/command.ml')
-rw-r--r-- | toplevel/command.ml | 281 |
1 files changed, 165 insertions, 116 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 5d2a7638..a9f2598e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -7,14 +7,12 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Flags open Term open Vars -open Context open Termops -open Entries open Environ open Redexpr open Declare @@ -37,17 +35,20 @@ open Evarconv open Indschemes open Misctypes open Vernacexpr +open Sigma.Notations +open Context.Rel.Declaration +open Entries let do_universe poly l = Declare.do_universe poly l let do_constraint poly l = Declare.do_constraint poly l let rec under_binders env sigma f n c = - if Int.equal n 0 then snd (f env sigma c) else + if Int.equal n 0 then f env sigma c else match kind_of_term c with | Lambda (x,t,c) -> - mkLambda (x,t,under_binders (push_rel (x,None,t) env) sigma f (n-1) c) + mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c) | LetIn (x,b,t,c) -> - mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) sigma f (n-1) c) + mkLetIn (x,b,t,under_binders (push_rel (LocalDef (x,b,t)) env) sigma f (n-1) c) | _ -> assert false let rec complete_conclusion a cs = function @@ -72,11 +73,21 @@ let red_constant_entry n ce sigma = function | Some red -> let proof_out = ce.const_entry_body in 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 + c + in { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out - (fun ((body,ctx),eff) -> - (under_binders env sigma - (fst (reduction_of_red_expr env red)) n body,ctx),eff) } - + (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) } + +let warn_implicits_in_term = + CWarnings.create ~name:"implicits-in-term" ~category:"implicits" + (fun () -> + strbrk "Implicit arguments declaration relies on type." ++ spc () ++ + strbrk "The term declares more implicits than the type here.") + let interp_definition pl bl p red_option c ctypopt = let env = Global.env() in let ctx = Evd.make_evar_universe_context env pl in @@ -87,7 +98,7 @@ let interp_definition pl bl p red_option c ctypopt = match ctypopt with None -> let subst = evd_comb0 Evd.nf_univ_variables evdref in - let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in + let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in let env_bl = push_rel_context ctx env in let c, imps2 = interp_constr_evars_impls ~impls env_bl evdref c in let nf,subst = Evarutil.e_nf_evars_and_universes evdref in @@ -100,7 +111,7 @@ let interp_definition pl bl p red_option c ctypopt = | Some ctyp -> let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in let subst = evd_comb0 Evd.nf_univ_variables evdref in - let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in + let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in let env_bl = push_rel_context ctx env in let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in let nf, subst = Evarutil.e_nf_evars_and_universes evdref in @@ -114,9 +125,7 @@ let interp_definition pl bl p red_option c ctypopt = impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *) in if not (try List.for_all chk imps2 with Not_found -> false) - then msg_warning - (strbrk "Implicit arguments declaration relies on type." ++ spc () ++ - strbrk "The term declares more implicits than the type here."); + then warn_implicits_in_term (); let vars = Univ.LSet.union (Universes.universes_of_constr body) (Universes.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in @@ -125,23 +134,27 @@ let interp_definition pl bl p red_option c ctypopt = definition_entry ~types:typ ~poly:p ~univs:uctx body in - red_constant_entry (rel_context_length ctx) ce !evdref red_option, !evdref, pl, imps + red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps let check_definition (ce, evd, _, imps) = check_evars_are_solved (Global.env ()) evd (Evd.empty,evd); ce -let get_locality id = function +let warn_local_declaration = + CWarnings.create ~name:"local-declaration" ~category:"scope" + (fun (id,kind) -> + pr_id id ++ strbrk " is declared as a local " ++ str kind) + +let get_locality id ~kind = function | Discharge -> (** If a Let is defined outside a section, then we consider it as a local definition *) - let msg = pr_id id ++ strbrk " is declared as a local definition" in - let () = msg_warning msg in + warn_local_declaration (id,kind); true | Local -> true | Global -> false let declare_global_definition ident ce local k pl imps = - let local = get_locality ident local in + let local = get_locality ident ~kind:"definition" local in let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in @@ -153,6 +166,12 @@ let declare_definition_hook = ref ignore let set_declare_definition_hook = (:=) declare_definition_hook let get_declare_definition_hook () = !declare_definition_hook +let warn_definition_not_visible = + CWarnings.create ~name:"definition-not-visible" ~category:"implicits" + (fun ident -> + strbrk "Section definition " ++ + pr_id ident ++ strbrk " is not visible from current goals") + let declare_definition ident (local, p, k) ce pl imps hook = let fix_exn = Future.fix_exn_of ce.const_entry_body in let () = !declare_definition_hook ce in @@ -164,9 +183,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = let gr = VarRef ident in let () = maybe_declare_manual_implicits false gr imps in let () = if Pfedit.refining () then - let msg = strbrk "Section definition " ++ - pr_id ident ++ strbrk " is not visible from current goals" in - msg_warning msg + warn_definition_not_visible ident in gr | Discharge | Local | Global -> @@ -177,7 +194,9 @@ let _ = Obligations.declare_definition_ref := (fun i k c imps hook -> declare_definition i k c [] imps hook) let do_definition ident k pl bl red_option c ctypopt hook = - let (ce, evd, pl, imps as def) = interp_definition pl bl (pi2 k) red_option c ctypopt in + let (ce, evd, pl', imps as def) = + interp_definition pl bl (pi2 k) red_option c ctypopt + in if Flags.is_program_mode () then let env = Global.env () in let (c,ctx), sideff = Future.force ce.const_entry_body in @@ -194,9 +213,9 @@ let do_definition ident k pl bl red_option c ctypopt hook = let ctx = Evd.evar_universe_context evd in let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in ignore(Obligations.add_definition - ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls) + ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in - ignore(declare_definition ident k ce pl imps + ignore(declare_definition ident k ce pl' imps (Lemmas.mk_hook (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) @@ -210,7 +229,7 @@ match local with let () = assumption_message ident in let () = if is_verbose () && Pfedit.refining () then - msg_warning (str"Variable" ++ spc () ++ pr_id ident ++ + Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++ strbrk " is not visible from current goals") in let r = VarRef ident in @@ -219,7 +238,7 @@ match local with (r,Univ.Instance.empty,true) | Global | Local | Discharge -> - let local = get_locality ident local in + let local = get_locality ident ~kind:"axiom" local in let inl = match nl with | NoInline -> None | DefaultInline -> Some (Flags.get_inline_level()) @@ -242,10 +261,7 @@ match local with let interp_assumption evdref env impls bl c = let c = prod_constr_expr c bl in - let ty, impls = interp_type_evars_impls env evdref ~impls c in - let evd, nf = nf_evars_and_universes !evdref in - let ctx = Evd.universe_context_set evd in - ((nf ty, ctx), impls) + interp_type_evars_impls env evdref ~impls c let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl = let refs, status, _ = @@ -258,6 +274,7 @@ let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl = List.rev refs, status let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = + let open Context.Named.Declaration in let env = Global.env () in let evdref = ref (Evd.from_env env) in let l = @@ -269,26 +286,32 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = l [] else l in + (* We intepret all declarations in the same evar_map, i.e. as a telescope. *) let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) -> - let (t,ctx),imps = interp_assumption evdref env ienv [] c in + let t,imps = interp_assumption evdref env ienv [] c in let env = - push_named_context (List.map (fun (_,id) -> (id,None,t)) idl) env in + push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in let ienv = List.fold_right (fun (_,id) ienv -> let impls = compute_internalization_data env Variable t imps in Id.Map.add id impls ienv) idl ienv in - ((env,ienv),((is_coe,idl),t,(ctx,imps)))) + ((env,ienv),((is_coe,idl),t,imps))) (env,empty_internalization_env) l in let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in + (* The universe constraints come from the whole telescope. *) + let evd = Evd.nf_constraints evd in + let ctx = Evd.universe_context_set evd in let l = List.map (on_pi2 (nf_evar evd)) l in - snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) -> + pi2 (List.fold_left (fun (subst,status,ctx) ((is_coe,idl),t,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,u) -> (id,Universes.constr_of_global_univ (c,u))) idl refs in - (subst'@subst, status' && status)) ([],true) l) + (subst'@subst, status' && status, + (* The universe constraints are declared with the first declaration only. *) + Univ.ContextSet.empty)) ([],true,ctx) l) let do_assumptions_bound_univs coe kind nl id pl c = let env = Global.env () in @@ -334,7 +357,7 @@ let do_assumptions kind nl l = match l with (* 3b| Mutual inductive definitions *) let push_types env idl tl = - List.fold_left2 (fun env id t -> Environ.push_rel (Name id,None,t) env) + List.fold_left2 (fun env id t -> Environ.push_rel (LocalAssum (Name id,t)) env) env idl tl type structured_one_inductive_expr = { @@ -377,8 +400,8 @@ let mk_mltype_data evdref env assums arity indname = (is_ml_type,indname,assums) let prepare_param = function - | (na,None,t) -> out_name na, LocalAssum t - | (na,Some b,_) -> out_name na, LocalDef b + | LocalAssum (na,t) -> out_name na, LocalAssumEntry t + | LocalDef (na,b,_) -> out_name 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. @@ -432,12 +455,12 @@ let interp_cstrs evdref env impls mldata arity ind = let sign_level env evd sign = fst (List.fold_right - (fun (_,b,t as d) (lev,env) -> - match b with - | Some _ -> (lev, push_rel d env) - | None -> - let s = destSort (Reduction.whd_betadeltaiota env - (nf_evar evd (Retyping.get_type_of env evd t))) + (fun d (lev,env) -> + match d with + | LocalDef _ -> lev, push_rel d env + | LocalAssum _ -> + let s = destSort (Reduction.whd_all env + (nf_evar evd (Retyping.get_type_of env evd (get_type d)))) in let u = univ_of_sort s in (Univ.sup u lev, push_rel d env)) @@ -448,7 +471,7 @@ let sup_list min = List.fold_left Univ.sup min let extract_level env evd min tys = let sorts = List.map (fun ty -> let ctx, concl = Reduction.dest_prod_assum env ty in - sign_level env evd ((Anonymous, None, concl) :: ctx)) tys + sign_level env evd (LocalAssum (Anonymous, concl) :: ctx)) tys in sup_list min sorts let is_flexible_sort evd u = @@ -517,11 +540,9 @@ let inductive_levels env evdref poly arities inds = in let duu = Sorts.univ_of_sort du in let evd = - if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then - if is_flexible_sort evd duu then - if Evd.check_leq evd Univ.type0_univ duu then - evd - else Evd.set_eq_sort env evd (Prop Null) du + if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then + if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then + Evd.set_eq_sort env evd (Prop Null) du else evd else Evd.set_eq_sort env evd (Type cu) du in @@ -540,6 +561,7 @@ let check_param = function | LocalRawDef (na, _) -> check_named na | LocalRawAssum (nas, Default _, _) -> List.iter check_named nas | LocalRawAssum (nas, Generalized _, _) -> () +| LocalPattern _ -> assert false let interp_mutual_inductive (paramsl,indl) notations poly prv finite = check_all_names_different indl; @@ -554,8 +576,8 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = let indnames = List.map (fun ind -> ind.ind_name) indl in (* Names of parameters as arguments of the inductive type (defs removed) *) - let assums = List.filter(fun (_,b,_) -> Option.is_empty b) ctx_params in - let params = List.map (fun (na,_,_) -> out_name na) assums in + let assums = List.filter is_local_assum ctx_params in + let params = List.map (fun decl -> out_name (get_name decl)) assums in (* Interpret the arities *) let arities = List.map (interp_ind_arity env_params evdref) indl in @@ -566,7 +588,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = (* Compute interpretation metadatas *) let indimpls = List.map (fun (_, _, impls) -> userimpls @ - lift_implicits (rel_context_nhyps ctx_params) impls) arities in + 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 mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in @@ -592,11 +614,11 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = let nf x = nf' (nf x) in let arities = List.map nf' arities in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in - let ctx_params = map_rel_context nf ctx_params in + let ctx_params = Context.Rel.map nf ctx_params in let evd = !evdref in let pl, uctx = Evd.universe_context ?names:pl evd in List.iter (check_evars env_params Evd.empty evd) arities; - iter_rel_context (check_evars env0 Evd.empty evd) ctx_params; + Context.Rel.iter (check_evars env0 Evd.empty evd) ctx_params; List.iter (fun (_,ctyps,_) -> List.iter (check_evars env_ar_params Evd.empty evd) ctyps) constructors; @@ -610,7 +632,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_lc = ctypes }) indl arities aritypoly constructors in let impls = - let len = rel_context_nhyps ctx_params in + let len = Context.Rel.nhyps ctx_params in List.map2 (fun indimpls (_,_,cimpls) -> indimpls, List.map (fun impls -> userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors @@ -622,7 +644,8 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_inds = entries; mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; - mind_entry_universes = uctx }, + mind_entry_universes = uctx; + }, pl, impls (* Very syntactical equality *) @@ -698,7 +721,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls = constrimpls) impls; let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in - if_verbose msg_info (minductive_message warn_prim names); + if_verbose Feedback.msg_info (minductive_message warn_prim names); if mie.mind_entry_private == None then declare_default_schemes mind; mind @@ -716,8 +739,10 @@ let do_mutual_inductive indl poly prv finite = (* Declare the possible notations of inductive types *) List.iter Metasyntax.add_notation_interpretation ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes - + List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes; + (* If positivity is assumed declares itself as unsafe. *) + if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () + (* 3c| Fixpoints and co-fixpoints *) (* An (unoptimized) function that maps preorders to partial orders... @@ -768,20 +793,25 @@ let rec partial_order cmp = function let non_full_mutual_message x xge y yge isfix rest = let reason = if Id.List.mem x yge then - pr_id y ++ str " depends on " ++ pr_id x ++ str " but not conversely" + pr_id y ++ str " depends on " ++ pr_id x ++ strbrk " but not conversely" else if Id.List.mem y xge then - pr_id x ++ str " depends on " ++ pr_id y ++ str " but not conversely" + pr_id x ++ str " depends on " ++ pr_id y ++ strbrk " but not conversely" else - pr_id y ++ str " and " ++ pr_id x ++ str " are not mutually dependent" in - let e = if List.is_empty rest then reason else str "e.g., " ++ reason in + pr_id y ++ str " and " ++ pr_id x ++ strbrk " are not mutually dependent" in + let e = if List.is_empty rest then reason else strbrk "e.g., " ++ reason in let k = if isfix then "fixpoint" else "cofixpoint" in let w = if isfix - then str "Well-foundedness check may fail unexpectedly." ++ fnl() + then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl() else mt () in - str "Not a fully mutually defined " ++ str k ++ fnl () ++ + strbrk "Not a fully mutually defined " ++ str k ++ fnl () ++ str "(" ++ e ++ str ")." ++ fnl () ++ w +let warn_non_full_mutual = + CWarnings.create ~name:"non-full-mutual" ~category:"fixpoints" + (fun (x,xge,y,yge,isfix,rest) -> + non_full_mutual_message x xge y yge isfix rest) + let check_mutuality env isfix fixl = let names = List.map fst fixl in let preorder = @@ -791,7 +821,7 @@ let check_mutuality env isfix fixl = let po = partial_order Id.equal preorder in match List.filter (function (_,Inr _) -> true | _ -> false) po with | (x,Inr xge)::(y,Inr yge)::rest -> - msg_warning (non_full_mutual_message x xge y yge isfix rest) + warn_non_full_mutual (x,xge,y,yge,isfix,rest) | _ -> () type structured_fixpoint_expr = { @@ -826,7 +856,7 @@ let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t im declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) let _ = Obligations.declare_fix_ref := - (fun ?opaque k ctx f d t imps -> declare_fix ?opaque k [] ctx f d t imps) + (fun ?opaque k ctx f d t imps -> declare_fix ?opaque k [] ctx f d t imps) let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in @@ -868,19 +898,20 @@ let well_founded = init_constant ["Init"; "Wf"] "well_founded" let mkSubset name typ prop = mkApp (Universes.constr_of_global (delayed_force build_sigma).typ, [| typ; mkLambda (name, typ, prop) |]) -let sigT = Lazy.lazy_from_fun build_sigma_type +let sigT = Lazy.from_fun build_sigma_type let make_qref s = Qualid (Loc.ghost, qualid_of_string s) let lt_ref = make_qref "Init.Peano.lt" let rec telescope = function | [] -> assert false - | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1 - | (n, None, t) :: tl -> + | [LocalAssum (n, t)] -> t, [LocalDef (n, mkRel 1, t)], mkRel 1 + | LocalAssum (n, t) :: tl -> let ty, tys, (k, constr) = List.fold_left - (fun (ty, tys, (k, constr)) (n, b, t) -> - let pred = mkLambda (n, t, ty) in + (fun (ty, tys, (k, constr)) decl -> + let t = get_type decl in + let pred = mkLambda (get_name decl, t, ty) in let ty = Universes.constr_of_global (Lazy.force sigT).typ in let intro = Universes.constr_of_global (Lazy.force sigT).intro in let sigty = mkApp (ty, [|t; pred|]) in @@ -889,26 +920,27 @@ let rec telescope = function (t, [], (2, mkRel 1)) tl in let (last, subst) = List.fold_right2 - (fun pred (n, b, t) (prev, subst) -> + (fun pred decl (prev, subst) -> + let t = get_type decl in let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in let proj1 = applistc p1 [t; pred; prev] in let proj2 = applistc p2 [t; pred; prev] in - (lift 1 proj2, (n, Some proj1, t) :: subst)) + (lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst)) (List.rev tys) tl (mkRel 1, []) - in ty, ((n, Some last, t) :: subst), constr + in ty, (LocalDef (n, last, t) :: subst), constr - | (n, Some b, t) :: tl -> let ty, subst, term = telescope tl in - ty, ((n, Some b, t) :: subst), lift 1 term + | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope tl in + ty, (LocalDef (n, b, t) :: subst), lift 1 term let nf_evar_context sigma ctx = - List.map (fun (n, b, t) -> - (n, Option.map (Evarutil.nf_evar sigma) b, Evarutil.nf_evar sigma t)) ctx + List.map (map_constr (Evarutil.nf_evar sigma)) ctx -let build_wellfounded (recname,n,bl,arityc,body) r measure notation = +let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = Coqlib.check_required_library ["Coq";"Program";"Wf"]; let env = Global.env() in - let evdref = ref (Evd.from_env env) in + let ctx = Evd.make_evar_universe_context env pl in + let evdref = ref (Evd.from_ctx ctx) in let _, ((env', binders_rel), impls) = interp_context_evars env evdref bl in let len = List.length binders_rel in let top_env = push_rel_context binders_rel env in @@ -916,11 +948,10 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let full_arity = it_mkProd_or_LetIn top_arity binders_rel in let argtyp, letbinders, make = telescope binders_rel in let argname = Id.of_string "recarg" in - let arg = (Name argname, None, argtyp) in + let arg = LocalAssum (Name argname, argtyp) in let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let rel, _ = interp_constr_evars_impls env evdref r in - let () = check_evars_are_solved env !evdref (Evd.empty,!evdref) in let relty = Typing.unsafe_type_of env !evdref rel in let relargty = let error () = @@ -931,10 +962,10 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = try let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in match ctx, kind_of_term ar with - | [(_, None, t); (_, None, u)], Sort (Prop Null) + | [LocalAssum (_,t); LocalAssum (_,u)], Sort (Prop Null) when Reductionops.is_conv env !evdref t u -> t | _, _ -> error () - with e when Errors.noncritical e -> error () + with e when CErrors.noncritical e -> error () in let measure = interp_casted_constr_evars binders_env evdref measure relargty in let wf_rel, wf_rel_fun, measure_fn = @@ -951,9 +982,9 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = in let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in let argid' = Id.of_string (Id.to_string argname ^ "'") in - let wfarg len = (Name argid', None, - mkSubset (Name argid') argtyp - (wf_rel_fun (mkRel 1) (mkRel (len + 1)))) + let wfarg len = LocalAssum (Name argid', + mkSubset (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 @@ -967,22 +998,22 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = (* substitute the projection of wfarg for something, now intern_arity is in wfarg :: arg *) let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in - let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in + 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*)Universes.constr_of_global (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 - let lam = (Name (Id.of_string "recproof"), None, rcurry) in + let lam = LocalAssum (Name (Id.of_string "recproof"), rcurry) in let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in - (Name recname, Some body, ty) + LocalDef (Name recname, body, ty) in let fun_bl = intern_fun_binder :: [arg] in let lift_lets = Termops.lift_rel_context 1 letbinders in let intern_body = - let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in + let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in let (r, l, impls, scopes) = Constrintern.compute_internalization_data env Constrintern.Recursive full_arity impls @@ -1002,7 +1033,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof; prop |]) in - let def = Typing.solve_evars env evdref def in + let def = Typing.e_solve_evars env evdref def in let _ = evdref := Evarutil.nf_evar_map !evdref in let def = mkApp (def, [|intern_body_lam|]) in let binders_rel = nf_evar_context !evdref binders_rel in @@ -1014,9 +1045,9 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let hook l gr _ = let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in - let pl, univs = Evd.universe_context !evdref in + let pl, univs = Evd.universe_context ?names:pl !evdref in (*FIXME poly? *) - let ce = definition_entry ~types:ty ~univs (Evarutil.nf_evar !evdref body) in + let ce = definition_entry ~poly ~types:ty ~univs (Evarutil.nf_evar !evdref body) in (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in @@ -1040,10 +1071,11 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp in let ctx = Evd.evar_universe_context !evdref in - ignore(Obligations.add_definition recname ~term:evars_def + ignore(Obligations.add_definition recname ~term:evars_def ?pl evars_typ ctx evars ~hook) let interp_recursive isfix fixl notations = + let open Context.Named.Declaration in let env = Global.env() in let fixnames = List.map (fun fix -> fix.fix_name) fixl in @@ -1056,7 +1088,7 @@ let interp_recursive isfix fixl notations = | 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"; - Some (ls @ us)) fixl None in + Some us) fixl None in let ctx = Evd.make_evar_universe_context env all_universes in let evdref = ref (Evd.from_ctx ctx) in let fixctxs, fiximppairs, fixannots = @@ -1076,11 +1108,11 @@ let interp_recursive isfix fixl notations = let fixprot = try let app = mkApp (delayed_force fix_proto, [|sort; t|]) in - Typing.solve_evars env evdref app - with e when Errors.noncritical e -> t + Typing.e_solve_evars env evdref app + with e when CErrors.noncritical e -> t in - (id,None,fixprot) :: env' - else (id,None,t) :: env') + LocalAssum (id,fixprot) :: env' + else LocalAssum (id,t) :: env') [] fixnames fixtypes in let env_rec = push_named_context rec_sign env in @@ -1098,11 +1130,11 @@ let interp_recursive isfix fixl notations = () in (* Instantiate evars and check all are resolved *) - let evd = consider_remaining_unif_problems env_rec !evdref in + let evd = solve_unif_constraints_with_heuristics env_rec !evdref in let evd, nf = nf_evars_and_universes evd in let fixdefs = List.map (Option.map nf) fixdefs in let fixtypes = List.map nf fixtypes in - let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in + let fixctxnames = List.map (fun (_,ctx) -> List.map get_name ctx) fixctxs in (* Build the fix declaration block *) (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots @@ -1220,6 +1252,11 @@ let out_def = function | Some def -> def | None -> error "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 + Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) + evars (Evd.from_ctx (Evd.evar_universe_context evd)) + let do_program_recursive local p fixkind fixl ntns = let isfix = fixkind != Obligations.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = @@ -1237,8 +1274,9 @@ let do_program_recursive local p fixkind fixl ntns = and typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in + let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = - Obligations.eterm_obligations env id evd + Obligations.eterm_obligations env id evm (List.length rec_sign) def typ in (id, def, typ, imps, evars) in @@ -1253,30 +1291,34 @@ let do_program_recursive local p fixkind fixl ntns = Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) in let indexes = - Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in - List.iteri (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl + Pretyping.search_guard + Loc.ghost (Global.env ()) possible_indexes fixdecls in + List.iteri (fun i _ -> + Inductive.check_fix env + ((indexes,i),fixdecls)) + fixl end in let ctx = Evd.evar_universe_context evd in let kind = match fixkind with | Obligations.IsFixpoint _ -> (local, p, Fixpoint) | Obligations.IsCoFixpoint -> (local, p, CoFixpoint) in - Obligations.add_mutual_definitions defs ~kind ctx ntns fixkind + Obligations.add_mutual_definitions defs ~kind ?pl ctx ntns fixkind let do_program_fixpoint local poly l = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in match g, l with - | [(n, CWfRec r)], [((((_,id),_),_,bl,typ,def),ntn)] -> + | [(n, CWfRec r)], [((((_,id),pl),_,bl,typ,def),ntn)] -> let recarg = match n with | Some n -> mkIdentC (snd n) | None -> errorlabstrm "do_program_fixpoint" (str "Recursive argument required for well-founded fixpoints") - in build_wellfounded (id, n, bl, typ, out_def def) r recarg ntn + in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn - | [(n, CMeasureRec (m, r))], [((((_,id),_),_,bl,typ,def),ntn)] -> - build_wellfounded (id, n, bl, typ, out_def def) + | [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] -> + build_wellfounded (id, pl, n, bl, typ, out_def def) poly (Option.default (CRef (lt_ref,None)) r) m ntn | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g -> @@ -1288,6 +1330,11 @@ let do_program_fixpoint local poly l = errorlabstrm "do_program_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") +let check_safe () = + let open Declarations in + let flags = Environ.typing_flags (Global.env ()) in + flags.check_universes && flags.check_guarded + let do_fixpoint local poly l = if Flags.is_program_mode () then do_program_fixpoint local poly l else @@ -1295,7 +1342,8 @@ let do_fixpoint local poly l = let (_, _, _, info as fix) = interp_fixpoint fixl ntns in let possible_indexes = List.map compute_possible_guardness_evidences info in - declare_fixpoint local poly fix possible_indexes ntns + declare_fixpoint local poly fix possible_indexes ntns; + if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () let do_cofixpoint local poly l = let fixl,ntns = extract_cofixpoint_components l in @@ -1303,4 +1351,5 @@ let do_cofixpoint local poly l = do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns else let cofix = interp_cofixpoint fixl ntns in - declare_cofixpoint local poly cofix ntns + declare_cofixpoint local poly cofix ntns; + if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () |