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

Diff of /typing/typer.ml

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

revision 16 by abate, Tue Jul 10 16:58:05 2007 UTC revision 172 by abate, Tue Jul 10 17:12:31 2007 UTC
# Line 4  Line 4 
4  open Location  open Location
5  open Ast  open Ast
6    
7  exception Pattern of string  module S = struct type t = string let compare = compare end
8    module StringMap = Map.Make(S)
9    module StringSet = Set.Make(S)
10    
11  exception NonExhaustive of Types.descr  exception NonExhaustive of Types.descr
12    exception MultipleLabel of Types.label
13  exception Constraint of Types.descr * Types.descr * string  exception Constraint of Types.descr * Types.descr * string
14    exception ShouldHave of Types.descr * string
15    exception WrongLabel of Types.descr * Types.label
16    exception UnboundId of string
17    
18  let raise_loc loc exn = raise (Location (loc,exn))  let raise_loc loc exn = raise (Location (loc,exn))
19    
# Line 15  Line 22 
22    
23  type ti = {  type ti = {
24    id : int;    id : int;
25      mutable seen : bool;
26    mutable loc' : loc;    mutable loc' : loc;
27    mutable fv : string SortedList.t option;    mutable fv : StringSet.t option;
28    mutable descr': descr;    mutable descr': descr;
29    mutable type_node: Types.node option;    mutable type_node: Types.node option;
30    mutable pat_node: Patterns.node option    mutable pat_node: Patterns.node option
31  }  }
32  and descr =  and descr =
33     [ `Alias of string * ti    | IAlias of string * ti
34     | `Type of Types.descr    | IType of Types.descr
35     | `Or of ti * ti    | IOr of ti * ti
36     | `And of ti * ti    | IAnd of ti * ti
37     | `Diff of ti * ti    | IDiff of ti * ti
38     | `Times of ti * ti    | ITimes of ti * ti
39     | `Arrow of ti * ti    | IXml of ti * ti
40     | `Record of Types.label * bool * ti    | IArrow of ti * ti
41     | `Capture of Patterns.capture    | IRecord of bool * (Types.label * bool * ti) list
42     | `Constant of Patterns.capture * Types.const    | ICapture of Patterns.capture
43     ]    | IConstant of Patterns.capture * Types.const
44    
45    
46    type glb = ti StringMap.t
 module S = struct type t = string let compare = compare end  
 module StringMap = Map.Make(S)  
 module StringSet = Set.Make(S)  
47    
48  let mk' =  let mk' =
49    let counter = ref 0 in    let counter = ref 0 in
# Line 46  Line 51 
51      incr counter;      incr counter;
52      let rec x = {      let rec x = {
53        id = !counter;        id = !counter;
54          seen = false;
55        loc' = loc;        loc' = loc;
56        fv = None;        fv = None;
57        descr' = `Alias ("__dummy__", x);        descr' = IAlias ("__dummy__", x);
58        type_node = None;        type_node = None;
59        pat_node = None        pat_node = None
60      } in      } in
# Line 69  Line 75 
75  *)  *)
76    
77  module Regexp = struct  module Regexp = struct
   let memo = Hashtbl.create 51  
78    let defs = ref []    let defs = ref []
79    let name =    let name =
80      let c = ref 0 in      let c = ref 0 in
# Line 83  Line 88 
88      | Star r | WeakStar r -> seq_vars accu r      | Star r | WeakStar r -> seq_vars accu r
89      | SeqCapture (v,r) -> seq_vars (StringSet.add v accu) r      | SeqCapture (v,r) -> seq_vars (StringSet.add v accu) r
90    
91    let rec propagate vars = function    let uniq_id = let r = ref 0 in fun () -> incr r; !r
     | Epsilon -> `Epsilon  
     | Elem x -> `Elem (vars,x)  
     | Seq (r1,r2) -> `Seq (propagate vars r1,propagate vars r2)  
     | Alt (r1,r2) -> `Alt (propagate vars r1, propagate vars r2)  
     | Star r -> `Star (propagate vars r)  
     | WeakStar r -> `WeakStar (propagate vars r)  
     | SeqCapture (v,x) -> propagate (StringSet.add v vars) x  
