summaryrefslogtreecommitdiff
path: root/tactics/nbtermdn.ml
blob: 7d6e1c4c90c3f8ccd1e99ca0b0dfcaeae9edc917 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)

open Util
open Names
open Term
open Libobject
open Library
open Pattern
open Libnames

(* Named, bounded-depth, term-discrimination nets.
   Implementation:
   Term-patterns are stored in discrimination-nets, which are
   themselves stored in a hash-table, indexed by the first label.
   They are also stored by name in a table on-the-side, so that we can
   override them if needed. *)

(* The former comments are from Chet.
   See the module dn.ml for further explanations.
   Eduardo (5/8/97) *)
module Make = 
  functor (Y:Map.OrderedType) ->
struct
  module X = struct
    type t = constr_pattern*int
    let compare = Pervasives.compare
  end

  module Term_dn = Termdn.Make(Y)
  open Term_dn
  module Z = struct 
     type t = Term_dn.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)(Z)(Y)
  module Bounded_net = Btermdn.Make(Y)

    
type 'na t = {
  mutable table : ('na,constr_pattern * Y.t) Gmap.t;
  mutable patterns : (Term_dn.term_label option,Bounded_net.t) Gmap.t }


type 'na frozen_t = 
    ('na,constr_pattern * Y.t) Gmap.t
    * (Term_dn.term_label option, Bounded_net.t) Gmap.t

let create () =
  { table = Gmap.empty;
    patterns = Gmap.empty }

let get_dn dnm hkey =
  try Gmap.find hkey dnm with Not_found -> Bounded_net.create ()

let add dn (na,(pat,valu)) =
  let hkey = Option.map fst (Term_dn.constr_pat_discr pat) in 
  dn.table <- Gmap.add na (pat,valu) dn.table;
  let dnm = dn.patterns in
  dn.patterns <- Gmap.add hkey (Bounded_net.add None (get_dn dnm hkey) (pat,valu)) dnm

let rmv dn na =
  let (pat,valu) = Gmap.find na dn.table in
  let hkey = Option.map fst (Term_dn.constr_pat_discr pat) in 
  dn.table <- Gmap.remove na dn.table;
  let dnm = dn.patterns in
  dn.patterns <- Gmap.add hkey (Bounded_net.rmv None (get_dn dnm hkey) (pat,valu)) dnm

let in_dn dn na = Gmap.mem na dn.table

let remap ndn na (pat,valu) =
  rmv ndn na;
  add ndn (na,(pat,valu))

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 
  decrec []

  let constr_val_discr t =
  let c, l = decomp t in
    match kind_of_term c with
    | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
    | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
    | Var id -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
    | Const _ -> Dn.Everything
    | _ -> Dn.Nothing

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 Dn.Everything else Dn.Label(Term_dn.GRLabel (ConstRef c),l)
    | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
    | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
    | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
    | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c])
    | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l)
    | Sort s -> Dn.Label(Term_dn.SortLabel (Some s), [])
    | Evar _ -> Dn.Everything
    | _ -> Dn.Nothing

let lookup dn valu =
  let hkey =
    match (constr_val_discr valu) with
    | Dn.Label(l,_) -> Some l
    | _ -> None
  in
  try Bounded_net.lookup None (Gmap.find hkey dn.patterns) valu with Not_found -> []

let app f dn = Gmap.iter f dn.table

let dnet_depth = Btermdn.dnet_depth

let freeze dn = (dn.table, dn.patterns)

let unfreeze (fnm,fdnm) dn =
  dn.table <- fnm;
  dn.patterns <- fdnm

let empty dn =
  dn.table <- Gmap.empty;
  dn.patterns <- Gmap.empty

let to2lists dn =
  (Gmap.to_list dn.table, Gmap.to_list dn.patterns)
end