From cf4b0ccb2b5d494f9c7856c7a849ca60ebf857cd Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 8 Oct 2009 09:59:20 +0000
Subject: [PATCH] new discrimination tree instantiation with inverse De Brujin
 indexes.

---
 .../components/ng_tactics/nTacStatus.ml       | 63 +++++++++++++++++++
 .../components/ng_tactics/nTacStatus.mli      | 12 ++++
 2 files changed, 75 insertions(+)

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index dc059d50d..d55f7439f 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -375,3 +375,66 @@ class type tac_status = [Continuationals.Stack.t] status
 
 type 'status tactic = #tac_status as 'status -> 'status
 
+module NCicInverseRelIndexable : Discrimination_tree.Indexable
+with type input = cic_term and type constant_name = NUri.uri = struct
+
+open Discrimination_tree
+
+type input = cic_term
+type constant_name = NUri.uri
+
+let ppelem = function
+  | Constant (uri,arity) -> 
+      "("^NUri.name_of_uri uri ^ "," ^ string_of_int arity^")"
+  | Bound (i,arity) -> 
+      "("^string_of_int i ^ "," ^ string_of_int arity^")"
+  | Variable -> "?"
+  | Proposition -> "Prop"
+  | Datatype -> "Type"
+  | Dead -> "Dead"
+;;
+
+let path_string_of (ctx,t) =
+  let len_ctx = List.length ctx in
+  let rec aux arity = function
+    | NCic.Appl ((NCic.Meta _|NCic.Implicit _)::_) -> [Variable]
+    | NCic.Appl (NCic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
+    | NCic.Appl [] -> assert false
+    | NCic.Appl (hd::tl) ->
+        aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) 
+    | NCic.Lambda _ | NCic.Prod _ -> [Variable]
+        (* I think we should CicSubstitution.subst Implicit t *)
+    | NCic.LetIn _ -> [Variable] (* z-reduce? *)
+    | NCic.Meta _ | NCic.Implicit _ -> assert (arity = 0); [Variable]
+    | NCic.Rel i -> [Bound (len_ctx - i, arity)]
+    | NCic.Sort (NCic.Prop) -> assert (arity=0); [Proposition]
+    | NCic.Sort _ -> assert (arity=0); [Datatype]
+    | NCic.Const (NReference.Ref (u,_)) -> [Constant (u, arity)]
+    | NCic.Match _ -> [Dead]
+  in 
+    aux 0 t
+;;
+
+let compare e1 e2 =
+  match e1,e2 with
+  | Constant (u1,a1),Constant (u2,a2) -> 
+       let x = NUri.compare u1 u2 in
+       if x = 0 then Pervasives.compare a1 a2 else x
+  | e1,e2 -> Pervasives.compare e1 e2
+;;
+
+let string_of_path l = String.concat "." (List.map ppelem l) ;;
+
+end
+
+module Ncic_termOT : Set.OrderedType with type t = cic_term =
+ struct
+   type t = cic_term
+   let compare = Pervasives.compare
+ end
+
+module Ncic_termSet : Set.S with type elt = cic_term = Set.Make(Ncic_termOT)
+
+module InvRelDiscriminationTree = 
+   Discrimination_tree.Make(NCicInverseRelIndexable)(Ncic_termSet)
+
diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 33b01b575..15a788669 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -93,4 +93,16 @@ class type tac_status = [Continuationals.Stack.t] status
 
 type 'status tactic = #tac_status as 'status -> 'status
 
+(* indexing facilities over cic_term based on inverse De Bruijn indexes *)
+
+module NCicInverseRelIndexable : Discrimination_tree.Indexable
+with type input = cic_term and type constant_name = NUri.uri 
+
+module Ncic_termSet : Set.S with type elt = cic_term
+
+module InvRelDiscriminationTree : Discrimination_tree.DiscriminationTree 
+with type constant_name = NCicInverseRelIndexable.constant_name
+and type input = NCicInverseRelIndexable.input
+and type data = Ncic_termSet.elt and type dataset = Ncic_termSet.t
+
 (* end *)
-- 
2.39.2