[r2002-11-01 20:09:48 by cvscast] Empty log message

Original author: cvscast
Date: 2002-11-01 20:09:49+00:00

Makefile

@@ -58,6 +58,9 @@ toplevel: $(OBJECTS) $(TOPLEVEL)
 	$(OCAMLC) $(DEBUG) -linkpkg -o $@ gramlib.cma $(OBJECTS) $(TOPLEVEL)
 
 
+dtd2cduce: tools/dtd2cduce.cmo
+	$(OCAMLC) $(DEBUG) -linkpkg -o $@ $<
+
 cduce.opt: all.cmxa $(XDRIVER)
 	$(OCAMLOPT) -linkpkg -o $@ gramlib.cmxa $(XOBJECTS) $(XDRIVER)
 

depend

@@ -52,20 +52,18 @@ types/types.cmo: types/atoms.cmi types/boolean.cmi types/chars.cmi \
 types/types.cmx: types/atoms.cmx types/boolean.cmx types/chars.cmx \
     types/intervals.cmx types/recursive.cmx types/recursive_noshare.cmx \
     types/sortedList.cmx types/sortedMap.cmx types/types.cmi 
-runtime/eval.cmo: types/chars.cmi runtime/load_xml.cmi \
-    runtime/run_dispatch.cmi typing/typed.cmo types/types.cmi \
-    runtime/value.cmi runtime/eval.cmi 
-runtime/eval.cmx: types/chars.cmx runtime/load_xml.cmx \
-    runtime/run_dispatch.cmx typing/typed.cmx types/types.cmx \
-    runtime/value.cmx runtime/eval.cmi 
+runtime/eval.cmo: runtime/load_xml.cmi runtime/run_dispatch.cmi \
+    typing/typed.cmo types/types.cmi runtime/value.cmi runtime/eval.cmi 
+runtime/eval.cmx: runtime/load_xml.cmx runtime/run_dispatch.cmx \
+    typing/typed.cmx types/types.cmx runtime/value.cmx runtime/eval.cmi 
 runtime/load_xml.cmo: types/sortedMap.cmi types/types.cmi runtime/value.cmi \
     runtime/load_xml.cmi 
 runtime/load_xml.cmx: types/sortedMap.cmx types/types.cmx runtime/value.cmx \
     runtime/load_xml.cmi 
 runtime/run_dispatch.cmo: types/patterns.cmi types/types.cmi \
-    runtime/run_dispatch.cmi 
+    runtime/value.cmi runtime/run_dispatch.cmi 
 runtime/run_dispatch.cmx: types/patterns.cmx types/types.cmx \
-    runtime/run_dispatch.cmi 
+    runtime/value.cmx runtime/run_dispatch.cmi 
 runtime/value.cmo: types/chars.cmi types/sequence.cmi types/sortedMap.cmi \
     types/types.cmi runtime/value.cmi 
 runtime/value.cmx: types/chars.cmx types/sequence.cmx types/sortedMap.cmx \

driver/cduce.ml

@@ -50,14 +50,14 @@ let rec print_exn ppf = function
       Format.fprintf ppf "but its infered type is: %a@\n" 
         print_norm s;
       Format.fprintf ppf "which is not a subtype, as shown by the value %a@\n" 
-	Types.Print.print_sample (Types.Sample.get (Types.diff s t));
+	Types.Sample.print (Types.Sample.get (Types.diff s t));
       Format.fprintf ppf "%s@\n" msg
   | Typer.NonExhaustive t ->
       Format.fprintf ppf "This pattern matching is not exhaustive@\n";
       Format.fprintf ppf "Residual type: %a@\n"
 	print_norm t;
       Format.fprintf ppf "Sample value: %a@\n" 
-	Types.Print.print_sample (Types.Sample.get t)
+	Types.Sample.print (Types.Sample.get t)
   | Typer.UnboundId x ->
       Format.fprintf ppf "Unbound identifier %s@\n" x
   | exn ->
