From 348e5e6b9765c760159107a0fdb102c3eff42cd9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 17 Sep 2008 10:22:57 +0000 Subject: [PATCH] ... --- .../ng_refiner/nDiscriminationTree.ml | 145 ++++++++++-------- .../ng_refiner/nDiscriminationTree.mli | 6 +- 2 files changed, 84 insertions(+), 67 deletions(-) diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml index 1089474e4..c4fd43ad2 100644 --- a/helm/software/components/ng_refiner/nDiscriminationTree.ml +++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml @@ -11,65 +11,87 @@ (* $Id$ *) +type path_string_elem = + | Constant of NUri.uri + | Bound of int + | Variable + | Proposition + | Datatype + | Dead of NCic.term +;; + +type path_string = path_string_elem list;; + +let ppelem = function + | Constant uri -> NUri.name_of_uri uri + | Bound i -> string_of_int i + | Variable -> "?" + | Proposition -> "Prop" + | Datatype -> "Type" + | Dead t -> + "DEAD("^NCicPp.ppterm ~context:[] ~subst:[] ~metasenv:[] t^")" +;; + +let pp_path_string l = String.concat "::" (List.map ppelem l) ;; + +let elem_of_cic = function + | NCic.Meta _ | NCic.Implicit _ -> Variable + | NCic.Rel i -> Bound i + | NCic.Sort (NCic.Prop) -> Proposition + | NCic.Sort _ -> Datatype + | NCic.Const (NReference.Ref (u,_)) -> Constant u + | NCic.Appl _ -> assert false (* should not happen *) + | NCic.LetIn _ | NCic.Lambda _ | NCic.Prod _ | NCic.Match _ as t -> + prerr_endline + "FIXME: the discrimination tree receives an invalid term"; + Dead t +;; + +let path_string_of_term arities = + let set_arity arities k n = + (assert (k<>Variable || n=0); + match k with + | Dead _ -> arities + | _ -> + (* here we override, but partial instantiation may trick us *) + (k,n)::(List.remove_assoc k arities)) + in + let rec aux arities = function + | NCic.Appl ((hd::tl) as l) -> + let arities = + set_arity arities (elem_of_cic hd) (List.length tl) + in + List.fold_left + (fun (arities,path) t -> + let arities,tpath = aux arities t in + arities,path@tpath) + (arities,[]) l + | t -> arities, [elem_of_cic t] + in + aux arities +;; + +let compare_elem e1 e2 = + match e1,e2 with + | Constant u1,Constant u2 -> NUri.compare u1 u2 + | e1,e2 -> Pervasives.compare e1 e2 +;; + +let head_of_term = function + | NCic.Appl (hd::tl) -> hd + | term -> term +;; + +let rec skip_prods = function + | NCic.Prod (_,_,t) -> skip_prods t + | term -> term +;; + + module DiscriminationTreeIndexing = functor (A:Set.S) -> struct - type path_string_elem = - | Constant of NUri.uri - | Bound of int | Variable | Proposition | Datatype | Dead;; - type path_string = path_string_elem list;; - - - (* needed by the retrieve_* functions, to know the arities of the - * "functions" *) - - let ppelem = function - | Constant uri -> NUri.name_of_uri uri - | Bound i -> string_of_int i - | Variable -> "?" - | Proposition -> "Prop" - | Datatype -> "Type" - | Dead -> "DEAD" - ;; - let pppath l = String.concat "::" (List.map ppelem l) ;; - let elem_of_cic = function - | NCic.Meta _ | NCic.Implicit _ -> Variable - | NCic.Rel i -> Bound i - | NCic.Sort (NCic.Prop) -> Proposition - | NCic.Sort _ -> Datatype - | NCic.Const (NReference.Ref (u,_)) -> Constant u - | NCic.Appl _ -> - assert false (* should not happen *) - | NCic.LetIn _ | NCic.Lambda _ | NCic.Prod _ | NCic.Match _ -> - prerr_endline "FIXME: the discrimination tree receives an invalid term"; - Dead - (* assert false universe.ml removes these *) - ;; - let path_string_of_term arities = - let set_arity arities k n = - (assert (k<>Variable || n=0); - if k = Dead then arities else (k,n)::(List.remove_assoc k arities)) - in - let rec aux arities = function - | NCic.Appl ((hd::tl) as l) -> - let arities = - set_arity arities (elem_of_cic hd) (List.length tl) in - List.fold_left - (fun (arities,path) t -> - let arities,tpath = aux arities t in - arities,path@tpath) - (arities,[]) l - | t -> arities, [elem_of_cic t] - in - aux arities - ;; - let compare_elem e1 e2 = - match e1,e2 with - | Constant u1,Constant u2 -> assert false (*NUri.compare u1 u2*) - | e1,e2 -> Pervasives.compare e1 e2 - ;; - module OrderedPathStringElement = struct type t = path_string_elem let compare = compare_elem @@ -82,10 +104,11 @@ module DiscriminationTreeIndexing = module DiscriminationTree = Trie.Make(PSMap);; type t = A.t DiscriminationTree.t * (path_string_elem*int) list + let empty = DiscriminationTree.empty, [] ;; let iter (dt, _ ) f = - DiscriminationTree.iter (fun _ x -> f x) dt + DiscriminationTree.iter (fun y x -> f y x) dt ;; let index (tree,arity) term info = @@ -118,16 +141,6 @@ module DiscriminationTreeIndexing = false ;; - let head_of_term = function - | NCic.Appl (hd::tl) -> hd - | term -> term - ;; - - let rec skip_prods = function - | NCic.Prod (_,_,t) -> skip_prods t - | term -> term - ;; - let rec subterm_at_pos pos term = match pos with | [] -> term diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.mli b/helm/software/components/ng_refiner/nDiscriminationTree.mli index a146c4b73..04f8c6907 100644 --- a/helm/software/components/ng_refiner/nDiscriminationTree.mli +++ b/helm/software/components/ng_refiner/nDiscriminationTree.mli @@ -12,12 +12,16 @@ (* $Id$ *) +type path_string + +val pp_path_string : path_string -> string + module DiscriminationTreeIndexing : functor (A : Set.S) -> sig type t - val iter : t -> (A.t -> unit) -> unit + val iter : t -> (path_string -> A.t -> unit) -> unit val empty : t val index : t -> NCic.term -> A.elt -> t -- 2.39.2