[r2002-10-17 12:30:01 by cvscast] Empty log message

Original author: cvscast
Date: 2002-10-17 12:30:46+00:00

Makefile

@@ -5,8 +5,9 @@ TYPING = typing/typed.cmo typing/typer.cmo
 TYPES  = types/recursive.cmo types/sortedList.cmo \
          types/sortedMap.cmo types/boolean.cmo \
          types/intervals.cmo types/chars.cmo types/atoms.cmo \
-         types/strings.cmo types/types.cmo \
-         types/patterns.cmo 
+         types/types.cmo \
+         types/patterns.cmo \
+         types/op.cmo
 
 DRIVER = driver/cduce.cmo
 
@@ -19,7 +20,7 @@ INCLUDES = -I +camlp4 -I parser -I types -I typing
 SYNTAX_PARSER = -pp 'camlp4o pa_extend.cmo'
 
 all.cma: $(OBJECTS)
-	ocamlc -o all.cma -I +camlp4 gramlib.cma -a $(OBJECTS)
+	ocamlc -o all.cma -I +camlp4 gramlib.cma nums.cma -a $(OBJECTS)
 
 cduce: all.cma $(DRIVER)
 	ocamlc -o cduce all.cma $(DRIVER)

depend

-parser/ast.cmo: parser/location.cmi types/patterns.cmi types/types.cmi 
-parser/ast.cmx: parser/location.cmx types/patterns.cmx types/types.cmx 
+parser/ast.cmo: parser/location.cmi types/op.cmi types/patterns.cmi \
+    types/types.cmi 
+parser/ast.cmx: parser/location.cmx types/op.cmx types/patterns.cmx \
+    types/types.cmx 
 parser/location.cmo: parser/location.cmi 
 parser/location.cmx: parser/location.cmi 
 parser/parser.cmo: parser/ast.cmo types/chars.cmi parser/location.cmi \
@@ -7,8 +9,10 @@ parser/parser.cmo: parser/ast.cmo types/chars.cmi parser/location.cmi \
 parser/parser.cmx: parser/ast.cmx types/chars.cmx parser/location.cmx \
     types/types.cmx parser/parser.cmi 
 parser/parser.cmi: parser/ast.cmo 
-typing/typed.cmo: parser/location.cmi types/patterns.cmi types/types.cmi 
-typing/typed.cmx: parser/location.cmx types/patterns.cmx types/types.cmx 
+typing/typed.cmo: parser/location.cmi types/op.cmi types/patterns.cmi \
+    types/types.cmi 
+typing/typed.cmx: parser/location.cmx types/op.cmx types/patterns.cmx \
+    types/types.cmx 
 typing/typer.cmo: parser/ast.cmo parser/location.cmi types/patterns.cmi \
     types/sortedList.cmi typing/typed.cmo types/types.cmi typing/typer.cmi 
 typing/typer.cmx: parser/ast.cmx parser/location.cmx types/patterns.cmx \
@@ -22,6 +26,8 @@ types/chars.cmo: types/chars.cmi
 types/chars.cmx: types/chars.cmi 
 types/intervals.cmo: types/intervals.cmi 
 types/intervals.cmx: types/intervals.cmi 
+types/op.cmo: parser/location.cmi types/types.cmi types/op.cmi 
+types/op.cmx: parser/location.cmx types/types.cmx types/op.cmi 
 types/patterns.cmo: types/sortedList.cmi types/sortedMap.cmi types/types.cmi \
     types/patterns.cmi 
 types/patterns.cmx: types/sortedList.cmx types/sortedMap.cmx types/types.cmx \
@@ -45,6 +51,7 @@ types/types.cmx: types/atoms.cmx types/boolean.cmx types/chars.cmx \
     types/intervals.cmx types/recursive.cmx types/sortedList.cmx \
     types/sortedMap.cmx types/strings.cmx types/types.cmi 
 types/boolean.cmi: types/sortedList.cmi 
+types/op.cmi: parser/location.cmi types/types.cmi 
 types/patterns.cmi: types/sortedList.cmi types/sortedMap.cmi types/types.cmi 
 types/sortedMap.cmi: types/sortedList.cmi 
 types/syntax.cmi: types/patterns.cmi types/types.cmi 

parser/ast.ml

@@ -27,7 +27,8 @@ and pexpr' =
   | RecordLitt of (Types.label * pexpr) list
       
   (* Data destructors *)
-  | Op of op * pexpr
+  | UnaryOp of Op.unary * pexpr
+  | BinaryOp of Op.binary * pexpr * pexpr
   | Match of pexpr * branches
   | Map of pexpr * branches
 
