[r2002-10-17 15:38:33 by cvscast] Empty log message

Original author: cvscast
Date: 2002-10-17 15:38:35+00:00

Makefile

@@ -6,8 +6,7 @@ TYPES  = types/recursive.cmo types/sortedList.cmo \
          types/sortedMap.cmo types/boolean.cmo \
          types/intervals.cmo types/chars.cmo types/atoms.cmo \
          types/types.cmo \
-         types/patterns.cmo \
-         types/op.cmo
+         types/patterns.cmo
 
 DRIVER = driver/cduce.cmo
 
@@ -20,10 +19,10 @@ 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 nums.cma -a $(OBJECTS)
+	ocamlc -g -o all.cma -I +camlp4 gramlib.cma nums.cma -a $(OBJECTS)
 
 cduce: all.cma $(DRIVER)
-	ocamlc -o cduce all.cma $(DRIVER)
+	ocamlc -g -o cduce all.cma $(DRIVER)
 
 compute_depend:
 	@echo "Computing dependencies ..."
@@ -43,12 +42,12 @@ clean:
 .SUFFIXES: .ml .mli .cmo .cmi .cmx
 
 .ml.cmo:
-	ocamlc -c $(SYNTAX_PARSER) $(INCLUDES) $<
+	ocamlc -g -c $(SYNTAX_PARSER) $(INCLUDES) $<
 .ml.cmx:
-	ocamlopt -c $(SYNTAX_PARSER) $(INCLUDES) $<
+	ocamlopt -g -c $(SYNTAX_PARSER) $(INCLUDES) $<
 
 .mli.cmi:
-	ocamlc -c $(INCLUDES) $<
+	ocamlc -g -c $(INCLUDES) $<
 
 # FORTPATH = /users/formel8/frisch/solaris/fort/fort
 FORTPATH = /home/frisch/fort

depend

-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/ast.cmo: parser/location.cmi types/patterns.cmi types/types.cmi 
+parser/ast.cmx: parser/location.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 \
@@ -9,14 +7,14 @@ 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/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 \
-    types/sortedList.cmx typing/typed.cmx types/types.cmx typing/typer.cmi 
+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/typer.cmo: parser/ast.cmo types/intervals.cmi parser/location.cmi \
+    types/patterns.cmi types/sortedList.cmi typing/typed.cmo types/types.cmi \
+    typing/typer.cmi 
+typing/typer.cmx: parser/ast.cmx types/intervals.cmx parser/location.cmx \
+    types/patterns.cmx types/sortedList.cmx typing/typed.cmx types/types.cmx \
+    typing/typer.cmi 
 typing/typer.cmi: parser/ast.cmo typing/typed.cmo types/types.cmi 
 types/atoms.cmo: types/sortedList.cmi types/atoms.cmi 
 types/atoms.cmx: types/sortedList.cmx types/atoms.cmi 
@@ -26,8 +24,6 @@ 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 \
@@ -46,16 +42,15 @@ types/type_bool.cmo: types/boolean.cmi types/recursive.cmi
 types/type_bool.cmx: types/boolean.cmx types/recursive.cmx 
 types/types.cmo: types/atoms.cmi types/boolean.cmi types/chars.cmi \
     types/intervals.cmi types/recursive.cmi types/sortedList.cmi \
-    types/sortedMap.cmi types/strings.cmi types/types.cmi 
+    types/sortedMap.cmi types/types.cmi 
 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/sortedMap.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 
-types/types.cmi: types/chars.cmi types/sortedMap.cmi types/strings.cmi 
+types/types.cmi: types/chars.cmi types/intervals.cmi types/sortedMap.cmi 
 driver/cduce.cmo: parser/ast.cmo parser/location.cmi parser/parser.cmi \
     typing/typer.cmi types/types.cmi 
 driver/cduce.cmx: parser/ast.cmx parser/location.cmx parser/parser.cmx \

parser/ast.ml

@@ -27,8 +27,7 @@ and pexpr' =
   | RecordLitt of (Types.label * pexpr) list
       
   (* Data destructors *)
-  | UnaryOp of Op.unary * pexpr
-  | BinaryOp of Op.binary * pexpr * pexpr
+  | Op of string * pexpr list
   | Match of pexpr * branches
   | Map of pexpr * branches
 

parser/parser.ml

@@ -48,8 +48,10 @@ open Ast
     ]
     
     | 
