Commit 598033dc authored by Pietro Abate's avatar Pietro Abate

[r2004-01-20 16:12:13 by afrisch] Debut des types abstraits

Original author: afrisch
Date: 2004-01-20 16:12:15+00:00
parent 9cf38918
......@@ -123,7 +123,7 @@ help:
# Source directories
DIRS = misc parser schema typing types compile runtime driver query
DIRS = misc parser schema typing types compile runtime driver query ocaml_iface
CLEAN_DIRS = $(DIRS) tools tests
# Objects to build
......@@ -132,7 +132,7 @@ OBJECTS = \
misc/stats.cmo \
misc/serialize.cmo misc/custom.cmo \
misc/state.cmo misc/pool.cmo misc/encodings.cmo misc/bool.cmo \
misc/pretty.cmo misc/ns.cmo misc/inttbl.cmo \
misc/pretty.cmo misc/ns.cmo misc/inttbl.cmo misc/imap.cmo \
\
types/sortedList.cmo types/boolean.cmo types/ident.cmo \
types/intervals.cmo types/chars.cmo types/atoms.cmo \
......@@ -165,6 +165,8 @@ OBJECTS = \
CQL_OBJECTS= query/query.cmo query/query_parse.cmo
CQL_OBJECTS_RUN = query/query_run.cmo
OCAML_IFACE_OBJECTS = $(OBJECTS) ocaml_iface/cduce_from_ocaml.cmo
VALIDATE_OBJECTS := $(shell for o in $(OBJECTS); do echo $$o; if [ "$$o" = "schema/schema_parser.cmo" ]; then exit 0; fi; done) # all objects until schema_parser.cmo
CDUCE = $(OBJECTS) $(CQL_OBJECTS) driver/run.cmo $(CQL_OBJECTS_RUN)
......@@ -184,12 +186,16 @@ INCLUDES = $(DIRS:%=-I %)
cduce: $(CDUCE:.cmo=.$(EXTENSION))
$(LINK) $(INCLUDES) -o $@ $^ $(EXTRA_LINK_OPTS)
cduce_packed.cma: $(OBJECTS)
$(CAMLC) -o cduce_all.cmo -pack $(OBJECTS)
$(CAMLC) -a -linkpkg -o cduce_packed.cma gramlib.cma cduce_all.cmo
run_ocaml_cduce_packed: cduce_packed.cma
ocaml cduce_packed.cma
cduce_from_ocaml.cma: $(OCAML_IFACE_OBJECTS)
$(CAMLC) -o cduce_from_ocaml_pack.cmo -pack $(OCAML_IFACE_OBJECTS)
$(CAMLC) -a -o cduce_from_ocaml.cma -linkpkg gramlib.cma camlp4o.cma cduce_from_ocaml_pack.cmo
cDuce_all.cma: $(OBJECTS)
$(CAMLC) -o cDuce_all.cmo -pack $(OBJECTS)
$(CAMLC) -a -o cDuce_all.cma -linkpkg gramlib.cma cDuce_all.cmo
#run_ocaml_cduce_packed: cduce_packed.cma
# ocaml cduce_packed.cma
webiface: $(WEBIFACE:.cmo=.$(EXTENSION))
$(LINK) -verbose $(INCLUDES) -o $@ $^ -ccopt -static
......
......@@ -22,6 +22,8 @@ misc/ns.cmx: misc/q_symbol.cmo misc/custom.cmx misc/encodings.cmx misc/pool.cmx
misc/serialize.cmx misc/state.cmx misc/ns.cmi
misc/inttbl.cmo: misc/q_symbol.cmo misc/inttbl.cmi
misc/inttbl.cmx: misc/q_symbol.cmo misc/inttbl.cmi
misc/imap.cmo: misc/q_symbol.cmo misc/imap.cmi
misc/imap.cmx: misc/q_symbol.cmo misc/imap.cmi
types/sortedList.cmo: misc/q_symbol.cmo misc/custom.cmo misc/serialize.cmi types/sortedList.cmi
types/sortedList.cmx: misc/q_symbol.cmo misc/custom.cmx misc/serialize.cmx types/sortedList.cmi
types/boolean.cmo: misc/q_symbol.cmo misc/custom.cmo types/sortedList.cmi types/boolean.cmi
......@@ -34,10 +36,10 @@ types/intervals.cmo: misc/q_symbol.cmo misc/serialize.cmi types/intervals.cmi
types/intervals.cmx: misc/q_symbol.cmo misc/serialize.cmx types/intervals.cmi
types/chars.cmo: misc/q_symbol.cmo misc/custom.cmo types/chars.cmi
types/chars.cmx: misc/q_symbol.cmo misc/custom.cmx types/chars.cmi
types/atoms.cmo: misc/q_symbol.cmo misc/custom.cmo misc/encodings.cmi misc/ns.cmi misc/pool.cmi \
misc/serialize.cmi types/sortedList.cmi types/atoms.cmi
types/atoms.cmx: misc/q_symbol.cmo misc/custom.cmx misc/encodings.cmx misc/ns.cmx misc/pool.cmx \
misc/serialize.cmx types/sortedList.cmx types/atoms.cmi
types/atoms.cmo: misc/q_symbol.cmo misc/custom.cmo misc/encodings.cmi misc/imap.cmi misc/ns.cmi \
misc/pool.cmi types/sortedList.cmi types/atoms.cmi
types/atoms.cmx: misc/q_symbol.cmo misc/custom.cmx misc/encodings.cmx misc/imap.cmx misc/ns.cmx \
misc/pool.cmx types/sortedList.cmx types/atoms.cmi
types/normal.cmo: misc/q_symbol.cmo types/normal.cmi
types/normal.cmx: misc/q_symbol.cmo types/normal.cmi
types/types.cmo: misc/q_symbol.cmo types/atoms.cmi misc/bool.cmi types/chars.cmi \
......@@ -108,8 +110,8 @@ schema/schema_parser.cmx: misc/q_symbol.cmo misc/encodings.cmx types/intervals.c
runtime/value.cmx schema/schema_parser.cmi
parser/location.cmo: misc/q_symbol.cmo parser/location.cmi
parser/location.cmx: misc/q_symbol.cmo parser/location.cmi
parser/url.cmo: misc/q_symbol.cmo parser/location.cmi parser/url.cmi
parser/url.cmx: misc/q_symbol.cmo parser/location.cmx parser/url.cmi
parser/url.cmo: misc/q_symbol.cmo parser/url.cmi
parser/url.cmx: misc/q_symbol.cmo parser/url.cmi
parser/ulexer.cmo: misc/q_symbol.cmo parser/ulexer.cmi
parser/ulexer.cmx: misc/q_symbol.cmo parser/ulexer.cmi
parser/ast.cmo: misc/q_symbol.cmo types/builtin_defs.cmi types/chars.cmi types/ident.cmo \
......@@ -182,12 +184,14 @@ runtime/eval.cmx: misc/q_symbol.cmo types/builtin_defs.cmx types/ident.cmx compi
types/patterns.cmx runtime/run_dispatch.cmx schema/schema_common.cmx \
schema/schema_types.cmi schema/schema_validator.cmx types/sequence.cmx \
typing/typer.cmx types/types.cmx runtime/value.cmx runtime/eval.cmi
compile/compile.cmo: misc/q_symbol.cmo parser/ast.cmo types/ident.cmo compile/lambda.cmo \
parser/location.cmi types/patterns.cmi misc/serialize.cmi \
typing/typed.cmo typing/typer.cmi types/types.cmi compile/compile.cmi
compile/compile.cmx: misc/q_symbol.cmo parser/ast.cmx types/ident.cmx compile/lambda.cmx \
parser/location.cmx types/patterns.cmx misc/serialize.cmx \
typing/typed.cmx typing/typer.cmx types/types.cmx compile/compile.cmi
compile/compile.cmo: misc/q_symbol.cmo parser/ast.cmo runtime/eval.cmi types/ident.cmo \
compile/lambda.cmo parser/location.cmi types/patterns.cmi \
misc/serialize.cmi typing/typed.cmo typing/typer.cmi types/types.cmi \
compile/compile.cmi
compile/compile.cmx: misc/q_symbol.cmo parser/ast.cmx runtime/eval.cmx types/ident.cmx \
compile/lambda.cmx parser/location.cmx types/patterns.cmx \
misc/serialize.cmx typing/typed.cmx typing/typer.cmx types/types.cmx \
compile/compile.cmi
compile/operators.cmo: misc/q_symbol.cmo misc/custom.cmo runtime/eval.cmi compile/lambda.cmo \
parser/location.cmi misc/pool.cmi typing/typer.cmi types/types.cmi \
runtime/value.cmi compile/operators.cmi
......@@ -218,14 +222,14 @@ driver/cduce.cmo: misc/q_symbol.cmo parser/ast.cmo types/builtin.cmi compile/com
misc/encodings.cmi runtime/eval.cmi runtime/explain.cmi types/ident.cmo \
driver/librarian.cmi parser/location.cmi misc/ns.cmi parser/parser.cmi \
types/patterns.cmi types/sample.cmi schema/schema_common.cmi \
misc/state.cmi typing/typed.cmo typing/typer.cmi types/types.cmi \
parser/ulexer.cmi runtime/value.cmi driver/cduce.cmi
misc/state.cmi typing/typer.cmi types/types.cmi parser/ulexer.cmi \
runtime/value.cmi driver/cduce.cmi
driver/cduce.cmx: misc/q_symbol.cmo parser/ast.cmx types/builtin.cmx compile/compile.cmx \
misc/encodings.cmx runtime/eval.cmx runtime/explain.cmx types/ident.cmx \
driver/librarian.cmx parser/location.cmx misc/ns.cmx parser/parser.cmx \
types/patterns.cmx types/sample.cmx schema/schema_common.cmx \
misc/state.cmx typing/typed.cmx typing/typer.cmx types/types.cmx \
parser/ulexer.cmx runtime/value.cmx driver/cduce.cmi
misc/state.cmx typing/typer.cmx types/types.cmx parser/ulexer.cmx \
runtime/value.cmx driver/cduce.cmi
query/query.cmo: misc/q_symbol.cmo parser/ast.cmo types/atoms.cmi types/builtin_defs.cmi \
types/chars.cmi types/ident.cmo types/intervals.cmi parser/location.cmi \
parser/parser.cmi types/types.cmi query/query.cmi
......@@ -291,7 +295,8 @@ runtime/print_xml.cmi: misc/q_symbol.cmo misc/ns.cmi runtime/value.cmi
runtime/eval.cmi: misc/q_symbol.cmo types/ident.cmo compile/lambda.cmo types/types.cmi \
runtime/value.cmi
compile/compile.cmi: misc/q_symbol.cmo parser/ast.cmo types/ident.cmo compile/lambda.cmo \
misc/serialize.cmi typing/typed.cmo typing/typer.cmi types/types.cmi
misc/serialize.cmi typing/typed.cmo typing/typer.cmi types/types.cmi \
runtime/value.cmi
compile/operators.cmi: misc/q_symbol.cmo misc/custom.cmo parser/location.cmi misc/serialize.cmi \
typing/typer.cmi types/types.cmi runtime/value.cmi
types/builtin.cmi: misc/q_symbol.cmo typing/typer.cmi
......
......@@ -187,6 +187,7 @@ let rec load id =
cu.depends <- List.map (fun (id,_) -> C.mk id) depend;
cu.digest <- Some dig;
C.Tbl.add tbl id cu;
Typer.register_types id cu.typing;
cu
and load_check id exp =
......
(* Patricia trees; code adapted from http://www.lri.fr/~filliatr/ftp/ocaml/misc/ptmap.ml *)
type 'a t =
| Empty
| Leaf of int * 'a
| Branch of int * int * 'a t * 'a t
type 'a s =
| DError
| DReturn of 'a
| DLeaf of int * 'a * 'a
| DBranch of int * int * 'a s * 'a s
let empty = Empty
let return x = DReturn x
let zero_bit k m = (k land m) == 0
let lowest_bit x = x land (-x)
let branching_bit p0 p1 = lowest_bit (p0 lxor p1)
let mask p m = p land (m-1)
let match_prefix k p m = (mask k m) == p
let rec prepare_def y = function
| Empty -> DReturn y
| Leaf (k,x) -> DLeaf (k,x,y)
| Branch (p,m,t0,t1) ->
DBranch (p,m,prepare_def y t0, prepare_def y t1)
let rec prepare_nodef = function
| Empty -> DError
| Leaf (k,x) -> DReturn x
| Branch (p,m,t0,t1) ->
match (prepare_nodef t0, prepare_nodef t1) with
| (DReturn x0, DReturn x1) when x0 == x1 -> DReturn x0
| (t0,t1) -> DBranch (p,m,t0,t1)
let prepare def y =
match def with
| None -> prepare_nodef y
| Some def -> prepare_def def y
let rec find k = function
| DError -> assert false
| DReturn y -> y
| DLeaf (j,x,y) -> if k == j then x else y
| DBranch (_, m, l, r) -> find k (if zero_bit k m then l else r)
let join p0 t0 p1 t1 =
let m = branching_bit p0 p1 in
if zero_bit p0 m
then Branch (mask p0 m, m, t0, t1)
else Branch (mask p0 m, m, t1, t0)
let rec add k x = function
| Empty -> Leaf (k,x)
| Leaf (j,_) as t ->
if j == k then Leaf (k,x) else join k (Leaf (k,x)) j t
| Branch (p,m,t0,t1) as t ->
if match_prefix k p m
then
if zero_bit k m
then Branch (p, m, add k x t0, t1)
else Branch (p, m, t0, add k x t1)
else
join k (Leaf (k,x)) p t
let rec dump f ppf = function
| DError -> Format.fprintf ppf "Error"
| DReturn x -> Format.fprintf ppf "Return %a" f x
| DLeaf(j,x,y) -> Format.fprintf ppf "Leaf(%i,%a,%a)" j f x f y
| DBranch (p,m,t0,t1) ->
Format.fprintf ppf "B(%i,%i,%a,%a)" p m (dump f) t0 (dump f) t1
type 'a t
type 'a s
val add: int -> 'a -> 'a t -> 'a t
val empty: 'a t
val return: 'a -> 'a s
val prepare: 'a option -> 'a t -> 'a s
val find: int -> 'a s -> 'a
val dump : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a s -> unit
......@@ -270,6 +270,7 @@ EXTEND
[ op = [ IDENT "flatten"
| IDENT "load_xml"
| IDENT "load_file" | IDENT "load_file_utf8"
| IDENT "float_of"
| IDENT "getenv"
| IDENT "load_html"
| IDENT "print_xml" | IDENT "print_xml_utf8"
......
......@@ -167,6 +167,9 @@ and run_disp_kind actions v =
| Abstraction2 (_,iface,_) ->
run_disp_basic v (fun t -> Types.Arrow.check_iface iface t)
actions.basic
| Abstract (abs,_) ->
run_disp_basic v (fun t -> Types.Abstract.contains abs (Types.get_abstract t))
actions.basic
| Absent ->
run_disp_basic v (fun t -> Types.Record.has_absent t) actions.basic
| Concat (_,_) as v -> run_disp_kind actions (Value.normalize v)
......
......@@ -10,6 +10,7 @@ type t =
| Char of Chars.V.t
| Abstraction of (Types.descr * Types.descr) list * (t -> t)
| Abstraction2 of t array * (Types.t * Types.t) list * Lambda.branches
| Abstract of Types.Abstract.V.t
| String_latin1 of int * int * string * t
| String_utf8 of Utf8.uindex * Utf8.uindex * Utf8.t * t
| Concat of t * t
......@@ -236,6 +237,10 @@ let rec print ppf v =
(Utf8.get_idx i) (Utf8.get_idx j) (Utf8.get_str s) print q
| Concat (x,y) ->
Format.fprintf ppf "<concat:%a;%a>" print x print y
| Abstract ((cu,id),_) ->
Format.fprintf ppf "<abstract=%a:%a>"
Utf8.print (Types.CompUnit.value cu)
Utf8.print (Id.value id)
| Absent ->
Format.fprintf ppf "<[absent]>"
| Delayed x ->
......@@ -329,6 +334,10 @@ let dump_xml ppf v =
| Abstraction2 _ ->
Format.fprintf ppf "@[<hv1>";
Format.fprintf ppf "<abstraction2 />@]"
| Abstract ((cu,id),_) ->
Format.fprintf ppf "<abstract><unit>%a</unit><type>%a</type></abstract>"
Utf8.print (Types.CompUnit.value cu)
Utf8.print (Id.value id)
| String_latin1 (_, _, s, v) ->
Format.fprintf ppf "@[<hv1>";
Format.fprintf ppf "<string_latin1>@,%s@,</string_latin1>@," s;
......@@ -374,6 +383,10 @@ let rec compare x y =
| Abstraction2 (_,_,_), _
| _, Abstraction2 (_,_,_) ->
raise (CDuceExn (string_latin1 "comparing functional values"))
| Abstract ((cu1,id1),v1), Abstract ((cu2,id2),v2) ->
let c = Types.CompUnit.compare cu1 cu2 in if c <> 0 then c
else let c = Id.compare id1 id2 in if c <> 0 then c
else raise (CDuceExn (string_latin1 "comparing abstract values"))
| Absent,_ | _,Absent
| Delayed _, _ | _, Delayed _ -> assert false
| Concat (_,_) as x, y -> eval_lazy_concat x; compare x y
......@@ -422,6 +435,7 @@ let rec compare x y =
| Record _,_ -> -1 | _, Record _ -> 1
| Atom _,_ -> -1 | _, Atom _ -> 1
| Integer _,_ -> -1 | _, Integer _ -> 1
| Abstract _, _ -> -1 | _, Abstract _ -> 1
let iter_xml pcdata_callback other_callback =
let rec aux = function
......
......@@ -11,6 +11,7 @@ type t =
| Char of Chars.V.t
| Abstraction of (Types.descr * Types.descr) list * (t -> t)
| Abstraction2 of t array * (Types.t * Types.t) list * Lambda.branches
| Abstract of Types.Abstract.V.t
(* Derived forms *)
| String_latin1 of int * int * string * t
......
This diff is collapsed.
......@@ -15,7 +15,8 @@ let types =
"Record", Types.Record.any;
"String", string;
"Latin1", string_latin1;
"Bool", bool
"Bool", bool;
"Float", float;
]
let env =
......@@ -223,6 +224,13 @@ unary_op_warning "int_of"
try Value.Integer (Intervals.V.mk (U.get_str s)) (* UTF-8 is ASCII compatible ! *)
with Failure _ -> raise exn_int_of);;
unary_op_cst "float_of"
string float
(fun v ->
let (s,_) = Value.get_string_utf8 v in
try Value.Abstract (float_abs, Obj.repr (float_of_string (U.get_str s)))
with Failure _ -> raise exn_int_of);;
unary_op_cst "atom_of"
string atom
(fun v ->
......
......@@ -60,3 +60,9 @@ let ref_type t =
let get = Types.cons (Types.arrow Sequence.nil_node t)
and set = Types.cons (Types.arrow t Sequence.nil_node) in
Types.record' (false , mk_ref ~get ~set)
let float_abs =
Types.CompUnit.pervasives, Ident.Id.mk (Encodings.Utf8.mk "float")
let float =
Types.abstract (Types.Abstract.atom float_abs)
......@@ -35,3 +35,6 @@ val time_kind: Types.t
val mk_ref: get:'a -> set:'a -> 'a Ident.label_map
val ref_type: Types.Node.t -> Types.t
val float: Types.t
val float_abs: Types.Abstract.abs
......@@ -791,12 +791,13 @@ struct
AKind
{ basic = basic;
atoms =
Atoms.mk_map (List.map (fun (t,r) -> Types.Atom.get t, r) basic);
Atoms.mk_map (List.map (fun (t,r) -> Types.Atom.get t, r) basic);
chars =
Chars.mk_map (List.map (fun (t,r) -> Types.Char.get t, r) basic);
Chars.mk_map (List.map (fun (t,r) -> Types.Char.get t, r) basic);
prod = prod;
xml = xml;
record = record }
record = record;
}
let combine f (disp,act) =
if Array.length act == 0 then Impossible
......
module type S =
sig
include Custom.T
type elem
external get: t -> elem list = "%identity"
val singleton: elem -> t
val iter: (elem -> unit) -> t -> unit
val filter: (elem -> bool) -> t -> t
val exists: (elem -> bool) -> t -> bool
val fold: ('a -> elem -> 'a) -> 'a -> t -> 'a
val pick: t -> elem option
val length: t -> int
val empty: t
val is_empty: t -> bool
val from_list : elem list -> t
val add: elem -> t -> t
val remove: elem -> t -> t
val disjoint: t -> t -> bool
val cup: t -> t -> t
val split: t -> t -> t * t * t
(* split l1 l2 = (l1 \ l2, l1 & l2, l2 \ l1) *)
val cap: t -> t -> t
val diff: t -> t -> t
val subset: t -> t -> bool
val map: (elem -> elem) -> t -> t
val mem: t -> elem -> bool
module Map: sig
type 'a map
external get: 'a map -> (elem * 'a) list = "%identity"
val empty: 'a map
val iter: ('a -> unit) -> 'a map -> unit
val filter: (elem -> 'a -> bool) -> 'a map -> 'a map
val is_empty: 'a map -> bool
val singleton: elem -> 'a -> 'a map
val assoc_remove: elem -> 'a map -> 'a * 'a map
val remove: elem -> 'a map -> 'a map
val merge: ('a -> 'a -> 'a ) -> 'a map -> 'a map -> 'a map
val cap: ('a -> 'a -> 'a ) -> 'a map -> 'a map -> 'a map
val sub: ('a -> 'a -> 'a ) -> 'a map -> 'a map -> 'a map
val merge_elem: 'a -> 'a map -> 'a map -> 'a map
val union_disj: 'a map -> 'a map -> 'a map
val diff: 'a map -> t -> 'a map
val from_list: ('a -> 'a -> 'a ) -> (elem * 'a) list -> 'a map
val from_list_disj: (elem * 'a) list -> 'a map
val map_from_slist: (elem -> 'a) -> t -> 'a map
val collide: ('a -> 'b -> unit) -> 'a map -> 'b map -> unit
val map: ('a -> 'b) -> 'a map -> 'b map
val mapi: (elem -> 'a -> 'b) -> 'a map -> 'b map
val constant: 'a -> t -> 'a map
val num: int -> t -> int map
val map_to_list: ('a -> 'b) -> 'a map -> 'b list
val mapi_to_list: (elem -> 'a -> 'b) -> 'a map -> 'b list
val assoc: elem -> 'a map -> 'a
val assoc_present: elem -> 'a map -> 'a
val compare: ('a -> 'a -> int) -> 'a map -> 'a map -> int
val hash: ('a -> int) -> 'a map -> int
val equal: ('a -> 'a -> bool) -> 'a map -> 'a map -> bool
end
end
module Make(X : Custom.T) = struct
include Custom.List(X)
let rec check = function
......@@ -434,5 +367,211 @@ end
Map.from_list_disj
(Serialize.Get.list (Serialize.Get.pair X.deserialize Y.deserialize) t)
end
end
module type FiniteCofinite = sig
type elem
type s = private Finite of elem list | Cofinite of elem list
include Custom.T with type t = s
val empty: t
val any: t
val atom: elem -> t
val cup: t -> t -> t
val cap: t -> t -> t
val diff: t -> t -> t
val neg: t -> t
val contains: elem -> t -> bool
val disjoint: t -> t -> bool
val is_empty: t -> bool
end
module FiniteCofinite(X : Custom.T) = struct
type elem = X.t
module SList = Make(X)
type s = Finite of SList.t | Cofinite of SList.t
type t = s
let hash = function
| Finite l -> SList.hash l
| Cofinite l -> 17 * SList.hash l + 1
let compare l1 l2 =
match (l1,l2) with
| Finite l1, Finite l2
| Cofinite l1, Cofinite l2 -> SList.compare l1 l2
| Finite _, Cofinite _ -> -1
| _ -> 1
let equal l1 l2 = compare l1 l2 = 0
let serialize t = function
| Finite s -> Serialize.Put.bool t true; SList.serialize t s
| Cofinite s -> Serialize.Put.bool t false; SList.serialize t s
let deserialize t =
if Serialize.Get.bool t
then Finite (SList.deserialize t)
else Cofinite (SList.deserialize t)
let check = function
| Finite s | Cofinite s -> SList.check s
let dump ppf = function
| Finite s -> Format.fprintf ppf "Finite[%a]" SList.dump s
| Cofinite s -> Format.fprintf ppf "Cofinite[%a]" SList.dump s
let empty = Finite []
let any = Cofinite []
let atom x = Finite [x]
let cup s t =
match (s,t) with
| (Finite s, Finite t) -> Finite (SList.cup s t)
| (Finite s, Cofinite t) -> Cofinite (SList.diff t s)
| (Cofinite s, Finite t) -> Cofinite (SList.diff s t)
| (Cofinite s, Cofinite t) -> Cofinite (SList.cap s t)
let cap s t =
match (s,t) with
| (Finite s, Finite t) -> Finite (SList.cap s t)
| (Finite s, Cofinite t) -> Finite (SList.diff s t)
| (Cofinite s, Finite t) -> Finite (SList.diff t s)
| (Cofinite s, Cofinite t) -> Cofinite (SList.cup s t)
let diff s t =
match (s,t) with
| (Finite s, Cofinite t) -> Finite (SList.cap s t)
| (Finite s, Finite t) -> Finite (SList.diff s t)
| (Cofinite s, Cofinite t) -> Finite (SList.diff t s)
| (Cofinite s, Finite t) -> Cofinite (SList.cup s t)
let neg = function
| Finite s -> Cofinite s
| Cofinite s -> Finite s
let contains x = function
| Finite s -> SList.mem s x
| Cofinite s -> not (SList.mem s x)
let disjoint s t =
match (s,t) with
| (Finite s, Finite t) -> SList.disjoint s t
| (Finite s, Cofinite t) -> SList.subset s t
| (Cofinite s, Finite t) -> SList.subset t s
| (Cofinite s, Cofinite t) -> false
let is_empty = function Finite [] -> true | _ -> false
end
module FiniteCofiniteMap(X : Custom.T)(SymbolSet : FiniteCofinite) =
struct
include Custom.Dummy
module T0 = Make(X)
module TMap = T0.MakeMap(SymbolSet)
module T = T0.Map
type t = Finite of TMap.t | Cofinite of TMap.t
let get = function
| Finite l -> `Finite (T.get l)
| Cofinite l -> `Cofinite (T.get l)
let check = function
| Finite l | Cofinite l -> TMap.check l
let dump ppf = function
| Finite s -> Format.fprintf ppf "Finite[%a]" TMap.dump s
| Cofinite s -> Format.fprintf ppf "Cofinite[%a]" TMap.dump s
let serialize t = function
| Finite s -> Serialize.Put.bool t true; TMap.serialize t s
| Cofinite s -> Serialize.Put.bool t false; TMap.serialize t s
let deserialize t =
if Serialize.Get.bool t
then Finite (TMap.deserialize t)
else Cofinite (TMap.deserialize t)
let empty = Finite T.empty
let any = Cofinite T.empty
let any_in_ns ns = Finite (T.singleton ns SymbolSet.any)
let finite l =
let l =
T.filter
(fun _ x -> match x with SymbolSet.Finite [] -> false | _ -> true)
l in
Finite l
let cofinite l =
let l =
T.filter
(fun _ x -> match x with SymbolSet.Cofinite [] -> false | _ -> true)
l in
Cofinite l
let atom (ns,x) = Finite (T.singleton ns (SymbolSet.atom x))
let cup s t =
match (s,t) with
| (Finite s, Finite t) -> finite (T.merge SymbolSet.cup s t)
| (Finite s, Cofinite t) -> cofinite (T.sub SymbolSet.diff t s)
| (Cofinite s, Finite t) -> cofinite (T.sub SymbolSet.diff s t)
| (Cofinite s, Cofinite t) -> cofinite (T.cap SymbolSet.cap s t)
let cap s t =
match (s,t) with
| (Finite s, Finite t) -> finite (T.cap SymbolSet.cap s t)
| (Finite s, Cofinite t) -> finite (T.sub SymbolSet.diff s t)
| (Cofinite s, Finite t) -> finite (T.sub SymbolSet.diff t s)
| (Cofinite s, Cofinite t) -> cofinite (T.merge SymbolSet.cup s t)
let diff s t =
match (s,t) with
| (Finite s, Cofinite t) -> finite (T.cap SymbolSet.cap s t)
| (Finite s, Finite t) -> finite (T.sub SymbolSet.diff s t)
| (Cofinite s, Cofinite t) -> finite (T.sub SymbolSet.diff t s)
| (Cofinite s, Finite t) -> cofinite (T.merge SymbolSet.cup s t)
let is_empty = function
| Finite l -> T.is_empty l
| _ -> false
let hash = function
| Finite l -> 1 + 17 * (TMap.hash l)
| Cofinite l -> 2 + 17 * (TMap.hash l)
let compare l1 l2 =
match (l1,l2) with
| Finite l1, Finite l2
| Cofinite l1, Cofinite l2 -> TMap.compare l1 l2
| Finite _, Cofinite _ -> -1
| _ -> 1