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

Diff of /typing/typer.ml

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

revision 28 by abate, Tue Jul 10 16:59:15 2007 UTC revision 72 by abate, Tue Jul 10 17:03:39 2007 UTC
# Line 10  Line 10 
10  exception Constraint of Types.descr * Types.descr * string  exception Constraint of Types.descr * Types.descr * string
11  exception ShouldHave of Types.descr * string  exception ShouldHave of Types.descr * string
12  exception WrongLabel of Types.descr * Types.label  exception WrongLabel of Types.descr * Types.label
13    exception UnboundId of string
14    
15  let raise_loc loc exn = raise (Location (loc,exn))  let raise_loc loc exn = raise (Location (loc,exn))
16    
# Line 28  Line 29 
29     [ `Alias of string * ti     [ `Alias of string * ti
30     | `Type of Types.descr     | `Type of Types.descr
31     | `Or of ti * ti     | `Or of ti * ti
32     | `And of ti * ti     | `And of ti * ti * bool
33     | `Diff of ti * ti     | `Diff of ti * ti
34     | `Times of ti * ti     | `Times of ti * ti
35     | `Arrow of ti * ti     | `Arrow of ti * ti
# Line 72  Line 73 
73  *)  *)
74    
75  module Regexp = struct  module Regexp = struct
   let memo = Hashtbl.create 51  
