/[svn]/typing/typer.ml
ViewVC logotype

Diff of /typing/typer.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 72 by abate, Tue Jul 10 17:03:39 2007 UTC revision 427 by abate, Tue Jul 10 17:33:51 2007 UTC
# Line 1  Line 1 
1    (* TODO:
2     - rewrite type-checking of operators to propagate constraint
3     - optimize computation of pattern free variables
4     - check whether it is worth using recursive hash-consing internally
5    *)
6    
7    
8    let warning loc msg =
9      Format.fprintf !Location.warning_ppf "Warning %a:@\n%a%s@\n"
10        Location.print_loc loc
11        Location.html_hilight loc
12        msg
13    
14  (* I. Transform the abstract syntax of types and patterns into  (* I. Transform the abstract syntax of types and patterns into
15        the internal form *)        the internal form *)
16    
17  open Location  open Location
18  open Ast  open Ast
19    open Ident
20    
21    module S = struct type t = string let compare = compare end
22    module TypeEnv = Map.Make(S)
23    
 exception Pattern of string  
24  exception NonExhaustive of Types.descr  exception NonExhaustive of Types.descr
25  exception MultipleLabel of Types.label  exception Constraint of Types.descr * Types.descr
 exception Constraint of Types.descr * Types.descr * string  
26  exception ShouldHave of Types.descr * string  exception ShouldHave of Types.descr * string
27  exception WrongLabel of Types.descr * Types.label  exception ShouldHave2 of Types.descr * string * Types.descr
28  exception UnboundId of string  exception WrongLabel of Types.descr * label
29    exception UnboundId of id
30    exception Error of string
31    
32  let raise_loc loc exn = raise (Location (loc,exn))  let raise_loc loc exn = raise (Location (loc,exn))
33    let error loc msg = raise_loc loc (Error msg)
34    
 (* 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 * bool  
    | `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)  
35    
36  let mk' =  (* Eliminate Recursion, propagate Sequence Capture Variables *)
   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 defs = ref []  
   let name =  
     let c = ref 0 in  
     fun () ->  
       incr c;  
       "#" ^ (string_of_int !c)  
37    
38    let rec seq_vars accu = function    let rec seq_vars accu = function
39      | Epsilon | Elem _ -> accu      | Epsilon | Elem _ -> accu
40      | Seq (r1,r2) | Alt (r1,r2) -> seq_vars (seq_vars accu r1) r2      | Seq (r1,r2) | Alt (r1,r2) -> seq_vars (seq_vars accu r1) r2
41      | Star r | WeakStar r -> seq_vars accu r      | Star r | WeakStar r -> seq_vars accu r
42      | SeqCapture (v,r) -> seq_vars (StringSet.add v accu) r    | SeqCapture (v,r) -> seq_vars (IdSet.add v accu) r
43    
44    let uniq_id = let r = ref 0 in fun () -> incr r; !r  type derecurs_slot = {
45      ploc : Location.loc;
46    type flat = [ `Epsilon    pid  : int;
47                | `Elem of int * Ast.ppat  (* the int arg is used to    mutable ploop : bool;
48                                              to stop generic comparison *)    mutable pdescr : derecurs option
49                | `Seq of flat * flat  } and derecurs =
50                | `Alt of flat * flat    | PAlias of derecurs_slot
51                | `Star of flat    | PType of Types.descr
52                | `WeakStar of flat ]    | POr of derecurs * derecurs
53      | PAnd of derecurs * derecurs
54    let rec propagate vars : regexp -> flat = function    | PDiff of derecurs * derecurs
55      | Epsilon -> `Epsilon    | PTimes of derecurs * derecurs
56      | Elem x -> let p = vars x in `Elem (uniq_id (),p)    | PXml of derecurs * derecurs
57      | Seq (r1,r2) -> `Seq (propagate vars r1,propagate vars r2)    | PArrow of derecurs * derecurs
58      | Alt (r1,r2) -> `Alt (propagate vars r1, propagate vars r2)    | POptional of derecurs
59      | Star r -> `Star (propagate vars r)    | PRecord of bool * derecurs label_map
60      | WeakStar r -> `WeakStar (propagate vars r)    | PCapture of id
61      | SeqCapture (v,x) ->    | PConstant of id * Types.const
62          let v= mk noloc (Capture v) in    | PRegexp of derecurs_regexp * derecurs
63          propagate (fun p -> mk noloc (And (vars p,v,true))) x  and derecurs_regexp =
64      | PEpsilon
65    let cup r1 r2 =    | PElem of derecurs
66      match (r1,r2) with    | PSeq of derecurs_regexp * derecurs_regexp
67        | (_, `Empty) -> r1    | PAlt of derecurs_regexp * derecurs_regexp
68        | (`Empty, _) -> r2    | PStar of derecurs_regexp
69        | (`Res t1, `Res t2) -> `Res (mk noloc (Or (t1,t2)))    | PWeakStar of derecurs_regexp
70    
71  (*TODO: review this compilation schema to avoid explosion when  let rec hash_derecurs = function
72    coding (Optional x) by  (Or(Epsilon,x)); memoization ... *)    | PAlias s ->
73          s.pid
74    module Memo = Map.Make(struct type t = flat list let compare = compare end)    | PType t ->
75    module Coind = Set.Make(struct type t = flat list let compare = compare end)        1 + 17 * (Types.hash_descr t)
76    let memo = ref Memo.empty    | POr (p1,p2) ->
77          2 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
78    let rec compile fin e seq : [`Res of Ast.ppat | `Empty] =    | PAnd (p1,p2) ->
79      if Coind.mem seq !e then `Empty        3 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
80      else (    | PDiff (p1,p2) ->
81        e := Coind.add seq !e;        4 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
82        match seq with    | PTimes (p1,p2) ->
83          | [] ->        5 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
84              `Res fin    | PXml (p1,p2) ->
85          | `Epsilon :: rest ->        6 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
86              compile fin e rest    | PArrow (p1,p2) ->
87          | `Elem (_,p) :: rest ->        7 + 17 * (hash_derecurs p1) + 257 * (hash_derecurs p2)
88              `Res (mk noloc (Prod (p, guard_compile fin rest)))    | POptional p ->
89          | `Seq (r1,r2) :: rest ->        8 + 17 * (hash_derecurs p)
90              compile fin e (r1 :: r2 :: rest)    | PRecord (o,r) ->
91          | `Alt (r1,r2) :: rest ->        (if o then 9 else 10) + 17 * (LabelMap.hash hash_derecurs r)
92              cup (compile fin e (r1::rest)) (compile fin e (r2::rest))    | PCapture x ->
93          | `Star r :: rest ->        11 + 17 * (Id.hash x)
94              cup (compile fin e (r::seq)) (compile fin e rest)    | PConstant (x,c) ->
95          | `WeakStar r :: rest ->        12 + 17 * (Id.hash x) + 257 * (Types.hash_const c)
96              cup (compile fin e rest) (compile fin e (r::seq))    | PRegexp (p,q) ->
97          13 + 17 * (hash_derecurs_regexp p) + 257 * (hash_derecurs q)
98    and hash_derecurs_regexp = function
99      | PEpsilon ->
100          1
101      | PElem p ->
102          2 + 17 * (hash_derecurs p)
103      | PSeq (p1,p2) ->
104          3 + 17 * (hash_derecurs_regexp p1) + 257 * (hash_derecurs_regexp p2)
105      | PAlt (p1,p2) ->
106          4 + 17 * (hash_derecurs_regexp p1) + 257 * (hash_derecurs_regexp p2)
107      | PStar p ->
108          5 + 17 * (hash_derecurs_regexp p)
109      | PWeakStar p ->
110          6 + 17 * (hash_derecurs_regexp p)
111    
112    let rec equal_derecurs p1 p2 = (p1 == p2) || match p1,p2 with
113      | PAlias s1, PAlias s2 ->
114          s1 == s2
115      | PType t1, PType t2 ->
116          Types.equal_descr t1 t2
117      | POr (p1,q1), POr (p2,q2)
118      | PAnd (p1,q1), PAnd (p2,q2)
119      | PDiff (p1,q1), PDiff (p2,q2)
120      | PTimes (p1,q1), PTimes (p2,q2)
121      | PXml (p1,q1), PXml (p2,q2)
122      | PArrow (p1,q1), PArrow (p2,q2) ->
123          (equal_derecurs p1 p2) && (equal_derecurs q1 q2)
124      | POptional p1, POptional p2 ->
125          equal_derecurs p1 p2
126      | PRecord (o1,r1), PRecord (o2,r2) ->
127          (o1 == o2) && (LabelMap.equal equal_derecurs r1 r2)
128      | PCapture x1, PCapture x2 ->
129          Id.equal x1 x2
130      | PConstant (x1,c1), PConstant (x2,c2) ->
131          (Id.equal x1 x2) && (Types.equal_const c1 c2)
132      | PRegexp (p1,q1), PRegexp (p2,q2) ->
133          (equal_derecurs_regexp p1 p2) && (equal_derecurs q1 q2)
134      | _ -> false
135    and equal_derecurs_regexp r1 r2 = match r1,r2 with
136      | PEpsilon, PEpsilon ->
137          true
138      | PElem p1, PElem p2 ->
139          equal_derecurs p1 p2
140      | PSeq (p1,q1), PSeq (p2,q2)
141      | PAlt (p1,q1), PAlt (p2,q2) ->
142          (equal_derecurs_regexp p1 p2) && (equal_derecurs_regexp q1 q2)
143      | PStar p1, PStar p2
144      | PWeakStar p1, PWeakStar p2 ->
145          equal_derecurs_regexp p1 p2
146      | _ -> false
147    
148    module DerecursTable = Hashtbl.Make(
149      struct
150        type t = derecurs
151        let hash = hash_derecurs
152        let equal = equal_derecurs
153      end
154      )      )
155    and guard_compile fin seq =  
156      try Memo.find seq !memo  module RE = Hashtbl.Make(
157      with    struct
158          Not_found ->      type t = derecurs_regexp * derecurs
159            let n = name () in      let hash (p,q) =
160            let v = mk noloc (PatVar n) in        (hash_derecurs_regexp p) + 17 * (hash_derecurs q)
161            memo := Memo.add seq v !memo;      let equal (p1,q1) (p2,q2) =
162            let d = compile fin (ref Coind.empty) seq in        (equal_derecurs_regexp p1 p2) && (equal_derecurs q1 q2)
           (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))), true))  
   
   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 (fun p -> p) regexp] in  
     memo := Memo.empty;  
     let d = !defs in  
     defs := [];  
     mk noloc (Recurs (n,d))  
163  end  end
164    )
165    
 let compile_regexp = Regexp.compile  
166    
167    let counter = State.ref "Typer.counter - derecurs" 0
168    let mk_slot loc =
169      incr counter;
170      { ploop = false; ploc = loc; pid = !counter; pdescr = None }
171    
172  let rec compile env { loc = loc; descr = d } : ti =  let rec derecurs env p = match p.descr with
173    match (d : Ast.ppat') with    | PatVar v ->
174    | PatVar s ->        (try PAlias (TypeEnv.find v env)
       (try StringMap.find s env  
175         with Not_found ->         with Not_found ->
176           raise_loc loc (Pattern ("Undefined type variable " ^ s))           raise_loc_generic p.loc ("Undefined type/pattern " ^ v))
177        )    | Recurs (p,b) -> derecurs (derecurs_def env b) p
178    | Recurs (t, b) -> compile (compile_many env b) t    | Internal t -> PType t
179    | Regexp (r,q) -> compile env (Regexp.compile r q)    | Or (p1,p2) -> POr (derecurs env p1, derecurs env p2)
180    | Internal t -> cons loc (`Type t)    | And (p1,p2) -> PAnd (derecurs env p1, derecurs env p2)
181    | Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2))    | Diff (p1,p2) -> PDiff (derecurs env p1, derecurs env p2)
182    | And (t1,t2,e) -> cons loc (`And (compile env t1, compile env t2,e))    | Prod (p1,p2) -> PTimes (derecurs env p1, derecurs env p2)
183    | Diff (t1,t2) -> cons loc (`Diff (compile env t1, compile env t2))    | XmlT (p1,p2) -> PXml (derecurs env p1, derecurs env p2)
184    | Prod (t1,t2) -> cons loc (`Times (compile env t1, compile env t2))    | Arrow (p1,p2) -> PArrow (derecurs env p1, derecurs env p2)
185    | Arrow (t1,t2) -> cons loc (`Arrow (compile env t1, compile env t2))    | Optional p -> POptional (derecurs env p)
186    | Record (l,o,t) -> cons loc (`Record (l,o,compile env t))    | Record (o,r) -> PRecord (o, LabelMap.map (derecurs env) r)
187    | Constant (x,v) -> cons loc (`Constant (x,v))    | Capture x -> PCapture x
188    | Capture x -> cons loc (`Capture x)    | Constant (x,c) -> PConstant (x,c)
189      | Regexp (r,q) ->
190  and compile_many env b =        let constant_nil t v =
191    let b = List.map (fun (v,t) -> (v,t,mk' t.loc)) b in          PAnd (t, PConstant (v, Types.Atom Sequence.nil_atom)) in
192    let env =        let vars = seq_vars IdSet.empty r in
193      List.fold_left (fun env (v,t,x) -> StringMap.add v x env) env b in        let q = IdSet.fold constant_nil (derecurs env q) vars in
194    List.iter (fun (v,t,x) -> x.descr' <- `Alias (v, compile env t)) b;        let r = derecurs_regexp (fun p -> p) env r in
195          PRegexp (r, q)
196    and derecurs_regexp vars env = function
197      | Epsilon ->
198          PEpsilon
199      | Elem p ->
200          PElem (vars (derecurs env p))
201      | Seq (p1,p2) ->
202          PSeq (derecurs_regexp vars env p1, derecurs_regexp vars env p2)
203      | Alt (p1,p2) ->
204          PAlt (derecurs_regexp vars env p1, derecurs_regexp vars env p2)
205      | Star p ->
206          PStar (derecurs_regexp vars env p)
207      | WeakStar p ->
208          PWeakStar (derecurs_regexp vars env p)
209      | SeqCapture (x,p) ->
210          derecurs_regexp (fun p -> PAnd (vars p, PCapture x)) env p
211    
212    
213    and derecurs_def env b =
214      let b = List.map (fun (v,p) -> (v,p,mk_slot p.loc)) b in
215      let env = List.fold_left (fun env (v,p,s) -> TypeEnv.add v s env) env b in
216      List.iter (fun (v,p,s) -> s.pdescr <- Some (derecurs env p)) b;
217    env    env
218    
219    (* Stratification and recursive hash-consing *)
220    
221    type descr =
222      | IType of Types.descr
223      | IOr of descr * descr
224      | IAnd of descr * descr
225      | IDiff of descr * descr
226      | ITimes of slot * slot
227      | IXml of slot * slot
228      | IArrow of slot * slot
229      | IOptional of descr
230      | IRecord of bool * slot label_map
231      | ICapture of id
232      | IConstant of id * Types.const
233    and slot = {
234      mutable fv : fv option;
235      mutable hash : int option;
236      mutable rank1: int; mutable rank2: int;
237      mutable gen1 : int; mutable gen2: int;
238      mutable d    : descr option
239    }
240    
241  let comp_fv_seen = ref []  let descr s =
242  let comp_fv_res = ref []    match s.d with
243  let rec comp_fv s =      | Some d -> d
244    if List.memq s !comp_fv_seen then ()      | None -> assert false
245    
246    let gen = ref 0
247    let rank = ref 0
248    
249    let rec hash_descr = function
250      | IType x -> Types.hash_descr x
251      | IOr (d1,d2) -> 1 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
252      | IAnd (d1,d2) -> 2 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
253      | IDiff (d1,d2) -> 3 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
254      | IOptional d -> 4 + 17 * (hash_descr d)
255      | ITimes (s1,s2) -> 5 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
256      | IXml (s1,s2) -> 6 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
257      | IArrow (s1,s2) -> 7 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
258      | IRecord (o,r) -> (if o then 8 else 9) + 17 * (LabelMap.hash hash_slot r)
259      | ICapture x -> 10 + 17 * (Id.hash x)
260      | IConstant (x,y) -> 11 + 17 * (Id.hash x) + 257 * (Types.hash_const y)
261    and hash_slot s =
262      if s.gen1 = !gen then 13 * s.rank1
263    else (    else (
264      comp_fv_seen := s :: !comp_fv_seen;      incr rank;
265      (match s.descr' with      s.rank1 <- !rank; s.gen1 <- !gen;
266        | `Alias (_,x) -> comp_fv x      hash_descr (descr s)
       | `Or (s1,s2)  
       | `And (s1,s2,_)  
       | `Diff (s1,s2)  
       | `Times (s1,s2)  
       | `Arrow (s1,s2) -> comp_fv s1; comp_fv s2  
       | `Record (l,opt,s) -> comp_fv s  
       | `Type _ -> ()  
       | `Capture x  
       | `Constant (x,_) -> comp_fv_res := x :: !comp_fv_res);  
     if (!comp_fv_res = []) then s.fv <- Some [];  
     (* TODO: check that the above line is correct *)  
267    )    )
268    
269    let rec equal_descr d1 d2 =
270      match (d1,d2) with
271      | IType x1, IType x2 -> Types.equal_descr x1 x2
272      | IOr (x1,y1), IOr (x2,y2)
273      | IAnd (x1,y1), IAnd (x2,y2)
274      | IDiff (x1,y1), IDiff (x2,y2) -> (equal_descr x1 x2) && (equal_descr y1 y2)
275      | IOptional x1, IOptional x2 -> equal_descr x1 x2
276      | ITimes (x1,y1), ITimes (x2,y2)
277      | IXml (x1,y1), IXml (x2,y2)
278      | IArrow (x1,y1), IArrow (x2,y2) -> (equal_slot x1 x2) && (equal_slot y1 y2)
279      | IRecord (o1,r1), IRecord (o2,r2) ->
280          (o1 = o2) && (LabelMap.equal equal_slot r1 r2)
281      | ICapture x1, ICapture x2 -> Id.equal x1 x2
282      | IConstant (x1,y1), IConstant (x2,y2) ->
283          (Id.equal x1 x2) && (Types.equal_const y1 y2)
284      | _ -> false
285    and equal_slot s1 s2 =
286      ((s1.gen1 = !gen) && (s2.gen2 = !gen) && (s1.rank1 = s2.rank2))
287      ||
288      ((s1.gen1 <> !gen) && (s2.gen2 <> !gen) && (
289         incr rank;
290         s1.rank1 <- !rank; s1.gen1 <- !gen;
291         s2.rank2 <- !rank; s2.gen2 <- !gen;
292         equal_descr (descr s1) (descr s2)
293       ))
294    
295    module Arg = struct
296      type t = slot
297    
298      let hash s =
299        match s.hash with
300          | Some h -> h
301          | None ->
302              incr gen; rank := 0;
303              let h = hash_slot s in
304              s.hash <- Some h;
305              h
306    
307      let equal s1 s2 =
308        (s1 == s2) ||
309        (incr gen; rank := 0;
310         let e = equal_slot s1 s2 in
311    (*     if e then Printf.eprintf "Recursive hash-consig: Equal\n";  *)
312         e)
313    end
314    module SlotTable = Hashtbl.Make(Arg)
315    
316    let rec fv_slot s =
 let fv s =  
