ETCSprover/proofmanager.sml at master · u5943321/ETCSprover · GitHub

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
183
184
185
(*fun readfq [QUOTE s] = rapf s

structure Parse = struct val Term=readfq end
*)

structure proofmanager =
struct
open goalstack

exception NO_PROOFS;

open abbrev History

type tactic = abbrev.tactic
datatype proof = GOALSTACK of goalstack.gstk history
datatype proofs = PRFS of proof list;


fun initial_proofs() = PRFS[];

fun add p (PRFS L) = PRFS (p::L);


fun drop (PRFS (_::rst)) = PRFS rst
  | drop (PRFS []) = raise NO_PROOFS;

fun current_proof (PRFS (p::_)) = p
  | current_proof (PRFS []) = raise NO_PROOFS;


fun rotl (a::rst) = rst@[a]
  | rotl [] = raise simple_fail "rotl: empty list"

fun rotate_proofs i (PRFS []) = PRFS []
  | rotate_proofs i (PRFS L) =
      if i<0 then raise simple_fail "rotate_proofs: negative rotation"
      else if i > length L
           then raise simple_fail "rotate_proofs: more rotations than proofs"
           else PRFS(funpow i rotl L);


fun hd_opr f (PRFS (p::t)) = PRFS(f p::t)
  | hd_opr f otherwise = raise NO_PROOFS;

fun hd_proj f (PRFS (p::_)) = f p
  | hd_proj f otherwise = raise NO_PROOFS;


fun new_history_default obj = new_history{obj=obj, limit=15}
fun new_goalstack g = GOALSTACK(new_history_default (goalstack.new_goal g));

fun set_goal g = new_goalstack g;


fun backup (GOALSTACK s) = GOALSTACK(undo s)

fun set_backup i (GOALSTACK s) = GOALSTACK(set_limit s i)

fun restore (GOALSTACK s) = GOALSTACK(History.restore s)

fun save (GOALSTACK s) = GOALSTACK(History.save s)

fun forget_history (GOALSTACK s) = GOALSTACK(remove_past s)

fun expandf (tac:tactic.tactic) (GOALSTACK s) = GOALSTACK (apply (goalstack.expandf tac) s)

fun expand (tac:tactic.tactic) (GOALSTACK s) = GOALSTACK (apply (goalstack.e0 tac) s)

fun top_thm (GOALSTACK s) = project goalstack.proved_th s


(*
fun rotate i (GOALSTACK s) = GOALSTACK(apply (C goalstack.rotate i) s)

fun flatn i (GOALSTACK s) = GOALSTACK(apply (C goalStack.flatn i) s)
  | flatn i (GOALTREE t) = raise ERR "flatn"
                               "not implemented for goal trees";

may later
*)

fun restart (GOALSTACK s) = GOALSTACK (new_history_default (initialValue s))

(*---------------------------------------------------------------------------*)
(* Prettyprinting of goalstacks and goaltrees.                               *)
(*---------------------------------------------------------------------------*)

fun pp_proof (GOALSTACK s) = project goalstack.ppgstk s


end

structure proofManagerLib = struct
open abbrev proofmanager

type tactic = tactic.tactic

type proof = proofmanager.proof
type proofs = proofmanager.proofs


val the_proofs = ref (proofmanager.initial_proofs());

fun proofs() = !the_proofs;
fun top_proof() = proofmanager.current_proof(proofs());


(*
fun new_goalstack g f = GOALSTACK(new_history_default (goalStack.new_goal g f));

fun new_goalstack g f =
   (the_proofs := Manager.add (Manager.new_goalstack g f) (proofs());
    proofs());

fun set_goal g = new_goalstack g Lib.I;

fun g q = set_goal([],Parse.Term q);

*)

fun new_goalstack g =
   (the_proofs := proofmanager.add (proofmanager.new_goalstack g) (proofs());
    proofs());

fun set_goal g:proofmanager.proofs = new_goalstack g;


fun g q = set_goal(fvf (Parse.Term q),[],Parse.Term q);

fun restart() =
   (the_proofs := hd_opr proofmanager.restart (proofs());
    top_proof());

fun backup () =
   (the_proofs := proofmanager.hd_opr proofmanager.backup (proofs());
    top_proof());

fun restore () =
   (the_proofs := proofmanager.hd_opr proofmanager.restore (proofs());
    top_proof());

fun save () =
   (the_proofs := proofmanager.hd_opr proofmanager.save (proofs());
    top_proof());

val b = backup;

fun set_backup i =
  (the_proofs := proofmanager.hd_opr (proofmanager.set_backup i) (proofs()));

fun forget_history () =
  (the_proofs := proofmanager.hd_opr (proofmanager.forget_history) (proofs()));

fun restart() =
   (the_proofs := proofmanager.hd_opr proofmanager.restart (proofs());
    top_proof());


fun drop_all () =
    (the_proofs := proofmanager.initial_proofs(); !the_proofs)

fun expand (tac:tactic.tactic) =
   (the_proofs := proofmanager.hd_opr (proofmanager.expand tac) (proofs());
    top_proof())

val e = expand;

fun ppproof (GOALSTACK s) = project goalstack.ppgstk s

fun PPproof printdepth _ (prf:proofmanager.proof) =
    let
        val s = ppproof prf
        val SOME (pretty,_,_) = lower s ()
    in pretty
    end

val _ = PolyML.addPrettyPrinter PPproof

end