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
|
open Names;;
open Sign;;
open Util;;
open Ast;;
open Term;;
open Pp;;
open Libobject;;
open Library;;
open Vernacinterp;;
open Termast;;
open Tacmach;;
open Pfedit;;
open Parsing;;
open Evd;;
open Evarutil;;
open Xlate;;
open Ctast;;
open Vtp;;
open Ascent;;
open Environ;;
open Proof_type;;
(* dead code: let rel_reference gt k oper =
if is_existential_oper oper then ope("XTRA", [str "ISEVAR"])
else begin
let id = id_of_global oper in
let oper', _ = global_operator (Nametab.sp_of_id k id) id in
if oper = oper' then nvar (string_of_id id)
else failwith "xlate"
end;;
*)
(* dead code:
let relativize relfun =
let rec relrec =
function
| Nvar (_, id) -> nvar id
| Slam (l, na, ast) -> Slam (l, na, relrec ast)
| Node (loc, nna, l) as ast -> begin
try relfun ast
with
| Failure _ -> Node (loc, nna, List.map relrec l)
end
| a -> a in
relrec;;
*)
(* dead code:
let dbize_sp =
function
| Path (loc, sl, s) -> begin
try section_path sl s
with
| Invalid_argument _ | Failure _ ->
anomaly_loc
(loc, "Translate.dbize_sp (taken from Astterm)",
[< str "malformed section-path" >])
end
| ast ->
anomaly_loc
(Ast.loc ast, "Translate.dbize_sp (taken from Astterm)",
[< str "not a section-path" >]);;
*)
(* dead code:
let relativize_cci gt = relativize (function
| Node (_, "CONST", (p :: _)) as gt ->
rel_reference gt CCI (Const (dbize_sp p))
| Node (_, "MUTIND", (p :: ((Num (_, tyi)) :: _))) as gt ->
rel_reference gt CCI (MutInd (dbize_sp p, tyi))
| Node (_, "MUTCONSTRUCT", (p :: ((Num (_, tyi)) :: ((Num (_, i)) :: _)))) as gt ->
rel_reference gt CCI (MutConstruct (
(dbize_sp p, tyi), i))
| _ -> failwith "caught") gt;;
*)
let coercion_description_holder = ref (function _ -> None : t -> int option);;
let coercion_description t = !coercion_description_holder t;;
let set_coercion_description f =
coercion_description_holder:=f; ();;
let rec nth_tl l n = if n = 0 then l
else (match l with
| a :: b -> nth_tl b (n - 1)
| [] -> failwith "list too short for nth_tl");;
let rec discard_coercions =
function
| Slam (l, na, ast) -> Slam (l, na, discard_coercions ast)
| Node (l, ("APPLIST" as nna), (f :: args as all_sons)) ->
(match coercion_description f with
| Some n ->
let new_args =
try nth_tl args n
with
| Failure "list too short for nth_tl" -> [] in
(match new_args with
| a :: (b :: c) -> Node (l, nna, List.map discard_coercions new_args)
| a :: [] -> discard_coercions a
| [] -> Node (l, nna, List.map discard_coercions all_sons))
| None -> Node (l, nna, List.map discard_coercions all_sons))
| Node (l, nna, all_sons) ->
Node (l, nna, List.map discard_coercions all_sons)
| it -> it;;
(*translates a formula into a centaur-tree --> FORMULA *)
let translate_constr at_top env c =
xlate_formula (Constrextern.extern_constr at_top env c);;
(*translates a named_context into a centaur-tree --> PREMISES_LIST *)
(* this code is inspired from printer.ml (function pr_named_context_of) *)
let translate_sign env =
let l =
Environ.fold_named_context
(fun env (id,v,c) l ->
(match v with
None ->
CT_premise(CT_ident(string_of_id id), translate_constr false env c)
| Some v1 ->
CT_eval_result
(CT_coerce_ID_to_FORMULA (CT_ident (string_of_id id)),
translate_constr false env v1,
translate_constr false env c))::l)
env ~init:[]
in
CT_premises_list l;;
(* the function rev_and_compact performs two operations:
1- it reverses the list of integers given as argument
2- it replaces sequences of "1" by a negative number that is
the length of the sequence. *)
let rec rev_and_compact l = function
[] -> l
| 1::tl ->
(match l with
n::tl' ->
if n < 0 then
rev_and_compact ((n - 1)::tl') tl
else
rev_and_compact ((-1)::l) tl
| [] -> rev_and_compact [-1] tl)
| a::tl ->
if a < 0 then
(match l with
n::tl' ->
if n < 0 then
rev_and_compact ((n + a)::tl') tl
else
rev_and_compact (a::l) tl
| [] -> rev_and_compact (a::l) tl)
else
rev_and_compact (a::l) tl;;
(*translates an int list into a centaur-tree --> SIGNED_INT_LIST *)
let translate_path l =
CT_signed_int_list
(List.map (function n -> CT_coerce_INT_to_SIGNED_INT (CT_int n))
(rev_and_compact [] l));;
(*translates a path and a goal into a centaur-tree --> RULE *)
let translate_goal (g:goal) =
CT_rule(translate_sign (evar_env g), translate_constr true (evar_env g) g.evar_concl);;
|
