viewcvs.cgi/typing/typer.ml

(* I. Transform the abstract syntax of types and patterns into
      the internal form *)

open Location
open Ast
exception ParsingPattern of string

let raise_loc loc msg = raise (Location loc (ParsingPattern msg))

(* Internal representation as a graph (desugar recursive types and regexp),
   to compute freevars, etc... *)

type ti = { 
  id : int; 
  mutable loc' : loc;
  mutable fv : string SortedList.t option; 
  mutable descr': descr;
  mutable type_node: Types.node option;
  mutable pat_node: Patterns.node option
} 
and descr =
   [ `Alias of ti
   | `Type of Types.descr
   | `Or of ti * ti
   | `And of ti * ti
   | `Diff of ti * ti
   | `Times of ti * ti
   | `Arrow of ti * ti
   | `Record of Types.label * bool * ti
   | `Capture of Patterns.capture
   | `Constant of Patterns.capture * Types.const
   ]
    

module S = struct type t = string let compare = compare end
module StringMap = Map.Make(S)
module StringSet = Set.Make(S)

let mk' =
  let counter = ref 0 in
  fun () ->
    incr counter;
    let rec x = { id = !counter; loc' = noloc; fv = None; descr' = `Alias x; 
                  type_node = None; pat_node = None } in
    x

let cons loc d =
  let x = mk' () in
  x.loc' <- loc;
  x.descr' <- d;
  x
    
(* Note:
   Compilation of Regexp is implemented as a ``rewriting'' of
   the parsed syntax, in order to be able to print its result
   (for debugging for instance)
   
   It would be possible (and a little more efficient) to produce
   directly ti nodes.
*)
    
module Regexp = struct
  let memo = Hashtbl.create 51
  let defs = ref []
  let name =
    let c = ref 0 in
    fun () ->
      incr c;
      "#" ^ (string_of_int !c)

  let rec seq_vars accu = function
    | Epsilon | Elem _ -> accu
    | Seq (r1,r2) | Alt (r1,r2) -> seq_vars (seq_vars accu r1) r2
    | Star r | WeakStar r -> seq_vars accu r
    | SeqCapture (v,r) -> seq_vars (StringSet.add v accu) r

  let rec propagate vars = function
    | Epsilon -> `Epsilon
    | Elem x -> `Elem (vars,x)
    | Seq (r1,r2) -> `Seq (propagate vars r1,propagate vars r2)
    | Alt (r1,r2) -> `Alt (propagate vars r1, propagate vars r2)
    | Star r -> `Star (propagate vars r)
    | WeakStar r -> `WeakStar (propagate vars r)
    | SeqCapture (v,x) -> propagate (StringSet.add v vars) x

  let cup r1 r2 = 
    match (r1,r2) with
      | (_, `Empty) -> r1
      | (`Empty, _) -> r2
      | (`Res t1, `Res t2) -> `Res (mk noloc (Or (t1,t2)))

  let rec compile fin e seq : [`Res of Ast.ppat | `Empty] = 
    if List.mem seq e then `Empty
    else 
      let e = seq :: e in
      match seq with
        | [] ->
            `Res fin
        | `Epsilon :: rest -> 
            compile fin e rest
        | `Elem (vars,x) :: rest -> 
            let capt = StringSet.fold
                         (fun v t -> mk noloc (And (t, (mk noloc (Capture v)))))
                         vars x in
            `Res (mk noloc (Prod (capt, guard_compile fin rest)))
        | `Seq (r1,r2) :: rest -> 
            compile fin e (r1 :: r2 :: rest)
        | `Alt (r1,r2) :: rest -> 
            cup (compile fin e (r1::rest)) (compile fin e (r2::rest))
        | `Star r :: rest -> cup (compile fin e (r::seq)) (compile fin e rest) 
        | `WeakStar r :: rest -> cup (compile fin e rest) (compile fin e (r::seq))

  and guard_compile fin seq =
    try Hashtbl.find memo seq 
    with
        Not_found ->
          let n = name () in
          let v = mk noloc (PatVar n) in
          Hashtbl.add memo seq v;
          let d = compile fin [] seq in
          (match d with
             | `Empty -> assert false
             | `Res d -> defs := (n,d) :: !defs);
          v


  let atom_nil = Types.mk_atom "nil"
  let constant_nil v t = 
    mk noloc (And (t, (mk noloc (Constant (v, Types.Atom atom_nil)))))

  let compile regexp queue : ppat =
    let vars = seq_vars StringSet.empty regexp in
    let fin = StringSet.fold constant_nil vars queue in
    let n = guard_compile fin [propagate StringSet.empty regexp] in
    Hashtbl.clear memo;
    let d = !defs in
    defs := [];
    mk noloc (Recurs (n,d))
end

let compile_regexp = Regexp.compile


let rec compile env { loc = loc; descr = d } : ti = 
  match (d : Ast.ppat') with
  | PatVar s -> 
      (try StringMap.find s env
       with Not_found -> raise_loc loc "Undefined variable"
      )
  | 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.descr' <- `Alias (compile env t)) b;
      compile env 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))
  | And (t1,t2) -> cons loc (`And (compile env t1, compile env t2))
  | Diff (t1,t2) -> cons loc (`Diff (compile env t1, compile env t2))
  | Prod (t1,t2) -> cons loc (`Times (compile env t1, compile env t2))
  | Arrow (t1,t2) -> cons loc (`Arrow (compile env t1, compile env t2))
  | Record (l,o,t) -> cons loc (`Record (l,o,compile env t))
  | Constant (x,v) -> cons loc (`Constant (x,v))
  | Capture x -> cons loc (`Capture x)

let rec comp_fv seen s =
  match s.fv with
    | Some l -> l
    | None ->
        let l = 
          match s.descr' with
            | `Alias x -> if List.memq s seen then [] else comp_fv (s :: seen) x
            | `Or (s1,s2) 
            | `And (s1,s2)
            | `Diff (s1,s2)
            | `Times (s1,s2)
            | `Arrow (s1,s2) -> SortedList.cup (comp_fv seen s1) (comp_fv seen s2)
            | `Record (l,opt,s) -> comp_fv seen s
            | `Type _ -> []
            | `Capture x
            | `Constant (x,_) -> [x]
        in
        if seen = [] then s.fv <- Some l;
        l


let fv = comp_fv []

let rec typ seen s : Types.descr =
  match s.descr' with
    | `Alias x ->
        if List.memq s seen then failwith "Unguarded recursion in this type"
        else typ (s :: seen) x
    | `Type t -> t
    | `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)
    | `And (s1,s2) ->  Types.cap (typ seen s1) (typ seen s2)
    | `Diff (s1,s2) -> Types.diff (typ seen s1) (typ seen s2)
    | `Times (s1,s2) -> Types.times (typ_node s1) (typ_node s2)
    | `Arrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)
    | `Record (l,o,s) -> Types.record l o (typ_node s)
    | _ -> failwith "This is not a type"

and typ_node s : Types.node =
  match s.type_node with
    | Some x -> x
    | None ->
        let x = Types.make () in
        s.type_node <- Some x;
        let t = typ [] s in
        Types.define x t;
        x

let type_node s = Types.internalize (typ_node s)

let rec pat seen s : Patterns.descr =
  if fv s = [] then Patterns.constr (type_node s) else
  match s.descr' with
    | `Alias x ->
        if List.memq s seen then failwith "Unguarded recursion in this pattern"
        else pat (s :: seen) x
    | `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)
    | `And (s1,s2) -> Patterns.cap (pat seen s1) (pat seen s2)
    | `Diff (s1,s2) when fv s2 = [] ->
        let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in
        Patterns.cap (pat seen s1) (Patterns.constr s2)
    | `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
    | `Record (l,false,s) -> Patterns.record l (pat_node s)
    | `Capture x ->  Patterns.capture x
    | `Constant (x,c) -> Patterns.constant x c
    | _ -> failwith "This is not a pattern"

and pat_node s : Patterns.node =
  match s.pat_node with
    | Some x -> x
    | None ->
        let x = Patterns.make (fv s) in
        s.pat_node <- Some x;
        let t = pat [] s in
        Patterns.define x t;
        x

let typ e =
  let e = compile StringMap.empty e in
  if fv e = [] then type_node e else failwith "This is not a type"

let pat e =
  let e = compile StringMap.empty e in
  pat_node e


(* II. Build skeleton *)

module Fv = StringSet

let rec expr { loc = loc; descr = d } = 
  let (fv,td) = 
    match d with
      | 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 ->
          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
  fv,
  { Typed.exp_loc = loc;
    Typed.exp_typ = Types.empty;
    Typed.exp_descr = td;
  }
              
  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 
        )
          
  
1	abate	5	(* I. Transform the abstract syntax of types and patterns into
2			the internal form *)
3
4			open Location
5			open Ast
6			exception ParsingPattern of string
7
8			let raise_loc loc msg = raise (Location loc (ParsingPattern msg))
9
10			(* Internal representation as a graph (desugar recursive types and regexp),
11			to compute freevars, etc... *)
12
13			type ti = {
14			id : int;
15			mutable loc' : loc;
16			mutable fv : string SortedList.t option;
17			mutable descr': descr;
18			mutable type_node: Types.node option;
19			mutable pat_node: Patterns.node option
20			}
21			and descr =
22			[ `Alias of ti
23			\| `Type of Types.descr
24			\| `Or of ti * ti
25			\| `And of ti * ti
26			\| `Diff of ti * ti
27			\| `Times of ti * ti
28			\| `Arrow of ti * ti
29			\| `Record of Types.label * bool * ti
30			\| `Capture of Patterns.capture
31			\| `Constant of Patterns.capture * Types.const
32			]
33
34
35
36			module S = struct type t = string let compare = compare end
37			module StringMap = Map.Make(S)
38			module StringSet = Set.Make(S)
39
40			let mk' =
41			let counter = ref 0 in
42			fun () ->
43			incr counter;
44			let rec x = { id = !counter; loc' = noloc; fv = None; descr' = `Alias x;
45			type_node = None; pat_node = None } in
46			x
47
48			let cons loc d =
49			let x = mk' () in
50			x.loc' <- loc;
51			x.descr' <- d;
52			x
53
54			(* Note:
55			Compilation of Regexp is implemented as a ``rewriting'' of
56			the parsed syntax, in order to be able to print its result
57			(for debugging for instance)
58
59			It would be possible (and a little more efficient) to produce
60			directly ti nodes.
61			*)
62
63			module Regexp = struct
64			let memo = Hashtbl.create 51
65			let defs = ref []
66			let name =
67			let c = ref 0 in
68			fun () ->
69			incr c;
70			"#" ^ (string_of_int !c)
71
72			let rec seq_vars accu = function
73			\| Epsilon \| Elem _ -> accu
74			\| Seq (r1,r2) \| Alt (r1,r2) -> seq_vars (seq_vars accu r1) r2
75			\| Star r \| WeakStar r -> seq_vars accu r
76			\| SeqCapture (v,r) -> seq_vars (StringSet.add v accu) r
77
78			let rec propagate vars = function
79			\| Epsilon -> `Epsilon
80			\| Elem x -> `Elem (vars,x)
81			\| Seq (r1,r2) -> `Seq (propagate vars r1,propagate vars r2)
82			\| Alt (r1,r2) -> `Alt (propagate vars r1, propagate vars r2)
83			\| Star r -> `Star (propagate vars r)
84			\| WeakStar r -> `WeakStar (propagate vars r)
85			\| SeqCapture (v,x) -> propagate (StringSet.add v vars) x
86
87			let cup r1 r2 =
88			match (r1,r2) with
89			\| (_, `Empty) -> r1
90			\| (`Empty, _) -> r2
91			\| (`Res t1, `Res t2) -> `Res (mk noloc (Or (t1,t2)))
92
93			let rec compile fin e seq : [`Res of Ast.ppat \| `Empty] =
94			if List.mem seq e then `Empty
95			else
96			let e = seq :: e in
97			match seq with
98			\| [] ->
99			`Res fin
100			\| `Epsilon :: rest ->
101			compile fin e rest
102			\| `Elem (vars,x) :: rest ->
103			let capt = StringSet.fold
104			(fun v t -> mk noloc (And (t, (mk noloc (Capture v)))))
105			vars x in
106			`Res (mk noloc (Prod (capt, guard_compile fin rest)))
107			\| `Seq (r1,r2) :: rest ->
108			compile fin e (r1 :: r2 :: rest)
109			\| `Alt (r1,r2) :: rest ->
110			cup (compile fin e (r1::rest)) (compile fin e (r2::rest))
111			\| `Star r :: rest -> cup (compile fin e (r::seq)) (compile fin e rest)
112			\| `WeakStar r :: rest -> cup (compile fin e rest) (compile fin e (r::seq))
113
114			and guard_compile fin seq =
115			try Hashtbl.find memo seq
116			with
117			Not_found ->
118			let n = name () in
119			let v = mk noloc (PatVar n) in
120			Hashtbl.add memo seq v;
121			let d = compile fin [] seq in
122			(match d with
123			\| `Empty -> assert false
124			\| `Res d -> defs := (n,d) :: !defs);
125			v
126
127
128			let atom_nil = Types.mk_atom "nil"
129			let constant_nil v t =
130			mk noloc (And (t, (mk noloc (Constant (v, Types.Atom atom_nil)))))
131
132			let compile regexp queue : ppat =
133			let vars = seq_vars StringSet.empty regexp in
134			let fin = StringSet.fold constant_nil vars queue in
135			let n = guard_compile fin [propagate StringSet.empty regexp] in
136			Hashtbl.clear memo;
137			let d = !defs in
138			defs := [];
139			mk noloc (Recurs (n,d))
140			end
141
142			let compile_regexp = Regexp.compile
143
144
145			let rec compile env { loc = loc; descr = d } : ti =
146			match (d : Ast.ppat') with
147			\| PatVar s ->
148			(try StringMap.find s env
149			with Not_found -> raise_loc loc "Undefined variable"
150			)
151			\| Recurs (t, b) ->
152			let b = List.map (fun (v,t) -> (v,t,mk' ())) b in
153			let env =
154			List.fold_left (fun env (v,t,x) -> StringMap.add v x env) env b in
155			List.iter (fun (v,t,x) -> x.descr' <- `Alias (compile env t)) b;
156			compile env t
157			\| Regexp (r,q) -> compile env (Regexp.compile r q)
158			\| Internal t -> cons loc (`Type t)
159			\| Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2))
160			\| And (t1,t2) -> cons loc (`And (compile env t1, compile env t2))
161			\| Diff (t1,t2) -> cons loc (`Diff (compile env t1, compile env t2))
162			\| Prod (t1,t2) -> cons loc (`Times (compile env t1, compile env t2))
163			\| Arrow (t1,t2) -> cons loc (`Arrow (compile env t1, compile env t2))
164			\| Record (l,o,t) -> cons loc (`Record (l,o,compile env t))
165			\| Constant (x,v) -> cons loc (`Constant (x,v))
166			\| Capture x -> cons loc (`Capture x)
167
168			let rec comp_fv seen s =
169			match s.fv with
170			\| Some l -> l
171			\| None ->
172			let l =
173			match s.descr' with
174			\| `Alias x -> if List.memq s seen then [] else comp_fv (s :: seen) x
175			\| `Or (s1,s2)
176			\| `And (s1,s2)
177			\| `Diff (s1,s2)
178			\| `Times (s1,s2)
179			\| `Arrow (s1,s2) -> SortedList.cup (comp_fv seen s1) (comp_fv seen s2)
180			\| `Record (l,opt,s) -> comp_fv seen s
181			\| `Type _ -> []
182			\| `Capture x
183			\| `Constant (x,_) -> [x]
184			in
185			if seen = [] then s.fv <- Some l;
186			l
187
188
189			let fv = comp_fv []
190
191			let rec typ seen s : Types.descr =
192			match s.descr' with
193			\| `Alias x ->
194			if List.memq s seen then failwith "Unguarded recursion in this type"
195			else typ (s :: seen) x
196			\| `Type t -> t
197			\| `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)
198			\| `And (s1,s2) -> Types.cap (typ seen s1) (typ seen s2)
199			\| `Diff (s1,s2) -> Types.diff (typ seen s1) (typ seen s2)
200			\| `Times (s1,s2) -> Types.times (typ_node s1) (typ_node s2)
201			\| `Arrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)
202			\| `Record (l,o,s) -> Types.record l o (typ_node s)
203			\| _ -> failwith "This is not a type"
204
205			and typ_node s : Types.node =
206			match s.type_node with
207			\| Some x -> x
208			\| None ->
209			let x = Types.make () in
210			s.type_node <- Some x;
211			let t = typ [] s in
212			Types.define x t;
213			x
214
215			let type_node s = Types.internalize (typ_node s)
216
217			let rec pat seen s : Patterns.descr =
218			if fv s = [] then Patterns.constr (type_node s) else
219			match s.descr' with
220			\| `Alias x ->
221			if List.memq s seen then failwith "Unguarded recursion in this pattern"
222			else pat (s :: seen) x
223			\| `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)
224			\| `And (s1,s2) -> Patterns.cap (pat seen s1) (pat seen s2)
225			\| `Diff (s1,s2) when fv s2 = [] ->
226			let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in
227			Patterns.cap (pat seen s1) (Patterns.constr s2)
228			\| `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
229			\| `Record (l,false,s) -> Patterns.record l (pat_node s)
230			\| `Capture x -> Patterns.capture x
231			\| `Constant (x,c) -> Patterns.constant x c
232			\| _ -> failwith "This is not a pattern"
233
234			and pat_node s : Patterns.node =
235			match s.pat_node with
236			\| Some x -> x
237			\| None ->
238			let x = Patterns.make (fv s) in
239			s.pat_node <- Some x;
240			let t = pat [] s in
241			Patterns.define x t;
242			x
243
244			let typ e =
245			let e = compile StringMap.empty e in
246			if fv e = [] then type_node e else failwith "This is not a type"
247
248			let pat e =
249			let e = compile StringMap.empty e in
250			pat_node e
251
252
253
254			(* II. Build skeleton *)
255
256	abate	6	module Fv = StringSet
257
258	abate	5	let rec expr { loc = loc; descr = d } =
259	abate	6	let (fv,td) =
260	abate	5	match d with
261	abate	6	\| Var s -> (Fv.singleton s, Typed.Var s)
262			\| Apply (e1,e2) ->
263			let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
264			(Fv.union fv1 fv2, Typed.Apply (e1,e2))
265	abate	5	\| Abstraction a ->
266	abate	6	let iface = List.map (fun (t1,t2) -> (typ t1, typ t2)) a.fun_iface in
267			let t = List.fold_left
268			(fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2))
269			Types.any iface in
270			let (fv0,body) = branches a.fun_body in
271			let fv = match a.fun_name with
272			\| None -> fv0
273			\| Some f -> Fv.remove f fv0 in
274			(fv,
275			Typed.Abstraction
276			{ Typed.fun_name = a.fun_name;
277			Typed.fun_iface = iface;
278			Typed.fun_body = body;
279			Typed.fun_typ = t;
280			Typed.fun_fv = Fv.elements fv0
281			}
282			)
283			\| Cst c -> (Fv.empty, Typed.Cst c)
284			\| Pair (e1,e2) ->
285			let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
286			(Fv.union fv1 fv2, Typed.Pair (e1,e2))
287			\| RecordLitt r ->
288			(* XXX TODO: check that no label appears twice *)
289			let fv = ref Fv.empty in
290			let r = List.map
291			(fun (l,e) ->
292			let (fv2,e) = expr e in
293			fv := Fv.union !fv fv2;
294			(l,e)
295			) r in
296			(!fv, Typed.RecordLitt r)
297			\| Op (o,e) ->
298			let (fv,e) = expr e in (fv, Typed.Op (o,e))
299			\| Match (e,b) ->
300			let (fv1,e) = expr e
301			and (fv2,b) = branches b in
302			(Fv.union fv1 fv2, Typed.Match (e, b))
303			\| Map (e,b) ->
304			let (fv1,e) = expr e
305			and (fv2,b) = branches b in
306			(Fv.union fv1 fv2, Typed.Map (e, b))
307	abate	5	in
308	abate	6	fv,
309			{ Typed.exp_loc = loc;
310	abate	5	Typed.exp_typ = Types.empty;
311			Typed.exp_descr = td;
312			}
313
314	abate	6	and branches b =
315			let fv = ref Fv.empty in
316			let b = List.map
317			(fun (p,e) ->
318			let (fv2,e) = expr e in
319			fv := Fv.union !fv fv2;
320			{ Typed.br_used = false;
321			Typed.br_typ = Types.empty;
322			Typed.br_pat = pat p;
323			Typed.br_body = e }
324			) b in
325			(!fv,b)
326	abate	5
327	abate	6	module Env = StringMap
328
329			open Typed
330
331			let rec compute_type env e =
332			let d = compute_type' e.exp_loc env e.exp_descr in
333			e.exp_typ <- Types.cup e.exp_typ d;
334			d
335
336			and compute_type' loc env = function
337			\| Var s -> Env.find s env
338			\| Apply (e1,e2) ->
339			let t1 = compute_type env e1 and t2 = compute_type env e2 in
340			Types.apply t1 t2
341			\| Abstraction a ->
342			let env = match a.fun_name with
343			\| None -> env
344			\| Some f -> Env.add f a.fun_typ env in
345			List.iter (fun (t1,t2) ->
346			let t = type_branches env (Types.descr t1) a.fun_body in
347			if not (Types.subtype t (Types.descr t2)) then
348			failwith "Constraint not satisfied"
349			) a.fun_iface;
350			a.fun_typ
351			\| Cst c -> Types.constant c
352			\| Pair (e1,e2) ->
353			let t1 = compute_type env e1 and t2 = compute_type env e2 in
354			let t1 = Types.cons t1 and t2 = Types.cons t2 in
355			Types.times t1 t2
356			\| RecordLitt r ->
357			List.fold_left
358			(fun accu (l,e) ->
359			let t = compute_type env e in
360			let t = Types.record l false (Types.cons t) in
361			Types.cap accu t
362			) Types.Record.any r
363			\| Op (op,e) -> assert false
364			\| Match (e,b) ->
365			let t = compute_type env e in
366			type_branches env t b
367			\| Map (e,b) -> assert false
368
369			and type_branches env targ branches =
370			if Types.is_empty targ then Types.empty
371			else branches_aux env targ Types.empty branches
372
373			and branches_aux env targ tres = function
374			\| [] -> failwith "Non-exhaustive pattern matching"
375			\| b :: rem ->
376			let p = b.br_pat in
377			let acc = Types.descr (Patterns.accept p) in
378
379			let targ' = Types.cap targ acc in
380			if Types.is_empty targ'
381			then branches_aux env targ tres rem
382			else
383			( b.br_used <- true;
384			let res = Patterns.filter targ' p in
385			let env' = List.fold_left
386			(fun env (x,t) -> Env.add x (Types.descr t) env)
387			env res in
388			let t = compute_type env' b.br_body in
389			branches_aux env (Types.diff targ acc) (Types.cup t tres) rem
390			)
391
392