[r2003-05-18 13:30:38 by cvscast] New pretty-printer for types

Original author: cvscast
Date: 2003-05-18 13:30:58+00:00

Makefile

@@ -5,7 +5,8 @@ CLEAN_DIRS = $(DIRS) tools tests
 
 # Objects to build
 
-MISC = misc/state.cmo misc/pool.cmo misc/encodings.cmo misc/bool.cmo
+MISC = misc/state.cmo misc/pool.cmo misc/encodings.cmo misc/bool.cmo \
+	misc/pretty.cmo
 
 PARSER = parser/lexer.cmo parser/location.cmo \
          parser/wlexer.cmo \

depend

@@ -4,6 +4,8 @@ misc/encodings.cmo: misc/encodings.cmi
 misc/encodings.cmx: misc/encodings.cmi 
 misc/pool.cmo: misc/state.cmi misc/pool.cmi 
 misc/pool.cmx: misc/state.cmx misc/pool.cmi 
+misc/pretty.cmo: misc/pretty.cmi 
+misc/pretty.cmx: misc/pretty.cmi 
 misc/state.cmo: misc/state.cmi 
 misc/state.cmx: misc/state.cmi 
 parser/ast.cmo: types/ident.cmo parser/location.cmi types/types.cmi 
@@ -24,14 +26,14 @@ typing/typed.cmo: types/ident.cmo parser/location.cmi types/patterns.cmi \
     types/types.cmi 
 typing/typed.cmx: types/ident.cmx parser/location.cmx types/patterns.cmx \
     types/types.cmx 
-typing/typer.cmo: parser/ast.cmo types/builtin.cmo types/ident.cmo \
-    types/intervals.cmi parser/location.cmi types/patterns.cmi \
-    types/sequence.cmi misc/state.cmi typing/typed.cmo types/types.cmi \
-    typing/typer.cmi 
-typing/typer.cmx: parser/ast.cmx types/builtin.cmx types/ident.cmx \
-    types/intervals.cmx parser/location.cmx types/patterns.cmx \
-    types/sequence.cmx misc/state.cmx typing/typed.cmx types/types.cmx \
-    typing/typer.cmi 
+typing/typer.cmo: parser/ast.cmo types/atoms.cmi types/builtin.cmo \
+    types/ident.cmo types/intervals.cmi parser/location.cmi \
+    types/patterns.cmi types/sequence.cmi misc/state.cmi typing/typed.cmo \
+    types/types.cmi typing/typer.cmi 
+typing/typer.cmx: parser/ast.cmx types/atoms.cmx types/builtin.cmx \
+    types/ident.cmx types/intervals.cmx parser/location.cmx \
+    types/patterns.cmx types/sequence.cmx misc/state.cmx typing/typed.cmx \
+    types/types.cmx typing/typer.cmi 
 types/atoms.cmo: misc/pool.cmi types/sortedList.cmi types/atoms.cmi 
 types/atoms.cmx: misc/pool.cmx types/sortedList.cmx types/atoms.cmi 
 types/boolean.cmo: types/sortedList.cmi types/boolean.cmi 
@@ -61,11 +63,11 @@ types/sortedMap.cmx: types/sortedMap.cmi
 types/type_bool.cmo: types/boolean.cmi 
 types/type_bool.cmx: types/boolean.cmx 
 types/types.cmo: types/atoms.cmi misc/bool.cmi types/chars.cmi \
-    types/ident.cmo types/intervals.cmi types/normal.cmi types/sortedList.cmi \
-    misc/state.cmi types/types.cmi 
+    types/ident.cmo types/intervals.cmi types/normal.cmi misc/pretty.cmi \
+    types/sortedList.cmi misc/state.cmi types/types.cmi 
 types/types.cmx: types/atoms.cmx misc/bool.cmx types/chars.cmx \
-    types/ident.cmx types/intervals.cmx types/normal.cmx types/sortedList.cmx \
-    misc/state.cmx types/types.cmi 
+    types/ident.cmx types/intervals.cmx types/normal.cmx misc/pretty.cmx \
+    types/sortedList.cmx misc/state.cmx types/types.cmi 
 runtime/eval.cmo: types/atoms.cmi types/ident.cmo types/intervals.cmi \
     runtime/load_xml.cmi parser/location.cmi runtime/print_xml.cmo \
     runtime/run_dispatch.cmi misc/state.cmi typing/typed.cmo \
@@ -78,10 +80,10 @@ runtime/load_xml.cmo: types/atoms.cmi types/ident.cmo parser/location.cmi \
     runtime/value.cmi runtime/load_xml.cmi 
 runtime/load_xml.cmx: types/atoms.cmx types/ident.cmx parser/location.cmx \
     runtime/value.cmx runtime/load_xml.cmi 
