diff options
Diffstat (limited to 'checker/declarations.ml')
| -rw-r--r-- | checker/declarations.ml | 51 |
1 files changed, 31 insertions, 20 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index d2c3f203..0540227c 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -196,7 +196,12 @@ let subst_con0 sub con u = let dup con = con, Const (con, u) in let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in match constant_of_delta_with_inline resolve con' with - | Some t -> con', subst_instance_constr u t + | Some (ctx, t) -> + (** FIXME: we never typecheck the inlined term, so that it could well + be garbage. What environment do we type it in though? The substitution + code should be moot in the checker but it **is** used nonetheless. *) + let () = assert (Univ.AUContext.size ctx == Univ.Instance.length u) in + con', subst_instance_constr u t | None -> let con'' = match side with | User -> constant_of_delta resolve con' @@ -209,11 +214,7 @@ let rec map_kn f f' c = match c with | Const (kn, u) -> (try snd (f' kn u) with No_subst -> c) | Proj (p,t) -> - let p' = - Projection.map (fun kn -> - try fst (f' kn Univ.Instance.empty) - with No_subst -> kn) p - in + let p' = Projection.map f p in let t' = func t in if p' == p && t' == t then c else Proj (p', t') @@ -231,7 +232,7 @@ let rec map_kn f f' c = in let p' = func p in let ct' = func ct in - let l' = Array.smartmap func l in + let l' = Array.Smart.map func l in if (ci.ci_ind==ci_ind && p'==p && l'==l && ct'==ct)then c else @@ -260,21 +261,21 @@ let rec map_kn f f' c = else LetIn (na, b', t', ct') | App (ct,l) -> let ct' = func ct in - let l' = Array.smartmap func l in + let l' = Array.Smart.map func l in if (ct'== ct && l'==l) then c else App (ct',l') | Evar (e,l) -> - let l' = Array.smartmap func l in + let l' = Array.Smart.map func l in if (l'==l) then c else Evar (e,l') | Fix (ln,(lna,tl,bl)) -> - let tl' = Array.smartmap func tl in - let bl' = Array.smartmap func bl in + let tl' = Array.Smart.map func tl in + let bl' = Array.Smart.map func bl in if (bl == bl'&& tl == tl') then c else Fix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.smartmap func tl in - let bl' = Array.smartmap func bl in + let tl' = Array.Smart.map func tl in + let bl' = Array.Smart.map func bl in if (bl == bl'&& tl == tl') then c else CoFix (ln,(lna,tl',bl')) | _ -> c @@ -340,7 +341,7 @@ let gen_subst_delta_resolver dom subst resolver = let kkey' = if dom then subst_kn subst kkey else kkey in let hint' = match hint with | Equiv kequ -> Equiv (subst_kn_delta subst kequ) - | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t)) + | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t)) | Inline (_,None) -> hint in Deltamap.add_kn kkey' hint' rslv @@ -480,7 +481,7 @@ let dest_subterms p = let (_,cstrs) = Rtree.dest_node p in Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs -let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p +let subst_wf_paths sub p = Rtree.Smart.map (subst_recarg sub) p let eq_recarg r1 r2 = match r1, r2 with | Norec, Norec -> true @@ -490,6 +491,16 @@ let eq_recarg r1 r2 = match r1, r2 with let eq_wf_paths = Rtree.equal eq_recarg +let inductive_make_projections ind mib = + match mib.mind_record with + | NotRecord | FakeRecord -> None + | PrimRecord infos -> + let projs = Array.mapi (fun proj_arg lab -> + Names.Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab) + (pi2 infos.(snd ind)) + in + Some projs + (**********************************************************************) (* Representation of mutual inductive types in the kernel *) (* @@ -513,7 +524,7 @@ let subst_decl_arity f g sub ar = let subst_rel_declaration sub = Term.map_rel_decl (subst_mps sub) -let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) +let subst_rel_context sub = List.Smart.map (subst_rel_declaration sub) let constant_is_polymorphic cb = match cb.const_universes with @@ -544,10 +555,10 @@ let subst_mind_packet sub mbp = mind_consnrealdecls = mbp.mind_consnrealdecls; mind_consnrealargs = mbp.mind_consnrealargs; mind_typename = mbp.mind_typename; - mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; + mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; mind_arity = subst_ind_arity sub mbp.mind_arity; - mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; + mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; mind_nrealdecls = mbp.mind_nrealdecls; mind_kelim = mbp.mind_kelim; @@ -560,7 +571,7 @@ let subst_mind_packet sub mbp = let subst_mind sub mib = { mib with mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt; - mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets } + mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets } (* Modules *) @@ -599,7 +610,7 @@ and subst_body : 'a. (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generi mod_mp = subst_mp sub mb.mod_mp; mod_expr = subst_impl sub mb.mod_expr; mod_type = subst_signature sub mb.mod_type; - mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg } + mod_type_alg = Option.Smart.map (subst_expression sub) mb.mod_type_alg } and subst_module sub mb = subst_body (fun sub e -> implem_map (subst_signature sub) (subst_expression sub) e) sub mb |