[r2002-10-10 16:39:45 by cvscast] Empty log message

Original author: cvscast
Date: 2002-10-10 16:39:45+00:00

depend

@@ -10,10 +10,10 @@ 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 parser/location.cmi types/patterns.cmi \
-    types/sortedList.cmi types/types.cmi typing/typer.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 types/types.cmx typing/typer.cmi 
-typing/typer.cmi: parser/ast.cmo types/types.cmi 
+    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 
 types/boolean.cmo: types/recursive.cmi types/sortedList.cmi types/boolean.cmi 

parser/parser.ml

@@ -74,7 +74,7 @@ module P = struct
   ];
 
   branch: [
-    [ p = pat; "->"; e = expr -> (p,e) ]
+    [ p = pat LEVEL "no_arrow"; "->"; e = expr -> (p,e) ]
   ];
 
 	  
@@ -98,7 +98,7 @@ module P = struct
         b = LIST1 [ a = UIDENT; "="; y = pat -> (a,y)] SEP "and"
             -> mk loc (Recurs (x,b)) ]
     | RIGHTA [ x = pat; "->"; y = pat -> mk loc (Arrow (x,y)) ]
-    | [ x = pat; "|"; y = pat -> mk loc (Or (x,y)) ] 
+    | "no_arrow" [ x = pat; "|"; y = pat -> mk loc (Or (x,y)) ] 
     | "simple" [ x = pat; "&"; y = pat -> mk loc (And (x,y)) 
       | x = pat; "-"; y = pat -> mk loc (Diff (x,y)) ]
     | 

types/types.ml

@@ -540,6 +540,10 @@ let rec rec_normalize d =
 
 let normalize n =
   internalize (rec_normalize (descr n))
+
+
+let apply t1 t2 = 
+  failwith "apply: not yet implemented"
   
 
 module Print =

types/types.mli

@@ -103,6 +103,7 @@ end
 
 val normalize : node -> node
 
+val apply : descr -> descr -> descr
 
 (** Subtyping and sample values **)
 

typing/typed.ml

@@ -14,10 +14,9 @@ open Location
 type tpat = Patterns.node
 type ttyp = Types.node
 