-runtime/print_xml.cmo: types/atoms.cmi types/chars.cmi types/ident.cmo \
-    types/sequence.cmi runtime/value.cmi 
-runtime/print_xml.cmx: types/atoms.cmx types/chars.cmx types/ident.cmx \
-    types/sequence.cmx runtime/value.cmx 
+runtime/print_xml.cmo: types/atoms.cmi types/chars.cmi misc/encodings.cmi \
+    types/ident.cmo types/sequence.cmi runtime/value.cmi 
+runtime/print_xml.cmx: types/atoms.cmx types/chars.cmx misc/encodings.cmx \
+    types/ident.cmx types/sequence.cmx runtime/value.cmx 
 runtime/run_dispatch.cmo: types/atoms.cmi types/chars.cmi misc/encodings.cmi \
     types/ident.cmo types/patterns.cmi types/types.cmi runtime/value.cmi \
     runtime/run_dispatch.cmi 

driver/cduce.ml

@@ -43,21 +43,21 @@ let rec print_exn ppf = function
   | Typer.WrongLabel (t,l) ->
       Format.fprintf ppf "Wrong record selection: the label %s@\n" 
         (LabelPool.value l);
-      Format.fprintf ppf "applied to an expression of type %a@\n"
+      Format.fprintf ppf "applied to an expression of type:@\n%a@\n"
         print_norm t
   | Typer.ShouldHave (t,msg) ->
-      Format.fprintf ppf "This expression should have type %a@\n%s@\n" 
+      Format.fprintf ppf "This expression should have type:@\n%a@\n%s@\n" 
         print_norm t
         msg
   | Typer.ShouldHave2 (t1,msg,t2) ->
-      Format.fprintf ppf "This expression should have type %a@\n%s %a@\n" 
+      Format.fprintf ppf "This expression should have type:@\n%a@\n%s %a@\n" 
         print_norm t1
         msg
         print_norm t2
   | Typer.Constraint (s,t,msg) ->
-      Format.fprintf ppf "This expression should have type %a@\n" 
+      Format.fprintf ppf "This expression should have type:@\n%a@\n" 
         print_norm t;
-      Format.fprintf ppf "but its infered type is: %a@\n" 
+      Format.fprintf ppf "but its infered type is:@\n%a@\n" 
         print_norm s;
       Format.fprintf ppf "which is not a subtype, as shown by the value " ;
       Location.protect ppf
@@ -66,9 +66,9 @@ let rec print_exn ppf = function
       Format.fprintf ppf "@\n%s@\n" msg
   | Typer.NonExhaustive t ->
       Format.fprintf ppf "This pattern matching is not exhaustive@\n";
-      Format.fprintf ppf "Residual type: %a@\n"
+      Format.fprintf ppf "Residual type:@\n%a@\n"
 	print_norm t;
-      Format.fprintf ppf "Sample value: %a@\n" 
+      Format.fprintf ppf "Sample value:@\n%a@\n" 
 	Types.Sample.print (Types.Sample.get t)
   | Typer.UnboundId x ->
       Format.fprintf ppf "Unbound identifier %s@\n" x

misc/bool.ml

@@ -147,7 +147,7 @@ struct
       | Split(_,x, p,i,n) ->
 	  let p = cap (atom x) (aux p)
 	  and i = aux i
-	  and n = diff (aux p) (atom x) in
+	  and n = diff (aux n) (atom x) in
 	  cup (cup p i) n
     in
     aux b

misc/pretty.ml

+type 'a regexp = 
+  | Empty
+  | Epsilon
+  | Seq of 'a regexp * 'a regexp
+  | Alt of 'a regexp * 'a regexp
+  | Star of 'a regexp
+  | Trans of 'a
+
+module Decompile(H : Hashtbl.S) = struct
+  let alt s1 s2 = match (s1,s2) with
+    | Empty,s | s,Empty -> s2 
+    | (s1,s2) -> Alt (s1,s2)
+
+  let star = function
+    | Empty | Epsilon -> Epsilon
+    | Star _ as s -> s 
+    | s -> Star s
+
+  let rec seq s1 s2 = match (s1,s2) with
+    | Empty,_ | _,Empty -> Empty
+    | Epsilon,s | s,Epsilon -> s
+    | Seq (a,b),s2 -> Seq (a, seq b s2)
+    | (s1,s2) -> Seq (s1,s2)
+
+  type 'a slot = { 
+    mutable weight : int;
+    mutable outg : ('a slot * 'a regexp) list;
+    mutable inc  : ('a slot * 'a regexp) list;
+    mutable self : 'a regexp;
+    mutable ok   : bool
+  }
+  let empty () = { weight = 0; outg = []; inc = []; self = Empty; ok = false }
+
+  let decompile trans n0 =
+    let slot_table = H.create 121 in
+    let slots = ref [] in
+    let slot n =
+      try H.find slot_table n
+      with Not_found -> 
+	let s = empty () in
+	H.add slot_table n s;
+	slots := s :: !slots;
+	s in
+
+    let add_trans s1 s2 t =
+      if s1 == s2 
+      then s1.self <- alt s1.self t
+      else (s1.outg <- (s2,t) :: s1.outg; s2.inc <- (s1,t) :: s2.inc) in
+
+    let final = empty () in
+    let initial = empty () in
+
+    let rec conv n =
+      let s = slot n in
+      if not s.ok then (
+	s.ok <- true;
+	let (tr,f) = trans n in
+	if f then add_trans s final Epsilon;
+	List.iter (fun (l,dst) -> add_trans s (conv dst) (Trans l)) tr;
+      );
+      s in
+
+    let elim s =
+      s.weight <- (-1);
+      let loop = star s.self in
+      List.iter 
+	(fun (s1,t1) -> if s1.weight >= 0 then 
+	   List.iter 
+	     (fun (s2,t2) -> if s2.weight >= 0 then 
+		add_trans s1 s2 (seq t1 (seq loop t2)))
+	     s.outg
+	) s.inc in
+
+    add_trans initial (conv n0) Epsilon;
+    List.iter 
+      (fun s -> s.weight <- List.length s.inc * List.length s.outg)
+      !slots;
+    let slots = List.sort (fun s1 s2 -> compare s1.weight s2.weight) !slots in
+    List.iter elim slots;
+    List.fold_left 
+      (fun accu (s,t) -> if s == final then alt accu t else accu)
+      Empty
+      initial.outg
+end

