[r2004-12-30 18:01:43 by afrisch] Explain

Original author: afrisch
Date: 2004-12-30 18:01:55+00:00

AUTHORS

+Main developer:
+  Alain Frisch
+
+Research project leaders, documentation:
+  Alain Frisch
+  Giuseppe Castagna
+  Vronique Benzaken
+
+Code contribution:
+  Cdric Miachon (CQL)
+  Julien Demouth (OCaml/CDuce interface)
+  Stefano Zacchiroli (XML Schema support)

compile/compile.ml

@@ -59,6 +59,7 @@ let find_ext cu x =
 let rec compile env tail e = compile_aux env tail e.Typed.exp_descr
 and compile_aux env tail = function
   | Typed.Forget (e,_) -> compile env tail e
+  | Typed.Check (e,t) -> Check (compile env false e, t)
   | Typed.Var x -> Var (find x env)
   | Typed.ExtVar (cu,x,_) -> Var (find_ext cu x)
   | Typed.Apply (e1,e2) -> Apply (tail, compile env false e1, compile env tail e2)

compile/lambda.ml

@@ -43,6 +43,7 @@ type expr =
   | Var of var_loc
   | Apply of bool * expr * expr
   | Abstraction of var_loc array * (Types.t * Types.t) list * branches
+  | Check of expr * Types.Node.t 
 
   | Const of Types.Const.t
   | Pair of expr * expr
@@ -214,6 +215,11 @@ module Put = struct
 	bits nbits s 20;
 	Ns.serialize_table s ns;
 	expr s e
+    | Check (e,t) ->
+	bits nbits s 21;
+	expr s e;
+	Types.Node.serialize s t
+	
 	  
   and branches s brs =
     list (pair Patterns.Node.serialize expr) s brs.brs;
@@ -330,6 +336,10 @@ module Get = struct
 	  let ns = Ns.deserialize_table s in
 	  let e = expr s in
 	  NsTable (ns,e)
+      | 21 ->
+	  let e = expr s in
+	  let t = Types.Node.deserialize s in
+	  Check (e,t)
       | _ -> assert false
 
   and branches s =

compile/lambda.mli

@@ -16,6 +16,7 @@ type expr =
   | Var of var_loc
   | Apply of bool * expr * expr
   | Abstraction of var_loc array * (Types.t * Types.t) list * branches
+  | Check of expr * Types.Node.t
 
   | Const of Types.Const.t
   | Pair of expr * expr

depend

@@ -188,14 +188,16 @@ runtime/print_xml.cmx: types/atoms.cmx misc/encodings.cmx types/ident.cmx \
     types/intervals.cmx parser/location.cmx misc/ns.cmx \
     schema/schema_builtin.cmx types/sequence.cmx runtime/value.cmx \
     runtime/print_xml.cmi 
-runtime/eval.cmo: types/ident.cmo compile/lambda.cmi misc/ns.cmi \
-    types/patterns.cmi runtime/run_dispatch.cmi schema/schema_common.cmi \
-    schema/schema_types.cmi schema/schema_validator.cmi typing/typer.cmi \
-    types/types.cmi runtime/value.cmi runtime/eval.cmi 
-runtime/eval.cmx: types/ident.cmx compile/lambda.cmx misc/ns.cmx \
-    types/patterns.cmx runtime/run_dispatch.cmx schema/schema_common.cmx \
-    schema/schema_types.cmx schema/schema_validator.cmx typing/typer.cmx \
-    types/types.cmx runtime/value.cmx runtime/eval.cmi 
+runtime/eval.cmo: runtime/explain.cmi types/ident.cmo compile/lambda.cmi \
+    misc/ns.cmi types/patterns.cmi runtime/run_dispatch.cmi \
+    schema/schema_common.cmi schema/schema_types.cmi \
+    schema/schema_validator.cmi typing/typer.cmi types/types.cmi \
+    runtime/value.cmi runtime/eval.cmi 
+runtime/eval.cmx: runtime/explain.cmx types/ident.cmx compile/lambda.cmx \
+    misc/ns.cmx types/patterns.cmx runtime/run_dispatch.cmx \
+    schema/schema_common.cmx schema/schema_types.cmx \
+    schema/schema_validator.cmx typing/typer.cmx types/types.cmx \
+    runtime/value.cmx runtime/eval.cmi 
 compile/compile.cmo: parser/ast.cmo runtime/eval.cmi types/ident.cmo \
     compile/lambda.cmi parser/location.cmi types/patterns.cmi \
     misc/serialize.cmi typing/typed.cmo typing/typer.cmi types/types.cmi \

driver/cduce.ml