@@ -39,8 +40,6 @@ and abstr = {
 
 and branches = (ppat * pexpr) list
     
-and op = string
-
 (* A common syntactic class for patterns and types *) 
 
 and ppat = ppat' located

parser/parser.ml

@@ -47,6 +47,9 @@ open Ast
     [ e1 = expr; e2 = expr -> mk loc (Apply (e1,e2))
     ]
     
+    | 
+    [ e1 = expr; "+"; e2 = expr -> mk loc (BinaryOp (Op.add,e1,e2))  ]
+    
     | "no_appl" 
     [ c = const -> mk loc (Cst c)
     | "("; l = LIST1 expr SEP ","; ")" -> tuple loc l
@@ -117,7 +120,8 @@ open Ast
       | "("; a = LIDENT; ":="; c = const; ")" -> mk loc (Constant (a,c))
       | a = UIDENT -> mk loc (PatVar a)
       | i = INT ; "--"; j = INT -> 
-          let i = int_of_string i and j = int_of_string j in
+          let i = Big_int.big_int_of_string i 
+	  and j = Big_int.big_int_of_string j in
           mk loc (Internal (Types.interval i j))
       | i = char ; "--"; j = char ->
           mk loc (Internal (Types.char_class i j))
@@ -153,8 +157,8 @@ open Ast
 
   const:
     [ 
-      [ i = INT -> Types.Integer (int_of_string i)
-      | x = STRING -> Types.String (Token.eval_string x)
+      [ i = INT -> Types.Integer (Big_int.big_int_of_string i)
+(*      | x = STRING -> Types.String (Token.eval_string x) *)
       | "`"; a = [LIDENT | UIDENT] -> Types.Atom (Types.mk_atom a) 
       | c = char -> Types.Char c ]
     ];

types/IDEAS

@@ -10,3 +10,11 @@
 
   Need to benchmark and define heuristics to know when to apply
   this mechanism => empirical.
+
+
+- Remember compiled regexp when printing; same with XML sugar
+
+- When an arrow constraint is not satisfied when typing a function,
+  point to the specific branch ...
+  Better: alternate mode of typing << check that this expression
+  has at most this type >> 

types/intervals.ml

-type t = (int*int) list
+open Big_int
+
+type interval = 
+  | Bounded of big_int * big_int
+  | Left of big_int
+  | Right of big_int
+  | Any
+
+type t = interval list
+
+let rec equal l1 l2 =
+  match (l1,l2) with
+    | (Bounded (a1,b1) :: l1, Bounded (a2,b2) :: l2) ->
+	(eq_big_int a1 a2) &&
+	(eq_big_int b1 b2) &&
+	(equal l1 l2)
+    | (Left b1 :: l1, Left b2 :: l2) ->
+	(eq_big_int b1 b2) &&
+	(equal l1 l2)
+    | (Right a1 :: l1, Right a2 :: l2) ->
+	(eq_big_int a1 a2) &&
+	(equal l1 l2)
+    | (Any :: _, Any :: _) -> true
+    | _ -> false
+
+let hash = function
+  | Bounded (a,b) :: _ ->
+      1 + 2 * (num_digits_big_int a) + 3 * (num_digits_big_int b)
+  | Left b :: _ ->
+      3 * num_digits_big_int b 
+  | Right a :: _ ->
+      2 * (num_digits_big_int a)
+  | Any :: _ -> 1234
+  | [] -> 0
 
 let empty = []
-let full = [min_int,max_int]
-let atom (a,b) =
-  if a<=b then [a,b] else empty
+let any = [Any]
+
+let atom a b =
+  if a<=b then [Bounded (a,b)] else empty
+
+
+let rec add_left l b = match l with
+  | [] -> [Left b]
+  | (Bounded (a1,_) | Right a1) :: _
+      when (lt_big_int b (pred_big_int a1)) -> 
+      Left b :: l
+  | Bounded (_,b1) :: l' -> 
+      add_left l' (max_big_int b b1)
+  | Left b1 :: _ when le_big_int b b1-> l
+  | Left _ :: l' ->
+      add_left l' b
+  | _ -> any
 
-let rec add l ((a,b) as i) = match l with
+let rec add_bounded l a b = match l with
   | [] -> 
-      [i]
-  | ((a1,_) :: _) as l when (a1<>min_int) && (b < (pred a1)) -> 
-      i::l
-  | ((a1,b1) as i' :: l') when (b1<>max_int) && (a > (succ b1)) -> 
-      i'::(add l' i)
-  | (a1,b1) :: l' -> 
-      add l' (min a a1, max b b1)
-
-let rec neg start l = match l with
-  | [] -> [start,max_int]
-  | (a,b) :: l' when a<>min_int -> 
-      if b = max_int then [start,pred a] else
-	(start, pred a) :: (neg (succ b) l')
-  | (_,b) :: l' ->
-      if b = max_int then [] else
-	(neg (succ b) l')
-
-let neg l = neg min_int l
+      [Bounded (a,b)]
+  | (Bounded (a1,_) | Right a1) :: _
+      when (lt_big_int b (pred_big_int a1)) -> 
+      Bounded (a,b) :: l
+  | ((Bounded (_,b1) | Left b1) as i') :: l' 
+      when (lt_big_int (succ_big_int b1) a) -> 
+      i'::(add_bounded l' a b)
+  | Bounded (a1,b1) :: l' -> 
+      add_bounded l' (min_big_int a a1) (max_big_int b b1)
+  | Left b1 :: l' ->
+      add_left l' b
+  | Right a1 :: _ -> [Right a]
+  | Any :: _ -> any
+
+let rec add_right l a = match l with
+  | [] -> [Right a]
+  | ((Bounded (_,b1) | Left b1) as i') :: l' 
+      when (lt_big_int (succ_big_int b1) a) -> 
+      i'::(add_right l' a)
+  | (Bounded (a1,_) | Right a1) :: _ -> 
+      [Right (min_big_int a a1)]
+  | _ -> any
+
+let add l = function
+  | Bounded (a,b) -> add_bounded l a b
+  | Left b -> add_left l b
+  | Right a -> add_right l a
+  | Any -> any
+
+let rec neg' start l = match l with
+  | [] -> [Right start]
+  | Bounded (a,b) :: l' -> 
+      Bounded (start, pred_big_int a) :: (neg' (succ_big_int b) l')
+  | Right a :: l' ->
+      [Bounded (start, pred_big_int a)]
+  | _ -> assert false
+
+let neg = function
+  | Any :: _ -> []
+  | [] -> any
+  | Left b :: l -> neg' (succ_big_int b) l
+  | Right a :: _ -> [Left (pred_big_int a)]
+  | Bounded (a,b) :: l -> Left (pred_big_int a) :: neg' (succ_big_int b) l
 
 let cup i1 i2 =
   List.fold_left add i1 i2
@@ -35,22 +107,42 @@ let cap i1 i2 =
 let diff i1 i2 =
   neg (cup (neg i1) i2)
 
-let is_empty i =
-  i = []  (* representation unique ! *)
+let is_empty i = i = []
 
 
+(* TODO: can optimize this to stop running through the list earlier *)
 let contains n =
-  List.exists (fun (a,b) -> (n>=a) && (n<=b))
+  List.exists (function
+		 | Any -> true
+		 | Left b -> le_big_int n b
+		 | Right a -> le_big_int a n
+		 | Bounded (a,b) -> (le_big_int a n) && (le_big_int n b)
+	      )
 
 let sample = function
-  | (i,j) :: _ -> i
-  | _ -> raise Not_found
+  | (Left x | Right x | Bounded (x,_)) :: _ -> x
+  | Any :: _ -> zero_big_int
+  | [] -> raise Not_found
   
 
 let print =
   List.map 
-    (fun (a,b) ->
-       if a = b 
-       then fun ppf -> Format.fprintf ppf "%i" a
-       else fun ppf -> Format.fprintf ppf "%i--%i" a b
+    (fun x ppf -> match x with
+       | Any ->
+	   Format.fprintf ppf "Int"
+       | Left b -> 
+	   Format.fprintf ppf "minfty--%s" 
+	     (string_of_big_int b)
+       | Right a -> 
+	   Format.fprintf ppf "%s--infy" 
+	     (string_of_big_int a)
+       | Bounded (a,b) when eq_big_int a b -> 
+	   Format.fprintf ppf "%s" 
+	     (string_of_big_int a)
+       | Bounded (a,b) ->
+	   Format.fprintf ppf "%s--%s" 
+	     (string_of_big_int a) 
+	     (string_of_big_int b)
     )
+
+

types/intervals.mli

-(* Combinaisons booléennes d'intervalles d'entiers;
+type t
 
-   elle sont representées comme des réunions disjointes d'intervalles,
-   sous la forme de listes de couples (ai,bi) tq  ai<=bi,  (bi)+1<a(i+1)
-
-   Note: il y a representation unique
-*)
-
-type t = (int*int) list
+val equal : t -> t -> bool
+val hash  : t -> int
 
 val empty : t
-val full  : t
+val any   : t
 val cup   : t -> t -> t
 val cap   : t -> t -> t
 val diff  : t -> t -> t
-val atom  : int*int -> t
+
+val atom  : Big_int.big_int -> Big_int.big_int -> t
 
 
 val is_empty : t -> bool
-val contains : int -> t -> bool
-val sample : t -> int
+val contains : Big_int.big_int -> t -> bool
+val sample : t -> Big_int.big_int
 
 
 val print : t -> (Format.formatter -> unit) list

types/op.ml

+type unary = {
+  un_type : 
+   Location.loc ->  (* location of the whole operator node *)
+   Location.loc -> Types.descr ->  (* first argument *)
+   Types.descr;   (* result *)   
+}
+
+type binary = {
+  bin_type : 
+   Location.loc ->  (* location of the whole operator node *)
+   Location.loc -> Types.descr ->  (* first argument *)
+   Location.loc -> Types.descr ->  (* second argument *)
+   Types.descr;   (* result *)   
+}
+
+
+let add = {
+  bin_type = fun loc loc1 t1 loc2 t2 -> failwith "add not implemented"
+}
+

types/op.mli

+type unary = {
+  un_type : 
+   Location.loc ->  (* location of the whole operator node *)
+   Location.loc -> Types.descr ->  (* first argument *)
+   Types.descr;   (* result *)   
+}
+
+type binary = {
+  bin_type : 
+   Location.loc ->  (* location of the whole operator node *)
+   Location.loc -> Types.descr ->  (* first argument *)
+   Location.loc -> Types.descr ->  (* second argument *)
+   Types.descr;   (* result *)   
+}
+
+
+val add: binary

types/recursive.ml

-(* $Id: recursive.ml,v 1.1.1.1 2002/10/10 09:11:23 cvscast Exp $ *)
+(* $Id: recursive.ml,v 1.2 2002/10/17 12:30:02 cvscast Exp $ *)
 
 exception NotEqual
 exception Incomplete
@@ -160,4 +160,5 @@ struct
       ignore (internalize nr)
     with Exit -> ()
 
+  let hash_descr d =  X.hash (fun n -> !n.id) d
 end

types/recursive.mli

-(* $Id: recursive.mli,v 1.1.1.1 2002/10/10 09:11:23 cvscast Exp $ *)
+(* $Id: recursive.mli,v 1.2 2002/10/17 12:30:02 cvscast Exp $ *)
 
 exception NotEqual
 exception Incomplete
@@ -43,5 +43,7 @@ sig
 
   val id: node -> int
   val descr: node -> descr
+
+  val hash_descr: descr -> int
 end
 

types/types.ml

@@ -6,7 +6,7 @@ open Printf
 type label = int
 type atom  = int
 
-type const = Integer of int | Atom of atom | String of string | Char of Chars.Unichar.t
+type const = Integer of Big_int.big_int | Atom of atom | Char of Chars.Unichar.t
 
 module I = struct
   type 'a t = {
@@ -16,9 +16,8 @@ module I = struct
     arrow : ('a * 'a) Boolean.t;
     record: (label * bool * 'a) Boolean.t;
     chars : Chars.t;
-    strs  : Strings.t;
   }
-		
+
   let empty = { 
     times = Boolean.empty; 
     arrow = Boolean.empty; 
@@ -26,30 +25,27 @@ module I = struct
     ints  = Intervals.empty;
     atoms = Atoms.empty;
     chars = Chars.empty;
-    strs  = Strings.empty;
   }
+
   let any =  {
     times = Boolean.full; 
     arrow = Boolean.full; 
     record= Boolean.full; 
-    ints  = Intervals.full;
+    ints  = Intervals.any;
     atoms = Atoms.full;
     chars = Chars.full;
-    strs  = Strings.any;
   }
 	       
-  let interval i j = { empty with ints = Intervals.atom (i,j) }
+  let interval i j = { empty with ints = Intervals.atom i j }
   let times x y = { empty with times = Boolean.atom (x,y) }
   let arrow x y = { empty with arrow = Boolean.atom (x,y) }
   let record label opt t = { empty with record = Boolean.atom (label,opt,t) }
   let atom a = { empty with atoms = Atoms.atom a }
-  let string r = { empty with strs = Strings.Regexp.compile r }
   let char c = { empty with chars = Chars.atom c }
   let char_class c1 c2 = { empty with chars = Chars.char_class c1 c2 }
   let constant = function
     | Integer i -> interval i i
     | Atom a -> atom a
-    | String s -> string (Strings.Regexp.str s)
     | Char c -> char c
 
 		   
@@ -63,7 +59,6 @@ module I = struct
       ints  = Intervals.cup x.ints  y.ints;
       atoms = Atoms.cup x.atoms y.atoms;
       chars = Chars.cup x.chars y.chars;
-      strs  = Strings.cup x.strs y.strs;
     }
       
   let cap x y = 
@@ -74,7 +69,6 @@ module I = struct
       ints  = Intervals.cap x.ints  y.ints;
       atoms = Atoms.cap x.atoms y.atoms;
       chars = Chars.cap x.chars y.chars;
-      strs  = Strings.cap x.strs y.strs;
     }
       
   let diff x y = 
@@ -85,16 +79,14 @@ module I = struct
       ints  = Intervals.diff x.ints  y.ints;
       atoms = Atoms.diff x.atoms y.atoms;
       chars = Chars.diff x.chars y.chars;
-      strs  = Strings.diff x.strs y.strs;
     }
 
   let neg x = diff any x
 		   
   let equal e a b =
-    if a.ints <> b.ints then raise NotEqual;
+    if not (Intervals.equal a.ints b.ints) then raise NotEqual;
     if a.atoms <> b.atoms then raise NotEqual;
     if a.chars <> b.chars then raise NotEqual;
-    if a.strs <> b.strs then raise NotEqual;
     Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.times b.times;
     Boolean.equal (fun (x1,x2) (y1,y2) -> e x1 y1; e x2 y2) a.arrow b.arrow;
     Boolean.equal (fun (l1,o1,x1) (l2,o2,x2) -> 
@@ -108,11 +100,11 @@ module I = struct
       ints  = a.ints;
       atoms = a.atoms;
       chars = a.chars;
-      strs  = a.strs;
     }
     
   let hash h a =
-    Hashtbl.hash (map h a)
+    (Hashtbl.hash { map h a with ints = Intervals.empty })
+    + (Intervals.hash a.ints)
       
   let iter f a =
     ignore (map f a)
@@ -232,7 +224,6 @@ let rec empty_rec d =
   else if not (Intervals.is_empty d.ints) then false
   else if not (Atoms.is_empty d.atoms) then false
   else if not (Chars.is_empty d.chars) then false
-  else if not (Strings.is_empty d.strs) then false
   else (
     let backup = !memo in
     memo := Assumptions.add d backup;
@@ -308,10 +299,9 @@ let rec find f = function
   | x::r -> try f x with Not_found -> find f r
 
 type t =
-  | Int of int
+  | Int of Big_int.big_int
   | Atom of atom
   | Char of Chars.Unichar.t
-  | String of string
   | Pair of t * t
   | Record of (label * t) list
   | Fun of (node * node) list
@@ -325,7 +315,6 @@ let rec sample_rec memo d =
     try Int (Intervals.sample d.ints) with Not_found ->
     try Atom (Atoms.sample (gen_atom 0) d.atoms) with Not_found ->
     try Char (Chars.sample d.chars) with Not_found ->
-    try String (Strings.sample d.strs) with Not_found ->
     try sample_rec_arrow d.arrow with Not_found ->
 
     let memo = Assumptions.add d memo in
@@ -567,7 +556,19 @@ let normalize n =
 
 module Print =
 struct
-  let marks = Hashtbl.create 63
+  module DescrHash = 
+    Hashtbl.Make(
+      struct 
+	type t = descr
+	let hash = hash_descr
+	let equal = (=)
+      end
+    )
+
+  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 () =
@@ -584,22 +585,20 @@ struct
   let worth_abbrev d = 
     not (trivial d.times && trivial d.arrow && trivial d.record) 
 
-  let rec mark n =
-    let i = id n and d = descr n in
-    try 
-      let r = Hashtbl.find marks i in
-      if (!r = None) && (worth_abbrev d) then 
-	(let na = name () in 
-	 r := Some na;
-	 wh := (na,d) :: !wh
-	)
-    with Not_found -> 
-      Hashtbl.add marks i (ref None);
-      mark_descr d
-  and mark_descr d = 
-    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 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
@@ -609,22 +608,25 @@ struct
 
   let print_atom ppf a = Format.fprintf ppf "`%s" (atom_name a)
 
-  let rec print ppf n =
-(*    Format.fprintf ppf "[%i]" (id n); *)
-    match !(Hashtbl.find marks (id n)) with
-      | Some n -> Format.fprintf ppf "%s" n
-      | None -> print_descr ppf (descr n)
+  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 ->
+      match !(DescrHash.find marks d) with
+      	| Some n -> Format.fprintf ppf "%s" n
+      	| None -> real_print_descr ppf d
+  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 @
-       Strings.print d.strs @
-       Atoms.print "AnyAtom" print_atom d.atoms @