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

Diff of /typing/typer.ml

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

revision 420 by abate, Tue Jul 10 17:32:46 2007 UTC revision 421 by abate, Tue Jul 10 17:33:25 2007 UTC
# Line 20  Line 20 
20    
21  module S = struct type t = string let compare = compare end  module S = struct type t = string let compare = compare end
22  module TypeEnv = Map.Make(S)  module TypeEnv = Map.Make(S)
 module Env = Map.Make(Id)  
   
23    
24  exception NonExhaustive of Types.descr  exception NonExhaustive of Types.descr
25  exception Constraint of Types.descr * Types.descr * string  exception Constraint of Types.descr * Types.descr
26  exception ShouldHave of Types.descr * string  exception ShouldHave of Types.descr * string
27  exception ShouldHave2 of Types.descr * string * Types.descr  exception ShouldHave2 of Types.descr * string * Types.descr
28  exception WrongLabel of Types.descr * label  exception WrongLabel of Types.descr * label
29  exception UnboundId of id  exception UnboundId of id
30    exception Error of string
31    
32  let raise_loc loc exn = raise (Location (loc,exn))  let raise_loc loc exn = raise (Location (loc,exn))
33    let error loc msg = raise_loc loc (Error msg)
34    
35    
36  (* Eliminate Recursion, propagate Sequence Capture Variables *)  (* Eliminate Recursion, propagate Sequence Capture Variables *)
# Line 491  Line 491 
491    
492  let all_branches = ref []  let all_branches = ref []
493    
 (* IDEA: introduce a node Loc in the AST to override nolocs  
    in sub-expressions *)  
   
494  let exp loc fv e =  let exp loc fv e =
495    fv,    fv,
496    { Typed.exp_loc = loc;    { Typed.exp_loc = loc;
# Line 558  Line 555 
555    | Op (op,le) ->    | Op (op,le) ->
556        let (fvs,ltes) = List.split (List.map (expr loc) le) in        let (fvs,ltes) = List.split (List.map (expr loc) le) in
557        let fv = List.fold_left Fv.cup Fv.empty fvs in        let fv = List.fold_left Fv.cup Fv.empty fvs in
558        exp loc fv (Typed.Op (op,ltes))        (try
559             (match (ltes,Typed.find_op op) with
560                | [e], `Unary op -> exp loc fv (Typed.UnaryOp (op, e))
561                | [e1;e2], `Binary op -> exp loc fv (Typed.BinaryOp (op, e1,e2))
562                | _ -> assert false)
563           with Not_found -> assert false)
564    
565    | Match (e,b) ->    | Match (e,b) ->
566        let (fv1,e) = expr loc e        let (fv1,e) = expr loc e
567        and (fv2,b) = branches b in        and (fv2,b) = branches b in
568        exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b))        exp loc (Fv.cup fv1 fv2) (Typed.Match (e, b))
569    | Map (def,e,b) ->    | Map (e,b) ->
570        let (fv1,e) = expr loc e        let (fv1,e) = expr loc e
571        and (fv2,b) = branches b in        and (fv2,b) = branches b in
572        exp loc (Fv.cup fv1 fv2) (Typed.Map (def,e, b))        exp loc (Fv.cup fv1 fv2) (Typed.Map (e, b))
573      | Transform (e,b) ->
574          let (fv1,e) = expr loc e
575          and (fv2,b) = branches b in
576          exp loc (Fv.cup fv1 fv2) (Typed.Transform (e, b))
577    | Xtrans (e,b) ->    | Xtrans (e,b) ->
578        let (fv1,e) = expr loc e        let (fv1,e) = expr loc e
579        and (fv2,b) = branches b in        and (fv2,b) = branches b in
# Line 615  Line 622 
622    
623  (* III. Type-checks *)  (* III. Type-checks *)
624    
 let int_cup_record = Types.cup Types.Int.any Types.Record.any  
   
   
625  type env = Types.descr Env.t  type env = Types.descr Env.t
626    
627  open Typed  open Typed
628    
629    let require loc t s =
630      if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
631    
632    let check loc t s =
633      require loc t s; t
634    
635  let check loc t s msg =  let should_have loc constr s =
636    if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg))    raise_loc loc (ShouldHave (constr,s))
637    
638    let flatten loc arg constr precise =
639      let constr' = Sequence.star
640                      (Sequence.approx (Types.cap Sequence.any constr)) in
641      let sconstr' = Sequence.star constr' in
642      let exact = Types.subtype constr' constr in
643      if exact then
644        let t = arg sconstr' precise in
645        if precise then Sequence.flatten t else constr
646      else
647        let t = arg sconstr' true in
648        Sequence.flatten t
649    
650  let rec type_check env e constr precise =  let rec type_check env e constr precise =
 (*  Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"  
     Types.Print.print_descr constr precise;  
 *)  
