1 (* Title: Specify-phase: specifying and modeling a problem or a subproblem. The
2 most important types are declared in mstools.sml.
3 TODO: allocate elements of Selem and of Stool appropriately
4 Author: Walther Neuper 991122, Mathias Lehnfeld
5 (c) due to copyright terms
7 signature SPECIFY_ELEMENT =
12 val res2str : term * term list -> string
13 type subs (* substitution as seen by learner. rename stubst_user ["(''bdv'', x)"]*)
14 type sube (* = subs. delete ! = stubst_user *)
15 type subte (* _sub_stitution as _t_erms of _e_qualities: revise ! [bdv = x] *)
16 type subst' (* substitution in isac-programs; rename subst_prog [(bdv, x)] *)
17 (*type subst for rewriting, in Rule (+?Isabelle); rename subst_rew [(bools, x)] *)
18 (* TODO use these types in functions below and elsewhere; rename below according to types *)
19 val subst'_to_sube : subst' -> TermC.as_string list (* e.g. rename to subst_user_of_prog *)
20 val subst_to_subst' : UnparseC.subst -> subst'
21 val subst'_to_subst : subst' -> (term * term) list
22 val sube2str : TermC.as_string list -> string
23 val sube2subst : theory -> TermC.as_string list -> (term * term) list
24 val sube2subte : TermC.as_string list -> term list
25 val subs2subst : theory -> TermC.as_string list -> (term * term) list
26 val subst2sube : (term * term) list -> TermC.as_string list (* for datatypes.sml *)
27 val subst2subs : (term * term) list -> TermC.as_string list
28 val subst2subs' : (term * term) list -> (string * string) list
29 val subte2sube : term list -> TermC.as_string list
31 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
32 val e_fmz : fmz_ * Spec.spec (* for datatypes.sml *)
33 val e_sube : TermC.as_string list
34 val e_subs : string list
35 val subte2subst : term list -> (term * term) list
36 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
38 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
40 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
41 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
45 structure Selem(**): SPECIFY_ELEMENT(**) =
51 linefeed o pair2str o (apsnd UnparseC.term) o (apfst UnparseC.term)))) s;
52 type fmz_ = TermC.as_string list;
53 (* a formalization of an example contains data
54 sufficient for mechanically finding the solution for the example.
55 FIXME.WN051014: dont store fmz = (_,spec) in the PblObj, this is done in origin *)
56 type fmz = fmz_ * Spec.spec;
57 val e_fmz = ([], Spec.empty_spec);
59 type result = term * term list
60 fun res2str (t, ts) = pair2str (UnparseC.term t, UnparseC.terms ts); (* for tests only *)
62 type subs = TermC.as_string list; (* substitution as seen by learner in tactics, in programs, etc.
63 questionable design. rename to stubst_user *)
64 val e_subs = ["(''bdv'', x)"]; (* for tests only *)
66 (* argument type of tac Rewrite_Inst *)
67 type sube = TermC.as_string list; (* = subs. delete *)
68 val e_sube = []: TermC.as_string list; (* for tests only *)
69 fun sube2str s = strs2str s;
71 type subte = term list; (* _sub_stitution as _t_erms of _e_qualities: revise ! *)
73 type subst' = term; (* substitution in isac-programs. rename to subst_prog
74 is "(char list * term) list", where term is Free ("xxx", _)
75 e.g. @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"} *)
76 fun subst'_to_sube sub = (sub
78 |> map HOLogic.dest_prod
79 |> map (fn (e1, e2) => (HOLogic.dest_string e1, UnparseC.term e2))
80 |> map (fn (e1, e2) => "(''" ^ e1 ^ "'', " ^ e2 ^ ")"): TermC.as_string list)
81 handle TERM _ => raise TERM ("subst'_to_sube: wrong argument ", [sub])
82 fun subst_to_subst' subst = subst
83 |> map (apfst TermC.free2str)
84 |> map (apfst HOLogic.mk_string)
85 |> map HOLogic.mk_prod
86 |> HOLogic.mk_list (HOLogic.mk_prodT (HOLogic.stringT, HOLogic.realT (*FIXME: 'a*)))
87 fun subst'_to_subst t = (t
89 |> map HOLogic.dest_prod
90 |> map (apfst HOLogic.dest_string))
91 |> map (apfst (fn e1 => (TermC.mk_Free (e1, HOLogic.realT))))
92 handle TERM _ => raise TERM ("subst'_to_subst: wrong argument ", [t])
93 val subte2sube = map UnparseC.term;
94 fun subst2subs subst_rew = (subst_rew
95 |> map (apsnd UnparseC.term)
96 |> map (apfst UnparseC.term)
97 |> map (apfst (enclose "''" "''")))
99 handle TERM _ => raise TERM ("subst2subs: wrong argument " ^ subst2str subst_rew, [])
100 fun subst2sube subst = map UnparseC.term (map HOLogic.mk_eq subst)
101 val subst2subs' = map ((apfst UnparseC.term) o (apsnd UnparseC.term));
102 fun subs2subst thy subs = (subs
103 |> map (TermC.parse_patt thy(*FIXME use context, get type of snd (e.g. x,y,z), copy to fst*))
104 |> map TermC.isapair2pair
105 |> map (apfst HOLogic.dest_string)
106 |> map (apfst (fn str => (TermC.mk_Free (str, HOLogic.realT)))))
107 handle TERM _ => raise TERM ("subs2subst: wrong argument " ^ strs2str' subs, [])
108 fun sube2subst thy s = map (TermC.dest_equals o (TermC.parse_patt thy)) s;
109 val sube2subte = map TermC.str2term;
110 val subte2subst = map HOLogic.dest_eq;