317    match s.fv with    match s.fv with
318      | Some l -> l      | Some x -> x
319      | None ->      | None ->
320          comp_fv s;          if s.gen1 = !gen then IdSet.empty
321          let l = SortedList.from_list !comp_fv_res in          else (s.gen1 <- !gen; fv_descr (descr s))
322          comp_fv_res := [];  and fv_descr = function
323          comp_fv_seen := [];    | IType _ -> IdSet.empty
324          s.fv <- Some l;    | IOr (d1,d2)
325          l    | IAnd (d1,d2)
326      | IDiff (d1,d2) -> IdSet.cup (fv_descr d1) (fv_descr d2)
327  let rec typ seen s : Types.descr =    | IOptional d -> fv_descr d
328    match s.descr' with    | ITimes (s1,s2)
329      | `Alias (v,x) ->    | IXml (s1,s2)
330          if List.memq s seen then    | IArrow (s1,s2) -> IdSet.cup (fv_slot s1) (fv_slot s2)
331            raise_loc s.loc'    | IRecord (o,r) ->
332              (Pattern        List.fold_left IdSet.cup IdSet.empty (LabelMap.map_to_list fv_slot r)
333                 ("Unguarded recursion on variable " ^ v ^ " in this type"))    | ICapture x | IConstant (x,_) -> IdSet.singleton x
         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  
334    
335  and typ_node s : Types.node =  
336    match s.type_node with  let compute_fv s =
337      | Some x -> x    match s.fv with
338        | Some x -> ()
339      | None ->      | None ->
340          let x = Types.make () in          incr gen;
341          s.type_node <- Some x;          let x = fv_slot s in
342          let t = typ [] s in          s.fv <- Some x
343          Types.define x t;  
344          x  
345    let todo_fv = ref []
346    
347  let type_node s =  let mk () =
348    let s = typ_node s in    let s =
349    let s = Types.internalize s in      { d = None;
350  (*  Types.define s (Types.normalize (Types.descr s)); *)        fv = None;
351          hash = None;
352          rank1 = 0; rank2 = 0;
353          gen1 = 0; gen2 = 0 } in
354      todo_fv := s :: !todo_fv;
355    s    s
356    
357  let rec pat seen s : Patterns.descr =  let flush_fv () =
358    if fv s = [] then Patterns.constr (type_node s) else    List.iter compute_fv !todo_fv;
359    match s.descr' with    todo_fv := []
     | `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,e) -> Patterns.cap (pat seen s1) (pat seen s2) e  
     | `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) true  
     | `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  
