From fe3e6c5d307ae6b9c13f28959d32e3f5d680eccb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Thu, 6 Jun 2024 11:22:17 +0200 Subject: [PATCH] Turn context_map into a record. --- src/context_map.ml | 65 ++++++++++++++++---------- src/context_map.mli | 10 ++-- src/covering.ml | 98 ++++++++++++++++++++++------------------ src/covering.mli | 2 +- src/principles.ml | 78 ++++++++++++++++++-------------- src/principles.mli | 7 +-- src/principles_proofs.ml | 22 +++++---- src/sigma_types.ml | 31 +++++++------ src/simplify.ml | 3 +- src/splitting.ml | 57 +++++++++++++---------- 10 files changed, 211 insertions(+), 162 deletions(-) diff --git a/src/context_map.ml b/src/context_map.ml index 0915d266..39604b68 100644 --- a/src/context_map.ml +++ b/src/context_map.ml @@ -28,8 +28,11 @@ type pat = | PInac of constr | PHide of int -type context_map = rel_context * pat list * rel_context - +type context_map = { + src_ctx : rel_context; + map_inst : pat list; + tgt_ctx : rel_context; +} let type_of_refresh env evdref c = let ty = Retyping.get_type_of env !evdref c in @@ -131,9 +134,9 @@ let rec pat_to_user_pat ?(avoid = ref Id.Set.empty) ?loc ctx = function and pats_to_lhs ?(avoid = ref Id.Set.empty) ?loc ctx pats = List.map_filter (pat_to_user_pat ~avoid ?loc ctx) pats -let context_map_to_lhs ?(avoid = Id.Set.empty) ?loc (ctx, pats, _) = +let context_map_to_lhs ?(avoid = Id.Set.empty) ?loc map = let avoid = ref avoid in - List.rev (pats_to_lhs ~avoid ?loc ctx pats) + List.rev (pats_to_lhs ~avoid ?loc map.src_ctx map.map_inst) let do_renamings env sigma ctx = let avoid, ctx' = @@ -179,7 +182,7 @@ let pr_context env sigma ctx = let ppcontext = ppenv_sigma pr_context -let pr_context_map env sigma (delta, patcs, gamma) = +let pr_context_map env sigma { src_ctx = delta; map_inst = patcs; tgt_ctx = gamma } = let env' = push_rel_context delta env in let ctx = pr_context env sigma delta in let ctx' = pr_context env sigma gamma in @@ -195,7 +198,7 @@ let ppcontext_map_empty = ppenv_sigma pr_context_map (** Debugging functions *) -let typecheck_map env evars (ctx, subst, ctx') = +let typecheck_map env evars { src_ctx = ctx; map_inst = subst; tgt_ctx = ctx' } = typecheck_rel_context env evars ctx; typecheck_rel_context env evars ctx'; let env = push_rel_context ctx env in @@ -227,7 +230,12 @@ let check_ctx_map ?(unsafe = false) env evars map = else map let mk_ctx_map ?(unsafe = false) env evars ctx subst ctx' = - let map = (ctx, subst, ctx') in check_ctx_map ~unsafe env evars map + let map = { + src_ctx = ctx; + map_inst = subst; + tgt_ctx = ctx'; + } in + check_ctx_map ~unsafe env evars map let rec map_patterns f ps = List.map (function @@ -238,8 +246,11 @@ let rec map_patterns f ps = | x -> x) ps -let map_ctx_map f (g, p, d) = - map_rel_context f g, map_patterns f p, map_rel_context f d +let map_ctx_map f map = { + src_ctx = map_rel_context f map.src_ctx; + map_inst = map_patterns f map.map_inst; + tgt_ctx = map_rel_context f map.tgt_ctx; +} (** Specialize by a substitution. *) @@ -285,7 +296,7 @@ let specialize_rel_context sigma s ctx = ctx (0, []) in res -let mapping_constr sigma (s : context_map) c = specialize_constr sigma (pi2 s) c +let mapping_constr sigma (s : context_map) c = specialize_constr sigma s.map_inst c (* Substitute a Constr.t in a pattern. *) @@ -326,8 +337,11 @@ let rec eq_pat env sigma p1 p2 = | PInac c, PInac c' -> EConstr.eq_constr sigma c c' | _, _ -> false -let make_permutation ?(env = Global.env ()) (sigma : Evd.evar_map) - ((ctx1, pats1, _ as map1) : context_map) ((ctx2, pats2, _ as map2) : context_map) : context_map = +let make_permutation ?(env = Global.env ()) (sigma : Evd.evar_map) map1 map2 : context_map = + let ctx1 = map1.src_ctx in + let pats1 = map1.map_inst in + let ctx2 = map2.src_ctx in + let pats2 = map2.map_inst in let len = List.length ctx1 in let perm = Array.make len None in let merge_rels i1 i2 = @@ -397,7 +411,7 @@ let make_permutation ?(env = Global.env ()) (sigma : Evd.evar_map) let specialize_mapping_constr sigma (m : context_map) c = - specialize_constr sigma (pi2 m) c + specialize_constr sigma m.map_inst c let rels_of_ctx ?(with_lets=true) ctx = let len = List.length ctx in @@ -596,7 +610,7 @@ let new_strengthen (env : Environ.env) (evd : Evd.evar_map) (ctx : rel_context) let id_pats g = List.rev (patvars_of_ctx g) -let id_subst g = (g, id_pats g, g) +let id_subst g = { src_ctx = g; map_inst = id_pats g; tgt_ctx = g } let eq_context_nolet env sigma (g : rel_context) (d : rel_context) = try @@ -627,20 +641,25 @@ let eq_context_nolet env sigma (g : rel_context) (d : rel_context) = (Printexc.to_string e); raise e -let check_eq_context_nolet env sigma (_, _, g as snd) (d, _, _ as fst) = +let check_eq_context_nolet env sigma snd fst = + let g = snd.tgt_ctx in + let d = fst.src_ctx in if eq_context_nolet env sigma g d then () else errorlabstrm (str "Contexts do not agree for composition: " ++ pr_context_map env sigma snd ++ str " and " ++ pr_context_map env sigma fst) -let compose_subst ?(unsafe = false) env ?(sigma=Evd.empty) ((g',p',d') as snd) ((g,p,d) as fst) = +let compose_subst ?(unsafe = false) env ?(sigma=Evd.empty) snd fst = + let { src_ctx = g; map_inst = p; tgt_ctx = d } = fst in + let { src_ctx = g'; map_inst = p'; tgt_ctx = d' } = snd in if !Equations_common.debug && not unsafe then check_eq_context_nolet env sigma snd fst; mk_ctx_map ~unsafe env sigma g' (specialize_pats sigma p' p) d (* (g', (specialize_pats p' p), d) *) -let push_mapping_context sigma decl (g,p,d) = +let push_mapping_context sigma decl subs = + let { src_ctx = g; map_inst = p; tgt_ctx = d } = subs in let decl' = map_rel_declaration (specialize_constr sigma p) decl in - (decl' :: g, (PRel 1 :: List.map (lift_pat 1) p), decl :: d) + { src_ctx = decl' :: g; map_inst = (PRel 1 :: List.map (lift_pat 1) p); tgt_ctx = decl :: d } let lift_subst env evd (ctx : context_map) (g : rel_context) = let map = List.fold_right (fun decl acc -> push_mapping_context evd decl acc) g ctx in @@ -664,7 +683,7 @@ let single_subst ?(unsafe = false) env evd x p g = (* (List.length g) *) in mk_ctx_map ~unsafe env evd substctx pats g else - let (ctx, s, g), invstr = new_strengthen env evd g x t in + let { src_ctx = ctx; map_inst = s; tgt_ctx = g }, invstr = new_strengthen env evd g x t in let x' = match nth s (pred x) with PRel i -> i | _ -> error "Occurs check singleton subst" and t' = specialize_constr evd s t in (* t' is in ctx. Do the substitution of [x'] by [t] now @@ -681,8 +700,8 @@ let is_local_def i ctx = let decl = List.nth ctx (pred i) in Context.Rel.Declaration.is_local_def decl -let filter_def_pats (ctx, pats, _) = +let filter_def_pats map = CList.map_filter (function - | PRel i when is_local_def i ctx -> None - | PHide i when is_local_def i ctx -> None - | p -> Some p) pats + | PRel i when is_local_def i map.src_ctx -> None + | PHide i when is_local_def i map.src_ctx -> None + | p -> Some p) map.map_inst diff --git a/src/context_map.mli b/src/context_map.mli index 3147ae02..d8550806 100644 --- a/src/context_map.mli +++ b/src/context_map.mli @@ -20,8 +20,12 @@ type pat = | PInac of constr | PHide of int -(** Substitutions *) -type context_map = rel_context * pat list * rel_context +(** Substitutions: src_ctx ⊢ map_inst : tgt_ctx *) +type context_map = { + src_ctx : rel_context; + map_inst : pat list; + tgt_ctx : rel_context; +} (** Tag with a Constant.t application (needs env to infer type) *) val mkInac : env -> esigma -> constr -> constr @@ -153,7 +157,7 @@ val new_strengthen : context_map * context_map val id_pats : ('a, 'b,'c) Context.Rel.pt -> pat list -val id_subst : ('a, 'b, 'c) Context.Rel.pt -> ('a, 'b, 'c) Context.Rel.pt * pat list * ('a,'b,'c) Context.Rel.pt +val id_subst : rel_context -> context_map val eq_context_nolet : env -> Evd.evar_map -> rel_context -> rel_context -> bool diff --git a/src/covering.ml b/src/covering.ml index c0bc247a..053cb001 100644 --- a/src/covering.ml +++ b/src/covering.ml @@ -94,16 +94,17 @@ and unify_constrs env evd flex g l l' = | [], [] -> id_subst g | hd :: tl, hd' :: tl' -> (try - let (d,s,_ as hdunif) = unify env evd flex g hd hd' in + let hdunif = unify env evd flex g hd hd' in + let { src_ctx = d; map_inst = s } = hdunif in let specrest = List.map (specialize_constr evd s) in let tl = specrest tl and tl' = specrest tl' in let tlunif = unify_constrs env evd flex d tl tl' in compose_subst env ~sigma:evd tlunif hdunif with Stuck -> let tlunif = unify_constrs env evd flex g tl tl' in - let spec = specialize_constr evd (pi2 tlunif) in + let spec = specialize_constr evd (tlunif.map_inst) in let hd = spec hd and hd' = spec hd' in - let (d, s, _) as hdunif = unify env evd flex (pi1 tlunif) hd hd' in + let hdunif = unify env evd flex (tlunif.src_ctx) hd hd' in compose_subst env ~sigma:evd hdunif tlunif) | _, _ -> raise Conflict @@ -170,9 +171,9 @@ and match_patterns env sigma pl l = open Constrintern -let matches env sigma (p : user_pats) ((phi,p',g') : context_map) = +let matches env sigma (p : user_pats) subst = try - let p' = filter (fun x -> not (hidden x)) (rev p') in + let p' = filter (fun x -> not (hidden x)) (rev subst.map_inst) in UnifSuccess (match_patterns env sigma p p') with Conflict -> UnifFailure | Stuck -> UnifStuck @@ -205,8 +206,8 @@ and match_user_patterns env pl l = | _, _ -> raise Stuck) | _ -> raise Conflict -let matches_user env ((phi,p',g') : context_map) (p : user_pats) = - try UnifSuccess (match_user_patterns env (filter (fun x -> not (hidden x)) (rev p')) p) +let matches_user env subst (p : user_pats) = + try UnifSuccess (match_user_patterns env (filter (fun x -> not (hidden x)) (rev subst.map_inst)) p) with Conflict -> UnifFailure | Stuck -> UnifStuck let refine_arg idx ctx = @@ -512,7 +513,7 @@ let unify_type env evars before id ty after = equations_debug Pp.(fun () -> str"Unification raised Not_found"); None -let blockers env curpats ((_, patcs, _) : context_map) = +let blockers env curpats (subst : context_map) = let rec pattern_blockers p c = match DAst.get p, c with | PUVar (i, _), t -> [] @@ -531,7 +532,7 @@ let blockers env curpats ((_, patcs, _) : context_map) = (pattern_blockers hd hd') @ (patterns_blockers tl tl') | _ -> [] - in patterns_blockers curpats (rev patcs) + in patterns_blockers curpats (rev subst.map_inst) let subst_matches_constr sigma k s c = let rec aux depth c = @@ -560,7 +561,8 @@ let split_var (env,evars) var delta = let branch = function | UnifFailure -> None | UnifStuck -> assert false - | UnifSuccess ((ctx',s,ctx), ctxlen, cstr, cstrpat) -> + | UnifSuccess (map, ctxlen, cstr, cstrpat) -> + let { src_ctx = ctx'; map_inst = s; tgt_ctx = ctx } = map in (* ctx' |- s : before ; ctxc *) (* ctx' |- cpat : ty *) if !debug then Feedback.msg_debug Pp.(str"cpat: " ++ pr_pat env !evars cstrpat); @@ -569,7 +571,8 @@ let split_var (env,evars) var delta = (* ctx' |- spat : before ; id *) let spat = let ctxcsubst, beforesubst = List.chop ctxlen s in - check_ctx_map env !evars (ctx', cpat :: beforesubst, decl :: before) + let map = { src_ctx = ctx'; map_inst = cpat :: beforesubst; tgt_ctx = decl :: before } in + check_ctx_map env !evars map in (* ctx' ; after |- safter : before ; id ; after = delta *) Some (lift_subst env !evars spat after) @@ -666,7 +669,7 @@ let split_at_eos env sigma ctx = List.split_when (fun decl -> is_lglobal env sigma coq_end_of_section (get_named_type decl)) ctx -let pr_problem p env sigma (delta, patcs, _) = +let pr_problem p env sigma { src_ctx = delta; map_inst = patcs }= let env' = push_rel_context delta env in let ctx = pr_context env sigma delta in Id.print p.program_id ++ str" " ++ pr_pats env' sigma patcs ++ @@ -838,10 +841,10 @@ let pats_of_sign sign = List.rev_map (fun decl -> DAst.make (PUVar (Name.get_id (Context.Rel.Declaration.get_name decl), Implicit))) sign -let abstract_term_in_context env evars idx t (g, p, d) = - let before, after = CList.chop (pred idx) g in +let abstract_term_in_context env evars idx t map = + let before, after = CList.chop (pred idx) map.src_ctx in let before' = subst_term_in_context evars (lift (- pred idx) t) before in - (before' @ after, p, d) + { src_ctx = before' @ after; map_inst = map.map_inst; tgt_ctx = map.tgt_ctx } let wf_fix_constr env evars sign arity sort carrier cterm crel = let sigma, tele, telety = Sigma_types.telescope_of_context env !evars sign in @@ -999,7 +1002,7 @@ let compute_rec_data env evars data lets subst p = let rec_sign = p.program_sign @ lets in let lhs = decl :: rec_sign in let pats = PHide 1 :: lift_pats 1 (id_pats rec_sign) in - let rec_prob = (lhs, pats, lhs) in + let rec_prob = { src_ctx = lhs; map_inst = pats; tgt_ctx = lhs } in let rec_node = { wf_rec_term = fix; wf_rec_functional = None; @@ -1022,7 +1025,8 @@ let compute_rec_data env evars data lets subst p = exception UnfaithfulSplit of (Loc.t option * Pp.t) -let rename_domain env sigma bindings (ctx, p, ctx') = +let rename_domain env sigma bindings map = + let { src_ctx = ctx; map_inst = p; tgt_ctx = ctx' } = map in let fn rel decl = match Int.Map.find rel bindings with | exception Not_found -> decl @@ -1051,7 +1055,8 @@ let loc_before loc loc' = end_ < end' || (end_ = end' && start <= start') let rec covering_aux env evars p data prev (clauses : (pre_clause * (int * int)) list) path - (ctx,pats,ctx' as prob) extpats lets ty = + prob extpats lets ty = + let { src_ctx = ctx; map_inst = pats; tgt_ctx = ctx' } = prob in if !Equations_common.debug then Feedback.msg_debug Pp.(str"Launching covering on "++ pr_preclauses env !evars (List.map fst clauses) ++ str " with problem " ++ pr_problem p env !evars prob ++ @@ -1076,7 +1081,7 @@ let rec covering_aux env evars p data prev (clauses : (pre_clause * (int * int)) else Id.Map.add x (loc, gen, pat) acc else if data.flags.allow_aliases then acc else - let env = push_rel_context (pi1 prob) env in + let env = push_rel_context prob.src_ctx env in let loc, pat, pat' = if loc_before loc loc' then loc', pat, pat' else loc, pat', pat @@ -1155,7 +1160,7 @@ let rec covering_aux env evars p data prev (clauses : (pre_clause * (int * int)) (str "This pattern cannot be empty, it matches value " ++ fnl () ++ pr_pat env !evars c)) | PRel i -> - match prove_empty (env,evars) (pi1 prob) i with + match prove_empty (env,evars) prob.src_ctx i with | Some (i, ctx, s) -> Some (List.rev prev @ ((Pre_clause (loc, lhs, rhs),(idx, cnt+1)) :: clauses'), Compute (prob, [], ty, REmpty (i, s))) @@ -1185,26 +1190,26 @@ let rec covering_aux env evars p data prev (clauses : (pre_clause * (int * int)) let blocks = blockers env (extpats @ lhs) prob in equations_debug (fun () -> str "blockers are: " ++ - prlist_with_sep spc (pr_rel_name (push_rel_context (pi1 prob) env)) blocks); + prlist_with_sep spc (pr_rel_name (push_rel_context prob.src_ctx env)) blocks); let rec try_split acc vars = match vars with | [] -> None | var :: vars -> equations_debug (fun () -> str "trying next blocker " ++ - pr_rel_name (push_rel_context (pi1 prob) env) var); - match split_var (env,evars) var (pi1 prob) with + pr_rel_name (push_rel_context prob.src_ctx env) var); + match split_var (env,evars) var prob.src_ctx with | Some (Splitted (var, newctx, s)) -> equations_debug (fun () -> str "splitting succeded for " ++ - pr_rel_name (push_rel_context (pi1 prob) env) var); - let prob' = (newctx, pats, ctx') in + pr_rel_name (push_rel_context prob.src_ctx env) var); + let prob' = { src_ctx = newctx; map_inst = pats; tgt_ctx = ctx' } in let coverrec clauses s = covering_aux env evars p data [] clauses path (compose_subst env ~sigma:!evars s prob') extpats - (specialize_rel_context !evars (pi2 s) lets) - (specialize_constr !evars (pi2 s) ty) + (specialize_rel_context !evars s.map_inst lets) + (specialize_constr !evars s.map_inst ty) in (try let rec_call clauses x = @@ -1232,7 +1237,7 @@ let rec covering_aux env evars p data prev (clauses : (pre_clause * (int * int)) | Some (CannotSplit _) as x -> equations_debug (fun () -> str "splitting failed for " ++ - pr_rel_name (push_rel_context (pi1 prob) env) var); + pr_rel_name (push_rel_context prob.src_ctx env) var); let acc = match acc with | None -> x | _ -> acc @@ -1251,7 +1256,7 @@ let rec covering_aux env evars p data prev (clauses : (pre_clause * (int * int)) | None -> None)) | [] -> (* Every clause failed for the problem, it's either uninhabited or the clauses are not exhaustive *) - match find_empty (env,evars) (pi1 prob) with + match find_empty (env,evars) prob.src_ctx with | Some (i, ctx, s) -> Some (List.rev prev @ clauses, (* Split (prob, i, ty, s)) *) Compute (prob, [], ty, REmpty (i, s))) @@ -1260,9 +1265,10 @@ let rec covering_aux env evars p data prev (clauses : (pre_clause * (int * int)) (str "Non-exhaustive pattern-matching, no clause found for:" ++ fnl () ++ pr_problem p env !evars prob)) -and interp_clause env evars p data prev clauses' path (ctx,pats,ctx' as prob) +and interp_clause env evars p data prev clauses' path prob extpats lets ty ((loc,lhs,rhs), used) (s, uinnacs, innacs) = + let { src_ctx = ctx; map_inst = pats; tgt_ctx = ctx' } = prob in let env' = push_rel_context_eos ctx env evars in let get_var loc i s = match assoc i s with @@ -1333,7 +1339,7 @@ and interp_clause env evars p data prev clauses' path (ctx,pats,ctx' as prob) Some res | Empty (loc,i) -> - (match prove_empty (env, evars) (pi1 prob) (get_var loc i s) with + (match prove_empty (env, evars) prob.src_ctx (get_var loc i s) with | None -> user_err_loc (loc, str"Cannot show that " ++ Id.print i ++ str"'s type is empty") | Some (i, ctx, s) -> Some (Compute (prob, [], ty, REmpty (i, s)))) @@ -1352,7 +1358,7 @@ and interp_clause env evars p data prev clauses' path (ctx,pats,ctx' as prob) let newctx, pats', pats'' = instance_of_pats env !evars ctx vars in (* revctx is a variable substitution from a reordered context to the current context *) - let revctx = check_ctx_map env !evars (newctx, pats', ctx) in + let revctx = check_ctx_map env !evars { src_ctx = newctx; map_inst = pats'; tgt_ctx = ctx } in let idref = Namegen.next_ident_away (Id.of_string "refine") (Id.Set.of_list (ids_of_rel_context newctx)) in let refterm (* in newctx *) = mapping_constr !evars revctx cconstr in let refty = mapping_constr !evars revctx cty in @@ -1384,40 +1390,42 @@ and interp_clause env evars p data prev clauses' path (ctx,pats,ctx' as prob) let refterm (* in extnewctx *) = lift 1 refterm in equations_debug Pp.(fun () -> str" Strenghtening variable decl: " ++ pr_context_map env !evars tytop); equations_debug Pp.(fun () -> str" Strenghtening variable decl inv: " ++ pr_context_map env !evars tytopinv); - let cmap, strinv = new_strengthen env !evars (pi1 tytop) 1 refterm in + let cmap, strinv = new_strengthen env !evars tytop.src_ctx 1 refterm in let cmap = compose_subst env ~sigma:!evars cmap tytop in let strinv = compose_subst env ~sigma:!evars tytopinv strinv in - let strinv_map = List.map_i (fun i -> function (PRel j) -> i, j | _ -> assert false) 1 (pi2 strinv) in + let strinv_map = List.map_i (fun i -> function (PRel j) -> i, j | _ -> assert false) 1 strinv.map_inst in equations_debug Pp.(fun () -> str" Strenghtening: " ++ pr_context_map env !evars cmap); equations_debug Pp.(fun () -> str" Strenghtening inverse: " ++ pr_context_map env !evars strinv); - let idx_of_refined = destPRel (CList.hd (pi2 cmap)) in + let idx_of_refined = destPRel (CList.hd cmap.map_inst) in equations_debug Pp.(fun () -> str" idx_of_refined: " ++ int idx_of_refined); let cmap = abstract_term_in_context env !evars idx_of_refined (mapping_constr !evars cmap refterm) cmap in equations_debug Pp.(fun () -> str" Strenghtening + abstraction: " ++ pr_context_map env !evars cmap); let newprob_to_lhs = - let inst_refctx = set_in_ctx idx_of_refined (mapping_constr !evars cmap refterm) (pi1 cmap) in - let str_to_new = - inst_refctx, (specialize_pats !evars (pi2 cmap) (lift_pats 1 pats')), newctx - in + let inst_refctx = set_in_ctx idx_of_refined (mapping_constr !evars cmap refterm) cmap.src_ctx in + let str_to_new = { + src_ctx = inst_refctx; + map_inst = specialize_pats !evars cmap.map_inst (lift_pats 1 pats'); + tgt_ctx = newctx; + } in equations_debug Pp.(fun () -> str" Strenghtening + abstraction + instantiation: " ++ pr_context_map env !evars str_to_new); compose_subst env ~sigma:!evars str_to_new revctx in equations_debug Pp.(fun () -> str" Strenghtening + abstraction + instantiation: " ++ pr_context_map env !evars newprob_to_lhs); let newprob = - let ctx = pi1 cmap in + let ctx = cmap.src_ctx in let pats = rev_map (fun c -> let idx = destRel !evars c in (* find out if idx in ctx should be hidden depending on its use in newprob_to_lhs *) if List.exists (function PHide idx' -> idx == idx' | _ -> false) - (pi2 newprob_to_lhs) then + newprob_to_lhs.map_inst then PHide idx else PRel idx) (rels_of_ctx ctx) in - (ctx, pats, ctx) + { src_ctx = ctx; map_inst = pats; tgt_ctx = ctx } in let newty = let env' = push_rel_context extnewctx env in @@ -1490,7 +1498,7 @@ and interp_clause env evars p data prev clauses' path (ctx,pats,ctx' as prob) let strength_app = List.map_filter (fun t -> if isRel !evars t then let i = destRel !evars t in - let decl = List.nth (pi1 prob) (pred i) in + let decl = List.nth prob.src_ctx (pred i) in if Context.Rel.Declaration.is_local_def decl then None else Some t else Some t) strength_app @@ -1501,7 +1509,7 @@ and interp_clause env evars p data prev clauses' path (ctx,pats,ctx' as prob) let _, ctxs, _ = lets_of_ctx env ctx evars s in let newlets = (lift_rel_context (succ letslen) ctxs) @ (lift_rel_context 1 lets) - in specialize_rel_context !evars (pi2 cmap) newlets + in specialize_rel_context !evars cmap.map_inst newlets in let clauses' = List.mapi (fun i x -> x, (succ i, 0)) cls' in match covering_aux env evars p data [] clauses' path' newprob [] lets' newty with @@ -1516,7 +1524,7 @@ and interp_clause env evars p data prev clauses' path (ctx,pats,ctx' as prob) let info = { refined_obj = (idref, cconstr, cty); refined_rettyp = ty; - refined_arg = refine_arg idx_of_refined (pi1 cmap); + refined_arg = refine_arg idx_of_refined cmap.src_ctx; refined_path = path'; refined_term = term; refined_filter = None; diff --git a/src/covering.mli b/src/covering.mli index 74ca721e..77e8a8e3 100644 --- a/src/covering.mli +++ b/src/covering.mli @@ -154,7 +154,7 @@ val split_at_eos : Environ.env -> Evd.evar_map -> named_context -> named_context * named_context val pr_problem : program_info -> - env -> Evd.evar_map -> rel_context * pat list * 'c -> Pp.t + env -> Evd.evar_map -> context_map -> Pp.t val rel_id : (Name.t * 'a * 'b) list -> int -> Id.t val push_named_context : named_context -> env -> env diff --git a/src/principles.ml b/src/principles.ml index a6660304..460e0b16 100644 --- a/src/principles.ml +++ b/src/principles.ml @@ -46,7 +46,6 @@ let nested = function Nested _ -> true | _ -> false let pi1 (x,_,_) = x let pi2 (_,y,_) = y -let pi3 (_,_,z) = z (** Objects to keep information about equations *) @@ -619,8 +618,10 @@ let arguments sigma c = snd (decompose_app sigma c) let unfold_constr sigma c = Tactics.unfold_in_concl [(Locus.OnlyOccurrences [1], Evaluable.EvalConstRef (fst (destConst sigma c)))] -let extend_prob_ctx delta (ctx, pats, ctx') = - (delta @ ctx, Context_map.lift_pats (List.length delta) pats, ctx') +let extend_prob_ctx delta map = + { src_ctx = delta @ map.src_ctx; + map_inst = Context_map.lift_pats (List.length delta) map.map_inst; + tgt_ctx = map.tgt_ctx } let map_proto evd recarg f ty = match recarg with @@ -648,24 +649,27 @@ let cut_problem evd s ctx = and s : prec -> Γ |- t : rec build Γ |- ps, ps' : Δ, Δ'[prec/rec] *) - let rec fn s (ctxl, pats, ctxr as ctxm) = + let rec fn s ctxm = match s with | [] -> ctxm | (id, (recarg, term)) :: s -> try + let { src_ctx = ctxl; map_inst = pats; tgt_ctx = ctxr } = ctxm in let rel, _, ty = Termops.lookup_rel_id id ctxr in let fK = map_proto evd recarg term (lift rel ty) in let ctxr' = subst_in_ctx rel fK ctxr in let left, right = CList.chop (pred rel) pats in let right' = List.tl right in let s' = List.map (fun (id, (recarg, t)) -> id, (recarg, substnl [fK] rel t)) s in - fn s' (ctxl, List.append left right', ctxr') + fn s' { src_ctx = ctxl; map_inst = List.append left right'; tgt_ctx = ctxr' } with Not_found -> fn s ctxm in fn s (id_subst ctx) -let subst_rec env evd cutprob s (ctx, p, _ as lhs) = +let subst_rec env evd cutprob s lhs = + let ctx = lhs.src_ctx in let subst = - List.fold_left (fun (ctx, pats, ctx' as lhs') (id, (recarg, b)) -> + List.fold_left (fun lhs' (id, (recarg, b)) -> + let ctx = lhs'.src_ctx in try let rel, _, ty = Termops.lookup_rel_id id ctx in (* Feedback.msg_debug Pp.(str"lhs': " ++ pr_context_map env evd lhs'); *) let fK = map_proto evd recarg (mapping_constr evd lhs b) (lift rel ty) in @@ -754,11 +758,13 @@ let _program_fixdecls p fixdecls = not (Id.equal id p.program_id)) fixdecls | _ -> fixdecls -let push_mapping_context env sigma decl ((g,p,d), cut) = +let push_mapping_context env sigma decl (map, cut) = let open Context.Rel.Declaration in let decl' = map_rel_declaration (mapping_constr sigma cut) decl in let declassum = LocalAssum (get_annot decl, get_type decl) in - (decl :: g, (PRel 1 :: List.map (lift_pat 1) p), decl' :: d), + { src_ctx = decl :: map.src_ctx; + map_inst = PRel 1 :: List.map (lift_pat 1) map.map_inst; + tgt_ctx = decl' :: map.tgt_ctx }, lift_subst env sigma cut [declassum] (** Assumes the declaration already live in \Gamma to produce \Gamma, decls |- ps : \Delta, decls *) @@ -782,7 +788,7 @@ let subst_rec_programs env evd ps = let recarg = match r with | Structural _ -> None | WellFounded _ -> Some (Context.Rel.nhyps p.program_info.program_sign - ctxlen) in - let oterm = lift (List.length (pi1 p.program_prob) - ctxlen) oterm in + let oterm = lift (List.length p.program_prob.src_ctx - ctxlen) oterm in Some (p.program_info.program_id, (recarg, oterm)) | None -> None in @@ -810,26 +816,27 @@ let subst_rec_programs env evd ps = let program_info' = { prog_info with program_rec = None; - program_sign = pi1 cutprob_subst; + program_sign = cutprob_subst.src_ctx; program_arity = mapping_constr !evd cutprob_subst prog_info.program_arity } in let program' = { p with program_info = program_info' } in let path' = p.program_info.program_id :: path in (* Feedback.msg_debug Pp.(str"In subst_programs, cut_problem s'" ++ pr_context env !evd (pi1 rec_prob)); *) - let rec_cutprob = cut_problem s' (pi1 rec_prob) in + let rec_cutprob = cut_problem s' rec_prob.src_ctx in let splitting' = aux rec_cutprob s' program' oterm path' p.program_splitting in let term', ty' = term_of_tree env evd (ESorts.make prog_info.program_sort) splitting' in { program_rec = None; program_info = program_info'; - program_prob = id_subst (pi3 cutprob_sign); + program_prob = id_subst cutprob_sign.tgt_ctx; program_term = term'; program_splitting = splitting' } in List.map2 one_program progs oterms and aux cutprob s p f path = function - | Compute ((ctx,pats,del as lhs), where, ty, c) -> + | Compute (lhs, where, ty, c) -> + let ctx = lhs.src_ctx in let subst, lhs' = subst_rec cutprob s lhs in let lhss = map_fix_subst !evd lhs s in let progctx = (extend_prob_ctx (where_context where) lhs) in @@ -840,7 +847,7 @@ let subst_rec_programs env evd ps = where_type} as w) (subst_wheres, wheres) = (* subst_wheres lives in lhs', i.e. has prototypes substituted already *) let wcontext = where_context subst_wheres in - let cutprob' = cut_problem s (pi3 subst) in + let cutprob' = cut_problem s subst.tgt_ctx in (* Feedback.msg_debug Pp.(str"where_context in subst rec : " ++ pr_context env !evd wcontext); * Feedback.msg_debug Pp.(str"lifting subst : " ++ pr_context_map env !evd subst); * Feedback.msg_debug Pp.(str"cutprob : " ++ pr_context_map env !evd cutprob'); *) @@ -853,7 +860,7 @@ let subst_rec_programs env evd ps = preceding ones. *) let s = List.map (fun (id, (recarg, b)) -> (id, (recarg, lift ((* List.length subst_wheres + *) - List.length (pi1 wp.program_prob) - List.length ctx) b))) lhss in + List.length wp.program_prob.src_ctx - List.length ctx) b))) lhss in let wp' = match subst_programs path s ctxlen [wp] [where_term w] with | [wp'] -> wp' @@ -868,7 +875,7 @@ let subst_rec_programs env evd ps = where_map := PathMap.add where_path (applistc where_program_term where_program_args (* substituted *), id, wp'.program_splitting) !where_map; - let where_program_args = extended_rel_list 0 (pi1 lhs') in + let where_program_args = extended_rel_list 0 lhs'.src_ctx in wp', where_program_args else let where_program_term = mapping_constr !evd wsubst0 wp.program_term in @@ -885,7 +892,7 @@ let subst_rec_programs env evd ps = where_program_args = args'; where_path; where_orig; - where_context_length = List.length (pi1 lhs'); + where_context_length = List.length lhs'.src_ctx; where_type } in (subst_where :: subst_wheres, w :: wheres) in @@ -917,21 +924,21 @@ let subst_rec_programs env evd ps = (* Feedback.msg_debug Pp.(str"newprob subst: " ++ prsubst env evd newprobs); Feedback.msg_debug Pp.(str"Newprob to lhs: " ++ pr_context_map env !evd info.refined_newprob_to_lhs); Feedback.msg_debug Pp.(str"Newprob : " ++ pr_context_map env !evd newprob); *) - let cutnewprob = cut_problem newprobs (pi3 newprob) in + let cutnewprob = cut_problem newprobs newprob.tgt_ctx in (* Feedback.msg_debug Pp.(str"cutnewprob : " ++ pr_context_map env !evd cutnewprob); *) let subst', newprob' = subst_rec cutnewprob newprobs newprob in (* Feedback.msg_debug Pp.(str"subst' : " ++ pr_context_map env !evd subst'); *) let subst, lhs' = subst_rec cutprob s lhs in (* Feedback.msg_debug Pp.(str"subst = " ++ pr_context_map env !evd subst); *) - let _, revctx' = subst_rec (cut_problem s (pi3 revctx)) lhss revctx in + let _, revctx' = subst_rec (cut_problem s revctx.tgt_ctx) lhss revctx in let _, newprob_to_prob' = - subst_rec (cut_problem lhss (pi3 info.refined_newprob_to_lhs)) lhss info.refined_newprob_to_lhs in + subst_rec (cut_problem lhss info.refined_newprob_to_lhs.tgt_ctx) lhss info.refined_newprob_to_lhs in let islogical = List.exists (fun (id, (recarg, f)) -> Option.has_some recarg) s in let path' = info.refined_path in let s' = aux cutnewprob newprobs p f path' sp in let count_lets len = let open Context.Rel.Declaration in - let ctx' = pi1 newprob' in + let ctx' = newprob'.src_ctx in let rec aux ctx len = if len = 0 then 0 else @@ -955,20 +962,20 @@ let subst_rec_programs env evd ps = (let len = List.length acc in refarg := (count_lets len, len)); if isRel !evd c then - let d = List.nth (pi1 lhs) (pred (destRel !evd c)) in + let d = List.nth lhs.src_ctx (pred (destRel !evd c)) in if List.mem_assoc (Nameops.Name.get_id (get_name d)) s then acc, filter else mapping_constr !evd subst c :: acc, i :: filter else mapping_constr !evd subst c :: acc, i :: filter) 0 ([], []) args in let args' = List.rev_map (Reductionops.nf_beta env !evd) args' in - equations_debug Pp.(fun () -> str"Chopped args: " ++ prlist_with_sep spc (Printer.pr_econstr_env (push_rel_context (pi1 subst) env) !evd) args'); + equations_debug Pp.(fun () -> str"Chopped args: " ++ prlist_with_sep spc (Printer.pr_econstr_env (push_rel_context subst.src_ctx env) !evd) args'); let term', args', arg', filter = if islogical then refhead, args', !refarg, None else - (let sigma, refargs = constrs_of_pats ~inacc_and_hide:false env !evd (pi2 subst') in - let refterm = it_mkLambda_or_LetIn (applistc refhead (List.rev refargs)) (pi1 subst') in + (let sigma, refargs = constrs_of_pats ~inacc_and_hide:false env !evd subst'.map_inst in + let refterm = it_mkLambda_or_LetIn (applistc refhead (List.rev refargs)) subst'.src_ctx in equations_debug Pp.(fun () -> str"refterm: " ++ (Printer.pr_econstr_env env !evd refterm)); let refarg = (fst arg - List.length s, snd arg - List.length s) in @@ -1088,9 +1095,10 @@ let _remove_let_pats sigma subst patsubst pats = in List.fold_right remove_let pats [] -let smash_ctx_map env sigma (l, p, r as m) = +let smash_ctx_map env sigma m = + let r = m.tgt_ctx in let subst, patsubst, r' = smash_rel_context sigma r in - let smashr' = (r, patsubst, r') in + let smashr' = { src_ctx = r; map_inst = patsubst; tgt_ctx = r' } in compose_subst env ~sigma m smashr', subst let pattern_instance ctxmap = @@ -1160,7 +1168,7 @@ let computations env evd alias refine p eqninfo : computation list = subterm, filter in let where_comp = - (termf, alias, w.where_orig, pi1 wsmash, (* substl smashsubst *) arity, + (termf, alias, w.where_orig, wsmash.src_ctx, (* substl smashsubst *) arity, pattern_instance wsmash, None (* no refinement *), comps) in (lhsterm :: wheres, where_comp :: where_comps) in @@ -1168,7 +1176,7 @@ let computations env evd alias refine p eqninfo : computation list = let ctx = compose_subst env ~sigma:evd lhs prob in if !Equations_common.debug then Feedback.msg_debug Pp.(str"where_instance: " ++ prlist_with_sep spc (Printer.pr_econstr_env env evd) inst); - let envlhs = (push_rel_context (pi1 lhs) env) in + let envlhs = (push_rel_context lhs.src_ctx env) in let envwhere = push_rel_context (where_context where) envlhs in let fn c = (* Feedback.msg_debug Pp.(str"substituting in c= " ++ Printer.pr_econstr_env envwhere evd c); *) @@ -1182,7 +1190,7 @@ let computations env evd alias refine p eqninfo : computation list = Feedback.msg_debug Pp.(str"substituted: " ++ pr_splitting_rhs ~verbose:true envlhs envlhs evd lhs c' ty)); let patsconstrs = pattern_instance ctx in let ty = substl inst ty in - [Computation (pi1 ctx, f, alias, patsconstrs, ty, + [Computation (ctx.src_ctx, f, alias, patsconstrs, ty, f, (Where, snd refine), c', Some wheres)] | Split (_, _, _, cs) -> @@ -1198,7 +1206,7 @@ let computations env evd alias refine p eqninfo : computation list = | Refined (lhs, info, cs) -> let (id, c, t) = info.refined_obj in - let (ctx', pats', _ as s) = compose_subst env ~sigma:evd lhs prob in + let s = compose_subst env ~sigma:evd lhs prob in let patsconstrs = pattern_instance s in let refineds = compose_subst env ~sigma:evd info.refined_newprob_to_lhs s in let refinedpats = pattern_instance refineds in @@ -1210,9 +1218,9 @@ let computations env evd alias refine p eqninfo : computation list = (push_rel_context (pi1 lhs) env) evd info.refined_term); Feedback.msg_debug Pp.(str"At refine node, program term: " ++ Printer.pr_econstr_env (push_rel_context (pi1 lhs) env) evd progterm); *) - [Computation (pi1 lhs, f, alias, patsconstrs, info.refined_rettyp, f, (Refine, true), + [Computation (lhs.src_ctx, f, alias, patsconstrs, info.refined_rettyp, f, (Refine, true), RProgram progterm, - Some [(info.refined_term, filter), None, info.refined_path, pi1 info.refined_newprob, + Some [(info.refined_term, filter), None, info.refined_path, info.refined_newprob.src_ctx, info.refined_newty, refinedpats, Some (mapping_constr evd info.refined_newprob_to_lhs c, info.refined_arg), computations env info.refined_newprob (lift 1 info.refined_term) None fsubst (Regular, true) cs])] @@ -1466,7 +1474,7 @@ let all_computations env evd alias progs = let pi = p.program_info in let topcomp = (((eqninfo.equations_f,[]), alias, [pi.program_id], pi.program_sign, pi.program_arity, - List.rev_map pat_constr (pi2 eqninfo.equations_prob), None, + List.rev_map pat_constr eqninfo.equations_prob.map_inst, None, (kind_of_prog pi,false)), top) in topcomp :: (rest @ acc) in diff --git a/src/principles.mli b/src/principles.mli index e21aadc1..5359a3df 100644 --- a/src/principles.mli +++ b/src/principles.mli @@ -87,9 +87,7 @@ type rec_subst = (Names.Id.t * (int option * EConstr.constr)) list val cut_problem : Evd.evar_map -> rec_subst -> - Equations_common.rel_declaration list -> - Equations_common.rel_declaration list * Context_map.pat list * - Equations_common.rel_declaration list + Equations_common.rel_declaration list -> Context_map.context_map val map_proto : Evd.evar_map -> int option -> EConstr.t -> EConstr.t -> EConstr.t @@ -97,8 +95,7 @@ val map_proto : Evd.evar_map -> int option -> EConstr.t -> EConstr.t -> EConstr. val subst_rec : Environ.env -> Evd.evar_map -> Context_map.context_map -> rec_subst -> - Equations_common.rel_context * Context_map.pat list * - Equations_common.rel_context -> + Context_map.context_map -> Context_map.context_map * Context_map.context_map val subst_rec_programs : diff --git a/src/principles_proofs.ml b/src/principles_proofs.ml index ea829b2c..6239a4f3 100644 --- a/src/principles_proofs.ml +++ b/src/principles_proofs.ml @@ -438,7 +438,7 @@ let aux_ind_fun info chop nested unfp unfids p = (tclTHEN intros (aux chop unfs unfids cs)))] and aux chop unfs unfids = function - | Split ((ctx,pats,_ as lhs), var, _, splits) -> + | Split (lhs, var, _, splits) -> let splits = List.map_filter (fun x -> x) (Array.to_list splits) in let unfs_splits = let unfs = map_opt_split destSplit unfs in @@ -470,7 +470,7 @@ let aux_ind_fun info chop nested unfp unfids p = let unfsplit = Option.map (fun s -> nth s (pred i)) unfs_splits in aux chop unfsplit unfids split)))) - | Refined ((ctx, _, _), refinfo, s) -> + | Refined (lhs, refinfo, s) -> let unfs = map_opt_split destRefined unfs in let id = pi1 refinfo.refined_obj in let elimtac gl = @@ -507,12 +507,13 @@ let aux_ind_fun info chop nested unfp unfids p = (tclSOLVE [Proofview.Goal.enter elimtac]); (solve_ind_rec_tac info.term_info)])) - | Compute ((lctx,_,_), wheres, _, c) -> + | Compute (lhs, wheres, _, c) -> + let lctx = lhs.src_ctx in let unfctx, unfswheres = let unfs = map_opt_split destWheres unfs in match unfs with | None -> [], List.map (fun _ -> None) wheres - | Some (unfctx, wheres) -> pi1 unfctx, List.map (fun w -> Some w) wheres + | Some (unfctx, wheres) -> unfctx.src_ctx, List.map (fun w -> Some w) wheres in let wheretac = if not (List.is_empty wheres) then @@ -935,7 +936,8 @@ type reckind = let compute_unfold_trace env sigma where_map split unfold_split = let rec aux split unfold_split = match split, unfold_split with - | Split (_, _, _, splits), Split ((ctx,pats,_), var, _, unfsplits) -> + | Split (_, _, _, splits), Split (lhs, var, _, unfsplits) -> + let ctx = lhs.src_ctx in if is_primitive env sigma ctx (pred var) then aux (Option.get (Array.hd splits)) (Option.get (Array.hd unfsplits)) else @@ -944,9 +946,9 @@ let compute_unfold_trace env sigma where_map split unfold_split = let trace = List.map2 (fun split unfsplit -> aux split unfsplit) splits unfsplits in UnfSplit trace | _, Mapping (lhs, s) -> aux split s - | Refined (_, _, s), Refined ((ctx, _, _), refinfo, unfs) -> + | Refined (_, _, s), Refined (lhs, refinfo, unfs) -> UnfRefined (refinfo, aux s unfs) - | Compute (_, wheres, _, RProgram _), Compute ((lctx, _, _), unfwheres, _, RProgram _) -> + | Compute (_, wheres, _, RProgram _), Compute (lhs, unfwheres, _, RProgram _) -> let () = assert (List.length wheres = List.length unfwheres) in let map w unfw = let assoc, id, _ = @@ -958,9 +960,9 @@ let compute_unfold_trace env sigma where_map split unfold_split = (wp, unfwp, assoc, id) in let data = List.map2 map wheres unfwheres in - UnfComputeProgram (data, lctx) - | Compute (_, _, _, _), Compute ((ctx,_,_), _, _, REmpty (id, sp)) -> - let d = nth ctx (pred id) in + UnfComputeProgram (data, lhs.src_ctx) + | Compute (_, _, _, _), Compute (lhs, _, _, REmpty (id, sp)) -> + let d = nth lhs.src_ctx (pred id) in let id = Name.get_id (get_name d) in UnfComputeEmpty id | _, _ -> assert false diff --git a/src/sigma_types.ml b/src/sigma_types.ml index 8221c2db..326155a0 100644 --- a/src/sigma_types.ml +++ b/src/sigma_types.ml @@ -616,9 +616,10 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref) let subst = Context_map.id_subst (arity_ctx @ ctx) in let rev_subst = Context_map.id_subst (arity_ctx @ ctx) in let subst, rev_subst = List.fold_left ( - fun ((ctx, _, _) as subst, rev_subst) -> function + fun (subst, rev_subst) -> function | None -> subst, rev_subst | Some rel -> + let ctx = subst.Context_map.src_ctx in let fresh_rel = Context_map.mapping_constr !evd subst (EConstr.mkRel 1) in let target_rel = EConstr.mkRel (rel + oib.mind_nrealargs + 1) in let target_rel = Context_map.mapping_constr !evd subst target_rel in @@ -632,8 +633,8 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref) (Context_map.mapping_constr !evd subst (EConstr.mkRel 1))) in (* [ctx'] is the context under which we will build the case in a first step. *) (* This is [ctx] where everything omitted and cut is removed. *) - let ctx' = List.skipn (nb_cuts_omit + oib.mind_nrealargs + 1) (pi3 rev_subst) in - let rev_subst' = List.skipn (nb_cuts_omit + oib.mind_nrealargs + 1) (pi2 rev_subst) in + let ctx' = List.skipn (nb_cuts_omit + oib.mind_nrealargs + 1) (rev_subst.Context_map.tgt_ctx) in + let rev_subst' = List.skipn (nb_cuts_omit + oib.mind_nrealargs + 1) (rev_subst.Context_map.map_inst) in let rev_subst' = Context_map.lift_pats (-(oib.mind_nrealargs+1)) rev_subst' in let rev_subst_without_cuts = Context_map.mk_ctx_map env !evd ctx rev_subst' ctx' in (* Now we will work under a context with [ctx'] as a prefix, so we will be @@ -641,10 +642,12 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref) (* ===== SUBSTITUTION ===== *) let subst = CList.fold_right_i ( - fun i omit ((ctx, pats, _) as subst)-> + fun i omit subst -> match omit with | None -> subst | Some rel -> + let ctx = subst.Context_map.src_ctx in + let pats = subst.Context_map.map_inst in let orig = oib.mind_nrealargs + 1 - i in let fresh_rel = Context_map.specialize !evd pats (Context_map.PRel orig) in let target_rel = EConstr.mkRel (rel + oib.mind_nrealargs + 1) in @@ -663,7 +666,7 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref) (* Also useful: a substitution from [ctx] to the context with cuts. *) let subst_to_cuts = let lift_subst = Context_map.mk_ctx_map env !evd (arity_ctx @ ctx) - (Context_map.lift_pats (oib.mind_nrealargs + 1) (pi2 (Context_map.id_subst ctx))) + (Context_map.lift_pats (oib.mind_nrealargs + 1) (Context_map.id_pats ctx)) ctx in Context_map.compose_subst ~unsafe:true env ~sigma:!evd subst lift_subst in @@ -672,7 +675,7 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref) let goal = Context_map.mapping_constr !evd subst_to_cuts goal in (* ===== CUTS ===== *) - let cuts_ctx, remaining = List.chop nb_cuts (pi1 subst) in + let cuts_ctx, remaining = List.chop nb_cuts (subst.Context_map.src_ctx) in let fresh_ctx = List.firstn (oib.mind_nrealargs + 1) remaining in let revert_cut x = let rec revert_cut i = function @@ -682,7 +685,7 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref) | Context.Rel.Declaration.LocalAssum _ -> Some (EConstr.mkRel i) | Context.Rel.Declaration.LocalDef _ -> None) | _ :: l -> revert_cut (succ i) l - in revert_cut (- oib.mind_nrealargs) (pi2 subst) + in revert_cut (- oib.mind_nrealargs) (subst.Context_map.map_inst) in let rev_cut_vars = CList.map revert_cut (CList.init nb_cuts (fun i -> succ i)) in let cut_vars = List.rev rev_cut_vars in @@ -692,7 +695,7 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref) let goal, to_apply, simpl = if Int.equal nb 0 then goal, [], false else - let arity_ctx' = Context_map.specialize_rel_context !evd (pi2 subst_to_cuts) arity_ctx in + let arity_ctx' = Context_map.specialize_rel_context !evd (subst_to_cuts.Context_map.map_inst) arity_ctx in let rev_indices' = List.map (Context_map.mapping_constr !evd subst_to_cuts) rev_indices in let _, rev_sigctx, tele_lhs, tele_rhs = CList.fold_left3 ( @@ -708,7 +711,7 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref) ) (succ nb_cuts, [], [], []) arity_ctx' rev_indices' omitted in let sigctx = List.rev rev_sigctx in - let sigty, _, sigconstr = telescope (push_rel_context (pi1 subst) env) evd sigctx in + let sigty, _, sigconstr = telescope (push_rel_context (subst.Context_map.src_ctx) env) evd sigctx in (* Build a goal with an equality of telescopes at the front. *) let left_sig = Vars.substl (List.rev tele_lhs) sigconstr in @@ -743,14 +746,14 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref) let indfam = Inductiveops.make_ind_family (pind, List.map EConstr.of_constr params) in let branches_info = Inductiveops.get_constructors env indfam in let full_subst = - let (ctx', pats, ctx) = Context_map.id_subst ctx in + let pats = Context_map.id_pats ctx in let pats = Context_map.lift_pats (oib.mind_nrealargs + 1) pats in - let ctx' = arity_ctx @ ctx' in + let ctx' = arity_ctx @ ctx in Context_map.mk_ctx_map env !evd ctx' pats ctx in let full_subst = Context_map.compose_subst ~unsafe:true env ~sigma:!evd subst full_subst in - let pats_ctx' = pi2 (Context_map.id_subst ctx') in - let pats_cuts = pi2 (Context_map.id_subst cuts_ctx) in + let pats_ctx' = Context_map.id_pats ctx' in + let pats_cuts = Context_map.id_pats cuts_ctx in let branches_subst = Array.map (fun summary -> (* This summary is under context [ctx']. *) let indices = summary.Inductiveops.cs_concl_realargs in @@ -770,7 +773,7 @@ let smart_case (env : Environ.env) (evd : Evd.evar_map ref) let cuts_ctx = Context_map.specialize_rel_context !evd pats cuts_ctx in let pats = Context_map.lift_pats nb_cuts pats in let pats = pats_cuts @ pats in - let csubst = Context_map.mk_ctx_map env !evd (cuts_ctx @ args @ ctx') pats (pi1 subst) in + let csubst = Context_map.mk_ctx_map env !evd (cuts_ctx @ args @ ctx') pats (subst.Context_map.src_ctx) in Context_map.compose_subst ~unsafe:true env ~sigma:!evd csubst full_subst ) branches_info in let branches_nb = Array.map (fun summary -> diff --git a/src/simplify.ml b/src/simplify.ml index e1db49de..90492824 100644 --- a/src/simplify.ml +++ b/src/simplify.ml @@ -735,7 +735,8 @@ SimpFun.make ~name:"solution" begin fun (env : Environ.env) (evd : Evd.evar_map raise (CannotSimplify (str "[solution] The variable appears on both sides of the equality.")) in (* let () = equations_debug (fun () -> str "solution on " ++ Printer.pr_econstr_env (push_rel_context ctx env) !evd ty) in *) - let (ctx', _, _) as subst, rev_subst = Context_map.new_strengthen env !evd ctx rel term in + let subst, rev_subst = Context_map.new_strengthen env !evd ctx rel term in + let ctx' = subst.Context_map.src_ctx in let trel' = Context_map.mapping_constr !evd subst trel in let rel' = EConstr.destRel !evd trel' in let term' = Context_map.mapping_constr !evd subst term in diff --git a/src/splitting.ml b/src/splitting.ml index 595ca0b1..877e13ca 100644 --- a/src/splitting.ml +++ b/src/splitting.ml @@ -161,7 +161,7 @@ let where_context wheres = let where_program_type w = program_type w.where_program -let pplhs env sigma lhs = pr_pats env sigma (pi2 lhs) +let pplhs env sigma lhs = pr_pats env sigma (lhs.Context_map.map_inst) let pr_splitting_rhs ?(verbose=false) env' env'' sigma lhs rhs ty = let verbose pp = if verbose then pp else mt () in @@ -194,7 +194,7 @@ let pr_splitting env sigma ?(verbose=false) split = let verb pp = if verbose then pp else mt () in let rec aux = function | Compute (lhs, wheres, ty, c) -> - let env' = push_rel_context (pi1 lhs) env in + let env' = push_rel_context (lhs.Context_map.src_ctx) env in let ppwhere w = hov 2 (str"where " ++ Id.print (where_id w) ++ str " : " ++ (try Printer.pr_econstr_env env' sigma w.where_type ++ @@ -212,7 +212,7 @@ let pr_splitting env sigma ?(verbose=false) split = (pr_splitting_rhs ~verbose env' env'' sigma lhs c ty ++ Pp.fnl () ++ ppwheres ++ verb (hov 2 (fnl () ++ str "(in context: " ++ spc () ++ pr_context_map env sigma lhs ++ str")" ++ fnl ()))) | Split (lhs, var, ty, cs) -> - let env' = push_rel_context (pi1 lhs) env in + let env' = push_rel_context (lhs.Context_map.src_ctx) env in (pplhs env' sigma lhs ++ str " split: " ++ pr_rel_name env' var ++ Pp.fnl () ++ verb (hov 2 (str" : " ++ @@ -234,7 +234,7 @@ let pr_splitting env sigma ?(verbose=false) split = info.refined_args, info.refined_revctx, info.refined_newprob, info.refined_newty in - let env' = push_rel_context (pi1 lhs) env in + let env' = push_rel_context (lhs.Context_map.src_ctx) env in hov 0 (pplhs env' sigma lhs ++ str " with " ++ Id.print id ++ str" := " ++ Printer.pr_econstr_env env' sigma (mapping_constr sigma revctx c) ++ Pp.fnl () ++ verb (hov 2 (str " : " ++ Printer.pr_econstr_env env' sigma cty ++ str" " ++ @@ -244,8 +244,8 @@ let pr_splitting env sigma ?(verbose=false) split = hov 2 (str "refine args: " ++ prlist_with_sep spc (Printer.pr_econstr_env env' sigma) info.refined_args) ++ hov 2 (str "New problem: " ++ pr_context_map env sigma newprob) ++ - hov 2 (str "For type: " ++ Printer.pr_econstr_env (push_rel_context (pi1 newprob) env) sigma newty) ++ - hov 2 (str"Eliminating:" ++ pr_rel_name (push_rel_context (pi1 newprob) env) (snd arg) ++ spc ()) ++ + hov 2 (str "For type: " ++ Printer.pr_econstr_env (push_rel_context (newprob.Context_map.src_ctx) env) sigma newty) ++ + hov 2 (str"Eliminating:" ++ pr_rel_name (push_rel_context (newprob.Context_map.src_ctx) env) (snd arg) ++ spc ()) ++ hov 2 (str "Revctx is: " ++ pr_context_map env sigma revctx) ++ hov 2 (str "New problem to problem substitution is: " ++ pr_context_map env sigma info.refined_newprob_to_lhs ++ Pp.fnl ()))) ++ hov 0 (aux s)) @@ -482,7 +482,8 @@ let check_typed ~where ?name env evd c = let term_of_tree env0 isevar sort tree = let rec aux env evm sort = function - | Compute ((ctx, _, _), where, ty, RProgram rhs) -> + | Compute (subst, where, ty, RProgram rhs) -> + let ctx = subst.Context_map.src_ctx in let compile_where ({where_program; where_type} as w) (env, evm, ctx) = let evm, c', ty' = evm, where_term w, where_type in @@ -492,8 +493,9 @@ let term_of_tree env0 isevar sort tree = let body = it_mkLambda_or_LetIn rhs ctx and typ = it_mkProd_or_subst env evm ty ctx in evm, body, typ - | Compute ((ctx, _, _) as lhs, where, ty, REmpty (split, sp)) -> + | Compute (lhs, where, ty, REmpty (split, sp)) -> assert (List.is_empty where); + let ctx = lhs.Context_map.src_ctx in let evm, bot = new_global evm (Lazy.force logic_bot) in let evm, prf, _ = aux env evm sort (Split (lhs, split, bot, sp)) in let evm, case = new_global evm (Lazy.force logic_bot_case) in @@ -502,14 +504,16 @@ let term_of_tree env0 isevar sort tree = let ty = it_mkProd_or_subst env evm ty ctx in evm, term, ty - | Mapping ((ctx, p, ctx'), s) -> + | Mapping (subst, s) -> + let ctx = subst.Context_map.src_ctx in let evm, term, ty = aux env evm sort s in - let args = Array.rev_of_list (snd (constrs_of_pats ~inacc_and_hide:false env evm p)) in + let args = Array.rev_of_list (snd (constrs_of_pats ~inacc_and_hide:false env evm subst.Context_map.map_inst)) in let term = it_mkLambda_or_LetIn (whd_beta env evm (mkApp (term, args))) ctx in let ty = it_mkProd_or_subst env evm (prod_appvect evm ty args) ctx in evm, term, ty - | Refined ((ctx, _, _), info, rest) -> + | Refined (subst, info, rest) -> + let ctx = subst.Context_map.src_ctx in let (id, _, _), ty, rarg, path, f, args, newprob, newty = info.refined_obj, info.refined_rettyp, info.refined_arg, info.refined_path, @@ -522,7 +526,8 @@ let term_of_tree env0 isevar sort tree = let ty = it_mkProd_or_subst env evm ty ctx in evm, term, ty - | Split ((ctx, _, _) as subst, rel, ty, sp) -> + | Split (subst, rel, ty, sp) -> + let ctx = subst.Context_map.src_ctx in (* Produce parts of a case that will be relevant. *) let evm, block = Equations_common.(get_fresh evm coq_block) in let blockty = mkLetIn (anonR, block, Retyping.get_type_of env evm block, lift 1 ty) in @@ -590,7 +595,7 @@ let term_of_tree env0 isevar sort tree = let next_subst = context_map_of_splitting s in let perm_subst = Context_map.make_permutation ~env evm subst next_subst in (* [next_term] starts with lambdas, so we apply it to its context. *) - let args = Equations_common.extended_rel_vect 0 (pi3 perm_subst) in + let args = Equations_common.extended_rel_vect 0 (perm_subst.Context_map.tgt_ctx) in let next_term = beta_appvect !evd next_term args in let next_term = Context_map.mapping_constr evm perm_subst next_term in (* We know the term is a correct instantiation of the evar, we @@ -702,8 +707,8 @@ let make_program env evd p prob s rec_info = | Some t -> t in let term = beta_appvect !evd wfr.wf_rec_term - [| beta_appvect !evd fn (extended_rel_vect 0 (pi1 lhs)) |] in - Single (p, prob, rec_info, s, it_mkLambda_or_LetIn term (pi1 lhs)) + [| beta_appvect !evd fn (extended_rel_vect 0 (lhs.Context_map.src_ctx)) |] in + Single (p, prob, rec_info, s, it_mkLambda_or_LetIn term (lhs.Context_map.src_ctx)) | StructRec sr -> let term, ty = term_of_tree env evd sort s in let args = extended_rel_vect 0 r.rec_lets in @@ -725,7 +730,7 @@ let make_program env evd p prob s rec_info = | NestedOn None -> (match s with | Split (ctx, var, _, _) -> - NestedOn (Some ((List.length (pi1 ctx)) - var - sr.struct_rec_protos, None)) + NestedOn (Some ((List.length (ctx.Context_map.src_ctx)) - var - sr.struct_rec_protos, None)) | _ -> ann) | _ -> ann in @@ -822,15 +827,16 @@ let make_single_program env evd flags p prob s rec_info = | [p] -> p | _ -> raise (Invalid_argument "make_single_program: more than one program") -let change_lhs s (l, p, r) = +let change_lhs s subs = let open Context.Rel.Declaration in let l' = List.map (function LocalDef ({binder_name=Name id}, b, t) as decl -> (try let b' = List.assoc id s in LocalDef (make_annot (Name id) (get_relevance decl), b', t) with Not_found -> decl) - | decl -> decl) l - in l', p, r + | decl -> decl) subs.Context_map.src_ctx + in + { subs with Context_map.src_ctx = l' } let change_splitting s sp = let rec aux = function @@ -866,8 +872,8 @@ let check_splitting env evd sp = () | Split (lhs, rel, ty, sp) -> let _ = check_ctx_map env evd lhs in - let _r = lookup_rel rel (push_rel_context (pi1 lhs) env) in - let _ = check_type (pi1 lhs) ty in + let _r = lookup_rel rel (push_rel_context (lhs.Context_map.src_ctx) env) in + let _ = check_type (lhs.Context_map.src_ctx) ty in Array.iter (Option.iter aux) sp | Mapping (lhs, sp) -> let _ = check_ctx_map env evd lhs in @@ -884,7 +890,7 @@ let check_splitting env evd sp = let def = make_def (nameR (where_id w)) (Some (where_term w)) w.where_type in def :: ctx in - let ctx = List.fold_left check_where (pi1 lhs) wheres in + let ctx = List.fold_left check_where (lhs.Context_map.src_ctx) wheres in ctx and check_program p = let ty = program_type p in @@ -966,12 +972,13 @@ let define_one_program_constants flags env0 isevar udecl unfold p = let evm, s' = aux env evm s in evm, Mapping (lhs, s') - | Refined ((ctx, _, _) as lhs, info, rest) -> + | Refined (lhs, info, rest) -> + let ctx = lhs.Context_map.src_ctx in let evm', rest' = aux env evm rest in let isevar = ref evm' in let env = Global.env () in let sort = - (Retyping.get_sort_of (push_rel_context (pi1 lhs) env) !isevar info.refined_rettyp) in + (Retyping.get_sort_of (push_rel_context ctx env) !isevar info.refined_rettyp) in let t, ty = term_of_tree env isevar sort rest' in let (cst, (evm, e)) = Equations_common.declare_constant (path_id ~unfold info.refined_path) @@ -1325,7 +1332,7 @@ let define_programs ~pm env evd udecl is_recursive fixprots flags ?(unfold=false let mapping_rhs sigma s = function | RProgram c -> RProgram (mapping_constr sigma s c) | REmpty (i, sp) -> - try match nth (pi2 s) (pred i) with + try match nth (s.Context_map.map_inst) (pred i) with | PRel i' -> REmpty (i', sp) | _ -> assert false with Not_found -> assert false