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. --- pretyping/cases.ml | 115 ++++++++++++++++++++++++++++++----------------------- 1 file changed, 66 insertions(+), 49 deletions(-) (limited to 'pretyping/cases.ml') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 069ba9572a..e22368d5e5 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -16,6 +16,7 @@ open Util open Names open Nameops open Constr +open Context open Termops open Environ open EConstr @@ -472,7 +473,8 @@ let push_current_pattern ~program_mode sigma (cur,ty) eqn = let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in match eqn.patterns with | pat::pats -> - let _,rhs_env = push_rel ~hypnaming sigma (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in + let r = Sorts.Relevant in (* TODO relevance *) + let _,rhs_env = push_rel ~hypnaming sigma (LocalDef (make_annot (alias_of_pat pat) r,cur,ty)) eqn.rhs.rhs_env in { eqn with rhs = { eqn.rhs with rhs_env = rhs_env }; patterns = pats } @@ -762,7 +764,10 @@ let get_names avoid env sigma sign eqns = (fun (l,avoid) d na -> let na = merge_name - (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid)) + (fun decl -> + let na = get_name decl in + let t = get_type decl in + Name (next_name_away (named_hd env sigma t na) avoid)) d na in (na::l,Id.Set.add (Name.get_id na) avoid)) @@ -782,10 +787,10 @@ let recover_and_adjust_alias_names (_,avoid) names sign = let rec aux = function | [],[] -> [] - | x::names, LocalAssum (_,t)::sign -> - (x, LocalAssum (alias_of_pat x,t)) :: aux (names,sign) + | x::names, LocalAssum (x',t)::sign -> + (x, LocalAssum ({x' with binder_name=alias_of_pat x},t)) :: aux (names,sign) | names, (LocalDef (na,_,_) as decl)::sign -> - (DAst.make @@ PatVar na, decl) :: aux (names,sign) + (DAst.make @@ PatVar na.binder_name, decl) :: aux (names,sign) | _ -> assert false in List.split (aux (names,sign)) @@ -1247,7 +1252,7 @@ let rec generalize_problem names sigma pb = function let pb',deps = generalize_problem names sigma pb l in let d = map_constr (lift i) (lookup_rel i !!(pb.env)) in begin match d with - | LocalDef (Anonymous,_,_) -> pb', deps + | LocalDef ({binder_name=Anonymous},_,_) -> pb', deps | _ -> (* for better rendering *) let d = RelDecl.map_type (fun c -> whd_betaiota sigma c) d in @@ -1436,16 +1441,15 @@ let compile ~program_mode sigma pb = brvals pb.tomatch pb.pred deps cstrs in let brvals = Array.map (fun (sign,body) -> it_mkLambda_or_LetIn body sign) brvals in - let (pred,typ) = + let (pred,typ) = find_predicate pb.caseloc pb.env sigma - pred current indt (names,dep) tomatch in - let ci = make_case_info !!(pb.env) (fst mind) pb.casestyle in + pred current indt (names,dep) tomatch + in + let rci = Typing.check_allowed_sort !!(pb.env) sigma mind current pred in + let ci = make_case_info !!(pb.env) (fst mind) rci pb.casestyle in let pred = nf_betaiota !!(pb.env) sigma pred in - let case = - make_case_or_project !!(pb.env) sigma indf ci pred current brvals - in + let case = make_case_or_project !!(pb.env) sigma indf ci pred current brvals in let sigma, _ = Typing.type_of !!(pb.env) sigma pred in - Typing.check_allowed_sort !!(pb.env) sigma mind current pred; sigma, { uj_val = applist (case, inst); uj_type = prod_applist sigma typ inst } @@ -1460,7 +1464,7 @@ let compile ~program_mode sigma pb = let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let pb = { pb with - env = snd (push_rel ~hypnaming sigma (LocalDef (na,current,ty)) env); + env = snd (push_rel ~hypnaming sigma (LocalDef (annotR na,current,ty)) env); tomatch = tomatch; pred = lift_predicate 1 pred tomatch; history = pop_history pb.history; @@ -1511,7 +1515,8 @@ let compile ~program_mode sigma pb = and compile_alias initial sigma pb (na,orig,(expanded,expanded_typ)) rest = let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let f c t = - let alias = LocalDef (na,c,t) in + let r = Retyping.relevance_of_type !!(pb.env) sigma t in + let alias = LocalDef (make_annot na r,c,t) in let pb = { pb with env = snd (push_rel ~hypnaming sigma alias pb.env); @@ -1524,7 +1529,7 @@ let compile ~program_mode sigma pb = if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then subst1 c j.uj_val else - mkLetIn (na,c,t,j.uj_val); + mkLetIn (make_annot na r,c,t,j.uj_val); uj_type = subst1 c j.uj_type } in (* spiwack: when an alias appears on a deep branch, its non-expanded form is automatically a variable of the same name. We avoid @@ -1812,7 +1817,7 @@ let build_inversion_problem ~program_mode loc env sigma tms t = List.rev_append patl patl',acc_sign,acc | (t, NotInd (bo,typ)) :: tms -> let pat,acc = make_patvar t acc in - let d = LocalAssum (alias_of_pat pat,typ) in + let d = LocalAssum (annotR (alias_of_pat pat),typ) in let patl,acc_sign,acc = aux (n+1) (snd (push_rel ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma d env)) (d::acc_sign) tms acc in pat::patl,acc_sign,acc in let avoid0 = GlobEnv.vars_of_env env in @@ -1913,9 +1918,11 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = match tm with | NotInd (bo,typ) -> (match t with - | None -> let sign = match bo with - | None -> [LocalAssum (na, lift n typ)] - | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign + | None -> + let r = Sorts.Relevant in (* TODO relevance *) + let sign = match bo with + | None -> [LocalAssum (make_annot na r, lift n typ)] + | Some b -> [LocalDef (make_annot na r, lift n b, lift n typ)] in sign | Some {CAst.loc} -> user_err ?loc (str"Unexpected type annotation for a term of non inductive type.")) @@ -1923,7 +1930,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let indf' = if dolift then lift_inductive_family n indf else indf in let ((ind,u),_) = dest_ind_family indf' in let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in - let arsign = fst (get_arity env0 indf') in + let arsign, inds = get_arity env0 indf' in let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in let realnal = match t with @@ -1935,8 +1942,9 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = List.rev realnal | None -> List.make nrealargs_ctxt Anonymous in + let r = Sorts.relevance_of_sort_family inds in let t = EConstr.of_constr (build_dependent_inductive env0 indf') in - LocalAssum (na, t) :: List.map2 RelDecl.set_name realnal arsign in + LocalAssum (make_annot na r, t) :: List.map2 RelDecl.set_name realnal arsign in let rec buildrec n = function | [],[] -> [] | (_,tm)::ltm, (_,x)::tmsign -> @@ -2143,9 +2151,10 @@ let constr_of_pat env sigma arsign pat avoid = | Anonymous -> let previd, id = prime avoid (Name (Id.of_string "wildcard")) in Name id, Id.Set.add id avoid - in - (sigma, (DAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, - (List.map (fun x -> mkRel 1) realargs), 1, avoid) + in + let r = Sorts.Relevant in (* TODO relevance *) + (sigma, (DAst.make ?loc @@ PatVar name), [LocalAssum (make_annot name r, ty)] @ realargs, mkRel 1, ty, + (List.map (fun x -> mkRel 1) realargs), 1, avoid) | PatCstr (((_, i) as cstr),args,alias) -> let cind = inductive_of_constructor cstr in let IndType (indf, _) = @@ -2184,9 +2193,11 @@ let constr_of_pat env sigma arsign pat avoid = match alias with Anonymous -> sigma, pat', sign, app, apptype, realargs, n, avoid - | Name id -> - let sign = LocalAssum (alias, lift m ty) :: sign in - let avoid = Id.Set.add id avoid in + | Name id -> + let _, inds = get_arity env indf in + let r = Sorts.relevance_of_sort_family inds in + let sign = LocalAssum (make_annot alias r, lift m ty) :: sign in + let avoid = Id.Set.add id avoid in let sigma, sign, i, avoid = try let env = EConstr.push_rel_context sign env in @@ -2196,11 +2207,12 @@ let constr_of_pat env sigma arsign pat avoid = (mkRel 1) (* alias *) (lift 1 app) (* aliased term *) in - let neq = eq_id avoid id in - sigma, LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, Id.Set.add neq avoid + let neq = eq_id avoid id in + (* if we ever allow using a SProp-typed coq_eq_ind this relevance will be wrong *) + sigma, LocalDef (nameR neq, mkRel 0, eq_t) :: sign, 2, Id.Set.add neq avoid with Evarconv.UnableToUnify _ -> sigma, sign, 1, avoid in - (* Mark the equality as a hole *) + (* Mark the equality as a hole *) sigma, pat', sign, lift i app, lift i apptype, realargs, n + i, avoid in let sigma, pat', sign, patc, patty, args, z, avoid = typ env sigma (RelDecl.get_type (List.hd arsign), List.tl arsign) pat avoid in @@ -2222,18 +2234,18 @@ match EConstr.kind sigma t with let rels_of_patsign sigma = List.map (fun decl -> match decl with - | LocalDef (na,t',t) when is_topvar sigma t' -> LocalAssum (na,t) + | LocalDef (na,t',t) when is_topvar sigma t' -> LocalAssum (na,t) | _ -> decl) let vars_of_ctx sigma ctx = let _, y = List.fold_right (fun decl (prev, vars) -> match decl with - | LocalDef (na,t',t) when is_topvar sigma t' -> + | LocalDef (na,t',t) when is_topvar sigma t' -> prev, (DAst.make @@ GApp ( (DAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), - [hole na; DAst.make @@ GVar prev])) :: vars + [hole na.binder_name; DAst.make @@ GVar prev])) :: vars | _ -> match RelDecl.get_name decl with Anonymous -> invalid_arg "vars_of_ctx" @@ -2343,12 +2355,13 @@ let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity = let args = List.rev args in substl args (liftn signlen (succ nargs) arity) in - let rhs_rels', tycon = + let r = Sorts.Relevant in (* TODO relevance *) + let rhs_rels', tycon = let neqs_rels, arity = match ineqs with | None -> [], arity | Some ineqs -> - [LocalAssum (Anonymous, ineqs)], lift 1 arity + [LocalAssum (make_annot Anonymous r, ineqs)], lift 1 arity in let eqs_rels, arity = decompose_prod_n_assum sigma neqs arity in eqs_rels @ neqs_rels @ rhs_rels', arity @@ -2359,7 +2372,7 @@ let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity = and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in let sigma, _btype = Typing.type_of !!env sigma bbody in let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in - let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in + let branch_decl = LocalDef (make_annot (Name branch_name) r, lift !i bbody, lift !i btype) in let branch = let bref = DAst.make @@ GVar branch_name in match vars_of_ctx sigma rhs_rels with @@ -2407,9 +2420,10 @@ let abstract_tomatch env sigma tomatchs tycon = | _ -> let tycon = Option.map (fun t -> subst_term sigma (lift 1 c) (lift 1 t)) tycon in - let name = next_ident_away (Id.of_string "filtered_var") names in + let name = next_ident_away (Id.of_string "filtered_var") names in + let r = Sorts.Relevant in (* TODO relevance *) (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, - LocalDef (Name name, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx, + LocalDef (make_annot (Name name) r, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx, Id.Set.add name names, tycon) ([], [], Id.Set.empty, tycon) tomatchs in List.rev prev, ctx, tycon @@ -2471,8 +2485,8 @@ let build_dependent_signature env sigma avoid tomatchs arsign = make_prime avoid name in (sigma, env, succ nargeqs, - (LocalAssum (Name (eq_id avoid previd), eq)) :: argeqs, - refl_arg :: refl_args, + (LocalAssum (make_annot (Name (eq_id avoid previd)) Sorts.Relevant, eq)) :: argeqs, + refl_arg :: refl_args, pred slift, RelDecl.set_name (Name id) decl :: argsign')) (sigma, env, neqs, [], [], slift, []) args argsign @@ -2486,8 +2500,8 @@ let build_dependent_signature env sigma avoid tomatchs arsign = in let sigma, refl_eq = mk_JMeq_refl sigma ty tm in let previd, id = make_prime avoid appn in - (sigma, (LocalAssum (Name (eq_id avoid previd), eq) :: argeqs) :: eqs, - succ nargeqs, + (sigma, (LocalAssum (make_annot (Name (eq_id avoid previd)) Sorts.Relevant, eq) :: argeqs) :: eqs, + succ nargeqs, refl_eq :: refl_args, pred slift, ((RelDecl.set_name (Name id) app_decl :: argsign') :: arsigns)) @@ -2503,8 +2517,9 @@ let build_dependent_signature env sigma avoid tomatchs arsign = (mkRel slift) (lift nar tm) in let sigma, refl = mk_eq_refl sigma tomatch_ty tm in + let na = make_annot (Name (eq_id avoid previd)) Sorts.Relevant in (sigma, - [LocalAssum (Name (eq_id avoid previd), eq)] :: eqs, succ neqs, + [LocalAssum (na, eq)] :: eqs, succ neqs, refl :: refl_args, pred slift, (arsign' :: []) :: arsigns)) (sigma, [], 0, [], nar, []) tomatchs arsign @@ -2580,11 +2595,12 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env (* We push the initial terms to match and push their alias to rhs' envs *) (* names of aliases will be recovered from patterns (hence Anonymous here) *) - let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t) - | NotInd (Some b, t) -> LocalDef (na,b,t) - | IsInd (typ,_,_) -> LocalAssum (na,typ) in + (* TODO relevance *) + let out_tmt na = function NotInd (None,t) -> LocalAssum (make_annot na Sorts.Relevant,t) + | NotInd (Some b, t) -> LocalDef (make_annot na Sorts.Relevant,b,t) + | IsInd (typ,_,_) -> LocalAssum (make_annot na Sorts.Relevant,typ) in let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in - + let typs = List.map (fun (c,d) -> (c,extract_inductive_data !!env sigma d,d)) typs in @@ -2654,10 +2670,11 @@ let compile_cases ?loc ~program_mode style (typing_fun, sigma) tycon env (predop (* names of aliases will be recovered from patterns (hence Anonymous *) (* here) *) + (* TODO relevance *) let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t) | NotInd (Some b,t) -> LocalDef (na,b,t) | IsInd (typ,_,_) -> LocalAssum (na,typ) in - let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in + let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt (make_annot na Sorts.Relevant) tmt)) nal tomatchs in let typs = List.map (fun (c,d) -> (c,extract_inductive_data !!env sigma d,d)) typs in -- cgit v1.2.3