360    
361  and pat_node s : Patterns.node =  let compile_slot_hash = DerecursTable.create 67
362    match s.pat_node with  let compile_hash = DerecursTable.create 67
     | 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  
363    
364  let global_types = ref StringMap.empty  let defs = ref []
365    
366  let mk_typ e =  let rec compile p =
367    if fv e = [] then type_node e    try DerecursTable.find compile_hash p
368    else raise_loc e.loc' (Pattern "Capture variables are not allowed in types")    with Not_found ->
369        let c = real_compile p in
370        DerecursTable.replace compile_hash p c;
371        c
372    and real_compile = function
373      | PAlias v ->
374          if v.ploop then
375            raise_loc_generic v.ploc ("Unguarded recursion on type/pattern");
376          v.ploop <- true;
377          let r = match v.pdescr with Some x -> compile x | _ -> assert false in
378          v.ploop <- false;
379          r
380      | PType t -> IType t
381      | POr (t1,t2) -> IOr (compile t1, compile t2)
382      | PAnd (t1,t2) -> IAnd (compile t1, compile t2)
383      | PDiff (t1,t2) -> IDiff (compile t1, compile t2)
384      | PTimes (t1,t2) -> ITimes (compile_slot t1, compile_slot t2)
385      | PXml (t1,t2) -> IXml (compile_slot t1, compile_slot t2)
386      | PArrow (t1,t2) -> IArrow (compile_slot t1, compile_slot t2)
387      | POptional t -> IOptional (compile t)
388      | PRecord (o,r) ->  IRecord (o, LabelMap.map compile_slot r)
389      | PConstant (x,v) -> IConstant (x,v)
390      | PCapture x -> ICapture x
391      | PRegexp (r,q) -> compile_regexp r q
392    and compile_regexp r q =
393      let memo = RE.create 17 in
394      let rec aux accu r q =
395        if RE.mem memo (r,q) then accu
396        else (
397          RE.add memo (r,q) ();
398          match r with
399            | PEpsilon ->
400                (match q with
401                   | PRegexp (r,q) -> aux accu r q
402                   | _ -> (compile q) :: accu)
403            | PElem p -> ITimes (compile_slot p, compile_slot q) :: accu
404            | PSeq (r1,r2) -> aux accu r1 (PRegexp (r2,q))
405            | PAlt (r1,r2) -> aux (aux accu r1 q) r2 q
406            | PStar r1 -> aux (aux accu r1 (PRegexp (r,q))) PEpsilon q
407            | PWeakStar r1 -> aux (aux accu PEpsilon q) r1 (PRegexp (r,q))
408        )
409      in
410      let accu = aux [] r q in
411      match accu with
412        | [] -> assert false
413        | p::l -> List.fold_left (fun acc p -> IOr (p,acc)) p l
414    and compile_slot p =
415      try DerecursTable.find compile_slot_hash p
416      with Not_found ->
417        let s = mk () in
418        defs := (s,p) :: !defs;
419        DerecursTable.add compile_slot_hash p s;
420        s
421    
422    
423  let typ e =  let rec flush_defs () =
424    mk_typ (compile !global_types e)    match !defs with
425        | [] -> ()
426        | (s,p)::t -> defs := t; s.d <- Some (compile p); flush_defs ()
427    
428    let typ_nodes = SlotTable.create 67
429    let pat_nodes = SlotTable.create 67
430    
431    let rec typ = function
432      | IType t -> t
433      | IOr (s1,s2) -> Types.cup (typ s1) (typ s2)
434      | IAnd (s1,s2) ->  Types.cap (typ s1) (typ s2)
435      | IDiff (s1,s2) -> Types.diff (typ s1) (typ s2)
436      | ITimes (s1,s2) -> Types.times (typ_node s1) (typ_node s2)
437      | IXml (s1,s2) -> Types.xml (typ_node s1) (typ_node s2)
438      | IArrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)
439      | IOptional s -> Types.Record.or_absent (typ s)
440      | IRecord (o,r) -> Types.record' (o, LabelMap.map typ_node r)
441      | ICapture x | IConstant (x,_) -> assert false
442    
443    and typ_node s : Types.node =
444      try SlotTable.find typ_nodes s
445      with Not_found ->
446        let x = Types.make () in
447        SlotTable.add typ_nodes s x;
448        Types.define x (typ (descr s));
449        x
450    
451    let rec pat d : Patterns.descr =
452      if IdSet.is_empty (fv_descr d)
453      then Patterns.constr (typ d)
454      else pat_aux d
455    
456    
457    and pat_aux = function
458      | IOr (s1,s2) -> Patterns.cup (pat s1) (pat s2)
459      | IAnd (s1,s2) -> Patterns.cap (pat s1) (pat s2)
460      | IDiff (s1,s2) when IdSet.is_empty (fv_descr s2) ->
461          let s2 = Types.neg (typ s2) in
462          Patterns.cap (pat s1) (Patterns.constr s2)
463      | IDiff _ ->
464          raise (Patterns.Error "Difference not allowed in patterns")
465      | ITimes (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
466      | IXml (s1,s2) -> Patterns.xml (pat_node s1) (pat_node s2)
467      | IOptional _ ->
468          raise (Patterns.Error "Optional field not allowed in record patterns")
469      | IRecord (o,r) ->
470          let pats = ref [] in
471          let aux l s =
472            if IdSet.is_empty (fv_slot s) then typ_node s
473            else
474              ( pats := Patterns.record l (pat_node s) :: !pats;
475                Types.any_node )
476          in
477          let constr = Types.record' (o,LabelMap.mapi aux r) in
478          List.fold_left Patterns.cap (Patterns.constr constr) !pats
479            (* TODO: can avoid constr when o=true, and all fields have fv *)
480      | ICapture x -> Patterns.capture x
481      | IConstant (x,c) -> Patterns.constant x c
482      | IArrow _ ->
483          raise (Patterns.Error "Arrow not allowed in patterns")
484      | IType _ -> assert false
485    
486    and pat_node s : Patterns.node =
487      try SlotTable.find pat_nodes s
488      with Not_found ->
489        let x = Patterns.make (fv_slot s) in
490        SlotTable.add pat_nodes s x;
491        Patterns.define x (pat (descr s));
492        x
493    
494    let glb = State.ref "Typer.glb_env" TypeEnv.empty
495    
 let pat e =  
   let e = compile !global_types e in  
   pat_node e  
496    
497  let register_global_types b =  let register_global_types b =
498    let env = compile_many !global_types b in    List.iter
499    List.iter (fun (v,_) ->      (fun (v,p) ->
500                 let d = Types.descr (mk_typ (StringMap.find v env)) in         if TypeEnv.mem v !glb
501  (*             let d = Types.normalize d in*)         then raise_loc_generic p.loc ("Multiple definition for type " ^ v)
                Types.Print.register_global v d;  
                ()  
502              ) b;              ) b;
503    global_types := env    glb := derecurs_def !glb b;
504      let b = List.map (fun (v,p) -> (v,p,compile (derecurs !glb p))) b in
505      flush_defs ();
506      flush_fv ();
507      List.iter
508        (fun (v,p,s) ->
509           if not (IdSet.is_empty (fv_descr s)) then
510             raise_loc_generic p.loc "Capture variables are not allowed in types";
511           let t = typ s in
512           if (p.loc <> noloc) && (Types.is_empty t) then
513             warning p.loc ("This definition yields an empty type for " ^ v);
514           Types.Print.register_global v t) b
515    
516    let dump_global_types ppf =
517      TypeEnv.iter (fun v _ -> Format.fprintf ppf " %s" v) !glb
518    
519    
520    let typ p =
521      let s = compile_slot (derecurs !glb p) in
522      flush_defs ();
523      flush_fv ();
524      if IdSet.is_empty (fv_slot s) then typ_node s
525      else raise_loc_generic p.loc "Capture variables are not allowed in types"
526    
527    let pat p =
528      let s = compile_slot (derecurs !glb p) in
529      flush_defs ();
530      flush_fv ();
531      try pat_node s
532      with Patterns.Error e -> raise_loc_generic p.loc e
533        | Location (loc,exn) when loc = noloc -> raise (Location (p.loc, exn))
534    
535    
536  (* II. Build skeleton *)  (* II. Build skeleton *)
537    
538  module Fv = StringSet  module Fv = IdSet
539    
540    type branch = Branch of Typed.branch * branch list
541    
542  let rec expr { loc = loc; descr = d } =  let cur_branch : branch list ref = ref []
543    let (fv,td) =  
544      match d with  let exp loc fv e =
545        | DebugTyper t -> (Fv.empty, Typed.DebugTyper (typ t))    fv,
546      { Typed.exp_loc = loc;
547        Typed.exp_typ = Types.empty;
548        Typed.exp_descr = e;
549      }
550    
551    
552    let rec expr loc = function
553      | LocatedExpr (loc,e) -> expr loc e
554        | Forget (e,t) ->        | Forget (e,t) ->
555            let (fv,e) = expr e and t = typ t in        let (fv,e) = expr loc e and t = typ t in
556            (fv, Typed.Forget (e,t))        exp loc fv (Typed.Forget (e,t))
557        | Var s -> (Fv.singleton s, Typed.Var s)    | Var s ->
558          exp loc (Fv.singleton s) (Typed.Var s)
559        | Apply (e1,e2) ->        | Apply (e1,e2) ->
560            let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in        let (fv1,e1) = expr loc e1 and (fv2,e2) = expr loc e2 in
561            (Fv.union fv1 fv2, Typed.Apply (e1,e2))        exp loc (Fv.cup fv1 fv2) (Typed.Apply (e1,e2))
562        | Abstraction a ->        | Abstraction a ->
563            let iface = List.map (fun (t1,t2) -> (typ t1, typ t2)) a.fun_iface in        let iface = List.map (fun (t1,t2) -> (typ t1, typ t2))
564                        a.fun_iface in
565            let t = List.fold_left            let t = List.fold_left
566                      (fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2))                      (fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2))
567                      Types.any iface in                      Types.any iface in
# Line 354  Line 572 
572            let fv = match a.fun_name with            let fv = match a.fun_name with
573              | None -> fv0              | None -> fv0
574              | Some f -> Fv.remove f fv0 in              | Some f -> Fv.remove f fv0 in
575            (fv,        let e = Typed.Abstraction
            Typed.Abstraction  
576               { Typed.fun_name = a.fun_name;               { Typed.fun_name = a.fun_name;
577                 Typed.fun_iface = iface;                 Typed.fun_iface = iface;
578                 Typed.fun_body = body;                 Typed.fun_body = body;
579                 Typed.fun_typ = t;                 Typed.fun_typ = t;
580                 Typed.fun_fv = Fv.elements fv                    Typed.fun_fv = fv
581               }                  } in
582            )        exp loc fv e
583        | Cst c -> (Fv.empty, Typed.Cst c)    | Cst c ->
584          exp loc Fv.empty (Typed.Cst c)
585        | Pair (e1,e2) ->        | Pair (e1,e2) ->
586            let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in        let (fv1,e1) = expr loc e1 and (fv2,e2) = expr loc e2 in
587            (Fv.union fv1 fv2, Typed.Pair (e1,e2))        exp loc (Fv.cup fv1 fv2) (Typed.Pair (e1,e2))
588      | Xml (e1,e2) ->
589          let (fv1,e1) = expr loc e1 and (fv2,e2) = expr loc e2 in
590          exp loc (Fv.cup fv1 fv2) (Typed.Xml (e1,e2))
591        | Dot (e,l) ->        | Dot (e,l) ->
592            let (fv,e) = expr e in        let (fv,e) = expr loc e in
593            (fv,  Typed.Dot (e,l))        exp loc fv (Typed.Dot (e,l))
594      | RemoveField (e,l) ->
595          let (fv,e) = expr loc e in
596          exp loc fv (Typed.RemoveField (e,l))
597        | RecordLitt r ->        | RecordLitt r ->
598            let fv = ref Fv.empty in            let fv = ref Fv.empty in
599            let r  = List.sort (fun (l1,_) (l2,_) -> compare l1 l2) r in        let r = LabelMap.map
600            let r = List.map                  (fun e ->
601                      (fun (l,e) ->                     let (fv2,e) = expr loc e
602                         let (fv2,e) = expr e in fv := Fv.union !fv fv2; (l,e))                     in fv := Fv.cup !fv fv2; e)
603                      r in                      r in
604            let rec check = function        exp loc !fv (Typed.RecordLitt r)
             | (l1,_) :: (l2,_) :: _ when l1 = l2 ->  
                 raise_loc loc (MultipleLabel l1)  
             | _ :: rem -> check rem  
             | _ -> () in  
           check r;  
           (!fv, Typed.RecordLitt r)  