651    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
652      let d = if precise then d else constr in
653    e.exp_typ <- Types.cup e.exp_typ d;    e.exp_typ <- Types.cup e.exp_typ d;
654    d    d
655    
# Line 638  Line 657 
657    | Forget (e,t) ->    | Forget (e,t) ->
658        let t = Types.descr t in        let t = Types.descr t in
659        ignore (type_check env e t false);        ignore (type_check env e t false);
660        t        check loc t constr
661    
662    | Abstraction a ->    | Abstraction a ->
663        let t =        let t =
664          try Types.Arrow.check_strenghten a.fun_typ constr          try Types.Arrow.check_strenghten a.fun_typ constr
665          with Not_found ->          with Not_found ->
666            raise_loc loc            should_have loc constr
667            (ShouldHave              "but the interface of the abstraction is not compatible"
              (constr, "but the interface of the abstraction is not compatible"))  
668        in        in
669        let env = match a.fun_name with        let env = match a.fun_name with
670          | None -> env          | None -> env
# Line 670  Line 689 
689    
690    | Pair (e1,e2) ->    | Pair (e1,e2) ->
691        type_check_pair loc env e1 e2 constr precise        type_check_pair loc env e1 e2 constr precise
692    
693    | Xml (e1,e2) ->    | Xml (e1,e2) ->
694        type_check_pair ~kind:`XML loc env e1 e2 constr precise        type_check_pair ~kind:`XML loc env e1 e2 constr precise
695    
696    | RecordLitt r ->    | RecordLitt r ->
697  (* try to get rid of precise = true for values of fields *)        type_record loc env r constr precise
698  (* also: the use equivalent of need_second to optimize... *)  
699        let precise = true in    | Map (e,b) ->
700        if not (Types.Record.has_record constr) then        type_map loc env false e b constr precise
701          raise_loc loc (ShouldHave (constr,"but it is a record."));  
702        let (rconstr,res) =    | Transform (e,b) ->
703          List.fold_left        flatten loc (type_map loc env true e b) constr precise
           (fun (rconstr,res) (l,e) ->  
              (* could compute (split l e) once... *)  
              let pi = Types.Record.project_opt rconstr l in  
              if Types.is_empty pi then  
                raise_loc loc  
                  (ShouldHave (constr,(Printf.sprintf  
                                         "Field %s is not allowed here."  
                                         (U.to_string (LabelPool.value l))  
                                      )  
                              ));  
              let t = type_check env e pi true in  
              let rconstr = Types.Record.condition rconstr l t in  
              let res = if precise then (l,Types.cons t) :: res else res in  
              (rconstr,res)  
           ) (constr, []) (LabelMap.get r)  
       in  
       if not (Types.Record.has_empty_record rconstr) then  
         raise_loc loc  
           (ShouldHave (constr,"More fields should be present"));  
       let t =  
         Types.record' (false, LabelMap.from_list (fun _ _ -> assert false) res)  
       in  
       check loc t constr "";  
       t  
 (*  
       if precise then  
         Types.record' (false, LabelMap.from_list (fun _ _ -> assert false) res)  
       else constr  
 *)  
   | Map (def,e,b) ->  
       let acc = if def then Sequence.any else Sequence.star b.br_accept in  
       let t = type_check env e acc true in  