92    
93      type flat =
94        | REpsilon
95        | RElem of int * Ast.ppat  (* the int arg is used
96                                                to stop generic comparison *)
97        | RSeq of flat * flat
98        | RAlt of flat * flat
99        | RStar of flat
100        | RWeakStar of flat
101    
102      let re_loc = ref noloc
103    
104      let rec propagate vars : regexp -> flat = function
105        | Epsilon -> REpsilon
106        | Elem x -> let p = vars x in RElem (uniq_id (),p)
107        | Seq (r1,r2) -> RSeq (propagate vars r1,propagate vars r2)
108        | Alt (r1,r2) -> RAlt (propagate vars r1, propagate vars r2)
109        | Star r -> RStar (propagate vars r)
110        | WeakStar r -> RWeakStar (propagate vars r)
111        | SeqCapture (v,x) ->
112            let v= mk !re_loc (Capture v) in
113            propagate (fun p -> mk !re_loc (And (vars p,v))) x
114    
115      let dummy_pat = mk noloc (PatVar "DUMMY")
116    let cup r1 r2 =    let cup r1 r2 =
117      match (r1,r2) with      if r1 == dummy_pat then r2 else
118        | (_, `Empty) -> r1        if r2 == dummy_pat then r1 else
119        | (`Empty, _) -> r2          mk !re_loc (Or (r1,r2))
       | (`Res t1, `Res t2) -> `Res (mk noloc (Or (t1,t2)))  
120    
121    let rec compile fin e seq : [`Res of Ast.ppat | `Empty] =  (*TODO: review this compilation schema to avoid explosion when
122      if List.mem seq e then `Empty    coding (Optional x) by  (Or(Epsilon,x)); memoization ... *)
123      else  
124        let e = seq :: e in    module Memo = Map.Make(struct type t = flat list let compare = compare end)
125      module Coind = Set.Make(struct type t = flat list let compare = compare end)
126      let memo = ref Memo.empty
127    
128    
129      let rec compile fin e seq : Ast.ppat =
130        if Coind.mem seq !e then dummy_pat
131        else (
132          e := Coind.add seq !e;
133        match seq with        match seq with
134          | [] ->          | [] ->
135              `Res fin              fin
136          | `Epsilon :: rest ->          | REpsilon :: rest ->
137              compile fin e rest              compile fin e rest
138          | `Elem (vars,x) :: rest ->          | RElem (_,p) :: rest ->
139              let capt = StringSet.fold              mk !re_loc (Prod (p, guard_compile fin rest))
140                           (fun v t -> mk noloc (And (t, (mk noloc (Capture v)))))          | RSeq (r1,r2) :: rest ->
                          vars x in  
             `Res (mk noloc (Prod (capt, guard_compile fin rest)))  
         | `Seq (r1,r2) :: rest ->  
141              compile fin e (r1 :: r2 :: rest)              compile fin e (r1 :: r2 :: rest)
142          | `Alt (r1,r2) :: rest ->          | RAlt (r1,r2) :: rest ->
143              cup (compile fin e (r1::rest)) (compile fin e (r2::rest))              cup (compile fin e (r1::rest)) (compile fin e (r2::rest))
144          | `Star r :: rest -> cup (compile fin e (r::seq)) (compile fin e rest)          | RStar r :: rest ->
145          | `WeakStar r :: rest -> cup (compile fin e rest) (compile fin e (r::seq))              cup (compile fin e (r::seq)) (compile fin e rest)
146            | RWeakStar r :: rest ->
147                cup (compile fin e rest) (compile fin e (r::seq))
148        )
149    and guard_compile fin seq =    and guard_compile fin seq =
150      try Hashtbl.find memo seq      try Memo.find seq !memo
151      with      with
152          Not_found ->          Not_found ->
153            let n = name () in            let n = name () in
154            let v = mk noloc (PatVar n) in            let v = mk !re_loc (PatVar n) in
155            Hashtbl.add memo seq v;            memo := Memo.add seq v !memo;
156            let d = compile fin [] seq in            let d = compile fin (ref Coind.empty) seq in
157            (match d with            assert (d != dummy_pat);
158               | `Empty -> assert false            defs := (n,d) :: !defs;
              | `Res d -> defs := (n,d) :: !defs);  
