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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Util
open Pp
open Names
open Libnames
open Rawterm
open Libobject
open Lib
open Nameops
(* Syntactic definitions. *)
let syntax_table = ref (KNmap.empty : rawconstr KNmap.t)
let _ = Summary.declare_summary
"SYNTAXCONSTANT"
{ Summary.freeze_function = (fun () -> !syntax_table);
Summary.unfreeze_function = (fun ft -> syntax_table := ft);
Summary.init_function = (fun () -> syntax_table := KNmap.empty);
Summary.survive_section = false }
let add_syntax_constant kn c =
syntax_table := KNmap.add kn c !syntax_table
let cache_syntax_constant ((sp,kn),c) =
if Nametab.exists_cci sp then
errorlabstrm "cache_syntax_constant"
(pr_id (basename sp) ++ str " already exists");
add_syntax_constant kn c;
Nametab.push_syntactic_definition (Nametab.Until 1) sp kn
let load_syntax_constant i ((sp,kn),c) =
if Nametab.exists_cci sp then
errorlabstrm "cache_syntax_constant"
(pr_id (basename sp) ++ str " already exists");
add_syntax_constant kn c;
Nametab.push_syntactic_definition (Nametab.Until i) sp kn
let open_syntax_constant i ((sp,kn),c) =
Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn
let subst_syntax_constant ((sp,kn),subst,c) =
subst_raw subst c
let classify_syntax_constant (_,c) = Substitute c
let (in_syntax_constant, out_syntax_constant) =
declare_object {(default_object "SYNTAXCONSTANT") with
cache_function = cache_syntax_constant;
load_function = load_syntax_constant;
open_function = open_syntax_constant;
subst_function = subst_syntax_constant;
classify_function = classify_syntax_constant;
export_function = (fun x -> Some x) }
let declare_syntactic_definition id c =
let _ = add_leaf id (in_syntax_constant c) in ()
let rec set_loc loc = function
| RRef (_,a) -> RRef (loc,a)
| RVar (_,a) -> RVar (loc,a)
| RApp (_,a,b) -> RApp (loc,set_loc loc a,List.map (set_loc loc) b)
| RSort (_,a) -> RSort (loc,a)
| RHole (_,a) -> RHole (loc,a)
| RLambda (_,na,ty,c) -> RLambda (loc,na,set_loc loc ty,set_loc loc c)
| RProd (_,na,ty,c) -> RProd (loc,na,set_loc loc ty,set_loc loc c)
| RLetIn (_,na,b,c) -> RLetIn (loc,na,set_loc loc b,set_loc loc c)
| RCast (_,a,b) -> RCast (loc,set_loc loc a,set_loc loc b)
| a -> warning "Unrelocatated syntactic definition"; a
let search_syntactic_definition loc kn =
set_loc loc (KNmap.find kn !syntax_table)
|