wneuper@59577
|
1 |
(* Title: ../contextC.sml
|
wneuper@59577
|
2 |
Author: Walther Neuper, Mathias Lehnfeld
|
wneuper@59577
|
3 |
(c) due to copyright terms
|
wneuper@59577
|
4 |
*)
|
wneuper@59577
|
5 |
(* Extension to Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *)
|
wneuper@59577
|
6 |
signature CONTEXT_C =
|
wneuper@59577
|
7 |
sig
|
wneuper@59577
|
8 |
val declare_constraints : string -> Proof.context -> Proof.context
|
wneuper@59577
|
9 |
val declare_constraints' : term list -> Proof.context -> Proof.context
|
wneuper@59577
|
10 |
val get_assumptions : Proof.context -> term list
|
wneuper@59577
|
11 |
val insert_assumptions : term list -> Proof.context -> Proof.context
|
wneuper@59577
|
12 |
val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context
|
wneuper@59577
|
13 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
wneuper@59577
|
14 |
(*NONE*)
|
wneuper@59577
|
15 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
wneuper@59577
|
16 |
val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context
|
wneuper@59577
|
17 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
wneuper@59577
|
18 |
end
|
wneuper@59577
|
19 |
|
wneuper@59577
|
20 |
(* survey on handling contexts:
|
wneuper@59577
|
21 |
-------------------------------
|
wneuper@59577
|
22 |
theory is required for Pattern.match (and thus for Tactic.Rewrite* ), while
|
wneuper@59577
|
23 |
ctxt is required for parsing and for managing pre-conditions and assumptions.
|
wneuper@59577
|
24 |
* model-specify-phase:
|
wneuper@59577
|
25 |
* Tactic.Model_Problem does declare_constraints for parsing (in Tactic.Add_Given, etc)
|
wneuper@59577
|
26 |
("insert_assumptions pres" has to wait for completing Tactic.Add_Given, etc)
|
wneuper@59577
|
27 |
(Tactic.Refine_Problem uses theory NOT ctxt due to Pattern.match)
|
wneuper@59577
|
28 |
*
|
wneuper@59577
|
29 |
*
|
wneuper@59577
|
30 |
* solve-phase by Lucas-Interpretation:
|
wneuper@59577
|
31 |
* locate_input_tactic:
|
wneuper@59577
|
32 |
* Tactic.Apply_Method
|
wneuper@59577
|
33 |
* initialises ctxt (declare_constraints' + insert_assumptions pres) by init_scrstate
|
wneuper@59577
|
34 |
* in solve for root problem
|
wneuper@59577
|
35 |
* in begin_end_prog for subproblem
|
wneuper@59577
|
36 |
* Tactic.Rewrite* create assumptions; respective insert_assumptions is done by associate
|
wneuper@59577
|
37 |
* associate..Subproblem' returns ctxt ONLY with declare_constraints',
|
wneuper@59577
|
38 |
with insert_assumptions wait for Tactic.Apply_Method
|
wneuper@59577
|
39 |
* storing ctxt is done after return form locate_input_tactic
|
wneuper@59577
|
40 |
* determine_next_tactic:
|
wneuper@59577
|
41 |
* TODO initialises ctxt by TODO
|
wneuper@59577
|
42 |
* Tactic.Rewrite* create assumptions; respective insert_assumptions TODO
|
wneuper@59577
|
43 |
*
|
wneuper@59577
|
44 |
*
|
wneuper@59577
|
45 |
*
|
wneuper@59577
|
46 |
* locate_input_formula: follows sig. of determine_next_tactic
|
wneuper@59577
|
47 |
* changing from one method to another (in determine_next_tactic only):
|
wneuper@59577
|
48 |
* from method to sub-program: just add new preconditions of the guard
|
wneuper@59577
|
49 |
* locate_input_tactic: init_scrstate by begin_end_prog
|
wneuper@59577
|
50 |
* determine_next_tactic:
|
wneuper@59577
|
51 |
* from_subpbl_to_caller
|
wneuper@59577
|
52 |
* finishing a method:
|
wneuper@59577
|
53 |
* Tactic.Check_Postcond' uses ctxt for proving the post-condition (not yet implemented)
|
wneuper@59577
|
54 |
*
|
wneuper@59577
|
55 |
*
|
wneuper@59577
|
56 |
*
|
wneuper@59577
|
57 |
*
|
wneuper@59577
|
58 |
================================================================================================
|
wneuper@59577
|
59 |
call hierarchy
|
wneuper@59577
|
60 |
================================================================================================
|
wneuper@59577
|
61 |
|
wneuper@59577
|
62 |
locatetac
|
wneuper@59577
|
63 |
applicable_in (p, p_) pt (Tactic.Apply_Method pres
|
wneuper@59577
|
64 |
insert_assumptions
|
wneuper@59577
|
65 |
|
wneuper@59577
|
66 |
context_thy
|
wneuper@59577
|
67 |
applicable_in (p, p_) pt (Tactic.Apply_Method pres
|
wneuper@59577
|
68 |
insert_assumptions
|
wneuper@59577
|
69 |
|
wneuper@59577
|
70 |
|
wneuper@59577
|
71 |
|
wneuper@59577
|
72 |
|
wneuper@59577
|
73 |
|
wneuper@59577
|
74 |
|
wneuper@59577
|
75 |
generate1 _ (Tactic.Rewrite***
|
wneuper@59577
|
76 |
insert_assumptions
|
wneuper@59577
|
77 |
|
wneuper@59577
|
78 |
|
wneuper@59577
|
79 |
|
wneuper@59577
|
80 |
|
wneuper@59577
|
81 |
|
wneuper@59577
|
82 |
------------------------------------------------------------------------------------------------
|
wneuper@59577
|
83 |
solve phase before LI
|
wneuper@59577
|
84 |
------------------------------------------------------------------------------------------------
|
wneuper@59577
|
85 |
autocalc
|
wneuper@59577
|
86 |
all_modspec
|
wneuper@59577
|
87 |
declare_constraints'
|
wneuper@59577
|
88 |
complete_solve
|
wneuper@59577
|
89 |
all_modspec
|
wneuper@59577
|
90 |
declare_constraints'
|
wneuper@59577
|
91 |
|
wneuper@59577
|
92 |
all_solve
|
wneuper@59577
|
93 |
begin_end_prog (Tactic.Apply_Method'
|
wneuper@59577
|
94 |
init_scrstate
|
wneuper@59577
|
95 |
declare_constraints'
|
wneuper@59577
|
96 |
insert_assumptions
|
wneuper@59577
|
97 |
|
wneuper@59577
|
98 |
nxt_specify_
|
wneuper@59577
|
99 |
begin_end_prog (Tactic.Apply_Method'
|
wneuper@59577
|
100 |
init_scrstate
|
wneuper@59577
|
101 |
declare_constraints'
|
wneuper@59577
|
102 |
insert_assumptions
|
wneuper@59577
|
103 |
------------------------------------------------------------------------------------------------
|
wneuper@59577
|
104 |
LI
|
wneuper@59577
|
105 |
------------------------------------------------------------------------------------------------
|
wneuper@59577
|
106 |
solve ("Apply_Method" root-program
|
wneuper@59577
|
107 |
init_scrstate
|
wneuper@59577
|
108 |
declare_constraints'
|
wneuper@59577
|
109 |
insert_assumptions
|
wneuper@59577
|
110 |
locate_input_tactic
|
wneuper@59577
|
111 |
execute_progr_2
|
wneuper@59577
|
112 |
assy ..leaf sub-program
|
wneuper@59577
|
113 |
associate
|
wneuper@59577
|
114 |
declare_constraints'
|
wneuper@59577
|
115 |
applicable_in .. Tactic.Apply_Method pres
|
wneuper@59577
|
116 |
insert_assumptions
|
wneuper@59577
|
117 |
? generate1 (look in test with "from ... to..))
|
wneuper@59577
|
118 |
|
wneuper@59577
|
119 |
determine_next_tactic
|
wneuper@59577
|
120 |
execute_progr_1
|
wneuper@59577
|
121 |
appy ..leaf
|
wneuper@59577
|
122 |
stac2tac_
|
wneuper@59577
|
123 |
declare_constraints'
|
wneuper@59577
|
124 |
applicable_in (p, p_) pt (Tactic.Apply_Method pres
|
wneuper@59577
|
125 |
insert_assumptions
|
wneuper@59577
|
126 |
? generate1 (look in test with "from ... to..))
|
wneuper@59577
|
127 |
|
wneuper@59577
|
128 |
locate_input_formula uses determine_next_tactic
|
wneuper@59577
|
129 |
compare_step
|
wneuper@59577
|
130 |
all_modspec
|
wneuper@59577
|
131 |
declare_constraints'
|
wneuper@59577
|
132 |
begin_end_prog (Tactic.Apply_Method'
|
wneuper@59577
|
133 |
init_scrstate
|
wneuper@59577
|
134 |
declare_constraints'
|
wneuper@59577
|
135 |
insert_assumptions
|
wneuper@59577
|
136 |
------------------------------------------------------------------------------------------------
|
wneuper@59577
|
137 |
specification phase
|
wneuper@59577
|
138 |
------------------------------------------------------------------------------------------------
|
wneuper@59577
|
139 |
loc_specify_
|
wneuper@59577
|
140 |
specify (Tactic.Init_Proof'
|
wneuper@59577
|
141 |
prep_ori
|
wneuper@59577
|
142 |
declare_constraints
|
wneuper@59577
|
143 |
|
wneuper@59577
|
144 |
CalcTree
|
wneuper@59577
|
145 |
nxt_specify_init_calc
|
wneuper@59577
|
146 |
prep_ori
|
wneuper@59577
|
147 |
declare_constraints
|
wneuper@59577
|
148 |
|
wneuper@59577
|
149 |
modifyCalcHead
|
wneuper@59577
|
150 |
input_icalhd
|
wneuper@59577
|
151 |
prep_ori
|
wneuper@59577
|
152 |
declare_constraints
|
wneuper@59577
|
153 |
|
wneuper@59577
|
154 |
refine
|
wneuper@59577
|
155 |
refin'
|
wneuper@59577
|
156 |
prep_ori
|
wneuper@59577
|
157 |
declare_constraints
|
wneuper@59577
|
158 |
------------------------------------------------------------------------------------------------
|
wneuper@59577
|
159 |
unused ?!
|
wneuper@59577
|
160 |
------------------------------------------------------------------------------------------------
|
wneuper@59577
|
161 |
??
|
wneuper@59577
|
162 |
match_pbl
|
wneuper@59577
|
163 |
prep_ori
|
wneuper@59577
|
164 |
declare_constraints
|
wneuper@59577
|
165 |
??
|
wneuper@59577
|
166 |
from_pblobj'
|
wneuper@59577
|
167 |
init_scrstate
|
wneuper@59577
|
168 |
declare_constraints'
|
wneuper@59577
|
169 |
insert_assumptions
|
wneuper@59577
|
170 |
??
|
wneuper@59577
|
171 |
tac2tac_
|
wneuper@59577
|
172 |
applicable_in (p, p_) pt (Tactic.Apply_Method pres
|
wneuper@59577
|
173 |
insert_assumptions
|
wneuper@59577
|
174 |
|
wneuper@59577
|
175 |
*)
|
wneuper@59577
|
176 |
|
wneuper@59577
|
177 |
structure ContextC(**) : CONTEXT_C(**) =
|
wneuper@59577
|
178 |
struct
|
wneuper@59577
|
179 |
|
wneuper@59577
|
180 |
fun declare_constraints' ts ctxt = fold Variable.declare_constraints (flat (map TermC.vars ts)) ctxt;
|
wneuper@59577
|
181 |
(*WN110613 fun declare_constraints' shall replace fun declare_constraints*)
|
wneuper@59577
|
182 |
fun declare_constraints t ctxt =
|
wneuper@59577
|
183 |
let
|
wneuper@59577
|
184 |
fun get_vars ((v, T) :: vs) = (case raw_explode v |> Library.read_int of
|
wneuper@59577
|
185 |
(_, _ :: _) => (Free (v, T) :: get_vars vs)
|
wneuper@59577
|
186 |
| (_, [] ) => get_vars vs) (*filter out nums as long as we have Free ("123",_)*)
|
wneuper@59577
|
187 |
| get_vars [] = [];
|
wneuper@59577
|
188 |
val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
|
wneuper@59577
|
189 |
in fold Variable.declare_constraints ts ctxt end;
|
wneuper@59577
|
190 |
|
wneuper@59577
|
191 |
structure Context_Data = Proof_Data (type T = term list fun init _ = []);
|
wneuper@59577
|
192 |
fun get_assumptions ctxt = Context_Data.get ctxt
|
wneuper@59577
|
193 |
fun insert_assumptions asms = Context_Data.map (fn xs => distinct (asms @ xs))
|
wneuper@59577
|
194 |
|
wneuper@59577
|
195 |
(* transfer assumptions from one to another ctxt.
|
wneuper@59577
|
196 |
does NOT respect scope: in a calculation identifiers are unique.
|
wneuper@59577
|
197 |
but environments are scoped as usual in Luacs-interpretation.
|
wneuper@59577
|
198 |
WN110520 redo (1) take declare_constraints (2) with combinators*)
|
wneuper@59577
|
199 |
fun transfer_asms_from_to from_ctxt to_ctxt =
|
wneuper@59577
|
200 |
let
|
wneuper@59577
|
201 |
val to_vars = get_assumptions to_ctxt |> map TermC.vars |> flat
|
wneuper@59577
|
202 |
fun transfer [] to_ctxt = to_ctxt
|
wneuper@59577
|
203 |
| transfer (from_asm :: fas) to_ctxt =
|
wneuper@59577
|
204 |
if inter op = (TermC.vars from_asm) to_vars = []
|
wneuper@59577
|
205 |
then transfer fas to_ctxt
|
wneuper@59577
|
206 |
else transfer fas (insert_assumptions [from_asm] to_ctxt)
|
wneuper@59577
|
207 |
in transfer (get_assumptions from_ctxt) to_ctxt end
|
wneuper@59577
|
208 |
|
wneuper@59577
|
209 |
(* exported from a subproblem to the context of the calling method:
|
wneuper@59577
|
210 |
# 'scrval': the result of script interpretation and
|
wneuper@59577
|
211 |
# those assumptions in the subproblem wich contain a variable known
|
wneuper@59577
|
212 |
in the calling method. *)
|
wneuper@59577
|
213 |
fun from_subpbl_to_caller sub_ctxt scrval caller_ctxt =
|
wneuper@59577
|
214 |
let
|
wneuper@59577
|
215 |
val caller_ctxt = (scrval |> TermC.dest_list' |> insert_assumptions) caller_ctxt
|
wneuper@59577
|
216 |
in transfer_asms_from_to sub_ctxt caller_ctxt end;
|
wneuper@59577
|
217 |
|
wneuper@59577
|
218 |
end
|