From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 31 Oct 2017 17:04:02 +0100 Subject: Add relevance marks on binders. Kernel should be mostly correct, higher levels do random stuff at times. --- vernac/comProgramFixpoint.ml | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) (limited to 'vernac/comProgramFixpoint.ml') diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index ae77cf12e5..ad7c65b70c 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -12,6 +12,7 @@ open Pp open CErrors open Util open Constr +open Context open Entries open Vars open Declare @@ -41,7 +42,7 @@ let well_founded sigma = init_constant sigma (lib_ref "core.wf.well_founded") let mkSubset sigma name typ prop = let open EConstr in let sigma, app_h = Evarutil.new_global sigma (delayed_force build_sigma).typ in - sigma, mkApp (app_h, [| typ; mkLambda (name, typ, prop) |]) + sigma, mkApp (app_h, [| typ; mkLambda (make_annot name Sorts.Relevant, typ, prop) |]) let make_qref s = qualid_of_string s let lt_ref = make_qref "Init.Peano.lt" @@ -58,7 +59,7 @@ let rec telescope sigma l = List.fold_left (fun (sigma, ty, tys, (k, constr)) decl -> let t = RelDecl.get_type decl in - let pred = mkLambda (RelDecl.get_name decl, t, ty) in + let pred = mkLambda (RelDecl.get_annot decl, t, ty) in let sigma, ty = Evarutil.new_global sigma (lib_ref "core.sigT.type") in let sigma, intro = Evarutil.new_global sigma (lib_ref "core.sigT.intro") in let sigty = mkApp (ty, [|t; pred|]) in @@ -73,7 +74,7 @@ let rec telescope sigma l = let sigma, p2 = Evarutil.new_global sigma (lib_ref "core.sigT.proj2") in let proj1 = applist (p1, [t; pred; prev]) in let proj2 = applist (p2, [t; pred; prev]) in - (sigma, lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst)) + (sigma, lift 1 proj2, LocalDef (get_annot decl, proj1, t) :: subst)) (List.rev tys) tl (sigma, mkRel 1, []) in sigma, ty, (LocalDef (n, last, t) :: subst), constr @@ -98,7 +99,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let full_arity = it_mkProd_or_LetIn top_arity binders_rel in let sigma, argtyp, letbinders, make = telescope sigma binders_rel in let argname = Id.of_string "recarg" in - let arg = LocalAssum (Name argname, argtyp) in + let arg = LocalAssum (make_annot (Name argname) Sorts.Relevant, argtyp) in let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let sigma, (rel, _) = interp_constr_evars_impls ~program_mode:true env sigma r in @@ -135,7 +136,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let argid' = Id.of_string (Id.to_string argname ^ "'") in let wfarg sigma len = let sigma, ss_term = mkSubset sigma (Name argid') argtyp (wf_rel_fun (mkRel 1) (mkRel (len + 1))) in - sigma, LocalAssum (Name argid', ss_term) + sigma, LocalAssum (make_annot (Name argid') Sorts.Relevant, ss_term) in let sigma, intern_bl = let sigma, wfa = wfarg sigma 1 in @@ -143,7 +144,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = in let _intern_env = push_rel_context intern_bl env in let sigma, proj = Evarutil.new_global sigma (delayed_force build_sigma).Coqlib.proj1 in - let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in + let wfargpred = mkLambda (make_annot (Name argid') Sorts.Relevant, argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in let projection = (* in wfarg :: arg :: before *) mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |]) in @@ -153,22 +154,23 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = now intern_arity is in wfarg :: arg *) let sigma, wfa = wfarg sigma 1 in let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfa] in - let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in + let intern_fun_binder = LocalAssum (make_annot (Name (add_suffix recname "'")) Sorts.Relevant, + intern_fun_arity_prod) in let sigma, curry_fun = - let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in + let wfpred = mkLambda (make_annot (Name argid') Sorts.Relevant, argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in let sigma, intro = Evarutil.new_global sigma (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 = LocalAssum (Name (Id.of_string "recproof"), rcurry) in + let lam = LocalAssum (make_annot (Name (Id.of_string "recproof")) Sorts.Relevant, 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 - sigma, LocalDef (Name recname, body, ty) + sigma, LocalDef (make_annot (Name recname) Sorts.Relevant, body, ty) in let fun_bl = intern_fun_binder :: [arg] in let lift_lets = lift_rel_context 1 letbinders in let sigma, intern_body = - let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in + let ctx = LocalAssum (make_annot (Name recname) Sorts.Relevant, get_type curry_fun) :: binders_rel in let (r, l, impls, scopes) = Constrintern.compute_internalization_data env sigma Constrintern.Recursive full_arity impls @@ -180,7 +182,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = ~impls:newimpls body (lift 1 top_arity) in 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 prop = mkLambda (make_annot (Name argname) Sorts.Relevant, argtyp, top_arity_let) in (* XXX: Previous code did parallel evdref update, so possible old weak ordering semantics may bite here. *) let sigma, def = @@ -272,7 +274,7 @@ let do_program_recursive local poly fixkind fixl ntns = (List.length rec_sign) def typ in (id, def, typ, imps, evars) in - let (fixnames,fixdefs,fixtypes) = fix in + let (fixnames,fixrs,fixdefs,fixtypes) = fix in let fiximps = List.map pi2 info in let fixdefs = List.map out_def fixdefs in let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in @@ -281,7 +283,7 @@ let do_program_recursive local poly fixkind fixl ntns = (* XXX: are we allowed to have evars here? *) let fixtypes = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixtypes in let fixdefs = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixdefs in - let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), + let fixdecls = Array.of_list (List.map2 (fun x r -> make_annot (Name x) r) fixnames fixrs), Array.of_list fixtypes, Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) in -- cgit v1.2.3