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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* File created by Vincent Siles, Oct 2007, extended into a generic
support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *)
(* This file provides support for registering inductive scheme builders,
declaring schemes and generating schemes on demand *)
open Names
open Mod_subst
open Libobject
open Nameops
open Declarations
open Term
open Errors
open Util
open Declare
open Entries
open Decl_kinds
(**********************************************************************)
(* Registering schemes in the environment *)
type mutual_scheme_object_function = mutual_inductive -> constr array
type individual_scheme_object_function = inductive -> constr
type 'a scheme_kind = string
let scheme_map = ref Indmap.empty
let cache_one_scheme kind (ind,const) =
let map = try Indmap.find ind !scheme_map with Not_found -> Stringmap.empty in
scheme_map := Indmap.add ind (Stringmap.add kind const map) !scheme_map
let cache_scheme (_,(kind,l)) =
Array.iter (cache_one_scheme kind) l
let subst_one_scheme subst ((mind,i),const) =
(* Remark: const is a def: the result of substitution is a constant *)
((subst_ind subst mind,i),fst (subst_con subst const))
let subst_scheme (subst,(kind,l)) =
(kind,Array.map (subst_one_scheme subst) l)
let discharge_scheme (_,(kind,l)) =
Some (kind,Array.map (fun (ind,const) ->
(Lib.discharge_inductive ind,Lib.discharge_con const)) l)
let inScheme : string * (inductive * constant) array -> obj =
declare_object {(default_object "SCHEME") with
cache_function = cache_scheme;
load_function = (fun _ -> cache_scheme);
subst_function = subst_scheme;
classify_function = (fun obj -> Substitute obj);
discharge_function = discharge_scheme}
(**********************************************************************)
(* Saving/restoring the table of scheme *)
let freeze_schemes () = !scheme_map
let unfreeze_schemes sch = scheme_map := sch
let init_schemes () = scheme_map := Indmap.empty
let _ =
Summary.declare_summary "Schemes"
{ Summary.freeze_function = freeze_schemes;
Summary.unfreeze_function = unfreeze_schemes;
Summary.init_function = init_schemes }
(**********************************************************************)
(* The table of scheme building functions *)
type individual
type mutual
type scheme_object_function =
| MutualSchemeFunction of (mutual_inductive -> constr array)
| IndividualSchemeFunction of (inductive -> constr)
let scheme_object_table =
(Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
let declare_scheme_object s aux f =
(try check_ident ("ind"^s) with _ ->
error ("Illegal induction scheme suffix: "^s));
let key = if aux = "" then s else aux in
try
let _ = Hashtbl.find scheme_object_table key in
(* let aux_msg = if aux="" then "" else " (with key "^aux^")" in*)
error ("Scheme object "^key^" already declared.")
with Not_found ->
Hashtbl.add scheme_object_table key (s,f);
key
let declare_mutual_scheme_object s ?(aux="") f =
declare_scheme_object s aux (MutualSchemeFunction f)
let declare_individual_scheme_object s ?(aux="") f =
declare_scheme_object s aux (IndividualSchemeFunction f)
(**********************************************************************)
(* Defining/retrieving schemes *)
let declare_scheme kind indcl =
Lib.add_anonymous_leaf (inScheme (kind,indcl))
let is_visible_name id =
try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true
with Not_found -> false
let compute_name internal id =
match internal with
| KernelVerbose | UserVerbose -> id
| KernelSilent ->
Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
let define internal id c =
let fd = declare_constant ~internal in
let id = compute_name internal id in
let kn = fd id
(DefinitionEntry
{ const_entry_body = c;
const_entry_secctx = None;
const_entry_type = None;
const_entry_opaque = false },
Decl_kinds.IsDefinition Scheme) in
(match internal with
| KernelSilent -> ()
| _-> definition_message id);
kn
let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
let c = f ind in
let mib = Global.lookup_mind mind in
let id = match idopt with
| Some id -> id
| None -> add_suffix mib.mind_packets.(i).mind_typename suff in
let const = define internal id c in
declare_scheme kind [|ind,const|];
const
let define_individual_scheme kind internal names (mind,i as ind) =
match Hashtbl.find scheme_object_table kind with
| _,MutualSchemeFunction f -> assert false
| s,IndividualSchemeFunction f ->
define_individual_scheme_base kind s f internal names ind
let define_mutual_scheme_base kind suff f internal names mind =
let cl = f mind in
let mib = Global.lookup_mind mind in
let ids = Array.init (Array.length mib.mind_packets) (fun i ->
try List.assoc i names
with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
let consts = Array.map2 (define internal) ids cl in
declare_scheme kind (Array.mapi (fun i cst -> ((mind,i),cst)) consts);
consts
let define_mutual_scheme kind internal names mind =
match Hashtbl.find scheme_object_table kind with
| _,IndividualSchemeFunction _ -> assert false
| s,MutualSchemeFunction f ->
define_mutual_scheme_base kind s f internal names mind
let find_scheme kind (mind,i as ind) =
try Stringmap.find kind (Indmap.find ind !scheme_map)
with Not_found ->
match Hashtbl.find scheme_object_table kind with
| s,IndividualSchemeFunction f ->
define_individual_scheme_base kind s f KernelSilent None ind
| s,MutualSchemeFunction f ->
(define_mutual_scheme_base kind s f KernelSilent [] mind).(i)
let check_scheme kind ind =
try let _ = Stringmap.find kind (Indmap.find ind !scheme_map) in true
with Not_found -> false
|