159            v            v
160    
161    (*
162      type trans = [ `Alt of gnode * gnode | `Elem of Ast.ppat * gnode | `Final ]
163      and gnode =
164          {
165            mutable seen  : bool;
166            mutable compile : bool;
167            name  : string;
168            mutable trans : trans;
169          }
170    
171      let new_node() = { seen = false; compile = false;
172                         name = name(); trans = `Final }
173      let to_compile = ref []
174    
175      let rec compile after = function
176        | `Epsilon -> after
177        | `Elem (_,p) ->
178            if not after.compile then (after.compile <- true;
179                                       to_compile := after :: !to_compile);
180            { new_node () with trans = `Elem (p, after)  }
181        | `Seq(r1,r2) -> compile (compile after r2) r1
182        | `Alt(r1,r2) ->
183            let r1 = compile after r1 and r2 = compile after r2 in
184            { new_node () with trans = `Alt (r1,r2) }
185        | `Star r ->
186            let n  = new_node() in
187            n.trans <- `Alt (compile n r, after);
188            n
189        | `WeakStar r ->
190            let n  = new_node() in
191            n.trans <- `Alt (after, compile n r);
192            n
193    
194      let seens = ref []
195      let rec collect_aux accu n =
196        if n.seen then accu
197        else ( seens := n :: !seens;
198               match n.trans with
199                 | `Alt (n1,n2) -> collect_aux (collect_aux accu n2) n1
200                 | _ -> n :: accu
201             )
202    
203      let collect fin n =
204        let l = collect_aux [] n in
205        List.iter (fun n -> n.seen <- false) !seens;
206        let l = List.map (fun n ->
207                            match n.trans with
208                              | `Final -> fin
209                              | `Elem (p,a) ->
210                                  mk !re_loc (Prod(p, mk !re_loc (PatVar a.name)))
211                              | _ -> assert false
212                         ) l in
213        match l with
214          | h::t ->
215              List.fold_left (fun accu p -> mk !re_loc (Or (accu,p))) h t
216          | _ -> assert false
217    *)
218    
219    
   let atom_nil = Types.mk_atom "nil"  
220    let constant_nil v t =    let constant_nil v t =
221      mk noloc (And (t, (mk noloc (Constant (v, Types.Atom atom_nil)))))      mk !re_loc
222          (And (t, (mk !re_loc (Constant (v, Types.Atom Sequence.nil_atom)))))
223    
224    let compile regexp queue : ppat =    let compile loc regexp queue : ppat =
225        re_loc := loc;
226      let vars = seq_vars StringSet.empty regexp in      let vars = seq_vars StringSet.empty regexp in
227      let fin = StringSet.fold constant_nil vars queue in      let fin = StringSet.fold constant_nil vars queue in
228      let n = guard_compile fin [propagate StringSet.empty regexp] in      let re = propagate (fun p -> p) regexp in
229      Hashtbl.clear memo;      let n = guard_compile fin [re] in
230        memo := Memo.empty;
231      let d = !defs in      let d = !defs in
232      defs := [];      defs := [];
233      mk noloc (Recurs (n,d))  
234    (*
235        let after = new_node() in
236        let n = collect queue (compile after re) in
237        let d = List.map (fun n -> (n.name, collect queue n)) !to_compile in
238        to_compile := [];
239    *)
240    
241        mk !re_loc (Recurs (n,d))
242  end  end
243    
244  let compile_regexp = Regexp.compile  let compile_regexp = Regexp.compile noloc
245    
246    
247  let rec compile env { loc = loc; descr = d } : ti =  let rec compile env { loc = loc; descr = d } : ti =
# Line 155  Line 249 
249    | PatVar s ->    | PatVar s ->
250        (try StringMap.find s env        (try StringMap.find s env
251         with Not_found ->         with Not_found ->
252           raise_loc loc (Pattern ("Undefined type variable " ^ s))           raise_loc_generic loc ("Undefined type variable " ^ s)
253        )        )
254    | Recurs (t, b) -> compile (compile_many env b) t    | Recurs (t, b) -> compile (compile_many env b) t
255    | Regexp (r,q) -> compile env (Regexp.compile r q)    | Regexp (r,q) -> compile env (Regexp.compile loc r q)
256    | Internal t -> cons loc (`Type t)    | Internal t -> cons loc (IType t)
257    | Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2))    | Or (t1,t2) -> cons loc (IOr (compile env t1, compile env t2))
258    | And (t1,t2) -> cons loc (`And (compile env t1, compile env t2))    | And (t1,t2) -> cons loc (IAnd (compile env t1, compile env t2))
259    | Diff (t1,t2) -> cons loc (`Diff (compile env t1, compile env t2))    | Diff (t1,t2) -> cons loc (IDiff (compile env t1, compile env t2))
260    | Prod (t1,t2) -> cons loc (`Times (compile env t1, compile env t2))    | Prod (t1,t2) -> cons loc (ITimes (compile env t1, compile env t2))
261    | Arrow (t1,t2) -> cons loc (`Arrow (compile env t1, compile env t2))    | XmlT (t1,t2) -> cons loc (IXml (compile env t1, compile env t2))
262    | Record (l,o,t) -> cons loc (`Record (l,o,compile env t))    | Arrow (t1,t2) -> cons loc (IArrow (compile env t1, compile env t2))
263    | Constant (x,v) -> cons loc (`Constant (x,v))    | Record (o,r) ->
264    | Capture x -> cons loc (`Capture x)        cons loc (IRecord (o, List.map (fun (l,o,t) -> l,o,compile env t) r))
265      | Constant (x,v) -> cons loc (IConstant (x,v))
266      | Capture x -> cons loc (ICapture x)
267    
268  and compile_many env b =  and compile_many env b =
269    let b = List.map (fun (v,t) -> (v,t,mk' t.loc)) b in    let b = List.map (fun (v,t) -> (v,t,mk' t.loc)) b in
270    let env =    let env =
271      List.fold_left (fun env (v,t,x) -> StringMap.add v x env) env b in      List.fold_left (fun env (v,t,x) -> StringMap.add v x env) env b in
272    List.iter (fun (v,t,x) -> x.descr' <- `Alias (v, compile env t)) b;    List.iter (fun (v,t,x) -> x.descr' <- IAlias (v, compile env t)) b;
273    env    env
274    
275    module IntSet =
276      Set.Make(struct type t = int let compare (x:int) y = compare x y end)
277    
278  let rec comp_fv seen s =  let comp_fv_seen = ref []
279    let comp_fv_res = ref StringSet.empty
280    let rec comp_fv s =
281    match s.fv with    match s.fv with
282      | Some l -> l      | Some fv -> comp_fv_res := StringSet.union fv !comp_fv_res
283      | None ->      | None ->
284          let l =          (match s.descr' with
285            match s.descr' with             | IAlias (_,x) ->
286              | `Alias (_,x) -> if List.memq s seen then [] else comp_fv (s :: seen) x                 if x.seen then ()
287              | `Or (s1,s2)                 else (
288              | `And (s1,s2)                   x.seen <- true;
289              | `Diff (s1,s2)                   comp_fv_seen := x :: !comp_fv_seen;
290              | `Times (s1,s2)                   comp_fv x
291              | `Arrow (s1,s2) -> SortedList.cup (comp_fv seen s1) (comp_fv seen s2)                 )
292              | `Record (l,opt,s) -> comp_fv seen s             | IOr (s1,s2)
293              | `Type _ -> []             | IAnd (s1,s2)
294              | `Capture x             | IDiff (s1,s2)
295              | `Constant (x,_) -> [x]             | ITimes (s1,s2) | IXml (s1,s2)
296          in             | IArrow (s1,s2) -> comp_fv s1; comp_fv s2
297          if seen = [] then s.fv <- Some l;             | IRecord (_,r) -> List.iter (fun (l,opt,s) -> comp_fv s) r
298          l             | IType _ -> ()
299               | ICapture x
300               | IConstant (x,_) -> comp_fv_res := StringSet.add x !comp_fv_res
301            )
302    
303    
304  let fv = comp_fv []  let fv s =
305      match s.fv with
306        | Some l -> l
307        | None ->
308            comp_fv s;
309            let l = !comp_fv_res in
310            comp_fv_res := StringSet.empty;
311            List.iter (fun n -> n.seen <- false) !comp_fv_seen;
312            comp_fv_seen := [];
313            s.fv <- Some l;
314            l
315    
316  let rec typ seen s : Types.descr =  let rec typ seen s : Types.descr =
317    match s.descr' with    match s.descr' with
318      | `Alias (v,x) ->      | IAlias (v,x) ->
319          if List.memq s seen then          if IntSet.mem s.id seen then
320            raise_loc s.loc'            raise_loc_generic s.loc'
321              (Pattern              ("Unguarded recursion on variable " ^ v ^ " in this type")
322                 ("Unguarded recursion on variable " ^ v ^ " in this type"))          else typ (IntSet.add s.id seen) x
323          else typ (s :: seen) x      | IType t -> t
324      | `Type t -> t      | IOr (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)
325      | `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)      | IAnd (s1,s2) ->  Types.cap (typ seen s1) (typ seen s2)
326      | `And (s1,s2) ->  Types.cap (typ seen s1) (typ seen s2)      | IDiff (s1,s2) -> Types.diff (typ seen s1) (typ seen s2)
327      | `Diff (s1,s2) -> Types.diff (typ seen s1) (typ seen s2)      | ITimes (s1,s2) -> Types.times (typ_node s1) (typ_node s2)
328      | `Times (s1,s2) -> Types.times (typ_node s1) (typ_node s2)      | IXml (s1,s2) ->   Types.xml (typ_node s1) (typ_node s2)
329      | `Arrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)      | IArrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)
330      | `Record (l,o,s) -> Types.record l o (typ_node s)      | IRecord (o,r) ->
331      | `Capture _ | `Constant _ -> assert false          Types.record'
332              (o,List.map (fun (l,o,s) -> (l,(o,typ_node s))) r)
333        | ICapture x | IConstant (x,_) -> assert false
334    
335  and typ_node s : Types.node =  and typ_node s : Types.node =
336    match s.type_node with    match s.type_node with
# Line 223  Line 338 
338      | None ->      | None ->
339          let x = Types.make () in          let x = Types.make () in
340          s.type_node <- Some x;          s.type_node <- Some x;
341          let t = typ [] s in          let t = typ IntSet.empty s in
342          Types.define x t;          Types.define x t;
343          x          x
344    
345  let type_node s = Types.internalize (typ_node s)  let type_node s =
346      let s = typ_node s in
347      let s = Types.internalize s in
348    (*  Types.define s (Types.normalize (Types.descr s)); *)
349      s
350    
351  let rec pat seen s : Patterns.descr =  let rec pat seen s : Patterns.descr =
352    if fv s = [] then Patterns.constr (type_node s) else    if StringSet.is_empty (fv s)
353    match s.descr' with    then Patterns.constr (Types.descr (type_node s))
354      | `Alias (v,x) ->    else
355          if List.memq s seen then      try pat_aux seen s
356            raise_loc s.loc'      with Patterns.Error e -> raise_loc_generic s.loc' e
357              (Pattern        | Location (loc,exn) when loc = noloc -> raise (Location (s.loc', exn))
358                 ("Unguarded recursion on variable " ^ v ^ " in this pattern"))  
359          else pat (s :: seen) x  
360      | `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)  and pat_aux seen s = match s.descr' with
361      | `And (s1,s2) -> Patterns.cap (pat seen s1) (pat seen s2)    | IAlias (v,x) ->
362      | `Diff (s1,s2) when fv s2 = [] ->        if IntSet.mem s.id seen
363          let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in        then raise
364            (Patterns.Error
365               ("Unguarded recursion on variable " ^ v ^ " in this pattern"));
366          pat (IntSet.add s.id seen) x
367      | IOr (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)
368      | IAnd (s1,s2) -> Patterns.cap (pat seen s1) (pat seen s2)
369      | IDiff (s1,s2) when StringSet.is_empty (fv s2) ->
370          let s2 = Types.neg (Types.descr (type_node s2)) in
371          Patterns.cap (pat seen s1) (Patterns.constr s2)          Patterns.cap (pat seen s1) (Patterns.constr s2)
372      | `Diff _ ->    | IDiff _ ->
373          raise_loc s.loc' (Pattern "Difference not allowed in patterns")        raise (Patterns.Error "Difference not allowed in patterns")
374      | `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)    | ITimes (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
375      | `Record (l,false,s) -> Patterns.record l (pat_node s)    | IXml (s1,s2) -> Patterns.xml (pat_node s1) (pat_node s2)
376      | `Record _ ->    | IRecord (o,r) ->
377          raise_loc s.loc'        let pats = ref [] in
378            (Pattern "Optional field not allowed in record patterns")        let aux (l,o,s) =
379      | `Capture x ->  Patterns.capture x          if StringSet.is_empty (fv s) then (l,(o,type_node s))
380      | `Constant (x,c) -> Patterns.constant x c          else
381      | `Arrow _ ->            if o then
382          raise_loc s.loc' (Pattern "Arrow not allowed in patterns")              raise
383      | `Type _ -> assert false                (Patterns.Error
384                     "Optional field not allowed in record patterns")
385              else (
386                pats := Patterns.record l (pat_node s) :: !pats;
387                (l,(false,Types.any_node))
388              ) in
389          let constr = Types.record' (o,List.map aux r) in
390          List.fold_left Patterns.cap (Patterns.constr constr) !pats
391    (* TODO: can avoid constr when o=true, and all fields have fv *)
392      | ICapture x ->  Patterns.capture x
393      | IConstant (x,c) -> Patterns.constant x c
394      | IArrow _ ->
395          raise (Patterns.Error "Arrow not allowed in patterns")
396      | IType _ -> assert false
397    
398  and pat_node s : Patterns.node =  and pat_node s : Patterns.node =
399    match s.pat_node with    match s.pat_node with
400      | Some x -> x      | Some x -> x
401      | None ->      | None ->
402          let x = Patterns.make (fv s) in          let fv = SortedList.from_list (StringSet.elements (fv s)) in
403            let x = Patterns.make fv in
404          s.pat_node <- Some x;          s.pat_node <- Some x;
405          let t = pat [] s in          let t = pat IntSet.empty s in
406          Patterns.define x t;          Patterns.define x t;
407          x          x
408    
 let global_types = ref StringMap.empty  
   
409  let mk_typ e =  let mk_typ e =
410    if fv e = [] then type_node e    if StringSet.is_empty (fv e) then type_node e
411    else raise_loc e.loc' (Pattern "Capture variables are not allowed in types")    else raise_loc_generic e.loc' "Capture variables are not allowed in types"
412    
413    
414  let typ e =  let typ glb e =
415    mk_typ (compile !global_types e)    mk_typ (compile glb e)
416    
417    let pat glb e =
418      pat_node (compile glb e)
419    
420    let register_global_types glb b =
421      let env' = compile_many glb b in
422      List.fold_left
423        (fun glb (v,{ loc = loc }) ->
424           let t = StringMap.find v env' in
425           let d = Types.descr (mk_typ t) in
426           (*              let d = Types.normalize d in*)
427           Types.Print.register_global v d;
428           if StringMap.mem v glb
429           then raise_loc_generic loc ("Multiple definition for type " ^ v);
430           StringMap.add v t glb
431        ) glb b
432    
 let pat e =  
   let e = compile !global_types e in  
   pat_node e  
   
 let register_global_types b =  
   let env = compile_many !global_types b in  
   List.iter (fun (v,_) ->  
                let d = Types.descr (mk_typ (StringMap.find v env)) in  
                Types.Print.register_global v d  
             ) b;  
   global_types := env  
433    
434    
435  (* II. Build skeleton *)  (* II. Build skeleton *)
436    
437  module Fv = StringSet  module Fv = StringSet
438    
439  let rec expr { loc = loc; descr = d } =  (* IDEA: introduce a node Loc in the AST to override nolocs
440       in sub-expressions *)
441    
442    let rec expr loc' glb { loc = loc; descr = d } =
443      let loc =  if loc = noloc then loc' else loc in
444    let (fv,td) =    let (fv,td) =
445      match d with      match d with
446          | Forget (e,t) ->
447              let (fv,e) = expr loc glb e and t = typ glb t in
448              (fv, Typed.Forget (e,t))
449        | Var s -> (Fv.singleton s, Typed.Var s)        | Var s -> (Fv.singleton s, Typed.Var s)
450        | Apply (e1,e2) ->        | Apply (e1,e2) ->
451            let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in            let (fv1,e1) = expr loc glb e1 and (fv2,e2) = expr loc glb e2 in
452            (Fv.union fv1 fv2, Typed.Apply (e1,e2))            (Fv.union fv1 fv2, Typed.Apply (e1,e2))
453        | Abstraction a ->        | Abstraction a ->
454            let iface = List.map (fun (t1,t2) -> (typ t1, typ t2)) a.fun_iface in            let iface = List.map (fun (t1,t2) -> (typ glb t1, typ glb t2))
455                            a.fun_iface in
456            let t = List.fold_left            let t = List.fold_left
457                      (fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2))                      (fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2))
458                      Types.any iface in                      Types.any iface in
459            let iface = List.map            let iface = List.map
460                          (fun (t1,t2) -> (Types.descr t1, Types.descr t2))                          (fun (t1,t2) -> (Types.descr t1, Types.descr t2))
461                          iface in                          iface in
462            let (fv0,body) = branches a.fun_body in            let (fv0,body) = branches loc glb a.fun_body in
463            let fv = match a.fun_name with            let fv = match a.fun_name with
464              | None -> fv0              | None -> fv0
465              | Some f -> Fv.remove f fv0 in              | Some f -> Fv.remove f fv0 in
# Line 318  Line 469 
469                 Typed.fun_iface = iface;                 Typed.fun_iface = iface;
470                 Typed.fun_body = body;                 Typed.fun_body = body;
471                 Typed.fun_typ = t;                 Typed.fun_typ = t;
472                 Typed.fun_fv = Fv.elements fv0                 Typed.fun_fv = Fv.elements fv
473               }               }
474            )            )
475        | Cst c -> (Fv.empty, Typed.Cst c)        | Cst c -> (Fv.empty, Typed.Cst c)
476        | Pair (e1,e2) ->        | Pair (e1,e2) ->
477            let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in            let (fv1,e1) = expr loc glb e1 and (fv2,e2) = expr loc glb e2 in
478            (Fv.union fv1 fv2, Typed.Pair (e1,e2))            (Fv.union fv1 fv2, Typed.Pair (e1,e2))
479          | Xml (e1,e2) ->
480              let (fv1,e1) = expr loc glb e1 and (fv2,e2) = expr loc glb e2 in
481              (Fv.union fv1 fv2, Typed.Xml (e1,e2))
482          | Dot (e,l) ->
483              let (fv,e) = expr loc glb e in
484              (fv,  Typed.Dot (e,l))
485        | RecordLitt r ->        | RecordLitt r ->
           (* XXX TODO: check that no label appears twice *)  
