[r2005-01-03 10:16:00 by afrisch] Explain, exit

Original author: afrisch
Date: 2005-01-03 10:16:01+00:00

CHANGES

@@ -11,7 +11,11 @@ Since 0.2.1
 - better compilation of sequence capture variables
 - punning in record/attribute expressions and values ({ x; y } -> {x=x;y=y})
 - removed the warning "no caml interface"
-- add "system: Latin1->Latin1"
+- add "system: Latin1->Latin1", "exit: (0--255)->Empty" 
+- (e :? t) raises an exception when e doesn't have type t;
+  the exception is an explanation of why this is not the case.
+
+
 
 0.2.1
 

compile/compile.ml

@@ -59,7 +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.Check (t0,e,t) -> Check (!t0, 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,7 +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 
+  | Check of Types.t * expr * Types.Node.t 
 
   | Const of Types.Const.t
   | Pair of expr * expr
@@ -215,8 +215,9 @@ module Put = struct
 	bits nbits s 20;
 	Ns.serialize_table s ns;
 	expr s e
-    | Check (e,t) ->
+    | Check (t0,e,t) ->
 	bits nbits s 21;
+	Types.serialize s t0;
 	expr s e;
 	Types.Node.serialize s t
 	
@@ -337,9 +338,10 @@ module Get = struct
 	  let e = expr s in
 	  NsTable (ns,e)
       | 21 ->
+	  let t0 = Types.deserialize s in
 	  let e = expr s in
 	  let t = Types.Node.deserialize s in
-	  Check (e,t)
+	  Check (t0,e,t)
       | _ -> assert false
 
   and branches s =

compile/lambda.mli

@@ -16,7 +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
+  | Check of Types.t * expr * Types.Node.t
 
   | Const of Types.Const.t
   | Pair of expr * expr

depend

@@ -244,6 +244,10 @@ driver/cduce.cmx: parser/ast.cmx types/builtin.cmx types/builtin_defs.cmx \
     types/patterns.cmx types/sample.cmx schema/schema_common.cmx \
     misc/state.cmx typing/typer.cmx types/types.cmx parser/ulexer.cmx \
     runtime/value.cmx driver/cduce.cmi 
+runtime/system.cmo: types/builtin_defs.cmi parser/location.cmi \
+    compile/operators.cmi runtime/value.cmi 
+runtime/system.cmx: types/builtin_defs.cmx parser/location.cmx \
+    compile/operators.cmx runtime/value.cmx 
 ocamliface/mltypes.cmo: ocamliface/asttypes.cmo driver/config.cmi \
     types/ident.cmo driver/librarian.cmi parser/location.cmi types/types.cmi \
     ocamliface/mltypes.cmi 

driver/cduce.ml

@@ -199,13 +199,13 @@ let debug ppf tenv cenv = function
 (*
        Patterns.demo_compile ppf (Types.descr t) (List.map Patterns.descr pl)  
 *)
-  | `Explain (t,e) ->
+  | `Explain (t0,t,e) ->
       Format.fprintf ppf "[DEBUG:explain]@.";
-      let t = Typer.typ tenv t in
-      (match Explain.explain (Types.descr t) (eval_quiet tenv cenv e) with
+      let t = Types.descr (Typer.typ tenv t) in
+      let t0 = Types.descr (Typer.typ tenv t0) in
+      (match Explain.explain t0 t (eval_quiet tenv cenv e) with
 	 | Some p ->
-	     Format.fprintf ppf "Path: @[%a@]@.Explain: %a@."
-	       Explain.print_path p
+	     Format.fprintf ppf "%a@."
 	       Explain.print p
 	 | None ->
 	     Format.fprintf ppf "Value has given type@.")

parser/ast.ml

@@ -21,7 +21,7 @@ and debug_directive =
   | `Accept of ppat
   | `Compile of ppat * ppat list 
   | `Subtype of ppat * ppat
-  | `Explain of ppat * pexpr
+  | `Explain of ppat * ppat * pexpr
   | `Single of ppat
   | `Approx of ppat * ppat
   ]

parser/parser.ml

@@ -189,7 +189,7 @@ EXTEND
     | IDENT "compile"; t = pat; p = LIST1 pat -> `Compile (t,p)
     | IDENT "sample"; t = pat -> `Sample t
     | IDENT "subtype"; t1 = pat; t2 = pat -> `Subtype (t1,t2)
-    | IDENT "explain"; t = pat; e = expr -> `Explain (t,e)
+    | IDENT "explain"; t0 = pat; t = pat; e = expr -> `Explain (t0,t,e)
     | IDENT "single"; t = pat -> `Single t
     | IDENT "approx"; p = pat; t = pat -> `Approx (p,t)
     ]

runtime/eval.ml

@@ -9,6 +9,13 @@ let ops = Hashtbl.create 13
 let register_op = Hashtbl.add ops
 let eval_op = Hashtbl.find ops
 
+let print_to_string f x =
+  let b = Buffer.create 1024 in
+  let ppf = Format.formatter_of_buffer b in
+  f ppf x;
+  Buffer.contents b
+
+
 (* To write tail-recursive map-like iteration *)
 
 let make_accu () = Value.Pair(nil,Absent)
@@ -144,17 +151,14 @@ 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
+  | Check (t0,e,t) -> eval_check env t0 e t
 
-and eval_check env e t =
+and eval_check env t0 e t =
   let v = eval env e in
-  match Explain.explain (Types.descr t) v with
+  match Explain.explain t0 (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
+	let s = print_to_string Explain.print p in
 	raise (CDuceExn (string_latin1 s))
 
 and eval_abstraction env slots iface body =

runtime/explain.ml

@@ -4,44 +4,19 @@ open Patterns.Compile
 open Encodings
 
 
-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 "*"
-  
+type t = (Value.t * Types.t Lazy.t) list
+
 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;
+  | [] -> ()
+  | (v, t) :: l ->
+      print ppf l;
       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 *)
-      )
-  | _ -> ()
-
+	Types.Print.print (Lazy.force t);
 
 
-exception Path of path
+exception Path of t
 
 let expected d fail =
   let ts = types_of_codes d in