76    let defs = ref []    let defs = ref []
77    let name =    let name =
78      let c = ref 0 in      let c = ref 0 in
# Line 86  Line 86 
86      | Star r | WeakStar r -> seq_vars accu r      | Star r | WeakStar r -> seq_vars accu r
87      | SeqCapture (v,r) -> seq_vars (StringSet.add v accu) r      | SeqCapture (v,r) -> seq_vars (StringSet.add v accu) r
88    
89    let rec propagate vars = function    let uniq_id = let r = ref 0 in fun () -> incr r; !r
90    
91      type flat = [ `Epsilon
92                  | `Elem of int * Ast.ppat  (* the int arg is used to
93                                                to stop generic comparison *)
94                  | `Seq of flat * flat
95                  | `Alt of flat * flat
96                  | `Star of flat
97                  | `WeakStar of flat ]
98    
99      let rec propagate vars : regexp -> flat = function
100      | Epsilon -> `Epsilon      | Epsilon -> `Epsilon
101      | Elem x -> `Elem (vars,x)      | Elem x -> let p = vars x in `Elem (uniq_id (),p)
102      | Seq (r1,r2) -> `Seq (propagate vars r1,propagate vars r2)      | Seq (r1,r2) -> `Seq (propagate vars r1,propagate vars r2)
103      | Alt (r1,r2) -> `Alt (propagate vars r1, propagate vars r2)      | Alt (r1,r2) -> `Alt (propagate vars r1, propagate vars r2)
104      | Star r -> `Star (propagate vars r)      | Star r -> `Star (propagate vars r)
105      | WeakStar r -> `WeakStar (propagate vars r)      | WeakStar r -> `WeakStar (propagate vars r)
106      | SeqCapture (v,x) -> propagate (StringSet.add v vars) x      | SeqCapture (v,x) ->
107            let v= mk noloc (Capture v) in
108            propagate (fun p -> mk noloc (And (vars p,v,true))) x
109    
110    let cup r1 r2 =    let cup r1 r2 =
111      match (r1,r2) with      match (r1,r2) with
# Line 101  Line 113 
113        | (`Empty, _) -> r2        | (`Empty, _) -> r2
114        | (`Res t1, `Res t2) -> `Res (mk noloc (Or (t1,t2)))        | (`Res t1, `Res t2) -> `Res (mk noloc (Or (t1,t2)))
115    
116    (*TODO: review this compilation schema to avoid explosion when
117      coding (Optional x) by  (Or(Epsilon,x)); memoization ... *)
118    
119      module Memo = Map.Make(struct type t = flat list let compare = compare end)
120      module Coind = Set.Make(struct type t = flat list let compare = compare end)
121      let memo = ref Memo.empty
122    
123    let rec compile fin e seq : [`Res of Ast.ppat | `Empty] =    let rec compile fin e seq : [`Res of Ast.ppat | `Empty] =
124      if List.mem seq e then `Empty      if Coind.mem seq !e then `Empty
125      else      else (
126        let e = seq :: e in        e := Coind.add seq !e;
127        match seq with        match seq with
128          | [] ->          | [] ->
129              `Res fin              `Res fin
130          | `Epsilon :: rest ->          | `Epsilon :: rest ->
131              compile fin e rest              compile fin e rest
132          | `Elem (vars,x) :: rest ->          | `Elem (_,p) :: rest ->
133              let capt = StringSet.fold              `Res (mk noloc (Prod (p, guard_compile fin rest)))
                          (fun v t -> mk noloc (And (t, (mk noloc (Capture v)))))  
                          vars x in  
             `Res (mk noloc (Prod (capt, guard_compile fin rest)))  
134          | `Seq (r1,r2) :: rest ->          | `Seq (r1,r2) :: rest ->
135              compile fin e (r1 :: r2 :: rest)              compile fin e (r1 :: r2 :: rest)
136          | `Alt (r1,r2) :: rest ->          | `Alt (r1,r2) :: rest ->
137              cup (compile fin e (r1::rest)) (compile fin e (r2::rest))              cup (compile fin e (r1::rest)) (compile fin e (r2::rest))
138          | `Star r :: rest -> cup (compile fin e (r::seq)) (compile fin e rest)          | `Star r :: rest ->
139          | `WeakStar r :: rest -> cup (compile fin e rest) (compile fin e (r::seq))              cup (compile fin e (r::seq)) (compile fin e rest)
140            | `WeakStar r :: rest ->
141                cup (compile fin e rest) (compile fin e (r::seq))
142        )
143    and guard_compile fin seq =    and guard_compile fin seq =
144      try Hashtbl.find memo seq      try Memo.find seq !memo
145      with      with
146          Not_found ->          Not_found ->
147            let n = name () in            let n = name () in
148            let v = mk noloc (PatVar n) in            let v = mk noloc (PatVar n) in
149            Hashtbl.add memo seq v;            memo := Memo.add seq v !memo;
150            let d = compile fin [] seq in            let d = compile fin (ref Coind.empty) seq in
151            (match d with            (match d with
152               | `Empty -> assert false               | `Empty -> assert false
153               | `Res d -> defs := (n,d) :: !defs);               | `Res d -> defs := (n,d) :: !defs);
# Line 138  Line 156 
156    
157    let atom_nil = Types.mk_atom "nil"    let atom_nil = Types.mk_atom "nil"
158    let constant_nil v t =    let constant_nil v t =
159      mk noloc (And (t, (mk noloc (Constant (v, Types.Atom atom_nil)))))      mk noloc (And (t, (mk noloc (Constant (v, Types.Atom atom_nil))), true))
160    
161    let compile regexp queue : ppat =    let compile regexp queue : ppat =
162      let vars = seq_vars StringSet.empty regexp in      let vars = seq_vars StringSet.empty regexp in
163      let fin = StringSet.fold constant_nil vars queue in      let fin = StringSet.fold constant_nil vars queue in
164      let n = guard_compile fin [propagate StringSet.empty regexp] in      let n = guard_compile fin [propagate (fun p -> p) regexp] in
165      Hashtbl.clear memo;      memo := Memo.empty;
166      let d = !defs in      let d = !defs in
167      defs := [];      defs := [];
168      mk noloc (Recurs (n,d))      mk noloc (Recurs (n,d))
# Line 164  Line 182 
182    | Regexp (r,q) -> compile env (Regexp.compile r q)    | Regexp (r,q) -> compile env (Regexp.compile r q)
183    | Internal t -> cons loc (`Type t)    | Internal t -> cons loc (`Type t)
184    | Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2))    | Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2))
185    | And (t1,t2) -> cons loc (`And (compile env t1, compile env t2))    | And (t1,t2,e) -> cons loc (`And (compile env t1, compile env t2,e))
186    | Diff (t1,t2) -> cons loc (`Diff (compile env t1, compile env t2))    | Diff (t1,t2) -> cons loc (`Diff (compile env t1, compile env t2))
187    | Prod (t1,t2) -> cons loc (`Times (compile env t1, compile env t2))    | Prod (t1,t2) -> cons loc (`Times (compile env t1, compile env t2))
188    | Arrow (t1,t2) -> cons loc (`Arrow (compile env t1, compile env t2))    | Arrow (t1,t2) -> cons loc (`Arrow (compile env t1, compile env t2))
# Line 180  Line 198 
198    env    env
199    
200    
201  let rec comp_fv seen s =  let comp_fv_seen = ref []
202    match s.fv with  let comp_fv_res = ref []
203      | Some l -> l  let rec comp_fv s =
204      | None ->    if List.memq s !comp_fv_seen then ()
205          let l =    else (
206            match s.descr' with      comp_fv_seen := s :: !comp_fv_seen;
207              | `Alias (_,x) -> if List.memq s seen then [] else comp_fv (s :: seen) x      (match s.descr' with
208          | `Alias (_,x) -> comp_fv x
209              | `Or (s1,s2)              | `Or (s1,s2)
210              | `And (s1,s2)        | `And (s1,s2,_)
211              | `Diff (s1,s2)              | `Diff (s1,s2)
212              | `Times (s1,s2)              | `Times (s1,s2)
213              | `Arrow (s1,s2) -> SortedList.cup (comp_fv seen s1) (comp_fv seen s2)        | `Arrow (s1,s2) -> comp_fv s1; comp_fv s2
214              | `Record (l,opt,s) -> comp_fv seen s        | `Record (l,opt,s) -> comp_fv s
215              | `Type _ -> []        | `Type _ -> ()
216              | `Capture x              | `Capture x
217              | `Constant (x,_) -> [x]        | `Constant (x,_) -> comp_fv_res := x :: !comp_fv_res);
218          in      if (!comp_fv_res = []) then s.fv <- Some [];
219          if seen = [] then s.fv <- Some l;      (* TODO: check that the above line is correct *)
220          l    )
221    
222    
223    
224  let fv = comp_fv []  let fv s =
225      match s.fv with
226        | Some l -> l
227        | None ->
228            comp_fv s;
229            let l = SortedList.from_list !comp_fv_res in
230            comp_fv_res := [];
231            comp_fv_seen := [];
232            s.fv <- Some l;
233            l
234    
235  let rec typ seen s : Types.descr =  let rec typ seen s : Types.descr =
236    match s.descr' with    match s.descr' with
# Line 213  Line 242 
242          else typ (s :: seen) x          else typ (s :: seen) x
243      | `Type t -> t      | `Type t -> t
244      | `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)      | `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)
245      | `And (s1,s2) ->  Types.cap (typ seen s1) (typ seen s2)      | `And (s1,s2,_) ->  Types.cap (typ seen s1) (typ seen s2)
246      | `Diff (s1,s2) -> Types.diff (typ seen s1) (typ seen s2)      | `Diff (s1,s2) -> Types.diff (typ seen s1) (typ seen s2)
247      | `Times (s1,s2) -> Types.times (typ_node s1) (typ_node s2)      | `Times (s1,s2) -> Types.times (typ_node s1) (typ_node s2)
248      | `Arrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)      | `Arrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)
# Line 230  Line 259 
259          Types.define x t;          Types.define x t;
260          x          x
261    
262  let type_node s = Types.internalize (typ_node s)  let type_node s =
263      let s = typ_node s in
264      let s = Types.internalize s in
265    (*  Types.define s (Types.normalize (Types.descr s)); *)
266      s
267    
268  let rec pat seen s : Patterns.descr =  let rec pat seen s : Patterns.descr =
269    if fv s = [] then Patterns.constr (type_node s) else    if fv s = [] then Patterns.constr (type_node s) else
# Line 242  Line 275 
275                 ("Unguarded recursion on variable " ^ v ^ " in this pattern"))                 ("Unguarded recursion on variable " ^ v ^ " in this pattern"))
276          else pat (s :: seen) x          else pat (s :: seen) x
277      | `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)      | `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)
278      | `And (s1,s2) -> Patterns.cap (pat seen s1) (pat seen s2)      | `And (s1,s2,e) -> Patterns.cap (pat seen s1) (pat seen s2) e
279      | `Diff (s1,s2) when fv s2 = [] ->      | `Diff (s1,s2) when fv s2 = [] ->
280          let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in          let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in
281          Patterns.cap (pat seen s1) (Patterns.constr s2)          Patterns.cap (pat seen s1) (Patterns.constr s2) true
282      | `Diff _ ->      | `Diff _ ->
283          raise_loc s.loc' (Pattern "Difference not allowed in patterns")          raise_loc s.loc' (Pattern "Difference not allowed in patterns")
284      | `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)      | `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
# Line 287  Line 320 
320    let env = compile_many !global_types b in    let env = compile_many !global_types b in
321    List.iter (fun (v,_) ->    List.iter (fun (v,_) ->
322                 let d = Types.descr (mk_typ (StringMap.find v env)) in                 let d = Types.descr (mk_typ (StringMap.find v env)) in
323                 Types.Print.register_global v d  (*             let d = Types.normalize d in*)
324                   Types.Print.register_global v d;
325                   ()
326              ) b;              ) b;
327    global_types := env    global_types := env
328    
# Line 300  Line 335 
335    let (fv,td) =    let (fv,td) =
336      match d with      match d with
337        | DebugTyper t -> (Fv.empty, Typed.DebugTyper (typ t))        | DebugTyper t -> (Fv.empty, Typed.DebugTyper (typ t))
338          | Forget (e,t) ->
339              let (fv,e) = expr e and t = typ t in
340              (fv, Typed.Forget (e,t))
341        | Var s -> (Fv.singleton s, Typed.Var s)        | Var s -> (Fv.singleton s, Typed.Var s)
342        | Apply (e1,e2) ->        | Apply (e1,e2) ->
343            let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in            let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
# Line 322  Line 360 
360                 Typed.fun_iface = iface;                 Typed.fun_iface = iface;
361                 Typed.fun_body = body;                 Typed.fun_body = body;
362                 Typed.fun_typ = t;                 Typed.fun_typ = t;
363                 Typed.fun_fv = Fv.elements fv0                 Typed.fun_fv = Fv.elements fv
364               }               }
365            )            )
366        | Cst c -> (Fv.empty, Typed.Cst c)        | Cst c -> (Fv.empty, Typed.Cst c)
# Line 333  Line 371 
371            let (fv,e) = expr e in            let (fv,e) = expr e in
372            (fv,  Typed.Dot (e,l))            (fv,  Typed.Dot (e,l))
373        | RecordLitt r ->        | RecordLitt r ->
           (* XXX TODO: check that no label appears twice *)  
