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

Diff of /typing/typer.ml

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

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