misc/pretty.mli

+(* Decompilation of regular expressions *)
+
+type 'a regexp = 
+  | Empty
+  | Epsilon
+  | Seq of 'a regexp * 'a regexp
+  | Alt of 'a regexp * 'a regexp
+  | Star of 'a regexp
+  | Trans of 'a
+
+module Decompile(H : Hashtbl.S) : sig
+  val decompile: (H.key -> ('a * H.key) list * bool) -> H.key -> 'a regexp
+end

types/chars.ml

@@ -114,7 +114,10 @@ let contains n = List.exists (fun (a,b) -> (n>=a) && (n<=b))
 let sample = function
   | (i,j) :: _ -> i
   | _ -> raise Not_found
-  
+
+let is_char = function
+  | [(i,j) ] when i = j -> Some i
+  | _ -> None
 
 let print =
   List.map 

types/chars.mli

@@ -26,6 +26,7 @@ val disjoint : t -> t -> bool
 val is_empty : t -> bool
 val contains : v -> t -> bool
 val sample : t -> v
+val is_char : t -> v option
 
 
 type 'a map

types/types.mli

@@ -128,6 +128,8 @@ module Record : sig
 
   val merge: descr -> descr -> descr
   val remove_field: descr -> label -> descr
+
+  val get: descr -> (descr label_map * bool * bool) list
 end
 
 module Arrow : sig
@@ -162,12 +164,8 @@ end
 
 module Int : sig
   val has_int : descr -> Intervals.v -> bool
-
-  val any : descr
-
-  val is_int : descr -> bool
   val get: descr -> Intervals.t
-  val put: Intervals.t -> descr
+  val any : descr
 end
 
 module Atom : sig
@@ -177,8 +175,8 @@ end
 
 module Char : sig
   val has_char : descr -> Chars.v -> bool
-  val any : descr
   val get: descr -> Chars.t
+  val any : descr
 end
 
 val normalize : descr -> descr

typing/typer.ml

@@ -949,12 +949,9 @@ and type_op loc op args =
 	let r = if Types.Record.has_record t1 then Some t1 else None in
 	(match (int,r) with
 	   | Some t1, None ->
-	       if not (Types.Int.is_int t2) then
-		 raise_loc loc2
-		   (Constraint 
-		      (t2,Types.Int.any,
-		       "The second argument of + must be an integer"));
-	       Types.Int.put
+	       check loc2 t2 Types.Int.any
+	       "The second argument of + must be an integer";
+	       Types.interval
 		 (Intervals.add t1 (Types.Int.get t2));
 	   | None, Some r1 ->
 	       check loc2 t2 Types.Record.any 
@@ -966,7 +963,7 @@ and type_op loc op args =
 	       check loc2 t2 int_cup_record
 	       "The second argument of + must be an integer or a record";
 	       Types.cup 
-		 (Types.Int.put (Intervals.add t1 (Types.Int.get t2)))
+		 (Types.interval (Intervals.add t1 (Types.Int.get t2)))
 		 (Types.Record.merge r1 t2)
 	)
     | "-", [loc1,t1; loc2,t2] ->
@@ -1029,17 +1026,11 @@ and type_op loc op args =
     | _ -> assert false
 
 and type_int_binop f loc1 t1 loc2 t2 =
-  if not (Types.Int.is_int t1) then
-    raise_loc loc1 
-      (Constraint 
-	 (t1,Types.Int.any,
-	  "The first argument must be an integer"));
-  if not (Types.Int.is_int t2) then
-    raise_loc loc2
-      (Constraint 
-	       (t2,Types.Int.any,
-		"The second argument must be an integer"));
-  Types.Int.put
+  check loc1 t1 Types.Int.any
+    "The first argument must be an integer";
+  check loc2 t2 Types.Int.any
+    "The second argument must be an integer";
+  Types.interval
     (f (Types.Int.get t1) (Types.Int.get t2))