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

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
      | 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
          (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))
      | 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 labs = ref [] in
          let r = List.map 
                    (fun (l,e) -> 
                       let (fv2,e) = expr e in
                       if (List.mem l !labs) then 
                         raise_loc loc (MultipleLabel l);
                       labs := l :: !labs;
                       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 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 = p;
                   Typed.br_body = e }
              ) b in
    (!fv, 
     { 
       Typed.br_typ = Types.empty; 
       Typed.br_branches = b; 
       Typed.br_accept = !accept 
     } 
    )

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 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 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) ->
           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
  | _ -> 
      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
  | 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)))
  | 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
  | 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
  | _ -> 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 
      (if precise then Types.empty else constr) 
      constr precise brs.br_branches
  )
    
and branches_aux loc env targ tres constr precise = 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 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 = 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'' 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 
               (t1,Types.Int.any,
                "The second argument must be an integer"));
  Types.Int.put
    (f (Types.Int.get t1) (Types.Int.get t2));
  

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