@@ -93,7 +93,7 @@ let eval_env = ref Eval.Env.empty
 let insert_type_bindings = 
   List.iter (fun (x,t) ->
 	       typing_env := Typer.Env.add x t !typing_env;
-	       Format.fprintf ppf "|- %s : %a@\n" x print_norm t)
+	       Format.fprintf ppf "|- %s : %a@\n@." x print_norm t)
 
 let type_decl decl =
   insert_type_bindings (Typer.type_let_decl !typing_env decl)
@@ -103,7 +103,7 @@ let eval_decl decl =
   List.iter 
     (fun (x,v) ->
        Eval.enter_global x v;
-       Format.fprintf ppf "=> %s : @[%a@]@\n" x Value.print v
+       Format.fprintf ppf "=> %s : @[%a@]@\n@." x Value.print v
     ) bindings
 
 let phrase ph =
@@ -111,9 +111,9 @@ let phrase ph =
     | Ast.EvalStatement e ->
 	let (fv,e) = Typer.expr e in
 	let t = Typer.type_check !typing_env e Types.any true in
-	Format.fprintf ppf "|- %a@\n" print_norm t;
+	Format.fprintf ppf "|- %a@\n@." print_norm t;
 	let v = Eval.eval !eval_env e in
-	Format.fprintf ppf "=> @[%a@]@\n" Value.print v
+	Format.fprintf ppf "=> @[%a@]@\n@." Value.print v
     | Ast.LetDecl (p,{descr=Ast.Abstraction _}) -> ()
     | Ast.LetDecl (p,e) ->
 	let decl = Typer.let_decl p e in

parser/parser.ml

@@ -173,7 +173,7 @@ EXTEND
     | x = regexp; "*?" -> WeakStar x
     | x = regexp; "+" -> Seq (x, Star x)
     | x = regexp; "+?" -> Seq (x, WeakStar x)
