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

Diff of /typing/typer.ml

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

revision 17 by abate, Tue Jul 10 16:58:13 2007 UTC revision 37 by abate, Tue Jul 10 16:59:53 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 284  Line 288 
288    let env = compile_many !global_types b in    let env = compile_many !global_types b in
289    List.iter (fun (v,_) ->    List.iter (fun (v,_) ->
290                 let d = Types.descr (mk_typ (StringMap.find v env)) in                 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                 Types.Print.register_global v d
293              ) b;              ) b;
294    global_types := env    global_types := env
# Line 296  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 325  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 ->
338            (* XXX TODO: check that no label appears twice *)            (* Note: quadratic check for non duplication of labels.
339                 Should improve that to O(n log n) for dealing
340                 with huge number of attributes ?
341              *)
342            let fv = ref Fv.empty in            let fv = ref Fv.empty in
343              let labs = ref [] in
344            let r = List.map            let r = List.map
345                      (fun (l,e) ->                      (fun (l,e) ->
346                         let (fv2,e) = expr e in                         let (fv2,e) = expr e in
347                           if (List.mem l !labs) then
348                             raise_loc loc (MultipleLabel l);
349                           labs := l :: !labs;
350                         fv := Fv.union !fv fv2;                         fv := Fv.union !fv fv2;
351                         (l,e)                         (l,e)
352                      ) r in                      ) r in
# Line 356  Line 372 
372    
373    and branches b =    and branches b =
374      let fv = ref Fv.empty in      let fv = ref Fv.empty in
375        let accept = ref Types.empty in
376      let b = List.map      let b = List.map
377                (fun (p,e) ->                (fun (p,e) ->
378                   let (fv2,e) = expr e in                   let (fv2,e) = expr e in
379                   fv := Fv.union !fv fv2;                   fv := Fv.union !fv fv2;
380                     let p = pat p in
381                     accept := Types.cup !accept (Types.descr (Patterns.accept p));
382                   { Typed.br_used = false;                   { Typed.br_used = false;
383                     Typed.br_pat = pat p;                     Typed.br_pat = p;
384                     Typed.br_body = e }                     Typed.br_body = e }
385                ) b in                ) b in
386      (!fv, { Typed.br_typ = Types.empty; Typed.br_branches = b } )      (!fv,
387         {
388           Typed.br_typ = Types.empty;
389           Typed.br_branches = b;
390           Typed.br_accept = !accept
391         }
392        )
393    
394  module Env = StringMap  module Env = StringMap
395    
# Line 374  Line 399 
399  let check loc t s msg =  let check loc t s msg =
400    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))
401    
402  let rec compute_type env e =  let rec type_check env e constr precise =
403    let d = compute_type' e.exp_loc env e.exp_descr in  (*  Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
404        Types.Print.print_descr constr precise;
405    *)
406      let d = type_check' e.exp_loc env e.exp_descr constr precise in
407    e.exp_typ <- Types.cup e.exp_typ d;    e.exp_typ <- Types.cup e.exp_typ d;
408    d    d
409    
410  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  
       if Types.is_empty t2  
       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"))  
411    | Abstraction a ->    | Abstraction a ->
412          let t =
413            try Types.Arrow.check_strenghten a.fun_typ constr
414            with Not_found ->
415              raise_loc loc
416              (ShouldHave
417                 (constr, "but the interface of the abstraction is not compatible"))
418          in
419        let env = match a.fun_name with        let env = match a.fun_name with
420          | None -> env          | None -> env
421          | Some f -> Env.add f a.fun_typ env in          | Some f -> Env.add f a.fun_typ env in
422        List.iter (fun (t1,t2) ->        List.iter
423                     let t = type_branches loc env t1 a.fun_body in          (fun (t1,t2) ->
424                     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"))  
425                  ) a.fun_iface;                  ) a.fun_iface;
426        a.fun_typ        t
427      | Match (e,b) ->
428          let t = type_check env e b.br_accept true in
429          type_check_branches loc env t b constr precise
430    
431      | Pair (e1,e2) ->
432          let rects = Types.Product.get constr in
433          if Types.Product.is_empty rects then
434            raise_loc loc (ShouldHave (constr,"but it is a pair."));
435          let pi1 = Types.Product.pi1 rects in
436    
437          let t1 = type_check env e1 (Types.Product.pi1 rects)
438                     (precise || (Types.Product.need_second rects))in
439          let rects = Types.Product.restrict_1 rects t1 in
440          let t2 = type_check env e2 (Types.Product.pi2 rects) precise in
441          if precise then
442            Types.times (Types.cons t1) (Types.cons t2)
443          else
444            constr
445    
446      | RecordLitt r ->
447          let rconstr = Types.Record.get constr in
448          if Types.Record.is_empty rconstr then
449            raise_loc loc (ShouldHave (constr,"but it is a record."));
450    
451          let (rconstr,res) =
452            List.fold_left
453              (fun (rconstr,res) (l,e) ->
454                 let rconstr = Types.Record.restrict_label_present rconstr l in
455                 let pi = Types.Record.project_field rconstr l in
456                 if Types.Record.is_empty rconstr then
457                   raise_loc loc
458                     (ShouldHave (constr,(Printf.sprintf
459                                            "Field %s is not allowed here."
460                                            (Types.label_name l)
461                                         )
462                                 ));
463                 let t = type_check env e pi true in
464                 let rconstr = Types.Record.restrict_field rconstr l t in
465    
466                 let res =
467                   if precise
468                   then Types.cap res (Types.record l false (Types.cons t))
469                   else res in
470                 (rconstr,res)
471              ) (rconstr, if precise then Types.Record.any else constr) r
472          in
473          res
474    
475      | Map (e,b) ->
476          let t = type_check env e (Sequence.star b.br_accept) true in
477    
478          let constr' = Sequence.approx (Types.cap Sequence.any constr) in
479          let exact = Types.subtype (Sequence.star constr') constr in
480    
481          if exact then (
482            (* Note: typing mail fail because of the approx on t *)
483            let res = type_check_branches loc env (Sequence.approx t)
484                        b constr' precise in
485            if precise then Sequence.star res else constr
486          )
487          else
488            (* Note:
489               - could be more precise by integrating the decomposition
490               of constr inside Sequence.map.
491            *)
492            let res =
493              Sequence.map
494                (fun t -> type_check_branches loc env t b constr' true)
495                t in
496            if not exact then check loc res constr "";
497            if precise then res else constr
498      | Op ("@", [e1;e2]) ->
499          let constr' = Sequence.star
500                          (Sequence.approx (Types.cap Sequence.any constr)) in
501          let exact = Types.subtype constr' constr in
502          if exact then
503            let t1 = type_check env e1 constr' precise
504            and t2 = type_check env e2 constr' precise in
505            if precise then Sequence.concat t1 t2 else constr
506          else
507            (* Note:
508               the knownledge of t1 may makes it useless to
509               check t2 with 'precise' ... *)
510            let t1 = type_check env e1 constr' true
511            and t2 = type_check env e2 constr' true in
512            let res = Sequence.concat t1 t2 in
513            check loc res constr "";
514            if precise then res else constr
515      | Op ("flatten", [e]) ->
516          let constr' = Sequence.star
517                          (Sequence.approx (Types.cap Sequence.any constr)) in
518          let sconstr' = Sequence.star constr' in
519          let exact = Types.subtype constr' constr in
520          if exact then
521            let t = type_check env e sconstr' precise in
522            if precise then Sequence.flatten t else constr
523          else
524            let t = type_check env e sconstr' true in
525            let res = Sequence.flatten t in
526            check loc res constr "";
527            if precise then res else constr
528      | _ ->
529          let t : Types.descr = compute_type' loc env e in
530          check loc t constr "";
531          t
532    
533    and compute_type env e =
534      type_check env e Types.any true
535    
536    and compute_type' loc env = function
537      | DebugTyper t -> Types.descr t
538      | Var s ->
539          (try Env.find s env
540           with Not_found -> raise_loc loc (UnboundId s)
541          )
542      | Apply (e1,e2) ->
543          let t1 = type_check env e1 Types.Arrow.any true in
544          let t1 = Types.Arrow.get t1 in
545          let dom = Types.Arrow.domain t1 in
546          if Types.Arrow.need_arg t1 then
547            let t2 = type_check env e2 dom true in
548            Types.Arrow.apply t1 t2
549          else
550            (ignore (type_check env e2 dom false); Types.Arrow.apply_noarg t1)
551    | Cst c -> Types.constant c    | Cst c -> Types.constant c
552      | Dot (e,l) ->
553          let t = type_check env e Types.Record.any true in
554             (try (Types.Record.project t l)
555              with Not_found -> raise_loc loc (WrongLabel(t,l)))
556      | Op (op, el) ->
557          let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in
558          type_op loc op args
559      | Map (e,b) ->
560          let t = compute_type env e in
561          Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t
562    
563    (* We keep these cases here to allow comparison and benchmarking ...
564       Just comment the corresponding cases in type_check' to
565       activate these ones.
566    *)
567    | Pair (e1,e2) ->    | Pair (e1,e2) ->
568        let t1 = compute_type env e1 and t2 = compute_type env e2 in        let t1 = compute_type env e1
569        let t1 = Types.cons t1 and t2 = Types.cons t2 in        and t2 = compute_type env e2 in
570        Types.times t1 t2        Types.times (Types.cons t1) (Types.cons t2)
571    | RecordLitt r ->    | RecordLitt r ->
572        List.fold_left        List.fold_left
573          (fun accu (l,e) ->          (fun accu (l,e) ->
# Line 422  Line 575 
575             let t = Types.record l false (Types.cons t) in             let t = Types.record l false (Types.cons t) in
576             Types.cap accu t             Types.cap accu t
577          ) Types.Record.any r          ) Types.Record.any r
   | Op (op, el) ->  
       let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in  
       type_op loc op args  
   | Match (e,b) ->  
       let t = compute_type env e in  
       type_branches loc env t b  
   | Map (e,b) ->  
       let t = compute_type env e in  
       Sequence.map (fun t -> type_branches loc env t b) t  
578    
579  and type_branches loc env targ brs =  
580      | _ -> assert false
581    
582    and type_check_branches loc env targ brs constr precise =
583    if Types.is_empty targ then Types.empty    if Types.is_empty targ then Types.empty
584    else (    else (
585      brs.br_typ <- Types.cup brs.br_typ targ;      brs.br_typ <- Types.cup brs.br_typ targ;
586      branches_aux loc env targ Types.empty brs.br_branches      branches_aux loc env targ
587          (if precise then Types.empty else constr)
588          constr precise brs.br_branches
589    )    )
590    
591  and branches_aux loc env targ tres = function  and branches_aux loc env targ tres constr precise = function
592    | [] -> raise_loc loc (NonExhaustive targ)    | [] -> raise_loc loc (NonExhaustive targ)
593    | b :: rem ->    | b :: rem ->
594        let p = b.br_pat in        let p = b.br_pat in
# Line 447  Line 596 
596    
597        let targ' = Types.cap targ acc in        let targ' = Types.cap targ acc in
598        if Types.is_empty targ'        if Types.is_empty targ'
599        then branches_aux loc env targ tres rem        then branches_aux loc env targ tres constr precise rem
600        else        else
601          ( b.br_used <- true;          ( b.br_used <- true;
602            let res = Patterns.filter targ' p in            let res = Patterns.filter targ' p in
603            let env' = List.fold_left            let env' = List.fold_left
604                         (fun env (x,t) -> Env.add x (Types.descr t) env)                         (fun env (x,t) -> Env.add x (Types.descr t) env)
605                         env res in                         env res in
606            let t = compute_type env' b.br_body in            let t = type_check env' b.br_body constr precise in
607            let tres = Types.cup t tres in            let tres = if precise then Types.cup t tres else tres in
608            let targ'' = Types.diff targ acc in            let targ'' = Types.diff targ acc in
609            if (Types.non_empty targ'') then            if (Types.non_empty targ'') then
610              branches_aux loc env targ'' (Types.cup t tres) rem              branches_aux loc env targ'' tres constr precise rem
611            else            else
612              tres              tres
613          )          )
# Line 488  Line 637 
637    if not (Types.Int.is_int t2) then    if not (Types.Int.is_int t2) then
638      raise_loc loc2      raise_loc loc2
639        (Constraint        (Constraint
640                 (t1,Types.Int.any,                 (t2,Types.Int.any,
641                  "The second argument must be an integer"));                  "The second argument must be an integer"));
642    Types.Int.put    Types.Int.put
643      (f (Types.Int.get t1) (Types.Int.get t2));      (f (Types.Int.get t1) (Types.Int.get t2));
Legend:
Removed from v.17  
changed lines
  Added in v.37
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5