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

Diff of /typing/typer.ml

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

revision 18 by abate, Tue Jul 10 16:58:28 2007 UTC revision 19 by abate, Tue Jul 10 16:58:37 2007 UTC
# Line 7  Line 7 
7  exception Pattern of string  exception Pattern of string
8  exception NonExhaustive of Types.descr  exception NonExhaustive of Types.descr
9  exception Constraint of Types.descr * Types.descr * string  exception Constraint of Types.descr * Types.descr * string
10    exception ShouldHave of Types.descr * string
11    
12  let raise_loc loc exn = raise (Location (loc,exn))  let raise_loc loc exn = raise (Location (loc,exn))
13    
# Line 357  Line 358 
358    
359    and branches b =    and branches b =
360      let fv = ref Fv.empty in      let fv = ref Fv.empty in
361        let accept = ref Types.empty in
362      let b = List.map      let b = List.map
363                (fun (p,e) ->                (fun (p,e) ->
364                   let (fv2,e) = expr e in                   let (fv2,e) = expr e in
365                   fv := Fv.union !fv fv2;                   fv := Fv.union !fv fv2;
366                     let p = pat p in
367                     accept := Types.cup !accept (Types.descr (Patterns.accept p));
368                   { Typed.br_used = false;                   { Typed.br_used = false;
369                     Typed.br_pat = pat p;                     Typed.br_pat = p;
370                     Typed.br_body = e }                     Typed.br_body = e }
371                ) b in                ) b in
372      (!fv, { Typed.br_typ = Types.empty; Typed.br_branches = b } )      (!fv,
373         {
374           Typed.br_typ = Types.empty;
375           Typed.br_branches = b;
376           Typed.br_accept = !accept
377         }
378        )
379    
380  module Env = StringMap  module Env = StringMap
381    
# Line 375  Line 385 
385  let check loc t s msg =  let check loc t s msg =
386    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))
387    
388  let rec compute_type env e =  let rec type_check env e constr precise =
389    let d = compute_type' e.exp_loc env e.exp_descr in   (* Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
390        Types.Print.print_descr constr precise;  *)
391      let d = type_check' e.exp_loc env e.exp_descr constr precise in
392    e.exp_typ <- Types.cup e.exp_typ d;    e.exp_typ <- Types.cup e.exp_typ d;
393    d    d
394    
395    and type_check' loc env e constr precise = match e with
396      | Abstraction a ->
397          let t =
398            try Types.Arrow.check_strenghten a.fun_typ constr
399            with Not_found ->
400              raise_loc loc
401              (ShouldHave
402                 (constr, "but the interface of the abstraction is not compatible"))
403          in
404          let env = match a.fun_name with
405            | None -> env
406            | Some f -> Env.add f a.fun_typ env in
407          List.iter
408            (fun (t1,t2) ->
409               ignore (type_check_branches loc env t1 a.fun_body t2 false)
410            ) a.fun_iface;
411          t
412      | Match (e,b) ->
413          let t = type_check env e b.br_accept true in
414          type_check_branches loc env t b constr precise
415      | Pair (e1,e2) ->
416          let rects = Types.Product.get constr in
417          if Types.Product.is_empty rects then
418            raise_loc loc (ShouldHave (constr,"but it is a pair."));
419          let pi1 = Types.Product.pi1 rects in
420    
421          let t1 = type_check env e1 (Types.Product.pi1 rects)
422                     (precise || (Types.Product.need_second rects))in
423          let rects = Types.Product.restrict_1 rects t1 in
424          let t2 = type_check env e2 (Types.Product.pi2 rects) precise in
425          if precise then
426            Types.times (Types.cons t1) (Types.cons t2)
427          else
428            constr
429      | _ ->
430          let t : Types.descr = compute_type' loc env e in
431          check loc t constr "";
432          t
433    
434    and compute_type env e =
435      type_check env e Types.any true
436    
437  and compute_type' loc env = function  and compute_type' loc env = function
438    | DebugTyper t -> Types.descr t    | DebugTyper t -> Types.descr t
439    | Var s -> Env.find s env    | Var s -> Env.find s env
440    | Apply (e1,e2) ->    | Apply (e1,e2) ->
441        let t1 = compute_type env e1 and t2 = compute_type env e2 in        let t1 = type_check env e1 Types.Arrow.any true in
       if Types.is_empty t2  
       then Types.empty  
       else  
         if Types.subtype t1 Types.Arrow.any  
         then  
