[r2002-10-19 15:56:14 by cvscast] Empty log message

Original author: cvscast
Date: 2002-10-19 15:56:15+00:00

Makefile

@@ -6,7 +6,8 @@ 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/patterns.cmo \
+	 types/sequence.cmo
 
 DRIVER = driver/cduce.cmo
 

depend

@@ -10,11 +10,11 @@ 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/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 
+    types/patterns.cmi types/sequence.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 
+    types/patterns.cmx types/sequence.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 
@@ -30,6 +30,8 @@ types/patterns.cmx: types/sortedList.cmx types/sortedMap.cmx types/types.cmx \
     types/patterns.cmi 
 types/recursive.cmo: types/recursive.cmi 
 types/recursive.cmx: types/recursive.cmi 
+types/sequence.cmo: types/types.cmi types/sequence.cmi 
+types/sequence.cmx: types/types.cmx types/sequence.cmi 
 types/sortedList.cmo: types/sortedList.cmi 
 types/sortedList.cmx: types/sortedList.cmi 
 types/sortedMap.cmo: types/sortedMap.cmi 
@@ -48,6 +50,7 @@ types/types.cmx: types/atoms.cmx types/boolean.cmx types/chars.cmx \
     types/sortedMap.cmx types/types.cmi 
 types/boolean.cmi: types/sortedList.cmi 
 types/patterns.cmi: types/sortedList.cmi types/sortedMap.cmi types/types.cmi 
+types/sequence.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/intervals.cmi types/sortedMap.cmi 

driver/cduce.ml

@@ -19,6 +19,12 @@ let rec print_exn ppf = function
 	Types.Print.print_descr t;
       Format.fprintf ppf "as shown by %a@\n" 
 	Types.Print.print_sample (Types.Sample.get (Types.diff s t))
+  | Typer.NonExhaustive t ->
+      Format.fprintf ppf "This pattern matching is not exhaustive@\n";
+      Format.fprintf ppf "Residual type: %a@\n"
+	Types.Print.print_descr t;
+      Format.fprintf ppf "Sample value: %a@\n" 
+	Types.Print.print_sample (Types.Sample.get t)
   | exn ->
       Format.fprintf ppf "%s@\n" (Printexc.to_string exn)
 
@@ -42,5 +48,5 @@ let () =
 	) [] p in
     Typer.register_global_types type_decls;
     List.iter phrase p
-  with exn -> print_exn ppf exn
+  with (Failure _) as e -> raise e | exn -> print_exn ppf exn
 	

parser/parser.ml

@@ -36,6 +36,8 @@ open Ast
     "top" RIGHTA
     [ "match"; e = SELF; "with"; b = branches -> mk loc (Match (e,b))
     | "map"; e = SELF; "with"; b = branches -> mk loc (Map (e,b))
+    | "transform"; e = SELF; "with"; b = branches -> 
+	mk noloc (Op ("flatten", [mk loc (Map (e,b))]))
     | "fun"; f = OPT LIDENT; "("; a = LIST1 arrow SEP ";"; ")";
       b = branches -> 
 	mk loc (Abstraction { fun_name = f; fun_iface = a; fun_body = b })
@@ -44,11 +46,13 @@ open Ast
     ]
 
     |
