Walther@60767
|
1 |
(* Title: Specify/p-spec.sml
|
walther@59822
|
2 |
Author: Walther Neuper
|
walther@59822
|
3 |
(c) due to copyright terms
|
walther@59960
|
4 |
|
Walther@60772
|
5 |
Major parts will be dropped at switch to Isabelle/PIDE.
|
Walther@60782
|
6 |
Thus the switch to I_Model.T is prepared quick and dirty.
|
walther@59960
|
7 |
*)
|
walther@59822
|
8 |
|
walther@59984
|
9 |
signature PRESENTATION_SPECIFICATION =
|
walther@59822
|
10 |
sig
|
walther@60132
|
11 |
type record
|
walther@59995
|
12 |
(*/------- rename -------\*)
|
Walther@60773
|
13 |
datatype p_model =
|
walther@59960
|
14 |
Find of TermC.as_string list
|
walther@59960
|
15 |
| Given of TermC.as_string list
|
walther@59960
|
16 |
| Relate of TermC.as_string list
|
Walther@60773
|
17 |
|
Walther@60782
|
18 |
val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
|
Walther@60782
|
19 |
string * TermC.as_string -> I_Model.single
|
Walther@60782
|
20 |
val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
|
Walther@60782
|
21 |
(Model_Def.m_field * TermC.as_string) list -> I_Model.T
|
walther@59977
|
22 |
val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool
|
Walther@60773
|
23 |
val fstr2itm_: theory -> Model_Pattern.T -> Model_Def.m_field * string ->
|
Walther@60782
|
24 |
int list * bool * Model_Def.m_field * (I_Model.feedback * Position.T)
|
Walther@60773
|
25 |
val imodel2fstr: p_model list -> (string * TermC.as_string) list
|
walther@59977
|
26 |
val is_e_ts: term list -> bool
|
Walther@60782
|
27 |
val itms2fstr: Proof.context -> I_Model.single -> string * string
|
Walther@60782
|
28 |
val par2fstr: I_Model.single -> string * TermC.as_string
|
Walther@60782
|
29 |
val unknown_expl: ThyC.id -> Model_Pattern.T -> (Model_Def.m_field * string) list -> I_Model.T
|
Walther@60772
|
30 |
(*\----- from isac_test for Minisubpbl*)
|
Walther@60772
|
31 |
|
Walther@60772
|
32 |
\<^isac_test>\<open>
|
Walther@60772
|
33 |
(**)
|
wenzelm@60223
|
34 |
\<close>
|
walther@59995
|
35 |
(*\------- rename -------/*)
|
walther@59822
|
36 |
end
|
walther@59822
|
37 |
|
walther@59977
|
38 |
(**)
|
walther@59984
|
39 |
structure P_Spec(**): PRESENTATION_SPECIFICATION(**) =
|
walther@59822
|
40 |
struct
|
walther@59977
|
41 |
(**)
|
walther@59822
|
42 |
|
walther@60132
|
43 |
type record = {thy_id: ThyC.id, pbl_id: Problem.id, (* headline of Problem *)
|
walther@60132
|
44 |
givens: TermC.as_string list, wheres: TermC.as_string list, (* Model.T *)
|
walther@60132
|
45 |
find: TermC.as_string, relates: TermC.as_string list,
|
walther@60154
|
46 |
rthy_id: ThyC.id, rpbl_id: Problem.id, rmet_id: MethodC.id} (* References.T *)
|
walther@60132
|
47 |
|
walther@59822
|
48 |
fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
|
walther@59822
|
49 |
|
walther@59982
|
50 |
(** handle an input P_Specific'action **)
|
walther@59822
|
51 |
|
Walther@60773
|
52 |
datatype p_model =
|
walther@59865
|
53 |
Given of TermC.as_string list
|
walther@59977
|
54 |
(*Where is still not input*)
|
walther@59865
|
55 |
| Find of TermC.as_string list
|
walther@59865
|
56 |
| Relate of TermC.as_string list
|
walther@59822
|
57 |
|
walther@59822
|
58 |
fun is_e_ts [] = true
|
wenzelm@60309
|
59 |
| is_e_ts [Const (\<^const_name>\<open>Nil\<close>, _)] = true
|
walther@59822
|
60 |
| is_e_ts _ = false;
|
walther@59822
|
61 |
|
Walther@60782
|
62 |
fun appl_add' dI oris (model: I_Model.T) pbt (sel, ct) =
|
walther@59822
|
63 |
let
|
Walther@60676
|
64 |
val ctxt = Know_Store.get_via_last_thy dI |> Proof_Context.init_global;
|
walther@59822
|
65 |
in
|
Walther@60663
|
66 |
(*/------------ replace by ParseC.term_position ------------------\*)
|
Walther@60663
|
67 |
case ParseC.term_opt ctxt ct of
|
Walther@60663
|
68 |
(*\------------ replace by ParseC.term_position ------------------/*)
|
Walther@60782
|
69 |
NONE => (0, [], false, sel, (I_Model.Syn ct, Position.none))
|
walther@59822
|
70 |
| SOME t =>
|
Walther@60471
|
71 |
(case O_Model.contains ctxt sel oris t of
|
walther@59822
|
72 |
("", ori', all) =>
|
Walther@60773
|
73 |
(case I_Model.is_notyet_input ctxt model all ori' pbt of
|
Walther@60773
|
74 |
("", itm) => itm
|
Walther@60773
|
75 |
| (msg,_) => raise ERROR ("P_Spec.appl_add': " ^ msg))
|
walther@59822
|
76 |
| (_, (i, v, _, d, ts), _) =>
|
walther@59822
|
77 |
if is_e_ts ts
|
Walther@60782
|
78 |
then (i, v, false, sel, (I_Model.Inc (d, ts), Position.none))
|
Walther@60782
|
79 |
else (i, v, false, sel, (I_Model.Sup (d, ts), Position.none)))
|
walther@59822
|
80 |
end
|
walther@59822
|
81 |
|
Walther@60422
|
82 |
(* generate preliminary itm_ from a string (with field "#Given" etc.) *)
|
walther@59822
|
83 |
fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
|
walther@59822
|
84 |
fun fstr2itm_ thy pbt (f, str) =
|
walther@59822
|
85 |
let
|
Walther@60663
|
86 |
(*/------------ replace by ParseC.term_position ? ------------\*)
|
Walther@60663
|
87 |
val topt = ParseC.term_opt (Proof_Context.init_global thy) str
|
Walther@60663
|
88 |
(*\------------ replace by ParseC.term_position ? ------------/*)
|
walther@59822
|
89 |
in
|
walther@59822
|
90 |
case topt of
|
Walther@60782
|
91 |
NONE => ([], false, f, (I_Model.Syn str, Position.none))
|
walther@59822
|
92 |
| SOME ct =>
|
walther@59822
|
93 |
let
|
Walther@60422
|
94 |
val (d, ts) = Input_Descript.split ct
|
walther@59822
|
95 |
val popt = find_first (eq7 (f, d)) pbt
|
walther@59822
|
96 |
in
|
walther@59822
|
97 |
case popt of
|
Walther@60782
|
98 |
NONE => ([1](*??*), true(*??*), f, (I_Model.Sup (d, ts), Position.none))
|
Walther@60782
|
99 |
| SOME (f, (d, id)) => ([1], true, f, (I_Model.Cor (d, ts), Position.none))
|
walther@59822
|
100 |
end
|
walther@59822
|
101 |
end
|
walther@59822
|
102 |
|
walther@59822
|
103 |
(*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
|
walther@59822
|
104 |
fun unknown_expl dI pbt selcts =
|
walther@59822
|
105 |
let
|
Walther@60649
|
106 |
val thy = Know_Store.get_via_last_thy dI
|
Walther@60773
|
107 |
val its_ = map (fstr2itm_ thy pbt) selcts
|
Walther@60472
|
108 |
val its = O_Model.add_enumerate its_
|
walther@59822
|
109 |
in map flattup2 its end
|
walther@59822
|
110 |
|
Walther@60773
|
111 |
fun eq_dsc ((_, _, _, _, (itm_, _)), (_, _, _, _, (iitm_, _))) =
|
Walther@60782
|
112 |
(I_Model.descriptor itm_ = I_Model.descriptor iitm_)
|
Walther@60782
|
113 |
fun add itm (itms: I_Model.T) = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
|
walther@59822
|
114 |
fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
|
walther@59822
|
115 |
(*already present itms in model are being overwritten*)
|
Walther@60782
|
116 |
| appl_adds _ _ (model: I_Model.T) _ [] = model
|
Walther@60782
|
117 |
| appl_adds dI oris (model: I_Model.T) pbt (selct :: ss) =
|
Walther@60586
|
118 |
let val itm = appl_add' dI oris model pbt selct;
|
Walther@60766
|
119 |
in appl_adds dI oris (add itm model) pbt ss end
|
walther@59822
|
120 |
|
Walther@60782
|
121 |
fun par2fstr (_, _, _, f, (I_Model.Syn s, _)) = (f, s)
|
Walther@60676
|
122 |
| par2fstr itm = raise ERROR ("par2fstr: called with " ^
|
Walther@60782
|
123 |
I_Model.single_to_string (ContextC.for_ERROR ()) itm)
|
Walther@60776
|
124 |
|
Walther@60782
|
125 |
fun itms2fstr _ (_, _, _, f, (I_Model.Cor (d, ts), _)) = (f, Input_Descript.join''' (d, ts))
|
Walther@60782
|
126 |
| itms2fstr _ (_, _, _, f, (I_Model.Syn str, _)) = (f, str)
|
Walther@60782
|
127 |
| itms2fstr _ (_, _, _, f, (I_Model.Inc (d, ts), _)) = (f, Input_Descript.join''' (d,ts))
|
Walther@60782
|
128 |
| itms2fstr _ (_, _, _, f, (I_Model.Sup (d, ts), _)) = (f, Input_Descript.join''' (d, ts))
|
walther@59822
|
129 |
|
walther@59822
|
130 |
fun imodel2fstr iitems =
|
walther@59822
|
131 |
let
|
walther@59822
|
132 |
fun xxx is [] = is
|
walther@59822
|
133 |
| xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis
|
walther@59822
|
134 |
| xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis
|
walther@59822
|
135 |
| xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
|
walther@59822
|
136 |
in xxx [] iitems end;
|
walther@59822
|
137 |
|
walther@59822
|
138 |
|
walther@60132
|
139 |
(**)end (**)
|