@@ -204,10 +204,11 @@ let debug ppf tenv cenv = function
       let t = Typer.typ tenv t in
       (match Explain.explain (Types.descr t) (eval_quiet tenv cenv e) with
 	 | Some p ->
-	     Format.fprintf ppf "Explanation: @[%a@]@." 
+	     Format.fprintf ppf "Path: @[%a@]@.Explain: %a@."
 	       Explain.print_path p
+	       Explain.print p
 	 | None ->
-	     Format.fprintf ppf "Explanation: value has given type@.")
+	     Format.fprintf ppf "Value has given type@.")
   | `Single t ->
       Format.fprintf ppf "[DEBUG:single]@.";
       let t = Typer.typ tenv t in

parser/ast.ml

@@ -72,6 +72,7 @@ and pexpr =
   (* Other *)
   | NamespaceIn of U.t * Ns.t * pexpr
   | Forget of pexpr * ppat    
+  | Check of pexpr * ppat
 (*  | Op of string * pexpr list *)
   | Ref of pexpr * ppat
   | External of string * ppat list

parser/parser.ml

@@ -236,6 +236,8 @@ EXTEND
 	exp loc (NamespaceIn (name, ns, e2))
     | e = expr; ":"; p = pat ->
 	exp loc (Forget (e,p))
+    | e = expr; ":"; "?"; p = pat ->
+	exp loc (Check (e,p))
     | e1 = expr; ";"; e2 = expr ->
 	exp loc (Match (e1, [pat_nil,e2]))
     | "ref"; p = pat; e = expr ->

runtime/eval.ml

@@ -144,7 +144,18 @@ let rec eval env = function
   | OpResolved (f,args) ->
       (Obj.magic f) (List.map (eval env) args)
   | NsTable (ns,e) -> ns_table := ns; eval env e
-      
+  | Check (e,t) -> eval_check env e t
+
+and eval_check env e t =
+  let v = eval env e in
+  match Explain.explain (Types.descr t) v with
+    | None -> v
+    | Some p -> 
+	let b = Buffer.create 1024 in
+	let ppf = Format.formatter_of_buffer b in
+	Explain.print ppf p;
+	let s = Buffer.contents b in
+	raise (CDuceExn (string_latin1 s))
 
 and eval_abstraction env slots iface body =
   let local_env = Array.map (eval_var env) slots in

runtime/explain.ml

@@ -4,17 +4,51 @@ open Patterns.Compile
 open Encodings
 
 
-type path = Left of path | Right of path | Label of label * path | Root
-
-let rec print_path ppf = function
-  | Left p -> print_path ppf p; Format.fprintf ppf "L"
-  | Right p -> print_path ppf p; Format.fprintf ppf "R"
-  | Label (l,p) -> print_path ppf p; Format.fprintf ppf "(lab:%s)" (Label.to_string (LabelPool.value l))
-  | Root -> Format.fprintf ppf "*"
+type rdir = RLeft of path | RRight of path | RLabel of label * path | RRoot
+and path = Value.t * Types.t * rdir
+
+let rec print_path ppf (v,t,pt) = match pt with
+  | RLeft p -> print_path ppf p; Format.fprintf ppf "L"
+  | RRight p -> print_path ppf p; Format.fprintf ppf "R"
+  | RLabel (l,p) -> print_path ppf p; Format.fprintf ppf "(lab:%s)" (Label.to_string (LabelPool.value l))
+  | RRoot -> Format.fprintf ppf "*"
   
+let rec print ppf = function
+  | Absent, t, (RLabel (l,p)) ->
+      print ppf p;
+      Format.fprintf ppf "Label @[%a@] is missing@."
+	Label.print (LabelPool.value l)
+  | v, t, p ->
+      print_xmlelt ppf p;
+      Format.fprintf ppf 
+	"Value @[%a@] does not match type @[%a@]@."
+	Value.print v
+	Types.Print.print t;
+
+and print_xmlelt ppf = function
+  | RLeft p | RRight p | RLabel (_,p) -> 
+      (match p with
+	 | Xml _ as v, t, p ->
+	     print_xmlelt ppf p;
+	     Format.fprintf ppf 
+	       "Value @[%a@] does not match type @[%a@]@."
+	       Value.print v
+	       Types.Print.print t
+	 | _, _, p -> ()
+(* 	     print_xmlelt ppf p *)
+      )
+  | _ -> ()
+
+
 
 exception Path of path
 
+let expected d fail =
+  let ts = types_of_codes d in
+  let a = ref Types.empty in
+  Array.iteri (fun i t -> if i != fail then a := Types.cup t !a) ts;
+  !a
+
 let make_result pt fail (code,_) =
   if fail == code then raise (Path pt);
   code
@@ -42,12 +76,15 @@ let new_fail_disp fail =
 let rec run_dispatcher pt fail d v = 
   match actions d with
     | AIgnore r -> make_result pt fail r
-    | AKind k -> run_disp_kind pt fail k v
+    | AKind k -> run_disp_kind pt d fail k v
+
+and run_disp pt fail d v =
+  run_dispatcher (v, expected d fail, pt) fail d v
 
-and run_disp_kind pt fail actions = function
-  | Pair (v1,v2) -> run_disp_prod pt fail v1 v2 actions.prod
-  | Xml (v1,v2,v3) -> run_disp_prod pt fail v1 (Pair(v2,v3)) actions.xml
-  | Record r -> run_disp_record pt fail false (LabelMap.get r) actions.record
+and run_disp_kind pt d fail actions = function
+  | Pair (v1,v2) -> run_disp_prod pt d fail v1 v2 actions.prod
+  | Xml (v1,v2,v3) -> run_disp_prod pt d fail v1 (Pair(v2,v3)) actions.xml
+  | Record r -> run_disp_record pt d fail false (LabelMap.get r) actions.record
   | Atom a -> make_result pt fail (Atoms.get_map a actions.atoms) 
   | Char c -> make_result pt fail (Chars.get_map c actions.chars) 
   | Integer i ->
@@ -59,34 +96,34 @@ and run_disp_kind pt fail actions = function
   | Absent ->
       run_disp_basic pt fail (fun t -> Types.Record.has_absent t) actions.basic
   | v ->
-      run_disp_kind pt fail actions (normalize v)
+      run_disp_kind pt d fail actions (normalize v)
 
 
-and run_disp_prod pt fail v1 v2 = function
+and run_disp_prod pt d fail v1 v2 = function
   | Impossible -> assert false
-  | TailCall d1 -> run_dispatcher (Left pt) fail d1 v1
-  | Ignore d2 -> run_disp_prod2 pt fail v2 d2
+  | TailCall d1 -> run_disp (RLeft pt) fail d1 v1
+  | Ignore d2 -> run_disp_prod2 pt d fail v2 d2
   | Dispatch (d1,b1) ->
-      let code1 = run_dispatcher (Left pt) (new_fail_disp fail b1) d1 v1 in
-      run_disp_prod2 pt fail v2 b1.(code1)
+      let code1 = run_disp (RLeft pt) (new_fail_disp fail b1) d1 v1 in
+      run_disp_prod2 pt d fail v2 b1.(code1)
 
-and run_disp_prod2 pt fail v2 = function
+and run_disp_prod2 pt (d:dispatcher) fail v2 = function
   | Impossible -> assert false
   | Ignore r -> make_result pt fail r
-  | TailCall d2 -> run_dispatcher (Right pt) fail d2 v2
+  | TailCall d2 -> run_disp (RRight pt) fail d2 v2
   | Dispatch (d2,b2) ->
-      let code2 = run_dispatcher (Right pt) (new_fail_res fail b2) d2 v2 in
+      let code2 = run_disp (RRight pt) (new_fail_res fail b2) d2 v2 in
       make_result pt fail b2.(code2)
 
-and run_disp_record pt fail other fields = function
+and run_disp_record pt (d:dispatcher) fail other fields = function
   | None -> assert false
-  | Some (RecLabel (l,d)) ->
+  | Some (RecLabel (l,r)) ->
       let rec aux other = function
 	| (l1,_) :: rem when l1 < l -> aux true rem
 	| (l1,vl) :: rem when l1 == l ->
-	    run_disp_record1 pt fail l other vl rem d
+	    run_disp_record1 pt d fail l other vl rem r
 	| rem -> 
-	    run_disp_record1 pt fail l other Absent rem d
+	    run_disp_record1 pt d fail l other Absent rem r
       in
       aux other fields
   | Some (RecNolabel (some,none)) ->
@@ -96,15 +133,15 @@ and run_disp_record pt fail other fields = function
 	| Some r -> make_result pt fail r
 	| None -> assert false
       
-and run_disp_record1 pt fail l other v1 rem = function
+and run_disp_record1 pt (d:dispatcher) fail l other v1 rem = function
   | Impossible -> assert false
-  | TailCall d1 -> run_dispatcher (Label (l,pt)) fail d1 v1
-  | Ignore d2 ->  run_disp_record2 pt fail other rem d2
+  | TailCall d1 -> run_disp (RLabel (l,pt)) fail d1 v1
+  | Ignore d2 ->  run_disp_record2 pt d fail other rem d2
   | Dispatch (d1,b1) ->
-      let code1 = run_dispatcher pt (new_fail_disp fail b1) d1 v1 in
-      run_disp_record2 pt fail other rem b1.(code1)
+      let code1 = run_disp (RLabel (l,pt)) (new_fail_disp fail b1) d1 v1 in
+      run_disp_record2 pt d fail other rem b1.(code1)
 
-and run_disp_record2 pt fail other rem = function
+and run_disp_record2 pt (d:dispatcher) fail other rem = function
   | Impossible -> assert false
   | Ignore r -> make_result pt fail r
   | TailCall d2 -> run_disp_record_loop pt fail other rem d2
@@ -115,7 +152,7 @@ and run_disp_record2 pt fail other rem = function
 and run_disp_record_loop pt fail other rem d =
   match actions d with
     | AIgnore r -> make_result pt fail r
-    | AKind k -> run_disp_record pt fail other rem k.record
+    | AKind k -> run_disp_record pt d fail other rem k.record
   
 let explain t v =
   let p = Patterns.make IdSet.empty in
@@ -123,7 +160,15 @@ let explain t v =
   let (d,rhs) = make_branches Types.any [ (p,()) ] in
   let fail = find_array (function Fail -> true | _ -> false) rhs in
   try 
-    ignore (run_dispatcher Root fail d v);
+    ignore (run_disp RRoot fail d v);
     None
   with Path p -> Some p
 
+
+(*
+let explanation ppf p t v =
+  match p,v with
+    | RLabel (l,p), Absent ->
+	Format.fprintf ppf 
+	  "Superfluous field In record @[%a@], field @[%a@] "
+*)

runtime/explain.mli

 type path
 
 val print_path: Format.formatter -> path -> unit
+val print: Format.formatter -> path -> unit
 
 val explain: Types.t -> Value.t -> path option
   (** [explain v t] 

types/patterns.ml

@@ -992,6 +992,8 @@ struct
     mutable printed : bool
   }
 
+  let types_of_codes d = Array.map (fun (t,ar,_) -> t) d.codes
+
   let equal_array f a1 a2 =
     let rec aux i = (i < 0) || ((f a1.(i) a2.(i)) && (aux (i - 1))) in
     let l1 = Array.length a1 and l2 = Array.length a2 in

types/patterns.mli

@@ -69,6 +69,8 @@ module Compile: sig
 
   val actions: dispatcher -> actions
 
+  val types_of_codes: dispatcher -> Types.t array
+
   type 'a rhs = Match of (id * int) list * 'a | Fail
       (* ids are listed in the same order as returned by fv_list,
 	 not fv ! *)

typing/typed.ml

@@ -23,6 +23,7 @@ type texpr  =
     }
 and  texpr' = 
   | Forget of texpr * ttyp
+  | Check of texpr * ttyp
   (* CDuce is a Lambda-calculus ... *)
   | Var of id
   | ExtVar of Types.CompUnit.t * id * Types.t
@@ -46,6 +47,7 @@ and  texpr' =
   | RemoveField of texpr * label
   | Dot of texpr * label
       
+
   (* Exception *)
   | Try of texpr * branches
 

typing/typer.ml

@@ -948,6 +948,9 @@ let rec expr env loc = function
   | Forget (e,t) ->
       let (fv,e) = expr env loc e and t = typ env t in
       exp loc fv (Typed.Forget (e,t))
+  | Check (e,t) ->
+      let (fv,e) = expr env loc e and t = typ env t in
+      exp loc fv (Typed.Check (e,t))
   | Var s -> var env loc s
   | Apply (e1,e2) -> 
       let (fv1,e1) = expr env loc e1 and (fv2,e2) = expr env loc e2 in
@@ -1184,6 +1187,10 @@ and type_check' loc env e constr precise = match e with
       ignore (type_check env e t false);
       verify loc t constr
 
+  | Check (e,t) ->
+      ignore (type_check env e Types.any false);
+      verify loc (Types.descr t) constr
+
   | Abstraction a ->
       let t =
 	try Types.Arrow.check_strenghten a.fun_typ constr 

web/download.xml

@@ -4,6 +4,7 @@
 <title>Download</title>
 
 <box title="Sources tarballs" link="src">
+<box/>
 
 <p>
 The latest available version for download is the 0.2.1 release. We

web/site.cd

@@ -529,7 +529,15 @@ let gen_page_seq
 
 ;;
 
-match load_include input with
+
+let input_xml = load_include input;;
+
+match input_xml with
  | [ <site>[ <title>(site & String) (p & Page) ] ] -> 
    let _ = gen_page (site,[],p,[], [], compute_sitemap p) in []
- | _ -> raise ("Invalid input document " @ input)
+ | _ -> 
+   let _ = 
+     try (input_xml :? [ Site ])
+     with (err & Latin1) -> print ['Invalid input document\n' !err '\n']
+   in []
+