-    [ e1 = expr; e2 = expr -> mk loc (Apply (e1,e2))
+    [ LIDENT "flatten"; e = expr -> mk loc (Op ("flatten",[e]))
+    | e1 = expr; e2 = expr -> mk loc (Apply (e1,e2))
     ]
     
     | 
-    [ e1 = expr; "+"; e2 = expr -> mk loc (Op ("+",[e1;e2]))  ]
+    [ e1 = expr; "+"; e2 = expr -> mk loc (Op ("+",[e1;e2]))  
+    | e1 = expr; "@"; e2 = expr -> mk loc (Op ("@",[e1;e2])) ]
     |
     [ e1 = expr; "*"; e2 = expr -> mk loc (Op ("*",[e1;e2]))  ]
 

types/sequence.ml

+let atom_nil = Types.mk_atom "nil"
+let type_nil = Types.atom atom_nil
+
+let decompose t =
+  (Types.Atom.has_atom t atom_nil,
+   Types.Product.get t)
+
+(*
+let memo_concat = Types.DescrHash.create 63
+
+let rec aux_concat t s =
+  try Types.DescrHash.find memo_concat t
+  with Not_found ->
+    let n = Types.make () in
+    Types.DescrHash.add memo_concat t n;
+    let (has_nil,rect) = decompose t in
+    let d = List.fold_left
+	      (fun accu (t1,t2) ->
+		 Types.cup accu (Types.times (Types.cons t1) (aux_concat t2 s))
+	      )
+	      (if has_nil then s else Types.empty)
+	      rect
+    in
+    Types.define n d;
+    n
+
+let concat t s =
+  let n = aux_concat t s in
+  Types.DescrHash.clear memo_concat;
+  Types.descr (Types.internalize n)
+*)
+
+module V = Types.Positive
+module H = Types.DescrHash
+
+let mapping f t queue =
+  let memo = H.create 13 in
+  let rec aux_map t =
+    try H.find memo t
+    with Not_found ->
+      let v = V.forward () in
+      H.add memo t v;
+      let (has_nil,rect) = decompose t in
+      let l = List.map (fun (t1,t2) -> f t1 (aux_map t2)) rect in
+      let l = if has_nil then queue :: l else l in
+      V.define v (V.cup l);
+      v
+
+  in
+  aux_map t
+  
+
+let aux_concat = mapping (fun t v -> V.times (V.ty t) v)
+let aux_flatten t = mapping aux_concat t (V.ty type_nil)
+let aux_map f t = mapping (fun t v -> V.times (V.ty (f t)) v) t (V.ty type_nil)
+
+let solve x = Types.descr (V.solve x)
+
+let concat t1 t2 = solve (aux_concat t1 (V.ty t2))
+let flatten t = solve (aux_flatten t)
+let map f t = solve (aux_map f t)
+
+let recurs f =
+  let n = Types.make () in
+  Types.define n (f n);
+  Types.internalize n
+
+let star t = recurs (fun n -> Types.cup type_nil (Types.times t n ))
+
+let any_node = star (Types.cons Types.any)
+let any = Types.descr any_node
+let seqseq = Types.descr (star any_node)
+
+  

types/sequence.mli

+val any: Types.descr
+val seqseq: Types.descr
+
+val concat: Types.descr -> Types.descr -> Types.descr
+val flatten: Types.descr -> Types.descr
+val map: (Types.descr -> Types.descr) -> Types.descr -> Types.descr

types/types.ml

@@ -52,7 +52,7 @@ module I = struct
   let any_record = { empty with record = any.record }
 
   let cup x y = 
-    if x = y then x else { 
+    if x == y then x else { 
       times = Boolean.cup x.times y.times;
       arrow = Boolean.cup x.arrow y.arrow;
       record= Boolean.cup x.record y.record;
@@ -62,7 +62,7 @@ module I = struct
     }
       
   let cap x y = 
-    if x = y then x else {
+    if x == y then x else {
       times = Boolean.cap x.times y.times;
       record= Boolean.cap x.record y.record;
       arrow = Boolean.cap x.arrow y.arrow;
@@ -72,7 +72,7 @@ module I = struct
     }
       
   let diff x y = 
-    if x = y then empty else { 
+    if x == y then empty else { 
       times = Boolean.diff x.times y.times;
       arrow = Boolean.diff x.arrow y.arrow;
       record= Boolean.diff x.record y.record;
@@ -380,6 +380,9 @@ module Product =
 struct
   type t = (descr * descr) list
 
+  let other d = { d with times = empty.times }
+  let is_product d = is_empty (other d)
+
   let get d =
     let line accu (left,right) =
       let rec aux accu d1 d2 = function
@@ -554,17 +557,17 @@ let rec rec_normalize d =
 let normalize n =
   internalize (rec_normalize (descr n))
 
+module DescrHash = 
+  Hashtbl.Make(
+    struct 
+      type t = descr
+      let hash = hash_descr
+      let equal = equal_descr
+    end
+  )
+
 module Print =
 struct
-  module DescrHash = 
-    Hashtbl.Make(
-      struct 
-	type t = descr
-	let hash = hash_descr
-	let equal = equal_descr
-      end
-    )
-
   let named = DescrHash.create 10
   let register_global name d = DescrHash.add named d name
 
@@ -751,6 +754,10 @@ module Int = struct
   let any = { empty with ints = Intervals.any }
 end
 
+module Atom = struct
+  let has_atom d a = Atoms.contains a d.atoms
+end
+
 (*
 let rec print_normal_record ppf = function
   | Success -> Format.fprintf ppf "Yes"

types/types.mli

@@ -20,6 +20,8 @@ val equal_descr: descr -> descr -> bool
 val hash_descr: descr -> int
 
 
+module DescrHash: Hashtbl.S with type key = descr
+
 (** Boolean connectives **)
 
 val cup    : descr -> descr -> descr
@@ -66,6 +68,8 @@ val label_name : label -> string
 
 module Product : sig
   val any : descr
+  val other : descr -> descr
+  val is_product : descr -> bool
 
   (* List of non-empty rectangles *)
   type t = (descr * descr) list
@@ -125,6 +129,10 @@ module Int : sig
   val put: Intervals.t -> descr
 end
 
+module Atom : sig
+  val has_atom : descr -> atom -> bool
+end
+
 val normalize : node -> node
 
 (** Subtyping and sample values **)

typing/typer.ml

@@ -370,6 +370,10 @@ module Env = StringMap
 
 open Typed
 
+
+let check loc t s msg =
+  if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg))
+
 let rec compute_type env e = 
   let d = compute_type' e.exp_loc env e.exp_descr in
   e.exp_typ <- Types.cup e.exp_typ d;
@@ -424,7 +428,9 @@ and compute_type' loc env = function
   | Match (e,b) ->
       let t = compute_type env e in
       type_branches loc env t b
-  | Map (e,b) -> assert false
+  | Map (e,b) ->
+      let t = compute_type env e in
+      Sequence.map (fun t -> type_branches loc env t b) t
 
 and type_branches loc env targ brs =
   if Types.is_empty targ then Types.empty 
@@ -463,6 +469,14 @@ and type_op loc op args =
 	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
+    | ("@", [loc1,t1; loc2,t2]) ->
+	check loc1 t1 Sequence.any
+	  "The first argument of @ must be a sequence";
+	Sequence.concat t1 t2
+    | ("flatten", [loc1,t1]) ->
+	check loc1 t1 Sequence.seqseq 
+	  "The argument of flatten must be a sequence of sequences";
+	Sequence.flatten t1
     | _ -> assert false
 
 and type_int_binop f loc1 t1 loc2 t2 =