-    [ e1 = expr; "+"; e2 = expr -> mk loc (BinaryOp (Op.add,e1,e2))  ]
-    
+    [ e1 = expr; "+"; e2 = expr -> mk loc (Op ("+",[e1;e2]))  ]
+    |
+    [ e1 = expr; "*"; e2 = expr -> mk loc (Op ("*",[e1;e2]))  ]
+
     | "no_appl" 
     [ c = const -> mk loc (Cst c)
     | "("; l = LIST1 expr SEP ","; ")" -> tuple loc l

types/intervals.ml

@@ -9,6 +9,7 @@ type interval =
 type t = interval list
 
 let rec equal l1 l2 =
+  (l1 == l2) ||
   match (l1,l2) with
     | (Bounded (a1,b1) :: l1, Bounded (a2,b2) :: l2) ->
 	(eq_big_int a1 a2) &&
@@ -21,6 +22,7 @@ let rec equal l1 l2 =
 	(eq_big_int a1 a2) &&
 	(equal l1 l2)
     | (Any :: _, Any :: _) -> true
+    | ([], []) -> true
     | _ -> false
 
 let hash = function
@@ -37,22 +39,22 @@ let empty = []
 let any = [Any]
 
 let atom a b =
-  if a<=b then [Bounded (a,b)] else empty
+  if le_big_int a b then [Bounded (a,b)] else empty
 
 
-let rec add_left l b = match l with
+let rec iadd_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)
+      iadd_left l' (max_big_int b b1)
   | Left b1 :: _ when le_big_int b b1-> l
   | Left _ :: l' ->
-      add_left l' b
+      iadd_left l' b
   | _ -> any
 
-let rec add_bounded l a b = match l with
+let rec iadd_bounded l a b = match l with
   | [] -> 
       [Bounded (a,b)]
   | (Bounded (a1,_) | Right a1) :: _
@@ -60,27 +62,27 @@ let rec add_bounded l a b = match l with
       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)
+      i'::(iadd_bounded l' a b)
   | Bounded (a1,b1) :: l' -> 
-      add_bounded l' (min_big_int a a1) (max_big_int b b1)
+      iadd_bounded l' (min_big_int a a1) (max_big_int b b1)
   | Left b1 :: l' ->
-      add_left l' b
+      iadd_left l' b
   | Right a1 :: _ -> [Right a]
   | Any :: _ -> any
 
-let rec add_right l a = match l with
+let rec iadd_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)
+      i'::(iadd_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
+let iadd l = function
+  | Bounded (a,b) -> iadd_bounded l a b
+  | Left b -> iadd_left l b
+  | Right a -> iadd_right l a
   | Any -> any
 
 let rec neg' start l = match l with
@@ -99,7 +101,7 @@ let neg = function
   | 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
+  List.fold_left iadd i1 i2
 
 let cap i1 i2 =
   neg (cup (neg i1) (neg i2))
@@ -107,7 +109,7 @@ let cap i1 i2 =
 let diff i1 i2 =
   neg (cup (neg i1) i2)
 
-let is_empty i = i = []
+let is_empty = function [] -> true | _ -> false
 
 
 (* TODO: can optimize this to stop running through the list earlier *)
@@ -131,10 +133,10 @@ let print =
        | Any ->
 	   Format.fprintf ppf "Int"
        | Left b -> 
-	   Format.fprintf ppf "minfty--%s" 
+	   Format.fprintf ppf "*--%s" 
 	     (string_of_big_int b)
        | Right a -> 
-	   Format.fprintf ppf "%s--infy" 
+	   Format.fprintf ppf "%s--*" 
 	     (string_of_big_int a)
        | Bounded (a,b) when eq_big_int a b -> 
 	   Format.fprintf ppf "%s" 
@@ -146,3 +148,27 @@ let print =
     )
 
 
+let (+) = add_big_int
+
+
+let add_inter i1 i2 = 
+  match (i1,i2) with
+    | Bounded (a1,b1), Bounded (a2,b2) -> Bounded (a1+a2, b1+b2)
+    | Bounded (_,b1), Left b2 
+    | Left b1, Bounded (_,b2)
+    | Left b1, Left b2 -> Left (b1+b2)
+    | Bounded (a1,_), Right a2 
+    | Right a1, Bounded (a2,_)
+    | Right a1, Right a2 -> Right (a1+a2)
+    | _ -> Any
+
+
+(* Optimize this ... *)
+let add l1 l2 =
+  List.fold_left 
+    (fun accu i1 ->
+       List.fold_left
+	 (fun accu i2 -> iadd accu (add_inter i1 i2))
+	 accu l2
+	 
+    ) empty l1

types/intervals.mli

@@ -18,3 +18,7 @@ val sample : t -> Big_int.big_int
 
 
 val print : t -> (Format.formatter -> unit) list
+
+
+
+val add : t -> t -> t

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.2 2002/10/17 12:30:02 cvscast Exp $ *)
+(* $Id: recursive.ml,v 1.3 2002/10/17 15:38:34 cvscast Exp $ *)
 
 exception NotEqual
 exception Incomplete
@@ -160,5 +160,14 @@ struct
       ignore (internalize nr)
     with Exit -> ()
 
+
   let hash_descr d =  X.hash (fun n -> !n.id) d
