From a0a94c1340a63cdb824507b973393882666ba52a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 19 Feb 2009 13:13:14 +0100
Subject: Imported Upstream version 8.2-1+dfsg

---
 checker/declarations.ml | 74 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 74 insertions(+)

(limited to 'checker/declarations.ml')

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 2cf3854a..c6a7b4b4 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -1,6 +1,7 @@
 open Util
 open Names
 open Term
+open Validate
 
 (* Bytecode *)
 type values
@@ -11,17 +12,22 @@ 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"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|]|]
 
 
 type substitution_domain = 
@@ -29,6 +35,9 @@ type substitution_domain =
   | MBI of mod_bound_id
   | MPI of module_path
 
+let val_subst_dom =
+  val_sum "substitution_domain" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|]
+
 module Umap = Map.Make(struct 
 			 type t = substitution_domain
 			 let compare = Pervasives.compare
@@ -39,6 +48,13 @@ type resolver
 type substitution = (module_path * resolver option) Umap.t
 type 'a subst_fun = substitution -> 'a -> 'a
 
+let val_res = val_opt no_val
+
+let val_subst =
+  val_map ~name:"substitution"
+    val_subst_dom (val_tuple "substition range" [|val_mp;val_res|])
+
+
 let fold_subst fs fb fp =
   Umap.fold
     (fun k (mp,_) acc ->
@@ -360,6 +376,11 @@ let force_constr = force subst_mps
 
 type constr_substituted = constr substituted
 
+let val_cstr_subst =
+  val_ref
+    (val_sum "constr_substituted" 0
+      [|[|val_constr|];[|val_subst;val_constr|]|])
+
 let subst_constr_subst = subst_substituted
 
 type constant_body = {
@@ -372,6 +393,11 @@ type constant_body = {
     const_opaque : bool; 
     const_inline : bool}
 
+let val_cb = val_tuple "constant_body"
+  [|val_nctxt;val_opt val_cstr_subst; val_cst_type;no_val;val_cstrs;
+    val_bool; 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
@@ -383,6 +409,8 @@ type recarg =
   | Norec 
   | Mrec of int 
   | Imbr of inductive
+let val_recarg = val_sum "recarg" 1 (* Norec *)
+  [|[|val_int|] (* Mrec *);[|val_ind|] (* Imbr *)|]
 
 let subst_recarg sub r = match r with
   | Norec | Mrec _  -> r
@@ -390,6 +418,12 @@ let subst_recarg sub r = match r with
       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 [||]
 
@@ -417,10 +451,14 @@ type monomorphic_inductive_arity = {
   mind_user_arity : constr;
   mind_sort : sorts;
 }
+let val_mono_ind_arity =
+  val_tuple"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 = {
 
@@ -471,6 +509,12 @@ type one_inductive_body = {
     mind_reloc_tbl :  reloc_table; 
   }
 
+let val_one_ind = val_tuple "one_inductive_body"
+  [|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr;
+    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 *)
@@ -503,6 +547,10 @@ type mutual_inductive_body = {
   (* Source of the inductive block when aliased in a module *)
     mind_equiv : kernel_name option
   }
+let val_ind_pack = val_tuple "mutual_inductive_body"
+  [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt;
+    val_int; val_int; val_rctxt;val_cstrs;val_opt val_kn|]
+
 
 let subst_arity sub = function
 | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
@@ -558,6 +606,8 @@ let subst_mind sub mib =
 
 (* 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
@@ -592,6 +642,30 @@ and module_type_body =
       typ_strength : module_path option;
       typ_alias : substitution}
 
+(* 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_mp;val_opt val_seb;val_opt val_cstrs|]; (* SFBalias *)
+    [|val_modtype|]   (* SFBmodtype *)
+  |] o
+and val_sb o = val_list (val_tuple"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_uid;val_sb|];              (* SEBstruct *)
+    [|val_seb;val_seb;val_cstrs|];   (* SEBapply *)
+    [|val_seb;val_with|]             (* SEBwith *)
+  |] o
+and val_with o = val_sum "with_declaration_body" 0
+  [|[|val_list val_id;val_mp;val_cstrs|];
+    [|val_list val_id;val_cb|]|] o
+and val_module o = val_tuple "module_body"
+  [|val_opt val_seb;val_opt val_seb;val_cstrs;val_subst;no_val|] o
+and val_modtype o = val_tuple "module_type_body"
+  [|val_seb;val_opt val_mp;val_subst|] o
+
 	
 let rec subst_with_body sub = function
   | With_module_body(id,mp,typ_opt,cst) ->
-- 
cgit v1.2.3