viewcvs.cgi/typing/typer.ml

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

open Location
open Ast

exception Pattern of string
exception NonExhaustive of Types.descr
exception Constraint of Types.descr * Types.descr * string

let raise_loc loc exn = raise (Location (loc,exn))

(* 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 string * 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 loc ->
    incr counter;
    let rec x = { 
      id = !counter; 
      loc' = loc; 
      fv = None; 
      descr' = `Alias ("__dummy__", x);  
      type_node = None; 
      pat_node = None 
    } in
    x

let cons loc d =
  let x = mk' loc in
  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 (Pattern ("Undefined type variable " ^ s))
      )
  | 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))
  | 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)

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
    | 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 (v,x) ->
        if List.memq s seen then 
          raise_loc s.loc' 
            (Pattern 
               ("Unguarded recursion on variable " ^ v ^ " 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)
    | `Capture _ | `Constant _ -> assert false

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 (v,x) ->
        if List.memq s seen then 
          raise_loc s.loc' 
            (Pattern 
               ("Unguarded recursion on variable " ^ v ^ " 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)
    | `Diff _ ->
        raise_loc s.loc' (Pattern "Difference not allowed in patterns")
    | `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
    | `Record (l,false,s) -> Patterns.record l (pat_node s)
    | `Record _ ->
        raise_loc s.loc' 
          (Pattern "Optional field not allowed in record patterns")
    | `Capture x ->  Patterns.capture x
    | `Constant (x,c) -> Patterns.constant x c
    | `Arrow _ ->
        raise_loc s.loc' (Pattern "Arrow not allowed in patterns")
    | `Type _ -> assert false

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 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")
    

let typ e =
  mk_typ (compile !global_types e)

let pat e =
  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
               Types.Print.register_global v d
            ) b;
  global_types := env


(* 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 iface = List.map 
                        (fun (t1,t2) -> (Types.descr t1, Types.descr t2)) 
                        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 (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
          (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_pat = pat p;
                   Typed.br_body = e }
              ) b in
    (!fv, { Typed.br_typ = Types.empty; Typed.br_branches = b } )

module Env = StringMap

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
  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
      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"))
  | 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 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
  | 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, 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

and type_branches loc env targ brs =
  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
  )
    
and branches_aux loc env targ tres = function
  | [] -> raise_loc loc (NonExhaustive targ)
  | 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 loc 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
          let tres = Types.cup t 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 
          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 
               (t1,Types.Int.any,
                "The second argument must be an integer"));
  Types.Int.put
    (f (Types.Int.get t1) (Types.Int.get t2));
  

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
7	abate	9	exception Pattern of string
8			exception NonExhaustive of Types.descr
9			exception Constraint of Types.descr * Types.descr * string
10	abate	5
11	abate	9	let raise_loc loc exn = raise (Location (loc,exn))
12
13	abate	5	(* Internal representation as a graph (desugar recursive types and regexp),
14			to compute freevars, etc... *)
15
16	abate	9	type ti = {
17	abate	5	id : int;
18			mutable loc' : loc;
19			mutable fv : string SortedList.t option;
20			mutable descr': descr;
21			mutable type_node: Types.node option;
22			mutable pat_node: Patterns.node option
23			}
24			and descr =
25	abate	9	[ `Alias of string * ti
26	abate	5	\| `Type of Types.descr
27			\| `Or of ti * ti
28			\| `And of ti * ti
29			\| `Diff of ti * ti
30			\| `Times of ti * ti
31			\| `Arrow of ti * ti
32			\| `Record of Types.label * bool * ti
33			\| `Capture of Patterns.capture
34			\| `Constant of Patterns.capture * Types.const
35			]
36
37
38
39			module S = struct type t = string let compare = compare end
40			module StringMap = Map.Make(S)
41			module StringSet = Set.Make(S)
42
43			let mk' =
44			let counter = ref 0 in
45	abate	13	fun loc ->
46	abate	5	incr counter;
47	abate	9	let rec x = {
48			id = !counter;
49	abate	13	loc' = loc;
50	abate	9	fv = None;
51			descr' = `Alias ("__dummy__", x);
52			type_node = None;
53			pat_node = None
54			} in
55	abate	5	x
56
57			let cons loc d =
58	abate	13	let x = mk' loc in
59	abate	5	x.descr' <- d;
60			x
61
62			(* Note:
63			Compilation of Regexp is implemented as a ``rewriting'' of
64			the parsed syntax, in order to be able to print its result
65			(for debugging for instance)
66
67			It would be possible (and a little more efficient) to produce
68			directly ti nodes.
69			*)
70
71			module Regexp = struct
72			let memo = Hashtbl.create 51
73			let defs = ref []
74			let name =
75			let c = ref 0 in
76			fun () ->
77			incr c;
78			"#" ^ (string_of_int !c)
79
80			let rec seq_vars accu = function
81			\| Epsilon \| Elem _ -> accu
82			\| Seq (r1,r2) \| Alt (r1,r2) -> seq_vars (seq_vars accu r1) r2
83			\| Star r \| WeakStar r -> seq_vars accu r
84			\| SeqCapture (v,r) -> seq_vars (StringSet.add v accu) r
85
86			let rec propagate vars = function
87			\| Epsilon -> `Epsilon
88			\| Elem x -> `Elem (vars,x)
89			\| Seq (r1,r2) -> `Seq (propagate vars r1,propagate vars r2)
90			\| Alt (r1,r2) -> `Alt (propagate vars r1, propagate vars r2)
91			\| Star r -> `Star (propagate vars r)
92			\| WeakStar r -> `WeakStar (propagate vars r)
93			\| SeqCapture (v,x) -> propagate (StringSet.add v vars) x
94
95			let cup r1 r2 =
96			match (r1,r2) with
97			\| (_, `Empty) -> r1
98			\| (`Empty, _) -> r2
99			\| (`Res t1, `Res t2) -> `Res (mk noloc (Or (t1,t2)))
100
101			let rec compile fin e seq : [`Res of Ast.ppat \| `Empty] =
102			if List.mem seq e then `Empty
103			else
104			let e = seq :: e in
105			match seq with
106			\| [] ->
107			`Res fin
108			\| `Epsilon :: rest ->
109			compile fin e rest
110			\| `Elem (vars,x) :: rest ->
111			let capt = StringSet.fold
112			(fun v t -> mk noloc (And (t, (mk noloc (Capture v)))))
113			vars x in
114			`Res (mk noloc (Prod (capt, guard_compile fin rest)))
115			\| `Seq (r1,r2) :: rest ->
116			compile fin e (r1 :: r2 :: rest)
117			\| `Alt (r1,r2) :: rest ->
118			cup (compile fin e (r1::rest)) (compile fin e (r2::rest))
119			\| `Star r :: rest -> cup (compile fin e (r::seq)) (compile fin e rest)
120			\| `WeakStar r :: rest -> cup (compile fin e rest) (compile fin e (r::seq))
121
122			and guard_compile fin seq =
123			try Hashtbl.find memo seq
124			with
125			Not_found ->
126			let n = name () in
127			let v = mk noloc (PatVar n) in
128			Hashtbl.add memo seq v;
129			let d = compile fin [] seq in
130			(match d with
131			\| `Empty -> assert false
132			\| `Res d -> defs := (n,d) :: !defs);
133			v
134
135
136			let atom_nil = Types.mk_atom "nil"
137			let constant_nil v t =
138			mk noloc (And (t, (mk noloc (Constant (v, Types.Atom atom_nil)))))
139
140			let compile regexp queue : ppat =
141			let vars = seq_vars StringSet.empty regexp in
142			let fin = StringSet.fold constant_nil vars queue in
143			let n = guard_compile fin [propagate StringSet.empty regexp] in
144			Hashtbl.clear memo;
145			let d = !defs in
146			defs := [];
147			mk noloc (Recurs (n,d))
148			end
149
150			let compile_regexp = Regexp.compile
151
152
153			let rec compile env { loc = loc; descr = d } : ti =
154			match (d : Ast.ppat') with
155			\| PatVar s ->
156			(try StringMap.find s env
157	abate	9	with Not_found ->
158			raise_loc loc (Pattern ("Undefined type variable " ^ s))
159	abate	5	)
160	abate	13	\| Recurs (t, b) -> compile (compile_many env b) t
161	abate	5	\| Regexp (r,q) -> compile env (Regexp.compile r q)
162			\| Internal t -> cons loc (`Type t)
163			\| Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2))
164			\| And (t1,t2) -> cons loc (`And (compile env t1, compile env t2))
165			\| Diff (t1,t2) -> cons loc (`Diff (compile env t1, compile env t2))
166			\| Prod (t1,t2) -> cons loc (`Times (compile env t1, compile env t2))
167			\| Arrow (t1,t2) -> cons loc (`Arrow (compile env t1, compile env t2))
168			\| Record (l,o,t) -> cons loc (`Record (l,o,compile env t))
169			\| Constant (x,v) -> cons loc (`Constant (x,v))
170			\| Capture x -> cons loc (`Capture x)
171
172	abate	13	and compile_many env b =
173			let b = List.map (fun (v,t) -> (v,t,mk' t.loc)) b in
174			let env =
175			List.fold_left (fun env (v,t,x) -> StringMap.add v x env) env b in
176			List.iter (fun (v,t,x) -> x.descr' <- `Alias (v, compile env t)) b;
177			env
178
179
180	abate	5	let rec comp_fv seen s =
181			match s.fv with
182			\| Some l -> l
183			\| None ->
184			let l =
185			match s.descr' with
186	abate	9	\| `Alias (_,x) -> if List.memq s seen then [] else comp_fv (s :: seen) x
187	abate	5	\| `Or (s1,s2)
188			\| `And (s1,s2)
189			\| `Diff (s1,s2)
190			\| `Times (s1,s2)
191			\| `Arrow (s1,s2) -> SortedList.cup (comp_fv seen s1) (comp_fv seen s2)
192			\| `Record (l,opt,s) -> comp_fv seen s
193			\| `Type _ -> []
194			\| `Capture x
195			\| `Constant (x,_) -> [x]
196			in
197			if seen = [] then s.fv <- Some l;
198			l
199
200
201			let fv = comp_fv []
202
203			let rec typ seen s : Types.descr =
204			match s.descr' with
205	abate	9	\| `Alias (v,x) ->
206			if List.memq s seen then
207			raise_loc s.loc'
208			(Pattern
209			("Unguarded recursion on variable " ^ v ^ " in this type"))
210	abate	5	else typ (s :: seen) x
211			\| `Type t -> t
212			\| `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)
213			\| `And (s1,s2) -> Types.cap (typ seen s1) (typ seen s2)
214			\| `Diff (s1,s2) -> Types.diff (typ seen s1) (typ seen s2)
215			\| `Times (s1,s2) -> Types.times (typ_node s1) (typ_node s2)
216			\| `Arrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)
217			\| `Record (l,o,s) -> Types.record l o (typ_node s)
218	abate	9	\| `Capture _ \| `Constant _ -> assert false
219	abate	5
220			and typ_node s : Types.node =
221			match s.type_node with
222			\| Some x -> x
223			\| None ->
224			let x = Types.make () in
225			s.type_node <- Some x;
226			let t = typ [] s in
227			Types.define x t;
228			x
229
230			let type_node s = Types.internalize (typ_node s)
231
232			let rec pat seen s : Patterns.descr =
233			if fv s = [] then Patterns.constr (type_node s) else
234			match s.descr' with
235	abate	9	\| `Alias (v,x) ->
236			if List.memq s seen then
237			raise_loc s.loc'
238			(Pattern
239			("Unguarded recursion on variable " ^ v ^ " in this pattern"))
240	abate	5	else pat (s :: seen) x
241			\| `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)
242			\| `And (s1,s2) -> Patterns.cap (pat seen s1) (pat seen s2)
243			\| `Diff (s1,s2) when fv s2 = [] ->
244			let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in
245			Patterns.cap (pat seen s1) (Patterns.constr s2)
246	abate	9	\| `Diff _ ->
247			raise_loc s.loc' (Pattern "Difference not allowed in patterns")
248	abate	5	\| `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
249			\| `Record (l,false,s) -> Patterns.record l (pat_node s)
250	abate	9	\| `Record _ ->
251			raise_loc s.loc'
252			(Pattern "Optional field not allowed in record patterns")
253	abate	5	\| `Capture x -> Patterns.capture x
254			\| `Constant (x,c) -> Patterns.constant x c
255	abate	9	\| `Arrow _ ->
256			raise_loc s.loc' (Pattern "Arrow not allowed in patterns")
257			\| `Type _ -> assert false
258	abate	5
259			and pat_node s : Patterns.node =
260			match s.pat_node with
261			\| Some x -> x
262			\| None ->
263			let x = Patterns.make (fv s) in
264			s.pat_node <- Some x;
265			let t = pat [] s in
266			Patterns.define x t;
267			x
268
269	abate	13	let global_types = ref StringMap.empty
270
271			let mk_typ e =
272	abate	9	if fv e = [] then type_node e
273	abate	13	else raise_loc e.loc' (Pattern "Capture variables are not allowed in types")
274
275	abate	5
276	abate	13	let typ e =
277			mk_typ (compile !global_types e)
278
279	abate	5	let pat e =
280	abate	13	let e = compile !global_types e in
281	abate	5	pat_node e
282
283	abate	13	let register_global_types b =
284			let env = compile_many !global_types b in
285	abate	15	List.iter (fun (v,_) ->
286			let d = Types.descr (mk_typ (StringMap.find v env)) in
287			Types.Print.register_global v d
288			) b;
289	abate	13	global_types := env
290	abate	5
291
292			(* II. Build skeleton *)
293
294	abate	6	module Fv = StringSet
295
296	abate	5	let rec expr { loc = loc; descr = d } =
297	abate	6	let (fv,td) =
298	abate	5	match d with
299	abate	6	\| Var s -> (Fv.singleton s, Typed.Var s)
300			\| Apply (e1,e2) ->
301			let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
302			(Fv.union fv1 fv2, Typed.Apply (e1,e2))
303	abate	5	\| Abstraction a ->
304	abate	6	let iface = List.map (fun (t1,t2) -> (typ t1, typ t2)) a.fun_iface in
305			let t = List.fold_left
306			(fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2))
307			Types.any iface in
308	abate	9	let iface = List.map
309			(fun (t1,t2) -> (Types.descr t1, Types.descr t2))
310			iface in
311	abate	6	let (fv0,body) = branches a.fun_body in
312			let fv = match a.fun_name with
313			\| None -> fv0
314			\| Some f -> Fv.remove f fv0 in
315			(fv,
316			Typed.Abstraction
317			{ Typed.fun_name = a.fun_name;
318			Typed.fun_iface = iface;
319			Typed.fun_body = body;
320			Typed.fun_typ = t;
321			Typed.fun_fv = Fv.elements fv0
322			}
323			)
324			\| Cst c -> (Fv.empty, Typed.Cst c)
325			\| Pair (e1,e2) ->
326			let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
327			(Fv.union fv1 fv2, Typed.Pair (e1,e2))
328			\| RecordLitt r ->
329			(* XXX TODO: check that no label appears twice *)
330			let fv = ref Fv.empty in
331			let r = List.map
332			(fun (l,e) ->
333			let (fv2,e) = expr e in
334			fv := Fv.union !fv fv2;
335			(l,e)
336			) r in
337			(!fv, Typed.RecordLitt r)
338	abate	16	\| Op (op,le) ->
339			let (fvs,ltes) = List.split (List.map expr le) in
340			let fv = List.fold_left Fv.union Fv.empty fvs in
341			(fv, Typed.Op (op,ltes))
342	abate	6	\| Match (e,b) ->
343			let (fv1,e) = expr e
344			and (fv2,b) = branches b in
345			(Fv.union fv1 fv2, Typed.Match (e, b))
346			\| Map (e,b) ->
347			let (fv1,e) = expr e
348			and (fv2,b) = branches b in
349			(Fv.union fv1 fv2, Typed.Map (e, b))
350	abate	5	in
351	abate	6	fv,
352			{ Typed.exp_loc = loc;
353	abate	5	Typed.exp_typ = Types.empty;
354			Typed.exp_descr = td;
355			}
356
357	abate	6	and branches b =
358			let fv = ref Fv.empty in
359			let b = List.map
360			(fun (p,e) ->
361			let (fv2,e) = expr e in
362			fv := Fv.union !fv fv2;
363			{ Typed.br_used = false;
364			Typed.br_pat = pat p;
365			Typed.br_body = e }
366			) b in
367	abate	9	(!fv, { Typed.br_typ = Types.empty; Typed.br_branches = b } )
368	abate	5
369	abate	6	module Env = StringMap
370
371			open Typed
372
373	abate	17
374			let check loc t s msg =
375			if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg))
376
377	abate	6	let rec compute_type env e =
378			let d = compute_type' e.exp_loc env e.exp_descr in
379			e.exp_typ <- Types.cup e.exp_typ d;
380			d
381
382			and compute_type' loc env = function
383			\| Var s -> Env.find s env
384			\| Apply (e1,e2) ->
385			let t1 = compute_type env e1 and t2 = compute_type env e2 in
386	abate	11	if Types.is_empty t2
387			then Types.empty
388			else
389			if Types.subtype t1 Types.Arrow.any
390			then
391			let t1 = Types.Arrow.get t1 in
392			let dom = Types.Arrow.domain t1 in
393			if Types.subtype t2 dom
394			then Types.Arrow.apply t1 t2
395			else
396			raise_loc loc
397			(Constraint
398			(t2,dom,"The argument is not in the domain of the function"))
399			else
400			raise_loc loc
401			(Constraint
402			(t1,Types.Arrow.any,"The expression in function position is not necessarily a function"))
403	abate	6	\| Abstraction a ->
404			let env = match a.fun_name with
405			\| None -> env
406			\| Some f -> Env.add f a.fun_typ env in
407			List.iter (fun (t1,t2) ->
408	abate	9	let t = type_branches loc env t1 a.fun_body in
409			if not (Types.subtype t t2) then
410			raise_loc loc (Constraint (t,t2,"Constraint not satisfied in interface"))
411	abate	6	) a.fun_iface;
412			a.fun_typ
413			\| Cst c -> Types.constant c
414			\| Pair (e1,e2) ->
415			let t1 = compute_type env e1 and t2 = compute_type env e2 in
416			let t1 = Types.cons t1 and t2 = Types.cons t2 in
417			Types.times t1 t2
418			\| RecordLitt r ->
419			List.fold_left
420			(fun accu (l,e) ->
421			let t = compute_type env e in
422			let t = Types.record l false (Types.cons t) in
423			Types.cap accu t
424			) Types.Record.any r
425	abate	16	\| Op (op, el) ->
426			let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in
427			type_op loc op args
428	abate	6	\| Match (e,b) ->
429			let t = compute_type env e in
430	abate	9	type_branches loc env t b
431	abate	17	\| Map (e,b) ->
432			let t = compute_type env e in
433			Sequence.map (fun t -> type_branches loc env t b) t
434	abate	6
435	abate	9	and type_branches loc env targ brs =
436	abate	6	if Types.is_empty targ then Types.empty
437	abate	9	else (
438			brs.br_typ <- Types.cup brs.br_typ targ;
439			branches_aux loc env targ Types.empty brs.br_branches
440			)
441	abate	6
442	abate	9	and branches_aux loc env targ tres = function
443			\| [] -> raise_loc loc (NonExhaustive targ)
444	abate	6	\| b :: rem ->
445			let p = b.br_pat in
446			let acc = Types.descr (Patterns.accept p) in
447
448			let targ' = Types.cap targ acc in
449			if Types.is_empty targ'
450	abate	9	then branches_aux loc env targ tres rem
451	abate	6	else
452			( b.br_used <- true;
453			let res = Patterns.filter targ' p in
454			let env' = List.fold_left
455			(fun env (x,t) -> Env.add x (Types.descr t) env)
456			env res in
457			let t = compute_type env' b.br_body in
458	abate	9	let tres = Types.cup t tres in
459			let targ'' = Types.diff targ acc in
460			if (Types.non_empty targ'') then
461			branches_aux loc env targ'' (Types.cup t tres) rem
462			else
463			tres
464	abate	6	)
465	abate	16
466			and type_op loc op args =
467			match (op,args) with
468			\| ("+", [loc1,t1; loc2,t2]) ->
469			type_int_binop Intervals.add loc1 t1 loc2 t2
470			\| ("*", [loc1,t1; loc2,t2]) ->
471			type_int_binop (fun i1 i2 -> Intervals.any) loc1 t1 loc2 t2
472	abate	17	\| ("@", [loc1,t1; loc2,t2]) ->
473			check loc1 t1 Sequence.any
474			"The first argument of @ must be a sequence";
475			Sequence.concat t1 t2
476			\| ("flatten", [loc1,t1]) ->
477			check loc1 t1 Sequence.seqseq
478			"The argument of flatten must be a sequence of sequences";
479			Sequence.flatten t1
480	abate	16	\| _ -> assert false
481
482			and type_int_binop f loc1 t1 loc2 t2 =
483			if not (Types.Int.is_int t1) then
484			raise_loc loc1
485			(Constraint
486			(t1,Types.Int.any,
487			"The first argument must be an integer"));
488			if not (Types.Int.is_int t2) then
489			raise_loc loc2
490			(Constraint
491			(t1,Types.Int.any,
492			"The second argument must be an integer"));
493			Types.Int.put
494			(f (Types.Int.get t1) (Types.Int.get t2));
495
496