Commit a9c835af authored by Pietro Abate's avatar Pietro Abate

[r2005-07-12 15:37:26 by afrisch] Empty log message

Original author: afrisch
Date: 2005-07-12 15:37:27+00:00
parent d63e2af2
......@@ -157,6 +157,20 @@ let rec print_exn ppf = function
Format.fprintf ppf "Collision on namespaces hash: %a, %a"
U.print ns1
U.print ns2
| Sequence.Error (Sequence.CopyTag (t,expect)) ->
Format.fprintf ppf "Tags in %a will be copied, but only %a are allowed.@.Counter-example:%a@."
Types.Print.print t
Types.Print.print expect
Sample.print (Sample.get (Types.diff t expect))
| Sequence.Error (Sequence.CopyAttr (t,expect)) ->
Format.fprintf ppf "Attributes in %a will be copied, but only %a are allowed.@.Counter-example:%a@."
Types.Print.print t
Types.Print.print expect
Sample.print (Sample.get (Types.diff t expect))
| Sequence.Error (Sequence.UnderTag (t,exn)) ->
Format.fprintf ppf "Under tag %a:@." Types.Print.print t;
print_exn ppf exn
| exn ->
(* raise exn *)
Format.fprintf ppf "%a@." print_protect (Printexc.to_string exn)
......
include "../web/xhtml-strict.cd";;
let fun f (x : Xhtml) : [ Xhtml ] =
xtransform [ x ] with <a>t -> [];;
let fun g (x : Xhtml) : [ Xhtml ] =
xtransform [ x ] with <a>t -> [ <b>t ];;
type T = <a>[ <b>[] T* <b>[] ];;
type S = <a>[ <x>[] S* <x>[] ];;
type T = <a>[ <b>[] T* <b>[] <z>[] ];;
type S = <a>[ <x>[] S* <x>[] <z>[] ];;
let fun f (x : [ T ]) : [ S ] =
xtransform x with <b>_ -> [ <x>[] ];;
let x = f [ <a>[ <b>[] <b>[] ] ];;
(*fun (x : Xhtml) : [Xhtml] = xtransform [x] with <h1>s -> [ ];;*)
(*let x : Xhtml =
<html>[ <head>[ <object>[ <p>[ <a>[ <map id="">[] ] ] ] <title>[] ]
<body>[] ]
*)
xtransform x with <b>_ -> [ [ <x>[] ] ]
type error =
| CopyTag of Types.t * Types.t
| CopyAttr of Types.t * Types.t
| UnderTag of Types.t * exn
exception Error of error
let nil_atom = Atoms.V.mk_ascii "nil"
let nil_type = Types.atom (Atoms.atom nil_atom)
let nil_node = Types.cons nil_type
......@@ -9,6 +16,7 @@ let decompose t =
module V = Types.Positive
module H = Map.Make(Types)
module H2 = Map.Make(Custom.Pair(Types)(Types))
let mapping f t queue =
let memo = ref H.empty in
......@@ -101,23 +109,54 @@ let approx t =
aux t;
!res
let precise = ref true
let map_tree f seq =
let memo = ref H.empty in
let rec aux t =
try H.find t !memo
let map_tree cstr f seq =
let memo = ref H2.empty in
let rec aux cstr t =
let x = (cstr,t) in
try H2.find x !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
memo := H2.add x v !memo;
let v' = mapping (descr_aux cstr) 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
and descr_aux cstr t v =
let cstr0 =
if !precise then Types.Product.normal ~kind:`XML cstr
else [] in
let cstr_tag =
if !precise then Types.Product.pi1 cstr0
else Types.any in
let (result,residual) = f (star cstr) t in
let f2 cstr_attr cstr1 (attr,child) =
let cstr_sub =
if !precise then (
if not (Types.subtype attr cstr_attr) then
raise (Error (CopyAttr (attr,cstr_attr)));
approx (Types.Product.constraint_on_2 cstr1 attr))
else Types.any in
V.times (V.ty attr) (aux cstr_sub 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 cstr1 =
if !precise then (
if not (Types.subtype tag cstr_tag) then
raise (Error (CopyTag (tag,cstr_tag)));
Types.Product.normal
(Types.Product.constraint_on_2 cstr0 tag))
else [] in
let cstr_attr =
if !precise then Types.Product.pi1 cstr1
else Types.any in
try
let x = V.cup (List.map (f2 cstr_attr cstr1) (Types.Product.get x)) in
V.xml (V.ty tag) x
with exn ->
raise (Error (UnderTag (tag,exn)))
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
......@@ -125,7 +164,8 @@ let map_tree f seq =
if iter = [] then result else
V.cup [V.times (V.cup iter) v; result ]
in
Types.descr (V.solve (aux seq))
let cstr = if !precise then approx cstr else Types.any in
Types.descr (V.solve (aux cstr seq))
let map_tree_mono domain seq =
let inp = ref Types.empty in
......
type error =
| CopyTag of Types.t * Types.t
| CopyAttr of Types.t * Types.t
| UnderTag of Types.t * exn
exception Error of error
val nil_type: Types.t
val nil_node: Types.Node.t
val nil_atom: Atoms.V.t
......@@ -15,11 +21,16 @@ val map: (Types.t -> Types.t) -> Types.t -> Types.t
val map_tree:
(Types.t -> Types.t * Types.t) -> Types.t -> Types.t
(* input type -> (result, residual) *) (* sequence type *)
Types.t -> (Types.t -> Types.t -> Types.t * Types.t) -> Types.t -> Types.t
(* maximal output type -> input type -> (result, residual) *)
(* sequence type *)
val map_mono: Types.t -> Types.t list * (Types.t list -> Types.t)
val map_tree_mono: Types.t -> Types.t -> Types.t * Types.t list * (Types.t list -> Types.t)
(* Arguments: domain of all branches, input type.
Results: input type for all branches, all the individual input types,
the function to call when all the individual output types have been
computed *)
val star: Types.t -> Types.t
(* For a type t, returns [t*] *)
......
......@@ -936,12 +936,15 @@ and type_check' loc env e constr precise = match e with
| Xtrans (e,b) ->
let t = type_check env e Sequence.any true in
let t =
Sequence.map_tree
(fun t ->
let resid = Types.diff t b.br_accept in
let res = type_check_branches loc env t b Sequence.any true in
(res,resid)
) t in
try
Sequence.map_tree constr
(fun cstr t ->
let resid = Types.diff t b.br_accept in
let res = type_check_branches loc env t b cstr true in
(res,resid)
) t
with (Sequence.Error _) as exn -> raise_loc loc exn
in
verify loc t constr
| Validate (e, t, _) ->
......
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