605        | Op (op,le) ->        | Op (op,le) ->
606            let (fvs,ltes) = List.split (List.map expr le) in        let (fvs,ltes) = List.split (List.map (expr loc) le) in
607            let fv = List.fold_left Fv.union Fv.empty fvs in        let fv = List.fold_left Fv.cup Fv.empty fvs in
608            (fv, Typed.Op (op,ltes))        (try
609             (match (ltes,Typed.find_op op) with
610                | [e], `Unary op -> exp loc fv (Typed.UnaryOp (op, e))
611                | [e1;e2], `Binary op -> exp loc fv (Typed.BinaryOp (op, e1,e2))
612                | _ -> assert false)
613           with Not_found -> assert false)
614    
615        | Match (e,b) ->        | Match (e,b) ->
616            let (fv1,e) = expr e        let (fv1,e) = expr loc e
617            and (fv2,b) = branches b in            and (fv2,b) = branches b in
618            (Fv.union fv1 fv2, Typed.Match (e, b))        exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b))
619        | Map (e,b) ->        | Map (e,b) ->
620            let (fv1,e) = expr e        let (fv1,e) = expr loc e
621          and (fv2,b) = branches b in
622          exp loc (Fv.cup fv1 fv2) (Typed.Map (e, b))
623      | Transform (e,b) ->
624          let (fv1,e) = expr loc e
625            and (fv2,b) = branches b in            and (fv2,b) = branches b in
626            (Fv.union fv1 fv2, Typed.Map (e, b))        exp loc (Fv.cup fv1 fv2) (Typed.Transform (e, b))
627      | Xtrans (e,b) ->
628          let (fv1,e) = expr loc e
629          and (fv2,b) = branches b in
630          exp loc (Fv.cup fv1 fv2) (Typed.Xtrans (e, b))
631        | Try (e,b) ->        | Try (e,b) ->
632            let (fv1,e) = expr e        let (fv1,e) = expr loc e
633            and (fv2,b) = branches b in            and (fv2,b) = branches b in
634            (Fv.union fv1 fv2, Typed.Try (e, b))        exp loc (Fv.cup fv1 fv2) (Typed.Try (e, b))
635    in  
   fv,  
   { Typed.exp_loc = loc;  
     Typed.exp_typ = Types.empty;  
     Typed.exp_descr = td;  
   }  
