module Coqast

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@25 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 81 insertions, 4 deletions

diff --git a/lib/coqast.ml b/lib/coqast.ml
new file mode 100644
index 0000000000..b0a825326c
--- /dev/null
+++ b/lib/coqast.ml
@@ -0,0 +1,65 @@
+
+(* $Id$ *)
+
+type loc = int * int
+
+type t =
+  | Node of loc * string * t list
+  | Nvar of loc * string
+  | Slam of loc * string option * t
+  | Num of loc * int
+  | Id of loc * string
+  | Str of loc * string
+  | Path of loc * string list* string
+  | Dynamic of loc * Dyn.t
+
+type the_coq_ast = t
+
+(* Hash-consing *)
+module Hloc = Hashcons.Make(
+  struct
+    type t = loc
+    type u = unit
+    let equal (b1,e1) (b2,e2) = b1=b2 & e1=e2
+    let hash_sub () x = x
+    let hash = Hashtbl.hash
+  end)
+
+module Hast = Hashcons.Make(
+  struct
+    type t = the_coq_ast
+    type u = (the_coq_ast -> the_coq_ast) * ((loc -> loc) * (string -> string))
+    let hash_sub (hast,(hloc,hstr)) = function
+      | Node(l,s,al) -> Node(hloc l, hstr s, List.map hast al)
+      | Nvar(l,s) -> Nvar(hloc l, hstr s)
+      | Slam(l,None,t) -> Slam(hloc l, None, hast t)
+      | Slam(l,Some s,t) -> Slam(hloc l, Some (hstr s), hast t)
+      | Num(l,n) -> Num(hloc l, n)
+      | Id(l,s) -> Id(hloc l, hstr s)
+      | Str(l,s) -> Str(hloc l, hstr s)
+      | Path(l,d,k) -> Path(hloc l, List.map hstr d, hstr k)
+      | Dynamic(l,d) -> Dynamic(hloc l, d)
+    let equal a1 a2 =
+      match (a1,a2) with
+        | (Node(l1,s1,al1), Node(l2,s2,al2)) ->
+            (l1==l2 & s1==s2 & List.length al1 = List.length al2)
+            & List.for_all2 (==) al1 al2
+        | (Nvar(l1,s1), Nvar(l2,s2)) -> l1==l2 & s1==s2
+        | (Slam(l1,None,t1), Slam(l2,None,t2)) -> l1==l2 & t1==t2
+        | (Slam(l1,Some s1,t1), Slam(l2,Some s2,t2)) -> l1==l2 & t1==t2
+        | (Num(l1,n1), Num(l2,n2)) -> l1==l2 & n1=n2
+        | (Id(l1,s1), Id(l2,s2)) -> l1==l2 & s1==s2
+        | (Str(l1,s1),Str(l2,s2)) -> l1==l2 & s1==s2
+        | (Path(l1,d1,k1), Path(l2,d2,k2)) ->
+            (l1==l2 & k1==k2 & List.length d1 = List.length d2)
+            & List.for_all2 (==) d1 d2
+        | _ -> false
+    let hash = Hashtbl.hash
+  end)
+
+let hcons_ast hstr =
+  let hloc = Hashcons.simple_hcons Hloc.f () in
+  let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr) in
+  (hast,hloc)
+
+
diff --git a/lib/util.ml b/lib/util.ml
index 3bac54cf94..95a609378f 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -63,12 +63,22 @@ let parse_section_path s =
 
 (* Lists *)
 
-let intersect l1 l2 = 
+let list_intersect l1 l2 = 
   List.filter (fun x -> List.mem x l2) l1
 
-let subtract l1 l2 =
+let list_unionq l1 l2 = 
+  let rec urec = function
+    | [] -> l2
+    | a::l -> if List.memq a l2 then urec l else a::urec l
+  in 
+  urec l1
+
+let list_subtract l1 l2 =
   if l2 = [] then l1 else List.filter (fun x -> not (List.mem x l2)) l1
 
+let list_subtractq l1 l2 = 
+  if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1
+
 let list_chop n l = 
   let rec chop_aux acc = function
     | (0, l2) -> (List.rev acc, l2)
diff --git a/lib/util.mli b/lib/util.mli
index c5e21f350a..0faf3f2900 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -24,8 +24,10 @@ val parse_section_path : string -> string list * string * string
 
 (* Lists *)
 
-val intersect : 'a list -> 'a list -> 'a list
-val subtract : 'a list -> 'a list -> 'a list
+val list_intersect : 'a list -> 'a list -> 'a list
+val list_unionq : 'a list -> 'a list -> 'a list
+val list_subtract : 'a list -> 'a list -> 'a list
+val list_subtractq : 'a list -> 'a list -> 'a list
 val list_chop : int -> 'a list -> 'a list * 'a list
 val list_tabulate : (int -> 'a) -> int -> 'a list
 val list_assign : 'a list -> int -> 'a -> 'a list