-type texpr  = { loc : Location.loc; 
+type texpr  = { exp_loc : Location.loc; 
 		mutable exp_typ : Types.descr; 
 		exp_descr : texpr';
-		fv : string list
 	      }
 and  texpr' = 
   (* CDuce is a Lambda-calculus ... *)
@@ -38,13 +37,15 @@ and  texpr' =
 and abstr = { 
   fun_name : string option; 
   fun_iface : (ttyp * ttyp) list;
-  fun_body : branches
+  fun_body : branches;
+  fun_typ  : Types.descr;
+  fun_fv   : string list;
 }
 
 and branches = branch list
 and branch = 
-    { mutable used : bool; 
-      mutable br_typ : Types.descr; 
+    { mutable br_used : bool; 
+      mutable br_typ : Types.descr;   (* TODO: move to branches and update *)
       br_pat : tpat; 
       br_body :  texpr }
     

typing/typer.ml

@@ -253,37 +253,140 @@ let pat e =
 
 (* II. Build skeleton *)
 
+module Fv = StringSet
+
 let rec expr { loc = loc; descr = d } = 
-  let td = 
+  let (fv,td) = 
     match d with
-      | Var s -> Typed.Var s
-      | Apply (e1,e2) -> Typed.Apply (expr e1, expr e2)
+      | Var s -> (Fv.singleton s, Typed.Var s)
+      | Apply (e1,e2) -> 
+	  let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
+	  (Fv.union fv1 fv2, Typed.Apply (e1,e2))
       | Abstraction a ->
-	  Typed.Abstraction 
-	    { Typed.fun_name = a.fun_name;
-	      Typed.fun_iface = 
-		List.map (fun (t1,t2) -> (typ t1, typ t2)) a.fun_iface;
-	      Typed.fun_body =
-		branches a.fun_body
-	    }
-      | Cst c -> Typed.Cst c
-      | Pair (e1,e2) -> Typed.Pair (expr e1, expr e2)
-      | RecordLitt r -> Typed.RecordLitt (List.map (fun (l,e) -> (l, expr e)) r)
-      | Op (o,e) -> Typed.Op (o, expr e)
-      | Match (e,b) -> Typed.Match (expr e, branches b)
-      | Map (e,b) -> Typed.Map (expr e, branches b)
+	  let iface = List.map (fun (t1,t2) -> (typ t1, typ t2)) a.fun_iface in
+	  let t = List.fold_left 
+		    (fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2)) 
+		    Types.any iface in
+	  let (fv0,body) = branches a.fun_body in
+	  let fv = match a.fun_name with
+	    | None -> fv0
+	    | Some f -> Fv.remove f fv0 in
+	  (fv,
+	   Typed.Abstraction 
+	     { Typed.fun_name = a.fun_name;
+	       Typed.fun_iface = iface;
+	       Typed.fun_body = body;
+	       Typed.fun_typ = t;
+	       Typed.fun_fv = Fv.elements fv0
+	     }
+	  )
+      | Cst c -> (Fv.empty, Typed.Cst c)
+      | Pair (e1,e2) ->
+	  let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
+	  (Fv.union fv1 fv2, Typed.Pair (e1,e2))
+      | RecordLitt r -> 
+	  (* XXX TODO: check that no label appears twice *)
+	  let fv = ref Fv.empty in
+	  let r = List.map 
+		    (fun (l,e) -> 
+		       let (fv2,e) = expr e in
+		       fv := Fv.union !fv fv2;
+		       (l,e)
+		    ) r in
+	  (!fv, Typed.RecordLitt r)
+      | Op (o,e) -> 
+	  let (fv,e) = expr e in (fv, Typed.Op (o,e))
+      | Match (e,b) -> 
+	  let (fv1,e) = expr e
+	  and (fv2,b) = branches b in
+	  (Fv.union fv1 fv2, Typed.Match (e, b))
+      | Map (e,b) ->
+	  let (fv1,e) = expr e
+	  and (fv2,b) = branches b in
+	  (Fv.union fv1 fv2, Typed.Map (e, b))
   in
-  { Typed.loc = loc;
+  fv,
+  { Typed.exp_loc = loc;
     Typed.exp_typ = Types.empty;
     Typed.exp_descr = td;
-    Typed.fv = []  (* XXX TODO *)
   }
 	      
-  and branches b = List.map branch b
-  and branch (p,e) = 
-    { Typed.used = false;
-      Typed.br_typ = Types.empty;
-      Typed.br_pat = pat p;
-      Typed.br_body = expr e }
-
-let compute_type t = failwith "Not yet implemented"
+  and branches b = 
+    let fv = ref Fv.empty in
+    let b = List.map 
+	      (fun (p,e) ->
+		 let (fv2,e) = expr e in
+		 fv := Fv.union !fv fv2;
+		 { Typed.br_used = false;
+		   Typed.br_typ = Types.empty;
+		   Typed.br_pat = pat p;
+		   Typed.br_body = e }
+	      ) b in
+    (!fv,b)
+
+module Env = StringMap
+
+open Typed
+
+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;
+  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
+  | Abstraction a ->
+      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 env (Types.descr t1) a.fun_body in
+		   if not (Types.subtype t (Types.descr t2)) then
+		     failwith "Constraint not satisfied"
+		) a.fun_iface;
+      a.fun_typ
+  | Cst c -> Types.constant c
+  | 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
+  | 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 env t b
+  | Map (e,b) -> assert false
+
+and type_branches env targ branches =
+  if Types.is_empty targ then Types.empty 
+  else branches_aux env targ Types.empty branches
+    
+and branches_aux env targ tres = function
+  | [] -> failwith "Non-exhaustive pattern matching"
+  | b :: rem ->
+      let p = b.br_pat in
+      let acc = Types.descr (Patterns.accept p) in
+
+      let targ' = Types.cap targ acc in
+      if Types.is_empty targ' 
+      then branches_aux env targ tres 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
+	  branches_aux env (Types.diff targ acc) (Types.cup t tres) rem 
+	)
+	  
+  

typing/typer.mli

@@ -5,5 +5,9 @@ val compile_regexp : Ast.regexp -> Ast.ppat -> Ast.ppat
 val typ : Ast.ppat -> Typed.ttyp
 val pat : Ast.ppat -> Typed.tpat
 
-val expr: Ast.pexpr -> Typed.texpr
-val compute_type: Typed.texpr -> Types.descr
+module Fv : Set.S with type elt = string
+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