1.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed Nov 30 13:05:08 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Dec 12 18:08:13 2016 +0100
1.3 @@ -2,228 +2,76 @@
1.4 most important types are declared in mstools.sml.
1.5 Author: Walther Neuper 991122, Mathias Lehnfeld
1.6 (c) due to copyright terms
1.7 +*)
1.8 +signature CALC_HEAD =
1.9 +sig
1.10 + type calcstate
1.11 + type calcstate'
1.12 + datatype appl = Appl of tac_ | Notappl of string
1.13 + val nxt_specify_init_calc : fmz -> calcstate
1.14 + val specify : tac_ -> pos' -> cid -> ptree ->
1.15 + (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac * safe * ptree
1.16 + val nxt_specif : tac -> ptree * (pos * pos_) -> calcstate'
1.17 + val nxt_spec : pos_ -> bool -> ori list -> spec -> itm list * itm list ->
1.18 + (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> pos_ * tac
1.19
1.20 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.21 - 10 20 30 40 50 60 70 80
1.22 -*)
1.23 + val reset_calchead : ptree * pos' -> ptree * pos'
1.24 + val get_ocalhd : ptree * pos' -> ocalhd
1.25 + val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool
1.26 + val all_modspec : ptree * pos' -> ptree * pos'
1.27
1.28 -(* TODO interne Funktionen aus sig entfernen *)
1.29 -signature CALC_HEAD =
1.30 - sig
1.31 - datatype additm = Add of SpecifyTools.itm | Err of string
1.32 - val all_dsc_in : SpecifyTools.itm_ list -> Term.term list
1.33 - val all_modspec : ptree * pos' -> ptree * pos'
1.34 - datatype appl = Appl of tac_ | Notappl of string
1.35 - val appl_add :
1.36 - Proof.context ->
1.37 - string ->
1.38 - SpecifyTools.ori list ->
1.39 - SpecifyTools.itm list ->
1.40 - (string * (Term.term * Term.term)) list -> cterm' -> additm
1.41 - type calcstate
1.42 - type calcstate'
1.43 - val chk_vars : term ppc -> string * Term.term list
1.44 - val chktyp :
1.45 - theory -> int * term list * term list -> term
1.46 - val chktyps :
1.47 - theory -> term list * term list -> term list
1.48 - val complete_metitms :
1.49 - SpecifyTools.ori list ->
1.50 - SpecifyTools.itm list ->
1.51 - SpecifyTools.itm list -> pat list -> SpecifyTools.itm list
1.52 - val complete_mod_ : ori list * pat list * pat list * itm list ->
1.53 - itm list * itm list
1.54 - val complete_mod : ptree * pos' -> ptree * (pos * pos_)
1.55 - val complete_spec : ptree * pos' -> ptree * pos'
1.56 - val cpy_nam :
1.57 - pat list -> preori list -> pat -> preori
1.58 - val e_calcstate : calcstate
1.59 - val e_calcstate' : calcstate'
1.60 - val eq1 : ''a -> 'b * (''a * 'c) -> bool
1.61 - val eq3 :
1.62 - ''a -> Term.term -> 'b * 'c * 'd * ''a * SpecifyTools.itm_ -> bool
1.63 - val eq4 : ''a -> 'b * ''a list * 'c * 'd * 'e -> bool
1.64 - val eq5 :
1.65 - 'a * 'b * 'c * 'd * SpecifyTools.itm_ ->
1.66 - 'e * 'f * 'g * Term.term * 'h -> bool
1.67 - val eq_dsc : SpecifyTools.itm * SpecifyTools.itm -> bool
1.68 - val eq_pos' : ''a * pos_ -> ''a * pos_ -> bool
1.69 - val f_mout : theory -> mout -> Term.term
1.70 - val filter_outs :
1.71 - SpecifyTools.ori list ->
1.72 - SpecifyTools.itm list -> SpecifyTools.ori list
1.73 - val filter_pbt :
1.74 - SpecifyTools.ori list ->
1.75 - ('a * (Term.term * 'b)) list -> SpecifyTools.ori list
1.76 - val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
1.77 - val foldr1 : ('a * 'a -> 'a) -> 'a list -> 'a
1.78 - val form : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
1.79 - val formres : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
1.80 - val gen_ins' : ('a * 'a -> bool) -> 'a * 'a list -> 'a list
1.81 - val get_formress :
1.82 - (string * (pos * pos_) * Term.term) list list ->
1.83 - pos -> ptree list -> (string * (pos * pos_) * Term.term) list
1.84 - val get_forms :
1.85 - (string * (pos * pos_) * Term.term) list list ->
1.86 - posel list -> ptree list -> (string * (pos * pos_) * Term.term) list
1.87 - val get_interval : pos' -> pos' -> int -> ptree -> (pos' * term) list
1.88 - val get_ocalhd : ptree * pos' -> ocalhd
1.89 - val get_spec_form : tac_ -> pos' -> ptree -> mout
1.90 - val geti_ct :
1.91 - theory ->
1.92 - SpecifyTools.ori -> SpecifyTools.itm -> string * cterm'
1.93 - val getr_ct : theory -> SpecifyTools.ori -> string * cterm'
1.94 - val has_list_type : Term.term -> bool
1.95 - val header : pos_ -> pblID -> metID -> pblmet
1.96 - val insert_ppc :
1.97 - theory ->
1.98 - int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
1.99 - SpecifyTools.itm list -> SpecifyTools.itm list
1.100 - val insert_ppc' :
1.101 - SpecifyTools.itm -> SpecifyTools.itm list -> SpecifyTools.itm list
1.102 - val is_complete_mod : ptree * pos' -> bool
1.103 - val is_complete_mod_ : SpecifyTools.itm list -> bool
1.104 - val is_complete_modspec : ptree * pos' -> bool
1.105 - val is_complete_spec : ptree * pos' -> bool
1.106 - val is_copy_named : 'a * ('b * Term.term) -> bool
1.107 - val is_copy_named_idstr : string -> bool
1.108 - val is_error : SpecifyTools.itm_ -> bool
1.109 - val is_field_correct : ''a -> ''b -> (''a * ''b list) list -> bool
1.110 - val is_known :
1.111 - Proof.context ->
1.112 - string ->
1.113 - SpecifyTools.ori list ->
1.114 - Term.term -> string * SpecifyTools.ori * Term.term list
1.115 - val is_list_type : Term.typ -> bool
1.116 - val is_notyet_input :
1.117 - Proof.context ->
1.118 - SpecifyTools.itm list ->
1.119 - Term.term list ->
1.120 - SpecifyTools.ori ->
1.121 - ('a * (Term.term * Term.term)) list -> string * SpecifyTools.itm
1.122 - val is_parsed : SpecifyTools.itm_ -> bool
1.123 - val is_untouched : SpecifyTools.itm -> bool
1.124 - val matc :
1.125 - theory ->
1.126 - pat list ->
1.127 - Term.term list ->
1.128 - (int list * string * Term.term * Term.term list) list ->
1.129 - (int list * string * Term.term * Term.term list) list
1.130 - val match_ags :
1.131 - theory -> pat list -> Term.term list -> SpecifyTools.ori list
1.132 - val oris2fmz_vals : ori list -> string list * term list
1.133 - val maxl : int list -> int
1.134 - val match_ags_msg : string list -> Term.term -> Term.term list -> unit
1.135 - val memI : ''a list -> ''a -> bool
1.136 - val mk_additem : string -> cterm' -> tac
1.137 - val mk_delete : theory -> string -> SpecifyTools.itm_ -> tac
1.138 - val mtc :
1.139 - theory -> pat -> Term.term -> SpecifyTools.preori option
1.140 - val nxt_add :
1.141 - theory ->
1.142 - SpecifyTools.ori list ->
1.143 - (string * (Term.term * 'a)) list ->
1.144 - SpecifyTools.itm list -> (string * cterm') option
1.145 - val nxt_model_pbl : tac_ -> ptree * (int list * pos_) -> tac_
1.146 - val nxt_spec :
1.147 - pos_ ->
1.148 - bool ->
1.149 - SpecifyTools.ori list ->
1.150 - spec ->
1.151 - SpecifyTools.itm list * SpecifyTools.itm list ->
1.152 - (string * (Term.term * 'a)) list * (string * (Term.term * 'b)) list ->
1.153 - spec -> pos_ * tac
1.154 - val nxt_specif : tac -> ptree * (int list * pos_) -> calcstate'
1.155 - val nxt_specif_additem :
1.156 - string -> cterm' -> ptree * (int list * pos_) -> calcstate'
1.157 - val nxt_specify_init_calc : fmz -> calcstate
1.158 - val ocalhd_complete :
1.159 - SpecifyTools.itm list ->
1.160 - (bool * Term.term) list -> domID * pblID * metID -> bool
1.161 - val ori2Coritm :
1.162 - pat list -> ori -> itm
1.163 - val ori_2itm :
1.164 - SpecifyTools.itm_ ->
1.165 - Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm
1.166 - val overwrite_ppc :
1.167 - theory ->
1.168 - int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
1.169 - SpecifyTools.itm list ->
1.170 - (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list
1.171 - val parse_ok : SpecifyTools.itm_ list -> bool
1.172 - val posform2str : pos' * ptform -> string
1.173 - val posforms2str : (pos' * ptform) list -> string
1.174 - val posterms2str : (pos' * term) list -> string (*tests only*)
1.175 - val ppc135list : 'a SpecifyTools.ppc -> 'a list
1.176 - val ppc2list : 'a SpecifyTools.ppc -> 'a list
1.177 - val pt_extract :
1.178 - ptree * (int list * pos_) ->
1.179 - ptform * tac option * Term.term list
1.180 - val pt_form : ppobj -> ptform
1.181 - val pt_model : ppobj -> pos_ -> ptform
1.182 - val reset_calchead : ptree * pos' -> ptree * pos'
1.183 - val seek_oridts :
1.184 - Proof.context ->
1.185 - string ->
1.186 - Term.term * Term.term list ->
1.187 - (int * SpecifyTools.vats * string * Term.term * Term.term list) list
1.188 - -> string * SpecifyTools.ori * Term.term list
1.189 - val seek_orits :
1.190 - Proof.context ->
1.191 - string ->
1.192 - Term.term list ->
1.193 - (int * SpecifyTools.vats * string * Term.term * Term.term list) list
1.194 - -> string * SpecifyTools.ori * Term.term list
1.195 - val seek_ppc :
1.196 - int -> SpecifyTools.itm list -> SpecifyTools.itm option
1.197 - val show_pt : ptree -> unit
1.198 - val some_spec : spec -> spec -> spec
1.199 - val specify :
1.200 - tac_ ->
1.201 - pos' ->
1.202 - cid ->
1.203 - ptree ->
1.204 - (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac *
1.205 - safe * ptree
1.206 - val specify_additem :
1.207 - string ->
1.208 - cterm' * 'a ->
1.209 - int list * pos_ ->
1.210 - 'b ->
1.211 - ptree ->
1.212 - (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
1.213 - val tag_form : theory -> term * term -> term
1.214 - val test_types : Proof.context -> Term.term * Term.term list -> string
1.215 - val typeless : Term.term -> Term.term
1.216 - val unbound_ppc : term SpecifyTools.ppc -> Term.term list
1.217 - val vals_of_oris : SpecifyTools.ori list -> Term.term list
1.218 - val variants_in : Term.term list -> int
1.219 - val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list
1.220 - val vars_of_pbl_' : ('a * ('b * Term.term)) list -> Term.term list
1.221 - end
1.222 -
1.223 + val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list
1.224 + val insert_ppc' : itm -> itm list -> itm list
1.225
1.226 + val complete_mod : ptree * pos' -> ptree * pos'
1.227 + val is_complete_mod : ptree * pos' -> bool
1.228 + val complete_spec : ptree * pos' -> ptree * pos'
1.229 + val is_complete_spec : ptree * pos' -> bool
1.230 + val some_spec : spec -> spec -> spec
1.231 + (* these could go to Ctree ..*)
1.232 + val show_pt : ptree -> unit
1.233 + val pt_extract : ptree * (posel list * pos_) -> ptform * tac option * term list
1.234 + val get_interval : int list * pos_ -> pos' -> int -> ptree -> (pos' * term) list
1.235
1.236 + val match_ags : theory -> pat list -> term list -> ori list
1.237 + val match_ags_msg : pblID -> term -> term list -> unit
1.238 + val oris2fmz_vals : ori list -> string list * term list
1.239 + val vars_of_pbl_' : ('a * ('b * term)) list -> term list
1.240 + val is_known : Proof.context -> string -> ori list -> term -> string * ori * term list
1.241 + val is_notyet_input : Proof.context -> itm list -> term list -> ori -> ('a * (term * term)) list
1.242 + -> string * itm
1.243 + val e_calcstate' : calcstate'
1.244 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.245 + val vals_of_oris : ori list -> term list
1.246 + val is_error : itm_ -> bool
1.247 + val is_copy_named : 'a * ('b * term) -> bool
1.248 + val ori2Coritm : pat list -> ori -> itm
1.249 + val ppc2list : 'a ppc -> 'a list
1.250 + val is_copy_named_idstr : string -> bool
1.251 + val matc : theory -> (string * (term * term)) list -> term list -> preori list -> preori list
1.252 + val mtc : theory -> pat -> term -> preori option
1.253 + val cpy_nam : pat list -> preori list -> pat -> preori
1.254 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.255 +end
1.256
1.257 -
1.258 -structure CalcHead (**): CALC_HEAD(**) =
1.259 -
1.260 +structure Chead(**): CALC_HEAD(**) =
1.261 struct
1.262
1.263 (* datatypes *)
1.264
1.265 -(*.the state wich is stored after each step of calculation; it contains
1.266 +(* the state wich is stored after each step of calculation; it contains
1.267 the calc-state and a list of [tac,istate](="tacis") to be applied next.
1.268 the last_elem tacis is the first to apply to the calc-state and
1.269 the (only) one shown to the front-end as the 'proposed tac'.
1.270 the calc-state resulting from the application of tacis is not stored,
1.271 because the tacis hold enough information for efficiently rebuilding
1.272 - this state just by "fun generate ".*)
1.273 + this state just by "fun generate "
1.274 +*)
1.275 type calcstate =
1.276 - (ptree * pos') * (*the calc-state to which the tacis could be applied*)
1.277 - (taci list); (*ev. several (hidden) steps;
1.278 - in REVERSE order: first tac_ to apply is last_elem*)
1.279 -val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]):calcstate;
1.280 + (ptree * pos') * (* the calc-state to which the tacis could be applied *)
1.281 + (taci list) (* ev. several (hidden) steps;
1.282 + in REVERSE order: first tac_ to apply is last_elem *)
1.283 +val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]) : calcstate;
1.284
1.285 (*the state used during one calculation within the mathengine; it contains
1.286 a list of [tac,istate](="tacis") which generated the the calc-state;
1.287 @@ -235,240 +83,122 @@
1.288 because the tacis hold enought information for efficiently rebuilding
1.289 this state just by "fun generate ".*)
1.290 type calcstate' =
1.291 - taci list * (*cas. several (hidden) steps;
1.292 - in REVERSE order: first tac_ to apply is last_elem*)
1.293 - pos' list * (*a "continuous" sequence of pos',
1.294 - deleted by application of taci list*)
1.295 - (ptree * pos'); (*the calc-state resulting from the application of tacis*)
1.296 + taci list * (* cas. several (hidden) steps;
1.297 + in REVERSE order: first tac_ to apply is last_elem*)
1.298 + pos' list * (* a "continuous" sequence of pos', deleted by application of taci list*)
1.299 + (ptree * pos') (* the calc-state resulting from the application of tacis*)
1.300 val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
1.301
1.302 -(*FIXXXME.WN020430 intermediate hack for fun ass_up*)
1.303 -fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (Thm.term_of o the o (parse thy)) f
1.304 - | f_mout thy _ = error "f_mout: not called with formula";
1.305 +(* FIXXXME.WN020430 intermediate hack for fun ass_up *)
1.306 +fun f_mout thy (Form' (FormKF (_, _, _, _, f))) = (Thm.term_of o the o (parse thy)) f
1.307 + | f_mout _ _ = error "f_mout: not called with formula";
1.308
1.309 +(* is the calchead complete ? *)
1.310 +fun ocalhd_complete its pre (dI, pI, mI) =
1.311 + foldl and_ (true, map #3 its) andalso
1.312 + foldl and_ (true, map #1 pre) andalso
1.313 + dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID
1.314
1.315 -(*.is the calchead complete ?.*)
1.316 -fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) =
1.317 - foldl and_ (true, map #3 its) andalso
1.318 - foldl and_ (true, map #1 pre) andalso
1.319 - dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID;
1.320 -
1.321 -(*["BOOL (1+x=2)","REAL x"] --match_ags--> oris
1.322 - --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"]*)
1.323 +(* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris
1.324 + --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
1.325 fun oris2fmz_vals oris =
1.326 - let fun ori2fmz_vals ((_,_,_,dsc,ts):ori) =
1.327 - ((term2str o comp_dts') (dsc, ts), last_elem ts)
1.328 - handle _ => error ("ori2fmz_env called with "^terms2str ts)
1.329 - in (split_list o (map ori2fmz_vals)) oris end;
1.330 + let fun ori2fmz_vals ((_, _, _, dsc, ts): ori) =
1.331 + ((term2str o comp_dts') (dsc, ts), last_elem ts)
1.332 + handle _ => error ("ori2fmz_env called with " ^ terms2str ts)
1.333 + in (split_list o (map ori2fmz_vals)) oris end
1.334
1.335 (* make a term 'typeless' for comparing with another 'typeless' term;
1.336 'type-less' usually is illtyped *)
1.337 -fun typeless (Const(s,_)) = (Const(s,e_type))
1.338 - | typeless (Free(s,_)) = (Free(s,e_type))
1.339 - | typeless (Var(n,_)) = (Var(n,e_type))
1.340 +fun typeless (Const (s, _)) = (Const (s, e_type))
1.341 + | typeless (Free (s, _)) = (Free (s, e_type))
1.342 + | typeless (Var (n, _)) = (Var (n, e_type))
1.343 | typeless (Bound i) = (Bound i)
1.344 - | typeless (Abs(s,_,t)) = Abs(s,e_type, typeless t)
1.345 - | typeless (t1 $ t2) = (typeless t1) $ (typeless t2);
1.346 -(*
1.347 -> val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
1.348 -> val (_,t1) = split_dsc_t hs (Thm.term_of ct);
1.349 -> val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
1.350 -> val (_,t2) = split_dsc_t hs (Thm.term_of ct);
1.351 -> typeless t1 = typeless t2;
1.352 -val it = true : bool
1.353 -*)
1.354 + | typeless (Abs (s, _,t)) = Abs(s, e_type, typeless t)
1.355 + | typeless (t1 $ t2) = (typeless t1) $ (typeless t2)
1.356
1.357 -
1.358 -
1.359 -(*.to an input (d,ts) find the according ori and insert the ts.*)
1.360 -(*WN.11.03: + dont take first inter<>[]*)
1.361 -fun seek_oridts ctxt sel (d,ts) [] =
1.362 +(* to an input (d,ts) find the according ori and insert the ts)
1.363 + WN.11.03: + dont take first inter<>[] *)
1.364 +fun seek_oridts ctxt sel (d, ts) [] =
1.365 ("seek_oridts: input ('" ^
1.366 - (term_to_string' ctxt (comp_dts (d,ts))) ^ "') not found in oris (typed)",
1.367 + (term_to_string' ctxt (comp_dts (d, ts))) ^ "') not found in oris (typed)",
1.368 (0, [], sel, d, ts),
1.369 [])
1.370 - | seek_oridts ctxt sel (d,ts) ((id, vat, sel', d', ts')::oris) =
1.371 - if sel = sel' andalso d = d' andalso (inter op = ts ts') <> [] then
1.372 - ("", (id, vat, sel, d, inter op = ts ts'), ts') else
1.373 - seek_oridts ctxt sel (d, ts) oris;
1.374 + | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
1.375 + if sel = sel' andalso d = d' andalso (inter op = ts ts') <> []
1.376 + then ("", (id, vat, sel, d, inter op = ts ts'), ts')
1.377 + else seek_oridts ctxt sel (d, ts) oris
1.378
1.379 -(*.to an input (_,ts) find the according ori and insert the ts.*)
1.380 -fun seek_orits ctxt sel ts [] =
1.381 +(* to an input (_,ts) find the according ori and insert the ts *)
1.382 +fun seek_orits ctxt _ ts [] =
1.383 ("seek_orits: input (_, '" ^ strs2str (map (term_to_string' ctxt) ts) ^
1.384 "') not found in oris (typed)", e_ori_, [])
1.385 - | seek_orits ctxt sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
1.386 + | seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: (oris: ori list)) =
1.387 if sel = sel' andalso (inter op = ts ts') <> []
1.388 - then if sel = sel'
1.389 - then ("", (id,vat,sel,d, inter op = ts ts'):ori, ts')
1.390 - else (((strs2str' o map (term_to_string' ctxt)) ts) ^ " not for " ^ sel, e_ori_, [])
1.391 - else seek_orits ctxt sel ts oris;
1.392 -(* false
1.393 -> val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
1.394 -> seek_orits thy sel ts [(id,vat,sel',d,ts')];
1.395 -uncaught exception TYPE
1.396 -> seek_orits thy sel ts [];
1.397 -uncaught exception TYPE
1.398 -*)
1.399 + then
1.400 + if sel = sel'
1.401 + then ("", (id, vat, sel, d, inter op = ts ts'): ori, ts')
1.402 + else (((strs2str' o map (term_to_string' ctxt)) ts) ^ " not for " ^ sel, e_ori_, [])
1.403 + else seek_orits ctxt sel ts oris
1.404
1.405 -(*find_first item with #1 equal to id*)
1.406 -fun seek_ppc id [] = NONE
1.407 - | seek_ppc id (p::(ppc:itm list)) =
1.408 - if id = #1 p then SOME p else seek_ppc id ppc;
1.409 +(* find_first item with #1 equal to id *)
1.410 +fun seek_ppc _ [] = NONE
1.411 + | seek_ppc id (p :: (ppc: itm list)) = if id = #1 p then SOME p else seek_ppc id ppc
1.412
1.413 +datatype appl =
1.414 + Appl of tac_ (* tactic is applicable at a certain position in the Ctree *)
1.415 +| Notappl of string (* tactic is NOT applicable *)
1.416
1.417 -datatype appl = Appl of tac_ | Notappl of string;
1.418 -
1.419 -fun ppc2list ({Given=gis,Where=whs,Find=fis,
1.420 - With=wis,Relate=res}: 'a ppc) =
1.421 - gis @ whs @ fis @ wis @ res;
1.422 -fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =
1.423 - gis @ fis @ res;
1.424 -
1.425 -
1.426 -
1.427 +fun ppc2list ({Given = gis, Where = whs, Find = fis, With = wis, Relate = res}: 'a ppc) =
1.428 + gis @ whs @ fis @ wis @ res
1.429 +fun ppc135list ({Given = gis, Find = fis, Relate = res, ...}: 'a ppc) = gis @ fis @ res
1.430
1.431 (* get the number of variants in a problem in 'original',
1.432 assumes equal descriptions in immediate sequence *)
1.433 fun variants_in ts =
1.434 - let fun eq(x,y) = head_of x = head_of y;
1.435 - fun cnt eq [] y n = ([n],[])
1.436 - | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)
1.437 - else ([n], x::xs);
1.438 - fun coll eq xs [] = xs
1.439 - | coll eq xs (y::ys) =
1.440 - let val (n,ys') = cnt eq (y::ys) y 0;
1.441 - in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
1.442 - val vts = subtract op = [1] (distinct (coll eq [] ts));
1.443 - in case vts of [] => 1 | [n] => n
1.444 - | _ => error "different variants in formalization" end;
1.445 -(*
1.446 -> cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
1.447 -val it = ([3],[4,5,5,5,5,5]) : int list * int list
1.448 -> coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
1.449 -val it = [1,3,1,5] : int list
1.450 -*)
1.451 + let
1.452 + fun eq (x, y) = head_of x = head_of y
1.453 + fun cnt _ [] _ n = ([n], [])
1.454 + | cnt eq (x :: xs) y n = if eq (x, y) then cnt eq xs y (n + 1) else ([n], x :: xs)
1.455 + fun coll _ xs [] = xs
1.456 + | coll eq xs (y :: ys) =
1.457 + let val (n, ys') = cnt eq (y :: ys) y 0
1.458 + in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end
1.459 + val vts = subtract op = [1] (distinct (coll eq [] ts))
1.460 + in
1.461 + case vts of
1.462 + [] => 1
1.463 + | [n] => n
1.464 + | _ => error "different variants in formalization"
1.465 + end
1.466
1.467 -fun is_list_type (Type("List.list",_)) = true
1.468 - | is_list_type _ = false;
1.469 -(* fun destr (Type(str,sort)) = (str,sort);
1.470 -> val (SOME ct) = parse thy "lll::real list";
1.471 -> val ty = (#T o rep_cterm) ct;
1.472 -> is_list_type ty;
1.473 -val it = true : bool
1.474 -> destr ty;
1.475 -val it = ("List.list",["RealDef.real"]) : string * typ list
1.476 -> atomty ((#t o rep_cterm) ct);
1.477 -*** -------------
1.478 -*** Free ( lll, real list)
1.479 -val it = () : unit
1.480 -
1.481 -> val (SOME ct) = parse thy "[lll::real]";
1.482 -> val ty = (#T o rep_cterm) ct;
1.483 -> is_list_type ty;
1.484 -val it = true : bool
1.485 -> destr ty;
1.486 -val it = ("List.list",["'a"]) : string * typ list
1.487 -> atomty ((#t o rep_cterm) ct);
1.488 -*** -------------
1.489 -*** Const ( List.list.Cons, [real, real list] => real list)
1.490 -*** Free ( lll, real)
1.491 -*** Const ( List.list.Nil, real list)
1.492 -
1.493 -> val (SOME ct) = parse thy "lll";
1.494 -> val ty = (#T o rep_cterm) ct;
1.495 -> is_list_type ty;
1.496 -val it = false : bool *)
1.497 -
1.498 -
1.499 -fun has_list_type (Free(_,T)) = is_list_type T
1.500 - | has_list_type _ = false;
1.501 -(*
1.502 -> val (SOME ct) = parse thy "lll::real list";
1.503 -> has_list_type (Thm.term_of ct);
1.504 -val it = true : bool
1.505 -> val (SOME ct) = parse thy "[lll::real]";
1.506 -> has_list_type (Thm.term_of ct);
1.507 -val it = false : bool *)
1.508 -
1.509 +fun is_list_type (Type ("List.list", _)) = true
1.510 + | is_list_type _ = false
1.511 +fun has_list_type (Free (_, T)) = is_list_type T
1.512 + | has_list_type _ = false
1.513 fun is_parsed (Syn _) = false
1.514 - | is_parsed _ = true;
1.515 -fun parse_ok its = foldl and_ (true, map is_parsed its);
1.516 + | is_parsed _ = true
1.517 +fun parse_ok its = foldl and_ (true, map is_parsed its)
1.518
1.519 fun all_dsc_in itm_s =
1.520 let
1.521 - fun d_in (Cor ((d,_),_)) = [d]
1.522 - | d_in (Syn c) = []
1.523 - | d_in (Typ c) = []
1.524 + fun d_in (Cor ((d, _), _)) = [d]
1.525 + | d_in (Syn _) = []
1.526 + | d_in (Typ _) = []
1.527 | d_in (Inc ((d,_),_)) = [d]
1.528 | d_in (Sup (d,_)) = [d]
1.529 - | d_in (Mis (d,_)) = [d];
1.530 - in (flat o (map d_in)) itm_s end;
1.531 + | d_in (Mis (d,_)) = [d]
1.532 + | d_in i = error ("all_dsc_in: uncovered case with " ^ itm_2str i)
1.533 + in (flat o (map d_in)) itm_s end;
1.534
1.535 -(* 30.1.00 ---
1.536 -fun is_Syn (Syn _) = true
1.537 - | is_Syn (Typ _) = true
1.538 - | is_Syn _ = false;
1.539 - --- *)
1.540 -fun is_error (Cor (_,ts)) = false
1.541 - | is_error (Sup (_,ts)) = false
1.542 - | is_error (Inc (_,ts)) = false
1.543 - | is_error (Mis (_,ts)) = false
1.544 - | is_error _ = true;
1.545 +fun is_error (Cor _) = false
1.546 + | is_error (Sup _) = false
1.547 + | is_error (Inc _) = false
1.548 + | is_error (Mis _) = false
1.549 + | is_error _ = true
1.550
1.551 -(* 30.1.00 ---
1.552 -fun ct_in (Syn (c)) = c
1.553 - | ct_in (Typ (c)) = c
1.554 - | ct_in _ = error "ct_in called for Cor .. Sup";
1.555 - --- *)
1.556 -
1.557 -(*#############################################################*)
1.558 -(*#############################################################*)
1.559 -(* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
1.560 -
1.561 -
1.562 -(* testdaten besorgen:
1.563 - use"test-coil-kernel.sml";
1.564 - val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) =
1.565 - get_obj I pt p;
1.566 - *)
1.567 -
1.568 -(* given oris, ppc,
1.569 - variant V: oris union ppc => int, id ID: oris union ppc => int
1.570 -
1.571 - ppc is_complete ==
1.572 - EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i
1.573 -
1.574 - and
1.575 - @vt = max sum(i : ppc) V i
1.576 -*)
1.577 -
1.578 -
1.579 -
1.580 -(*
1.581 -> ((vts_cnt (vts_in itms))) itms;
1.582 -
1.583 -
1.584 -
1.585 ----^^--test 10.3.
1.586 -> val vts = vts_in itms;
1.587 -val vts = [1,2,3] : int list
1.588 -> val nvts = vts_cnt vts itms;
1.589 -val nvts = [(1,6),(2,5),(3,7)] : (int * int) list
1.590 -> val mx = max2 nvts;
1.591 -val mx = (3,7) : int * int
1.592 -> val v = max_vt itms;
1.593 -val v = 3 : int
1.594 ---------------------------
1.595 ->
1.596 -*)
1.597 -
1.598 -(*.get the first term in ts from ori.*)
1.599 -(* val (_,_,fd,d,ts) = hd miss;
1.600 - *)
1.601 +(* get the first term in ts from ori *)
1.602 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
1.603 - (fd, ((term_to_string''' thy) o comp_dts) (d,[hd ts]) : cterm');
1.604 -(* val t = comp_dts (d,[hd ts]);
1.605 - *)
1.606 + (fd, ((term_to_string''' thy) o comp_dts) (d,[hd ts]) : cterm')
1.607
1.608 (* get a term from ori, notyet input in itm.
1.609 the term from ori is thrown back to a string in order to reuse
1.610 @@ -477,16 +207,11 @@
1.611 (fd, ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm')
1.612
1.613 (* in FE dsc, not dat: this is in itms ...*)
1.614 -fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
1.615 - | is_untouched _ = false;
1.616 -
1.617 +fun is_untouched ((_, _, false, _, Inc ((_, []), _)): itm) = true
1.618 + | is_untouched _ = false
1.619
1.620 (* select an item in oris, notyet input in itms
1.621 (precondition: in itms are only Cor, Sup, Inc) *)
1.622 -local infix mem;
1.623 -fun x mem [] = false
1.624 - | x mem (y :: ys) = x = y orelse x mem ys;
1.625 -in
1.626 (*args of nxt_add
1.627 thy : for?
1.628 oris: from formalization 'type fmz', structured for efficient access
1.629 @@ -494,65 +219,51 @@
1.630 itms: already input items
1.631 *)
1.632 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
1.633 - let
1.634 - fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
1.635 - fun is_elem itms (f,(d,t)) =
1.636 - case find_first (test_d d) itms of
1.637 - SOME _ => true | NONE => false;
1.638 - in case filter_out (is_elem itms) pbt of
1.639 -(* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
1.640 - *)
1.641 - (f,(d,_))::itms =>
1.642 - SOME (f : string, ((term_to_string''' thy) o comp_dts) (d, []) : cterm')
1.643 - | _ => NONE end
1.644 + let
1.645 + fun test_d d ((i, _, _, _, itm_): itm) = (d = (d_in itm_)) andalso i <> 0
1.646 + fun is_elem itms (_, (d, _)) =
1.647 + case find_first (test_d d) itms of SOME _ => true | NONE => false
1.648 + in
1.649 + case filter_out (is_elem itms) pbt of
1.650 + (f, (d, _)) :: _ => SOME (f : string, ((term_to_string''' thy) o comp_dts) (d, []) : cterm')
1.651 + | _ => NONE
1.652 + end
1.653 + | nxt_add thy oris _ itms =
1.654 + let
1.655 + fun testr_vt v ori = member op= (#2 (ori:ori)) v andalso (#3 ori) <> "#undef"
1.656 + fun testi_vt v itm =member op= (#2 (itm:itm)) v
1.657 + fun test_id ids r = member op= ids (#1 (r:ori))
1.658 + fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
1.659 + (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts)
1.660 + fun false_and_not_Sup ((_, _, false, _, Sup _): itm) = false
1.661 + | false_and_not_Sup (_, _, false, _, _) = true
1.662 + | false_and_not_Sup _ = false
1.663 + val v = if itms = [] then 1 else max_vt itms
1.664 + val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
1.665 + val vits =
1.666 + if v = 0
1.667 + then itms (* because of dsc without dat *)
1.668 + else filter (testi_vt v) itms; (* itms..vat *)
1.669 + val icl = filter false_and_not_Sup vits; (* incomplete *)
1.670 + in
1.671 + if icl = []
1.672 + then case filter_out (test_id (map #1 vits)) vors of
1.673 + [] => NONE
1.674 + | miss => SOME (getr_ct thy (hd miss))
1.675 + else
1.676 + case find_first (test_subset (hd icl)) vors of
1.677 + NONE => error "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
1.678 + | SOME ori => SOME (geti_ct thy ori (hd icl))
1.679 + end
1.680
1.681 -(* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
1.682 - *)
1.683 - | nxt_add thy oris pbt itms =
1.684 - let
1.685 - fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
1.686 - andalso (#3 ori) <>"#undef";
1.687 - fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
1.688 - fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
1.689 - fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
1.690 - (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
1.691 - fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
1.692 - | false_and_not_Sup (i,v,false,f, _) = true
1.693 - | false_and_not_Sup _ = false;
1.694 -
1.695 - val v = if itms = [] then 1 else max_vt itms;
1.696 - val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
1.697 - val vits = if v = 0 then itms (*because of dsc without dat*)
1.698 - else filter (testi_vt v) itms; (*itms..vat*)
1.699 - val icl = filter false_and_not_Sup vits; (* incomplete *)
1.700 - in if icl = []
1.701 - then case filter_out (test_id (map #1 vits)) vors of
1.702 - [] => NONE
1.703 - (* val miss = filter_out (test_id (map #1 vits)) vors;
1.704 - *)
1.705 - | miss => SOME (getr_ct thy (hd miss))
1.706 - else
1.707 - case find_first (test_subset (hd icl)) vors of
1.708 - (* val SOME ori = find_first (test_subset (hd icl)) vors;
1.709 - *)
1.710 - NONE => error "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
1.711 - | SOME ori => SOME (geti_ct thy ori (hd icl))
1.712 - end
1.713 -end;
1.714 -
1.715 -
1.716 -
1.717 -fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
1.718 - | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
1.719 +fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
1.720 + | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
1.721 | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
1.722 - | mk_delete thy str _ =
1.723 - error ("mk_delete: called with field '"^str^"'");
1.724 + | mk_delete _ str _ = error ("mk_delete: called with field \"" ^ str ^ "\"")
1.725 fun mk_additem "#Given" ct = Add_Given ct
1.726 - | mk_additem "#Find" ct = Add_Find ct
1.727 + | mk_additem "#Find" ct = Add_Find ct
1.728 | mk_additem "#Relate"ct = Add_Relation ct
1.729 - | mk_additem str _ =
1.730 - error ("mk_additem: called with field '"^str^"'");
1.731 -
1.732 + | mk_additem str _ = error ("mk_additem: called with field \"" ^ str ^ "\"")
1.733
1.734 (* determine the next step of specification;
1.735 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
1.736 @@ -567,95 +278,77 @@
1.737 (pbt, mpc) problem type, guard of method
1.738 *)
1.739 fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec)
1.740 - ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
1.741 - ((*tracing"### nxt_spec Pbl";*)
1.742 - if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
1.743 + ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) =
1.744 + (if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI')
1.745 else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI')
1.746 - else case find_first (is_error o #5) (pbl:itm list) of
1.747 - SOME (_, _, _, fd, itm_) =>
1.748 - (Pbl, mk_delete
1.749 - (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
1.750 - | NONE =>
1.751 - ((*tracing"### nxt_spec is_error NONE";*)
1.752 - case nxt_add (assoc_thy (if dI = e_domID then dI' else dI))
1.753 - oris pbt pbl of
1.754 - SOME (fd,ct') => ((*tracing"### nxt_spec nxt_add SOME";*)
1.755 - (Pbl, mk_additem fd ct'))
1.756 - | NONE => (*pbl-items complete*)
1.757 - if not preok then (Pbl, Refine_Problem pI')
1.758 - else
1.759 - if dI = e_domID then (Pbl, Specify_Theory dI')
1.760 - else if pI = e_pblID then (Pbl, Specify_Problem pI')
1.761 - else if mI = e_metID then (Pbl, Specify_Method mI')
1.762 - else
1.763 - case find_first (is_error o #5) met of
1.764 - SOME (_,_,_,fd,itm_) =>
1.765 - (Met, mk_delete (assoc_thy dI) fd itm_)
1.766 - | NONE =>
1.767 - (case nxt_add (assoc_thy dI) oris mpc met of
1.768 - SOME (fd,ct') => (*30.8.01: pre?!?*)
1.769 - (Met, mk_additem fd ct')
1.770 - | NONE =>
1.771 - ((*Solv 3.4.00*)Met, Apply_Method mI))))
1.772 -
1.773 - | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
1.774 - ((*tracing"### nxt_spec Met"; *)
1.775 - case find_first (is_error o #5) met of
1.776 - SOME (_,_,_,fd,itm_) =>
1.777 - (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
1.778 - | NONE =>
1.779 - case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
1.780 - SOME (fd,ct') => (Met, mk_additem fd ct')
1.781 - | NONE =>
1.782 - ((*tracing"### nxt_spec Met: nxt_add NONE";*)
1.783 - if dI = e_domID then (Met, Specify_Theory dI')
1.784 - else if pI = e_pblID then (Met, Specify_Problem pI')
1.785 - else if not preok then (Met, Specify_Method mI)
1.786 - else (Met, Apply_Method mI)));
1.787 -
1.788 -(* di_ pI_ mI_ pos_
1.789 -val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
1.790 - (2,[2],true,"#Find",Syn("empty"))];
1.791 -*)
1.792 + else
1.793 + case find_first (is_error o #5) (pbl:itm list) of
1.794 + SOME (_, _, _, fd, itm_) =>
1.795 + (Pbl, mk_delete (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_)
1.796 + | NONE =>
1.797 + (case nxt_add (assoc_thy (if dI = e_domID then dI' else dI)) oris pbt pbl of
1.798 + SOME (fd,ct') => (Pbl, mk_additem fd ct')
1.799 + | NONE => (*pbl-items complete*)
1.800 + if not preok then (Pbl, Refine_Problem pI')
1.801 + else if dI = e_domID then (Pbl, Specify_Theory dI')
1.802 + else if pI = e_pblID then (Pbl, Specify_Problem pI')
1.803 + else if mI = e_metID then (Pbl, Specify_Method mI')
1.804 + else
1.805 + case find_first (is_error o #5) met of
1.806 + SOME (_, _, _, fd, itm_) => (Met, mk_delete (assoc_thy dI) fd itm_)
1.807 + | NONE =>
1.808 + (case nxt_add (assoc_thy dI) oris mpc met of
1.809 + SOME (fd, ct') => (Met, mk_additem fd ct') (*30.8.01: pre?!?*)
1.810 + | NONE => (Met, Apply_Method mI))))
1.811 + | nxt_spec Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
1.812 + (case find_first (is_error o #5) met of
1.813 + SOME (_,_,_,fd,itm_) => (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
1.814 + | NONE =>
1.815 + case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
1.816 + SOME (fd,ct') => (Met, mk_additem fd ct')
1.817 + | NONE =>
1.818 + (if dI = e_domID then (Met, Specify_Theory dI')
1.819 + else if pI = e_pblID then (Met, Specify_Problem pI')
1.820 + else if not preok then (Met, Specify_Method mI)
1.821 + else (Met, Apply_Method mI)))
1.822 + | nxt_spec p _ _ _ _ _ _ = error ("nxt_spec: uncovered case with " ^ pos_2str p)
1.823
1.824 fun is_field_correct sel d dscpbt =
1.825 case assoc (dscpbt, sel) of
1.826 NONE => false
1.827 - | SOME ds => member op = ds d;
1.828 + | SOME ds => member op = ds d
1.829
1.830 -(*. update the itm_ already input, all..from ori .*)
1.831 -(* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
1.832 - *)
1.833 -fun ori_2itm itm_ pid all ((id,vt,fd,d,ts):ori) =
1.834 +(* update the itm_ already input, all..from ori *)
1.835 +fun ori_2itm itm_ pid all ((id, vt, fd, d, ts): ori) =
1.836 let
1.837 val ts' = union op = (ts_in itm_) ts;
1.838 val pval = pbl_ids' d ts'
1.839 - (*WN.9.5.03: FIXXXME [#0, epsilon]
1.840 - here would upd_penv be called for [#0, epsilon] etc. *)
1.841 - val complete = if eq_set op = (ts', all) then true else false;
1.842 - in case itm_ of
1.843 - (Cor _) =>
1.844 - (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
1.845 - else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
1.846 - | (Syn c) => error ("ori_2itm wants to overwrite "^c)
1.847 - | (Typ c) => error ("ori_2itm wants to overwrite "^c)
1.848 - | (Inc _) => if complete
1.849 - then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
1.850 - else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
1.851 - | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
1.852 - (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
1.853 - (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
1.854 -(* 28.1.00: not completely clear ---^^^ etc.*)
1.855 -(* 4.9.01: Mis just copied---vvv *)
1.856 - | (Mis _) => if complete
1.857 - then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
1.858 - else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
1.859 - end;
1.860 + (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
1.861 + val complete = if eq_set op = (ts', all) then true else false
1.862 + in
1.863 + case itm_ of
1.864 + (Cor _) =>
1.865 + (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
1.866 + else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval)))): itm
1.867 + | (Syn c) => error ("ori_2itm wants to overwrite " ^ c)
1.868 + | (Typ c) => error ("ori_2itm wants to overwrite " ^ c)
1.869 + | (Inc _) =>
1.870 + if complete
1.871 + then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
1.872 + else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
1.873 + | (Sup (d,ts')) => (*4.9.01 lost env*)
1.874 + (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
1.875 + (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
1.876 + (* 28.1.00: not completely clear ---^^^ etc.*)
1.877 + | (Mis _) => (* 4.9.01: Mis just copied *)
1.878 + if complete
1.879 + then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
1.880 + else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
1.881 + | i => error ("ori_2itm: uncovered case of "^ itm_2str i)
1.882 + end
1.883
1.884 -
1.885 -fun eq1 d (_,(d',_)) = (d = d');
1.886 -fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
1.887 -
1.888 +fun eq1 d (_, (d', _)) = (d = d')
1.889 +fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (d_in itm_)
1.890
1.891 (* 'all' ts from ori; ts is the input; (ori carries rest of info)
1.892 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
1.893 @@ -667,675 +360,609 @@
1.894 (2) ori(ts) subset itm(ts) --- Err "already input"
1.895 (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
1.896 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
1.897 -(* val(itms,(i,v,f,d,ts)) = (ppc,ori');
1.898 - *)
1.899 -fun is_notyet_input ctxt (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
1.900 +fun is_notyet_input ctxt (itms: itm list) all ((i, v, f, d, ts): ori) pbt =
1.901 case find_first (eq1 d) pbt of
1.902 - SOME (_,(_,pid)) =>
1.903 + SOME (_, (_, pid)) =>
1.904 (case find_first (eq3 f d) itms of
1.905 SOME (_,_,_,_,itm_) =>
1.906 - let
1.907 - val ts' = inter op = (ts_in itm_) ts;
1.908 - in
1.909 - if subset op = (ts, ts')
1.910 - then (((strs2str' o map (term_to_string' ctxt)) ts') ^ " already input", e_itm)(*2*)
1.911 - else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
1.912 + let val ts' = inter op = (ts_in itm_) ts
1.913 + in
1.914 + if subset op = (ts, ts')
1.915 + then (((strs2str' o map (term_to_string' ctxt)) ts') ^ " already input", e_itm) (*2*)
1.916 + else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*)
1.917 end
1.918 - | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[]))) pid all (i,v,f,d,ts))) (*1*)
1.919 - | NONE => ("", ori_2itm (Sup (d,ts)) e_term all (i,v,f,d,ts));
1.920 + | NONE => ("", ori_2itm (Inc ((e_term, []), (pid, []))) pid all (i, v, f, d, ts))) (*1*)
1.921 + | NONE => ("", ori_2itm (Sup (d, ts)) e_term all (i, v, f, d, ts))
1.922
1.923 fun test_types ctxt (d,ts) =
1.924 let
1.925 - val opt = (try comp_dts) (d,ts);
1.926 + val opt = (try comp_dts) (d, ts)
1.927 val msg = case opt of
1.928 SOME _ => ""
1.929 | NONE => (term_to_string' ctxt d ^ " " ^
1.930 - (strs2str' o map (term_to_string' ctxt)) ts ^ " is illtyped");
1.931 - in msg end;
1.932 + (strs2str' o map (term_to_string' ctxt)) ts ^ " is illtyped")
1.933 + in msg end
1.934
1.935 -fun maxl [] = error "maxl of []"
1.936 - | maxl (y::ys) =
1.937 - let fun mx x [] = x
1.938 - | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
1.939 - in mx y ys end;
1.940 -
1.941 -
1.942 -(*. is the input term t known in oris ?
1.943 - give feedback on all(?) strange input;
1.944 - return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
1.945 +(* is the input term t known in oris ?
1.946 + give feedback on all(?) strange input;
1.947 + return _all_ terms already input to this item (e.g. valuesFor a,b) *)
1.948 fun is_known ctxt sel ori t =
1.949 let
1.950 - val _ = tracing ("RM is_known: t=" ^ term2str t);
1.951 - val ots = (distinct o flat o (map #5)) (ori:ori list);
1.952 - val oids = ((map (fst o dest_Free)) o distinct o
1.953 - flat o (map vars)) ots;
1.954 - val (d, ts) = split_dts t;
1.955 - val ids = map (fst o dest_Free)
1.956 - ((distinct o (flat o (map vars))) ts);
1.957 - in if (subtract op = oids ids) <> []
1.958 - then (("identifiers "^(strs2str' (subtract op = oids ids)) ^
1.959 - " not in example"), e_ori_, [])
1.960 - else
1.961 - if d = e_term
1.962 - then
1.963 - if not (subset op = (map typeless ts, map typeless ots))
1.964 - then ("terms '" ^ (strs2str' o (map (term_to_string' ctxt))) ts ^
1.965 - "' not in example (typeless)", e_ori_, [])
1.966 - else
1.967 - (case seek_orits ctxt sel ts ori of
1.968 - ("", ori_ as (_,_,_,d,ts), all) =>
1.969 - (case test_types ctxt (d,ts) of
1.970 - "" => ("", ori_, all)
1.971 - | msg => (msg, e_ori_, []))
1.972 - | (msg,_,_) => (msg, e_ori_, []))
1.973 - else
1.974 - if member op = (map #4 ori) d
1.975 - then seek_oridts ctxt sel (d,ts) ori
1.976 - else (term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), [])
1.977 - end;
1.978 + val _ = tracing ("RM is_known: t=" ^ term2str t)
1.979 + val ots = (distinct o flat o (map #5)) (ori:ori list)
1.980 + val oids = ((map (fst o dest_Free)) o distinct o flat o (map vars)) ots
1.981 + val (d, ts) = split_dts t
1.982 + val ids = map (fst o dest_Free) ((distinct o (flat o (map vars))) ts)
1.983 + in
1.984 + if (subtract op = oids ids) <> []
1.985 + then (("identifiers "^(strs2str' (subtract op = oids ids)) ^ " not in example"), e_ori_, [])
1.986 + else
1.987 + if d = e_term
1.988 + then
1.989 + if not (subset op = (map typeless ts, map typeless ots))
1.990 + then ("terms '" ^ (strs2str' o (map (term_to_string' ctxt))) ts ^
1.991 + "' not in example (typeless)", e_ori_, [])
1.992 + else
1.993 + (case seek_orits ctxt sel ts ori of
1.994 + ("", ori_ as (_,_,_,d,ts), all) =>
1.995 + (case test_types ctxt (d,ts) of
1.996 + "" => ("", ori_, all)
1.997 + | msg => (msg, e_ori_, []))
1.998 + | (msg,_,_) => (msg, e_ori_, []))
1.999 + else
1.1000 + if member op = (map #4 ori) d
1.1001 + then seek_oridts ctxt sel (d, ts) ori
1.1002 + else (term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), [])
1.1003 + end
1.1004
1.1005 -(*. for return-value of appl_add .*)
1.1006 +
1.1007 datatype additm =
1.1008 - Add of itm
1.1009 - | Err of string; (*error-message*)
1.1010 + Add of itm (* return-value of appl_add *)
1.1011 +| Err of string (* error-message *)
1.1012
1.1013 +(* add an item to the model; check wrt. oris and pbt.
1.1014 + in contrary to oris<>[] below, this part handles user-input
1.1015 + extremely acceptive, i.e. accept input instead error-msg *)
1.1016 +fun appl_add ctxt sel [] ppc pbt ct =
1.1017 + let
1.1018 + val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl)
1.1019 + in
1.1020 + case parseNEW ctxt ct of
1.1021 + NONE => Add (i, [], false, sel, Syn ct)
1.1022 + | SOME t =>
1.1023 + let val (d, ts) = split_dts t
1.1024 + in
1.1025 + if d = e_term
1.1026 + then Add (i, [], false, sel, Mis (dsc_unknown, hd ts))
1.1027 + else
1.1028 + (case find_first (eq1 d) pbt of
1.1029 + NONE => Add (i, [], true, sel, Sup (d,ts))
1.1030 + | SOME (f, (_, id)) =>
1.1031 + let fun eq2 d (i, _, _, _, itm_) = d = (d_in itm_) andalso i <> 0
1.1032 + in case find_first (eq2 d) ppc of
1.1033 + NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
1.1034 + | SOME (i', _, _, _, itm_) =>
1.1035 + if is_list_dsc d
1.1036 + then
1.1037 + let
1.1038 + val in_itm = ts_in itm_
1.1039 + val ts' = union op = ts in_itm
1.1040 + val i'' = if in_itm = [] then i else i'
1.1041 + in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts')))end
1.1042 + else Add (i', [], true, f, Cor ((d, ts), (id, pbl_ids' d ts)))
1.1043 + end)
1.1044 + end
1.1045 + end
1.1046 + | appl_add ctxt sel oris ppc pbt str =
1.1047 + case parseNEW ctxt str of
1.1048 + NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
1.1049 + | SOME t =>
1.1050 + case is_known ctxt sel oris t of
1.1051 + ("", ori', all) =>
1.1052 + (case is_notyet_input ctxt ppc all ori' pbt of
1.1053 + ("", itm) => Add itm
1.1054 + | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
1.1055 + | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
1.1056
1.1057 -(** add an item to the model; check wrt. oris and pbt **)
1.1058 -(* in contrary to oris<>[] below, this part handles user-input
1.1059 - extremely acceptive, i.e. accept input instead error-msg *)
1.1060 -fun appl_add ctxt sel [] ppc pbt ct =
1.1061 - let
1.1062 - val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
1.1063 - in
1.1064 - case parseNEW ctxt ct of
1.1065 - NONE => Add (i, [], false, sel, Syn ct)
1.1066 - | SOME t =>
1.1067 - let val (d, ts) = split_dts t;
1.1068 - in
1.1069 - if d = e_term
1.1070 - then Add (i, [], false, sel, Mis (dsc_unknown, hd ts))
1.1071 - else
1.1072 - (case find_first (eq1 d) pbt of
1.1073 - NONE => Add (i, [], true, sel, Sup (d,ts))
1.1074 - | SOME (f, (_, id)) =>
1.1075 - let fun eq2 d (i, _, _, _, itm_) =
1.1076 - d = (d_in itm_) andalso i <> 0;
1.1077 - in case find_first (eq2 d) ppc of
1.1078 - NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
1.1079 - | SOME (i', _, _, _, itm_) =>
1.1080 - if is_list_dsc d
1.1081 - then
1.1082 - let
1.1083 - val in_itm = ts_in itm_;
1.1084 - val ts' = union op = ts in_itm;
1.1085 - val i'' = if in_itm = [] then i else i';
1.1086 - in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts'))) end
1.1087 - else Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
1.1088 - end)
1.1089 - end
1.1090 - end
1.1091 - | appl_add ctxt sel oris ppc pbt str =
1.1092 - case parseNEW ctxt str of
1.1093 - NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
1.1094 - | SOME t =>
1.1095 - case is_known ctxt sel oris t of
1.1096 - ("", ori', all) =>
1.1097 - (case is_notyet_input ctxt ppc all ori' pbt of
1.1098 - ("", itm) => Add itm
1.1099 - | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
1.1100 - | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
1.1101 +(* make oris from args of the stac SubProblem and from pbt.
1.1102 + can this formal argument (of a model-pattern) be omitted in the arg-list
1.1103 + of a SubProblem ? see calcelems.sml 'type met ' *)
1.1104 +fun is_copy_named_idstr str =
1.1105 + case (rev o Symbol.explode) str of
1.1106 + "'" :: _ :: "'" :: _ =>
1.1107 + (tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " T"); true)
1.1108 + | _ =>
1.1109 + (tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " F"); false)
1.1110 +fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t
1.1111
1.1112 +(* should this formal argument (of a model-pattern) create a new identifier? *)
1.1113 +fun is_copy_named_generating_idstr str =
1.1114 + if is_copy_named_idstr str
1.1115 + then
1.1116 + case (rev o Symbol.explode) str of
1.1117 + "'" :: "'" :: "'" :: _ => false
1.1118 + | _ => true
1.1119 + else false
1.1120 +fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o free2str) t
1.1121
1.1122 -(** make oris from args of the stac SubProblem and from pbt **)
1.1123 -(* can this formal argument (of a model-pattern) be omitted in the arg-list
1.1124 - of a SubProblem ? see calcelems.sml 'type met ' *)
1.1125 -fun is_copy_named_idstr str =
1.1126 - case (rev o Symbol.explode) str of
1.1127 - "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))
1.1128 - "is_copy_named_idstr: " ^ str ^ " T"); true)
1.1129 - | _ => (tracing ((strs2str o (rev o Symbol.explode))
1.1130 - "is_copy_named_idstr: " ^ str ^ " F"); false);
1.1131 -fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
1.1132 +(* split type-wrapper from scr-arg and build part of an ori;
1.1133 + an type-error is reported immediately, raises an exn,
1.1134 + subsequent handling of exn provides 2nd part of error message *)
1.1135 +fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
1.1136 + ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
1.1137 + SOME ((([1], str, dsc, (*[var]*)
1.1138 + split_dts' (dsc, var))): preori)(*:ori without leading #*))
1.1139 + handle e as TYPE _ =>
1.1140 + (tracing (dashs 70 ^ "\n"
1.1141 + ^ "*** ERROR while creating the items for the model of the ->problem\n"
1.1142 + ^ "*** from the ->stac with ->typeconstructor in arglist:\n"
1.1143 + ^ "*** item (->description ->value): " ^ term2str dsc ^ " " ^ term2str var ^ "\n"
1.1144 + ^ "*** description: " ^ term_detail2str dsc
1.1145 + ^ "*** value: " ^ term_detail2str var
1.1146 + ^ "*** typeconstructor in script: " ^ term_detail2str ty
1.1147 + ^ "*** checked by theory: " ^ theory2str thy ^ "\n"
1.1148 + ^ "*** " ^ dots 66);
1.1149 + writeln (PolyML.makestring e);
1.1150 + reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
1.1151 + NONE))
1.1152 + | mtc _ _ t = error ("mtc: uncovered case with" ^ term2str t)
1.1153
1.1154 -(*.should this formal argument (of a model-pattern) create a new identifier?.*)
1.1155 -fun is_copy_named_generating_idstr str =
1.1156 - if is_copy_named_idstr str
1.1157 - then case (rev o Symbol.explode) str of
1.1158 - "'"::"'"::"'"::_ => false
1.1159 - | _ => true
1.1160 - else false;
1.1161 -fun is_copy_named_generating (_, (_, t)) =
1.1162 - (is_copy_named_generating_idstr o free2str) t;
1.1163 -
1.1164 -(*.split type-wrapper from scr-arg and build part of an ori;
1.1165 - an type-error is reported immediately, raises an exn,
1.1166 - subsequent handling of exn provides 2nd part of error message.*)
1.1167 -fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
1.1168 - (* val (thy, (str, (dsc, _)), (ty $ var)) =
1.1169 - (thy, p, a);
1.1170 - *)
1.1171 - (Thm.global_cterm_of thy (dsc $ var);(*type check*)
1.1172 - SOME ((([1], str, dsc, (*[var]*)
1.1173 - split_dts' (dsc, var))): preori)(*:ori without leading #*))
1.1174 - handle e as TYPE _ =>
1.1175 - (tracing (dashs 70 ^ "\n"
1.1176 - ^"*** ERROR while creating the items for the model of the ->problem\n"
1.1177 - ^"*** from the ->stac with ->typeconstructor in arglist:\n"
1.1178 - ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
1.1179 - ^"*** description: "^(term_detail2str dsc)
1.1180 - ^"*** value: "^(term_detail2str var)
1.1181 - ^"*** typeconstructor in script: "^(term_detail2str ty)
1.1182 - ^"*** checked by theory: "^(theory2str thy)^"\n"
1.1183 - ^"*** " ^ dots 66);
1.1184 - (*OldGoals.print_exn e; raises exn again*)
1.1185 - writeln (PolyML.makestring e);
1.1186 - reraise e;
1.1187 - (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
1.1188 - NONE);
1.1189 -
1.1190 -(*.match each pat of the model-pattern with an actual argument;
1.1191 - precondition: copy-named vars are filtered out.*)
1.1192 -fun matc thy ([]:pat list) _ (oris:preori list) = oris
1.1193 - | matc thy pbt [] _ =
1.1194 +(* match each pat of the model-pattern with an actual argument;
1.1195 + precondition: copy-named vars are filtered out *)
1.1196 +fun matc _ ([]:pat list) _ (oris:preori list) = oris
1.1197 + | matc _ pbt [] _ =
1.1198 (tracing (dashs 70);
1.1199 - error ("actual arg(s) missing for '"^pats2str pbt
1.1200 - ^"' i.e. should be 'copy-named' by '*_._'"))
1.1201 - | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
1.1202 - (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
1.1203 - (thy, pbt', ags, []);
1.1204 - (*recursion..*)
1.1205 - val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
1.1206 - (thy, pbt, ags, (oris @ [ori]));
1.1207 - *)
1.1208 + error ("actual arg(s) missing for '" ^ pats2str pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
1.1209 + | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =
1.1210 (*del?..*)if (is_copy_named_idstr o free2str) t then oris
1.1211 - else(*..del?*) let val opt = mtc thy p a;
1.1212 - in case opt of
1.1213 - (* val SOME ori = mtc thy p a;
1.1214 - *)
1.1215 - SOME ori => matc thy pbt ags (oris @ [ori])
1.1216 + else(*..del?*)
1.1217 + let val opt = mtc thy p a
1.1218 + in
1.1219 + case opt of
1.1220 + SOME ori => matc thy pbt ags (oris @ [ori])
1.1221 | NONE => [](*WN050903 skipped by exn handled in match_ags*)
1.1222 - end;
1.1223 -(* run subp-rooteq.sml until Init_Proof before ...
1.1224 -> val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
1.1225 -> fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
1.1226 -
1.1227 - other vars as in mtc ..
1.1228 -> matc thy (drop_last pbt) ags [];
1.1229 -val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
1.1230 -
1.1231 -
1.1232 -(* generate a new variable "x_i" name from a related given one "x"
1.1233 - by use of oris relating "v_i_" (is_copy_named!) to "v_"
1.1234 - e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
1.1235 + end
1.1236
1.1237 (* generate a new variable "x_i" name from a related given one "x"
1.1238 by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
1.1239 e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
1.1240 but leave is_copy_named_generating as is, e.t. ss''' *)
1.1241 -fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
1.1242 +fun cpy_nam (pbt: pat list) (oris: preori list) (p as (field, (dsc, t)): pat) =
1.1243 (if is_copy_named_generating p
1.1244 then (*WN051014 kept strange old code ...*)
1.1245 - let fun sel (_,_,d,ts) = comp_ts (d, ts)
1.1246 - val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
1.1247 - val ext = (last_elem o drop_last o Symbol.explode o free2str) t
1.1248 - val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
1.1249 - val vals = map sel oris
1.1250 - val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
1.1251 - in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
1.1252 + let fun sel (_,_,d,ts) = comp_ts (d, ts)
1.1253 + val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t
1.1254 + val ext = (last_elem o drop_last o Symbol.explode o free2str) t
1.1255 + val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
1.1256 + val vals = map sel oris
1.1257 + val cy_ext = (free2str o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
1.1258 + in ([1], field, dsc, [mk_free (type_of t) cy_ext]): preori end
1.1259 else ([1], field, dsc, [t])
1.1260 - )
1.1261 - handle _ => error ("cpy_nam: for "^(term2str t));
1.1262 + ) handle _ => error ("cpy_nam: for "^(term2str t))
1.1263
1.1264 -(*.match the actual arguments of a SubProblem with a model-pattern
1.1265 +(* match the actual arguments of a SubProblem with a model-pattern
1.1266 and create an ori list (in root-pbl created from formalization).
1.1267 expects ags:pats = 1:1, while copy-named are filtered out of pats;
1.1268 if no 1:1 the exn raised by matc/mtc and handled at call.
1.1269 - copy-named pats are appended in order to get them into the model-items.*)
1.1270 -fun match_ags thy (pbt:pat list) ags =
1.1271 - let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
1.1272 - val pbt' = filter_out is_copy_named pbt;
1.1273 - val cy = filter is_copy_named pbt;
1.1274 - val oris' = matc thy pbt' ags [];
1.1275 - val cy' = map (cpy_nam pbt' oris') cy;
1.1276 - val ors = add_id (oris' @ cy');
1.1277 - (*appended in order to get ^^^^^ into the model-items*)
1.1278 - in (map flattup ors):ori list end;
1.1279 + copy-named pats are appended in order to get them into the model-items *)
1.1280 +fun match_ags thy (pbt: pat list) ags =
1.1281 + let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_)
1.1282 + val pbt' = filter_out is_copy_named pbt
1.1283 + val cy = filter is_copy_named pbt
1.1284 + val oris' = matc thy pbt' ags []
1.1285 + val cy' = map (cpy_nam pbt' oris') cy
1.1286 + val ors = add_id (oris' @ cy') (*...appended in order to get into the model-items *)
1.1287 + in (map flattup ors): ori list end
1.1288
1.1289 -(*.report part of the error-msg which is not available in match_args.*)
1.1290 +(* report part of the error-msg which is not available in match_args *)
1.1291 fun match_ags_msg pI stac ags =
1.1292 - let (*val s = !show_types
1.1293 - val _ = show_types:= true*)
1.1294 - val pats = (#ppc o get_pbt) pI
1.1295 - val msg = (dots 70^"\n"
1.1296 - ^"*** problem "^strs2str pI^" has the ...\n"
1.1297 - ^"*** model-pattern "^pats2str pats^"\n"
1.1298 - ^"*** stac '"^term2str stac^"' has the ...\n"
1.1299 - ^"*** arg-list "^terms2str ags^"\n"
1.1300 - ^dashs 70)
1.1301 - (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
1.1302 - (*val _ = show_types:= s*)
1.1303 - in tracing msg end;
1.1304 + let
1.1305 + val pats = (#ppc o get_pbt) pI
1.1306 + val msg = (dots 70^"\n"
1.1307 + ^ "*** problem "^strs2str pI ^ " has the ...\n"
1.1308 + ^ "*** model-pattern "^pats2str pats ^ "\n"
1.1309 + ^ "*** stac '"^term2str stac ^ "' has the ...\n"
1.1310 + ^ "*** arg-list "^terms2str ags ^ "\n"
1.1311 + ^ dashs 70)
1.1312 + (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
1.1313 + in tracing msg end
1.1314
1.1315 -
1.1316 -(*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
1.1317 +(* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)
1.1318 fun vars_of_pbl_ pbl_ =
1.1319 - let fun var_of_pbl_ (gfr,(dsc,t)) = t
1.1320 - in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
1.1321 + let
1.1322 + fun var_of_pbl_ (_, (_, t)) = t
1.1323 + in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end
1.1324 fun vars_of_pbl_' pbl_ =
1.1325 - let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
1.1326 - in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
1.1327 + let
1.1328 + fun var_of_pbl_ (_, (_, t)) = t: term
1.1329 + in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end
1.1330
1.1331 fun overwrite_ppc thy itm ppc =
1.1332 let
1.1333 - fun repl ppc' (_,_,_,_,itm_) [] =
1.1334 - error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^
1.1335 - " not found")
1.1336 - | repl ppc' itm (p::ppc) =
1.1337 - if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
1.1338 - else repl (ppc' @ [p]) itm ppc
1.1339 - in repl [] itm ppc end;
1.1340 + fun repl _ (_, _, _, _, itm_) [] =
1.1341 + error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^ " not found")
1.1342 + | repl ppc' itm (p :: ppc) =
1.1343 + if (#1 itm) = (#1 (p: itm))
1.1344 + then ppc' @ [itm] @ ppc
1.1345 + else repl (ppc' @ [p]) itm ppc
1.1346 + in repl [] itm ppc end
1.1347
1.1348 -(*10.3.00: insert the already compiled itm into model;
1.1349 +(* 10.3.00: insert the already compiled itm into model;
1.1350 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
1.1351 -(* val ppc=pbl;
1.1352 - *)
1.1353 fun insert_ppc thy itm ppc =
1.1354 - let
1.1355 - fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
1.1356 - | eq_untouched _ _ = false;
1.1357 - val ppc' =
1.1358 - (
1.1359 - (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)
1.1360 - case seek_ppc (#1 itm) ppc of
1.1361 - (* val SOME xxx = seek_ppc (#1 itm) ppc;
1.1362 - *)
1.1363 - SOME _ => (*itm updated in is_notyet_input WN.11.03*)
1.1364 - overwrite_ppc thy itm ppc
1.1365 - | NONE => (ppc @ [itm]));
1.1366 - in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
1.1367 + let
1.1368 + fun eq_untouched d ((0, _, _, _, itm_): itm) = (d = d_in itm_)
1.1369 + | eq_untouched _ _ = false
1.1370 + val ppc' = case seek_ppc (#1 itm) ppc of
1.1371 + SOME _ => overwrite_ppc thy itm ppc (*itm updated in is_notyet_input WN.11.03*)
1.1372 + | NONE => (ppc @ [itm])
1.1373 + in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end
1.1374
1.1375 -(*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
1.1376 -fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
1.1377 +fun eq_dsc ((_, _, _, _, itm_): itm, (_, _, _, _, iitm_): itm) = (d_in itm_ = d_in iitm_)
1.1378
1.1379 -fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
1.1380 - (d_in itm_) = (d_in iitm_);
1.1381 -(*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
1.1382 - handles superfluous items carelessly*)
1.1383 -fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
1.1384 -(* val eee = op=;
1.1385 - > gen_ins' eee (4,[1,3,5,7]);
1.1386 -val it = [1, 3, 5, 7, 4] : int list*)
1.1387 +(* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
1.1388 + handles superfluous items carelessly *)
1.1389 +fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
1.1390
1.1391 +(* output the headline to a ppc *)
1.1392 +fun header p_ pI mI =
1.1393 + case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1.1394 + | Met => Method mI
1.1395 + | pos => error ("header called with "^ pos_2str pos)
1.1396
1.1397 -(*. output the headline to a ppc .*)
1.1398 -fun header p_ pI mI =
1.1399 - case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1.1400 - | Met => Method mI
1.1401 - | pos => error ("header called with "^ pos_2str pos);
1.1402 -
1.1403 -
1.1404 -fun specify_additem sel (ct,_) (p, Met) c pt =
1.1405 +fun specify_additem sel (ct, _) (p, Met) _ pt =
1.1406 + let
1.1407 + val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
1.1408 + (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
1.1409 + => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
1.1410 + | _ => error "specify_additem: uncovered case of get_obj I pt p"
1.1411 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI
1.1412 + val cpI = if pI = e_pblID then pI' else pI
1.1413 + val cmI = if mI = e_metID then mI' else mI
1.1414 + val {ppc, pre, prls, ...} = get_met cmI
1.1415 + in
1.1416 + case appl_add ctxt sel oris met ppc ct of
1.1417 + Add itm => (*..union old input *)
1.1418 + let
1.1419 + val met' = insert_ppc thy itm met
1.1420 + val arg = case sel of
1.1421 + "#Given" => Add_Given' (ct, met')
1.1422 + | "#Find" => Add_Find' (ct, met')
1.1423 + | "#Relate"=> Add_Relation'(ct, met')
1.1424 + | str => error ("specify_additem: uncovered case with " ^ str)
1.1425 + val (p, Met, pt') = case generate1 thy arg (Uistate, ctxt) (p, Met) pt of
1.1426 + ((p, Met), _, _, pt') => (p, Met, pt')
1.1427 + | _ => error "specify_additem: uncovered case of generate1 (WARNING WHY ?)"
1.1428 + val pre' = check_preconds thy prls pre met'
1.1429 + val pb = foldl and_ (true, map fst pre')
1.1430 + val (p_, nxt) =
1.1431 + nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1.1432 + ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1.1433 + in ((p, p_), ((p, p_), Uistate),
1.1434 + Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.1435 + (Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
1.1436 + end
1.1437 + | Err msg =>
1.1438 + let
1.1439 + val pre' = check_preconds thy prls pre met
1.1440 + val pb = foldl and_ (true, map fst pre')
1.1441 + val (p_, nxt) =
1.1442 + nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1.1443 + ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1.1444 + in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1.1445 + end
1.1446 + | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
1.1447 let
1.1448 - val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.1449 - probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1.1450 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.1451 - val cpI = if pI = e_pblID then pI' else pI;
1.1452 - val cmI = if mI = e_metID then mI' else mI;
1.1453 - val {ppc,pre,prls,...} = get_met cmI;
1.1454 - in
1.1455 - case appl_add ctxt sel oris met ppc ct of
1.1456 - Add itm (*..union old input *) =>
1.1457 - let
1.1458 - val met' = insert_ppc thy itm met;
1.1459 - val ((p, Met), _, _, pt') =
1.1460 - generate1 thy (case sel of
1.1461 - "#Given" => Add_Given' (ct, met')
1.1462 - | "#Find" => Add_Find' (ct, met')
1.1463 - | "#Relate"=> Add_Relation'(ct, met'))
1.1464 - (Uistate, ctxt) (p, Met) pt
1.1465 - val pre' = check_preconds thy prls pre met'
1.1466 - val pb = foldl and_ (true, map fst pre')
1.1467 - val (p_, nxt) =
1.1468 - nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1.1469 - ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1.1470 - in ((p, p_), ((p, p_), Uistate),
1.1471 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.1472 - (Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
1.1473 - end
1.1474 - | Err msg =>
1.1475 - let
1.1476 - val pre' = check_preconds thy prls pre met
1.1477 - val pb = foldl and_ (true, map fst pre')
1.1478 - val (p_, nxt) =
1.1479 - nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1.1480 - ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1.1481 - in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1.1482 - end
1.1483 -
1.1484 - | specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt =
1.1485 - let
1.1486 - val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.1487 - probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1.1488 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.1489 - val cpI = if pI = e_pblID then pI' else pI;
1.1490 - val cmI = if mI = e_metID then mI' else mI;
1.1491 - val {ppc,where_,prls,...} = get_pbt cpI;
1.1492 + val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
1.1493 + (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
1.1494 + => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
1.1495 + | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
1.1496 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI
1.1497 + val cpI = if pI = e_pblID then pI' else pI
1.1498 + val cmI = if mI = e_metID then mI' else mI
1.1499 + val {ppc, where_, prls, ...} = get_pbt cpI
1.1500 in
1.1501 case appl_add ctxt sel oris pbl ppc ct of
1.1502 - Add itm (*..union old input *) =>
1.1503 + Add itm => (*..union old input *)
1.1504 let
1.1505 val pbl' = insert_ppc thy itm pbl
1.1506 - val ((p, Pbl), _, _, pt') =
1.1507 - generate1 thy (case sel of
1.1508 - "#Given" => Add_Given' (ct, pbl')
1.1509 - | "#Find" => Add_Find' (ct, pbl')
1.1510 - | "#Relate"=> Add_Relation'(ct, pbl'))
1.1511 - (Uistate, ctxt) (p,Pbl) pt
1.1512 + val arg = case sel of
1.1513 + "#Given" => Add_Given' (ct, pbl')
1.1514 + | "#Find" => Add_Find' (ct, pbl')
1.1515 + | "#Relate"=> Add_Relation'(ct, pbl')
1.1516 + | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
1.1517 + val ((p, Pbl), _, _, pt') = generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
1.1518 val pre = check_preconds thy prls where_ pbl'
1.1519 val pb = foldl and_ (true, map fst pre)
1.1520 val (p_, nxt) =
1.1521 - nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1.1522 - (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1.1523 - val ppc = if p_= Pbl then pbl' else met;
1.1524 - in ((p,p_), ((p,p_),Uistate),
1.1525 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.1526 - (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt,Safe,pt')
1.1527 + nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
1.1528 + val ppc = if p_= Pbl then pbl' else met
1.1529 + in
1.1530 + ((p, p_), ((p, p_), Uistate),
1.1531 + Form' (PpcKF (0, EdUndef, (length p), Nundef,
1.1532 + (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt, Safe, pt')
1.1533 end
1.1534 | Err msg =>
1.1535 let
1.1536 val pre = check_preconds thy prls where_ pbl
1.1537 val pb = foldl and_ (true, map fst pre)
1.1538 val (p_, nxt) =
1.1539 - nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1.1540 - (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1.1541 - in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1.1542 - end;
1.1543 + nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
1.1544 + (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
1.1545 + in ((p, p_), ((p, p_), Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1.1546 + end
1.1547
1.1548 -fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1.1549 +fun specify (Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
1.1550 let (* either """"""""""""""" all empty or complete *)
1.1551 - val thy = assoc_thy dI';
1.1552 + val thy = assoc_thy dI'
1.1553 val (oris, ctxt) =
1.1554 if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*)
1.1555 then ([], e_ctxt)
1.1556 else pI' |> #ppc o get_pbt |> prep_ori fmz thy
1.1557 - val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
1.1558 + val (pt, _) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz, spec')
1.1559 (oris, (dI',pI',mI'), e_term)
1.1560 val pt = update_ctxt pt [] ctxt
1.1561 - val {ppc, prls, where_, ...} = get_pbt pI'
1.1562 - val (pbl, pre, pb) = ([], [], false)
1.1563 + val (pbl, pre) = ([], [])
1.1564 in
1.1565 case mI' of
1.1566 ["no_met"] =>
1.1567 (([], Pbl), (([], Pbl), Uistate),
1.1568 - Form' (PpcKF (0, EdUndef, (length []), Nundef,
1.1569 - (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.1570 + Form' (PpcKF (0, EdUndef, (length []), Nundef, (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.1571 Refine_Tacitly pI', Safe, pt)
1.1572 | _ =>
1.1573 (([], Pbl), (([], Pbl), Uistate),
1.1574 - Form' (PpcKF (0, EdUndef, (length []), Nundef,
1.1575 - (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.1576 + Form' (PpcKF (0, EdUndef, (length []), Nundef, (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.1577 Model_Problem, Safe, pt)
1.1578 - end
1.1579 -
1.1580 - (*ONLY for STARTING modeling phase*)
1.1581 - | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1.1582 - let
1.1583 - val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_), ctxt, ...}) = get_obj I pt p
1.1584 - val thy' = if dI = e_domID then dI' else dI
1.1585 - val thy = assoc_thy thy'
1.1586 - val {ppc,prls,where_,...} = get_pbt pI'
1.1587 - val pre = check_preconds thy prls where_ pbl
1.1588 - val pb = foldl and_ (true, map fst pre)
1.1589 - val ((p,_),_,_,pt) =
1.1590 - generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
1.1591 - val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1.1592 - (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1.1593 - in ((p, Pbl), ((p, p_), Uistate),
1.1594 - Form' (PpcKF (0, EdUndef, length p, Nundef,
1.1595 - (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1.1596 - nxt, Safe, pt)
1.1597 - end
1.1598 -
1.1599 - (*. called only if no_met is specified .*)
1.1600 - | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1.1601 + end
1.1602 + (* ONLY for STARTING modeling phase *)
1.1603 + | specify (Model_Problem' (_, pbl, met)) (pos as (p, p_)) _ pt =
1.1604 + let
1.1605 + val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of
1.1606 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>
1.1607 + (oris, dI',pI',mI', dI, ctxt)
1.1608 + | _ => error "specify (Model_Problem': uncovered case get_obj"
1.1609 + val thy' = if dI = e_domID then dI' else dI
1.1610 + val thy = assoc_thy thy'
1.1611 + val {ppc, prls, where_, ...} = get_pbt pI'
1.1612 + val pre = check_preconds thy prls where_ pbl
1.1613 + val pb = foldl and_ (true, map fst pre)
1.1614 + val ((p, _), _, _, pt) =
1.1615 + generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
1.1616 + val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
1.1617 + (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1.1618 + in
1.1619 + ((p, Pbl), ((p, p_), Uistate),
1.1620 + Form' (PpcKF (0, EdUndef, length p, Nundef, (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1.1621 + nxt, Safe, pt)
1.1622 + end
1.1623 + (* called only if no_met is specified *)
1.1624 + | specify (Refine_Tacitly' (pI, pIre, _, _, _)) (pos as (p, _)) _ pt =
1.1625 let
1.1626 - val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ctxt, ...}) = get_obj I pt p;
1.1627 - val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1.1628 - val (domID, metID) =
1.1629 - (string_of_thy thy, if length met = 0 then e_metID else hd met)
1.1630 - val ((p,_),_,_,pt) =
1.1631 - generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1.1632 - (Uistate, ctxt) pos pt
1.1633 - val (pbl, pre, pb) = ([], [], false)
1.1634 + val (dI', ctxt) = case get_obj I pt p of
1.1635 + PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
1.1636 + | _ => error "specify (Refine_Tacitly': uncovered case get_obj"
1.1637 + val {met, thy,...} = get_pbt pIre
1.1638 + val (domID, metID) = (string_of_thy thy, if length met = 0 then e_metID else hd met)
1.1639 + val ((p,_), _, _, pt) =
1.1640 + generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
1.1641 + val (pbl, pre, _) = ([], [], false)
1.1642 in ((p, Pbl), (pos, Uistate),
1.1643 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.1644 - (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1.1645 + Form' (PpcKF (0, EdUndef, length p, Nundef, (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1.1646 Model_Problem, Safe, pt)
1.1647 end
1.1648 -
1.1649 - | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1.1650 + | specify (Refine_Problem' rfd) pos _ pt =
1.1651 let
1.1652 val ctxt = get_ctxt pt pos
1.1653 - val (pos,_,_,pt) =
1.1654 + val (pos, _, _, pt) =
1.1655 generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.1656 - in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1.1657 - Model_Problem, Safe, pt)
1.1658 + in
1.1659 + (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Problems (RefinedKF rfd), Model_Problem, Safe, pt)
1.1660 end
1.1661 (*WN110515 initialise ctxt again from itms and add preconds*)
1.1662 - | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1.1663 + | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
1.1664 let
1.1665 - val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1.1666 - meth=met, ctxt, ...}) = get_obj I pt p;
1.1667 + val (oris, dI', pI', mI', dI, mI, ctxt, met) = case get_obj I pt p of
1.1668 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
1.1669 + (oris, dI', pI', mI', dI, mI, ctxt, met)
1.1670 + | _ => error "specify (Specify_Problem': uncovered case get_obj"
1.1671 val thy = assoc_thy dI
1.1672 - val ((p,Pbl),_,_,pt)=
1.1673 - generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt
1.1674 - val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1.1675 - val mI'' = if mI=e_metID then mI' else mI;
1.1676 - val (_, nxt) =
1.1677 - nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1.1678 - ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1.1679 - in ((p,Pbl), (pos,Uistate),
1.1680 + val (p, Pbl, pt) =
1.1681 + case generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of
1.1682 + ((p, Pbl), _, _, pt) => (p, Pbl, pt)
1.1683 + | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
1.1684 + val dI'' = assoc_thy (if dI=e_domID then dI' else dI)
1.1685 + val mI'' = if mI=e_metID then mI' else mI
1.1686 + val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o get_pbt) pI,
1.1687 + (#ppc o get_met) mI'') (dI, pI, mI);
1.1688 + in
1.1689 + ((p,Pbl), (pos,Uistate),
1.1690 Form' (PpcKF (0,EdUndef,(length p),Nundef, (Problem pI, itms2itemppc dI'' itms pre))),
1.1691 - nxt, Safe, pt)
1.1692 + nxt, Safe, pt)
1.1693 end
1.1694 (*WN110515 initialise ctxt again from itms and add preconds*)
1.1695 - | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1.1696 + | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) _ pt =
1.1697 let
1.1698 - val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1.1699 - meth=met, ctxt, ...}) = get_obj I pt p;
1.1700 + val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
1.1701 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
1.1702 + (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
1.1703 + | _ => error "specify (Specify_Problem': uncovered case get_obj"
1.1704 val {ppc,pre,prls,...} = get_met mID
1.1705 val thy = assoc_thy dI
1.1706 - val oris = add_field' thy ppc oris;
1.1707 - val dI'' = if dI=e_domID then dI' else dI;
1.1708 - val pI'' = if pI = e_pblID then pI' else pI;
1.1709 - val met = if met=[] then pbl else met;
1.1710 - val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1.1711 + val oris = add_field' thy ppc oris
1.1712 + val dI'' = if dI=e_domID then dI' else dI
1.1713 + val pI'' = if pI = e_pblID then pI' else pI
1.1714 + val met = if met = [] then pbl else met
1.1715 + val (_, (itms, pre')) = match_itms_oris thy met (ppc, pre, prls ) oris
1.1716 val (pos, _, _, pt) =
1.1717 generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.1718 - val (_,nxt) =
1.1719 - nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1.1720 - ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1.1721 - in (pos, (pos,Uistate),
1.1722 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.1723 - (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1.1724 - nxt, Safe, pt)
1.1725 + val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
1.1726 + ((#ppc o get_pbt) pI'', ppc) (dI'', pI'', mID)
1.1727 + in
1.1728 + (pos, (pos,Uistate),
1.1729 + Form' (PpcKF (0, EdUndef, length p, Nundef, (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1.1730 + nxt, Safe, pt)
1.1731 end
1.1732 -
1.1733 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1.1734 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1.1735 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1.1736 -
1.1737 - | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1.1738 + | specify (Specify_Theory' domID) (pos as (p,p_)) _ pt =
1.1739 let
1.1740 val p_ = case p_ of Met => Met | _ => Pbl
1.1741 - val thy = assoc_thy domID;
1.1742 - val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1.1743 - probl=pbl, spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1.1744 - val mppc = case p_ of Met => met | _ => pbl;
1.1745 - val cpI = if pI = e_pblID then pI' else pI;
1.1746 - val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1.1747 - val cmI = if mI = e_metID then mI' else mI;
1.1748 - val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1.1749 - val pre =
1.1750 - case p_ of
1.1751 - Met => (check_preconds thy mer mwh met)
1.1752 - | _ => (check_preconds thy per pwh pbl)
1.1753 + val thy = assoc_thy domID
1.1754 + val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of
1.1755 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} =>
1.1756 + (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)
1.1757 + | _ => error "specify (Specify_Theory': uncovered case get_obj"
1.1758 + val mppc = case p_ of Met => met | _ => pbl
1.1759 + val cpI = if pI = e_pblID then pI' else pI
1.1760 + val {prls = per, ppc, where_ = pwh, ...} = get_pbt cpI
1.1761 + val cmI = if mI = e_metID then mI' else mI
1.1762 + val {prls = mer, ppc = mpc, pre= mwh, ...} = get_met cmI
1.1763 + val pre = case p_ of
1.1764 + Met => (check_preconds thy mer mwh met)
1.1765 + | _ => (check_preconds thy per pwh pbl)
1.1766 val pb = foldl and_ (true, map fst pre)
1.1767 in
1.1768 if domID = dI
1.1769 then
1.1770 - let val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1.1771 - (pbl,met) (ppc,mpc) (dI,pI,mI);
1.1772 - in ((p,p_), (pos,Uistate),
1.1773 - Form'(PpcKF (0,EdUndef,(length p), Nundef,
1.1774 - (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.1775 - nxt,Safe,pt)
1.1776 + let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
1.1777 + in
1.1778 + ((p, p_), (pos, Uistate),
1.1779 + Form'(PpcKF (0, EdUndef, length p, Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.1780 + nxt, Safe, pt)
1.1781 end
1.1782 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1.1783 let
1.1784 - val ((p,p_),_,_,pt) =
1.1785 - generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
1.1786 - val (p_,nxt) =
1.1787 - nxt_spec p_ pb oris (dI',pI',mI') (pbl,met) (ppc,mpc) (domID,pI,mI);
1.1788 - in ((p,p_), (pos,Uistate),
1.1789 - Form' (PpcKF (0, EdUndef, (length p),Nundef,
1.1790 - (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.1791 - nxt, Safe,pt)
1.1792 + val ((p, p_), _, _, pt) = generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
1.1793 + val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
1.1794 + in
1.1795 + ((p,p_), (pos,Uistate),
1.1796 + Form' (PpcKF (0, EdUndef, length p, Nundef, (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.1797 + nxt, Safe, pt)
1.1798 end
1.1799 end
1.1800 -
1.1801 - | specify m' _ _ _ =
1.1802 - error ("specify: not impl. for " ^ tac_2str m');
1.1803 + | specify m' _ _ _ = error ("specify: not impl. for " ^ tac_2str m')
1.1804
1.1805 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
1.1806 -- for input from scratch*)
1.1807 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1.1808 - let
1.1809 - val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1.1810 - probl=pbl,spec=(dI,pI,_), ctxt, ...}) = get_obj I pt p;
1.1811 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.1812 - val cpI = if pI = e_pblID then pI' else pI;
1.1813 - in
1.1814 - case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
1.1815 - Add itm (*..union old input *) =>
1.1816 - let
1.1817 - (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1.1818 - val pbl' = insert_ppc thy itm pbl
1.1819 - val (tac,tac_) =
1.1820 - case sel of
1.1821 - "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1.1822 - | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1.1823 - | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1.1824 - val ((p,Pbl),c,_,pt') =
1.1825 - generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt
1.1826 - in ([(tac,tac_,((p,Pbl),(Uistate, ctxt)))], c, (pt',(p,Pbl))):calcstate'
1.1827 - end
1.1828 - | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
1.1829 - FIXME ..and dont abuse a tactic for that purpose*)
1.1830 - ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1.1831 - (e_pos', (e_istate, e_ctxt)))], [], ptp)
1.1832 - end
1.1833 + let
1.1834 + val (oris, dI', pI', dI, pI, pbl, ctxt) = case get_obj I pt p of
1.1835 + PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
1.1836 + (oris, dI', pI', dI, pI, pbl, ctxt)
1.1837 + | _ => error "specify (Specify_Theory': uncovered case get_obj"
1.1838 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.1839 + val cpI = if pI = e_pblID then pI' else pI;
1.1840 + in
1.1841 + case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
1.1842 + Add itm (*..union old input *) =>
1.1843 + let
1.1844 + val pbl' = insert_ppc thy itm pbl
1.1845 + val (tac, tac_) = case sel of
1.1846 + "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1.1847 + | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1.1848 + | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1.1849 + | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
1.1850 + val (p, Pbl, c, pt') = case generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of
1.1851 + ((p, Pbl), c, _, pt') => (p, Pbl, c, pt')
1.1852 + | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
1.1853 + in
1.1854 + ([(tac, tac_, ((p, Pbl), (Uistate, ctxt)))], c, (pt', (p, Pbl))) : calcstate'
1.1855 + end
1.1856 + | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
1.1857 + FIXME ..and dont abuse a tactic for that purpose*)
1.1858 + ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1.1859 + (e_pos', (e_istate, e_ctxt)))], [], ptp)
1.1860 + end
1.1861 + | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) =
1.1862 + let
1.1863 + val (oris, dI', mI', dI, mI, met, ctxt) = case get_obj I pt p of
1.1864 + PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
1.1865 + (oris, dI', mI', dI, mI, met, ctxt)
1.1866 + | _ => error "nxt_specif_additem Met: uncovered case get_obj"
1.1867 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.1868 + val cmI = if mI = e_metID then mI' else mI;
1.1869 + in
1.1870 + case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
1.1871 + Add itm (*..union old input *) =>
1.1872 + let
1.1873 + val met' = insert_ppc thy itm met;
1.1874 + val (tac,tac_) = case sel of
1.1875 + "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1.1876 + | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1.1877 + | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1.1878 + | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
1.1879 + val (p, Met, c, pt') = case generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of
1.1880 + ((p, Met), c, _, pt') => (p, Met, c, pt')
1.1881 + | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
1.1882 + in
1.1883 + ([(tac, tac_, ((p, Met), (Uistate, ctxt)))], c, (pt', (p, Met)))
1.1884 + end
1.1885 + | Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
1.1886 + end
1.1887 + | nxt_specif_additem _ _ (_, p) = error ("nxt_specif_additem not impl. for" ^ pos'2str p)
1.1888
1.1889 - | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1.1890 - let
1.1891 - val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.1892 - probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1.1893 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.1894 - val cmI = if mI = e_metID then mI' else mI;
1.1895 - in
1.1896 - case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
1.1897 - Add itm (*..union old input *) =>
1.1898 - let
1.1899 - val met' = insert_ppc thy itm met;
1.1900 - val (tac,tac_) =
1.1901 - case sel of
1.1902 - "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1.1903 - | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1.1904 - | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1.1905 - val ((p,Met),c,_,pt') =
1.1906 - generate1 thy tac_ (Uistate, ctxt) (p,Met) pt
1.1907 - in ([(tac,tac_,((p,Met), (Uistate, ctxt)))], c, (pt',(p,Met))) end
1.1908 - | Err msg => ([(*tacis*)], [], ptp)
1.1909 - (*nxt_me collects tacis until not hide; here just no progress*)
1.1910 - end;
1.1911 +fun ori2Coritm (pbt : pat list) ((i, v, f, d, ts) : ori) =
1.1912 + ((i, v, true, f, Cor ((d,ts),((snd o snd o the o (find_first (eq1 d))) pbt,ts))) : itm)
1.1913 + handle _ => ((i, v, true, f, Cor ((d, ts), (d, ts))) : itm)
1.1914 + (*dsc in oris, but not in pbl pat list: keep this dsc*)
1.1915
1.1916 -fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1.1917 - (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1.1918 - handle _ => error ("ori2Coritm: dsc "^
1.1919 - term2str d^
1.1920 - "in ori, but not in pbt")
1.1921 - ,ts))):itm;
1.1922 -fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
1.1923 - ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
1.1924 - (find_first (eq1 d))) pbt,ts))):itm)
1.1925 - handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
1.1926 - ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
1.1927 -
1.1928 -
1.1929 -(*filter out oris which have same description in itms*)
1.1930 +(* filter out oris which have same description in itms *)
1.1931 fun filter_outs oris [] = oris
1.1932 | filter_outs oris (i::itms) =
1.1933 - let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
1.1934 - (#4:ori -> term)) oris;
1.1935 - in filter_outs ors itms end;
1.1936 + let
1.1937 + val ors = filter_out ((curry op = ((d_in o #5) (i:itm))) o (#4 : ori -> term)) oris
1.1938 + in
1.1939 + filter_outs ors itms
1.1940 + end
1.1941
1.1942 -fun memI a b = member op = a b;
1.1943 -(*filter oris which are in pbt, too*)
1.1944 +(* filter oris which are in pbt, too *)
1.1945 fun filter_pbt oris pbt =
1.1946 - let val dscs = map (fst o snd) pbt
1.1947 - in filter ((memI dscs) o (#4: ori -> term)) oris end;
1.1948 + let
1.1949 + val dscs = map (fst o snd) pbt
1.1950 + in
1.1951 + filter ((member op= dscs) o (#4 : ori -> term)) oris
1.1952 + end
1.1953
1.1954 -(*.combine itms from pbl + met and complete them wrt. pbt.*)
1.1955 -(*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1.1956 -local infix mem;
1.1957 -fun x mem [] = false
1.1958 - | x mem (y :: ys) = x = y orelse x mem ys;
1.1959 -in
1.1960 -fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1.1961 -(* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1.1962 - *)
1.1963 - let val vat = max_vt pits;
1.1964 - val itms = pits @
1.1965 - (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
1.1966 - val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1.1967 - val os = filter_outs ors itms;
1.1968 - (*WN.12.03?: does _NOT_ add itms from met ?!*)
1.1969 - in itms @ (map (ori2Coritm met) os) end
1.1970 -end;
1.1971 +(* combine itms from pbl + met and complete them wrt. pbt *)
1.1972 +(* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1.1973 +fun complete_metitms (oris : ori list) (pits : itm list) (mits: itm list) met =
1.1974 + let
1.1975 + val vat = max_vt pits;
1.1976 + val itms = pits @ (filter ((member_swap op = vat) o (#2 : itm -> int list)) mits)
1.1977 + val ors = filter ((member_swap op= vat) o (#2 : ori -> int list)) oris
1.1978 + val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
1.1979 + in
1.1980 + itms @ (map (ori2Coritm met) os)
1.1981 + end
1.1982
1.1983 +(* complete model and guard of a calc-head *)
1.1984 +fun complete_mod_ (oris, mpc, ppc, probl) =
1.1985 + let
1.1986 + val pits = filter_out ((curry op= false) o (#3 : itm -> bool)) probl
1.1987 + val vat = if probl = [] then 1 else max_vt probl
1.1988 + val pors = filter ((member_swap op = vat) o (#2 : ori -> int list)) oris
1.1989 + val pors = filter_outs pors pits (*which are in pbl already*)
1.1990 + val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1.1991 + val pits = pits @ (map (ori2Coritm ppc) pors)
1.1992 + val mits = complete_metitms oris pits [] mpc
1.1993 + in (pits, mits) end
1.1994
1.1995 +fun some_spec ((odI, opI, omI) : spec) ((dI, pI, mI) : spec) =
1.1996 + (if dI = e_domID then odI else dI,
1.1997 + if pI = e_pblID then opI else pI,
1.1998 + if mI = e_metID then omI else mI) : spec
1.1999
1.2000 -(*.complete model and guard of a calc-head .*)
1.2001 -local infix mem;
1.2002 -fun x mem [] = false
1.2003 - | x mem (y :: ys) = x = y orelse x mem ys;
1.2004 -in
1.2005 -fun complete_mod_ (oris, mpc, ppc, probl) =
1.2006 - let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1.2007 - val vat = if probl = [] then 1 else max_vt probl
1.2008 - val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
1.2009 - val pors = filter_outs pors pits (*which are in pbl already*)
1.2010 - val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1.2011 -
1.2012 - val pits = pits @ (map (ori2Coritm ppc) pors)
1.2013 - val mits = complete_metitms oris pits [] mpc
1.2014 - in (pits, mits) end
1.2015 -end;
1.2016 -
1.2017 -fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1.2018 - (if dI = e_domID then odI else dI,
1.2019 - if pI = e_pblID then opI else pI,
1.2020 - if mI = e_metID then omI else mI):spec;
1.2021 -
1.2022 -
1.2023 -(*.find a next applicable tac (for calcstate) and update ptree
1.2024 - (for ev. finding several more tacs due to hide).*)
1.2025 -(*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
1.2026 -(*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1.2027 -(*WN.24.10.03 fun nxt_solv = ...................................??*)
1.2028 -fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1.2029 +(* find a next applicable tac (for calcstate) and update ptree
1.2030 + (for ev. finding several more tacs due to hide) *)
1.2031 +(* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *)
1.2032 +(* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *)
1.2033 +(* WN.24.10.03 fun nxt_solv = ...................................?? *)
1.2034 +fun nxt_specif (tac as Model_Problem) (pt, pos as (p, _)) =
1.2035 let
1.2036 - val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p
1.2037 + val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
1.2038 + PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
1.2039 + | _ => error "nxt_specif Model_Problem; uncovered case get_obj"
1.2040 val (dI, pI, mI) = some_spec ospec spec
1.2041 val thy = assoc_thy dI
1.2042 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1.2043 @@ -1343,525 +970,426 @@
1.2044 val pbl = init_pbl ppc (* fill in descriptions *)
1.2045 (*----------------if you think, this should be done by the Dialog
1.2046 in the java front-end, search there for WN060225-modelProblem----*)
1.2047 - val (pbl, met) =
1.2048 - case cas of NONE => (pbl, [])
1.2049 - | _ => complete_mod_ (oris, mpc, ppc, probl)
1.2050 + val (pbl, met) = case cas of
1.2051 + NONE => (pbl, [])
1.2052 + | _ => complete_mod_ (oris, mpc, ppc, probl)
1.2053 (*----------------------------------------------------------------*)
1.2054 val tac_ = Model_Problem' (pI, pbl, met)
1.2055 val (pos,c,_,pt) = generate1 thy tac_ (Uistate, ctxt) pos pt
1.2056 - in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
1.2057 -
1.2058 + in ([(tac, tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)) : calcstate' end
1.2059 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1.2060 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1.2061 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1.2062 -
1.2063 (*. called only if no_met is specified .*)
1.2064 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1.2065 - let
1.2066 - val (PblObj {origin = (oris, (dI,_,_),_), ctxt, ...}) = get_obj I pt p
1.2067 - val opt = refine_ori oris pI
1.2068 - in
1.2069 - case opt of
1.2070 - SOME pI' =>
1.2071 - let
1.2072 - val {met,ppc,...} = get_pbt pI'
1.2073 - val pbl = init_pbl ppc
1.2074 - (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1.2075 - val mI = if length met = 0 then e_metID else hd met
1.2076 - val thy = assoc_thy dI
1.2077 - val (pos,c,_,pt) =
1.2078 - generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1.2079 - (Uistate, ctxt) pos pt
1.2080 - in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1.2081 - (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.2082 - end
1.2083 - | NONE => ([], [], ptp)
1.2084 - end
1.2085 -
1.2086 + let
1.2087 + val (oris, dI, ctxt) = case get_obj I pt p of
1.2088 + (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
1.2089 + | _ => error "nxt_specif Refine_Tacitly: uncovered case get_obj"
1.2090 + val opt = refine_ori oris pI
1.2091 + in
1.2092 + case opt of
1.2093 + SOME pI' =>
1.2094 + let
1.2095 + val {met, ...} = get_pbt pI'
1.2096 + (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1.2097 + val mI = if length met = 0 then e_metID else hd met
1.2098 + val thy = assoc_thy dI
1.2099 + val (pos, c, _, pt) =
1.2100 + generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt
1.2101 + in
1.2102 + ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1.2103 + (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.2104 + end
1.2105 + | NONE => ([], [], ptp)
1.2106 + end
1.2107 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1.2108 - let
1.2109 - val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_), probl, ctxt, ...}) = get_obj I pt p
1.2110 - val thy = if dI' = e_domID then dI else dI'
1.2111 - in
1.2112 - case refine_pbl (assoc_thy thy) pI probl of
1.2113 - NONE => ([], [], ptp)
1.2114 - | SOME (rfd as (pI',_)) =>
1.2115 - let
1.2116 - val (pos,c,_,pt) = generate1 (assoc_thy thy)
1.2117 - (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.2118 - in ([(Refine_Problem pI, Refine_Problem' rfd,
1.2119 - (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.2120 - end
1.2121 - end
1.2122 -
1.2123 + let
1.2124 + val (dI, dI', probl, ctxt) = case get_obj I pt p of
1.2125 + PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
1.2126 + (dI, dI', probl, ctxt)
1.2127 + | _ => error "nxt_specif Refine_Problem: uncovered case get_obj"
1.2128 + val thy = if dI' = e_domID then dI else dI'
1.2129 + in
1.2130 + case refine_pbl (assoc_thy thy) pI probl of
1.2131 + NONE => ([], [], ptp)
1.2132 + | SOME rfd =>
1.2133 + let
1.2134 + val (pos,c,_,pt) = generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.2135 + in
1.2136 + ([(Refine_Problem pI, Refine_Problem' rfd, (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.2137 + end
1.2138 + end
1.2139 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1.2140 - let
1.2141 - val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...}) = get_obj I pt p;
1.2142 - val thy = assoc_thy (if dI' = e_domID then dI else dI');
1.2143 - val {ppc,where_,prls,...} = get_pbt pI
1.2144 - val pbl as (_,(itms,_)) =
1.2145 - if pI'=e_pblID andalso pI=e_pblID
1.2146 - then (false, (init_pbl ppc, []))
1.2147 - else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1.2148 - (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1.2149 - val ((p,Pbl),c,_,pt) =
1.2150 - generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt
1.2151 - in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1.2152 - (pos,(Uistate, e_ctxt)))], c, (pt,pos))
1.2153 - end
1.2154 -
1.2155 - (*transfers oris (not required in pbl) to met-model for script-env
1.2156 - FIXME.WN.8.03: application of several mIDs to SAME model?*)
1.2157 - | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1.2158 - let
1.2159 - val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1.2160 - meth=met, ctxt, ...}) = get_obj I pt p;
1.2161 - val {ppc,pre,prls,...} = get_met mID
1.2162 - val thy = assoc_thy dI
1.2163 - val oris = add_field' thy ppc oris;
1.2164 - val dI'' = if dI=e_domID then dI' else dI;
1.2165 - val pI'' = if pI = e_pblID then pI' else pI;
1.2166 - val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1.2167 - val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1.2168 - val (pos,c,_,pt)=
1.2169 - generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.2170 - in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1.2171 - (pos,(Uistate, e_ctxt)))], c, (pt,pos))
1.2172 - end
1.2173 -
1.2174 - | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1.2175 - let
1.2176 - val ctxt = get_ctxt pt pos
1.2177 - val (dI',_,_) = get_obj g_spec pt p
1.2178 - val (pos,c,_,pt) =
1.2179 - generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.2180 - in (*FIXXXME: check if pbl can still be parsed*)
1.2181 - ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, ctxt)))], c,
1.2182 - (pt, pos))
1.2183 - end
1.2184 -
1.2185 - | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1.2186 - let
1.2187 - val ctxt = get_ctxt pt pos
1.2188 - val (dI',_,_) = get_obj g_spec pt p
1.2189 - val (pos,c,_,pt) =
1.2190 - generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.2191 - in (*FIXXXME: check if met can still be parsed*)
1.2192 - ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, ctxt)))], c,
1.2193 - (pt, pos))
1.2194 - end
1.2195 -
1.2196 - | nxt_specif m' _ =
1.2197 - error ("nxt_specif: not impl. for "^tac2str m');
1.2198 + let
1.2199 + val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
1.2200 + PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...} =>
1.2201 + (oris, dI, dI', pI', probl, ctxt)
1.2202 + | _ => error ""
1.2203 + val thy = assoc_thy (if dI' = e_domID then dI else dI');
1.2204 + val {ppc,where_,prls,...} = get_pbt pI
1.2205 + val pbl =
1.2206 + if pI' = e_pblID andalso pI = e_pblID
1.2207 + then (false, (init_pbl ppc, []))
1.2208 + else match_itms_oris thy probl (ppc,where_,prls) oris
1.2209 + (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1.2210 + val (c, pt) = case generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
1.2211 + ((_, Pbl), c, _, pt) => (c, pt)
1.2212 + | _ => error ""
1.2213 + in
1.2214 + ([(Specify_Problem pI, Specify_Problem' (pI, pbl), (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.2215 + end
1.2216 + (* transfers oris (not required in pbl) to met-model for script-env
1.2217 + FIXME.WN.8.03: application of several mIDs to SAME model? *)
1.2218 + | nxt_specif (Specify_Method mID) (pt, pos as (p,_)) =
1.2219 + let
1.2220 + val (oris, pbl, dI, met, ctxt) = case get_obj I pt p of
1.2221 + PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}
1.2222 + => (oris, pbl, dI, met, ctxt)
1.2223 + | _ => error "nxt_specif Specify_Method: uncovered case get_obj"
1.2224 + val {ppc,pre,prls,...} = get_met mID
1.2225 + val thy = assoc_thy dI
1.2226 + val oris = add_field' thy ppc oris
1.2227 + val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
1.2228 + val (_, (itms, _)) = match_itms_oris thy met (ppc,pre,prls ) oris
1.2229 + val (pos, c, _, pt) =
1.2230 + generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.2231 + in
1.2232 + ([(Specify_Method mID, Specify_Method' (mID, oris, itms), (pos, (Uistate, e_ctxt)))], c, (pt, pos))
1.2233 + end
1.2234 + | nxt_specif (Specify_Theory dI) (pt, pos as (_, Pbl)) =
1.2235 + let
1.2236 + val ctxt = get_ctxt pt pos
1.2237 + val (pos, c, _, pt) =
1.2238 + generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.2239 + in (*FIXXXME: check if pbl can still be parsed*)
1.2240 + ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c,
1.2241 + (pt, pos))
1.2242 + end
1.2243 + | nxt_specif (Specify_Theory dI) (pt, pos as (_, Met)) =
1.2244 + let
1.2245 + val ctxt = get_ctxt pt pos
1.2246 + val (pos, c, _, pt) = generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.2247 + in (*FIXXXME: check if met can still be parsed*)
1.2248 + ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c, (pt, pos))
1.2249 + end
1.2250 + | nxt_specif m' _ = error ("nxt_specif: not impl. for "^tac2str m')
1.2251
1.2252 (* get the values from oris; handle the term list w.r.t. penv *)
1.2253 -local infix mem;
1.2254 -fun x mem [] = false
1.2255 - | x mem (y :: ys) = x = y orelse x mem ys;
1.2256 -in
1.2257 fun vals_of_oris oris =
1.2258 - ((map (mkval' o (#5:ori -> term list))) o
1.2259 - (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1.2260 -end;
1.2261 + ((map (mkval' o (#5 : ori -> term list))) o
1.2262 + (filter ((member_swap op= 1) o (#2 : ori -> int list)))) oris
1.2263
1.2264 (* create a calc-tree with oris via an cas.refined pbl *)
1.2265 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1.2266 - if pI <> []
1.2267 - then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1.2268 + if pI <> []
1.2269 + then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1.2270 + let
1.2271 + val {cas, met, ppc, thy, ...} = get_pbt pI
1.2272 + val dI = if dI = "" then theory2theory' thy else dI
1.2273 + val mI = if mI = [] then hd met else mI
1.2274 + val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1.2275 + val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI, pI, mI))
1.2276 + ([], (dI,pI,mI), hdl)
1.2277 + val pt = update_spec pt [] (dI, pI, mI)
1.2278 + val pits = init_pbl' ppc
1.2279 + val pt = update_pbl pt [] pits
1.2280 + in ((pt, ([] , Pbl)), []) : calcstate end
1.2281 + else
1.2282 + if mI <> []
1.2283 + then (* from met-browser *)
1.2284 let
1.2285 - val {cas, met, ppc, thy, ...} = get_pbt pI
1.2286 - val dI = if dI = "" then theory2theory' thy else dI
1.2287 - val thy = assoc_thy dI
1.2288 - val mI = if mI = [] then hd met else mI
1.2289 - val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1.2290 - val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1.2291 - ([], (dI,pI,mI), hdl)
1.2292 - val pt = update_spec pt [] (dI,pI,mI)
1.2293 - val pits = init_pbl' ppc
1.2294 - val pt = update_pbl pt [] pits
1.2295 - in ((pt, ([] ,Pbl)), []) : calcstate end
1.2296 - else
1.2297 - if mI <> []
1.2298 - then (* from met-browser *)
1.2299 - let
1.2300 - val {ppc,...} = get_met mI
1.2301 - val dI = if dI = "" then "Isac" else dI
1.2302 - val thy = assoc_thy dI;
1.2303 - val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1.2304 - ([], (dI,pI,mI), e_term(*FIXME met*));
1.2305 - val pt = update_spec pt [] (dI,pI,mI);
1.2306 - val mits = init_pbl' ppc;
1.2307 - val pt = update_met pt [] mits;
1.2308 - in ((pt, ([], Met)), []) : calcstate end
1.2309 - else (* new example, pepare for interactive modeling *)
1.2310 - let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1.2311 - ([], e_spec, e_term)
1.2312 - in ((pt, ([], Pbl)), []) : calcstate end
1.2313 + val {ppc, ...} = get_met mI
1.2314 + val dI = if dI = "" then "Isac" else dI
1.2315 + val (pt, _) =
1.2316 + cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
1.2317 + val pt = update_spec pt [] (dI, pI, mI)
1.2318 + val mits = init_pbl' ppc
1.2319 + val pt = update_met pt [] mits
1.2320 + in ((pt, ([], Met)), []) end
1.2321 + else (* new example, pepare for interactive modeling *)
1.2322 + let
1.2323 + val (pt, _) =
1.2324 + cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term)
1.2325 + in ((pt, ([], Pbl)), []) end
1.2326 + | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1.2327 + let (* both """"""""""""""""""""""""" either empty or complete *)
1.2328 + val thy = assoc_thy dI
1.2329 + val (pI, (pors, pctxt), mI) =
1.2330 + if mI = ["no_met"]
1.2331 + then
1.2332 + let
1.2333 + val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
1.2334 + val pI' = refine_ori' pors pI;
1.2335 + in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
1.2336 + (hd o #met o get_pbt) pI')
1.2337 + end
1.2338 + else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
1.2339 + val {cas, ppc, thy = thy', ...} = get_pbt pI (*take dI from _refined_ pbl*)
1.2340 + val dI = theory2theory' (maxthy thy thy')
1.2341 + val hdl = case cas of
1.2342 + NONE => pblterm dI pI
1.2343 + | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
1.2344 + val (pt, _) =
1.2345 + cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
1.2346 + val pt = update_ctxt pt [] pctxt
1.2347 + in
1.2348 + ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1.2349 + end
1.2350
1.2351 - | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1.2352 - let (* both """"""""""""""""""""""""" either empty or complete *)
1.2353 - val thy = assoc_thy dI
1.2354 - val (pI, (pors, pctxt), mI) =
1.2355 - if mI = ["no_met"]
1.2356 - then
1.2357 - let
1.2358 - val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
1.2359 - val pI' = refine_ori' pors pI;
1.2360 - in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
1.2361 - (hd o #met o get_pbt) pI') end
1.2362 - else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
1.2363 - val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1.2364 - val dI = theory2theory' (maxthy thy thy')
1.2365 - val hdl =
1.2366 - case cas of
1.2367 - NONE => pblterm dI pI
1.2368 - | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
1.2369 - val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
1.2370 - (pors, (dI, pI, mI), hdl)
1.2371 - val pt = update_ctxt pt [] pctxt
1.2372 - in ((pt, ([], Pbl)),
1.2373 - fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1.2374 - end;
1.2375 +fun get_spec_form m ((p, p_) : pos') pt =
1.2376 + let val (_, _, f, _, _, _) = specify m (p, p_) [] pt
1.2377 + in f end
1.2378
1.2379 -
1.2380 -
1.2381 -(*18.12.99*)
1.2382 -fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
1.2383 -(* case appl_spec p pt m of /// 19.1.00
1.2384 - Notappl e => Error' (Error_ e)
1.2385 - | Appl =>
1.2386 -*) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1.2387 - in f end;
1.2388 -
1.2389 -
1.2390 -(*fun tag_form thy (formal, given) = Thm.global_cterm_of thy
1.2391 - (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819*)
1.2392 +(* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
1.2393 + (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
1.2394 fun tag_form thy (formal, given) =
1.2395 (let
1.2396 val gf = (head_of given) $ formal;
1.2397 val _ = Thm.global_cterm_of thy gf
1.2398 in gf end)
1.2399 handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^
1.2400 - " .. " ^ term_to_string''' thy formal ^ " ..types do not match");
1.2401 -(* val formal = (the o (parse thy)) "[R::real]";
1.2402 -> val given = (the o (parse thy)) "fixed_values (cs::real list)";
1.2403 -> tag_form thy (formal, given);
1.2404 -val it = "fixed_values [R]" : cterm
1.2405 -*)
1.2406 + " .. " ^ term_to_string''' thy formal ^ " ..types do not match")
1.2407
1.2408 fun chktyp thy (n, fs, gs) =
1.2409 ((writeln o (term_to_string''' thy) o (nth n)) fs;
1.2410 (writeln o (term_to_string''' thy) o (nth n)) gs;
1.2411 - tag_form thy (nth n fs, nth n gs));
1.2412 -fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1.2413 -
1.2414 -(* #####################################################
1.2415 - find the failing item:
1.2416 -> val n = 2;
1.2417 -> val tag__form = chktyp (n,formals,givens);
1.2418 -> (type_of o Thm.term_of o (nth n)) formals;
1.2419 -> (type_of o Thm.term_of o (nth n)) givens;
1.2420 -> atomty ((Thm.term_of o (nth n)) formals);
1.2421 -> atomty ((Thm.term_of o (nth n)) givens);
1.2422 -> atomty (Thm.term_of tag__form);
1.2423 -> use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
1.2424 - ##################################################### *)
1.2425 -
1.2426 -(* #####################################################
1.2427 - testdata setup
1.2428 -val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
1.2429 -val formals = map (the o (parse thy)) origin;
1.2430 -
1.2431 -val given = ["equation (lhs=rhs)",
1.2432 - "bound_variable bdv", (* TODO type *)
1.2433 - "error_bound apx"];
1.2434 -val where_ = ["e is_root_equation_in bdv",
1.2435 - "bdv is_var",
1.2436 - "apx is_const_expr"];
1.2437 -val find = ["L::rat set"];
1.2438 -val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
1.2439 -val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1.2440 -val givens = map (the o (parse thy)) given;
1.2441 -
1.2442 -val tag__forms = chktyps (formals, givens);
1.2443 -map ((atomty) o Thm.term_of) tag__forms;
1.2444 - ##################################################### *)
1.2445 -
1.2446 + tag_form thy (nth n fs, nth n gs))
1.2447 +fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs)
1.2448
1.2449 (* check pbltypes, announces one failure a time *)
1.2450 -(*fun chk_vars ctppc =
1.2451 - let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1.2452 - appc flat (mappc (vars o Thm.term_of) ctppc)
1.2453 - in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
1.2454 - else if (re\\(gi union fi)) <> []
1.2455 - then ("re\\(gi union fi)",re\\(gi union fi))
1.2456 - else ("ok",[]) end;*)
1.2457 fun chk_vars ctppc =
1.2458 - let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1.2459 - appc flat (mappc vars ctppc)
1.2460 - val chked = subtract op = gi wh
1.2461 - in if chked <> [] then ("wh\\gi", chked)
1.2462 - else let val chked = subtract op = (union op = gi fi) re
1.2463 - in if chked <> []
1.2464 - then ("re\\(gi union fi)", chked)
1.2465 - else ("ok", [])
1.2466 - end
1.2467 - end;
1.2468 + let
1.2469 + val {Given = gi, Where = wh, Find = fi, Relate = re, ...} = appc flat (mappc vars ctppc)
1.2470 + val chked = subtract op = gi wh
1.2471 + in
1.2472 + if chked <> [] then ("wh\\gi", chked)
1.2473 + else
1.2474 + let val chked = subtract op = (union op = gi fi) re
1.2475 + in
1.2476 + if chked <> []
1.2477 + then ("re\\(gi union fi)", chked)
1.2478 + else ("ok", [])
1.2479 + end
1.2480 + end
1.2481
1.2482 (* check a new pbltype: variables (Free) unbound by given, find*)
1.2483 fun unbound_ppc ctppc =
1.2484 - let val {Given=gi,Find=fi,Relate=re,...} =
1.2485 - appc flat (mappc vars ctppc)
1.2486 - in distinct (*re\\(gi union fi)*)
1.2487 - (subtract op = (union op = gi fi) re) end;
1.2488 -(*
1.2489 -> val org = {Given=["[R=(R::real)]"],Where=[],
1.2490 - Find=["[A::real]"],With=[],
1.2491 - Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
1.2492 - }:string ppc;
1.2493 -> val ctppc = mappc (the o (parse thy)) org;
1.2494 -> unbound_ppc ctppc;
1.2495 -val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
1.2496 -*)
1.2497 + let
1.2498 + val {Given = gi, Find = fi, Relate = re, ...} = appc flat (mappc vars ctppc)
1.2499 + in
1.2500 + distinct (subtract op = (union op = gi fi) re)
1.2501 + end
1.2502
1.2503 -
1.2504 -(* f, a binary operator, is nested rightassociative *)
1.2505 +(* f, a binary operator, is nested right associative *)
1.2506 fun foldr1 f xs =
1.2507 let
1.2508 - fun fld f (x::[]) = x
1.2509 - | fld f (x::x'::[]) = f (x',x)
1.2510 - | fld f (x::x'::xs) = f (fld f (x'::xs),x);
1.2511 - in ((fld f) o rev) xs end;
1.2512 -(*
1.2513 -> val (SOME ct) = parse thy "[a=b,c=d,e=f]";
1.2514 -> val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
1.2515 -> val conj = foldr1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
1.2516 -> Thm.global_cterm_of thy conj;
1.2517 -val it = "(a = b & c = d) & e = f" : cterm
1.2518 -*)
1.2519 + fun fld _ (x :: []) = x
1.2520 + | fld f (x :: x' :: []) = f (x', x)
1.2521 + | fld f (x :: x' :: xs) = f (fld f (x' :: xs), x)
1.2522 + | fld _ _ = error "foldr1 uncovered definition"
1.2523 + in ((fld f) o rev) xs end
1.2524
1.2525 (* f, a binary operator, is nested leftassociative *)
1.2526 -fun foldl1 f (x::[]) = x
1.2527 - | foldl1 f (x::x'::[]) = f (x,x')
1.2528 - | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1.2529 -(*
1.2530 -> val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
1.2531 -> val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
1.2532 -> val conj = foldl1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
1.2533 -> Thm.global_cterm_of thy conj;
1.2534 -val it = "a = b & c = d & e = f & g = h" : cterm
1.2535 -*)
1.2536 -
1.2537 +fun foldl1 _ (x :: []) = x
1.2538 + | foldl1 f (x :: x' :: []) = f (x, x')
1.2539 + | foldl1 f (x :: x' :: xs) = f (x, foldl1 f (x' :: xs))
1.2540 + | foldl1 _ _ = error "foldl1 uncovered definition"
1.2541
1.2542 (* called only once, if a Subproblem has been located in the script*)
1.2543 -fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_,_)) ptp =
1.2544 - (case metID of
1.2545 - ["no_met"] =>
1.2546 - (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1.2547 - | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1.2548 - (*all stored in tac_ itms^^^^^^^^^^*)
1.2549 - | nxt_model_pbl tac_ _ =
1.2550 - error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_);
1.2551 +fun nxt_model_pbl (Subproblem' ((_, pblID, metID), _, _, _, _, _)) ptp =
1.2552 + (case metID of
1.2553 + ["no_met"] => (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1.2554 + | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1.2555 + (*all stored in tac_ itms^^^^^^^^^^*)
1.2556 + | nxt_model_pbl tac_ _ = error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_)
1.2557
1.2558 -(*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1.2559 -fun eq4 v (_,vts,_,_,_) = member op = vts v;
1.2560 -fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1.2561 +(* fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml *)
1.2562 +fun eq4 v (_, vts, _, _, _) = member op = vts v
1.2563 +fun eq5 (_, _, _, _, itm_) (_, _, _, d, _) = d_in itm_ = d
1.2564
1.2565 -
1.2566 -(*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1.2567 - + met from fmz; assumes pos on PblObj, meth = [].*)
1.2568 -fun complete_mod (pt, pos as (p, p_):pos') =
1.2569 -(* val (pt, (p, _)) = (pt, p);
1.2570 - val (pt, (p, _)) = (pt, pos);
1.2571 - *)
1.2572 - let val _= if p_ <> Pbl
1.2573 - then tracing("###complete_mod: only impl.for Pbl, called with "^
1.2574 - pos'2str pos) else ()
1.2575 - val (PblObj{origin=(oris, ospec, hdl), probl, spec, ...}) =
1.2576 - get_obj I pt p
1.2577 - val (dI,pI,mI) = some_spec ospec spec
1.2578 - val mpc = (#ppc o get_met) mI
1.2579 - val ppc = (#ppc o get_pbt) pI
1.2580 - val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1.2581 - val pt = update_pblppc pt p pits
1.2582 - val pt = update_metppc pt p mits
1.2583 - in (pt, (p,Met):pos') end
1.2584 -;
1.2585 -(*| complete_mod (pt, pos as (p, Met):pos') =
1.2586 - error ("###complete_mod: only impl.for Pbl, called with "^
1.2587 - pos'2str pos);*)
1.2588 +(* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1.2589 + + met from fmz; assumes pos on PblObj, meth = [] *)
1.2590 +fun complete_mod (pt, pos as (p, p_) : pos') =
1.2591 + let
1.2592 + val _ = if p_ <> Pbl
1.2593 + then error ("###complete_mod: only impl.for Pbl, called with " ^ pos'2str pos)
1.2594 + else ()
1.2595 + val (oris, ospec, probl, spec) = case get_obj I pt p of
1.2596 + PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
1.2597 + | _ => error "complete_mod: unvered case get_obj"
1.2598 + val (_, pI, mI) = some_spec ospec spec
1.2599 + val mpc = (#ppc o get_met) mI
1.2600 + val ppc = (#ppc o get_pbt) pI
1.2601 + val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1.2602 + val pt = update_pblppc pt p pits
1.2603 + val pt = update_metppc pt p mits
1.2604 + in (pt, (p, Met) : pos') end
1.2605
1.2606 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1.2607 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1.2608 -fun all_modspec (pt, (p,_):pos') =
1.2609 - let
1.2610 - val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
1.2611 - val thy = assoc_thy dI;
1.2612 - val {ppc, ...} = get_met mI;
1.2613 - val (fmz_, vals) = oris2fmz_vals pors;
1.2614 +fun all_modspec (pt, (p, _) : pos') =
1.2615 + let
1.2616 + val (pors, dI, pI, mI) = case get_obj I pt p of
1.2617 + PblObj {origin = (pors, (dI, pI, mI), _), ...} => (pors, dI, pI, mI)
1.2618 + | _ => error "all_modspec: uncovered case get_obj"
1.2619 + val {ppc, ...} = get_met mI
1.2620 + val (_, vals) = oris2fmz_vals pors
1.2621 val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
1.2622 |> declare_constraints' vals
1.2623 - val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1.2624 - val pt = update_metppc pt p (map (ori2Coritm ppc) pors); (*WN110716 = _pblppc ?!?*)
1.2625 - val pt = update_spec pt p (dI,pI,mI);
1.2626 + val pt = update_pblppc pt p (map (ori2Coritm ppc) pors)
1.2627 + val pt = update_metppc pt p (map (ori2Coritm ppc) pors) (*WN110716 = _pblppc ?!?*)
1.2628 + val pt = update_spec pt p (dI, pI, mI)
1.2629 val pt = update_ctxt pt p ctxt
1.2630 -(*
1.2631 - val mors = prep_ori fmz_ thy ppc |> #1;
1.2632 - val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1.2633 - val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1.2634 - (*WN110715: why pors, mors handled so differently?*)
1.2635 - val pt = update_spec pt p (dI,pI,mI);
1.2636 -*)
1.2637 - in (pt, (p,Met): pos') end;
1.2638 + in
1.2639 + (pt, (p, Met) : pos')
1.2640 + end
1.2641
1.2642 -(*WN0312: use in nxt_spec, too ? what about variants ???*)
1.2643 -fun is_complete_mod_ ([]: itm list) = false
1.2644 - | is_complete_mod_ itms =
1.2645 - foldl and_ (true, (map #3 itms));
1.2646 +(* WN0312: use in nxt_spec, too ? what about variants ??? *)
1.2647 +fun is_complete_mod_ ([] : itm list) = false
1.2648 + | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))
1.2649
1.2650 -fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1.2651 - if (is_pblobj o (get_obj I pt)) p
1.2652 - then (is_complete_mod_ o (get_obj g_pbl pt)) p
1.2653 - else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1.2654 +fun is_complete_mod (pt, pos as (p, Pbl) : pos') =
1.2655 + if (is_pblobj o (get_obj I pt)) p
1.2656 + then (is_complete_mod_ o (get_obj g_pbl pt)) p
1.2657 + else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1.2658 | is_complete_mod (pt, pos as (p, Met)) =
1.2659 - if (is_pblobj o (get_obj I pt)) p
1.2660 - then (is_complete_mod_ o (get_obj g_met pt)) p
1.2661 - else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1.2662 + if (is_pblobj o (get_obj I pt)) p
1.2663 + then (is_complete_mod_ o (get_obj g_met pt)) p
1.2664 + else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1.2665 | is_complete_mod (_, pos) =
1.2666 - error ("is_complete_mod called by " ^ pos'2str pos ^
1.2667 - " (should be Pbl or Met)");
1.2668 + error ("is_complete_mod called by " ^ pos'2str pos ^ " (should be Pbl or Met)")
1.2669
1.2670 -(*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1.2671 -fun is_complete_spec (pt, pos as (p,_): pos') =
1.2672 - if (not o is_pblobj o (get_obj I pt)) p
1.2673 - then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1.2674 - else let val (dI,pI,mI) = get_obj g_spec pt p
1.2675 - in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
1.2676 -(*.complete empty items in specification from origin (pbl, met ev.refined);
1.2677 - assumes 'is_complete_mod'.*)
1.2678 -fun complete_spec (pt, pos as (p,_): pos') =
1.2679 - let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
1.2680 - val pt = update_spec pt p (some_spec ospec spec)
1.2681 - in (pt, pos) end;
1.2682 +(* have (thy, pbl, met) _all_ been specified explicitly ? *)
1.2683 +fun is_complete_spec (pt, pos as (p, _) : pos') =
1.2684 + if (not o is_pblobj o (get_obj I pt)) p
1.2685 + then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1.2686 + else
1.2687 + let val (dI,pI,mI) = get_obj g_spec pt p
1.2688 + in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end
1.2689
1.2690 -fun is_complete_modspec ptp =
1.2691 - is_complete_mod ptp andalso is_complete_spec ptp;
1.2692 +(* complete empty items in specification from origin (pbl, met ev.refined);
1.2693 + assumes 'is_complete_mod' *)
1.2694 +fun complete_spec (pt, pos as (p, _) : pos') =
1.2695 + let
1.2696 + val (ospec, spec) = case get_obj I pt p of
1.2697 + PblObj {origin = (_,ospec,_), spec,...} => (ospec, spec)
1.2698 + | _ => error "complete_spec: uncovered case get_obj"
1.2699 + val pt = update_spec pt p (some_spec ospec spec)
1.2700 + in
1.2701 + (pt, pos)
1.2702 + end
1.2703
1.2704 +fun is_complete_modspec ptp = is_complete_mod ptp andalso is_complete_spec ptp
1.2705
1.2706 +fun pt_model (PblObj {meth, spec, origin = (_, spec', hdl), ...}) Met =
1.2707 + let
1.2708 + val (_, _, metID) = get_somespec' spec spec'
1.2709 + val pre = if metID = e_metID then []
1.2710 + else
1.2711 + let
1.2712 + val {prls, pre= where_, ...} = get_met metID
1.2713 + val pre = check_preconds' prls where_ meth 0
1.2714 + in pre end
1.2715 + val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))
1.2716 + in
1.2717 + ModSpec (allcorrect, Met, hdl, meth, pre, spec)
1.2718 + end
1.2719 + | pt_model (PblObj {probl, spec, origin = (_, spec', hdl), ...}) _(*Frm,Pbl*) =
1.2720 + let
1.2721 + val (_, pI, _) = get_somespec' spec spec'
1.2722 + val pre = if pI = e_pblID then []
1.2723 + else
1.2724 + let
1.2725 + val {prls, where_, ...} = get_pbt pI
1.2726 + val pre = check_preconds' prls where_ probl 0
1.2727 + in pre end
1.2728 + val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))
1.2729 + in
1.2730 + ModSpec (allcorrect, Pbl, hdl, probl, pre, spec)
1.2731 + end
1.2732 + | pt_model _ _ = error "pt_model: uncovered definition"
1.2733
1.2734 +fun pt_form (PrfObj {form, ...}) = Form form
1.2735 + | pt_form (PblObj {probl, spec, origin = (_, spec', _), ...}) =
1.2736 + let
1.2737 + val (dI, pI, _) = get_somespec' spec spec'
1.2738 + val {cas, ...} = get_pbt pI
1.2739 + in case cas of
1.2740 + NONE => Form (pblterm dI pI)
1.2741 + | SOME t => Form (subst_atomic (mk_env probl) t)
1.2742 + end
1.2743
1.2744 -fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
1.2745 -(* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
1.2746 - *)
1.2747 - let val (_,_,metID) = get_somespec' spec spec'
1.2748 - val pre =
1.2749 - if metID = e_metID then []
1.2750 - else let val {prls,pre=where_,...} = get_met metID
1.2751 - val pre = check_preconds' prls where_ meth 0
1.2752 - in pre end
1.2753 - val allcorrect = is_complete_mod_ meth
1.2754 - andalso foldl and_ (true, (map #1 pre))
1.2755 - in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
1.2756 - | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
1.2757 -(* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
1.2758 - *)
1.2759 - let val (_,pI,_) = get_somespec' spec spec'
1.2760 - val pre =
1.2761 - if pI = e_pblID then []
1.2762 - else let val {prls,where_,cas,...} = get_pbt pI
1.2763 - val pre = check_preconds' prls where_ probl 0
1.2764 - in pre end
1.2765 - val allcorrect = is_complete_mod_ probl
1.2766 - andalso foldl and_ (true, (map #1 pre))
1.2767 - in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
1.2768 -
1.2769 -
1.2770 -fun pt_form (PrfObj {form,...}) = Form form
1.2771 - | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
1.2772 - let val (dI, pI, _) = get_somespec' spec spec'
1.2773 - val {cas,...} = get_pbt pI
1.2774 - in case cas of
1.2775 - NONE => Form (pblterm dI pI)
1.2776 - | SOME t => Form (subst_atomic (mk_env probl) t)
1.2777 - end;
1.2778 -(*vvv takes the tac _generating_ the formula=result, asm ok....
1.2779 -fun pt_result (PrfObj {result=(t,asm), tac,...}) =
1.2780 - (Form t,
1.2781 - if null asm then NONE else SOME asm,
1.2782 - SOME tac)
1.2783 - | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
1.2784 - let val (_,_,metID) = some_spec ospec spec
1.2785 - in (Form t,
1.2786 - if null asm then NONE else SOME asm,
1.2787 - if metID = e_metID then NONE else SOME (Apply_Method metID)) end;
1.2788 --------------------------------------------------------------------------*)
1.2789 -
1.2790 -
1.2791 -(*.pt_extract returns
1.2792 +(* pt_extract returns
1.2793 # the formula at pos
1.2794 # the tactic applied to this formula
1.2795 # the list of assumptions generated at this formula
1.2796 (by application of another tac to the preceding formula !)
1.2797 - pos is assumed to come from the frontend, ie. generated by moveDown.*)
1.2798 -(*cannot be in ctree.sml, because ModSpec has to be calculated*)
1.2799 -fun pt_extract (pt,([],Res)) = (* WN120512: --returns--> Check_Postcondition WRONGLY
1.2800 - see --- build fun is_exactly_equal*)
1.2801 - (* ML_TODO 110417 get assumptions from ctxt !? *)
1.2802 - let val (f, asm) = get_obj g_result pt []
1.2803 - in (Form f, NONE, asm) end
1.2804 + pos is assumed to come from the frontend, ie. generated by moveDown.
1.2805 + Notes: cannot be in ctree.sml, because ModSpec has to be calculated.
1.2806 + TODO 110417 get assumptions from ctxt !?
1.2807 +*)
1.2808 +fun pt_extract (pt, ([], Res)) =
1.2809 + (* WN120512: returns Check_Postcondition WRONGLY see --- build fun is_exactly_equal *)
1.2810 + let
1.2811 + val (f, asm) = get_obj g_result pt []
1.2812 + in (Form f, NONE, asm) end
1.2813 | pt_extract (pt,(p,Res)) =
1.2814 - let
1.2815 - val (f, asm) = get_obj g_result pt p
1.2816 - val tac =
1.2817 - if last_onlev pt p
1.2818 + let
1.2819 + val (f, asm) = get_obj g_result pt p
1.2820 + val tac =
1.2821 + if last_onlev pt p
1.2822 + then
1.2823 + if is_pblobj' pt (lev_up p)
1.2824 then
1.2825 - if is_pblobj' pt (lev_up p)
1.2826 - then
1.2827 - let
1.2828 - val (PblObj{spec=(_,pI,_),...}) = get_obj I pt (lev_up p)
1.2829 - in if pI = e_pblID then NONE else SOME (Check_Postcond pI) end
1.2830 - else SOME End_Trans (*WN0502 TODO for other branches*)
1.2831 - else
1.2832 - let val p' = lev_on p
1.2833 - in
1.2834 - if is_pblobj' pt p'
1.2835 - then
1.2836 - let val (PblObj{origin = (_,(dI,pI,_),_),...}) = get_obj I pt p'
1.2837 - in SOME (Subproblem (dI, pI)) end
1.2838 - else
1.2839 - if f = get_obj g_form pt p'
1.2840 - then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)
1.2841 - else SOME (Take (term2str (get_obj g_form pt p')))
1.2842 - end
1.2843 - in (Form f, tac, asm) end
1.2844 - | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
1.2845 + let
1.2846 + val pI = case get_obj I pt (lev_up p) of
1.2847 + PblObj{spec = (_, pI, _), ...} => pI
1.2848 + | _ => error "pt_extract last_onlev: uncovered case get_obj"
1.2849 + in if pI = e_pblID then NONE else SOME (Check_Postcond pI) end
1.2850 + else SOME End_Trans (* WN0502 TODO for other branches *)
1.2851 + else
1.2852 + let val p' = lev_on p
1.2853 + in
1.2854 + if is_pblobj' pt p'
1.2855 + then
1.2856 + let
1.2857 + val (dI ,pI) = case get_obj I pt p' of
1.2858 + PblObj{origin = (_, (dI, pI, _), _), ...} => (dI ,pI)
1.2859 + | _ => error "pt_extract \<not>last_onlev: uncovered case get_obj"
1.2860 + in SOME (Subproblem (dI, pI)) end
1.2861 + else
1.2862 + if f = get_obj g_form pt p'
1.2863 + then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)
1.2864 + else SOME (Take (term2str (get_obj g_form pt p')))
1.2865 + end
1.2866 + in (Form f, tac, asm) end
1.2867 + | pt_extract (pt, (p,p_(*Frm,Pbl*))) =
1.2868 let
1.2869 val ppobj = get_obj I pt p
1.2870 val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p
1.2871 val tac = g_tac ppobj
1.2872 - in (f, SOME tac, []) end;
1.2873 + in (f, SOME tac, []) end
1.2874
1.2875 +(** get the formula from a ctree-node:
1.2876 + take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1.2877 + take res from all other PrfObj's
1.2878 + Designed for interSteps, outcommented 04 in favour of calcChangedEvent **)
1.2879 +fun formres p (Nd (PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =
1.2880 + [("headline", (p, Frm), h), ("stepform", (p, Res), r)]
1.2881 + | formres p (Nd (PrfObj {form, result = (r, _), ...}, _)) =
1.2882 + [("stepform", (p, Frm), form), ("stepform", (p, Res), r)]
1.2883 + | formres _ _ = error "formres: uncovered definition"
1.2884 +fun form p (Nd (PrfObj {result = (r, _), ...}, _)) =
1.2885 + [("stepform", (p, Res), r)]
1.2886 + | form _ _ = error "form: uncovered definition"
1.2887
1.2888 -(**. get the formula from a ctree-node:
1.2889 - take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1.2890 - take res from all other PrfObj's .**)
1.2891 -(*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
1.2892 -fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
1.2893 - [("headline", (p, Frm), h),
1.2894 - ("stepform", (p, Res), r)]
1.2895 - | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
1.2896 - [("stepform", (p, Frm), form),
1.2897 - ("stepform", (p, Res), r)];
1.2898 -
1.2899 -fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
1.2900 - [("stepform", (p, Res), r)]
1.2901 -
1.2902 -(*assumes to take whole level, in particular hd -- for use in interSteps*)
1.2903 -fun get_formress fs p [] = flat fs
1.2904 +(* assumes to take whole level, in particular hd -- for use in interSteps *)
1.2905 +fun get_formress fs _ [] = flat fs
1.2906 | get_formress fs p (nd::nds) =
1.2907 (* start with 'form+res' and continue with trying 'res' only*)
1.2908 get_forms (fs @ [formres p nd]) (lev_on p) nds
1.2909 -and get_forms fs p [] = flat fs
1.2910 +and get_forms fs _ [] = flat fs
1.2911 | get_forms fs p (nd::nds) =
1.2912 if is_pblnd nd
1.2913 (* start again with 'form+res' ///ugly repeat with Check_elementwise
1.2914 @@ -1870,28 +1398,17 @@
1.2915 (* continue with trying 'res' only*)
1.2916 else get_forms (fs @ [form p nd]) (lev_on p) nds;
1.2917
1.2918 -(**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
1.2919 -(*WN050219 made robust against _'to' below or after Complete nodes
1.2920 - by handling exn caused by move_dn*)
1.2921 -(*WN0401 this functionality belongs to ctree.sml,
1.2922 -but fetching a calc_head requires calculations defined in modspec.sml
1.2923 -transfer to ME/me.sml !!!
1.2924 -WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
1.2925 -is returned !!!!!!!!!!!!!
1.2926 -*)
1.2927 -fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
1.2928 - | eq_pos' (p1,Res) (p2,Res) = p1 = p2
1.2929 - | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
1.2930 - Pbl => true
1.2931 - | Met => true
1.2932 - | _ => false)
1.2933 - | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
1.2934 - Pbl => true
1.2935 - | Met => true
1.2936 - | _ => false)
1.2937 +(** get an 'interval' 'from' 'to' of formulae from a ptree **)
1.2938 +(* WN0401 this functionality belongs to ctree.sml *)
1.2939 +fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2
1.2940 + | eq_pos' (p1, Res) (p2, Res) = p1 = p2
1.2941 + | eq_pos' (p1, Pbl) (p2, p2_) =
1.2942 + p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
1.2943 + | eq_pos' (p1, Met) (p2, p2_) =
1.2944 + p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)
1.2945 | eq_pos' _ _ = false;
1.2946
1.2947 -(*.get an 'interval' from the ctree; 'interval' is w.r.t. the
1.2948 +(* get an 'interval' from the ctree; 'interval' is w.r.t. the
1.2949 total ordering Position#compareTo(Position p) in the java-code
1.2950 val get_interval = fn
1.2951 : pos' -> : from is "move_up 1st-element" to return
1.2952 @@ -1901,23 +1418,16 @@
1.2953 ptree -> :
1.2954 (pos' * : of the formula
1.2955 Term.term) : the formula
1.2956 - list
1.2957 -.*)
1.2958 + list *)
1.2959 fun get_interval from to level pt =
1.2960 let
1.2961 - fun get_inter c (from:pos') (to:pos') lev pt =
1.2962 - if eq_pos' from to orelse from = ([],Res)
1.2963 - (*orelse ... avoids Exception- PTREE "end of calculation" raised,
1.2964 - if 'to' has values NOT generated by move_dn, see systest/me.sml
1.2965 - TODO.WN0501: introduce an order on pos' and check "from > to"..
1.2966 - ...there is an order in Java!
1.2967 - WN051224 the hack got worse with returning term instead ptform*)
1.2968 + fun get_inter c (from : pos') (to : pos') lev pt =
1.2969 + if eq_pos' from to orelse from = ([], Res)
1.2970 then
1.2971 - let val (f,_,_) = pt_extract (pt, from)
1.2972 - in
1.2973 - case f of
1.2974 - ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
1.2975 - | Form t => c @ [(from, t)]
1.2976 + let val (f, _, _) = pt_extract (pt, from)
1.2977 + in case f of
1.2978 + ModSpec (_,_,headline, _, _, _) => c @ [(from, headline)]
1.2979 + | Form t => c @ [(from, t)]
1.2980 end
1.2981 else
1.2982 if lev < lev_of from
1.2983 @@ -1925,60 +1435,62 @@
1.2984 handle (PTREE _(*from move_dn too far*)) => c
1.2985 else
1.2986 let
1.2987 - val (f,_,_) = pt_extract (pt, from)
1.2988 + val (f, _, _) = pt_extract (pt, from)
1.2989 val term = case f of
1.2990 ModSpec (_,_,headline,_,_,_) => headline
1.2991 | Form t => t
1.2992 in (get_inter (c @ [(from, term)]) (move_dn [] pt from) to lev pt)
1.2993 handle (PTREE _(*from move_dn too far*)) => c @ [(from, term)]
1.2994 end
1.2995 - in get_inter [] from to level pt end;
1.2996 + in get_inter [] from to level pt end
1.2997
1.2998 -(*for tests*)
1.2999 -fun posform2str (pos:pos', form) =
1.3000 - "("^ pos'2str pos ^", "^
1.3001 - (case form of
1.3002 - Form f => term2str f
1.3003 - | ModSpec c => term2str (#3 c(*the headline*)))
1.3004 - ^")";
1.3005 -fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
1.3006 - (map posform2str)) pfs;
1.3007 -fun posterm2str (pos:pos', t) =
1.3008 - "("^ pos'2str pos ^", "^term2str t^")";
1.3009 -fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
1.3010 - (map posterm2str)) pfs;
1.3011 +(* for tests *)
1.3012 +fun posform2str (pos : pos', form) =
1.3013 + "(" ^ pos'2str pos ^ ", " ^
1.3014 + (case form of Form f => term2str f | ModSpec c => term2str (#3 c(*the headline*))) ^
1.3015 + ")"
1.3016 +fun posforms2str pfs =
1.3017 + (strs2str' o (map (curry op ^ "\n")) o (map posform2str)) pfs
1.3018 +fun posterm2str (pos:pos', t) = "(" ^ pos'2str pos ^ ", " ^ term2str t ^ ")"
1.3019 +fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posterm2str)) pfs
1.3020
1.3021 +(* WN050225 omits the last step, if pt is incomplete *)
1.3022 +fun show_pt pt = tracing (posterms2str (get_interval ([], Frm) ([], Res) 99999 pt))
1.3023
1.3024 -(*WN050225 omits the last step, if pt is incomplete*)
1.3025 -fun show_pt pt =
1.3026 - tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
1.3027 +(* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
1.3028 +fun get_ocalhd (pt, (p, Pbl) : pos') =
1.3029 + let
1.3030 + val (ospec, hdf', spec, probl) = case get_obj I pt p of
1.3031 + PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
1.3032 + | _ => error "get_ocalhd Pbl: uncovered case get_obj"
1.3033 + val {prls, where_, ...} = get_pbt (#2 (some_spec ospec spec))
1.3034 + val pre = check_preconds (assoc_thy"Isac") prls where_ probl
1.3035 + in
1.3036 + (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec) : ocalhd
1.3037 + end
1.3038 + | get_ocalhd (pt, (p, Met)) =
1.3039 + let
1.3040 + val (ospec, hdf', spec, meth) = case get_obj I pt p of
1.3041 + PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
1.3042 + | _ => error "get_ocalhd Met: uncovered case get_obj"
1.3043 + val {prls, pre, ...} = get_met (#3 (some_spec ospec spec))
1.3044 + val pre = check_preconds (assoc_thy"Isac") prls pre meth
1.3045 + in
1.3046 + (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec)
1.3047 + end
1.3048 + | get_ocalhd _ = error "get_ocalhd: uncovered definition"
1.3049
1.3050 -(*.get a calchead from a PblObj-node in the ctree;
1.3051 - preconditions must be calculated.*)
1.3052 -fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
1.3053 - let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
1.3054 - get_obj I pt p
1.3055 - val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
1.3056 - val pre = check_preconds (assoc_thy"Isac") prls where_ probl
1.3057 - in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
1.3058 -| get_ocalhd (pt, pos' as (p,Met):pos') =
1.3059 - let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
1.3060 - spec, meth, ...} =
1.3061 - get_obj I pt p
1.3062 - val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
1.3063 - val pre = check_preconds (assoc_thy"Isac") prls pre meth
1.3064 - in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
1.3065 +(* at the activeFormula set the Model, the Guard and the Specification
1.3066 + to empty and return a CalcHead;
1.3067 + the 'origin' remains (for reconstructing all that) *)
1.3068 +fun reset_calchead (pt, (p,_) : pos') =
1.3069 + let
1.3070 + val () = case get_obj I pt p of
1.3071 + PblObj _ => ()
1.3072 + | _ => error "reset_calchead: uncovered case get_obj"
1.3073 + val pt = update_pbl pt p []
1.3074 + val pt = update_met pt p []
1.3075 + val pt = update_spec pt p e_spec
1.3076 + in (pt, (p, Pbl) : pos') end
1.3077
1.3078 -(*.at the activeFormula set the Model, the Guard and the Specification
1.3079 - to empty and return a CalcHead;
1.3080 - the 'origin' remains (for reconstructing all that).*)
1.3081 -fun reset_calchead (pt, pos' as (p,_):pos') =
1.3082 - let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
1.3083 - val pt = update_pbl pt p []
1.3084 - val pt = update_met pt p []
1.3085 - val pt = update_spec pt p e_spec
1.3086 - in (pt, (p,Pbl):pos') end;
1.3087 -
1.3088 -end
1.3089 -
1.3090 -open CalcHead;
1.3091 +end
1.3092 \ No newline at end of file