442            let t1 = Types.Arrow.get t1 in            let t1 = Types.Arrow.get t1 in
443            let dom = Types.Arrow.domain t1 in            let dom = Types.Arrow.domain t1 in
444            if Types.subtype t2 dom        if Types.Arrow.need_arg t1 then
445            then Types.Arrow.apply t1 t2          let t2 = type_check env e2 dom true in
446            else          Types.Arrow.apply t1 t2
             raise_loc loc  
               (Constraint  
                  (t2,dom,"The argument is not in the domain of the function"))  
447          else          else
448            raise_loc loc          (ignore (type_check env e2 dom false); Types.Arrow.apply_noarg t1)
             (Constraint  
                (t1,Types.Arrow.any,"The expression in function position is not necessarily a function"))  
   | Abstraction a ->  
       let env = match a.fun_name with  
         | None -> env  
         | Some f -> Env.add f a.fun_typ env in  
       List.iter (fun (t1,t2) ->  
                    let t = type_branches loc env t1 a.fun_body in  
                    if not (Types.subtype t t2) then  
                      raise_loc loc (Constraint (t,t2,"Constraint not satisfied in interface"))  
                 ) a.fun_iface;  
       a.fun_typ  
449    | Cst c -> Types.constant c    | Cst c -> Types.constant c
   | Pair (e1,e2) ->  
       let t1 = compute_type env e1 and t2 = compute_type env e2 in  
       let t1 = Types.cons t1 and t2 = Types.cons t2 in  
       Types.times t1 t2  
450    | RecordLitt r ->    | RecordLitt r ->
451        List.fold_left        List.fold_left
452          (fun accu (l,e) ->          (fun accu (l,e) ->
# Line 427  Line 457 
457    | Op (op, el) ->    | Op (op, el) ->
458        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
459        type_op loc op args        type_op loc op args
   | Match (e,b) ->  
       let t = compute_type env e in  
       type_branches loc env t b  
460    | Map (e,b) ->    | Map (e,b) ->
461        let t = compute_type env e in        let t = compute_type env e in
462        Sequence.map (fun t -> type_branches loc env t b) t        Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t
463      | _ -> assert false
464    
465  and type_branches loc env targ brs =  and type_check_branches loc env targ brs constr precise =
466    if Types.is_empty targ then Types.empty    if Types.is_empty targ then Types.empty
467    else (    else (
468      brs.br_typ <- Types.cup brs.br_typ targ;      brs.br_typ <- Types.cup brs.br_typ targ;
469      branches_aux loc env targ Types.empty brs.br_branches      branches_aux loc env targ
470          (if precise then Types.empty else constr)
471          constr precise brs.br_branches
472    )    )
473    
474  and branches_aux loc env targ tres = function  and branches_aux loc env targ tres constr precise = function
475    | [] -> raise_loc loc (NonExhaustive targ)    | [] -> raise_loc loc (NonExhaustive targ)
476    | b :: rem ->    | b :: rem ->
477        let p = b.br_pat in        let p = b.br_pat in
# Line 449  Line 479 
479    
480        let targ' = Types.cap targ acc in        let targ' = Types.cap targ acc in
481        if Types.is_empty targ'        if Types.is_empty targ'
482        then branches_aux loc env targ tres rem        then branches_aux loc env targ tres constr precise rem
483        else        else
484          ( b.br_used <- true;          ( b.br_used <- true;
485            let res = Patterns.filter targ' p in            let res = Patterns.filter targ' p in
486            let env' = List.fold_left            let env' = List.fold_left
487                         (fun env (x,t) -> Env.add x (Types.descr t) env)                         (fun env (x,t) -> Env.add x (Types.descr t) env)
488                         env res in                         env res in
489            let t = compute_type env' b.br_body in            let t = type_check env' b.br_body constr precise in
490            let tres = Types.cup t tres in            let tres = if precise then Types.cup t tres else tres in
491            let targ'' = Types.diff targ acc in            let targ'' = Types.diff targ acc in
492            if (Types.non_empty targ'') then            if (Types.non_empty targ'') then
493              branches_aux loc env targ'' (Types.cup t tres) rem              branches_aux loc env targ'' tres constr precise rem
494            else            else
495              tres              tres
496          )          )
Legend:
Removed from v.18  
changed lines
  Added in v.19
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5