636    
637    and branches b =    and branches b =
638      let fv = ref Fv.empty in      let fv = ref Fv.empty in
639      let accept = ref Types.empty in      let accept = ref Types.empty in
640      let b = List.map      let branch (p,e) =
641                (fun (p,e) ->        let cur_br = !cur_branch in
642                   let (fv2,e) = expr e in        cur_branch := [];
643          let (fv2,e) = expr noloc e in
644          let br_loc = merge_loc p.loc e.Typed.exp_loc in
645                   let p = pat p in                   let p = pat p in
646                   let fv2 = List.fold_right Fv.remove (Patterns.fv p) fv2 in        let fv2 = Fv.diff fv2 (Patterns.fv p) in
647                   fv := Fv.union !fv fv2;        fv := Fv.cup !fv fv2;
648                   accept := Types.cup !accept (Types.descr (Patterns.accept p));                   accept := Types.cup !accept (Types.descr (Patterns.accept p));
649                   { Typed.br_used = false;        let br =
650            {
651              Typed.br_loc = br_loc;
652              Typed.br_used = br_loc = noloc;
653                     Typed.br_pat = p;                     Typed.br_pat = p;
654                     Typed.br_body = e }            Typed.br_body = e } in
655                ) b in        cur_branch := Branch (br, !cur_branch) :: cur_br;
656          br in
657        let b = List.map branch b in
658      (!fv,      (!fv,
659       {       {
660         Typed.br_typ = Types.empty;         Typed.br_typ = Types.empty;
# Line 430  Line 664 
664       }       }
665      )      )
666    
667    let expr = expr noloc
668    
669  let let_decl p e =  let let_decl p e =
670    let (_,e) = expr e in    let (_,e) = expr e in
671    { Typed.let_pat = pat p;    { Typed.let_pat = pat p;
# Line 438  Line 674 
674    
675  (* III. Type-checks *)  (* III. Type-checks *)
676    
 module Env = StringMap  
677  type env = Types.descr Env.t  type env = Types.descr Env.t
678    
679  open Typed  open Typed
680    
681  let warning loc msg =  let require loc t s =
682    Format.fprintf Format.std_formatter    if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
683      "Warning %a:@\n%s@\n" Location.print_loc loc msg  
684    let check loc t s =
685      require loc t s; t
686    
687    let should_have loc constr s =
688      raise_loc loc (ShouldHave (constr,s))
689    
690  let check loc t s msg =  let flatten loc arg constr precise =
691    if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg))    let constr' = Sequence.star
692                      (Sequence.approx (Types.cap Sequence.any constr)) in
693      let sconstr' = Sequence.star constr' in
694      let exact = Types.subtype constr' constr in
695      if exact then
696        let t = arg sconstr' precise in
697        if precise then Sequence.flatten t else constr
698      else
699        let t = arg sconstr' true in
700        Sequence.flatten t
701    
702  let rec type_check env e constr precise =  let rec type_check env e constr precise =
 (*  Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"  
     Types.Print.print_descr constr precise;  
 *)  
