From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 tactics/termdn.ml | 101 ++++++++++++++++++++++++++++++++++++++++--------------
 1 file changed, 75 insertions(+), 26 deletions(-)

(limited to 'tactics/termdn.ml')

diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index bd439fb4..7b6d3ea7 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: termdn.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id$ *)
 
 open Util
 open Names
@@ -20,25 +20,60 @@ open Nametab
 (* Discrimination nets of terms.
    See the module dn.ml for further explanations.
    Eduardo (5/8/97) *)
+module Make =
+  functor (Z : Map.OrderedType) ->
+struct
 
-type 'a t = (global_reference,constr_pattern,'a) Dn.t
+  module X = struct
+    type t = constr_pattern
+    let compare = Pervasives.compare
+  end
+
+  type term_label = 
+    | GRLabel of global_reference
+    | ProdLabel 
+    | LambdaLabel
+    | SortLabel of sorts option
+	
+  module Y =  struct 
+     type t = term_label
+        let compare x y = 
+       let make_name n =
+	 match n with
+	 | GRLabel(ConstRef con) -> 
+	     GRLabel(ConstRef(constant_of_kn(canonical_con con)))
+	 | GRLabel(IndRef (kn,i)) ->
+	     GRLabel(IndRef(mind_of_kn(canonical_mind kn),i))
+	 | GRLabel(ConstructRef ((kn,i),j ))->
+	     GRLabel(ConstructRef((mind_of_kn(canonical_mind kn),i),j))
+	 | k -> k
+       in
+	 Pervasives.compare (make_name x) (make_name y)
+  end
+       
+      
+  module Dn = Dn.Make(X)(Y)(Z)
+      
+  type t = Dn.t
+
+  type 'a lookup_res = 'a Dn.lookup_res
 
 (*If we have: f a b c ..., decomp gives: (f,[a;b;c;...])*)
 
-let decomp = 
+let decomp =
   let rec decrec acc c = match kind_of_term c with
     | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
     | Cast (c1,_,_) -> decrec acc c1
     | _ -> (c,acc)
-  in 
+  in
   decrec []
 
-let decomp_pat = 
+let decomp_pat =
   let rec decrec acc = function
     | PApp (f,args) -> decrec (Array.to_list args @ acc) f
     | c -> (c,acc)
-  in 
-  decrec []   
+  in
+  decrec []
 
 let constr_pat_discr t =
   if not (occur_meta_pattern t) then
@@ -46,49 +81,63 @@ let constr_pat_discr t =
   else
     match decomp_pat t with
     | PRef ((IndRef _) as ref), args
-    | PRef ((ConstructRef _ ) as ref), args -> Some (ref,args)
-    | PRef ((VarRef v) as ref), args -> Some(ref,args)
+    | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
+    | PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args)
     | _ -> None
 
 let constr_pat_discr_st (idpred,cpred) t =
   match decomp_pat t with
   | PRef ((IndRef _) as ref), args
-  | PRef ((ConstructRef _ ) as ref), args -> Some (ref,args)
-  | PRef ((VarRef v) as ref), args when not (Idpred.mem v idpred) -> 
-      Some(ref,args)
+  | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
+  | PRef ((VarRef v) as ref), args when not (Idpred.mem v idpred) ->
+      Some(GRLabel ref,args)
   | PVar v, args when not (Idpred.mem v idpred) ->
-      Some(VarRef v,args)
+      Some(GRLabel (VarRef v),args)
   | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) ->
-      Some (ref, args)
+      Some (GRLabel ref, args)
+  | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c])
+  | PLambda (_, d, c), l -> Some (LambdaLabel, [d ; c] @ l)
+  | PSort s, [] -> 
+      let s' = match s with
+	| RProp c -> Some (Prop c)
+	| RType _ -> None 
+	    (* Don't try to be clever about type levels here *)
+      in Some (SortLabel s', [])
   | _ -> None
 
 open Dn
 
-let constr_val_discr t =  
+let constr_val_discr t =
   let c, l = decomp t in
     match kind_of_term c with
-    | Ind ind_sp -> Label(IndRef ind_sp,l)
-    | Construct cstr_sp -> Label((ConstructRef cstr_sp),l)
-    | Var id -> Label(VarRef id,l)
+    | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l)
+    | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l)
+    | Var id -> Label(GRLabel (VarRef id),l)
     | Const _ -> Everything
     | _ -> Nothing
-	
-let constr_val_discr_st (idpred,cpred) t =  
+
+let constr_val_discr_st (idpred,cpred) t =
   let c, l = decomp t in
     match kind_of_term c with
-    | Const c -> if Cpred.mem c cpred then Everything else Label(ConstRef c,l)
-    | Ind ind_sp -> Label(IndRef ind_sp,l)
-    | Construct cstr_sp -> Label((ConstructRef cstr_sp),l)
-    | Var id when not (Idpred.mem id idpred) -> Label(VarRef id,l)
+    | Const c -> if Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l)
+    | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l)
+    | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l)
+    | Var id when not (Idpred.mem id idpred) -> Label(GRLabel (VarRef id),l)
+    | Prod (n, d, c) -> Label(ProdLabel, [d; c])
+    | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l)
+    | Sort s when is_small s -> Label(SortLabel (Some s), [])
+    | Sort _ -> Label (SortLabel None, [])
     | Evar _ -> Everything
     | _ -> Nothing
 
-let create = Dn.create 
+let create = Dn.create
 
 let add dn st = Dn.add dn (constr_pat_discr_st st)
 
 let rmv dn st = Dn.rmv dn (constr_pat_discr_st st)
 
 let lookup dn st t = Dn.lookup dn (constr_val_discr_st st) t
-  
+
 let app f dn = Dn.app f dn
+
+end
-- 
cgit v1.2.3