From 07c80f246315ac314c82d580bf356df3fb8201d8 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 15 Apr 2013 16:05:00 +0000 Subject: Checker: reified encoding of .vo types in values.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16399 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/declarations.ml | 99 ------------------------------------------------- 1 file changed, 99 deletions(-) (limited to 'checker/declarations.ml') diff --git a/checker/declarations.ml b/checker/declarations.ml index 42d49e83b..886901e1a 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -2,15 +2,6 @@ open Util open Names open Cic open Term -open Validate - -let val_eng = val_enum "eng" 1 - -let val_pol_arity = - val_tuple ~name:"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|] - -let val_cst_type = - val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|] (** Substitutions, code imported from kernel/mod_subst *) @@ -55,22 +46,6 @@ 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) @@ -297,11 +272,6 @@ let subst_mps sub c = if is_empty_subst sub then c else map_kn (subst_ind sub) (subst_con0 sub) c -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 = @@ -448,8 +418,6 @@ let force_constr = force subst_mps let from_val c = ref (LSval c) -let val_cstr_subst = val_substituted val_constr - let subst_constr_subst = subst_substituted let subst_lazy_constr sub = function @@ -463,13 +431,6 @@ let force_lazy_constr = function let c = !indirect_opaque_access dp i in force_constr (List.fold_right subst_constr_subst l (from_val c)) -let val_lazy_constr = - val_sum "lazy_constr" 0 [|[|val_list val_subst;val_dp;val_int|]|] - -let val_cst_def = - val_sum "constant_def" 0 - [|[|val_opt val_int|]; [|val_cstr_subst|]; [|val_lazy_constr|]|] - let subst_constant_def sub = function | Undef inl -> Undef inl | Def c -> Def (subst_constr_subst sub c) @@ -488,15 +449,6 @@ 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; - no_val; - val_bool|] - 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 @@ -504,21 +456,11 @@ let subst_rel_declaration sub (id,copt,t as x) = let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) -let val_recarg = val_sum "recarg" 1 (* Norec *) - [|[|val_ind|] (* Mrec *);[|val_ind|] (* Imbr *)|] - 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) -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 = @@ -541,22 +483,6 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn *) -let val_mono_ind_arity = - val_tuple ~name:"monomorphic_inductive_arity"[|val_constr;val_sort|] - -let val_ind_arity = val_sum "inductive_arity" 0 - [|[|val_mono_ind_arity|];[|val_pol_arity|]|] - -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|] - -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;no_val|] - - let subst_arity sub = function | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) @@ -609,31 +535,6 @@ let subst_mind sub mib = (* Modules *) -(* 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) -- cgit v1.2.3