486            let fv = ref Fv.empty in            let fv = ref Fv.empty in
487              let r  = List.sort (fun (l1,_) (l2,_) -> compare l1 l2) r in
488            let r = List.map            let r = List.map
489                      (fun (l,e) ->                      (fun (l,e) ->
490                         let (fv2,e) = expr e in                         let (fv2,e) = expr loc glb e
491                         fv := Fv.union !fv fv2;                         in fv := Fv.union !fv fv2; (l,e))
492                         (l,e)                      r in
493                      ) r in            let rec check = function
494                | (l1,_) :: (l2,_) :: _ when l1 = l2 ->
495                    raise_loc loc (MultipleLabel l1)
496                | _ :: rem -> check rem
497                | _ -> () in
498              check r;
499            (!fv, Typed.RecordLitt r)            (!fv, Typed.RecordLitt r)
500        | Op (op,le) ->        | Op (op,le) ->
501            let (fvs,ltes) = List.split (List.map expr le) in            let (fvs,ltes) = List.split (List.map (expr loc glb) le) in
502            let fv = List.fold_left Fv.union Fv.empty fvs in            let fv = List.fold_left Fv.union Fv.empty fvs in
503            (fv, Typed.Op (op,ltes))            (fv, Typed.Op (op,ltes))
504        | Match (e,b) ->        | Match (e,b) ->
505            let (fv1,e) = expr e            let (fv1,e) = expr loc glb e
506            and (fv2,b) = branches b in            and (fv2,b) = branches loc glb b in
507            (Fv.union fv1 fv2, Typed.Match (e, b))            (Fv.union fv1 fv2, Typed.Match (e, b))
508        | Map (e,b) ->        | Map (e,b) ->
509            let (fv1,e) = expr e            let (fv1,e) = expr loc glb e
510            and (fv2,b) = branches b in            and (fv2,b) = branches loc glb b in
511            (Fv.union fv1 fv2, Typed.Map (e, b))            (Fv.union fv1 fv2, Typed.Map (e, b))
512          | Try (e,b) ->
513              let (fv1,e) = expr loc glb e
514              and (fv2,b) = branches loc glb b in
515              (Fv.union fv1 fv2, Typed.Try (e, b))
516    in    in
517    fv,    fv,
518    { Typed.exp_loc = loc;    { Typed.exp_loc = loc;
# Line 354  Line 520 
520      Typed.exp_descr = td;      Typed.exp_descr = td;
521    }    }
522    
523    and branches b =    and branches loc glb b =
524      let fv = ref Fv.empty in      let fv = ref Fv.empty in
525        let accept = ref Types.empty in
526      let b = List.map      let b = List.map
527                (fun (p,e) ->                (fun (p,e) ->
528                   let (fv2,e) = expr e in                   let (fv2,e) = expr loc glb e in
529                     let p = pat glb p in
530                     let fv2 = List.fold_right Fv.remove (Patterns.fv p) fv2 in
531                   fv := Fv.union !fv fv2;                   fv := Fv.union !fv fv2;
532                     accept := Types.cup !accept (Types.descr (Patterns.accept p));
533                   { Typed.br_used = false;                   { Typed.br_used = false;
534                     Typed.br_pat = pat p;                     Typed.br_pat = p;
535                     Typed.br_body = e }                     Typed.br_body = e }
536                ) b in                ) b in
537      (!fv, { Typed.br_typ = Types.empty; Typed.br_branches = b } )      (!fv,
538         {
539           Typed.br_typ = Types.empty;
540           Typed.br_branches = b;
541           Typed.br_accept = !accept;
542           Typed.br_compiled = None;
543         }
544        )
545    
546    let expr = expr noloc
547    
548    let let_decl glb p e =
549      let (_,e) = expr glb e in
550      { Typed.let_pat = pat glb p;
551        Typed.let_body = e;
552        Typed.let_compiled = None }
553    
554    (* III. Type-checks *)
555    
556  module Env = StringMap  module Env = StringMap
557    type env = Types.descr Env.t
558    
559  open Typed  open Typed
560    
561  let rec compute_type env e =  let warning loc msg =
562    let d = compute_type' e.exp_loc env e.exp_descr in    Format.fprintf !Location.warning_ppf "Warning %a:@\n%a%s@\n"
563        Location.print_loc loc
564        Location.html_hilight loc
565        msg
566    
567    let check loc t s msg =
568      if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg))
569    
570    let rec type_check env e constr precise =
571    (*  Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
572        Types.Print.print_descr constr precise;
573    *)
574      let d = type_check' e.exp_loc env e.exp_descr constr precise in
575    e.exp_typ <- Types.cup e.exp_typ d;    e.exp_typ <- Types.cup e.exp_typ d;
576    d    d
577    
578  and compute_type' loc env = function  and type_check' loc env e constr precise = match e with
579    | Var s -> Env.find s env    | Forget (e,t) ->
580    | Apply (e1,e2) ->        let t = Types.descr t in
581        let t1 = compute_type env e1 and t2 = compute_type env e2 in        ignore (type_check env e t false);
582        if Types.is_empty t2        t
       then Types.empty  
       else  
         if Types.subtype t1 Types.Arrow.any  
         then  
           let t1 = Types.Arrow.get t1 in  
           let dom = Types.Arrow.domain t1 in  
           if Types.subtype t2 dom  
           then Types.Arrow.apply t1 t2  
           else  
             raise_loc loc  
               (Constraint  
                  (t2,dom,"The argument is not in the domain of the function"))  
         else  
           raise_loc loc  
             (Constraint  
                (t1,Types.Arrow.any,"The expression in function position is not necessarily a function"))  
