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

Diff of /typing/typer.ml

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

revision 53 by abate, Tue Jul 10 17:01:10 2007 UTC revision 54 by abate, Tue Jul 10 17:01:32 2007 UTC
# Line 29  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 113  Line 113 
113              compile fin e rest              compile fin e rest
114          | `Elem (vars,x) :: rest ->          | `Elem (vars,x) :: rest ->
115              let capt = StringSet.fold              let capt = StringSet.fold
116                           (fun v t -> mk noloc (And (t, (mk noloc (Capture v)))))                           (fun v t -> mk noloc (And (t, (mk noloc (Capture v)), true)))
117                           vars x in                           vars x in
118              `Res (mk noloc (Prod (capt, guard_compile fin rest)))              `Res (mk noloc (Prod (capt, guard_compile fin rest)))
119          | `Seq (r1,r2) :: rest ->          | `Seq (r1,r2) :: rest ->
# Line 139  Line 139 
139    
140    let atom_nil = Types.mk_atom "nil"    let atom_nil = Types.mk_atom "nil"
141    let constant_nil v t =    let constant_nil v t =
142      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))
143    
144    let compile regexp queue : ppat =    let compile regexp queue : ppat =
145      let vars = seq_vars StringSet.empty regexp in      let vars = seq_vars StringSet.empty regexp in
# Line 165  Line 165 
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))
168    | 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))
169    | Diff (t1,t2) -> cons loc (`Diff (compile env t1, compile env t2))    | Diff (t1,t2) -> cons loc (`Diff (compile env t1, compile env t2))
170    | Prod (t1,t2) -> cons loc (`Times (compile env t1, compile env t2))    | Prod (t1,t2) -> cons loc (`Times (compile env t1, compile env t2))
171    | 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 189  Line 189 
189            match s.descr' with            match s.descr' with
190              | `Alias (_,x) -> if List.memq s seen then [] else comp_fv (s :: seen) x              | `Alias (_,x) -> if List.memq s seen then [] else comp_fv (s :: seen) x
191              | `Or (s1,s2)              | `Or (s1,s2)
192              | `And (s1,s2)              | `And (s1,s2,_)
193              | `Diff (s1,s2)              | `Diff (s1,s2)
194              | `Times (s1,s2)              | `Times (s1,s2)
195              | `Arrow (s1,s2) -> SortedList.cup (comp_fv seen s1) (comp_fv seen s2)              | `Arrow (s1,s2) -> SortedList.cup (comp_fv seen s1) (comp_fv seen s2)
# Line 214  Line 214 
214          else typ (s :: seen) x          else typ (s :: seen) x
215      | `Type t -> t      | `Type t -> t
216      | `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)      | `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2)
217      | `And (s1,s2) ->  Types.cap (typ seen s1) (typ seen s2)      | `And (s1,s2,_) ->  Types.cap (typ seen s1) (typ seen s2)
218      | `Diff (s1,s2) -> Types.diff (typ seen s1) (typ seen s2)      | `Diff (s1,s2) -> Types.diff (typ seen s1) (typ seen s2)
219      | `Times (s1,s2) -> Types.times (typ_node s1) (typ_node s2)      | `Times (s1,s2) -> Types.times (typ_node s1) (typ_node s2)
220      | `Arrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)      | `Arrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)
# Line 243  Line 243 
243                 ("Unguarded recursion on variable " ^ v ^ " in this pattern"))                 ("Unguarded recursion on variable " ^ v ^ " in this pattern"))
244          else pat (s :: seen) x          else pat (s :: seen) x
245      | `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)      | `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2)
246      | `And (s1,s2) -> Patterns.cap (pat seen s1) (pat seen s2)      | `And (s1,s2,e) -> Patterns.cap (pat seen s1) (pat seen s2) e
247      | `Diff (s1,s2) when fv s2 = [] ->      | `Diff (s1,s2) when fv s2 = [] ->
248          let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in          let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in
249          Patterns.cap (pat seen s1) (Patterns.constr s2)          Patterns.cap (pat seen s1) (Patterns.constr s2) true
250      | `Diff _ ->      | `Diff _ ->
251          raise_loc s.loc' (Pattern "Difference not allowed in patterns")          raise_loc s.loc' (Pattern "Difference not allowed in patterns")
252      | `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)      | `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
# Line 302  Line 302 
302    let (fv,td) =    let (fv,td) =
303      match d with      match d with
304        | DebugTyper t -> (Fv.empty, Typed.DebugTyper (typ t))        | DebugTyper t -> (Fv.empty, Typed.DebugTyper (typ t))
305          | Forget (e,t) ->
306              let (fv,e) = expr e and t = typ t in
307              (fv, Typed.Forget (e,t))
308        | Var s -> (Fv.singleton s, Typed.Var s)        | Var s -> (Fv.singleton s, Typed.Var s)
309        | Apply (e1,e2) ->        | Apply (e1,e2) ->
310            let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in            let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in
# Line 406  Line 409 
409    d    d
410    
411  and type_check' loc env e constr precise = match e with  and type_check' loc env e constr precise = match e with
412      | Forget (e,t) ->
413          let t = Types.descr t in
414          ignore (type_check env e t false);
415          t
416    | Abstraction a ->    | Abstraction a ->
417        let t =        let t =
418          try Types.Arrow.check_strenghten a.fun_typ constr          try Types.Arrow.check_strenghten a.fun_typ constr
# Line 475  Line 482 
482    
483        let constr' = Sequence.approx (Types.cap Sequence.any constr) in        let constr' = Sequence.approx (Types.cap Sequence.any constr) in
484        let exact = Types.subtype (Sequence.star constr') constr in        let exact = Types.subtype (Sequence.star constr') constr in
485    (*
486        if exact then (        Format.fprintf Format.std_formatter
487          (* Note: typing mail fail because of the approx on t *)          "(Map) constr = %a@;  exact = %b\n@." Types.Print.print_descr constr exact;
488          let res = type_check_branches loc env (Sequence.approx t)  *)
                     b constr' precise in  
         if precise then Sequence.star res else constr  
       )  
       else  
489          (* Note:          (* Note:
490             - could be more precise by integrating the decomposition             - could be more precise by integrating the decomposition
491             of constr inside Sequence.map.             of constr inside Sequence.map.
492          *)          *)
493          let res =          let res =
494            Sequence.map            Sequence.map
495              (fun t -> type_check_branches loc env t b constr' true)            (fun t ->
496                 type_check_branches loc env t b constr' (precise || (not exact)))
497              t in              t in
498          if not exact then check loc res constr "";          if not exact then check loc res constr "";
499          if precise then res else constr          if precise then res else constr
Legend:
Removed from v.53  
changed lines
  Added in v.54
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5