Commit 57f3390a authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2002-10-21 21:12:57 by cvscast] Empty log message

Original author: cvscast
Date: 2002-10-21 21:12:57+00:00
parent 5c21ad34
......@@ -47,11 +47,11 @@ run_top: all.cma
ledit ocaml $(INCLUDES) all.cma
clean:
(cd parser; rm -f *.cmi *.cmo *.cma *~)
(cd types; rm -f *.cmi *.cmo *.cma *~)
(cd typing; rm -f *.cmi *.cmo *.cma *~)
(cd driver; rm -f *.cmi *.cmo *.cma *~)
rm -f *.cmi *.cmo *.cma *~
(cd parser; rm -f *.cmi *.cmo *.cma *.cmx *.o *~)
(cd types; rm -f *.cmi *.cmo *.cma *.cmx *.o *~)
(cd typing; rm -f *.cmi *.cmo *.cma *.cmx *.o *~)
(cd driver; rm -f *.cmi *.cmo *.cma *.cmx *.o *~)
rm -f *.cmi *.cmo *.cma *.cmx *.o *~
rm -f cduce
.SUFFIXES: .ml .mli .cmo .cmi .cmx
......
......@@ -5,49 +5,23 @@ let decompose t =
(Types.Atom.has_atom t nil_atom,
Types.Product.get t)
(*
let memo_concat = Types.DescrHash.create 63
let rec aux_concat t s =
try Types.DescrHash.find memo_concat t
with Not_found ->
let n = Types.make () in
Types.DescrHash.add memo_concat t n;
let (has_nil,rect) = decompose t in
let d = List.fold_left
(fun accu (t1,t2) ->
Types.cup accu (Types.times (Types.cons t1) (aux_concat t2 s))
)
(if has_nil then s else Types.empty)
rect
in
Types.define n d;
n
let concat t s =
let n = aux_concat t s in
Types.DescrHash.clear memo_concat;
Types.descr (Types.internalize n)
*)
module V = Types.Positive
module H = Types.DescrHash
let mapping f t queue =
let memo = H.create 13 in
let rec aux_map t =
let rec aux t =
try H.find memo t
with Not_found ->
let v = V.forward () in
H.add memo t v;
let (has_nil,rect) = decompose t in
let l = List.map (fun (t1,t2) -> f t1 (aux_map t2)) rect in
let l = List.map (fun (t1,t2) -> f t1 (aux t2)) rect in
let l = if has_nil then queue :: l else l in
V.define v (V.cup l);
v
in
aux_map t
aux t
let aux_concat = mapping (fun t v -> V.times (V.ty t) v)
......@@ -65,10 +39,26 @@ let recurs f =
Types.define n (f n);
Types.internalize n
let star t = recurs (fun n -> Types.cup nil_type (Types.times t n ))
let star_node t = recurs (fun n -> Types.cup nil_type (Types.times t n ))
let any_node = star (Types.cons Types.any)
let any_node = star_node (Types.cons Types.any)
let any = Types.descr any_node
let seqseq = Types.descr (star any_node)
let seqseq = Types.descr (star_node any_node)
let star t = Types.descr (star_node (Types.cons t))
let approx t =
let memo = H.create 13 in
let res = ref Types.empty in
let rec aux t =
try H.find memo t
with Not_found ->
H.add memo t ();
let rect = Types.Product.get t in
List.iter (fun (t1,t2) -> res := Types.cup t1 !res; aux t2) rect;
in
aux t;
!res
......@@ -6,3 +6,15 @@ val seqseq: Types.descr
val concat: Types.descr -> Types.descr -> Types.descr
val flatten: Types.descr -> Types.descr
val map: (Types.descr -> Types.descr) -> Types.descr -> Types.descr
val star: Types.descr -> Types.descr
(* For a type t, returns [t*] *)
val approx: Types.descr -> Types.descr
(* For a type t <= [Any*], returns the least type s such that:
t <= [s*]
In general, for an arbitrary type, returns the least type s such that:
t <= (X where X = (s, X) | Any \ (Any,Any))
*)
......@@ -398,8 +398,9 @@ let check loc t s msg =
if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg))
let rec type_check env e constr precise =
(* Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
Types.Print.print_descr constr precise; *)
(* Format.fprintf Format.std_formatter "constr=%a precise=%b@\n"
Types.Print.print_descr constr precise;
*)
let d = type_check' e.exp_loc env e.exp_descr constr precise in
e.exp_typ <- Types.cup e.exp_typ d;
d
......@@ -469,6 +470,43 @@ and type_check' loc env e constr precise = match e with
in
res
| Map (e,b) ->
let t = type_check env e (Sequence.star b.br_accept) true in
let constr' = Sequence.approx (Types.cap Sequence.any constr) in
let exact = Types.subtype (Sequence.star constr') constr in
if exact then
let res = type_check_branches loc env t b constr' precise in
if precise then Sequence.star res else constr
else
(* Note:
- could be more precise by integrating the decomposition
of constr inside Sequence.map.
*)
let res =
Sequence.map
(fun t -> type_check_branches loc env t b constr' true)
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
| _ ->
let t : Types.descr = compute_type' loc env e in
check loc t constr "";
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment