[r2002-10-21 21:12:57 by cvscast] Empty log message

Original author: cvscast
Date: 2002-10-21 21:12:57+00:00

Makefile

@@ -47,11 +47,11 @@ run_top: all.cma
 	ledit ocaml $(INCLUDES) all.cma
 
 clean:
-	(cd parser; rm -f *.cmi *.cmo *.cma *~)
-	(cd types; rm -f *.cmi *.cmo *.cma *~)
-	(cd typing; rm -f *.cmi *.cmo *.cma *~)
-	(cd driver; rm -f *.cmi *.cmo *.cma *~)
-	rm -f *.cmi *.cmo *.cma *~
+	(cd parser; rm -f *.cmi *.cmo *.cma *.cmx *.o *~)
+	(cd types; rm -f *.cmi *.cmo *.cma *.cmx *.o *~)
+	(cd typing; rm -f *.cmi *.cmo *.cma *.cmx *.o *~)
+	(cd driver; rm -f *.cmi *.cmo *.cma *.cmx *.o *~)
+	rm -f *.cmi *.cmo *.cma *.cmx *.o *~
 	rm -f cduce
 
 .SUFFIXES: .ml .mli .cmo .cmi .cmx

types/sequence.ml

@@ -5,49 +5,23 @@ let decompose t =
   (Types.Atom.has_atom t nil_atom,
    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 =
+  let rec aux 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 = List.map (fun (t1,t2) -> f t1 (aux 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
+  aux t
   
 
 let aux_concat = mapping (fun t v -> V.times (V.ty t) v)
@@ -65,10 +39,26 @@ let recurs f =
   Types.define n (f n);
   Types.internalize n
 
-let star t = recurs (fun n -> Types.cup nil_type (Types.times t n ))
+let star_node t = recurs (fun n -> Types.cup nil_type (Types.times t n ))
 
-let any_node = star (Types.cons Types.any)
+let any_node = star_node (Types.cons Types.any)
 let any = Types.descr any_node
-let seqseq = Types.descr (star any_node)
+let seqseq = Types.descr (star_node any_node)
+
+let star t = Types.descr (star_node (Types.cons t))
+  
+
+let approx t =
+  let memo = H.create 13 in
+  let res = ref Types.empty in
+  let rec aux t =
+    try H.find memo t
+    with Not_found ->
+      H.add memo t ();
+      let rect = Types.Product.get t in
+      List.iter (fun (t1,t2) -> res := Types.cup t1 !res; aux t2) rect;
+  in
+  aux t;
+  !res
 
   

types/sequence.mli

@@ -6,3 +6,15 @@ 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
+
+
+val star: Types.descr -> Types.descr
+  (* For a type t, returns [t*] *)
+
+val approx: Types.descr -> Types.descr
+  (*  For a type t <= [Any*], returns the least type s such that:
+      t <= [s*]
+      
+      In general, for an arbitrary type, returns the least type s such that:
+      t <= (X where X = (s, X) |  Any \ (Any,Any))
+  *)

typing/typer.ml

@@ -398,8 +398,9 @@ let check loc t s msg =
   if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg))
 
 let rec type_check env e constr precise = 
- (* Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
-    Types.Print.print_descr constr precise;  *)
+(*  Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
+    Types.Print.print_descr constr precise; 
+*)
   let d = type_check' e.exp_loc env e.exp_descr constr precise in
   e.exp_typ <- Types.cup e.exp_typ d;
   d
@@ -469,6 +470,43 @@ and type_check' loc env e constr precise = match e with
       in
       res
 
+  | Map (e,b) ->
+      let t = type_check env e (Sequence.star b.br_accept) true in
+
+      let constr' = Sequence.approx (Types.cap Sequence.any constr) in
+      let exact = Types.subtype (Sequence.star constr') constr in
+
+      if exact then
+	let res = type_check_branches loc env t b constr' precise in
+	if precise then Sequence.star res else constr
+      else
+	(* Note: 
+	   - could be more precise by integrating the decomposition
+	   of constr inside Sequence.map.
+	*)
+	let res = 
+	  Sequence.map 
+	    (fun t -> type_check_branches loc env t b constr' true) 
+	    t in
+	if not exact then check loc res constr "";
+	if precise then res else constr
+  | Op ("@", [e1;e2]) ->
+      let constr' = Sequence.star 
+		      (Sequence.approx (Types.cap Sequence.any constr)) in
+      let exact = Types.subtype constr' constr in
+      if exact then
+	let t1 = type_check env e1 constr' precise
+	and t2 = type_check env e2 constr' precise in
+	if precise then Sequence.concat t1 t2 else constr
+      else
+	(* Note:
+	   the knownledge of t1 may makes it useless to
+	   check t2 with 'precise' ... *)
+	let t1 = type_check env e1 constr' true
+	and t2 = type_check env e2 constr' true in
+	let res = Sequence.concat t1 t2 in
+	check loc res constr "";
+	if precise then res else constr
   | _ -> 
       let t : Types.descr = compute_type' loc env e in
       check loc t constr "";