1 files changed, 71 insertions, 49 deletions

diff --git a/checker/validate.ml b/checker/validate.ml
index 7d368f05..c5e0bd34 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (* This module defines validation functions to ensure an imported
    value (using input_value) has the correct structure. *)
 
@@ -38,44 +36,59 @@ let pr_obj o = pr_obj_rec o; Format.print_newline()
 (**************************************************************************)
 (* Obj low-level validators *)
 
-exception ValidObjError of string * Obj.t
-let fail o s = raise (ValidObjError(s,o))
+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)
+
 
-let ep s1 f s2 = f (s1^"/"^s2) 
+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 o
-  with ValidObjError(msg,obj) ->
+  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 (o:Obj.t) = ()
+let no_val (c:error_context) (o:Obj.t) = ()
 
 (* Check that object o is a block with tag t *)
-let val_tag t o =
+let val_tag t ctx o =
   if Obj.is_block o && Obj.tag o = t then ()
-  else fail o ("expected tag "^string_of_int t)
+  else fail ctx o ("expected tag "^string_of_int t)
 
-let val_block s o =
+let val_block ctx o =
   if Obj.is_block o then
     (if Obj.tag o > Obj.no_scan_tag then
-      fail o (s^": found no scan tag"))
-  else fail o (s^": expected block obj")
+      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
    expected size of the object. *)
-let val_tuple s v o =
+let val_tuple ?name v ctx o =
+  let ctx = match name with
+      Some n -> ctx/n
+    | _ -> ctx in
   let n = Array.length v in
-  val_block ("tuple: "^s) o;
-  if Obj.size o = n then Array.iteri (fun i f -> f (Obj.field o i)) v
+  let val_fld i f =
+    f (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
   else
-    fail o ("tuple:" ^s^" size found:"^string_of_int (Obj.size o))
+    fail ctx o
+      ("tuple size: found "^string_of_int (Obj.size o)^
+	 ", 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
@@ -83,70 +96,79 @@ let val_tuple s v o =
    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 s cc vv o =
+let val_sum name cc vv ctx o =
+  let ctx = ctx/name in
   if Obj.is_block o then
-    (val_block s o;
+    (val_block (ctx/name) o;
     let n = Array.length vv in
     let i = Obj.tag o in
-    if i < n then val_tuple (s^"(tag "^string_of_int i^")") vv.(i) o
-    else fail o ("bad tag in (sum type) "^s^": found "^string_of_int i))
+    let ctx' = if n=1 then ctx else ctx/("tag="^string_of_int i) in
+    if i < n then val_tuple vv.(i) ctx' o
+    else fail ctx' o ("sum: unexpected tag"))
   else if Obj.is_int o then
     let (n:int) = Obj.magic o in
     (if n<0 || n>=cc then
-      fail o (s^": bad constant constructor "^string_of_int n))
-  else fail o ("not a sum ("^s^")")
+      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 s cc f o =
-  val_sum s cc (f (val_rec_sum s cc f)) o
-
-let rec val_rectype f o =
-  f (val_rectype f) o
+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 ?(name="array") f o =
-  val_block name o;
+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
+  val_block (ctx/"array") o;
   for i = 0 to Obj.size o - 1 do
-    (f (Obj.field o i):unit)
+    (f (upd_ctx i) (Obj.field o i):unit)
   done
 
 (* Integer validator *)
-let val_int o =
-  if not (Obj.is_int o) then fail o "expected an int"
+let val_int ctx o =
+  if not (Obj.is_int o) then fail ctx o "expected an int"
 
 (* String validator *)
-let val_str o =
-  try val_tag Obj.string_tag o
-  with Failure _ -> fail o "expected a string"
+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|]|]
+let val_opt ?(name="option") f =
+  val_sum name 1 [|[|f|]|]
 
 (* Lists *)
-let val_list ?(name="list") f =
-  val_rec_sum name 1 (fun vlist -> [|[|f;vlist|]|])
+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 = val_tuple name [|f|]
+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;f;vset;val_int|]|])
+  val_rec_sum name 1
+    (fun vset -> [|[|vset;ext "elem" f;
+		     vset;ext "bal" val_int|]|])
 
 (* Maps *)
 let rec val_map ?(name="Map.t") fk fv =
-  val_rec_sum name 1 (fun vmap -> [|[|vmap;fk;fv;vmap;val_int|]|])
+  val_rec_sum name 1
+    (fun vmap ->
+       [|[|vmap; ext "key" fk; ext "value" fv;
+	   vmap; ext "bal" val_int|]|])
 
 (**************************************************************************)
 (* Coq types *)
@@ -158,19 +180,19 @@ let val_dp = val_list ~name:"dirpath" val_id
 
 let val_name = val_sum "name" 1 [|[|val_id|]|]
 
-let val_uid = val_tuple "uniq_ident" [|val_int;val_str;val_dp|]
+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 "kernel_name" [|val_mp;val_dp;val_id|]
+let val_kn = val_tuple ~name:"kernel_name" [|val_mp;val_dp;val_id|]
 
 let val_con =
-  val_tuple "constant/mutind" [|val_kn;val_kn|]
+  val_tuple ~name:"constant/mutind" [|val_kn;val_kn|]
 
-let val_ind = val_tuple "inductive"[|val_con;val_int|]
-let val_cstr = val_tuple "constructor"[|val_ind;val_int|]
+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_dp;val_int|]|]
@@ -179,5 +201,5 @@ let val_univ = val_sum "univ" 0
 
 let val_cstrs =
   val_set ~name:"Univ.constraints"
-   (val_tuple "univ_constraint"
+   (val_tuple ~name:"univ_constraint"
      [|val_level;val_enum "order_request" 3;val_level|])