704    
       let constr' = Sequence.approx (Types.cap Sequence.any constr) in  
       let exact = Types.subtype (Sequence.star constr') constr in  
       (* Note:  
          - could be more precise by integrating the decomposition  
          of constr inside Sequence.map.  
       *)  
       let res =  
         Sequence.map  
           (fun t ->  
              let res =  
                type_check_branches loc env t b constr' (precise || (not exact)) in  
              if def && not (Types.subtype t b.br_accept)  
              then Types.cup res Sequence.nil_type  
              else res)  
           t in  
       if not exact then check loc res constr "";  
       if precise then res else constr  
   | Op ("@", [e1;e2]) ->  
       let constr' = Sequence.star  
                       (Sequence.approx (Types.cap Sequence.any constr)) in  
       let exact = Types.subtype constr' constr in  
       if exact then  
         let t1 = type_check env e1 constr' precise  
         and t2 = type_check env e2 constr' precise in  
         if precise then Sequence.concat t1 t2 else constr  
       else  
         (* Note:  
            the knownledge of t1 may makes it useless to  
            check t2 with 'precise' ... *)  
         let t1 = type_check env e1 constr' true  
         and t2 = type_check env e2 constr' true in  
         let res = Sequence.concat t1 t2 in  
         check loc res constr "";  
         if precise then res else constr  
705    | Apply (e1,e2) ->    | Apply (e1,e2) ->
706        let t1 = type_check env e1 Types.Arrow.any true in        let t1 = type_check env e1 Types.Arrow.any true in
707        let t1 = Types.Arrow.get t1 in        let t1 = Types.Arrow.get t1 in
# Line 759  Line 713 
713          else          else
714            (ignore (type_check env e2 dom false); Types.Arrow.apply_noarg t1)            (ignore (type_check env e2 dom false); Types.Arrow.apply_noarg t1)
715        in        in
716        check loc res constr "";        check loc res constr
717        res  
718    | Op ("flatten", [e]) ->    | UnaryOp (o,e) ->
719        let constr' = Sequence.star        let t = o.un_op_typer loc (type_check env e) constr precise in
720                        (Sequence.approx (Types.cap Sequence.any constr)) in        check loc t constr
721        let sconstr' = Sequence.star constr' in  
722        let exact = Types.subtype constr' constr in    | BinaryOp (o,e1,e2) ->
723        if exact then        let t = o.bin_op_typer loc (type_check env e1) (type_check env e2) constr precise in
724          let t = type_check env e sconstr' precise in        check loc t constr
725          if precise then Sequence.flatten t else constr  
726        else    | Var s ->
727          let t = type_check env e sconstr' true in        let t =
728          let res = Sequence.flatten t in          try Env.find s env
729          check loc res constr "";          with Not_found -> raise_loc loc (UnboundId s) in
730          if precise then res else constr        check loc t constr
731    | Op ("atom_of", [e]) ->  
732        let t = type_check env e Sequence.string false in    | Cst c ->
733        Types.atom Atoms.any        check loc (Types.constant c) constr
734    | _ ->  
735        let t : Types.descr = compute_type' loc env e in    | Dot (e,l) ->
736        check loc t constr "";        let t = type_check env e Types.Record.any true in
737        t        let t =
738            try (Types.Record.project t l)
739            with Not_found -> raise_loc loc (WrongLabel(t,l))
740          in
741          check loc t constr
742    
743      | RemoveField (e,l) ->
744          let t = type_check env e Types.Record.any true in
745          let t = Types.Record.remove_field t l in
746          check loc t constr
747    
748      | Xtrans (e,b) ->
749          let t = type_check env e Sequence.any true in
750          let t =
751            Sequence.map_tree
752              (fun t ->
753                 let resid = Types.diff t b.br_accept in
754                 let res = type_check_branches loc env t b Sequence.any true in
755                 (res,resid)
756              ) t in
757          check loc t constr
758    
759    
760  and type_check_pair ?(kind=`Normal) loc env e1 e2 constr precise =  and type_check_pair ?(kind=`Normal) loc env e1 e2 constr precise =
761    let rects = Types.Product.normal ~kind constr in    let rects = Types.Product.normal ~kind constr in
762    if Types.Product.is_empty rects then    if Types.Product.is_empty rects then
763      (match kind with      (match kind with
764        | `Normal -> raise_loc loc (ShouldHave (constr,"but it is a pair."))        | `Normal -> should_have loc constr "but it is a pair"
765        | `XML -> raise_loc loc (ShouldHave (constr,"but it is an XML element.")));        | `XML -> should_have loc constr "but it is an XML element");
766    let need_s = Types.Product.need_second rects in    let need_s = Types.Product.need_second rects in
767    let t1 = type_check env e1 (Types.Product.pi1 rects) (precise || need_s) in    let t1 = type_check env e1 (Types.Product.pi1 rects) (precise || need_s) in
768    let c2 = Types.Product.constraint_on_2 rects t1 in    let c2 = Types.Product.constraint_on_2 rects t1 in
# Line 802  Line 777 
777    else    else
778      constr      constr
779    
780    and type_record loc env r constr precise =
781  and compute_type env e =  (* try to get rid of precise = true for values of fields *)
782    type_check env e Types.any true  (* also: the use equivalent of need_second to optimize... *)
783      if not (Types.Record.has_record constr) then
784  and compute_type' loc env = function      should_have loc constr "but it is a record";
785    | Var s ->    let (rconstr,res) =
786        (try Env.find s env      List.fold_left
787         with Not_found -> raise_loc loc (UnboundId s)        (fun (rconstr,res) (l,e) ->
788        )           (* could compute (split l e) once... *)
789    | Cst c -> Types.constant c           let pi = Types.Record.project_opt rconstr l in
790    | Dot (e,l) ->           if Types.is_empty pi then
791        let t = type_check env e Types.Record.any true in             (let l = U.to_string (LabelPool.value l) in
792           (try (Types.Record.project t l)              should_have loc constr
793            with Not_found -> raise_loc loc (WrongLabel(t,l)))                (Printf.sprintf "Field %s is not allowed here." l));
794    | RemoveField (e,l) ->           let t = type_check env e pi true in
795        let t = type_check env e Types.Record.any true in           let rconstr = Types.Record.condition rconstr l t in
796        Types.Record.remove_field t l           let res = (l,Types.cons t) :: res in
797    | Op (op, el) ->           (rconstr,res)
798        let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in        ) (constr, []) (LabelMap.get r)
       type_op loc op args  
   | Xtrans (e,b) ->  
       let t = type_check env e Sequence.any true in  
       let r =  
         Sequence.map_tree  
           (fun t ->  
              let resid = Types.diff t b.br_accept in  
              let res = type_check_branches loc env t b Sequence.any true in  
              (res,resid)  
           ) t  
799        in        in
800        r    if not (Types.Record.has_empty_record rconstr) then
801        should_have loc constr "More fields should be present";
802      let t =
803        Types.record' (false, LabelMap.from_list (fun _ _ -> assert false) res)
804      in
805      check loc t constr
806    
 (* We keep these cases here to allow comparison and benchmarking ...  
    Just comment the corresponding cases in type_check' to  
    activate these ones.  
 *)  
   | Pair (e1,e2) ->  
       let t1 = compute_type env e1  
       and t2 = compute_type env e2 in  
       Types.times (Types.cons t1) (Types.cons t2)  
   | RecordLitt r ->  
       let r = LabelMap.map (fun e -> Types.cons (compute_type env e)) r in  
       Types.record' (false,r)  
   | _ -> assert false  
807    
808  and type_check_branches loc env targ brs constr precise =  and type_check_branches loc env targ brs constr precise =
809    if Types.is_empty targ then Types.empty    if Types.is_empty targ then Types.empty
# Line 880  Line 838 
838              tres              tres
839          )          )
840    
841    and type_map loc env def e b constr precise =
842      let acc = if def then Sequence.any else Sequence.star b.br_accept in
843      let t = type_check env e acc true in
844    
845      let constr' = Sequence.approx (Types.cap Sequence.any constr) in
846      let exact = Types.subtype (Sequence.star constr') constr in
847      (* Note:
848         - could be more precise by integrating the decomposition
849         of constr inside Sequence.map.
850      *)
851      let res =
852        Sequence.map
853          (fun t ->
854             let res =
855               type_check_branches loc env t b constr' (precise || (not exact)) in
856             if def && not (Types.subtype t b.br_accept)
857             then Types.cup res Sequence.nil_type
858             else res)
859          t in
860      if exact then res else check loc res constr
861    
862  and type_let_decl env l =  and type_let_decl env l =
863    let acc = Types.descr (Patterns.accept l.let_pat) in    let acc = Types.descr (Patterns.accept l.let_pat) in
864    let t = type_check env l.let_body acc true in    let t = type_check env l.let_body acc true in
# Line 905  Line 884 
884         | _ -> assert false) l;         | _ -> assert false) l;
885    types    types
886    
   
 and type_op loc op args =  
   match (op,args) with  
     | "+", [loc1,t1; loc2,t2] ->  
         if (Types.is_empty t1) || (Types.is_empty t2) then Types.empty  
         else if Types.subtype t1 Types.Int.any  
         then (  
           check loc2 t2 Types.Int.any  
                 "The second argument of + must be an integer as the first one";  
           Types.interval  
             (Intervals.add (Types.Int.get t1) (Types.Int.get t2))  
         )  
         else (  
           check loc1 t1 Types.Record.any  
                 "The first argument of + must be a record or an integer";  
           check loc2 t2 Types.Record.any  
                 "The second argument of + must be a record as the first one";  
           Types.Record.merge t1 t2  
         )  
     | "-", [loc1,t1; loc2,t2] ->  
         type_int_binop Intervals.sub loc1 t1 loc2 t2  
     | ("*" | "/" | "mod"), [loc1,t1; loc2,t2] ->  
         type_int_binop (fun i1 i2 -> Intervals.any) loc1 t1 loc2 t2  
     | "@", [loc1,t1; loc2,t2] ->  
         check loc1 t1 Sequence.any  
           "The first argument of @ must be a sequence";  
         Sequence.concat t1 t2  
     | "flatten", [loc1,t1] ->  
         check loc1 t1 Sequence.seqseq  
           "The argument of flatten must be a sequence of sequences";  
         Sequence.flatten t1  
     | "load_xml", [loc1,t1] ->  
         check loc1 t1 Sequence.string  
           "The argument of load_xml must be a string (filename)";  
         Types.any  
     | "load_file_utf8", [loc1,t1] ->  
         check loc1 t1 Sequence.string  
           "The argument of load_file must be a string (filename)";  
         Sequence.string  
     | "load_file", [loc1,t1] ->  
         check loc1 t1 Sequence.string  
           "The argument of load_file must be a string (filename)";  
         Builtin.string_latin1  
     | "load_html", [loc1,t1] ->  
         check loc1 t1 Sequence.string  
           "The argument of load_html must be a string (filename)";  
         Types.any  
     | "raise", [loc1,t1] ->  
         Types.empty  
     | "print_xml", [loc1,t1] ->  
         Builtin.string_latin1  
     | "print_xml_utf8", [loc1,t1] ->  
         Sequence.string  
     | "print", [loc1,t1] ->  
         check loc1 t1 Sequence.string  
           "The argument of print must be a string";  
         if not (Types.subtype t1 Builtin.string_latin1) then  
           warning loc "This application of print may fail";  
         Sequence.nil_type  
     | "dump_to_file_utf8", [loc1,t1; loc2,t2] ->  
         check loc1 t1 Sequence.string  
           "The argument of dump_to_file_utf8 must be a string (filename)";  
         check loc2 t2 Sequence.string  
           "The argument of dump_to_file_utf8 must be a string (value to dump)";  
         Sequence.nil_type  
     | "dump_to_file", [loc1,t1; loc2,t2] ->  
         check loc1 t1 Sequence.string  
           "The argument of dump_to_file must be a string (filename)";  
         check loc2 t2 Sequence.string  
           "The argument of dump_to_file must be a string (value to dump)";  
         if not (Types.subtype t2 Builtin.string_latin1) then  
           warning loc "This application of dump_to_file may fail";  
         Sequence.nil_type  
     | "int_of", [loc1,t1] ->  
         check loc1 t1 Sequence.string  
           "The argument of int_of must be a string";  
         if not (Types.subtype t1 Builtin.intstr) then  
           warning loc "This application of int_of may fail";  
         Types.interval Intervals.any  
     | "string_of", [loc1,t1] ->  
         Builtin.string_latin1  
     | "=", [loc1,t1; loc2,t2] ->  
         (* could prevent comparision of functional value here... *)  
         (* could also handle the case when t1 and t2 are the same  
            singleton type *)  
         if Types.is_empty (Types.cap t1 t2) then  
           Builtin.false_type  
         else  
           Builtin.bool  
     | ("<=" | "<" | ">" | ">=" ), [loc1,t1; loc2,t2] ->  
         (* could prevent comparision of functional value here... *)  
         Builtin.bool  
     | _ -> assert false  
   
 and type_int_binop f loc1 t1 loc2 t2 =  
   check loc1 t1 Types.Int.any  
     "The first argument must be an integer";  
   check loc2 t2 Types.Int.any  
     "The second argument must be an integer";  
   Types.interval  
     (f (Types.Int.get t1) (Types.Int.get t2))  
   
   
   
   
887  let report_unused_branches () =  let report_unused_branches () =
888    List.iter    List.iter
889      (fun b ->      (fun b -> if not b.br_used then warning b.br_loc "This branch is not used")
        if not b.br_used then  
          warning b.br_loc "This branch is not used"  
     )  
890      !all_branches;      !all_branches;
891    all_branches := []    all_branches := []
892    
Legend:
Removed from v.420  
changed lines
  Added in v.421
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5