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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i*)
open Names
open Globnames
open Term
open Environ
open Util
open Libobject
module NamedDecl = Context.Named.Declaration
(*i*)
let name_table =
Summary.ref (Refmap.empty : Name.t list Refmap.t)
~name:"rename-arguments"
type req =
| ReqLocal
| ReqGlobal of global_reference * Name.t list
let load_rename_args _ (_, (_, (r, names))) =
name_table := Refmap.add r names !name_table
let cache_rename_args o = load_rename_args 1 o
let classify_rename_args = function
| ReqLocal, _ -> Dispose
| ReqGlobal _, _ as o -> Substitute o
let subst_rename_args (subst, (_, (r, names as orig))) =
ReqLocal,
let r' = fst (subst_global subst r) in
if r==r' then orig else (r', names)
let section_segment_of_reference = function
| ConstRef con -> Lib.section_segment_of_constant con
| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
Lib.section_segment_of_mutual_inductive kn
| _ -> [], Univ.LMap.empty, Univ.UContext.empty
let discharge_rename_args = function
| _, (ReqGlobal (c, names), _ as req) ->
(try
let vars,_,_ = section_segment_of_reference c in
let c' = pop_global_reference c in
let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
let names' = var_names @ names in
Some (ReqGlobal (c', names), (c', names'))
with Not_found -> Some req)
| _ -> None
let rebuild_rename_args x = x
let inRenameArgs = declare_object { (default_object "RENAME-ARGUMENTS" ) with
load_function = load_rename_args;
cache_function = cache_rename_args;
classify_function = classify_rename_args;
subst_function = subst_rename_args;
discharge_function = discharge_rename_args;
rebuild_function = rebuild_rename_args;
}
let rename_arguments local r names =
let req = if local then ReqLocal else ReqGlobal (r, names) in
Lib.add_anonymous_leaf (inRenameArgs (req, (r, names)))
let arguments_names r = Refmap.find r !name_table
let rec rename_prod c = function
| [] -> c
| (Name _ as n) :: tl ->
(match kind_of_type c with
| ProdType (_, s, t) -> mkProd (n, s, rename_prod t tl)
| _ -> c)
| _ :: tl ->
match kind_of_type c with
| ProdType (n, s, t) -> mkProd (n, s, rename_prod t tl)
| _ -> c
let rename_type ty ref =
try rename_prod ty (arguments_names ref)
with Not_found -> ty
let rename_type_of_constant env c =
let ty = Typeops.type_of_constant_in env c in
rename_type ty (ConstRef (fst c))
let rename_type_of_inductive env ind =
let ty = Inductiveops.type_of_inductive env ind in
rename_type ty (IndRef (fst ind))
let rename_type_of_constructor env cstruct =
let ty = Inductiveops.type_of_constructor env cstruct in
rename_type ty (ConstructRef (fst cstruct))
let rename_typing env c =
let j = Typeops.infer env c in
let j' =
match kind_of_term c with
| Const (c,u) -> { j with uj_type = rename_type j.uj_type (ConstRef c) }
| Ind (i,u) -> { j with uj_type = rename_type j.uj_type (IndRef i) }
| Construct (k,u) -> { j with uj_type = rename_type j.uj_type (ConstructRef k) }
| _ -> j
in j'
|