583    | Abstraction a ->    | Abstraction a ->
584          let t =
585            try Types.Arrow.check_strenghten a.fun_typ constr
586            with Not_found ->
587              raise_loc loc
588              (ShouldHave
589                 (constr, "but the interface of the abstraction is not compatible"))
590          in
591        let env = match a.fun_name with        let env = match a.fun_name with
592          | None -> env          | None -> env
593          | Some f -> Env.add f a.fun_typ env in          | Some f -> Env.add f a.fun_typ env in
594        List.iter (fun (t1,t2) ->        List.iter
595                     let t = type_branches loc env t1 a.fun_body in          (fun (t1,t2) ->
596                     if not (Types.subtype t t2) then             ignore (type_check_branches loc env t1 a.fun_body t2 false)
                      raise_loc loc (Constraint (t,t2,"Constraint not satisfied in interface"))  
597                  ) a.fun_iface;                  ) a.fun_iface;
598        a.fun_typ        t
599    | Cst c -> Types.constant c  
600      | Match (e,b) ->
601          let t = type_check env e b.br_accept true in
602          type_check_branches loc env t b constr precise
603    
604      | Try (e,b) ->
605          let te = type_check env e constr precise in
606          let tb = type_check_branches loc env Types.any b constr precise in
607          Types.cup te tb
608    
609    | Pair (e1,e2) ->    | Pair (e1,e2) ->
610        let t1 = compute_type env e1 and t2 = compute_type env e2 in        type_check_pair loc env e1 e2 constr precise
611        let t1 = Types.cons t1 and t2 = Types.cons t2 in    | Xml (e1,e2) ->
612        Types.times t1 t2        type_check_pair ~kind:`XML loc env e1 e2 constr precise
613    
614    (*
615    | RecordLitt r ->    | RecordLitt r ->
616          let rconstr = Types.Record.get constr in
617          if Types.Record.is_empty rconstr then
618            raise_loc loc (ShouldHave (constr,"but it is a record."));
619    
620    (* Completely buggy !  Need to check at the end that all required labels
621       are present ...A better to do it without precise = true ? *)
622          let precise = true in
623    
624          let (rconstr,res) =
625        List.fold_left        List.fold_left
626          (fun accu (l,e) ->            (fun (rconstr,res) (l,e) ->
627             let t = compute_type env e in               let rconstr = Types.Record.restrict_label_present rconstr l in
628             let t = Types.record l false (Types.cons t) in               let pi = Types.Record.project_field rconstr l in
629             Types.cap accu t               if Types.Record.is_empty rconstr then
630          ) Types.Record.any r                 raise_loc loc
631                     (ShouldHave (constr,(Printf.sprintf
632                                            "Field %s is not allowed here."
633                                            (Types.LabelPool.value l)
634                                         )
635                                 ));
636                 let t = type_check env e pi true in
637                 let rconstr = Types.Record.restrict_field rconstr l t in
638    
639                 let res =
640                   if precise
641                   then Types.cap res (Types.record l false (Types.cons t))
642                   else res in
643                 (rconstr,res)
644              ) (rconstr, if precise then Types.Record.any else constr) r
645          in
646    (*      check loc res constr ""; *)
647          res
648    *)
649    
650      | Map (e,b) ->
651          let t = type_check env e (Sequence.star b.br_accept) true in
652    
653          let constr' = Sequence.approx (Types.cap Sequence.any constr) in
654          let exact = Types.subtype (Sequence.star constr') constr in
655          (* Note:
656             - could be more precise by integrating the decomposition
657             of constr inside Sequence.map.
658          *)
659          let res =
660            Sequence.map
661              (fun t ->
662                 type_check_branches loc env t b constr' (precise || (not exact)))
663              t in
664          if not exact then check loc res constr "";
665          if precise then res else constr
666      | Op ("@", [e1;e2]) ->
667          let constr' = Sequence.star
668                          (Sequence.approx (Types.cap Sequence.any constr)) in
669          let exact = Types.subtype constr' constr in
670          if exact then
671            let t1 = type_check env e1 constr' precise
672            and t2 = type_check env e2 constr' precise in
673            if precise then Sequence.concat t1 t2 else constr
674          else
675            (* Note:
676               the knownledge of t1 may makes it useless to
677               check t2 with 'precise' ... *)
678            let t1 = type_check env e1 constr' true
679            and t2 = type_check env e2 constr' true in
680            let res = Sequence.concat t1 t2 in
681            check loc res constr "";
682            if precise then res else constr
683      | Apply (e1,e2) ->
684    (*
685          let constr' = Sequence.star
686                          (Sequence.approx (Types.cap Sequence.any constr)) in
687          let t1 = type_check env e1 (Types.cup Types.Arrow.any constr') true in
688          let t1_fun = Types.Arrow.get t1 in
689    
690          let has_fun = not (Types.Arrow.is_empty t1_fun)
691          and has_seq = not (Types.subtype t1 Types.Arrow.any) in
692    
693          let constr' =
694            Types.cap
695              (if has_fun then Types.Arrow.domain t1_fun else Types.any)
696              (if has_seq then constr' else Types.any)
697          in
698          let need_arg = has_fun && Types.Arrow.need_arg t1_fun in
699          let precise  = need_arg || has_seq in
700          let t2 = type_check env e2 constr' precise in
701          let res = Types.cup
702                      (if has_fun then
703                         if need_arg then Types.Arrow.apply t1_fun t2
704                         else Types.Arrow.apply_noarg t1_fun
705                       else Types.empty)
706                      (if has_seq then Sequence.concat t1 t2
707                       else Types.empty)
708          in
709          check loc res constr "";
710          res
711    *)
712          let t1 = type_check env e1 Types.Arrow.any true in
713          let t1 = Types.Arrow.get t1 in
714          let dom = Types.Arrow.domain t1 in
715          let res =
716            if Types.Arrow.need_arg t1 then
717              let t2 = type_check env e2 dom true in
718              Types.Arrow.apply t1 t2
719            else
720              (ignore (type_check env e2 dom false); Types.Arrow.apply_noarg t1)
721          in
722          check loc res constr "";
723          res
724      | Op ("flatten", [e]) ->
725          let constr' = Sequence.star
726                          (Sequence.approx (Types.cap Sequence.any constr)) in
727          let sconstr' = Sequence.star constr' in
728          let exact = Types.subtype constr' constr in
729          if exact then
730            let t = type_check env e sconstr' precise in
731            if precise then Sequence.flatten t else constr
732          else
733            let t = type_check env e sconstr' true in
734            let res = Sequence.flatten t in
735            check loc res constr "";
736            if precise then res else constr
737      | _ ->
738          let t : Types.descr = compute_type' loc env e in
739          check loc t constr "";
740          t
741    
742    and type_check_pair ?(kind=`Normal) loc env e1 e2 constr precise =
743      let rects = Types.Product.get ~kind constr in
744      if Types.Product.is_empty rects then
745        (match kind with
746          | `Normal -> raise_loc loc (ShouldHave (constr,"but it is a pair."))
747          | `XML -> raise_loc loc (ShouldHave (constr,"but it is an XML element.")));
748      let pi1 = Types.Product.pi1 rects in
749    
750      let t1 = type_check env e1 (Types.Product.pi1 rects)
751                 (precise || (Types.Product.need_second rects))in
752      let rects = Types.Product.restrict_1 rects t1 in
753      let t2 = type_check env e2 (Types.Product.pi2 rects) precise in
754      if precise then
755        match kind with
756          | `Normal -> Types.times (Types.cons t1) (Types.cons t2)
757          | `XML -> Types.xml (Types.cons t1) (Types.cons t2)
758      else
759        constr
760    
761    
762    and compute_type env e =
763      type_check env e Types.any true
764    
765    and compute_type' loc env = function
766      | Var s ->
767          (try Env.find s env
768           with Not_found -> raise_loc loc (UnboundId s)
769          )
770      | Cst c -> Types.constant c
771      | Dot (e,l) ->
772          let t = type_check env e Types.Record.any true in
773             (try (Types.Record.project t l)
774              with Not_found -> raise_loc loc (WrongLabel(t,l)))
775    | Op (op, el) ->    | Op (op, el) ->
776        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
777        type_op loc op args        type_op loc op args
778    | Match (e,b) ->    | Map (e,b) ->
779        let t = compute_type env e in        let t = compute_type env e in
780        type_branches loc env t b        Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t
781    | Map (e,b) -> assert false  
782    (* We keep these cases here to allow comparison and benchmarking ...
783       Just comment the corresponding cases in type_check' to
784       activate these ones.
785    *)
786      | Pair (e1,e2) ->
787          let t1 = compute_type env e1
788          and t2 = compute_type env e2 in
789          Types.times (Types.cons t1) (Types.cons t2)
790      | RecordLitt r ->
791          let r =
792            List.map
793              (fun (l,e) -> (l,(false,Types.cons (compute_type env e))))
794              r in
795          Types.record' (false,r)
796      | _ -> assert false
797    
798  and type_branches loc env targ brs =  and type_check_branches loc env targ brs constr precise =
799    if Types.is_empty targ then Types.empty    if Types.is_empty targ then Types.empty
800    else (    else (
801      brs.br_typ <- Types.cup brs.br_typ targ;      brs.br_typ <- Types.cup brs.br_typ targ;
802      branches_aux loc env targ Types.empty brs.br_branches      branches_aux loc env targ
803          (if precise then Types.empty else constr)
804          constr precise brs.br_branches
805    )    )
806    
807  and branches_aux loc env targ tres = function  and branches_aux loc env targ tres constr precise = function
808    | [] -> raise_loc loc (NonExhaustive targ)    | [] -> raise_loc loc (NonExhaustive targ)
809    | b :: rem ->    | b :: rem ->
810        let p = b.br_pat in        let p = b.br_pat in
# Line 441  Line 812 
812    
813        let targ' = Types.cap targ acc in        let targ' = Types.cap targ acc in
814        if Types.is_empty targ'        if Types.is_empty targ'
815        then branches_aux loc env targ tres rem        then branches_aux loc env targ tres constr precise rem
816        else        else
817          ( b.br_used <- true;          ( b.br_used <- true;
818            let res = Patterns.filter targ' p in            let res = Patterns.filter targ' p in
819            let env' = List.fold_left            let env' = List.fold_left
820                         (fun env (x,t) -> Env.add x (Types.descr t) env)                         (fun env (x,t) -> Env.add x (Types.descr t) env)
821                         env res in                         env res in
822            let t = compute_type env' b.br_body in            let t = type_check env' b.br_body constr precise in
823            let tres = Types.cup t tres in            let tres = if precise then Types.cup t tres else tres in
824            let targ'' = Types.diff targ acc in            let targ'' = Types.diff targ acc in
825            if (Types.non_empty targ'') then            if (Types.non_empty targ'') then
826              branches_aux loc env targ'' (Types.cup t tres) rem              branches_aux loc env targ'' tres constr precise rem
827            else            else
828              tres              tres
829          )          )
830    
831    and type_let_decl env l =
832      let acc = Types.descr (Patterns.accept l.let_pat) in
833      let t = type_check env l.let_body acc true in
834      let res = Patterns.filter t l.let_pat in
835      List.map (fun (x,t) -> (x, Types.descr t)) res
836    
837    and type_rec_funs env l =
838      let types =
839        List.fold_left
840          (fun accu -> function  {let_body={exp_descr=Abstraction a}} as l ->
841             let t = a.fun_typ in
842             let acc = Types.descr (Patterns.accept l.let_pat) in
843             if not (Types.subtype t acc) then
844               raise_loc l.let_body.exp_loc (NonExhaustive (Types.diff t acc));
845             let res = Patterns.filter t l.let_pat in
846             List.fold_left (fun accu (x,t) -> (x, Types.descr t)::accu) accu res
847             | _ -> assert false) [] l
848      in
849      let env' = List.fold_left (fun env (x,t) -> Env.add x t env) env types in
850      List.iter
851        (function  { let_body = { exp_descr = Abstraction a } } as l ->
852           ignore (type_check env' l.let_body Types.any false)
853           | _ -> assert false) l;
854      types
855    
856    
857  and type_op loc op args =  and type_op loc op args =
858    match (op,args) with    match (op,args) with
859      | ("+", [loc1,t1; loc2,t2]) ->      | "+", [loc1,t1; loc2,t2] ->
860          type_int_binop Intervals.add loc1 t1 loc2 t2          type_int_binop Intervals.add loc1 t1 loc2 t2
861      | ("*", [loc1,t1; loc2,t2]) ->      | "-", [loc1,t1; loc2,t2] ->
862            type_int_binop Intervals.sub loc1 t1 loc2 t2
863        | ("*" | "/"), [loc1,t1; loc2,t2] ->
864          type_int_binop (fun i1 i2 -> Intervals.any) loc1 t1 loc2 t2          type_int_binop (fun i1 i2 -> Intervals.any) loc1 t1 loc2 t2
865        | "@", [loc1,t1; loc2,t2] ->
866            check loc1 t1 Sequence.any
867              "The first argument of @ must be a sequence";
868            Sequence.concat t1 t2
869        | "flatten", [loc1,t1] ->
870            check loc1 t1 Sequence.seqseq
871              "The argument of flatten must be a sequence of sequences";
872            Sequence.flatten t1
873        | "load_xml", [loc1,t1] ->
874            check loc1 t1 Sequence.string
875              "The argument of load_xml must be a string (filename)";
876            Types.any
877        | "raise", [loc1,t1] ->
878            Types.empty
879        | "print_xml", [loc1,t1] ->
880            Sequence.string
881        | "print", [loc1,t1] ->
882            check loc1 t1 Sequence.string
883              "The argument of print must be a string";
884            Sequence.nil_type
885        | "dump_to_file", [loc1,t1; loc2,t2] ->
886            check loc1 t1 Sequence.string
887              "The argument of dump_to_file must be a string (filename)";
888            check loc2 t2 Sequence.string
889              "The argument of dump_to_file must be a string (value to dump)";
890            Sequence.nil_type
891        | "int_of", [loc1,t1] ->
892            check loc1 t1 Sequence.string
893              "The argument of int_of must be a string";
894            if not (Types.subtype t1 Builtin.intstr) then
895              warning loc "This application of int_of may fail";
896            Types.interval Intervals.any
897        | "string_of", [loc1,t1] ->
898            Sequence.string
899      | _ -> assert false      | _ -> assert false
900    
901  and type_int_binop f loc1 t1 loc2 t2 =  and type_int_binop f loc1 t1 loc2 t2 =
# Line 474  Line 907 
907    if not (Types.Int.is_int t2) then    if not (Types.Int.is_int t2) then
908      raise_loc loc2      raise_loc loc2
909        (Constraint        (Constraint
910                 (t1,Types.Int.any,                 (t2,Types.Int.any,
911                  "The second argument must be an integer"));                  "The second argument must be an integer"));
912    Types.Int.put    Types.Int.put
913      (f (Types.Int.get t1) (Types.Int.get t2));      (f (Types.Int.get t1) (Types.Int.get t2));
Legend:
Removed from v.16  
changed lines
  Added in v.172
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5