@@ -49,7 +24,7 @@ let expected d fail =
   Array.iteri (fun i t -> if i != fail then a := Types.cup t !a) ts;
   !a
 
-let make_result pt fail (code,_) =
+let make_result pt  fail (code,_) =
   if fail == code then raise (Path pt);
   code
 
@@ -79,7 +54,7 @@ let rec run_dispatcher pt fail d 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
+  run_dispatcher ((v, lazy (expected d fail))::pt) fail d v
 
 and run_disp_kind pt d fail actions = function
   | Pair (v1,v2) -> run_disp_prod pt d fail v1 v2 actions.prod
@@ -101,18 +76,18 @@ and run_disp_kind pt d fail actions = function
 
 and run_disp_prod pt d fail v1 v2 = function
   | Impossible -> assert false
-  | TailCall d1 -> run_disp (RLeft pt) fail d1 v1
+  | TailCall d1 -> run_disp pt fail d1 v1
   | Ignore d2 -> run_disp_prod2 pt d fail v2 d2
   | Dispatch (d1,b1) ->
-      let code1 = run_disp (RLeft pt) (new_fail_disp fail b1) d1 v1 in
+      let code1 = run_disp pt (new_fail_disp fail b1) d1 v1 in
       run_disp_prod2 pt d fail v2 b1.(code1)
 
 and run_disp_prod2 pt (d:dispatcher) fail v2 = function
   | Impossible -> assert false
   | Ignore r -> make_result pt fail r
-  | TailCall d2 -> run_disp (RRight pt) fail d2 v2
+  | TailCall d2 -> run_disp pt fail d2 v2
   | Dispatch (d2,b2) ->
-      let code2 = run_disp (RRight pt) (new_fail_res fail b2) d2 v2 in
+      let code2 = run_disp pt (new_fail_res fail b2) d2 v2 in
       make_result pt fail b2.(code2)
 
 and run_disp_record pt (d:dispatcher) fail other fields = function
@@ -135,10 +110,10 @@ and run_disp_record pt (d:dispatcher) fail other fields = function
       
 and run_disp_record1 pt (d:dispatcher) fail l other v1 rem = function
   | Impossible -> assert false
-  | TailCall d1 -> run_disp (RLabel (l,pt)) fail d1 v1
+  | TailCall d1 -> run_disp pt fail d1 v1
   | Ignore d2 ->  run_disp_record2 pt d fail other rem d2
   | Dispatch (d1,b1) ->
-      let code1 = run_disp (RLabel (l,pt)) (new_fail_disp fail b1) d1 v1 in
+      let code1 = run_disp pt (new_fail_disp fail b1) d1 v1 in
       run_disp_record2 pt d fail other rem b1.(code1)
 
 and run_disp_record2 pt (d:dispatcher) fail other rem = function
@@ -153,22 +128,28 @@ 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 d fail other rem k.record
-  
-let explain t v =
+
+let is_xml = function Xml _ -> true | _ -> false
+
+let rec prepare = function
+  | (Absent, _) :: l -> prepare l
+  | x :: l ->
+      (try
+	 let y = List.find (function (Xml _,_) -> true | _ -> false) l in
+	 [ x; y ]
+       with Not_found -> [ x ])
+  | [] -> assert false
+
+let explain t0 t v =
   let p = Patterns.make IdSet.empty in
   Patterns.define p (Patterns.constr t);
-  let (d,rhs) = make_branches Types.any [ (p,()) ] in
-  let fail = find_array (function Fail -> true | _ -> false) rhs in
-  try 
-    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@] "
-*)
+  let (d,rhs) = make_branches t0 [ (p,()) ] in
+  (* The instrumented dispatcher is slower, so we first try the normal
+     one. This is optimized for the case where the value matches. *)
+  let (code,_) = Run_dispatch.run_dispatcher d v in
+  (* let fail = find_array (function Fail -> true | _ -> false) rhs in *)
+  match rhs.(code) with
+    | Fail ->
+	(try ignore (run_disp [] code d v); assert false 
+	 with Path p -> Some (prepare p))
+    | _ -> None