703    let d = type_check' e.exp_loc env e.exp_descr constr precise in    let d = type_check' e.exp_loc env e.exp_descr constr precise in
704      let d = if precise then d else constr in
705    e.exp_typ <- Types.cup e.exp_typ d;    e.exp_typ <- Types.cup e.exp_typ d;
706    d    d
707    
# Line 462  Line 709 
709    | Forget (e,t) ->    | Forget (e,t) ->
710        let t = Types.descr t in        let t = Types.descr t in
711        ignore (type_check env e t false);        ignore (type_check env e t false);
712        t        check loc t constr
713    
714    | Abstraction a ->    | Abstraction a ->
715        let t =        let t =
716          try Types.Arrow.check_strenghten a.fun_typ constr          try Types.Arrow.check_strenghten a.fun_typ constr
717          with Not_found ->          with Not_found ->
718            raise_loc loc            should_have loc constr
719            (ShouldHave              "but the interface of the abstraction is not compatible"
              (constr, "but the interface of the abstraction is not compatible"))  
720        in        in
721        let env = match a.fun_name with        let env = match a.fun_name with
722          | None -> env          | None -> env
723          | Some f -> Env.add f a.fun_typ env in          | Some f -> Env.add f a.fun_typ env in
724        List.iter        List.iter
725          (fun (t1,t2) ->          (fun (t1,t2) ->
726               let acc = a.fun_body.br_accept in
727               if not (Types.subtype t1 acc) then
728                 raise_loc loc (NonExhaustive (Types.diff t1 acc));
729             ignore (type_check_branches loc env t1 a.fun_body t2 false)             ignore (type_check_branches loc env t1 a.fun_body t2 false)
730          ) a.fun_iface;          ) a.fun_iface;
731        t        t
# Line 490  Line 740 
740        Types.cup te tb        Types.cup te tb
741    
742    | Pair (e1,e2) ->    | Pair (e1,e2) ->
743        let rects = Types.Product.get constr in        type_check_pair loc env e1 e2 constr precise
       if Types.Product.is_empty rects then  
         raise_loc loc (ShouldHave (constr,"but it is a pair."));  
       let pi1 = Types.Product.pi1 rects in  