+  let equal_descr d1 d2 =
+    (d1 == d2) ||
+    try 
+      X.equal 
+      	(fun n1 n2 -> if !n1.id <> !n2.id then raise NotEqual) 
+	d1 d2; 
+      true
+    with NotEqual -> false
 end

types/recursive.mli

-(* $Id: recursive.mli,v 1.2 2002/10/17 12:30:02 cvscast Exp $ *)
+(* $Id: recursive.mli,v 1.3 2002/10/17 15:38:34 cvscast Exp $ *)
 
 exception NotEqual
 exception Incomplete
@@ -45,5 +45,6 @@ sig
   val descr: node -> descr
 
   val hash_descr: descr -> int
+  val equal_descr: descr -> descr -> bool
 end
 

types/types.ml

@@ -108,7 +108,7 @@ module I = struct
       
   let iter f a =
     ignore (map f a)
-      
+     
   let deep = 4
 end
 
@@ -561,7 +561,7 @@ struct
       struct 
 	type t = descr
 	let hash = hash_descr
-	let equal = (=)
+	let equal = equal_descr
       end
     )
 
@@ -614,9 +614,12 @@ struct
       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
+      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 
@@ -741,6 +744,12 @@ struct
 end
   
 
+module Int = struct
+  let get d = d.ints
+  let put i = { empty with ints = i }
+  let is_int d = is_empty { d with ints = Intervals.empty }
+  let any = { empty with ints = Intervals.any }
+end
 
 (*
 let rec print_normal_record ppf = function

types/types.mli

@@ -16,6 +16,9 @@ val internalize: node -> node
 val id: node -> int
 val descr: node -> descr
 
+val equal_descr: descr -> descr -> bool
+val hash_descr: descr -> int
+
 
 (** Boolean connectives **)
 
@@ -114,6 +117,14 @@ module Arrow : sig
 end
 
 
+module Int : sig
+  val any : descr
+
+  val is_int : descr -> bool
+  val get: descr -> Intervals.t
+  val put: Intervals.t -> descr
+end
+
 val normalize : node -> node
 
 (** Subtyping and sample values **)

typing/typed.ml

@@ -30,8 +30,7 @@ and  texpr' =
   | RecordLitt of (Types.label * texpr) list
       
   (* Data destructors *)
-  | UnaryOp of Op.unary * texpr
-  | BinaryOp of Op.binary * texpr * texpr
+  | Op of string * texpr list
   | Match of texpr * branches
   | Map of texpr * branches
 
@@ -52,4 +51,3 @@ and branch = {
   br_pat : tpat; 
   br_body :  texpr 
 }
-

typing/typer.ml

@@ -335,11 +335,10 @@ let rec expr { loc = loc; descr = d } =
 		       (l,e)
 		    ) r in
 	  (!fv, Typed.RecordLitt r)
-      | UnaryOp (o,e) -> 
-	  let (fv,e) = expr e in (fv, Typed.UnaryOp (o,e))
-      | BinaryOp (o,e1,e2) -> 
-	  let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
-	  (Fv.union fv1 fv2, Typed.BinaryOp (o,e1,e2))
+      | Op (op,le) ->
+	  let (fvs,ltes) = List.split (List.map expr le) in
+	  let fv = List.fold_left Fv.union Fv.empty fvs in
+	  (fv, Typed.Op (op,ltes))
       | Match (e,b) -> 
 	  let (fv1,e) = expr e
 	  and (fv2,b) = branches b in
@@ -419,12 +418,9 @@ and compute_type' loc env = function
 	   let t = Types.record l false (Types.cons t) in
 	   Types.cap accu t
 	) Types.Record.any r
-  | UnaryOp (op,e) -> 
-      let t = compute_type env e in
-      op.Op.un_type loc e.exp_loc t
-  | BinaryOp (op,e1,e2) -> 
-      let t1 = compute_type env e1 and t2 = compute_type env e2 in
-      op.Op.bin_type loc e1.exp_loc t1 e2.exp_loc t2
+  | Op (op, el) ->
+      let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in
+      type_op loc op args
   | Match (e,b) ->
       let t = compute_type env e in
       type_branches loc env t b
@@ -460,3 +456,27 @@ and branches_aux loc env targ tres = function
 	  else
 	    tres
 	)
+
+and type_op loc op args =
+  match (op,args) with
+    | ("+", [loc1,t1; loc2,t2]) ->
+	type_int_binop Intervals.add loc1 t1 loc2 t2
+    | ("*", [loc1,t1; loc2,t2]) ->
+	type_int_binop (fun i1 i2 -> Intervals.any) loc1 t1 loc2 t2
+    | _ -> 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 
+	       (t1,Types.Int.any,
+		"The second argument must be an integer"));
+  Types.Int.put
+    (f (Types.Int.get t1) (Types.Int.get t2));
+  
+