[r2002-10-20 19:07:35 by cvscast] Empty log message

Original author: cvscast
Date: 2002-10-20 19:08:05+00:00

driver/cduce.ml

@@ -17,13 +17,18 @@ let rec print_exn ppf = function
   | Location ((i,j), exn) ->
       Format.fprintf ppf "Error at chars %i-%i@\n" i j;
       print_exn ppf exn
+  | Typer.ShouldHave (t,msg) ->
+      Format.fprintf ppf "This expression should have type %a@\n%s@\n" 
+        Types.Print.print_descr t
+      msg
   | Typer.Constraint (s,t,msg) ->
-      Format.fprintf ppf "%s@\n" msg;
-      Format.fprintf ppf "%a is not a subtype of %a@\n" 
-	Types.Print.print_descr s 
-	Types.Print.print_descr t;
-      Format.fprintf ppf "as shown by %a@\n" 
-	Types.Print.print_sample (Types.Sample.get (Types.diff s t))
+      Format.fprintf ppf "This expression should have type %a@\n" 
+        Types.Print.print_descr t;
+      Format.fprintf ppf "but its infered type is: %a@\n" 
+        Types.Print.print_descr s;
+      Format.fprintf ppf "which is not a subtype, as shown by the value %a@\n" 
+	Types.Print.print_sample (Types.Sample.get (Types.diff s t));
+      Format.fprintf ppf "%s@\n" msg
   | Typer.NonExhaustive t ->
       Format.fprintf ppf "This pattern matching is not exhaustive@\n";
       Format.fprintf ppf "Residual type: %a@\n"
@@ -37,7 +42,7 @@ let phrase ph =
   match ph.descr with
     | Ast.EvalStatement e ->
 	let (fv,e) = Typer.expr e in
-	let t = Typer.compute_type Typer.Env.empty e in
+	let t = Typer.type_check Typer.Env.empty e Types.any true in
 	Format.fprintf ppf "%a@\n" Types.Print.print_descr t;
     | Ast.TypeDecl _ -> ()
     | _ -> assert false

parser/parser.ml

@@ -15,7 +15,7 @@ open Ast
 
   let rec tuple loc = function
     | [ x ] -> x
-    | x :: l -> mk loc (Pair (x, tuple loc l))
+    | x :: l -> mk (x.loc) (Pair (x, tuple loc l))
     | [] -> assert false
 	
   let char = mk noloc (Internal (Types.char Chars.any))
@@ -157,6 +157,8 @@ open Ast
           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 ->
+          mk loc (Internal (Types.char (Chars.char_class i i)))
       | i = char ; "--"; j = char ->
           mk loc (Internal (Types.char (Chars.char_class i j)))
       | c = const -> mk loc (Internal (Types.constant c))

tests/addrbook.cd

+type Content = [(Name Addr Tel?)*];;
+type Addrbook = <addrbook>Content;;
+type Name = <name>[String];;
+type Addr = <addr>[String];;
+type Tel = <tel>[String];;
+
+(*
+<addrbook>[
+  <name>["Haruo Hosoya"]
+  <addr>["Tokyo"]
+  <name>["Benjamin Pierce"]
+  <addr>["Philadelphia"] 
+  <tel>["123-456-789"]
+  <name>["Peter Buneman"]
+  <addr>["Scotland"]
+ ];;
+*)
+
+(* converting an address book into a telephone list *)
+
+(*
+fun mkTelList ([ (Name Addr Tel?)* ] -> [ (Name Tel)* ])
+| [ <name>n <addr>a <tel>t ; rest] -> [ <name>n <tel>t ; mkTelList rest] 
+| [ <name>n <addr>a; rest] -> mkTelList rest
+| [ ] -> [ ]
+;;
+
+fun mkTelList (Addrbook -> [ (Name Tel)* ])
+<_>[ ( ( (x::Name) Addr (x::Tel) ) | _ )* ] ->  x
+;;
+*)
+
+(*
+fun (Int -> Addrbook) x ->
+<addrbook>[
+  <name>["Haruo Hosoya"]
+  <addr>["Tokyo"]
+  <name>["Benjamin Pierce"]
+  <addr>["Philadelphia"] 
+  <tel>["123-456-789"]
+  <name>["Peter Buneman"]
+  <addr>["Scotland"]
+ ] 
+;;
+*)
+
+match <addrbook>[
+  <name>["Haruo Hosoya"]
+  <addr>["Tokyo"]
+  <name>["Benjamin Pierce"]
+  <addr>["Philadelphia"] 
+  <tel>["123-456-789"]
+  <name>["Peter Buneman"]
+  <addr>["Scotland"]
+ ] with
+<_>[ ( ( (x::Name) Addr (x::Tel) ) | _ )* ] ->  x;;
+
+(*
+(* the pattern extract the full sequence of subelements *)
+match ex with addrbook:[;a] -> mkTelList a;;
+*)

