blob: 6e4782be09243dc0d5b08b016e7f54e1b15d4ce7 (
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
70
71
72
73
74
75
76
77
|
open Names;;
open Sign;;
open Util;;
open Term;;
open Pp;;
open Libobject;;
open Library;;
open Vernacinterp;;
open Tacmach;;
open Pfedit;;
open Parsing;;
open Evd;;
open Evarutil;;
open Xlate;;
open Vtp;;
open Ascent;;
open Environ;;
open Proof_type;;
(*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);;
|
