diff options
| -rw-r--r-- | checker/check.ml | 4 | ||||
| -rw-r--r-- | checker/check.mllib | 3 | ||||
| -rw-r--r-- | checker/cic.mli | 18 | ||||
| -rw-r--r-- | checker/declarations.ml | 99 | ||||
| -rw-r--r-- | checker/declarations.mli | 5 | ||||
| -rw-r--r-- | checker/safe_typing.ml | 41 | ||||
| -rw-r--r-- | checker/safe_typing.mli | 3 | ||||
| -rw-r--r-- | checker/term.ml | 50 | ||||
| -rw-r--r-- | checker/term.mli | 7 | ||||
| -rw-r--r-- | checker/validate.ml | 155 | ||||
| -rw-r--r-- | checker/values.ml | 280 |
11 files changed, 354 insertions, 311 deletions
diff --git a/checker/check.ml b/checker/check.ml index 7ac15393a..db2c537aa 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -40,7 +40,7 @@ type compilation_unit_name = DirPath.t type library_disk = { md_name : compilation_unit_name; - md_compiled : Safe_typing.compiled_library; + md_compiled : Cic.compiled_library; md_objects : library_objects; md_deps : (compilation_unit_name * Digest.t) array; md_imports : compilation_unit_name array } @@ -55,7 +55,7 @@ type library_disk = { type library_t = { library_name : compilation_unit_name; library_filename : CUnix.physical_path; - library_compiled : Safe_typing.compiled_library; + library_compiled : Cic.compiled_library; library_opaques : Cic.constr array; library_deps : (compilation_unit_name * Digest.t) array; library_digest : Digest.t } diff --git a/checker/check.mllib b/checker/check.mllib index 04c31103f..e327e275e 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -27,7 +27,6 @@ Rtree Names Univ Esubst -Validate Term Declarations Environ @@ -40,6 +39,8 @@ Typeops Indtypes Subtyping Mod_checking +Values +Validate Safe_typing Check Check_stat diff --git a/checker/cic.mli b/checker/cic.mli index 5c1345ba0..e72563c7d 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -21,7 +21,7 @@ The following types are also described in a reified manner in values.ml, for validating the layout of structures after de-marshalling. So: - IF YOU ADAPT THIS FILE, PLEASE MODIFY ACCORDINGLY values.ml ! + IF YOU ADAPT THIS FILE, YOU SHOULD MODIFY values.ml ACCORDINGLY ! *) open Names @@ -329,3 +329,19 @@ and module_type_body = typ_constraints : Univ.constraints; (** quotiented set of equivalent constant and inductive name *) typ_delta : delta_resolver} + + +(*************************************************************************) +(** {4 From safe_typing.ml} *) + +type nativecode_symb_array + +type library_info = DirPath.t * Digest.t + +type compiled_library = { + comp_name : DirPath.t; + comp_mod : module_body; + comp_deps : library_info array; + comp_enga : engagement option; + comp_natsymbs : nativecode_symb_array +} 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) diff --git a/checker/declarations.mli b/checker/declarations.mli index af38ab0fb..64234e8cd 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -43,8 +43,3 @@ val subst_structure : substitution -> structure_body -> structure_body val subst_module : substitution -> module_body -> module_body val join : substitution -> substitution -> substitution - -(* Validation *) -val val_eng : Validate.func -val val_module : Validate.func -val val_modtype : Validate.func diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 2ccaad3e9..7c96fda5b 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -60,19 +60,7 @@ let check_imports f caller env needed = in Array.iter check needed -type nativecode_symb_array - -type compiled_library = - DirPath.t * - module_body * - (DirPath.t * Digest.t) array * - engagement option * - nativecode_symb_array - open Validate -let val_deps = val_array (val_tuple ~name:"dep"[|val_dp;no_val|]) -let val_vo = val_tuple ~name:"vo" - [|val_dp;val_module;val_deps;val_opt val_eng; no_val|] (* This function should append a certificate to the .vo file. The digest must be part of the certicate to rule out attackers @@ -83,25 +71,22 @@ let stamp_library file digest = () (* When the module is checked, digests do not need to match, but a warning is issued in case of mismatch *) -let import file (dp,mb,depends,engmt,_ as vo) table digest = - Validate.apply !Flags.debug val_vo vo; - Validate.apply !Flags.debug (val_array Term.val_constr) table; +let import file clib table digest = + Validate.validate !Flags.debug Values.v_compiled_lib clib; + Validate.validate !Flags.debug (Values.Array Values.v_constr) table; Flags.if_verbose ppnl (str "*** vo structure validated ***"); pp_flush (); let env = !genv in - check_imports msg_warning dp env depends; - check_engagement env engmt; - Mod_checking.check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb; + check_imports msg_warning clib.comp_name env clib.comp_deps; + check_engagement env clib.comp_enga; + let mb = clib.comp_mod in + Mod_checking.check_module + (add_constraints mb.mod_constraints env) mb.mod_mp mb; stamp_library file digest; - (* We drop proofs once checked *) -(* let mb = lighten_module mb in*) - full_add_module dp mb digest + full_add_module clib.comp_name mb digest (* When the module is admitted, digests *must* match *) -let unsafe_import file (dp,mb,depends,engmt,_ as vo) digest = - if !Flags.debug then ignore vo; (*Validate.apply !Flags.debug val_vo vo;*) +let unsafe_import file clib digest = let env = !genv in - check_imports (errorlabstrm"unsafe_import") dp env depends; - check_engagement env engmt; - (* We drop proofs once checked *) -(* let mb = lighten_module mb in*) - full_add_module dp mb digest + check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps; + check_engagement env clib.comp_enga; + full_add_module clib.comp_name clib.comp_mod digest diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli index 6a7708971..cef93ad05 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -14,9 +14,6 @@ open Environ val get_env : unit -> env -(* exporting and importing modules *) -type compiled_library - val set_engagement : engagement -> unit val import : CUnix.physical_path -> compiled_library -> constr array -> Digest.t -> unit diff --git a/checker/term.ml b/checker/term.ml index 937b27ca0..b52f08cfa 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -13,15 +13,9 @@ open Util open Names open Univ open Esubst -open Validate open Cic -let val_ci = - let val_cstyle = val_enum "case_style" 5 in - let val_cprint = val_tuple ~name:"case_printing" [|val_int;val_cstyle|] in - val_tuple ~name:"case_info" [|val_ind;val_int;val_array val_int;val_cprint|] - (* Sorts. *) let family_of_sort = function @@ -29,47 +23,10 @@ let family_of_sort = function | Prop Pos -> InSet | Type _ -> InType -let val_sort = val_sum "sort" 0 [|[|val_enum "cnt" 2|];[|val_univ|]|] -let val_sortfam = val_enum "sorts_family" 3 - (********************************************************************) (* Constructions as implemented *) (********************************************************************) -let val_evar f = val_tuple ~name:"pexistential" [|val_int;val_array f|] -let val_prec f = - val_tuple ~name:"prec_declaration" - [|val_array val_name; val_array f; val_array f|] -let val_fix f = - val_tuple ~name:"pfixpoint" - [|val_tuple~name:"fix2"[|val_array val_int;val_int|];val_prec f|] -let val_cofix f = val_tuple ~name:"pcofixpoint"[|val_int;val_prec f|] - -let val_cast = val_enum "cast_kind" 3 - -(*s*******************************************************************) -(* The type of constructions *) - -let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [| - [|val_int|]; (* Rel *) - [|val_id|]; (* Var *) - [|val_int|]; (* Meta *) - [|val_evar val_constr|]; (* Evar *) - [|val_sort|]; (* Sort *) - [|val_constr;val_cast;val_constr|]; (* Cast *) - [|val_name;val_constr;val_constr|]; (* Prod *) - [|val_name;val_constr;val_constr|]; (* Lambda *) - [|val_name;val_constr;val_constr;val_constr|]; (* LetIn *) - [|val_constr;val_array val_constr|]; (* App *) - [|val_con|]; (* Const *) - [|val_ind|]; (* Ind *) - [|val_cstr|]; (* Construct *) - [|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *) - [|val_fix val_constr|]; (* Fix *) - [|val_cofix val_constr|] (* CoFix *) -|]) - - let rec strip_outer_cast c = match c with | Cast (c,_,_) -> strip_outer_cast c | _ -> c @@ -252,13 +209,6 @@ let subst1 lam = substl [lam] (* Type of assumptions and contexts *) (***************************************************************************) -let val_ndecl = - val_tuple ~name:"named_declaration"[|val_id;val_opt val_constr;val_constr|] -let val_rdecl = - val_tuple ~name:"rel_declaration"[|val_name;val_opt val_constr;val_constr|] -let val_nctxt = val_list val_ndecl -let val_rctxt = val_list val_rdecl - let empty_named_context = [] let fold_named_context f l ~init = List.fold_right f l init diff --git a/checker/term.mli b/checker/term.mli index 4993e0718..127fc113d 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -55,10 +55,3 @@ val destArity : constr -> arity val isArity : constr -> bool val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool val eq_constr : constr -> constr -> bool - -(* Validation *) -val val_sortfam : Validate.func -val val_sort : Validate.func -val val_constr : Validate.func -val val_rctxt : Validate.func -val val_nctxt : Validate.func diff --git a/checker/validate.ml b/checker/validate.ml index 649b2cdd6..4c5ca184e 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -39,29 +39,12 @@ let pr_obj o = pr_obj_rec o; Format.print_newline() type error_context = string list let mt_ec : error_context = [] let (/) (ctx:error_context) s : error_context = s::ctx -let overr (ctx:error_context) f = (fun (_:error_context) -> f ctx) -let ext s f (ctx:error_context) = f (ctx/s) - exception ValidObjError of string * error_context * Obj.t let fail ctx o s = raise (ValidObjError(s,ctx,o)) type func = error_context -> Obj.t -> unit -let apply debug f x = - let o = Obj.repr x in - try f mt_ec o - with ValidObjError(msg,ctx,obj) -> - if debug then begin - print_endline ("Validation failed: "^msg); - print_endline ("Context: "^String.concat"/"(List.rev ctx)); - pr_obj obj - end; - failwith "vo structure validation failed" - -(* data not validated *) -let no_val (c:error_context) (o:Obj.t) = () - (* Check that object o is a block with tag t *) let val_tag t ctx o = if Obj.is_block o && Obj.tag o = t then () @@ -73,30 +56,46 @@ let val_block ctx o = fail ctx o "block: found no scan tag") else fail ctx o "expected block obj" -(* Check that an object is a tuple (or a record). v is an array of - validation functions for each field. Its size corresponds to the +open Values + +let rec val_gen v ctx o = match v with + | Tuple (name,vs) -> val_tuple ~name vs ctx o + | Sum (name,cc,vv) -> val_sum name cc vv ctx o + | Array v -> val_array v ctx o + | List v0 -> val_sum "list" 1 [|[|Annot ("elem",v0);v|]|] ctx o + | Opt v -> val_sum "option" 1 [|[|v|]|] ctx o + | Int -> if not (Obj.is_int o) then fail ctx o "expected an int" + | String -> + (try val_tag Obj.string_tag ctx o + with Failure _ -> fail ctx o "expected a string") + | Any -> () + | Annot (s,v) -> val_gen v (ctx/s) o + +(* Check that an object is a tuple (or a record). vs is an array of + value representation for each field. Its size corresponds to the expected size of the object. *) -let val_tuple ?name v ctx o = +and val_tuple ?name vs ctx o = let ctx = match name with - Some n -> ctx/n - | _ -> ctx in - let n = Array.length v in - let val_fld i f = - f (ctx/("fld="^string_of_int i)) (Obj.field o i) in + | Some n -> ctx/n + | _ -> ctx + in + let n = Array.length vs in + let val_fld i v = + val_gen v (ctx/("fld="^string_of_int i)) (Obj.field o i) in val_block ctx o; - if Obj.size o = n then Array.iteri val_fld v + if Obj.size o = n then Array.iteri val_fld vs else fail ctx o ("tuple size: found "^string_of_int (Obj.size o)^ - ", expected "^string_of_int n) + ", expected "^string_of_int n) (* Check that the object is either a constant constructor of tag < cc, or a constructed variant. each element of vv is an array of - validation functions to be applied to the constructor arguments. + value representations of the constructor arguments. The size of vv corresponds to the number of non-constant constructors, and the size of vv.(i) is the expected arity of the i-th non-constant constructor. *) -let val_sum name cc vv ctx o = +and val_sum name cc vv ctx o = let ctx = ctx/name in if Obj.is_block o then (val_block (ctx/name) o; @@ -111,94 +110,20 @@ let val_sum name cc vv ctx o = fail ctx o ("bad constant constructor "^string_of_int n)) else fail ctx o "not a sum" -let val_enum s n = val_sum s n [||] - -(* Recursive types: avoid looping by eta-expansion *) -let rec val_rec_sum name cc f ctx o = - val_sum name cc (f (overr (ctx/name) (val_rec_sum name cc f))) ctx o - -(**************************************************************************) -(* Builtin types *) - (* Check the o is an array of values satisfying f. *) -let val_array ?(pos=false) f ctx o = - let upd_ctx = - if pos then (fun i -> ctx/string_of_int i) else (fun _ -> ctx) in +and val_array v ctx o = val_block (ctx/"array") o; for i = 0 to Obj.size o - 1 do - (f (upd_ctx i) (Obj.field o i):unit) + val_gen v ctx (Obj.field o i) done -(* Integer validator *) -let val_int ctx o = - if not (Obj.is_int o) then fail ctx o "expected an int" - -(* String validator *) -let val_str ctx o = - try val_tag Obj.string_tag ctx o - with Failure _ -> fail ctx o "expected a string" - -(* Booleans *) -let val_bool = val_enum "bool" 2 - -(* Option type *) -let val_opt ?(name="option") f = - val_sum name 1 [|[|f|]|] - -(* Lists *) -let val_list ?(name="list") f ctx = - val_rec_sum name 1 (fun vlist -> [|[|ext "elem" f;vlist|]|]) - ctx - -(* Reference *) -let val_ref ?(name="ref") f ctx = - val_tuple [|f|] (ctx/name) - -(**************************************************************************) -(* Standard library types *) - -(* Sets *) -let val_set ?(name="Set.t") f = - val_rec_sum name 1 - (fun vset -> [|[|vset;ext "elem" f; - vset;ext "bal" val_int|]|]) - -(* Maps *) -let val_map ?(name="Map.t") fk fv = - val_rec_sum name 1 - (fun vmap -> - [|[|vmap; ext "key" fk; ext "value" fv; - vmap; ext "bal" val_int|]|]) - -(**************************************************************************) -(* Coq types *) - -(* names *) -let val_id = val_str - -let val_dp = val_list ~name:"dirpath" val_id - -let val_name = val_sum "name" 1 [|[|val_id|]|] - -let val_uid = val_tuple ~name:"uniq_ident" [|val_int;val_str;val_dp|] - -let val_mp = - val_rec_sum "module_path" 0 - (fun vmp -> [|[|val_dp|];[|val_uid|];[|vmp;val_id|]|]) - -let val_kn = val_tuple ~name:"kernel_name" [|val_mp;val_dp;val_id|] - -let val_con = val_sum "constant/mutind" 0 [|[|val_kn|];[|val_kn;val_kn|]|] - -let val_ind = val_tuple ~name:"inductive"[|val_con;val_int|] -let val_cstr = val_tuple ~name:"constructor"[|val_ind;val_int|] - -(* univ *) -let val_level = val_sum "level" 1 [|[|val_int;val_dp|]|] -let val_univ = val_sum "univ" 0 - [|[|val_level|];[|val_list val_level;val_list val_level|]|] - -let val_cstrs = - val_set ~name:"Univ.constraints" - (val_tuple ~name:"univ_constraint" - [|val_level;val_enum "order_request" 3;val_level|]) +let validate debug v x = + let o = Obj.repr x in + try val_gen v mt_ec o + with ValidObjError(msg,ctx,obj) -> + if debug then begin + print_endline ("Validation failed: "^msg); + print_endline ("Context: "^String.concat"/"(List.rev ctx)); + pr_obj obj + end; + failwith "vo structure validation failed" diff --git a/checker/values.ml b/checker/values.ml new file mode 100644 index 000000000..2e096e2a4 --- /dev/null +++ b/checker/values.ml @@ -0,0 +1,280 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Abstract representations of values in a vo *) + +(** NB: UPDATE THIS FILE EACH TIME cic.mli IS MODIFIED ! *) + +(** We reify here the types of values present in a vo (see cic.mli), + in order to validate its structure. Maybe this reification + could become automatically generated someday ? + + - [Any] stands for a value that we won't check, + - [Tuple] provides a name and sub-values in this block + - [Sum] provides a name, a number of constant constructors, + and sub-values at each position of each possible constructed + variant + - [List] and [Opt] could have been defined via [Sum], but + having them here helps defining some recursive values below + - [Annot] is a no-op, just there for improving debug messages *) + +type value = + | Any + | Tuple of string * value array + | Sum of string * int * value array array + | Array of value + | List of value + | Opt of value + | Int + | String + | Annot of string * value + +(** Some pseudo-constructors *) + +let v_tuple name v = Tuple(name,v) +let v_sum name cc vv = Sum(name,cc,vv) +let v_enum name n = Sum(name,n,[||]) + +(** Ocaml standard library *) + +let v_bool = v_enum "bool" 2 +let v_ref v = v_tuple "ref" [|v|] + +let v_set v = + let rec s = Sum ("Set.t",1, + [|[|s; Annot("elem",v); s; Annot("bal",Int)|]|]) + in s + +let v_map vk vd = + let rec m = Sum ("Map.t",1, + [|[|m; Annot("key",vk); Annot("data",vd); m; Annot("bal",Int)|]|]) + in m + + +(** kernel/names *) + +let v_id = String +let v_dp = Annot ("dirpath", List v_id) +let v_name = v_sum "name" 1 [|[|v_id|]|] +let v_uid = v_tuple "uniq_ident" [|Int;String;v_dp|] +let rec v_mp = Sum("module_path",0, + [|[|v_dp|]; + [|v_uid|]; + [|v_mp;v_id|]|]) +let v_kn = v_tuple "kernel_name" [|v_mp;v_dp;v_id|] +let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|] +let v_ind = v_tuple "inductive" [|v_cst;Int|] +let v_cons = v_tuple "constructor" [|v_ind;Int|] + + +(** kernel/univ *) + +let v_level = v_sum "level" 1 [|[|Int;v_dp|]|] +let v_univ = v_sum "univ" 0 + [|[|v_level|]; + [|List v_level;List v_level|]|] + +let v_cstrs = + Annot + ("Univ.constraints", + v_set + (v_tuple "univ_constraint" + [|v_level;v_enum "order_request" 3;v_level|])) + + +(** kernel/term *) + +let v_sort = v_sum "sort" 0 [|[|v_enum "cnt" 2|];[|v_univ|]|] +let v_sortfam = v_enum "sorts_family" 3 + +let v_caseinfo = + let v_cstyle = v_enum "case_style" 5 in + let v_cprint = v_tuple "case_printing" [|Int;v_cstyle|] in + v_tuple "case_info" [|v_ind;Int;Array Int;v_cprint|] + +let v_cast = v_enum "cast_kind" 3 +(** NB : In fact there are 4 cast markers, but the last one + (REVERTcast) isn't supposed to appear in a vo *) + +let rec v_constr = + Sum ("constr",0,[| + [|Int|]; (* Rel *) + [|v_id|]; (* Var *) + [|Int|]; (* Meta *) + [|v_evar|]; (* Evar *) + [|v_sort|]; (* Sort *) + [|v_constr;v_cast;v_constr|]; (* Cast *) + [|v_name;v_constr;v_constr|]; (* Prod *) + [|v_name;v_constr;v_constr|]; (* Lambda *) + [|v_name;v_constr;v_constr;v_constr|]; (* LetIn *) + [|v_constr;Array v_constr|]; (* App *) + [|v_cst|]; (* Const *) + [|v_ind|]; (* Ind *) + [|v_cons|]; (* Construct *) + [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *) + [|v_fix|]; (* Fix *) + [|v_cofix|] (* CoFix *) + |]) + +and v_evar = Tuple ("pexistential",[|Int;Array v_constr|]) +and v_prec = Tuple ("prec_declaration", + [|Array v_name; Array v_constr; Array v_constr|]) +and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|]) +and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|]) + + +let v_ndecl = v_tuple "named_declaration" [|v_id;Opt v_constr;v_constr|] +let v_rdecl = v_tuple "rel_declaration" [|v_name;Opt v_constr;v_constr|] +let v_nctxt = List v_ndecl +let v_rctxt = List v_rdecl + + +(** kernel/mod_subst *) + +let v_delta_hint = + v_sum "delta_hint" 0 [|[|Int; Opt v_constr|];[|v_kn|]|] + +let v_resolver = + v_tuple "delta_resolver" + [|v_map v_mp v_mp; + v_map v_kn v_delta_hint|] + +let v_mp_resolver = v_tuple "" [|v_mp;v_resolver|] + +let v_subst = + v_tuple "substitution" + [|v_map v_mp v_mp_resolver; + v_map v_uid v_mp_resolver|] + + +(** kernel/lazyconstr *) + +let v_substituted v_a = + v_ref + (v_sum "constr_substituted" 0 + [|[|v_a|];[|List v_subst;v_a|]|]) + +let v_cstr_subst = v_substituted v_constr + +(** NB: Second constructor [Direct] isn't supposed to appear in a .vo *) +let v_lazy_constr = + v_sum "lazy_constr" 0 [|[|List v_subst;v_dp;Int|]|] + + +(** kernel/declarations *) + +let v_engagement = v_enum "eng" 1 + +let v_pol_arity = + v_tuple "polymorphic_arity" [|List(Opt v_univ);v_univ|] + +let v_cst_type = + v_sum "constant_type" 0 [|[|v_constr|];[|v_rctxt;v_pol_arity|]|] + +let v_cst_def = + v_sum "constant_def" 0 + [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] + +let v_cb = v_tuple "constant_body" + [|v_nctxt; + v_cst_def; + v_cst_type; + Any; + v_cstrs; + Any; + v_bool|] + +let v_recarg = v_sum "recarg" 1 (* Norec *) + [|[|v_ind|] (* Mrec *);[|v_ind|] (* Imbr *)|] + +let rec v_wfp = Sum ("wf_paths",0, + [|[|Int;Int|]; (* Rtree.Param *) + [|v_recarg;Array v_wfp|]; (* Rtree.Node *) + [|Int;Array v_wfp|] (* Rtree.Rec *) + |]) + +let v_mono_ind_arity = + v_tuple "monomorphic_inductive_arity" [|v_constr;v_sort|] + +let v_ind_arity = v_sum "inductive_arity" 0 + [|[|v_mono_ind_arity|];[|v_pol_arity|]|] + +let v_one_ind = v_tuple "one_inductive_body" + [|v_id; + v_rctxt; + v_ind_arity; + Array v_id; + Array v_constr; + Int; + Int; + List v_sortfam; + Array v_constr; + Array Int; + v_wfp; + Int; + Int; + Any|] + +let v_ind_pack = v_tuple "mutual_inductive_body" + [|Array v_one_ind; + v_bool; + v_bool; + Int; + v_nctxt; + Int; + Int; + v_rctxt; + v_cstrs; + Any|] + +let rec v_sfb = + Sum ("struct_field_body",0, + [|[|v_cb|]; (* SFBconst *) + [|v_ind_pack|]; (* SFBmind *) + [|v_module|]; (* SFBmodule *) + [|v_modtype|] (* SFBmodtype *) + |]) +and v_sb = List (Tuple ("label*sfb",[|v_id;v_sfb|])) +and v_seb = + Sum ("struct_expr_body",0, + [|[|v_mp|]; (* SEBident *) + [|v_uid;v_modtype;v_seb|]; (* SEBfunctor *) + [|v_seb;v_seb;v_cstrs|]; (* SEBapply *) + [|v_sb|]; (* SEBstruct *) + [|v_seb;v_with|] (* SEBwith *) + |]) +and v_with = + Sum ("with_declaration_body",0, + [|[|List v_id;v_mp|]; + [|List v_id;v_cb|]|]) +and v_module = + Tuple ("module_body", + [|v_mp;Opt v_seb;v_seb; + Opt v_seb;v_cstrs;v_resolver;Any|]) +and v_modtype = + Tuple ("module_type_body", + [|v_mp;v_seb;Opt v_seb;v_cstrs;v_resolver|]) + + +(** kernel/safe_typing *) + +let v_deps = Array (v_tuple "dep" [|v_dp;String|]) +let v_compiled_lib = + v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|] + +(** Library objects (unused by the checker) *) + +let v_obj = Tuple ("Dyn.t",[|String;Any|]) +let v_libobj = Tuple ("libobj", [|v_id;v_obj|]) +let v_libobjs = List v_libobj +let v_libraryobjs = Tuple ("library_objects",[|v_mp;v_libobjs;v_libobjs|]) + +(** Main structure of a vo (opaque tables left aside) *) + +let v_lib = + Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps; List v_dp|]) |