744    
745        let t1 = type_check env e1 (Types.Product.pi1 rects)    | Xml (e1,e2) ->
746                   (precise || (Types.Product.need_second rects))in        type_check_pair ~kind:`XML loc env e1 e2 constr precise
       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  
747    
748    | RecordLitt r ->    | RecordLitt r ->
749        let rconstr = Types.Record.get constr in        type_record loc env r constr precise
       if Types.Record.is_empty rconstr then  
         raise_loc loc (ShouldHave (constr,"but it is a record."));  
   
       let (rconstr,res) =  
         List.fold_left  
           (fun (rconstr,res) (l,e) ->  
              let rconstr = Types.Record.restrict_label_present rconstr l in  
              let pi = Types.Record.project_field rconstr l in  
              if Types.Record.is_empty rconstr then  
                raise_loc loc  
                  (ShouldHave (constr,(Printf.sprintf  
                                         "Field %s is not allowed here."  
                                         (Types.label_name l)  
                                      )  
                              ));  
              let t = type_check env e pi true in  
              let rconstr = Types.Record.restrict_field rconstr l t in  
   
              let res =  
                if precise  
                then Types.cap res (Types.record l false (Types.cons t))  
                else res in  
              (rconstr,res)  
           ) (rconstr, if precise then Types.Record.any else constr) r  
       in  
       res  
750    
751    | Map (e,b) ->    | Map (e,b) ->
752        let t = type_check env e (Sequence.star b.br_accept) true in        type_map loc env false e b constr precise
   
       let constr' = Sequence.approx (Types.cap Sequence.any constr) in  
       let exact = Types.subtype (Sequence.star constr') constr in  
       (* Note:  
          - could be more precise by integrating the decomposition  
          of constr inside Sequence.map.  
       *)  
       let res =  
         Sequence.map  
           (fun t ->  
              type_check_branches loc env t b constr' (precise || (not exact)))  
           t in  
       if not exact then check loc res constr "";  
       if precise then res else constr  
   | Op ("@", [e1;e2]) ->  
       let constr' = Sequence.star  
                       (Sequence.approx (Types.cap Sequence.any constr)) in  
       let exact = Types.subtype constr' constr in  
       if exact then  
         let t1 = type_check env e1 constr' precise  
         and t2 = type_check env e2 constr' precise in  
         if precise then Sequence.concat t1 t2 else constr  
       else  
         (* Note:  
            the knownledge of t1 may makes it useless to  
            check t2 with 'precise' ... *)  
         let t1 = type_check env e1 constr' true  
         and t2 = type_check env e2 constr' true in  
         let res = Sequence.concat t1 t2 in  
         check loc res constr "";  
         if precise then res else constr  
   | Op ("flatten", [e]) ->  
       let constr' = Sequence.star  
                       (Sequence.approx (Types.cap Sequence.any constr)) in  
       let sconstr' = Sequence.star constr' in  
       let exact = Types.subtype constr' constr in  
       if exact then  
         let t = type_check env e sconstr' precise in  
         if precise then Sequence.flatten t else constr  
       else  
         let t = type_check env e sconstr' true in  
         let res = Sequence.flatten t in  
         check loc res constr "";  
         if precise then res else constr  
   | _ ->  
       let t : Types.descr = compute_type' loc env e in  
       check loc t constr "";  
       t  
753    
754  and compute_type env e =    | Transform (e,b) ->
755    type_check env e Types.any true        flatten loc (type_map loc env true e b) constr precise
756    
 and compute_type' loc env = function  
   | DebugTyper t -> Types.descr t  
   | Var s ->  
       (try Env.find s env  
        with Not_found -> raise_loc loc (UnboundId s)  
       )  
757    | Apply (e1,e2) ->    | Apply (e1,e2) ->
758        let t1 = type_check env e1 Types.Arrow.any true in        let t1 = type_check env e1 Types.Arrow.any true in
759        let t1 = Types.Arrow.get t1 in        let t1 = Types.Arrow.get t1 in
760        let dom = Types.Arrow.domain t1 in        let dom = Types.Arrow.domain t1 in
761          let res =
762        if Types.Arrow.need_arg t1 then        if Types.Arrow.need_arg t1 then
763          let t2 = type_check env e2 dom true in          let t2 = type_check env e2 dom true in
764          Types.Arrow.apply t1 t2          Types.Arrow.apply t1 t2
765        else        else
766          (ignore (type_check env e2 dom false); Types.Arrow.apply_noarg t1)          (ignore (type_check env e2 dom false); Types.Arrow.apply_noarg t1)
767    | Cst c -> Types.constant c        in
768          check loc res constr
769    
770      | UnaryOp (o,e) ->
771          let t = o.un_op_typer loc
772                    (type_check env e) constr precise in
773          check loc t constr
774    
775      | BinaryOp (o,e1,e2) ->
776          let t = o.bin_op_typer loc
777                    (type_check env e1)
778                    (type_check env e2) constr precise in
779          check loc t constr
780    
781      | Var s ->
782          let t =
783            try Env.find s env
784            with Not_found -> raise_loc loc (UnboundId s) in
785          check loc t constr
786    
787      | Cst c ->
788          check loc (Types.constant c) constr
789    
790    | Dot (e,l) ->    | Dot (e,l) ->
791        let t = type_check env e Types.Record.any true in        let t = type_check env e Types.Record.any true in
792           (try (Types.Record.project t l)        let t =
793            with Not_found -> raise_loc loc (WrongLabel(t,l)))          try (Types.Record.project t l)
794    | Op (op, el) ->          with Not_found -> raise_loc loc (WrongLabel(t,l))
795        let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in        in
796        type_op loc op args        check loc t constr
   | 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  
797    
798  (* We keep these cases here to allow comparison and benchmarking ...    | RemoveField (e,l) ->
799     Just comment the corresponding cases in type_check' to        let t = type_check env e Types.Record.any true in
800     activate these ones.        let t = Types.Record.remove_field t l in
801  *)        check loc t constr
802    | Pair (e1,e2) ->  
803        let t1 = compute_type env e1    | Xtrans (e,b) ->
804        and t2 = compute_type env e2 in        let t = type_check env e Sequence.any true in
805        Types.times (Types.cons t1) (Types.cons t2)        let t =
806    | RecordLitt r ->          Sequence.map_tree
807        List.fold_left            (fun t ->
808          (fun accu (l,e) ->               let resid = Types.diff t b.br_accept in
809             let t = compute_type env e in               let res = type_check_branches loc env t b Sequence.any true in
810             let t = Types.record l false (Types.cons t) in               (res,resid)
811             Types.cap accu t            ) t in
812          ) Types.Record.any r        check loc t constr
813    
814    
815    and type_check_pair ?(kind=`Normal) loc env e1 e2 constr precise =
816      let rects = Types.Product.normal ~kind constr in
817      if Types.Product.is_empty rects then
818        (match kind with
819          | `Normal -> should_have loc constr "but it is a pair"
820          | `XML -> should_have loc constr "but it is an XML element");
821      let need_s = Types.Product.need_second rects in
822      let t1 = type_check env e1 (Types.Product.pi1 rects) (precise || need_s) in
823      let c2 = Types.Product.constraint_on_2 rects t1 in
824      if Types.is_empty c2 then
825        raise_loc loc (ShouldHave2 (constr,"but the first component has type",t1));
826      let t2 = type_check env e2 c2 precise in
827    
828      if precise then
829        match kind with
830          | `Normal -> Types.times (Types.cons t1) (Types.cons t2)
831          | `XML -> Types.xml (Types.cons t1) (Types.cons t2)
832      else
833        constr
834    
835    and type_record loc env r constr precise =
836    (* try to get rid of precise = true for values of fields *)
837    (* also: the use equivalent of need_second to optimize... *)
838      if not (Types.Record.has_record constr) then
839        should_have loc constr "but it is a record";
840      let (rconstr,res) =
841        List.fold_left
842          (fun (rconstr,res) (l,e) ->
843             (* could compute (split l e) once... *)
844             let pi = Types.Record.project_opt rconstr l in
845             if Types.is_empty pi then
846               (let l = U.to_string (LabelPool.value l) in
847                should_have loc constr
848                  (Printf.sprintf "Field %s is not allowed here." l));
849             let t = type_check env e pi true in
850             let rconstr = Types.Record.condition rconstr l t in
851             let res = (l,Types.cons t) :: res in
852             (rconstr,res)
853          ) (constr, []) (LabelMap.get r)
854      in
855      if not (Types.Record.has_empty_record rconstr) then
856        should_have loc constr "More fields should be present";
857      let t =
858        Types.record' (false, LabelMap.from_list (fun _ _ -> assert false) res)
859      in
860      check loc t constr
861    
   | _ -> assert false  
