Commit 9cf4a7db authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2003-03-17 22:44:29 by cvscast] Empty log message

Original author: cvscast
Date: 2003-03-17 22:44:44+00:00
parent f88e43b9
......@@ -41,12 +41,15 @@ and pexpr' =
| Op of string * pexpr list
| Match of pexpr * branches
| Map of pexpr * branches
| Ttree of pexpr * branches
| Dot of pexpr* label
| RemoveField of pexpr * label
(* Exceptions *)
| Try of pexpr * branches
| MatchFail (* internal usage *)
and abstr = {
fun_name : id option;
fun_iface : (ppat * ppat) list;
......
......@@ -114,6 +114,7 @@ EXTEND
mknoloc (Op ("raise",[mknoloc (Var (ident "x"))]))) in
mk loc (Try (e,b@[default]))
| "map"; e = SELF; "with"; b = branches -> mk loc (Map (e,b))
| "ttree"; e = SELF; "with"; b = branches -> mk loc (Ttree (e,b))
| "if"; e = SELF; "then"; e1 = SELF; "else"; e2 = SELF ->
let p1 = mk loc (Internal (Builtin.true_type))
and p2 = mk loc (Internal (Builtin.false_type)) in
......
......@@ -18,6 +18,7 @@ let exn_int_of = CDuceExn (Pair (
(* Evaluation of expressions *)
exception EMatchFail
let rec eval env e0 =
match e0.Typed.exp_descr with
......@@ -52,6 +53,7 @@ let rec eval env e0 =
| Typed.Cst c -> const c
| Typed.Match (arg,brs) -> eval_branches env brs (eval env arg)
| Typed.Map (arg,brs) -> eval_map env brs (eval env arg)
| Typed.Ttree (arg,brs) -> eval_ttree env brs (eval env arg)
| Typed.Op ("raise", [e]) -> raise (CDuceExn (eval env e))
| Typed.Try (arg,brs) ->
(try eval env arg with CDuceExn v -> eval_branches env brs v)
......@@ -80,6 +82,7 @@ let rec eval env e0 =
| Typed.Op (">=",[e1; e2]) -> eval_gte (eval env e1) (eval env e2)
| Typed.Dot (e, l) -> eval_dot l (eval env e)
| Typed.RemoveField (e, l) -> eval_remove_field l (eval env e)
| Typed.MatchFail -> raise EMatchFail
| Typed.Op (o,_) -> failwith ("Unknown operator " ^ o)
......@@ -124,6 +127,25 @@ and eval_transform env brs = function
| String (_,_,_,_) as v -> eval_transform env brs (normalize v)
| q -> q
and eval_ttree env brs = function
| Pair (x,y) ->
let y = eval_ttree env brs y in (* Beware of evaluation order !! Reverse it ? *)
(try
let x = eval_branches env brs x in
(* TODO: avoid raising exceptions (for each character/element !) *)
eval_concat x y
with EMatchFail ->
let x = match x with
| Xml (tag, Pair (attr, child)) ->
let child = eval_ttree env brs child in
Xml (tag, Pair (attr, child))
| Xml (_,_) -> assert false
| x -> x in
Pair (x,y))
| String (_,_,_,_) as v -> eval_ttree env brs (normalize v)
(* TODO: optimize for strings, to avoid decomposing compound String values *)
| q -> q
and eval_concat l1 l2 = match l1 with
| Pair (x,y) -> Pair (x, eval_concat y l2)
| String (s,i,j,q) -> String (s,i,j, eval_concat q l2)
......
include "../web/xhtml-strict.cd";;
let fun f (x : Xhtml) : [ Xhtml ] =
ttree [ x ] with <a>t -> [];;
(*
type T = <a>[ <b>[] T* <b>[] ];;
type S = <a>[ <x>[] S* <x>[] ];;
let fun f (x : [ T ]) : [ S ] =
ttree x with <b>_ -> [ <x>[] ];;
let x = f [ <a>[ <b>[] <b>[] ] ];;
*)
......@@ -90,7 +90,20 @@ let equal t1 t2 = match (t1,t2) with
| (Cofinite l1, Cofinite l2) -> equal_rec l1 l2
| _ -> false
let rec compare_rec l1 l2 =
if (l1 == l2) then 0 else
match (l1,l2) with
| (x1::l1,x2::l2) ->
let c = AtomPool.compare x1 x2 in if c <> 0 then c
else compare_rec l1 l2
| ([],_) -> -1
| _ -> 1
let compare t1 t2 = match (t1,t2) with
| (Finite l1, Finite l2) -> compare_rec l1 l2
| (Cofinite l1, Cofinite l2) -> compare_rec l1 l2
| (Finite _, Cofinite _) -> -1
| (Cofinite _, Finite _) -> 1
(* Optimize lookup:
- decision tree
......
......@@ -8,6 +8,7 @@ val vcompare: v -> v -> int
type t
val hash: int -> t -> int
val equal: t -> t -> bool
val compare: t -> t -> int
val print : t -> (Format.formatter -> unit) list
val empty : t
......
(* Optimization ideas:
- (A|B) & (C|D) = A | (B & (C|D)) if A <= C
*)
module type S =
sig
type 'a elem
......
......@@ -19,6 +19,7 @@ type interval =
type t = interval list
let rec equal l1 l2 =
(l1 == l2) ||
match (l1,l2) with
......@@ -84,7 +85,7 @@ let rec iadd_bounded l a b = match l with
| Bounded (a1,b1) :: l' ->
iadd_bounded l' (min_big_int a a1) (max_big_int b b1)
| Left b1 :: l' ->
iadd_left l' b
iadd_left l' (max_big_int b b1)
| Right a1 :: _ -> [Right (min_big_int a a1)]
| Any :: _ -> any
......@@ -202,3 +203,20 @@ let negat =
let sub l1 l2 =
add l1 (negat l2)
(*
let dump s i =
let ppf = Format.std_formatter in
Format.fprintf ppf "%s = [ " s;
List.iter (fun x -> x ppf; Format.fprintf ppf " ") (print i);
Format.fprintf ppf "] "
let diff i1 i2 =
let ppf = Format.std_formatter in
Format.fprintf ppf "Intervals.diff.";
dump "i1" i1;
dump "i2" i2;
dump "~i1|i2" (cup (neg i1) i2);
Format.fprintf ppf "@\n";
diff i1 i2
*)
......@@ -49,6 +49,7 @@ let star t = Types.descr (star_node (Types.cons t))
let plus t = let t = Types.cons t in Types.times t (star_node t)
let string = star (Types.Char.any)
(* Mmmmh, it may be faster to add pi1(rect) and iterate over pi2(rect) ... ? *)
let approx t =
let memo = ref H.empty in
let res = ref Types.empty in
......@@ -63,3 +64,33 @@ let approx t =
!res
let map_tree f seq =
let memo = ref H.empty in
let rec aux t =
(* Printf.eprintf "A"; flush stderr; *)
try H.find t !memo
with Not_found ->
let v = V.forward () in
memo := H.add t v !memo;
let v' = mapping descr_aux t (V.ty nil_type) in
V.define v v';
v
and descr_aux t v =
let (result,residual) = f t in
let f2 (attr,child) = V.times (V.ty attr) (aux child) in
let f1 (tag,x) =
let x = V.cup (List.map f2 (Types.Product.get x)) in
V.xml (V.ty tag) x in
let iter = List.map f1 (Types.Product.get ~kind:`XML residual) in
let resid = Types.Product.other ~kind:`XML residual in
let iter = if Types.is_empty resid then iter else V.ty resid :: iter in
let result = aux_concat result v in
if iter = [] then result else
V.cup [V.times (V.cup iter) v; result ]
in
let d = Types.descr (V.solve (aux seq)) in
(* Printf.eprintf "Done."; flush stderr; *)
(* Format.fprintf Format.std_formatter "%a\n" Types.Print.print_descr d; *)
d
(* TODO: avoid flushing the memo between calls to mapping inside map_tree *)
......@@ -8,6 +8,9 @@ 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 map_tree:
(Types.descr -> Types.descr * Types.descr) -> Types.descr -> Types.descr
(* input type -> (result, residual) *) (* sequence type *)
val star: Types.descr -> Types.descr
(* For a type t, returns [t*] *)
......
......@@ -172,13 +172,6 @@ let diff x y =
absent= x.absent && not y.absent;
}
let count = ref 0
let make () = incr count; { id = !count; descr = empty }
let define n d = n.descr <- d
let cons d = incr count; { id = !count; descr = d }
let descr n = n.descr
let internalize n = n
let id n = n.id
let rec compare_rec r1 r2 =
if r1 == r2 then 0
......@@ -288,7 +281,8 @@ let equal_descr a b =
(a.absent == b.absent)
let compare_descr a b =
let c = compare a.atoms b.atoms in if c <> 0 then c
if a == b then 0
else let c = Atoms.compare a.atoms b.atoms in if c <> 0 then c
else let c = compare a.chars b.chars in if c <> 0 then c
else let c = compare a.ints b.ints in if c <> 0 then c
else let c = BoolPair.compare a.times b.times in if c <> 0 then c
......@@ -344,6 +338,7 @@ let hash_descr a =
let accu = if a.absent then accu+5 else accu in
accu
module DescrHash =
Hashtbl.Make(
struct
......@@ -353,6 +348,25 @@ module DescrHash =
end
)
let hash_cons = DescrHash.create 17000
let count = ref 0
let make () = incr count; { id = !count; descr = empty }
let define n d =
(* DescrHash.add hash_cons d n; *)
n.descr <- d
let cons d =
(* try DescrHash.find hash_cons d with Not_found ->
incr count; let n = { id = !count; descr = d } in
DescrHash.add hash_cons d n; n *)
incr count; { id = !count; descr = d }
let descr n = n.descr
let internalize n = n
let id n = n.id
let print_descr = ref (fun _ _ -> assert false)
let neg x = diff any x
......@@ -461,7 +475,7 @@ let rec iter_s s f = function
let set s =
s.status <- NEmpty;
notify s.notify;
(* s.notify <- Nothing; *)
s.notify <- Nothing;
raise NotEmpty
let rec big_conj f l n =
......@@ -502,14 +516,17 @@ and slot d =
s
and check_times (left,right) s =
(* Printf.eprintf "[%i]" (List.length right);
flush stderr; *)
let rec aux accu1 accu2 right s = match right with
| (t1,t2)::right ->
if trivially_empty (cap_t accu1 t1) ||
trivially_empty (cap_t accu2 t2) then
aux accu1 accu2 right s
else
trivially_empty (cap_t accu2 t2) then (
aux accu1 accu2 right s )
else (
let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 right) s;
let accu2' = diff_t accu2 t2 in guard accu2' (aux accu1 accu2' right) s
)
| [] -> set s
in
let (accu1,accu2) = cap_product left in
......@@ -559,11 +576,13 @@ and check_record (labels,(oleft,left),rights) s =
let is_empty d =
(* Printf.eprintf "is_empty: start\n"; flush stderr; *)
let s = slot d in
List.iter
(fun s' -> if s'.status = Maybe then s'.status <- Empty; s'.notify <- Nothing)
!marks;
marks := [];
(* Printf.eprintf "is_empty: done\n"; flush stderr; *)
s.status = Empty
......@@ -988,7 +1007,7 @@ let () = print_descr := Print.print_descr
module Positive =
struct
type rhs = [ `Type of descr | `Cup of v list | `Times of v * v ]
type rhs = [ `Type of descr | `Cup of v list | `Times of v * v | `Xml of v * v ]
and v = { mutable def : rhs; mutable node : node option }
......@@ -1001,6 +1020,7 @@ struct
| `Cup vl ->
List.fold_left (fun acc v -> cup acc (make_descr seen v)) empty vl
| `Times (v1,v2) -> times (make_node v1) (make_node v2)
| `Xml (v1,v2) -> xml (make_node v1) (make_node v2)
and make_node v =
match v.node with
......@@ -1018,6 +1038,7 @@ struct
let ty d = cons (`Type d)
let cup vl = cons (`Cup vl)
let times d1 d2 = cons (`Times (d1,d2))
let xml d1 d2 = cons (`Xml (d1,d2))
let define v1 v2 = def v1 (`Cup [v2])
let solve v = internalize (make_node v)
......@@ -1044,7 +1065,7 @@ type t =
| Record of (bool * (label * t) list)
| Fun of (node * node) list
| Other
exception FoundSampleRecord of bool * (label * t) list
exception FoundSampleRecord of bool * (label * t) list
let rec sample_rec memo d =
if (Assumptions.mem d memo) || (is_empty d) then raise Not_found
......@@ -1154,6 +1175,8 @@ let get x = try sample_rec Assumptions.empty x with Not_found -> Other
| Atom a -> Atoms.print_v ppf a
| Char c -> Chars.print_v ppf c
| Pair (x1,x2) -> Format.fprintf ppf "(%a,%a)" print x1 print x2
| Xml (Atom tag, Pair (attr, child)) ->
Format.fprintf ppf "<%s>%a" (Atoms.value tag) (*print attr*) print child
| Xml (x1,x2) -> Format.fprintf ppf "XML(%a,%a)" print x1 print x2
| Record (o,r) ->
Format.fprintf ppf "{ %a%s }"
......
......@@ -62,6 +62,7 @@ sig
val ty: descr -> v
val cup: v list -> v
val times: v -> v -> v
val xml: v -> v -> v
val solve: v -> node
end
......
......@@ -36,12 +36,15 @@ and texpr' =
| Op of string * texpr list
| Match of texpr * branches
| Map of texpr * branches
| Ttree of texpr * branches
| RemoveField of texpr * label
| Dot of texpr * label
(* Exception *)
| Try of texpr * branches
| MatchFail (* internal usage *)
and abstr = {
fun_name : id option;
fun_iface : (Types.descr * Types.descr) list;
......
......@@ -512,6 +512,12 @@ let rec expr loc' glb { loc = loc; descr = d } =
let (fv1,e) = expr loc glb e
and (fv2,b) = branches loc glb b in
(Fv.cup fv1 fv2, Typed.Map (e, b))
| Ttree (e,b) ->
let b = b @ [ (mknoloc (Internal Types.any)), mknoloc MatchFail ] in
let (fv1,e) = expr loc glb e
and (fv2,b) = branches loc glb b in
(Fv.cup fv1 fv2, Typed.Ttree (e, b))
| MatchFail -> (Fv.empty, Typed.MatchFail)
| Try (e,b) ->
let (fv1,e) = expr loc glb e
and (fv2,b) = branches loc glb b in
......@@ -561,6 +567,8 @@ let int_cup_record = Types.cup Types.Int.any Types.Record.any
type env = Types.descr Env.t
let match_fail = ref Types.empty
open Typed
let warning loc msg =
......@@ -775,14 +783,27 @@ and compute_type' loc env = function
| Op (op, el) ->
let args = List.map (fun e -> (e.exp_loc, compute_type env e)) el in
type_op loc op args
| Map (e,b) ->
let t = compute_type env e in
Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t
| Ttree (e,b) ->
let t = type_check env e Sequence.any true in
let r =
Sequence.map_tree
(fun t ->
let res = type_check_branches loc env t b Sequence.any true in
let resid = !match_fail in
match_fail := Types.empty;
(res,resid)
) t
in
Printf.eprintf "Ttree typed.\n"; flush stderr;
r
(* We keep these cases here to allow comparison and benchmarking ...
Just comment the corresponding cases in type_check' to
activate these ones.
*)
| Map (e,b) ->
let t = compute_type env e in
Sequence.map (fun t -> type_check_branches loc env t b Types.any true) t
| Pair (e1,e2) ->
let t1 = compute_type env e1
and t2 = compute_type env e2 in
......@@ -803,6 +824,9 @@ and type_check_branches loc env targ brs constr precise =
and branches_aux loc env targ tres constr precise = function
| [] -> raise_loc loc (NonExhaustive targ)
| { br_body = { exp_descr = MatchFail } } :: _ ->
match_fail := Types.cup !match_fail targ;
tres
| b :: rem ->
let p = b.br_pat in
let acc = Types.descr (Patterns.accept p) in
......
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