-    | x = regexp; "?" -> Alt (x, Epsilon)
+    | x = regexp; "?" ->  Alt (x, Epsilon)
     | x = regexp; "??" -> Alt (Epsilon, x) ]
   | [ "("; x = regexp; ")" -> x
     | UIDENT "PCDATA" -> string_regexp

runtime/eval.ml

@@ -130,14 +130,3 @@ and eval_int_of e =
   try Integer (Big_int.big_int_of_string s)
   with Failure _ -> raise exn_int_of
   
-and get_string e =
-  let rec compute_len accu = function
-    | Pair (_,y) -> compute_len (accu + 1) y
-    | String (i,j,_,y) -> compute_len (accu + j - i) y
-    | _ -> accu in
-  let rec fill pos s = function
-    | Pair (Char x,y) -> s.[pos] <- Chars.Unichar.to_char x; fill (pos + 1) s y
-    | String (i,j,src,y) -> 
-	String.blit src i s pos (j - i); fill (pos + j - i) s y
-    | _ -> s in
-  fill 0 (String.create (compute_len 0 e)) e

runtime/eval.mli

@@ -10,3 +10,4 @@ val eval: env -> Typed.texpr -> t
 val eval_let_decl: env -> Typed.let_decl -> (string * t) list
 
 
+

runtime/run_dispatch.ml

@@ -46,7 +46,8 @@ let rec run_dispatcher d v =
     | `Ignore r -> make_result_basic v r
     | `Kind k -> run_disp_kind k v
 
-and run_disp_kind actions v = match v with
+and run_disp_kind actions v =
+  match v with
   | Pair (v1,v2) -> run_disp_prod v v1 v2 actions.Patterns.Compile.prod
   | Record r -> run_disp_record r v [] r actions.Patterns.Compile.record
   | Atom a -> 
@@ -65,13 +66,15 @@ and run_disp_kind actions v = match v with
       run_disp_kind actions (normalize v) 
 
 
-and run_disp_basic v f = function
+and run_disp_basic v f x = 
+  match x with
   | [(_,r)] -> make_result_basic v r
   | (t,r)::rem -> if f t then make_result_basic v r else run_disp_basic v f rem
   | _ -> assert false
   
 
-and run_disp_prod v v1 v2 = function
+and run_disp_prod v v1 v2 x =
+  match x with
   | `None -> assert false
   | `TailCall d1 -> run_dispatcher d1 v1
   | `Ignore d2 -> run_disp_prod2 v1 dummy_r v v2 d2
@@ -79,7 +82,8 @@ and run_disp_prod v v1 v2 = function
       let (code1,r1) = run_dispatcher d1 v1 in
       run_disp_prod2 v1 r1 v v2 b1.(code1)
 
-and run_disp_prod2 v1 r1 v v2 = function
+and run_disp_prod2 v1 r1 v v2 x =
+  match x with
   | `None -> assert false
   | `Ignore r -> make_result_prod v1 r1 v2 dummy_r v r
   | `TailCall d2 -> run_dispatcher d2 v2

runtime/value.ml

@@ -18,6 +18,18 @@ let const = function
   | Types.Atom a -> Atom a
   | Types.Char c -> Char c
 
+let get_string e =
+  let rec compute_len accu = function
+    | Pair (_,y) -> compute_len (accu + 1) y
+    | String (i,j,_,y) -> compute_len (accu + j - i) y
+    | _ -> accu in
+  let rec fill pos s = function
+    | Pair (Char x,y) -> s.[pos] <- Chars.Unichar.to_char x; fill (pos + 1) s y
+    | String (i,j,src,y) -> 
+	String.blit src i s pos (j - i); fill (pos + j - i) s y
+    | _ -> s in
+  fill 0 (String.create (compute_len 0 e)) e
+
 let rec is_seq = function
   | Pair (_, y) when is_seq y -> true
   | Atom a when a = Sequence.nil_atom -> true
@@ -88,4 +100,4 @@ let normalize = function
       if i = j then q else
 	Pair (Char (Chars.Unichar.from_char s.[i]),
 	      String (succ i,j,s,q))
-  | v -> v
+  | v -> assert false

runtime/value.mli

@@ -21,3 +21,5 @@ val normalize: t -> t
 val const : Types.const -> t
 val string : string -> t
 val nil : t
+
+val get_string : t -> string

tools/dtd2cduce.ml

+open Pxp_yacc
+open Pxp_lexer_types
+open Pxp_types
+
+let import_dtd ppf name filename =
+  let config = default_config in
+  let mgr = create_entity_manager config (from_file filename) in
+  let next_event = 
+    create_pull_parser config (`Entry_document [`Extend_dtd_fully]) mgr in
+  let event = ref (Some E_end_of_stream) in
+
+  let rec regexp ppf = function
+    | Optional re -> Format.fprintf ppf "%a?" regexp re
+    | Repeated re -> Format.fprintf ppf "%a*" regexp re
+    | Repeated1 re -> Format.fprintf ppf "%a+" regexp re
+    | Seq (re1 :: res) -> 
+	Format.fprintf ppf "(@[%a" regexp re1;
+	List.iter (fun re -> Format.fprintf ppf "@ %a" regexp re) res;
+	Format.fprintf ppf "@])"
+    | Alt (re1 :: res) -> 
+	Format.fprintf ppf "(@[%a" regexp re1;
+	List.iter (fun re -> Format.fprintf ppf "@ | %a" regexp re) res;
+	Format.fprintf ppf "@])"
+    | Child s -> Format.fprintf ppf "%s" (name s)
+    | _ -> assert false
+  in
+  let content ppf = function
+    | Unspecified | Any -> Format.fprintf ppf "Any*"
+    | Empty -> Format.fprintf ppf ""
+    | Mixed l -> 
+	let l = List.map 
+		  (function 
+		     | MPCDATA -> "Char"
+		     | MChild s -> name s) l in
+	Format.fprintf ppf "(%s)*" (String.concat " | " l)
+    | Regexp r -> regexp ppf r
+  in    
+  let elt ppf e = 
+    Format.fprintf ppf "type %s = <%s>[@[%a@]];;@\n" 
+      (name (e # name))
+      (e # name)
+      content (e # content_model)
+  in      
+  let handle = function
+    | E_start_doc(_,_,dtd) ->
+	List.iter (fun x -> elt ppf (dtd # element x)) (dtd # element_names);
+	exit 1
+    | _ -> ()
+  in
+  let rec loop () =
+    match next_event () with
+      | None -> ()
+      | Some e -> handle e; loop ()
+  in
+  loop ()
+ 
+	  
+
+let () =
+  let name s = Sys.argv.(1) ^ s in
+  import_dtd Format.std_formatter name Sys.argv.(2)

types/patterns.ml

+  let wrap s f x =
+    Printf.eprintf "%s start\n" s; flush stderr;
+    let r = f x in
+    Printf.eprintf "%s stop\n" s; flush stderr;
+    r
+
 type capture = string
 type fv = capture SortedList.t
 
@@ -283,7 +289,6 @@ struct
 
   let bigcap = List.fold_left (fun a p -> cap a (nf (descr p))) any
 
-
   let normal nf =
     let basic =
       List.map (fun ((res,()),acc) -> (res,acc)) 
@@ -292,8 +297,10 @@ struct
       let line accu (((res,(pl,ql)),acc)) =
 	let p = bigcap pl and q = bigcap ql in
 	let aux accu (t1,t2) = (res,(restrict t1 p,restrict t2 q))::accu in
-	List.fold_left aux accu (Types.Product.normal acc) in
+	let t = Types.Product.normal acc in
+	List.fold_left aux accu t in
       List.fold_left line []
+   
 
     and record =
       let rec aux nr fields = 
@@ -332,6 +339,7 @@ struct
       nprod   = nlines (prod nf.prod);
       nrecord = nlines (record nf.record);
     }
+
 end
 
 
@@ -617,8 +625,9 @@ struct
     let aux i x = 
       let yes, no = f x in
       List.iter (fun (p,info) ->
-		   let p = Normal.normal (Normal.restrict t p) in
-		   accu := (p,[i, info]) :: !accu
+		   let p = Normal.restrict t p in
+		   let p = Normal.normal p in
+		   accu := (p,[i, info]) :: !accu;
 		) yes;
       unselect.(i) <- no @ unselect.(i) in
     Array.iteri (fun i -> List.iter (aux i)) pl;
@@ -632,10 +641,10 @@ struct
       List.iter (fun (j,r) -> List.iter (add r) infos.(j)) m;
       d t selected unselect
     in
-
     let res = Array.map result disp.codes in
     post (disp,res)
 
+
   let make_branches t brs =
     let (_,brs) = 
       List.fold_left

types/types.ml

@@ -6,6 +6,25 @@ open Printf
 type label = int
 type atom  = int
 
+let counter_label = ref 0
+let label_table = Hashtbl.create 63
+let label_names = Hashtbl.create 63
+
+let label s =
+  try Hashtbl.find label_table s
+  with Not_found ->
+    incr counter_label;
+    Hashtbl.add label_table s !counter_label;
+    Hashtbl.add label_names !counter_label s;
+    !counter_label
+
+let label_name l =
+  Hashtbl.find label_names l
+
+let mk_atom = label
+
+let atom_name = label_name
+
 type const = Integer of Big_int.big_int | Atom of atom | Char of Chars.Unichar.t
 
 module I = struct
@@ -118,6 +137,16 @@ end
 module Algebra = Recursive_noshare.Make(I)
 include I
 include Algebra
+module DescrHash = 
+  Hashtbl.Make(
+    struct 
+      type t = descr
+      let hash = hash_descr
+      let equal = equal_descr
+    end
+  )
+
+module DescrMap = Map.Make(struct type t = descr let compare = compare end)
 
 let check d =
   Boolean.check d.times;
@@ -135,6 +164,115 @@ let cons d =
   internalize n
 
 
+module Print = 
+struct
+  let print_atom ppf a = Format.fprintf ppf "`%s" (atom_name a)
+
+  let print_const ppf = function
+    | Integer i -> Format.fprintf ppf "%s" (Big_int.string_of_big_int i)
+    | Atom a -> print_atom ppf a
+    | Char c -> Chars.Unichar.print ppf c
+
+  let named = DescrHash.create 10
+  let register_global name d = DescrHash.add named d name
+
+  let marks = DescrHash.create 63
+  let wh = ref []
+  let count_name = ref 0
+  let name () =
+    incr count_name;
+    "X" ^ (string_of_int !count_name)
+(* TODO: 
+   check that these generated names does not conflict with declared types *)
+
+  let bool_iter f b =
+    List.iter (fun (p,n) -> List.iter f p; List.iter f n) b
+
+  let trivial b = b = Boolean.empty || b = Boolean.full
+
+  let worth_abbrev d = 
+    not (trivial d.times && trivial d.arrow && trivial d.record) 
+
+  let rec mark n = mark_descr (descr n)
+  and mark_descr d =
+    if not (DescrHash.mem named d) then
+      try 
+	let r = DescrHash.find marks d in
+	if (!r = None) && (worth_abbrev d) then 
+	  let na = name () in 
+	  r := Some na;
+	  wh := (na,d) :: !wh
+      with Not_found -> 
+	DescrHash.add marks d (ref None);
+    	bool_iter (fun (n1,n2) -> mark n1; mark n2) d.times;
+    	bool_iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
+    	bool_iter (fun (l,o,n) -> mark n) d.record
+
+    
+  let rec print_union ppf = function
+    | [] -> Format.fprintf ppf "Empty"
+    | [h] -> h ppf
+    | h::t -> Format.fprintf ppf "@[%t |@ %a@]" h print_union t
+
+
+  let rec print ppf n = print_descr ppf (descr n)
+  and print_descr ppf d = 
+    try 
+      let name = DescrHash.find named d in
+      Format.fprintf ppf "%s" name
+    with Not_found ->
+      try
+      	match !(DescrHash.find marks d) with
+      	  | Some n -> Format.fprintf ppf "%s" n
+      	  | None -> real_print_descr ppf d
+      with
+	  Not_found -> Format.fprintf ppf "XXX"
+  and real_print_descr ppf d = 
+    if d = any then Format.fprintf ppf "Any" else
+      print_union ppf 
+	(Intervals.print d.ints @
+	 Chars.print d.chars @
+	 Atoms.print "Atom" print_atom d.atoms @
+	 Boolean.print "Pair" print_times d.times @
+	 Boolean.print "Arrow" print_arrow d.arrow @
+	 Boolean.print "Record" print_record d.record
+	)
+  and print_times ppf (t1,t2) =
+    Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
+  and print_arrow ppf (t1,t2) =
+    Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
+  and print_record ppf (l,o,t) =
+    Format.fprintf ppf "@[{ %s =%s %a }@]" 
+      (label_name l) (if o then "?" else "") print t
+
+	  
+  let end_print ppf =
+    (match List.rev !wh with
+       | [] -> ()
+       | (na,d)::t ->
+	   Format.fprintf ppf " where@ @[%s = %a" na real_print_descr d;
+	   List.iter 
+	     (fun (na,d) -> 
+		Format.fprintf ppf " and@ %s = %a" na real_print_descr d)
+	     t;
+	   Format.fprintf ppf "@]"
+    );
+    Format.fprintf ppf "@]";
+    count_name := 0;
+    wh := [];
+    DescrHash.clear marks
+
+  let print_descr ppf d =
+    mark_descr d;
+    Format.fprintf ppf "@[%a" print_descr d;
+    end_print ppf
+
+   let print ppf n = print_descr ppf (descr n)
+
+end
+
+
+
 module Positive =
 struct
   type rhs = [ `Type of descr | `Cup of v list | `Times of v * v ]
@@ -183,24 +321,6 @@ let get_record r =
   List.map line r
     
 
-let counter_label = ref 0
-let label_table = Hashtbl.create 63
-let label_names = Hashtbl.create 63
-
-let label s =
-  try Hashtbl.find label_table s
-  with Not_found ->
-    incr counter_label;
-    Hashtbl.add label_table s !counter_label;
-    Hashtbl.add label_names !counter_label s;
-    !counter_label
-
-let label_name l =
-  Hashtbl.find label_names l
-
-let mk_atom = label
-
-let atom_name = label_name
 
 (* Subtyping algorithm *)
 
@@ -376,6 +496,36 @@ and sample_rec_record_aux memo fields =
 
 let get x = sample_rec Assumptions.empty x
 
+  let rec print_sep f sep ppf = function
+    | [] -> ()
+    | [x] -> f ppf x
+    | x::rem -> f ppf x; Format.fprintf ppf "%s" sep; print_sep f sep ppf rem
+
+
+  let rec print ppf = function
+    | Int i -> Format.fprintf ppf "%s" (Big_int.string_of_big_int i)
+    | Atom a -> Format.fprintf ppf "`%s" (atom_name a)
+    | Char c -> Chars.Unichar.print ppf c
+    | Pair (x1,x2) -> Format.fprintf ppf "(%a,%a)" print x1 print x2
+    | Record r ->
+	Format.fprintf ppf "{ %a }"
+	  (print_sep 
+	     (fun ppf (l,x) -> 
+		Format.fprintf ppf "%s = %a"
+		(label_name l)
+		print x
+	     )
+	     " ; "
+	  ) r
+    | Fun iface ->
+	Format.fprintf ppf "(fun ( %a ) x -> ...)"
+	  (print_sep
+	     (fun ppf (t1,t2) ->
+		Format.fprintf ppf "%a -> %a; "
+		Print.print t1 Print.print t2
+	     )
+	     " ; "
+	  ) iface
 end
 
 
@@ -388,8 +538,40 @@ struct
 
   let need_second = function _::_::_ -> true | _ -> false
 
-  let get d =
+  let normal_aux d =
+    let res = ref [] in
+
+    let add (t1,t2) =
+      let rec loop t1 t2 = function
+	| [] -> res := (ref (t1,t2)) :: !res
+	| ({contents = (d1,d2)} as r)::l ->
+	    (*OPT*) 
+	    if d1 = t1 then r := (d1,cup d2 t2) else
+	      
+	      let i = cap t1 d1 in
+	      if is_empty i then loop t1 t2 l
+	      else (
+		r := (i, cup t2 d2);
+		let k = diff d1 t1 in 
+		if non_empty k then res := (ref (k,d2)) :: !res;
+		
+		let j = diff t1 d1 in 
+		if non_empty j then loop j t2 l
+	      )
+      in
+      loop t1 t2 !res
+    in
+    List.iter add d;
+    List.map (!) !res
+
+(*
+This version explodes when dealing with
+   Any - [ t1? t2? t3? ... tn? ]
+==> need partitioning 
+*)
+  let get_aux d =
     let line accu (left,right) =
+      let debug = List.length right = 28 in
       let rec aux accu d1 d2 = function
 	| (t1,t2)::right ->
 	    let accu = 
@@ -399,12 +581,38 @@ struct
               let d2 = diff_t d2 t2 in
               if is_empty d2 then accu else aux accu d1 d2 right in
 	    accu
-	| [] ->  (d1,d2) :: accu
+	| [] -> (d1,d2) :: accu
       in
       let (d1,d2) = cap_product left in
       if (is_empty d1) || (is_empty d2) then accu else aux accu d1 d2 right
     in
-    List.fold_left line [] d.times
+    List.fold_left line [] d
+
+(* Partitioning *)
+
+  let get_aux d =
+    let accu = ref [] in
+    let line (left,right) =
+      let (d1,d2) = cap_product left in
+      if (non_empty d1) && (non_empty d2) then
+	let right = List.map (fun (t1,t2) -> descr t1, descr t2) right in
+	let right = normal_aux right in
+	let resid1 = ref d1 in
+	let () = 
+	  List.iter
+	    (fun (t1,t2) ->
+	       let t1 = cap d1 t1 in
+	       if (non_empty t1) then
+		 let () = resid1 := diff !resid1 t1 in
+		 let t2 = diff d2 t2 in
+		 if (non_empty t2) then accu := (t1,t2) :: !accu
+	    ) right in
+	if non_empty !resid1 then accu := (!resid1, d2) :: !accu 
+    in
+    List.iter line d;