862    
863  and type_check_branches loc env targ brs constr precise =  and type_check_branches loc env targ brs constr precise =
864    if Types.is_empty targ then Types.empty    if Types.is_empty targ then Types.empty
# Line 643  Line 870 
870    )    )
871    
872  and branches_aux loc env targ tres constr precise = function  and branches_aux loc env targ tres constr precise = function
873    | [] -> raise_loc loc (NonExhaustive targ)    | [] -> tres
874    | b :: rem ->    | b :: rem ->
875        let p = b.br_pat in        let p = b.br_pat in
876        let acc = Types.descr (Patterns.accept p) in        let acc = Types.descr (Patterns.accept p) in
# Line 666  Line 893 
893              tres              tres
894          )          )
895    
896    and type_map loc env def e b constr precise =
897      let acc = if def then Sequence.any else Sequence.star b.br_accept in
898      let t = type_check env e acc true in
899    
900      let constr' = Sequence.approx (Types.cap Sequence.any constr) in
901      let exact = Types.subtype (Sequence.star constr') constr in
902      (* Note:
903         - could be more precise by integrating the decomposition
904         of constr inside Sequence.map.
905      *)
906      let res =
907        Sequence.map
908          (fun t ->
909             let res =
910               type_check_branches loc env t b constr' (precise || (not exact)) in
911             if def && not (Types.subtype t b.br_accept)
912             then Types.cup res Sequence.nil_type
913             else res)
914          t in
915      if exact then res else check loc res constr
916    
917  and type_let_decl env l =  and type_let_decl env l =
918    let acc = Types.descr (Patterns.accept l.let_pat) in    let acc = Types.descr (Patterns.accept l.let_pat) in
919    let t = type_check env l.let_body acc true in    let t = type_check env l.let_body acc true in
# Line 692  Line 940 
940    types    types
941    
942    
943  and type_op loc op args =  let rec unused_branches b =
944    match (op,args) with    List.iter
945      | "+", [loc1,t1; loc2,t2] ->      (fun (Branch (br,s)) ->
946          type_int_binop Intervals.add loc1 t1 loc2 t2         if not br.br_used
947      | "-", [loc1,t1; loc2,t2] ->         then warning br.br_loc "This branch is not used"
948          type_int_binop Intervals.sub loc1 t1 loc2 t2         else unused_branches s
949      | ("*" | "/"), [loc1,t1; loc2,t2] ->      )
950          type_int_binop (fun i1 i2 -> Intervals.any) loc1 t1 loc2 t2      b
     | "@", [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  
     | "load_xml", [loc1,t1] ->  
         check loc1 t1 Sequence.string  
           "The argument of load_xml must be a string (filename)";  
         Types.any  
     | "raise", [loc1,t1] ->  
         Types.empty  
     | "int_of", [loc1,t1] ->  
         check loc1 t1 Sequence.string  
           "The argument of int_of must a string";  
         if not (Types.subtype t1 Builtin.intstr) then  
           warning loc "This application of int_of may fail";  
         Types.interval Intervals.any  
     | _ -> assert false  
   
 and type_int_binop f loc1 t1 loc2 t2 =  
   if not (Types.Int.is_int t1) then  
     raise_loc loc1  
       (Constraint  
          (t1,Types.Int.any,  
           "The first argument must be an integer"));  
   if not (Types.Int.is_int t2) then  
     raise_loc loc2  
       (Constraint  
                (t2,Types.Int.any,  
                 "The second argument must be an integer"));  
   Types.Int.put  
     (f (Types.Int.get t1) (Types.Int.get t2));  
951    
952    let report_unused_branches () =
953      unused_branches !cur_branch;
954      cur_branch := []
955    
Legend:
Removed from v.72  
changed lines
  Added in v.427
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5