types/patterns.ml

@@ -706,13 +706,15 @@ test_filter "[ (1 2 3?)* ]" "[ (x::(1 2) 3?)* ]";;
 *)
 
 (*
-let pat s = Patterns.descr (Syntax.make_pat (Syntax.parse s));;
-let typ s = Types.descr (Syntax.make_type (Syntax.parse s));;
+let pat s = Patterns.descr (Typer.pat (Parser.From_string.pat s));;
+let typ s = Types.descr (Typer.typ (Parser.From_string.pat s));;
 let f s = Patterns.NF.nf (pat s);;
 let show' t l = Patterns.NF.show Format.std_formatter t (List.map f l);;
 let show l = show' Types.any l;;
 let showt t l = show' (typ t) l;;
 
+ showt " [(`A `B `C?)*] "  [" [ (((x::`A) `B (x::`C))|_)* ] "];;
+
 show ["{x=2;y=3}"];;
 show [" [((x::1)|(y::2))*] "];;
 

types/types.ml

@@ -382,6 +382,8 @@ struct
   let other d = { d with times = empty.times }
   let is_product d = is_empty (other d)
 
+  let need_second = function _::_::_ -> true | _ -> false
+
   let get d =
     let line accu (left,right) =
       let rec aux accu d1 d2 = function
@@ -437,6 +439,7 @@ struct
     List.map (!) !res
 
   let any = { empty with times = any.times }
+  let is_empty d = d = []
 end
 
 
@@ -701,6 +704,31 @@ end
 
 module Arrow =
 struct
+  let check_simple left s1 s2 =
+    let rec aux accu1 accu2 = function
+      | (t1,t2)::left ->
+          let accu1' = diff_t accu1 t1 in
+          if not (empty_rec accu1') then aux accu1 accu2 left;
+          let accu2' = cap_t accu2 t2 in
+          if not (empty_rec accu2') then aux accu1 accu2 left
+      | [] -> raise NotEmpty
+    in
+    let accu1 = descr s1 in
+    (is_empty accu1) ||
+    (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
+      
+  let check_strenghten t s =
+    let left = match t.arrow with [ (p,[]) ] -> p | _ -> assert false in
+    let rec aux = function
+      | [] -> raise Not_found
+      | (p,n) :: rem ->
+	  if (List.for_all (fun (a,b) -> check_simple left a b) p) &&
+	    (List.for_all (fun (a,b) -> not (check_simple left a b)) n) then
+	      { empty with arrow = [ (SortedList.cup left p, n) ] }
+	  else aux rem
+    in
+    aux s.arrow
+
   type t = descr * (descr * descr) list list
 
   let get t =
@@ -742,7 +770,20 @@ struct
   let apply (_,arr) t =
     List.fold_left (apply_simple t) empty arr
 
+  let need_arg (dom, arr) =
+    List.exists (function [_] -> false | _ -> true) arr
+
+  let apply_noarg (_,arr) =
+    List.fold_left 
+      (fun accu -> 
+	 function 
+	   | [(t,s)] -> cup accu s
+	   | _ -> assert false
+      )
+      empty arr
+
   let any = { empty with arrow = any.arrow }
+  let is_empty (_,arr) = arr = []
 end
   
 

types/types.mli

@@ -72,6 +72,7 @@ module Product : sig
 
   (* List of non-empty rectangles *)
   type t = (descr * descr) list
+  val is_empty: t -> bool
   val get: descr -> t
   val pi1: t -> descr
   val pi2: t -> descr
@@ -82,7 +83,10 @@ module Product : sig
   (* List of non-empty rectangles whose first projection
      are pair-wise disjunct *)
   type normal = t
-  val normal: descr -> t
+  val normal: descr -> normal
+
+  val need_second: t -> bool
+    (* Is there more than a single rectangle ? *)
 end
 
 module Record : sig
@@ -110,13 +114,28 @@ end
 module Arrow : sig
   val any : descr
 
+  val check_strenghten: descr -> descr -> descr
+    (* [check_strenghten t s]
+       Assume that [t] is an intersection of arrow types
+       representing the interface of an abstraction;
+       check that this abstraction has type [s] (otherwise raise Not_found)
+       and returns a refined type for this abstraction.
+    *)
+
   type t
+  val is_empty: t -> bool
   val get: descr -> t
     (* Always succeed; no check <= Arrow.any *)
 
   val domain: t -> descr
   val apply: t -> descr -> descr
     (* Always succeed; no check on the domain *)
+
+  val need_arg : t -> bool
+    (* True if the type of the argument is needed to obtain
+       the type of the result (must use [apply]; otherwise,
+       [apply_noarg] is enough *)
+  val apply_noarg : t -> descr
 end
 
 

typing/typed.ml

@@ -46,6 +46,7 @@ and abstr = {
 
 and branches = { 
   mutable br_typ : Types.descr;
+  br_accept : Types.descr;
   br_branches: branch list
 }
 and branch = { 

typing/typer.ml

@@ -7,6 +7,7 @@ open Ast
 exception Pattern of string
 exception NonExhaustive of Types.descr
 exception Constraint of Types.descr * Types.descr * string
+exception ShouldHave of Types.descr * string
 
 let raise_loc loc exn = raise (Location (loc,exn))
 
@@ -357,15 +358,24 @@ let rec expr { loc = loc; descr = d } =
 	      
   and branches b = 
     let fv = ref Fv.empty in
+    let accept = ref Types.empty in
     let b = List.map 
 	      (fun (p,e) ->
 		 let (fv2,e) = expr e in
 		 fv := Fv.union !fv fv2;
+		 let p = pat p in
+		 accept := Types.cup !accept (Types.descr (Patterns.accept p));
 		 { Typed.br_used = false;
-		   Typed.br_pat = pat p;
+		   Typed.br_pat = p;
 		   Typed.br_body = e }
 	      ) b in
-    (!fv, { Typed.br_typ = Types.empty; Typed.br_branches = b } )
+    (!fv, 
+     { 
+       Typed.br_typ = Types.empty; 
+       Typed.br_branches = b; 
+       Typed.br_accept = !accept 
+     } 
+    )
 
 module Env = StringMap
 
@@ -375,48 +385,68 @@ 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
+let rec type_check env e 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
 
-and compute_type' loc env = function
-  | DebugTyper t -> Types.descr t
-  | Var s -> Env.find s env
-  | Apply (e1,e2) ->
-      let t1 = compute_type env e1 and t2 = compute_type env e2 in
-      if Types.is_empty t2 
-      then Types.empty
-      else 
-	if Types.subtype t1 Types.Arrow.any 
-	then
-	  let t1 = Types.Arrow.get t1 in
-	  let dom = Types.Arrow.domain t1 in
-	  if Types.subtype t2 dom
-	  then Types.Arrow.apply t1 t2
-	  else
-	    raise_loc loc 
-	      (Constraint 
-		 (t2,dom,"The argument is not in the domain of the function"))
-	else
-	  raise_loc loc
-	    (Constraint
-	       (t1,Types.Arrow.any,"The expression in function position is not necessarily a function"))
+and type_check' loc env e constr precise = match e with
   | Abstraction a ->
+      let t =
+	try Types.Arrow.check_strenghten a.fun_typ constr 
+	with Not_found -> 
+	  raise_loc loc 
+	  (ShouldHave
+	     (constr, "but the interface of the abstraction is not compatible"))
+      in
       let env = match a.fun_name with
 	| None -> env
 	| Some f -> Env.add f a.fun_typ env in
-      List.iter (fun (t1,t2) ->
-		   let t = type_branches loc env t1 a.fun_body in
-		   if not (Types.subtype t t2) then
-		     raise_loc loc (Constraint (t,t2,"Constraint not satisfied in interface"))
-		) a.fun_iface;
-      a.fun_typ
-  | Cst c -> Types.constant c
+      List.iter 
+	(fun (t1,t2) ->
+	   ignore (type_check_branches loc env t1 a.fun_body t2 false)
+	) a.fun_iface;
+      t
+  | Match (e,b) ->
+      let t = type_check env e b.br_accept true in
+      type_check_branches loc env t b constr precise
   | Pair (e1,e2) -> 
-      let t1 = compute_type env e1 and t2 = compute_type env e2 in
-      let t1 = Types.cons t1 and t2 = Types.cons t2 in
-      Types.times t1 t2
+      let rects = Types.Product.get constr in
+      if Types.Product.is_empty rects then 
+	raise_loc loc (ShouldHave (constr,"but it is a pair."));
+      let pi1 = Types.Product.pi1 rects in
+
+      let t1 = type_check env e1 (Types.Product.pi1 rects) 
+		 (precise || (Types.Product.need_second rects))in
+      let rects = Types.Product.restrict_1 rects t1 in
+      let t2 = type_check env e2 (Types.Product.pi2 rects) precise in
+      if precise then 
+	Types.times (Types.cons t1) (Types.cons t2)
+      else
+	constr
+  | _ -> 
+      let t : Types.descr = compute_type' loc env e in
+      check loc t constr "";
+      t
+
+and compute_type env e =
+  type_check env e Types.any true
+
+and compute_type' loc env = function
+  | DebugTyper t -> Types.descr t
+  | Var s -> Env.find s env
+  | Apply (e1,e2) ->
+      let t1 = type_check env e1 Types.Arrow.any true in
+      let t1 = Types.Arrow.get t1 in
+      let dom = Types.Arrow.domain t1 in
+      if Types.Arrow.need_arg t1 then
+	let t2 = type_check env e2 dom true in
+	Types.Arrow.apply t1 t2
+      else
+	(ignore (type_check env e2 dom false); Types.Arrow.apply_noarg t1)
+  | Cst c -> Types.constant c
   | RecordLitt r ->
       List.fold_left 
 	(fun accu (l,e) ->
@@ -427,21 +457,21 @@ and compute_type' loc env = function
   | 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
   | Map (e,b) ->
       let t = compute_type env e in
-      Sequence.map (fun t -> type_branches loc env t b) t
+      Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t
+  | _ -> assert false
 
-and type_branches loc env targ brs =
+and type_check_branches loc env targ brs constr precise =
   if Types.is_empty targ then Types.empty 
   else (
     brs.br_typ <- Types.cup brs.br_typ targ;
-    branches_aux loc env targ Types.empty brs.br_branches
+    branches_aux loc env targ 
+      (if precise then Types.empty else constr) 
+      constr precise brs.br_branches
   )
     
-and branches_aux loc env targ tres = function
+and branches_aux loc env targ tres constr precise = function
   | [] -> raise_loc loc (NonExhaustive targ)
   | b :: rem ->
       let p = b.br_pat in
@@ -449,18 +479,18 @@ and branches_aux loc env targ tres = function
 
       let targ' = Types.cap targ acc in
       if Types.is_empty targ' 
-      then branches_aux loc env targ tres rem
+      then branches_aux loc env targ tres constr precise rem
       else 
 	( b.br_used <- true;
 	  let res = Patterns.filter targ' p in
 	  let env' = List.fold_left 
 		       (fun env (x,t) -> Env.add x (Types.descr t) env) 
 		       env res in
-	  let t = compute_type env' b.br_body in
-	  let tres = Types.cup t tres in
+	  let t = type_check env' b.br_body constr precise in
+	  let tres = if precise then Types.cup t tres else tres in
 	  let targ'' = Types.diff targ acc in
 	  if (Types.non_empty targ'') then 
-	    branches_aux loc env targ'' (Types.cup t tres) rem 
+	    branches_aux loc env targ'' tres constr precise rem 
 	  else
 	    tres
 	)

typing/typer.mli

 exception Pattern of string
 exception NonExhaustive of Types.descr
 exception Constraint of Types.descr * Types.descr * string
+exception ShouldHave of Types.descr * string
 
 val compile_regexp : Ast.regexp -> Ast.ppat -> Ast.ppat
 
@@ -15,4 +16,10 @@ module Env : Map.S with type key = string
 
 val expr: Ast.pexpr -> Fv.t * Typed.texpr
 
-val compute_type: Types.descr Env.t -> Typed.texpr -> Types.descr
+val type_check: 
+  Types.descr Env.t -> Typed.texpr -> Types.descr -> bool -> Types.descr
+  (* [compute_type env e t precise] checks that expression [e] 
+     has type [t] under typing environment [env]; if [precise=true], 
+     also returns a possible more precise type for [e].
+  *)
+