diff options
Diffstat (limited to 'checker/declarations.ml')
| -rw-r--r-- | checker/declarations.ml | 582 |
1 files changed, 159 insertions, 423 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 890996d1..c6709a78 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -1,44 +1,14 @@ open Util open Names +open Cic open Term -open Validate - -(* Bytecode *) -type values -type reloc_table -type to_patch_substituted -(*Retroknowledge *) -type action -type retroknowledge - -type engagement = ImpredicativeSet -let val_eng = val_enum "eng" 1 - - -type polymorphic_arity = { - poly_param_levels : Univ.universe option list; - poly_level : Univ.universe; -} -let val_pol_arity = - val_tuple ~name:"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|] - -type constant_type = - | NonPolymorphicType of constr - | PolymorphicArity of rel_context * polymorphic_arity - -let val_cst_type = - val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|] (** Substitutions, code imported from kernel/mod_subst *) -type delta_hint = - | Inline of int * constr option - | Equiv of kernel_name - - module Deltamap = struct - type t = module_path MPmap.t * delta_hint KNmap.t + type t = delta_resolver let empty = MPmap.empty, KNmap.empty + let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km) let add_mp mp mp' (mm,km) = (MPmap.add mp mp' mm, km) let remove_mp mp (mm,km) = (MPmap.remove mp mm, km) @@ -52,18 +22,10 @@ module Deltamap = struct let join map1 map2 = fold add_mp add_kn map1 map2 end -type delta_resolver = Deltamap.t - let empty_delta_resolver = Deltamap.empty -module MBImap = Map.Make - (struct - type t = mod_bound_id - let compare = Pervasives.compare - end) - module Umap = struct - type 'a t = 'a MPmap.t * 'a MBImap.t + type 'a t = 'a umap_t let empty = MPmap.empty, MBImap.empty let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2 let add_mbi mbi x (m1,m2) = (m1,MBImap.add mbi x m2) @@ -78,29 +40,12 @@ module Umap = struct let join map1 map2 = fold add_mp add_mbi map1 map2 end -type substitution = (module_path * delta_resolver) Umap.t type 'a subst_fun = substitution -> 'a -> 'a let empty_subst = Umap.empty let is_empty_subst = Umap.is_empty -let val_delta_hint = - val_sum "delta_hint" 0 - [|[|val_int; val_opt val_constr|];[|val_kn|]|] - -let val_res = - val_tuple ~name:"delta_resolver" - [|val_map ~name:"delta_resolver" val_mp val_mp; - val_map ~name:"delta_resolver" val_kn val_delta_hint|] - -let val_mp_res = val_tuple [|val_mp;val_res|] - -let val_subst = - val_tuple ~name:"substitution" - [|val_map ~name:"substitution" val_mp val_mp_res; - val_map ~name:"substitution" val_uid val_mp_res|] - let add_mbid mbid mp = Umap.add_mbi mbid (mp,empty_delta_resolver) let add_mp mp1 mp2 = Umap.add_mp mp1 (mp2,empty_delta_resolver) @@ -110,7 +55,7 @@ let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst let mp_in_delta mp = Deltamap.mem_mp mp -let rec find_prefix resolve mp = +let find_prefix resolve mp = let rec sub_mp = function | MPdot(mp,l) as mp_sup -> (try Deltamap.find_mp mp_sup resolve @@ -136,10 +81,8 @@ let solve_delta_kn resolve kn = make_kn new_mp dir l let gen_of_delta resolve x kn fix_can = - try - let new_kn = solve_delta_kn resolve kn in - if kn == new_kn then x else fix_can new_kn - with _ -> x + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then x else fix_can new_kn let constant_of_delta resolve con = let kn = user_con con in @@ -221,6 +164,11 @@ let gen_subst_mp f sub mp1 mp2 = | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2 +let make_mind_equiv mpu mpc dir l = + let knu = make_kn mpu dir l in + if mpu == mpc then mind_of_kn knu + else mind_of_kn_equiv knu (make_kn mpc dir l) + let subst_ind sub mind = let kn1,kn2 = user_mind mind, canonical_mind mind in let mp1,dir,l = repr_kn kn1 in @@ -233,12 +181,17 @@ let subst_ind sub mind = | Canonical -> mind_of_delta2 resolve mind' with No_subst -> mind -let subst_con0 sub con = +let make_con_equiv mpu mpc dir l = + let knu = make_kn mpu dir l in + if mpu == mpc then constant_of_kn knu + else constant_of_kn_equiv knu (make_kn mpc dir l) + +let subst_con0 sub con u = let kn1,kn2 = user_con con,canonical_con con in let mp1,dir,l = repr_kn kn1 in let mp2,_,_ = repr_kn kn2 in let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in - let dup con = con, Const con in + 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', t @@ -252,13 +205,21 @@ let subst_con0 sub con = let rec map_kn f f' c = let func = map_kn f f' in match c with - | Const kn -> (try snd (f' kn) with No_subst -> c) - | Ind (kn,i) -> + | Const (kn, u) -> (try snd (f' kn u) with No_subst -> c) + | Proj (kn,t) -> + let kn' = + try fst (f' kn Univ.Instance.empty) + with No_subst -> kn + in + let t' = func t in + if kn' == kn && t' == t then c + else Proj (kn', t') + | Ind ((kn,i),u) -> let kn' = f kn in - if kn'==kn then c else Ind (kn',i) - | Construct ((kn,i),j) -> + if kn'==kn then c else Ind ((kn',i),u) + | Construct (((kn,i),j),u) -> let kn' = f kn in - if kn'==kn then c else Construct ((kn',i),j) + if kn'==kn then c else Construct (((kn',i),j),u) | Case (ci,p,ct,l) -> let ci_ind = let (kn,i) = ci.ci_ind in @@ -267,7 +228,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.smartmap func l in if (ci.ci_ind==ci_ind && p'==p && l'==l && ct'==ct)then c else @@ -296,21 +257,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.smartmap 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.smartmap 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.smartmap func tl in + let bl' = Array.smartmap 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.smartmap func tl in + let bl' = Array.smartmap func bl in if (bl == bl'&& tl == tl') then c else CoFix (ln,(lna,tl',bl')) | _ -> c @@ -318,24 +279,10 @@ let rec map_kn f f' c = let subst_mps sub c = if is_empty_subst sub then c else map_kn (subst_ind sub) (subst_con0 sub) c - - -type 'a lazy_subst = - | LSval of 'a - | LSlazy of substitution list * 'a - -type 'a substituted = 'a lazy_subst ref - -let val_substituted val_a = - val_ref - (val_sum "constr_substituted" 0 - [|[|val_a|];[|val_list val_subst;val_a|]|]) - -let from_val a = ref (LSval a) let rec replace_mp_in_mp mpfrom mpto mp = match mp with - | _ when mp = mpfrom -> mpto + | _ when ModPath.equal mp mpfrom -> mpto | MPdot (mp1,l) -> let mp1' = replace_mp_in_mp mpfrom mpto mp1 in if mp1==mp1' then mp @@ -344,7 +291,7 @@ let rec replace_mp_in_mp mpfrom mpto mp = let rec mp_in_mp mp mp1 = match mp1 with - | _ when mp1 = mp -> true + | _ when ModPath.equal mp1 mp -> true | MPdot (mp2,l) -> mp_in_mp mp mp2 | _ -> false @@ -417,14 +364,14 @@ let update_delta_resolver resolver1 resolver2 = let add_delta_resolver resolver1 resolver2 = if resolver1 == resolver2 then resolver2 - else if resolver2 = empty_delta_resolver then + else if Deltamap.is_empty resolver2 then resolver1 else Deltamap.join (update_delta_resolver resolver1 resolver2) resolver2 let substition_prefixed_by k mp subst = let mp_prefixmp kmp (mp_to,reso) sub = - if mp_in_mp mp kmp && mp <> kmp then + if mp_in_mp mp kmp && not (ModPath.equal mp kmp) then let new_key = replace_mp_in_mp mp k kmp in Umap.add_mp new_key (mp_to,reso) sub else sub @@ -455,75 +402,51 @@ let join subst1 subst2 = let subst = Umap.fold mp_apply_subst mbi_apply_subst subst1 empty_subst in Umap.join subst2 subst -let force fsubst r = - match !r with - | LSval a -> a - | LSlazy(s,a) -> - let subst = List.fold_left join empty_subst (List.rev s) in - let a' = fsubst subst a in - r := LSval a'; - a' - -let subst_substituted s r = - match !r with - | LSval a -> ref (LSlazy([s],a)) - | LSlazy(s',a) -> - ref (LSlazy(s::s',a)) +let from_val x = { subst_value = x; subst_subst = []; } -let force_constr = force subst_mps +let force fsubst r = match r.subst_subst with +| [] -> r.subst_value +| s -> + let subst = List.fold_left join empty_subst (List.rev s) in + let x = fsubst subst r.subst_value in + let () = r.subst_subst <- [] in + let () = r.subst_value <- x in + x -type constr_substituted = constr substituted +let subst_substituted s r = { r with subst_subst = s :: r.subst_subst; } -let val_cstr_subst = val_substituted val_constr +let force_constr = force subst_mps let subst_constr_subst = subst_substituted -(** Beware! In .vo files, lazy_constr are stored as integers - used as indexes for a separate table. The actual lazy_constr is restored - later, by [Safe_typing.LightenLibrary.load]. This allows us - to use here a different definition of lazy_constr than coqtop: - since the checker will inspect all proofs parts, even opaque - ones, no need to use Lazy.t here *) - -type lazy_constr = constr_substituted -let subst_lazy_constr = subst_substituted -let force_lazy_constr = force_constr -let lazy_constr_from_val c = c -let val_lazy_constr = val_cstr_subst - -(** Inlining level of parameters at functor applications. - This is ignored by the checker. *) - -type inline = int option +let subst_lazy_constr sub = function + | Indirect (l,dp,i) -> Indirect (sub::l,dp,i) -(** A constant can have no body (axiom/parameter), or a - transparent body, or an opaque one *) +let indirect_opaque_access = + ref ((fun dp i -> assert false) : DirPath.t -> int -> constr) +let indirect_opaque_univ_access = + ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.constraints) -type constant_def = - | Undef of inline - | Def of constr_substituted - | OpaqueDef of lazy_constr +let force_lazy_constr = function + | Indirect (l,dp,i) -> + let c = !indirect_opaque_access dp i in + force_constr (List.fold_right subst_constr_subst l (from_val c)) -let val_cst_def = - val_sum "constant_def" 0 - [|[|val_opt val_int|]; [|val_cstr_subst|]; [|val_lazy_constr|]|] +let force_lazy_constr_univs = function + | OpaqueDef (Indirect (l,dp,i)) -> !indirect_opaque_univ_access dp i + | _ -> Univ.empty_constraint let subst_constant_def sub = function | Undef inl -> Undef inl | Def c -> Def (subst_constr_subst sub c) | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc) -type constant_body = { - const_hyps : section_context; (* New: younger hyp at top *) - const_body : constant_def; - const_type : constant_type; - const_body_code : to_patch_substituted; - const_constraints : Univ.constraints } +(** Local variables and graph *) let body_of_constant cb = match cb.const_body with | Undef _ -> None - | Def c -> Some c - | OpaqueDef c -> Some c + | Def c -> Some (force_constr c) + | OpaqueDef c -> Some (force_lazy_constr c) let constant_has_body cb = match cb.const_body with | Undef _ -> false @@ -533,40 +456,18 @@ let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true | Def _ | Undef _ -> false -let val_cb = val_tuple ~name:"constant_body" - [|val_nctxt; - val_cst_def; - val_cst_type; - no_val; - val_cstrs|] - let subst_rel_declaration sub (id,copt,t as x) = let copt' = Option.smartmap (subst_mps sub) copt in let t' = subst_mps sub t in - if copt == copt' & t == t' then x else (id,copt',t') - -let subst_rel_context sub = list_smartmap (subst_rel_declaration sub) + if copt == copt' && t == t' then x else (id,copt',t') -type recarg = - | Norec - | Mrec of inductive - | Imbr of inductive -let val_recarg = val_sum "recarg" 1 (* Norec *) - [|[|val_ind|] (* Mrec *);[|val_ind|] (* Imbr *)|] +let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) let subst_recarg sub r = match r with | Norec -> r | (Mrec(kn,i)|Imbr (kn,i)) -> let kn' = subst_ind sub kn in if kn==kn' then r else Imbr (kn',i) -type wf_paths = recarg Rtree.t -let val_wfp = val_rec_sum "wf_paths" 0 - (fun val_wfp -> - [|[|val_int;val_int|]; (* Rtree.Param *) - [|val_recarg;val_array val_wfp|]; (* Rtree.Node *) - [|val_int;val_array val_wfp|] (* Rtree.Rec *) - |]) - let mk_norec = Rtree.mk_node Norec [||] let mk_paths r recargs = @@ -581,6 +482,14 @@ let dest_subterms p = let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p +let eq_recarg r1 r2 = match r1, r2 with + | Norec, Norec -> true + | Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 + | Imbr i1, Imbr i2 -> Names.eq_ind i1 i2 + | _ -> false + +let eq_wf_paths = Rtree.equal eq_recarg + (**********************************************************************) (* Representation of mutual inductive types in the kernel *) (* @@ -589,142 +498,66 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn *) -type monomorphic_inductive_arity = { - mind_user_arity : constr; - mind_sort : sorts; -} -let val_mono_ind_arity = - val_tuple ~name:"monomorphic_inductive_arity"[|val_constr;val_sort|] - -type inductive_arity = -| Monomorphic of monomorphic_inductive_arity -| Polymorphic of polymorphic_arity -let val_ind_arity = val_sum "inductive_arity" 0 - [|[|val_mono_ind_arity|];[|val_pol_arity|]|] - -type one_inductive_body = { - -(* Primitive datas *) - - (* Name of the type: [Ii] *) - mind_typename : identifier; - (* Arity context of [Ii] with parameters: [forall params, Ui] *) - mind_arity_ctxt : rel_context; +let subst_decl_arity f g sub ar = + match ar with + | RegularArity x -> + let x' = f sub x in + if x' == x then ar + else RegularArity x' + | TemplateArity x -> + let x' = g sub x in + if x' == x then ar + else TemplateArity x' - (* Arity sort, original user arity, and allowed elim sorts, if monomorphic *) - mind_arity : inductive_arity; +let map_decl_arity f g = function + | RegularArity a -> RegularArity (f a) + | TemplateArity a -> TemplateArity (g a) - (* Names of the constructors: [cij] *) - mind_consnames : identifier array; - (* Types of the constructors with parameters: [forall params, Tij], - where the Ik are replaced by de Bruijn index in the context - I1:forall params, U1 .. In:forall params, Un *) - mind_user_lc : constr array; - -(* Derived datas *) - - (* Number of expected real arguments of the type (no let, no params) *) - mind_nrealargs : int; - - (* Length of realargs context (with let, no params) *) - mind_nrealargs_ctxt : int; - - (* List of allowed elimination sorts *) - mind_kelim : sorts_family list; - - (* Head normalized constructor types so that their conclusion is atomic *) - mind_nf_lc : constr array; - - (* Length of the signature of the constructors (with let, w/o params) *) - mind_consnrealdecls : int array; - - (* Signature of recursive arguments in the constructors *) - mind_recargs : wf_paths; - -(* Datas for bytecode compilation *) - - (* number of constant constructor *) - mind_nb_constant : int; - - (* number of no constant constructor *) - mind_nb_args : int; - - mind_reloc_tbl : reloc_table; - } - -let val_one_ind = val_tuple ~name:"one_inductive_body" - [|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr; - val_int;val_int;val_list val_sortfam;val_array val_constr;val_array val_int; - val_wfp;val_int;val_int;no_val|] - - -type mutual_inductive_body = { - - (* The component of the mutual inductive block *) - mind_packets : one_inductive_body array; - - (* Whether the inductive type has been declared as a record *) - mind_record : bool; - - (* Whether the type is inductive or coinductive *) - mind_finite : bool; - - (* Number of types in the block *) - mind_ntypes : int; - - (* Section hypotheses on which the block depends *) - mind_hyps : section_context; +let subst_rel_declaration sub (id,copt,t as x) = + let copt' = Option.smartmap (subst_mps sub) copt in + let t' = subst_mps sub t in + if copt == copt' && t == t' then x else (id,copt',t') - (* Number of expected parameters *) - mind_nparams : int; +let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) - (* Number of recursively uniform (i.e. ordinary) parameters *) - mind_nparams_rec : int; +let subst_template_cst_arity sub (ctx,s as arity) = + let ctx' = subst_rel_context sub ctx in + if ctx==ctx' then arity else (ctx',s) - (* The context of parameters (includes let-in declaration) *) - mind_params_ctxt : rel_context; +let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s - (* Universes constraints enforced by the inductive declaration *) - mind_constraints : Univ.constraints; +(* TODO: should be changed to non-coping after Term.subst_mps *) +(* NB: we leave bytecode and native code fields untouched *) +let subst_const_body sub cb = + { cb with + const_body = subst_constant_def sub cb.const_body; + const_type = subst_arity sub cb.const_type } - } -let val_ind_pack = val_tuple ~name:"mutual_inductive_body" - [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt; - val_int; val_int; val_rctxt;val_cstrs|] +let subst_regular_ind_arity sub s = + let uar' = subst_mps sub s.mind_user_arity in + if uar' == s.mind_user_arity then s + else { mind_user_arity = uar'; mind_sort = s.mind_sort } -let subst_arity sub = function -| NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) -| PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) +let subst_template_ind_arity sub s = s -(* TODO: should be changed to non-coping after Term.subst_mps *) -let subst_const_body sub cb = { - const_hyps = (assert (cb.const_hyps=[]); []); - const_body = subst_constant_def sub cb.const_body; - const_type = subst_arity sub cb.const_type; - const_body_code = (*Cemitcodes.subst_to_patch_subst sub*) cb.const_body_code; - const_constraints = cb.const_constraints} - -let subst_arity sub = function -| Monomorphic s -> - Monomorphic { - mind_user_arity = subst_mps sub s.mind_user_arity; - mind_sort = s.mind_sort; - } -| Polymorphic s as x -> x +(* FIXME records *) +let subst_ind_arity = + subst_decl_arity subst_regular_ind_arity subst_template_ind_arity let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; 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.smartmap (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; - mind_arity = subst_arity sub mbp.mind_arity; - mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc; + mind_arity = subst_ind_arity sub mbp.mind_arity; + mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; - mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; + mind_nrealdecls = mbp.mind_nrealdecls; mind_kelim = mbp.mind_kelim; mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); mind_nb_constant = mbp.mind_nb_constant; @@ -733,146 +566,49 @@ let subst_mind_packet sub mbp = let subst_mind sub mib = - { mind_record = mib.mind_record ; - mind_finite = mib.mind_finite ; - mind_ntypes = mib.mind_ntypes ; - mind_hyps = (assert (mib.mind_hyps=[]); []) ; - mind_nparams = mib.mind_nparams; - mind_nparams_rec = mib.mind_nparams_rec; - 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_constraints = mib.mind_constraints } + { 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 } (* Modules *) -(* Whenever you change these types, please do update the validation - functions below *) -type structure_field_body = - | SFBconst of constant_body - | SFBmind of mutual_inductive_body - | SFBmodule of module_body - | SFBmodtype of module_type_body - -and structure_body = (label * structure_field_body) list - -and struct_expr_body = - | SEBident of module_path - | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body - | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints - | SEBstruct of structure_body - | SEBwith of struct_expr_body * with_declaration_body - -and with_declaration_body = - With_module_body of identifier list * module_path - | With_definition_body of identifier list * constant_body - -and module_body = - { mod_mp : module_path; - mod_expr : struct_expr_body option; - mod_type : struct_expr_body; - mod_type_alg : struct_expr_body option; - mod_constraints : Univ.constraints; - mod_delta : delta_resolver; - mod_retroknowledge : action list} - -and module_type_body = - { typ_mp : module_path; - typ_expr : struct_expr_body; - typ_expr_alg : struct_expr_body option ; - typ_constraints : Univ.constraints; - typ_delta :delta_resolver} - -(* the validation functions: *) -let rec val_sfb o = val_sum "struct_field_body" 0 - [|[|val_cb|]; (* SFBconst *) - [|val_ind_pack|]; (* SFBmind *) - [|val_module|]; (* SFBmodule *) - [|val_modtype|] (* SFBmodtype *) - |] o -and val_sb o = val_list (val_tuple ~name:"label*sfb"[|val_id;val_sfb|]) o -and val_seb o = val_sum "struct_expr_body" 0 - [|[|val_mp|]; (* SEBident *) - [|val_uid;val_modtype;val_seb|]; (* SEBfunctor *) - [|val_seb;val_seb;val_cstrs|]; (* SEBapply *) - [|val_sb|]; (* SEBstruct *) - [|val_seb;val_with|] (* SEBwith *) - |] o -and val_with o = val_sum "with_declaration_body" 0 - [|[|val_list val_id;val_mp|]; - [|val_list val_id;val_cb|]|] o -and val_module o = val_tuple ~name:"module_body" - [|val_mp;val_opt val_seb;val_seb; - val_opt val_seb;val_cstrs;val_res;no_val|] o -and val_modtype o = val_tuple ~name:"module_type_body" - [|val_mp;val_seb;val_opt val_seb;val_cstrs;val_res|] o - - -let rec subst_with_body sub = function - | With_module_body(id,mp) -> - With_module_body(id,subst_mp sub mp) - | With_definition_body(id,cb) -> - With_definition_body( id,subst_const_body sub cb) - -and subst_modtype sub mtb= - let typ_expr' = subst_struct_expr sub mtb.typ_expr in - let typ_alg' = - Option.smartmap - (subst_struct_expr sub) mtb.typ_expr_alg in - let mp = subst_mp sub mtb.typ_mp - in - if typ_expr'==mtb.typ_expr && - typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then - mtb - else - {mtb with - typ_mp = mp; - typ_expr = typ_expr'; - typ_expr_alg = typ_alg'} +let rec functor_map fty f0 = function + | NoFunctor a -> NoFunctor (f0 a) + | MoreFunctor (mbid,ty,e) -> MoreFunctor(mbid,fty ty,functor_map fty f0 e) -and subst_structure sub sign = - let subst_body = function - SFBconst cb -> - SFBconst (subst_const_body sub cb) - | SFBmind mib -> - SFBmind (subst_mind sub mib) - | SFBmodule mb -> - SFBmodule (subst_module sub mb) - | SFBmodtype mtb -> - SFBmodtype (subst_modtype sub mtb) - in - List.map (fun (l,b) -> (l,subst_body b)) sign +let implem_map fs fa = function + | Struct s -> Struct (fs s) + | Algebraic a -> Algebraic (fa a) + | impl -> impl +let subst_with_body sub = function + | WithMod(id,mp) -> WithMod(id,subst_mp sub mp) + | WithDef(id,c) -> WithDef(id,subst_mps sub c) -and subst_module sub mb = - let mtb' = subst_struct_expr sub mb.mod_type in - let typ_alg' = Option.smartmap - (subst_struct_expr sub ) mb.mod_type_alg in - let me' = Option.smartmap - (subst_struct_expr sub) mb.mod_expr in - let mp = subst_mp sub mb.mod_mp in - if mtb'==mb.mod_type && mb.mod_expr == me' - && mp == mb.mod_mp - then mb else - { mb with - mod_mp = mp; - mod_expr = me'; - mod_type_alg = typ_alg'; - mod_type=mtb'} - -and subst_struct_expr sub = function - | SEBident mp -> SEBident (subst_mp sub mp) - | SEBfunctor (mbid, mtb, meb') -> - SEBfunctor(mbid,subst_modtype sub mtb - ,subst_struct_expr sub meb') - | SEBstruct (str)-> - SEBstruct( subst_structure sub str) - | SEBapply (meb1,meb2,cst)-> - SEBapply(subst_struct_expr sub meb1, - subst_struct_expr sub meb2, - cst) - | SEBwith (meb,wdb)-> - SEBwith(subst_struct_expr sub meb, - subst_with_body sub wdb) +let rec subst_expr sub = function + | MEident mp -> MEident (subst_mp sub mp) + | MEapply (me1,mp2)-> MEapply (subst_expr sub me1, subst_mp sub mp2) + | MEwith (me,wd)-> MEwith (subst_expr sub me, subst_with_body sub wd) + +let rec subst_expression sub me = + functor_map (subst_module sub) (subst_expr sub) me +and subst_signature sub sign = + functor_map (subst_module sub) (subst_structure sub) sign +and subst_structure sub struc = + let subst_body = function + | SFBconst cb -> SFBconst (subst_const_body sub cb) + | SFBmind mib -> SFBmind (subst_mind sub mib) + | SFBmodule mb -> SFBmodule (subst_module sub mb) + | SFBmodtype mtb -> SFBmodtype (subst_module sub mtb) + in + List.map (fun (l,b) -> (l,subst_body b)) struc + +and subst_module sub mb = + { mb with + mod_mp = subst_mp sub mb.mod_mp; + mod_expr = + implem_map (subst_signature sub) (subst_expression sub) mb.mod_expr; + mod_type = subst_signature sub mb.mod_type; + mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg } |