--- typing/typer.ml	2007/07/10 16:57:19	9
+++ typing/typer.ml	2007/07/10 17:00:52	47
@@ -6,7 +6,11 @@
 
 exception Pattern of string
 exception NonExhaustive of Types.descr
+exception MultipleLabel of Types.label
 exception Constraint of Types.descr * Types.descr * string
+exception ShouldHave of Types.descr * string
+exception WrongLabel of Types.descr * Types.label
+exception UnboundId of string
 
 let raise_loc loc exn = raise (Location (loc,exn))
 
@@ -42,11 +46,11 @@
 
 let mk' =
   let counter = ref 0 in
-  fun () ->
+  fun loc ->
     incr counter;
     let rec x = { 
       id = !counter; 
-      loc' = noloc; 
+      loc' = loc; 
       fv = None; 
       descr' = `Alias ("__dummy__", x);  
       type_node = None; 
@@ -55,8 +59,7 @@
     x
 
 let cons loc d =
-  let x = mk' () in
-  x.loc' <- loc;
+  let x = mk' loc in
   x.descr' <- d;
   x
     
@@ -158,14 +161,7 @@
        with Not_found -> 
 	 raise_loc loc (Pattern ("Undefined type variable " ^ s))
       )
-  | Recurs (t, b) ->
-      let b = List.map (fun (v,t) -> (v,t,mk' ())) b in
-      let env = 
-	List.fold_left (fun env (v,t,x) -> StringMap.add v x env) env b in
-      List.iter 
-	(fun (v,t,x) -> x.loc' <- t.loc; x.descr' <- `Alias (v, compile env t)) 
-	b;
-      compile env t
+  | Recurs (t, b) -> compile (compile_many env b) t
   | Regexp (r,q) -> compile env (Regexp.compile r q)
   | Internal t -> cons loc (`Type t)
   | Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2))
@@ -177,6 +173,14 @@
   | Constant (x,v) -> cons loc (`Constant (x,v))
   | Capture x -> cons loc (`Capture x)
 
+and compile_many env b = 
+  let b = List.map (fun (v,t) -> (v,t,mk' t.loc)) b in
+  let env = 
+    List.fold_left (fun env (v,t,x) -> StringMap.add v x env) env b in
+  List.iter (fun (v,t,x) -> x.descr' <- `Alias (v, compile env t)) b;
+  env
+
+
 let rec comp_fv seen s =
   match s.fv with
     | Some l -> l
@@ -266,16 +270,28 @@
 	Patterns.define x t;
 	x
 
-let typ e =
-  let e = compile StringMap.empty e in
+let global_types = ref StringMap.empty
+
+let mk_typ e =
   if fv e = [] then type_node e 
-  else (raise_loc e.loc' 
-	  (Pattern "Capture variables are not allowed in types"))
+  else raise_loc e.loc' (Pattern "Capture variables are not allowed in types")
+    
+
+let typ e =
+  mk_typ (compile !global_types e)
 
 let pat e =
-  let e = compile StringMap.empty e in
+  let e = compile !global_types e in
   pat_node e
 
+let register_global_types b =
+  let env = compile_many !global_types b in
+  List.iter (fun (v,_) -> 
+	       let d = Types.descr (mk_typ (StringMap.find v env)) in
+	       let d = Types.normalize d in
+	       Types.Print.register_global v d
+	    ) b;
+  global_types := env
 
 
 (* II. Build skeleton *)
@@ -285,6 +301,7 @@
 let rec expr { loc = loc; descr = d } = 
   let (fv,td) = 
     match d with
+      | DebugTyper t -> (Fv.empty, Typed.DebugTyper (typ t))
       | Var s -> (Fv.singleton s, Typed.Var s)
       | Apply (e1,e2) -> 
 	  let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
@@ -314,18 +331,27 @@
       | Pair (e1,e2) ->
 	  let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
 	  (Fv.union fv1 fv2, Typed.Pair (e1,e2))
+      | Dot (e,l) ->
+	  let (fv,e) = expr e in
+	  (fv,  Typed.Dot (e,l))
       | RecordLitt r -> 
-	  (* XXX TODO: check that no label appears twice *)
 	  let fv = ref Fv.empty in
+	  let r  = List.sort (fun (l1,_) (l2,_) -> compare l1 l2) r in
 	  let r = List.map 
 		    (fun (l,e) -> 
-		       let (fv2,e) = expr e in
-		       fv := Fv.union !fv fv2;
-		       (l,e)
-		    ) r in
+		       let (fv2,e) = expr e in fv := Fv.union !fv fv2; (l,e))
+		    r in
+	  let rec check = function
+	    | (l1,_) :: (l2,_) :: _ when l1 = l2 -> 
+		raise_loc loc (MultipleLabel l1)
+	    | _ :: rem -> check rem
+	    | _ -> () in
+	  check r;
 	  (!fv, Typed.RecordLitt r)
-      | Op (o,e) -> 
-	  let (fv,e) = expr e in (fv, Typed.Op (o,e))
+      | 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
@@ -343,66 +369,224 @@
 	      
   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;
+       Typed.br_compiled = None;
+     } 
+    )
 
 module Env = StringMap
 
 open Typed
 
-let rec compute_type env e = 
-  let d = compute_type' e.exp_loc env e.exp_descr in
+
+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; 
+*)
+  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
-  | Var s -> Env.find s env
-  | Apply (e1,e2) ->
-      let t1 = compute_type env e1 and t2 = compute_type env e2 in
-      Types.apply t1 t2
+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
+      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 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
+
+  | RecordLitt r ->
+      let rconstr = Types.Record.get constr in
+      if Types.Record.is_empty rconstr then
+	raise_loc loc (ShouldHave (constr,"but it is a record."));
+
+      let (rconstr,res) = 
+	List.fold_left 
+	  (fun (rconstr,res) (l,e) ->
+	     let rconstr = Types.Record.restrict_label_present rconstr l in
+	     let pi = Types.Record.project_field rconstr l in
+	     if Types.Record.is_empty rconstr then
+	       raise_loc loc 
+		 (ShouldHave (constr,(Printf.sprintf 
+					"Field %s is not allowed here."
+					(Types.label_name l)
+				     )
+			     ));
+	     let t = type_check env e pi true in
+	     let rconstr = Types.Record.restrict_field rconstr l t in
+	     
+	     let res = 
+	       if precise 
+	       then Types.cap res (Types.record l false (Types.cons t))
+	       else res in
+	     (rconstr,res)
+	  ) (rconstr, if precise then Types.Record.any else constr) r
+      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 (
+	(* Note: typing mail fail because of the approx on t *)
+	let res = type_check_branches loc env (Sequence.approx 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
+  | Op ("flatten", [e]) ->
+      let constr' = Sequence.star 
+		      (Sequence.approx (Types.cap Sequence.any constr)) in
+      let sconstr' = Sequence.star constr' in
+      let exact = Types.subtype constr' constr in
+      if exact then
+	let t = type_check env e sconstr' precise in
+	if precise then Sequence.flatten t else constr
+      else
+	let t = type_check env e sconstr' true in
+	let res = Sequence.flatten t 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 "";
+      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 -> 
+      (try Env.find s env 
+       with Not_found -> raise_loc loc (UnboundId s)
+      )
+  | 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
+  | Dot (e,l) ->
+      let t = type_check env e Types.Record.any true in
+         (try (Types.Record.project t l) 
+          with Not_found -> raise_loc loc (WrongLabel(t,l)))
+  | Op (op, el) ->
+      let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in
+      type_op loc op args
+  | Map (e,b) ->
+      let t = compute_type env e in
+      Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t
+
+(* We keep these cases here to allow comparison and benchmarking ...
+   Just comment the corresponding cases in type_check' to
+   activate these ones.
+*)
   | 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 t1 = compute_type env e1 
+      and t2 = compute_type env e2 in
+      Types.times (Types.cons t1) (Types.cons t2)
   | RecordLitt r ->
       List.fold_left 
-	(fun accu (l,e) ->
-	   let t = compute_type env e in
-	   let t = Types.record l false (Types.cons t) in
-	   Types.cap accu t
-	) Types.Record.any r
-  | Op (op,e) -> assert false
-  | Match (e,b) ->
-      let t = compute_type env e in
-      type_branches loc env t b
-  | Map (e,b) -> assert false
+        (fun accu (l,e) ->
+           let t = compute_type env e in
+           let t = Types.record l false (Types.cons t) in
+           Types.cap accu t
+        ) Types.Record.any r
 
-and type_branches loc env targ brs =
+
+  | _ -> assert false
+
+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
@@ -410,18 +594,50 @@
 
       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
 	)
+
+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
+    | ("@", [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 =
+  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 
+	       (t2,Types.Int.any,
+		"The second argument must be an integer"));
+  Types.Int.put
+    (f (Types.Int.get t1) (Types.Int.get t2));
+  
+