Commit 78448cfb authored by Pietro Abate's avatar Pietro Abate
Browse files

[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 ca2d864c
......@@ -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
......
......@@ -33,321 +33,51 @@ module V = struct
end
module SymbolSet = struct
module SList = SortedList.Make(Symbol)
type t = Finite of SList.t | Cofinite of SList.t
module SymbolSet = SortedList.FiniteCofinite(Symbol)
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 rec iter_sep sep f = function
| [] -> ()
| [ h ] -> f h
| h :: t -> f h; sep (); iter_sep sep f t
(* Atom
bla:* bla:x
:* :x *)
let print ns ppf = function
| Finite l ->
iter_sep
(fun () -> Format.fprintf ppf " |@ ")
(fun x -> V.print_quote ppf (ns,x)) l
| Cofinite t ->
Format.fprintf ppf "@[`%a" V.print_any_in_ns ns;
List.iter (fun x -> Format.fprintf ppf " \@ %a" V.print_quote (ns,x)) t;
Format.fprintf ppf "@]"
end
module T0 = SortedList.Make(Ns)
module TMap = T0.MakeMap(SymbolSet)
module T = T0.Map
type t = Finite of TMap.t | Cofinite of TMap.t
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 print_tag = function
| Finite l ->
(match T.get l with
| [ns, SymbolSet.Finite [a]] ->
Some (fun ppf -> V.print ppf (ns,a))
| [ns, SymbolSet.Cofinite []] ->
Some (fun ppf -> Format.fprintf ppf "%a" V.print_any_in_ns ns)
| _ -> None)
| Cofinite l ->
(match T.get l with
| [] ->
Some (fun ppf -> Format.fprintf ppf "_")
| _ -> None)
let symbol_set ns = function
| Finite s ->
(try T.assoc ns s with Not_found -> SymbolSet.empty)
| Cofinite s ->
(try SymbolSet.neg (T.assoc ns s) with Not_found -> SymbolSet.any)
let contains (ns,x) = function
| Finite s ->
(try SymbolSet.contains x (T.assoc ns s) with Not_found -> false)
| Cofinite s ->
(try not (SymbolSet.contains x (T.assoc ns s)) with Not_found -> true)
let disjoint s t =
is_empty (cap t s) (* TODO: OPT *)
let print = function
| Finite l ->
List.map (fun (ns,s) ppf -> SymbolSet.print ns ppf s) (T.get l)
| Cofinite l ->
match T.get l with
| [] -> [ fun ppf -> Format.fprintf ppf "Atom" ]
| l ->
[ fun ppf ->
Format.fprintf ppf "Atom";
List.iter
(fun (ns,s) ->
Format.fprintf ppf " \@ (%a)" (SymbolSet.print ns) s)
l ]
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
let equal t1 t2 =
compare t1 t2 = 0
(* Optimize lookup:
- decision tree
- merge adjacent segment with same result
*)
(*
type 'a map = v -> 'a
let rec mk_map l v =
match l with
| [] -> assert false
| (x,y) :: rem -> if (contains v x) then y else mk_map rem v
let get_map v m = m v
*)
(* Patricia trees; code adapted from http://www.lri.fr/~filliatr/ftp/ocaml/misc/ptmap.ml *)
module IMap = struct
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 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)