aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/conv_oracle.ml
blob: c195a5496d5663ed3bee27ef05fc172e922a0e47 (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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Created by Bruno Barras as part of the rewriting of the conversion
   algorithm, Nov 2001 *)

open Names

(* Priority for the expansion of constant in the conversion test.
 * Higher levels means that the expansion is less prioritary.
 * (And Expand stands for -oo, and Opaque +oo.)
 * The default value is [Level 100].
 *)
type level = Expand | Level of int | Opaque
let default = Level 0
let transparent = default

type oracle = level Idmap.t * level Cmap.t

let var_opacity = ref Idmap.empty
let cst_opacity = ref Cmap.empty

let get_strategy = function
  | VarKey id ->
      (try Idmap.find id !var_opacity
      with Not_found -> default)
  | ConstKey c ->
      (try Cmap.find c !cst_opacity
      with Not_found -> default)
  | RelKey _ -> Expand

let set_strategy k l =
  match k with
  | VarKey id ->
      var_opacity :=
      if l=default then Idmap.remove id !var_opacity
      else Idmap.add id l !var_opacity
  | ConstKey c ->
      cst_opacity :=
      if l=default then Cmap.remove c !cst_opacity
      else Cmap.add c l !cst_opacity
  | RelKey _ -> Errors.error "set_strategy: RelKey"

let get_transp_state () =
  (Idmap.fold
    (fun id l ts -> if  l=Opaque then Idpred.remove id ts else ts)
    !var_opacity Idpred.full,
   Cmap.fold
    (fun c l ts -> if  l=Opaque then Cpred.remove c ts else ts)
    !cst_opacity Cpred.full)

(* Unfold the first constant only if it is "more transparent" than the
   second one. In case of tie, expand the second one. *)
let oracle_order l2r k1 k2 =
  match get_strategy k1, get_strategy k2 with
    | Expand, _ -> true
    | Level n1, Opaque -> true
    | Level n1, Level n2 -> n1 < n2
    | _ -> l2r (* use recommended default *)

(* summary operations *)
let init() = (cst_opacity := Cmap.empty; var_opacity := Idmap.empty)
let freeze () = (!var_opacity, !cst_opacity)
let unfreeze (vo,co) = (cst_opacity := co; var_opacity := vo)