package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file btermdn.ml

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
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Util
open Constr
open EConstr
open Names
open Pattern

(* Discrimination nets with bounded depth.
   See the module dn.ml for further explanations.
   Eduardo (5/8/97). *)

let dnet_depth = ref 8

type term_label =
| GRLabel of GlobRef.t
| ProdLabel
| SortLabel

let compare_term_label t1 t2 = match t1, t2 with
| GRLabel gr1, GRLabel gr2 -> GlobRef.CanOrd.compare gr1 gr2
| _ -> pervasives_compare t1 t2 (** OK *)

type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything

let eta_reduce = Reductionops.shrink_eta

(* TODO: instead of doing that on patterns we should try to perform it on terms
   before translating them into patterns in Hints. *)
let rec eta_reduce_pat p = match p with
| PLambda (_, _, q) ->
  let f, cl = match eta_reduce_pat q with
  | PApp (f, cl) -> f, cl
  | q -> q, [||]
  in
  let napp = Array.length cl in
  if napp > 0 then
    let r = eta_reduce_pat (Array.last cl) in
    match r with
    | PRel 1 ->
      let lc = Array.sub cl 0 (napp - 1) in
      let u = if Array.is_empty lc then f else PApp (f, lc) in
      if Patternops.noccurn_pattern 1 u then Patternops.lift_pattern (-1) u else p
    | _ -> p
  else p
| PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _ | PProj _ | PProd _
| PLetIn _ | PSort _ | PMeta _ | PIf _ | PCase _ | PFix _ | PCoFix _ | PInt _
| PFloat _ | PArray _ -> p

let decomp_pat p =
  let rec decrec acc = function
    | PApp (f,args) -> decrec (Array.to_list args @ acc) f
    | PProj (p, c) ->
      let hole = PMeta None in
      let params = List.make (Projection.npars p) hole in
      (PRef (GlobRef.ConstRef (Projection.constant p)), params @ c :: acc)
    | c -> (c,acc)
  in
  decrec [] (eta_reduce_pat p)

let decomp sigma t =
  let rec decrec acc c = match EConstr.kind sigma c with
    | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
    | Proj (p, c) ->
      (* Hack: fake evar to generate [Everything] in the functions below *)
      let hole = mkEvar (Evar.unsafe_of_int (-1), SList.empty) in
      let params = List.make (Projection.npars p) hole in
      (mkConst (Projection.constant p), params @ c :: acc)
    | Cast (c1,_,_) -> decrec acc c1
    | _ -> (c,acc)
  in
    decrec [] (eta_reduce sigma t)

let evaluable_constant c env ts =
  (* This is a hack to work around a broken Print Module implementation, see
     bug #2668. *)
  (if Environ.mem_constant c env then Environ.evaluable_constant c env else true) &&
  (match ts with None -> true | Some ts -> TransparentState.is_transparent_constant ts c)

let evaluable_named id env ts =
  (try Environ.evaluable_named id env with Not_found -> true) &&
  (match ts with None -> true | Some ts -> TransparentState.is_transparent_variable ts id)

(* The pattern view functions below try to overapproximate βι-neutral terms up
   to η-conversion. Some historical design choices are still incorrect w.r.t. to
   this specification. TODO: try to make them follow the spec. *)

let constr_val_discr env sigma ts t =
  (* Should we perform weak βι here? *)
  let c, l = decomp sigma t in
  let open GlobRef in
    match EConstr.kind sigma c with
    | Const (c,u) ->
      if evaluable_constant c env ts then Everything
      else Label(GRLabel (ConstRef c),l)
    | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l)
    | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l)
    | Var id ->
      if evaluable_named id env ts then Everything
      else Label(GRLabel (VarRef id),l)
    | Prod (n, d, c) ->
      Label(ProdLabel, [d; c])
    | Lambda (n, d, c) ->
      if Option.is_empty ts && List.is_empty l then Nothing
      else Everything
    | Sort _ -> Label(SortLabel, [])
    | Evar _ -> Everything
    | Case (_, _, _, _, _, c, _) ->
      (* Overapproximate wildly. TODO: be less brutal. *)
      Everything
    | Rel _ | Meta _ | Cast _ | LetIn _ | App _ | Fix _ | CoFix _
    | Proj _ | Int _ | Float _ | Array _ -> Nothing

let constr_pat_discr env ts t =
  let open GlobRef in
  match decomp_pat t with
  | PRef ((IndRef _) as ref), args
  | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
  | PRef ((VarRef v) as ref), args ->
    if evaluable_named v env ts then None
    else Some(GRLabel ref,args)
  | PRef ((ConstRef c) as ref), args ->
    if evaluable_constant c env ts then None
    else Some (GRLabel ref, args)
  | PVar v, args ->
    if evaluable_named v env ts then None
    else Some(GRLabel (VarRef v),args)
  | PProd (_, d, c), [] ->
    Some (ProdLabel, [d ; c])
  | PLambda (_, d, c), [] -> None
  | PSort s, [] ->
    Some (SortLabel, [])
  | _ -> None

let bounded_constr_pat_discr env st (t,depth) =
  if Int.equal depth 0 then None
  else match constr_pat_discr env st t with
  | None -> None
  | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)

let bounded_constr_val_discr env st sigma (t,depth) =
  if Int.equal depth 0 then
    Nothing
  else match constr_val_discr env sigma st t with
  | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l)
  | Nothing -> Nothing
  | Everything -> Everything

module Make =
  functor (Z : Map.OrderedType) ->
struct

 module Y = struct
    type t = term_label
    let compare = compare_term_label
 end

 module Dn = Dn.Make(Y)(Z)

 type t = Dn.t

  type pattern = Dn.pattern

  let pattern env st pat =
    Dn.pattern (bounded_constr_pat_discr env st) (pat, !dnet_depth)

  let constr_pattern env sigma st pat =
    let mk p = match bounded_constr_val_discr env st sigma p with
    | Label l -> Some l
    | Everything | Nothing -> None
    in
    Dn.pattern mk (pat, !dnet_depth)

  let empty = Dn.empty
  let add = Dn.add
  let rmv = Dn.rmv

  let lookup env sigma st dn t =
    Dn.lookup dn (bounded_constr_val_discr env st sigma) (t,!dnet_depth)

end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct