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

Diff of /typing/typer.ml

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

revision 9 by abate, Tue Jul 10 16:57:19 2007 UTC revision 47 by abate, Tue Jul 10 17:00:52 2007 UTC
# Line 6  Line 6 
6    
7  exception Pattern of string  exception Pattern of string
8  exception NonExhaustive of Types.descr  exception NonExhaustive of Types.descr
9    exception MultipleLabel of Types.label
10  exception Constraint of Types.descr * Types.descr * string  exception Constraint of Types.descr * Types.descr * string
11    exception ShouldHave of Types.descr * string
12    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 42  Line 46 
46    
47  let mk' =  let mk' =
48    let counter = ref 0 in    let counter = ref 0 in
49    fun () ->    fun loc ->
50      incr counter;      incr counter;
51      let rec x = {      let rec x = {
52        id = !counter;        id = !counter;
53        loc' = noloc;        loc' = loc;
54        fv = None;        fv = None;
55        descr' = `Alias ("__dummy__", x);        descr' = `Alias ("__dummy__", x);
56        type_node = None;        type_node = None;
# Line 55  Line 59 
59      x      x
60    
61  let cons loc d =  let cons loc d =
62    let x = mk' () in    let x = mk' loc in
   x.loc' <- loc;  
63    x.descr' <- d;    x.descr' <- d;
64    x    x
65    
# Line 158  Line 161 
161         with Not_found ->         with Not_found ->
162           raise_loc loc (Pattern ("Undefined type variable " ^ s))           raise_loc loc (Pattern ("Undefined type variable " ^ s))
163        )        )
164    | Recurs (t, b) ->    | Recurs (t, b) -> compile (compile_many env b) t
       let b = List.map (fun (v,t) -> (v,t,mk' ())) b in  
       let env =  
         List.fold_left (fun env (v,t,x) -> StringMap.add v x env) env b in  
       List.iter  
         (fun (v,t,x) -> x.loc' <- t.loc; x.descr' <- `Alias (v, compile env t))  
         b;  
       compile env t  
165    | Regexp (r,q) -> compile env (Regexp.compile r q)    | Regexp (r,q) -> compile env (Regexp.compile r q)
166    | Internal t -> cons loc (`Type t)    | Internal t -> cons loc (`Type t)
167    | Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2))    | Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2))
# Line 177  Line 173 
173    | Constant (x,v) -> cons loc (`Constant (x,v))    | Constant (x,v) -> cons loc (`Constant (x,v))
174    | Capture x -> cons loc (`Capture x)    | Capture x -> cons loc (`Capture x)
175    
176    and compile_many env b =
177      let b = List.map (fun (v,t) -> (v,t,mk' t.loc)) b in
178      let env =
179        List.fold_left (fun env (v,t,x) -> StringMap.add v x env) env b in
180      List.iter (fun (v,t,x) -> x.descr' <- `Alias (v, compile env t)) b;
181      env
182    
183    
184  let rec comp_fv seen s =  let rec comp_fv seen s =
185    match s.fv with    match s.fv with
186      | Some l -> l      | Some l -> l
# Line 266  Line 270 
270          Patterns.define x t;          Patterns.define x t;
271          x          x
272    
273  let typ e =  let global_types = ref StringMap.empty
274    let e = compile StringMap.empty e in  
275    let mk_typ e =
276    if fv e = [] then type_node e    if fv e = [] then type_node e
277    else (raise_loc e.loc'    else raise_loc e.loc' (Pattern "Capture variables are not allowed in types")
278            (Pattern "Capture variables are not allowed in types"))  
279    
280    let typ e =
281      mk_typ (compile !global_types e)
282    
283  let pat e =  let pat e =
284    let e = compile StringMap.empty e in    let e = compile !global_types e in
285    pat_node e    pat_node e
286    
287    let register_global_types b =
288      let env = compile_many !global_types b in
289      List.iter (fun (v,_) ->
290                   let d = Types.descr (mk_typ (StringMap.find v env)) in
291                   let d = Types.normalize d in
292                   Types.Print.register_global v d
293                ) b;
294      global_types := env
295    
296    
297  (* II. Build skeleton *)  (* II. Build skeleton *)
# Line 285  Line 301 
301  let rec expr { loc = loc; descr = d } =  let rec expr { loc = loc; descr = d } =
302    let (fv,td) =    let (fv,td) =
303      match d with      match d with
304          | DebugTyper t -> (Fv.empty, Typed.DebugTyper (typ t))
305        | Var s -> (Fv.singleton s, Typed.Var s)        | Var s -> (Fv.singleton s, Typed.Var s)
306        | Apply (e1,e2) ->        | Apply (e1,e2) ->
307            let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in            let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
# Line 314  Line 331 
331        | Pair (e1,e2) ->        | Pair (e1,e2) ->
332            let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in            let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
333            (Fv.union fv1 fv2, Typed.Pair (e1,e2))            (Fv.union fv1 fv2, Typed.Pair (e1,e2))
334          | Dot (e,l) ->
335              let (fv,e) = expr e in
336              (fv,  Typed.Dot (e,l))
337        | RecordLitt r ->        | RecordLitt r ->
           (* XXX TODO: check that no label appears twice *)  
338            let fv = ref Fv.empty in            let fv = ref Fv.empty in
339              let r  = List.sort (fun (l1,_) (l2,_) -> compare l1 l2) r in
340            let r = List.map            let r = List.map
341                      (fun (l,e) ->                      (fun (l,e) ->
342                         let (fv2,e) = expr e in                         let (fv2,e) = expr e in fv := Fv.union !fv fv2; (l,e))
343                         fv := Fv.union !fv fv2;                      r in
344                         (l,e)            let rec check = function
345                      ) r in              | (l1,_) :: (l2,_) :: _ when l1 = l2 ->
346                    raise_loc loc (MultipleLabel l1)
347                | _ :: rem -> check rem
348                | _ -> () in
349              check r;
350            (!fv, Typed.RecordLitt r)            (!fv, Typed.RecordLitt r)
351        | Op (o,e) ->        | Op (op,le) ->
352            let (fv,e) = expr e in (fv, Typed.Op (o,e))            let (fvs,ltes) = List.split (List.map expr le) in
353              let fv = List.fold_left Fv.union Fv.empty fvs in
354              (fv, Typed.Op (op,ltes))
355        | Match (e,b) ->        | Match (e,b) ->
356            let (fv1,e) = expr e            let (fv1,e) = expr e
357            and (fv2,b) = branches b in            and (fv2,b) = branches b in
# Line 343  Line 369 
369    
370    and branches b =    and branches b =
371      let fv = ref Fv.empty in      let fv = ref Fv.empty in
372        let accept = ref Types.empty in
373      let b = List.map      let b = List.map
374                (fun (p,e) ->                (fun (p,e) ->
375                   let (fv2,e) = expr e in                   let (fv2,e) = expr e in
376                   fv := Fv.union !fv fv2;                   fv := Fv.union !fv fv2;
377                     let p = pat p in
378                     accept := Types.cup !accept (Types.descr (Patterns.accept p));
379                   { Typed.br_used = false;                   { Typed.br_used = false;
380                     Typed.br_pat = pat p;                     Typed.br_pat = p;
381                     Typed.br_body = e }                     Typed.br_body = e }
382                ) b in                ) b in
383      (!fv, { Typed.br_typ = Types.empty; Typed.br_branches = b } )      (!fv,
384         {
385           Typed.br_typ = Types.empty;
386           Typed.br_branches = b;
387           Typed.br_accept = !accept;
388           Typed.br_compiled = None;
389         }
390        )
391    
392  module Env = StringMap  module Env = StringMap
393    
394  open Typed  open Typed
395    
396  let rec compute_type env e =  
397    let d = compute_type' e.exp_loc env e.exp_descr in  let check loc t s msg =
398      if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg))
399    
400    let rec type_check env e constr precise =
401    (*  Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
402        Types.Print.print_descr constr precise;
403    *)
404      let d = type_check' e.exp_loc env e.exp_descr constr precise in
405    e.exp_typ <- Types.cup e.exp_typ d;    e.exp_typ <- Types.cup e.exp_typ d;
406    d    d
407    
408  and compute_type' loc env = function  and type_check' loc env e constr precise = match e with
   | Var s -> Env.find s env  
   | Apply (e1,e2) ->  
       let t1 = compute_type env e1 and t2 = compute_type env e2 in  
       Types.apply t1 t2  
409    | Abstraction a ->    | Abstraction a ->
410          let t =
411            try Types.Arrow.check_strenghten a.fun_typ constr
412            with Not_found ->
413              raise_loc loc
414              (ShouldHave
415                 (constr, "but the interface of the abstraction is not compatible"))
416          in
417        let env = match a.fun_name with        let env = match a.fun_name with
418          | None -> env          | None -> env
419          | Some f -> Env.add f a.fun_typ env in          | Some f -> Env.add f a.fun_typ env in
420        List.iter (fun (t1,t2) ->        List.iter
421                     let t = type_branches loc env t1 a.fun_body in          (fun (t1,t2) ->
422                     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"))  
423                  ) a.fun_iface;                  ) a.fun_iface;
424        a.fun_typ        t
425      | Match (e,b) ->
426          let t = type_check env e b.br_accept true in
427          type_check_branches loc env t b constr precise
428    
429      | Pair (e1,e2) ->
430          let rects = Types.Product.get constr in
431          if Types.Product.is_empty rects then
432            raise_loc loc (ShouldHave (constr,"but it is a pair."));
433          let pi1 = Types.Product.pi1 rects in
434    
435          let t1 = type_check env e1 (Types.Product.pi1 rects)
436                     (precise || (Types.Product.need_second rects))in
437          let rects = Types.Product.restrict_1 rects t1 in
438          let t2 = type_check env e2 (Types.Product.pi2 rects) precise in
439          if precise then
440            Types.times (Types.cons t1) (Types.cons t2)
441          else
442            constr
443    
444      | RecordLitt r ->
445          let rconstr = Types.Record.get constr in
446          if Types.Record.is_empty rconstr then
447            raise_loc loc (ShouldHave (constr,"but it is a record."));
448    
449          let (rconstr,res) =
450            List.fold_left
451              (fun (rconstr,res) (l,e) ->
452                 let rconstr = Types.Record.restrict_label_present rconstr l in
453                 let pi = Types.Record.project_field rconstr l in
454                 if Types.Record.is_empty rconstr then
455                   raise_loc loc
456                     (ShouldHave (constr,(Printf.sprintf
457                                            "Field %s is not allowed here."
458                                            (Types.label_name l)
459                                         )
460                                 ));
461                 let t = type_check env e pi true in
462                 let rconstr = Types.Record.restrict_field rconstr l t in
463    
464                 let res =
465                   if precise
466                   then Types.cap res (Types.record l false (Types.cons t))
467                   else res in
468                 (rconstr,res)
469              ) (rconstr, if precise then Types.Record.any else constr) r
470          in
471          res
472    
473      | Map (e,b) ->
474          let t = type_check env e (Sequence.star b.br_accept) true in
475    
476          let constr' = Sequence.approx (Types.cap Sequence.any constr) in
477          let exact = Types.subtype (Sequence.star constr') constr in
478    
479          if exact then (
480            (* Note: typing mail fail because of the approx on t *)
481            let res = type_check_branches loc env (Sequence.approx t)
482                        b constr' precise in
483            if precise then Sequence.star res else constr
484          )
485          else
486            (* Note:
487               - could be more precise by integrating the decomposition
488               of constr inside Sequence.map.
489            *)
490            let res =
491              Sequence.map
492                (fun t -> type_check_branches loc env t b constr' true)
493                t in
494            if not exact then check loc res constr "";
495            if precise then res else constr
496      | Op ("@", [e1;e2]) ->
497          let constr' = Sequence.star
498                          (Sequence.approx (Types.cap Sequence.any constr)) in
499          let exact = Types.subtype constr' constr in
500          if exact then
501            let t1 = type_check env e1 constr' precise
502            and t2 = type_check env e2 constr' precise in
503            if precise then Sequence.concat t1 t2 else constr
504          else
505            (* Note:
506               the knownledge of t1 may makes it useless to
507               check t2 with 'precise' ... *)
508            let t1 = type_check env e1 constr' true
509            and t2 = type_check env e2 constr' true in
510            let res = Sequence.concat t1 t2 in
511            check loc res constr "";
512            if precise then res else constr
513      | Op ("flatten", [e]) ->
514          let constr' = Sequence.star
515                          (Sequence.approx (Types.cap Sequence.any constr)) in
516          let sconstr' = Sequence.star constr' in
517          let exact = Types.subtype constr' constr in
518          if exact then
519            let t = type_check env e sconstr' precise in
520            if precise then Sequence.flatten t else constr
521          else
522            let t = type_check env e sconstr' true in
523            let res = Sequence.flatten t in
524            check loc res constr "";
525            if precise then res else constr
526      | _ ->
527          let t : Types.descr = compute_type' loc env e in
528          check loc t constr "";
529          t
530    
531    and compute_type env e =
532      type_check env e Types.any true
533    
534    and compute_type' loc env = function
535      | DebugTyper t -> Types.descr t
536      | Var s ->
537          (try Env.find s env
538           with Not_found -> raise_loc loc (UnboundId s)
539          )
540      | Apply (e1,e2) ->
541          let t1 = type_check env e1 Types.Arrow.any true in
542          let t1 = Types.Arrow.get t1 in
543          let dom = Types.Arrow.domain t1 in
544          if Types.Arrow.need_arg t1 then
545            let t2 = type_check env e2 dom true in
546            Types.Arrow.apply t1 t2
547          else
548            (ignore (type_check env e2 dom false); Types.Arrow.apply_noarg t1)
549    | Cst c -> Types.constant c    | Cst c -> Types.constant c
550      | Dot (e,l) ->
551          let t = type_check env e Types.Record.any true in
552             (try (Types.Record.project t l)
553              with Not_found -> raise_loc loc (WrongLabel(t,l)))
554      | Op (op, el) ->
555          let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in
556          type_op loc op args
557      | Map (e,b) ->
558          let t = compute_type env e in
559          Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t
560    
561    (* We keep these cases here to allow comparison and benchmarking ...
562       Just comment the corresponding cases in type_check' to
563       activate these ones.
564    *)
565    | Pair (e1,e2) ->    | Pair (e1,e2) ->
566        let t1 = compute_type env e1 and t2 = compute_type env e2 in        let t1 = compute_type env e1
567        let t1 = Types.cons t1 and t2 = Types.cons t2 in        and t2 = compute_type env e2 in
568        Types.times t1 t2        Types.times (Types.cons t1) (Types.cons t2)
569    | RecordLitt r ->    | RecordLitt r ->
570        List.fold_left        List.fold_left
571          (fun accu (l,e) ->          (fun accu (l,e) ->
# Line 389  Line 573 
573             let t = Types.record l false (Types.cons t) in             let t = Types.record l false (Types.cons t) in
574             Types.cap accu t             Types.cap accu t
575          ) Types.Record.any r          ) Types.Record.any r
   | Op (op,e) -> assert false  
   | Match (e,b) ->  
       let t = compute_type env e in  
       type_branches loc env t b  
   | Map (e,b) -> assert false  
576    
577  and type_branches loc env targ brs =  
578      | _ -> assert false
579    
580    and type_check_branches loc env targ brs constr precise =
581    if Types.is_empty targ then Types.empty    if Types.is_empty targ then Types.empty
582    else (    else (
583      brs.br_typ <- Types.cup brs.br_typ targ;      brs.br_typ <- Types.cup brs.br_typ targ;
584      branches_aux loc env targ Types.empty brs.br_branches      branches_aux loc env targ
585          (if precise then Types.empty else constr)
586          constr precise brs.br_branches
587    )    )
588    
589  and branches_aux loc env targ tres = function  and branches_aux loc env targ tres constr precise = function
590    | [] -> raise_loc loc (NonExhaustive targ)    | [] -> raise_loc loc (NonExhaustive targ)
591    | b :: rem ->    | b :: rem ->
592        let p = b.br_pat in        let p = b.br_pat in
# Line 410  Line 594 
594    
595        let targ' = Types.cap targ acc in        let targ' = Types.cap targ acc in
596        if Types.is_empty targ'        if Types.is_empty targ'
597        then branches_aux loc env targ tres rem        then branches_aux loc env targ tres constr precise rem
598        else        else
599          ( b.br_used <- true;          ( b.br_used <- true;
600            let res = Patterns.filter targ' p in            let res = Patterns.filter targ' p in
601            let env' = List.fold_left            let env' = List.fold_left
602                         (fun env (x,t) -> Env.add x (Types.descr t) env)                         (fun env (x,t) -> Env.add x (Types.descr t) env)
603                         env res in                         env res in
604            let t = compute_type env' b.br_body in            let t = type_check env' b.br_body constr precise in
605            let tres = Types.cup t tres in            let tres = if precise then Types.cup t tres else tres in
606            let targ'' = Types.diff targ acc in            let targ'' = Types.diff targ acc in
607            if (Types.non_empty targ'') then            if (Types.non_empty targ'') then
608              branches_aux loc env targ'' (Types.cup t tres) rem              branches_aux loc env targ'' tres constr precise rem
609            else            else
610              tres              tres
611          )          )
612    
613    and type_op loc op args =
614      match (op,args) with
615        | ("+", [loc1,t1; loc2,t2]) ->
616            type_int_binop Intervals.add loc1 t1 loc2 t2
617        | ("*", [loc1,t1; loc2,t2]) ->
618            type_int_binop (fun i1 i2 -> Intervals.any) loc1 t1 loc2 t2
619        | ("@", [loc1,t1; loc2,t2]) ->
620            check loc1 t1 Sequence.any
621              "The first argument of @ must be a sequence";
622            Sequence.concat t1 t2
623        | ("flatten", [loc1,t1]) ->
624            check loc1 t1 Sequence.seqseq
625              "The argument of flatten must be a sequence of sequences";
626            Sequence.flatten t1
627        | _ -> assert false
628    
629    and type_int_binop f loc1 t1 loc2 t2 =
630      if not (Types.Int.is_int t1) then
631        raise_loc loc1
632          (Constraint
633             (t1,Types.Int.any,
634              "The first argument must be an integer"));
635      if not (Types.Int.is_int t2) then
636        raise_loc loc2
637          (Constraint
638                   (t2,Types.Int.any,
639                    "The second argument must be an integer"));
640      Types.Int.put
641        (f (Types.Int.get t1) (Types.Int.get t2));
642    
643    
Legend:
Removed from v.9  
changed lines
  Added in v.47
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5