From cf4b0ccb2b5d494f9c7856c7a849ca60ebf857cd Mon Sep 17 00:00:00 2001 From: Enrico Tassi 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