runtime/explain.mli

-type path
+type t
 
-val print_path: Format.formatter -> path -> unit
-val print: Format.formatter -> path -> unit
+val print: Format.formatter -> t -> unit
 
-val explain: Types.t -> Value.t -> path option
-  (** [explain v t] 
+val explain: Types.t -> Types.t -> Value.t -> t option
+  (** [explain t0 t v] 
     Return a path on [v] that explains why [v] is not of type [t],
-    or [None] if [v] has type [t]
+    or [None] if [v] has type [t].
+    [v] is assumed to have type [t0].
   *)

runtime/system.ml

@@ -3,30 +3,36 @@ open Builtin_defs
 
 let len = 1024;;
 
-register_fun "system"
-  string_latin1 string_latin1
+let run_process s =
+  let ic = Unix.open_process_in s in
+  let b = Buffer.create (1024*10) in
+  let buf = String.create len in
+  let rec aux () =
+    let i = input ic buf 0 len in
+    if i = 0 then () else (Buffer.add_string b (String.sub buf 0 i); aux ())
+  in
+  aux ();
+  let s = Value.string_latin1 (Buffer.contents b) in
+  s, Unix.close_process_in ic
+
+
+
+let () = register_fun "system" string_latin1 string_latin1
   (fun v ->
      Location.protect_op "system";
-     let s = Value.get_string_latin1 v in
-     let ic = Unix.open_process_in s in
-     let b = Buffer.create (1024*10) in
-     let buf = String.create len in
-     let rec aux () =
-       let i = input ic buf 0 len in
-       if i = 0 then () else (Buffer.add_string b (String.sub buf 0 i); aux ())
-     in
-     aux ();
-     let s = Value.string_latin1 (Buffer.contents b) in
-     match Unix.close_process_in ic with
-       | Unix.WEXITED n ->
+     match run_process (Value.get_string_latin1 v) with
+       | s,Unix.WEXITED n ->
 	   if (n = 0) then s
 	   else
 	     Value.raise' 
 	       (Value.tagged_tuple "exited" [ Value.ocaml2cduce_int n; s ])
-       | Unix.WSTOPPED n ->
+       | s,Unix.WSTOPPED n ->
 	   Value.raise' 
 	     (Value.tagged_tuple "stopped" [ Value.ocaml2cduce_int n; s ])
-       | Unix.WSIGNALED n ->
+       | s,Unix.WSIGNALED n ->
 	   Value.raise' 
 	     (Value.tagged_tuple "signaled" [ Value.ocaml2cduce_int n; s ])
   )
+  
+let () = register_fun "exit" byte_int Types.empty
+  (fun v -> Location.protect_op "exit"; exit (Value.cduce2ocaml_int v))

types/builtin_defs.ml

@@ -12,6 +12,7 @@ let int_int = mk_interval_type "-2147483648" "2147483647"
 let short_int = mk_interval_type "-32768" "32767"
 let byte_int = mk_interval_type "-128" "127"
 let caml_int = mk_interval_type (string_of_int min_int) (string_of_int max_int)
+let byte_int = mk_interval_type "0" "255"
 
 let non_zero_int = Types.cup pos_int neg_int
 

types/builtin_defs.mli

@@ -9,7 +9,7 @@ val int_int : Types.t         (** -2147483648 .. 2147483647 *)
 val short_int : Types.t       (** -32768 .. 32767 *)
 val byte_int : Types.t        (** -128 .. 127 *)
 val caml_int : Types.t        (** min_int .. max_int *)
-
+val byte_int : Types.t        (** 0 .. 255 *)
 val non_zero_int : Types.t
 
 val intstr : Types.t

typing/typed.ml

@@ -23,7 +23,7 @@ type texpr  =
     }
 and  texpr' = 
   | Forget of texpr * ttyp
-  | Check of texpr * ttyp
+  | Check of (Types.t ref) * texpr * ttyp
   (* CDuce is a Lambda-calculus ... *)
   | Var of id
   | ExtVar of Types.CompUnit.t * id * Types.t

typing/typer.ml

@@ -950,7 +950,7 @@ let rec expr env loc = function
       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))
+      exp loc fv (Typed.Check (ref Types.empty,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
@@ -1187,8 +1187,9 @@ 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);
+  | Check (t0,e,t) ->
+      let te = type_check env e Types.any true in
+      t0 := Types.cup !t0 te;
       verify loc (Types.descr t) constr
 
   | Abstraction a ->

web/download.xml

@@ -4,7 +4,6 @@
 <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

@@ -530,14 +530,10 @@ let gen_page_seq
 ;;
 
 
-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 []
- | _ -> 
-   let _ = 
-     try (input_xml :? [ Site ])
-     with (err & Latin1) -> print ['Invalid input document\n' !err '\n']
-   in []
-
+let [<site>[ <title>site p ] ] = 
+ try (load_include input :? [ Site ])
+ with (err & Latin1) -> 
+   print ['Invalid input document\n' !err '\n']; 
+   exit 2
+in
+let _ = gen_page (site,[],p,[], [], compute_sitemap p) in []