374            let fv = ref Fv.empty in            let fv = ref Fv.empty in
375            let labs = ref [] in            let r  = List.sort (fun (l1,_) (l2,_) -> compare l1 l2) r in
376            let r = List.map            let r = List.map
377                      (fun (l,e) ->                      (fun (l,e) ->
378                         let (fv2,e) = expr e in                         let (fv2,e) = expr e in fv := Fv.union !fv fv2; (l,e))
379                         if (List.mem l !labs) then                      r in
380                           raise_loc loc (MultipleLabel l);            let rec check = function
381                         labs := l :: !labs;              | (l1,_) :: (l2,_) :: _ when l1 = l2 ->
382                         fv := Fv.union !fv fv2;                  raise_loc loc (MultipleLabel l1)
383                         (l,e)              | _ :: rem -> check rem
384                      ) r in              | _ -> () in
385              check r;
386            (!fv, Typed.RecordLitt r)            (!fv, Typed.RecordLitt r)
387        | Op (op,le) ->        | Op (op,le) ->
388            let (fvs,ltes) = List.split (List.map expr le) in            let (fvs,ltes) = List.split (List.map expr le) in
# Line 358  Line 396 
396            let (fv1,e) = expr e            let (fv1,e) = expr e
397            and (fv2,b) = branches b in            and (fv2,b) = branches b in
398            (Fv.union fv1 fv2, Typed.Map (e, b))            (Fv.union fv1 fv2, Typed.Map (e, b))
399          | Try (e,b) ->
400              let (fv1,e) = expr e
401              and (fv2,b) = branches b in
402              (Fv.union fv1 fv2, Typed.Try (e, b))
403    in    in
404    fv,    fv,
405    { Typed.exp_loc = loc;    { Typed.exp_loc = loc;
# Line 371  Line 413 
413      let b = List.map      let b = List.map
414                (fun (p,e) ->                (fun (p,e) ->
415                   let (fv2,e) = expr e in                   let (fv2,e) = expr e in
                  fv := Fv.union !fv fv2;  
416                   let p = pat p in                   let p = pat p in
417                     let fv2 = List.fold_right Fv.remove (Patterns.fv p) fv2 in
418                     fv := Fv.union !fv fv2;
419                   accept := Types.cup !accept (Types.descr (Patterns.accept p));                   accept := Types.cup !accept (Types.descr (Patterns.accept p));
420                   { Typed.br_used = false;                   { Typed.br_used = false;
421                     Typed.br_pat = p;                     Typed.br_pat = p;
# Line 382  Line 425 
425       {       {
426         Typed.br_typ = Types.empty;         Typed.br_typ = Types.empty;
427         Typed.br_branches = b;         Typed.br_branches = b;
428         Typed.br_accept = !accept         Typed.br_accept = !accept;
429           Typed.br_compiled = None;
430       }       }
431      )      )
432    
433    let let_decl p e =
434      let (_,e) = expr e in
435      { Typed.let_pat = pat p;
436        Typed.let_body = e;
437        Typed.let_compiled = None }
438    
439    (* III. Type-checks *)
440    
441  module Env = StringMap  module Env = StringMap
442    type env = Types.descr Env.t
443    
444  open Typed  open Typed
445    
446    let warning loc msg =
447      Format.fprintf Format.std_formatter
448        "Warning %a:@\n%s@\n" Location.print_loc loc msg
449    
450  let check loc t s msg =  let check loc t s msg =
451    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))
452    
453  let rec type_check env e constr precise =  let rec type_check env e constr precise =
454   (* Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"   (* Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
455      Types.Print.print_descr constr precise;  *)      Types.Print.print_descr constr precise;
456    *)
457    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
458    e.exp_typ <- Types.cup e.exp_typ d;    e.exp_typ <- Types.cup e.exp_typ d;
459    d    d
460    
461  and type_check' loc env e constr precise = match e with  and type_check' loc env e constr precise = match e with
462      | Forget (e,t) ->
463          let t = Types.descr t in
464          ignore (type_check env e t false);
465          t
466    | Abstraction a ->    | Abstraction a ->
467        let t =        let t =
468          try Types.Arrow.check_strenghten a.fun_typ constr          try Types.Arrow.check_strenghten a.fun_typ constr
# Line 418  Line 479 
479             ignore (type_check_branches loc env t1 a.fun_body t2 false)             ignore (type_check_branches loc env t1 a.fun_body t2 false)
480          ) a.fun_iface;          ) a.fun_iface;
481        t        t
482    
483    | Match (e,b) ->    | Match (e,b) ->
484        let t = type_check env e b.br_accept true in        let t = type_check env e b.br_accept true in
485        type_check_branches loc env t b constr precise        type_check_branches loc env t b constr precise
486    
487      | Try (e,b) ->
488          let te = type_check env e constr precise in
489          let tb = type_check_branches loc env Types.any b constr precise in
490          Types.cup te tb
491    
492    | Pair (e1,e2) ->    | Pair (e1,e2) ->
493        let rects = Types.Product.get constr in        let rects = Types.Product.get constr in
494        if Types.Product.is_empty rects then        if Types.Product.is_empty rects then
# Line 435  Line 503 
503          Types.times (Types.cons t1) (Types.cons t2)          Types.times (Types.cons t1) (Types.cons t2)
504        else        else
505          constr          constr
506    
507      | RecordLitt r ->
508          let rconstr = Types.Record.get constr in
509          if Types.Record.is_empty rconstr then
510            raise_loc loc (ShouldHave (constr,"but it is a record."));
511    
512          let (rconstr,res) =
513            List.fold_left
514              (fun (rconstr,res) (l,e) ->
515                 let rconstr = Types.Record.restrict_label_present rconstr l in
516                 let pi = Types.Record.project_field rconstr l in
517                 if Types.Record.is_empty rconstr then
518                   raise_loc loc
519                     (ShouldHave (constr,(Printf.sprintf
520                                            "Field %s is not allowed here."
521                                            (Types.label_name l)
522                                         )
523                                 ));
524                 let t = type_check env e pi true in
525                 let rconstr = Types.Record.restrict_field rconstr l t in
526    
527                 let res =
528                   if precise
529                   then Types.cap res (Types.record l false (Types.cons t))
530                   else res in
531                 (rconstr,res)
532              ) (rconstr, if precise then Types.Record.any else constr) r
533          in
534          res
535    
536      | Map (e,b) ->
537          let t = type_check env e (Sequence.star b.br_accept) true in
538    
539          let constr' = Sequence.approx (Types.cap Sequence.any constr) in
540          let exact = Types.subtype (Sequence.star constr') constr in
541          (* Note:
542             - could be more precise by integrating the decomposition
543             of constr inside Sequence.map.
544          *)
545          let res =
546            Sequence.map
547              (fun t ->
548                 type_check_branches loc env t b constr' (precise || (not exact)))
549              t in
550          if not exact then check loc res constr "";
551          if precise then res else constr
552      | Op ("@", [e1;e2]) ->
553          let constr' = Sequence.star
554                          (Sequence.approx (Types.cap Sequence.any constr)) in
555          let exact = Types.subtype constr' constr in
556          if exact then
557            let t1 = type_check env e1 constr' precise
558            and t2 = type_check env e2 constr' precise in
559            if precise then Sequence.concat t1 t2 else constr
560          else
561            (* Note:
562               the knownledge of t1 may makes it useless to
563               check t2 with 'precise' ... *)
564            let t1 = type_check env e1 constr' true
565            and t2 = type_check env e2 constr' true in
566            let res = Sequence.concat t1 t2 in
567            check loc res constr "";
568            if precise then res else constr
569      | Op ("flatten", [e]) ->
570          let constr' = Sequence.star
571                          (Sequence.approx (Types.cap Sequence.any constr)) in
572          let sconstr' = Sequence.star constr' in
573          let exact = Types.subtype constr' constr in
574          if exact then
575            let t = type_check env e sconstr' precise in
576            if precise then Sequence.flatten t else constr
577          else
578            let t = type_check env e sconstr' true in
579            let res = Sequence.flatten t in
580            check loc res constr "";
581            if precise then res else constr
582    | _ ->    | _ ->
583        let t : Types.descr = compute_type' loc env e in        let t : Types.descr = compute_type' loc env e in
584        check loc t constr "";        check loc t constr "";
# Line 445  Line 589 
589    
590  and compute_type' loc env = function  and compute_type' loc env = function
591    | DebugTyper t -> Types.descr t    | DebugTyper t -> Types.descr t
592    | Var s -> Env.find s env    | Var s ->
593          (try Env.find s env
594           with Not_found -> raise_loc loc (UnboundId s)
595          )
596    | Apply (e1,e2) ->    | Apply (e1,e2) ->
597        let t1 = type_check env e1 Types.Arrow.any true in        let t1 = type_check env e1 Types.Arrow.any true in
598        let t1 = Types.Arrow.get t1 in        let t1 = Types.Arrow.get t1 in
# Line 460  Line 607 
607        let t = type_check env e Types.Record.any true in        let t = type_check env e Types.Record.any true in
608           (try (Types.Record.project t l)           (try (Types.Record.project t l)
609            with Not_found -> raise_loc loc (WrongLabel(t,l)))            with Not_found -> raise_loc loc (WrongLabel(t,l)))
610      | Op (op, el) ->
611          let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in
612          type_op loc op args
613      | Map (e,b) ->
614          let t = compute_type env e in
615          Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t
616    
617    (* We keep these cases here to allow comparison and benchmarking ...
618       Just comment the corresponding cases in type_check' to
619       activate these ones.
620    *)
621      | Pair (e1,e2) ->
622          let t1 = compute_type env e1
623          and t2 = compute_type env e2 in
624          Types.times (Types.cons t1) (Types.cons t2)
625    | RecordLitt r ->    | RecordLitt r ->
626        List.fold_left        List.fold_left
627          (fun accu (l,e) ->          (fun accu (l,e) ->
# Line 467  Line 629 
629             let t = Types.record l false (Types.cons t) in             let t = Types.record l false (Types.cons t) in
630             Types.cap accu t             Types.cap accu t
631          ) Types.Record.any r          ) Types.Record.any r
632    | Op (op, el) ->  
633        let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in  
       type_op loc op args  
   | Map (e,b) ->  
       let t = compute_type env e in  
       Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t  
634    | _ -> assert false    | _ -> assert false
635    
636  and type_check_branches loc env targ brs constr precise =  and type_check_branches loc env targ brs constr precise =
# Line 508  Line 666 
666              tres              tres
667          )          )
668    
669    and type_let_decl env l =
670      let acc = Types.descr (Patterns.accept l.let_pat) in
671      let t = type_check env l.let_body acc true in
672      let res = Patterns.filter t l.let_pat in
673      List.map (fun (x,t) -> (x, Types.descr t)) res
674    
675    and type_rec_funs env l =
676      let types =
677        List.fold_left
678          (fun accu -> function  {let_body={exp_descr=Abstraction a}} as l ->
679             let t = a.fun_typ in
680             let acc = Types.descr (Patterns.accept l.let_pat) in
681             if not (Types.subtype t acc) then
682               raise_loc l.let_body.exp_loc (NonExhaustive (Types.diff t acc));
683             let res = Patterns.filter t l.let_pat in
684             List.fold_left (fun accu (x,t) -> (x, Types.descr t)::accu) accu res
685             | _ -> assert false) [] l
686      in
687      let env' = List.fold_left (fun env (x,t) -> Env.add x t env) env types in
688      List.iter
689        (function  { let_body = { exp_descr = Abstraction a } } as l ->
690           ignore (type_check env' l.let_body Types.any false)
691           | _ -> assert false) l;
692      types
693    
694    
695  and type_op loc op args =  and type_op loc op args =
696    match (op,args) with    match (op,args) with
697      | ("+", [loc1,t1; loc2,t2]) ->      | "+", [loc1,t1; loc2,t2] ->
698          type_int_binop Intervals.add loc1 t1 loc2 t2          type_int_binop Intervals.add loc1 t1 loc2 t2
699      | ("*", [loc1,t1; loc2,t2]) ->      | "-", [loc1,t1; loc2,t2] ->
700            type_int_binop Intervals.sub loc1 t1 loc2 t2
701        | ("*" | "/"), [loc1,t1; loc2,t2] ->
702          type_int_binop (fun i1 i2 -> Intervals.any) loc1 t1 loc2 t2          type_int_binop (fun i1 i2 -> Intervals.any) loc1 t1 loc2 t2
703      | ("@", [loc1,t1; loc2,t2]) ->      | "@", [loc1,t1; loc2,t2] ->
704          check loc1 t1 Sequence.any          check loc1 t1 Sequence.any
705            "The first argument of @ must be a sequence";            "The first argument of @ must be a sequence";
706          Sequence.concat t1 t2          Sequence.concat t1 t2
707      | ("flatten", [loc1,t1]) ->      | "flatten", [loc1,t1] ->
708          check loc1 t1 Sequence.seqseq          check loc1 t1 Sequence.seqseq
709            "The argument of flatten must be a sequence of sequences";            "The argument of flatten must be a sequence of sequences";
710          Sequence.flatten t1          Sequence.flatten t1
711        | "load_xml", [loc1,t1] ->
712            check loc1 t1 Sequence.string
713              "The argument of load_xml must be a string (filename)";
714            Types.any
715        | "raise", [loc1,t1] ->
716            Types.empty
717        | "int_of", [loc1,t1] ->
718            check loc1 t1 Sequence.string
719              "The argument of int_of must a string";
720            if not (Types.subtype t1 Builtin.intstr) then
721              warning loc "This application of int_of may fail";
722            Types.interval Intervals.any
723      | _ -> assert false      | _ -> assert false
724    
725  and type_int_binop f loc1 t1 loc2 t2 =  and type_int_binop f loc1 t1 loc2 t2 =
# Line 533  Line 731 
731    if not (Types.Int.is_int t2) then    if not (Types.Int.is_int t2) then
732      raise_loc loc2      raise_loc loc2
733        (Constraint        (Constraint
734                 (t1,Types.Int.any,                 (t2,Types.Int.any,
735                  "The second argument must be an integer"));                  "The second argument must be an integer"));
736    Types.Int.put    Types.Int.put
737      (f (Types.Int.get t1) (Types.Int.get t2));      (f (Types.Int.get t1) (Types.Int.get t2));
Legend:
Removed from v.28  
changed lines
  Added in v.72
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5