1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/ME/calchead.sml Thu Aug 12 11:02:32 2010 +0200
1.3 @@ -0,0 +1,2260 @@
1.4 +(* Specify-phase: specifying and modeling a problem or a subproblem. The
1.5 + most important types are declared in mstools.sml.
1.6 + author: Walther Neuper
1.7 + 991122
1.8 + (c) due to copyright terms
1.9 +
1.10 +use"ME/calchead.sml";
1.11 +use"calchead.sml";
1.12 +*)
1.13 +
1.14 +(* TODO interne Funktionen aus sig entfernen *)
1.15 +signature CALC_HEAD =
1.16 + sig
1.17 + datatype additm = Add of SpecifyTools.itm | Err of string
1.18 + val all_dsc_in : SpecifyTools.itm_ list -> Term.term list
1.19 + val all_modspec : ptree * pos' -> ptree * pos'
1.20 + datatype appl = Appl of tac_ | Notappl of string
1.21 + val appl_add :
1.22 + Theory.theory ->
1.23 + string ->
1.24 + SpecifyTools.ori list ->
1.25 + SpecifyTools.itm list ->
1.26 + (string * (Term.term * Term.term)) list -> cterm' -> additm
1.27 + type calcstate
1.28 + type calcstate'
1.29 + val chk_vars : Thm.cterm SpecifyTools.ppc -> string * Term.term list
1.30 + val chktyp :
1.31 + Theory.theory -> int * Thm.cterm list * Thm.cterm list -> Thm.cterm
1.32 + val chktyps :
1.33 + Theory.theory -> Thm.cterm list * Thm.cterm list -> Thm.cterm list
1.34 + val complete_metitms :
1.35 + SpecifyTools.ori list ->
1.36 + SpecifyTools.itm list ->
1.37 + SpecifyTools.itm list -> pat list -> SpecifyTools.itm list
1.38 + val complete_mod_ : ori list * pat list * pat list * itm list ->
1.39 + itm list * itm list
1.40 + val complete_mod : ptree * pos' -> ptree * (pos * pos_)
1.41 + val complete_spec : ptree * pos' -> ptree * pos'
1.42 + val cpy_nam :
1.43 + pat list -> preori list -> pat -> preori
1.44 + val e_calcstate : calcstate
1.45 + val e_calcstate' : calcstate'
1.46 + val eq1 : ''a -> 'b * (''a * 'c) -> bool
1.47 + val eq3 :
1.48 + ''a -> Term.term -> 'b * 'c * 'd * ''a * SpecifyTools.itm_ -> bool
1.49 + val eq4 : ''a -> 'b * ''a list * 'c * 'd * 'e -> bool
1.50 + val eq5 :
1.51 + 'a * 'b * 'c * 'd * SpecifyTools.itm_ ->
1.52 + 'e * 'f * 'g * Term.term * 'h -> bool
1.53 + val eq_dsc : SpecifyTools.itm * SpecifyTools.itm -> bool
1.54 + val eq_pos' : ''a * pos_ -> ''a * pos_ -> bool
1.55 + val f_mout : Theory.theory -> mout -> Term.term
1.56 + val filter_outs :
1.57 + SpecifyTools.ori list ->
1.58 + SpecifyTools.itm list -> SpecifyTools.ori list
1.59 + val filter_pbt :
1.60 + SpecifyTools.ori list ->
1.61 + ('a * (Term.term * 'b)) list -> SpecifyTools.ori list
1.62 + val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
1.63 + val foldr1 : ('a * 'a -> 'a) -> 'a list -> 'a
1.64 + val form : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
1.65 + val formres : 'a -> ptree -> (string * ('a * pos_) * Term.term) list
1.66 + val gen_ins' : ('a * 'a -> bool) -> 'a * 'a list -> 'a list
1.67 + val get_formress :
1.68 + (string * (pos * pos_) * Term.term) list list ->
1.69 + pos -> ptree list -> (string * (pos * pos_) * Term.term) list
1.70 + val get_forms :
1.71 + (string * (pos * pos_) * Term.term) list list ->
1.72 + posel list -> ptree list -> (string * (pos * pos_) * Term.term) list
1.73 + val get_interval : pos' -> pos' -> int -> ptree -> (pos' * term) list
1.74 + val get_ocalhd : ptree * pos' -> ocalhd
1.75 + val get_spec_form : tac_ -> pos' -> ptree -> mout
1.76 + val geti_ct :
1.77 + Theory.theory ->
1.78 + SpecifyTools.ori -> SpecifyTools.itm -> string * cterm'
1.79 + val getr_ct : Theory.theory -> SpecifyTools.ori -> string * cterm'
1.80 + val has_list_type : Term.term -> bool
1.81 + val header : pos_ -> pblID -> metID -> pblmet
1.82 + val insert_ppc :
1.83 + Theory.theory ->
1.84 + int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
1.85 + SpecifyTools.itm list -> SpecifyTools.itm list
1.86 + val insert_ppc' :
1.87 + SpecifyTools.itm -> SpecifyTools.itm list -> SpecifyTools.itm list
1.88 + val is_complete_mod : ptree * pos' -> bool
1.89 + val is_complete_mod_ : SpecifyTools.itm list -> bool
1.90 + val is_complete_modspec : ptree * pos' -> bool
1.91 + val is_complete_spec : ptree * pos' -> bool
1.92 + val is_copy_named : 'a * ('b * Term.term) -> bool
1.93 + val is_copy_named_idstr : string -> bool
1.94 + val is_error : SpecifyTools.itm_ -> bool
1.95 + val is_field_correct : ''a -> ''b -> (''a * ''b list) list -> bool
1.96 + val is_known :
1.97 + Theory.theory ->
1.98 + string ->
1.99 + SpecifyTools.ori list ->
1.100 + Term.term -> string * SpecifyTools.ori * Term.term list
1.101 + val is_list_type : Term.typ -> bool
1.102 + val is_notyet_input :
1.103 + Theory.theory ->
1.104 + SpecifyTools.itm list ->
1.105 + Term.term list ->
1.106 + SpecifyTools.ori ->
1.107 + ('a * (Term.term * Term.term)) list -> string * SpecifyTools.itm
1.108 + val is_parsed : SpecifyTools.itm_ -> bool
1.109 + val is_untouched : SpecifyTools.itm -> bool
1.110 + val matc :
1.111 + Theory.theory ->
1.112 + pat list ->
1.113 + Term.term list ->
1.114 + (int list * string * Term.term * Term.term list) list ->
1.115 + (int list * string * Term.term * Term.term list) list
1.116 + val match_ags :
1.117 + Theory.theory -> pat list -> Term.term list -> SpecifyTools.ori list
1.118 + val maxl : int list -> int
1.119 + val match_ags_msg : string list -> Term.term -> Term.term list -> unit
1.120 + val memI : ''a list -> ''a -> bool
1.121 + val mk_additem : string -> cterm' -> tac
1.122 + val mk_delete : Theory.theory -> string -> SpecifyTools.itm_ -> tac
1.123 + val mtc :
1.124 + Theory.theory -> pat -> Term.term -> SpecifyTools.preori Library.option
1.125 + val nxt_add :
1.126 + Theory.theory ->
1.127 + SpecifyTools.ori list ->
1.128 + (string * (Term.term * 'a)) list ->
1.129 + SpecifyTools.itm list -> (string * cterm') Library.option
1.130 + val nxt_model_pbl : tac_ -> ptree * (int list * pos_) -> tac_
1.131 + val nxt_spec :
1.132 + pos_ ->
1.133 + bool ->
1.134 + SpecifyTools.ori list ->
1.135 + spec ->
1.136 + SpecifyTools.itm list * SpecifyTools.itm list ->
1.137 + (string * (Term.term * 'a)) list * (string * (Term.term * 'b)) list ->
1.138 + spec -> pos_ * tac
1.139 + val nxt_specif : tac -> ptree * (int list * pos_) -> calcstate'
1.140 + val nxt_specif_additem :
1.141 + string -> cterm' -> ptree * (int list * pos_) -> calcstate'
1.142 + val nxt_specify_init_calc : fmz -> calcstate
1.143 + val ocalhd_complete :
1.144 + SpecifyTools.itm list ->
1.145 + (bool * Term.term) list -> domID * pblID * metID -> bool
1.146 + val ori2Coritm :
1.147 + pat list -> ori -> itm
1.148 + val ori_2itm :
1.149 + 'a ->
1.150 + SpecifyTools.itm_ ->
1.151 + Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm
1.152 + val overwrite_ppc :
1.153 + Theory.theory ->
1.154 + int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
1.155 + SpecifyTools.itm list ->
1.156 + (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list
1.157 + val parse_ok : SpecifyTools.itm_ list -> bool
1.158 + val posform2str : pos' * ptform -> string
1.159 + val posforms2str : (pos' * ptform) list -> string
1.160 + val posterms2str : (pos' * term) list -> string (*tests only*)
1.161 + val ppc135list : 'a SpecifyTools.ppc -> 'a list
1.162 + val ppc2list : 'a SpecifyTools.ppc -> 'a list
1.163 + val pt_extract :
1.164 + ptree * (int list * pos_) ->
1.165 + ptform * tac Library.option * Term.term list
1.166 + val pt_form : ppobj -> ptform
1.167 + val pt_model : ppobj -> pos_ -> ptform
1.168 + val reset_calchead : ptree * pos' -> ptree * pos'
1.169 + val seek_oridts :
1.170 + Theory.theory ->
1.171 + string ->
1.172 + Term.term * Term.term list ->
1.173 + (int * SpecifyTools.vats * string * Term.term * Term.term list) list
1.174 + -> string * SpecifyTools.ori * Term.term list
1.175 + val seek_orits :
1.176 + Theory.theory ->
1.177 + string ->
1.178 + Term.term list ->
1.179 + (int * SpecifyTools.vats * string * Term.term * Term.term list) list
1.180 + -> string * SpecifyTools.ori * Term.term list
1.181 + val seek_ppc :
1.182 + int -> SpecifyTools.itm list -> SpecifyTools.itm Library.option
1.183 + val show_pt : ptree -> unit
1.184 + val some_spec : spec -> spec -> spec
1.185 + val specify :
1.186 + tac_ ->
1.187 + pos' ->
1.188 + cid ->
1.189 + ptree ->
1.190 + (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac *
1.191 + safe * ptree
1.192 + val specify_additem :
1.193 + string ->
1.194 + cterm' * 'a ->
1.195 + int list * pos_ ->
1.196 + 'b ->
1.197 + ptree ->
1.198 + (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
1.199 + val tag_form : Theory.theory -> Thm.cterm * Thm.cterm -> Thm.cterm
1.200 + val test_types : Theory.theory -> Term.term * Term.term list -> string
1.201 + val typeless : Term.term -> Term.term
1.202 + val unbound_ppc : Thm.cterm SpecifyTools.ppc -> Term.term list
1.203 + val vals_of_oris : SpecifyTools.ori list -> Term.term list
1.204 + val variants_in : Term.term list -> int
1.205 + val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list
1.206 + val vars_of_pbl_' : ('a * ('b * Term.term)) list -> Term.term list
1.207 + end
1.208 +
1.209 +
1.210 +
1.211 +
1.212 +
1.213 +(*---------------------------------------------------------------------*)
1.214 +structure CalcHead (**): CALC_HEAD(**) =
1.215 +
1.216 +struct
1.217 +(*---------------------------------------------------------------------*)
1.218 +
1.219 +(* datatypes *)
1.220 +
1.221 +(*.the state wich is stored after each step of calculation; it contains
1.222 + the calc-state and a list of [tac,istate](="tacis") to be applied.
1.223 + the last_elem tacis is the first to apply to the calc-state and
1.224 + the (only) one shown to the front-end as the 'proposed tac'.
1.225 + the calc-state resulting from the application of tacis is not stored,
1.226 + because the tacis hold enought information for efficiently rebuilding
1.227 + this state just by "fun generate ".*)
1.228 +type calcstate =
1.229 + (ptree * pos') * (*the calc-state to which the tacis could be applied*)
1.230 + (taci list); (*ev. several (hidden) steps;
1.231 + in REVERSE order: first tac_ to apply is last_elem*)
1.232 +val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]):calcstate;
1.233 +
1.234 +(*the state used during one calculation within the mathengine; it contains
1.235 + a list of [tac,istate](="tacis") which generated the the calc-state;
1.236 + while this state's tacis are extended by each (internal) step,
1.237 + the calc-state is used for creating new nodes in the calc-tree
1.238 + (eg. applicable_in requires several particular nodes of the calc-tree)
1.239 + and then replaced by the the newly created;
1.240 + on leave of the mathengine the resuing calc-state is dropped anyway,
1.241 + because the tacis hold enought information for efficiently rebuilding
1.242 + this state just by "fun generate ".*)
1.243 +type calcstate' =
1.244 + taci list * (*cas. several (hidden) steps;
1.245 + in REVERSE order: first tac_ to apply is last_elem*)
1.246 + pos' list * (*a "continuous" sequence of pos',
1.247 + deleted by application of taci list*)
1.248 + (ptree * pos'); (*the calc-state resulting from the application of tacis*)
1.249 +val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
1.250 +
1.251 +(*FIXXXME.WN020430 intermediate hack for fun ass_up*)
1.252 +fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f
1.253 + | f_mout thy _ = raise error "f_mout: not called with formula";
1.254 +
1.255 +
1.256 +(*.is the calchead complete ?.*)
1.257 +fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) =
1.258 + foldl and_ (true, map #3 its) andalso
1.259 + foldl and_ (true, map #1 pre) andalso
1.260 + dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID;
1.261 +
1.262 +
1.263 +(* make a term 'typeless' for comparing with another 'typeless' term;
1.264 + 'type-less' usually is illtyped *)
1.265 +fun typeless (Const(s,_)) = (Const(s,e_type))
1.266 + | typeless (Free(s,_)) = (Free(s,e_type))
1.267 + | typeless (Var(n,_)) = (Var(n,e_type))
1.268 + | typeless (Bound i) = (Bound i)
1.269 + | typeless (Abs(s,_,t)) = Abs(s,e_type, typeless t)
1.270 + | typeless (t1 $ t2) = (typeless t1) $ (typeless t2);
1.271 +(*
1.272 +> val (Some ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
1.273 +> val (_,t1) = split_dsc_t hs (term_of ct);
1.274 +> val (Some ct) = parse thy "A=#2*a*b - a^^^#2";
1.275 +> val (_,t2) = split_dsc_t hs (term_of ct);
1.276 +> typeless t1 = typeless t2;
1.277 +val it = true : bool
1.278 +*)
1.279 +
1.280 +
1.281 +
1.282 +(*.to an input (d,ts) find the according ori and insert the ts.*)
1.283 +(*WN.11.03: + dont take first inter<>[]*)
1.284 +fun seek_oridts thy sel (d,ts) [] =
1.285 + ("'"^(string_of_cterm (comp_dts thy (d,ts)))^
1.286 + (*"' not found (typed)", e_ori_:ori, []) ///11.11.03*)
1.287 + "' not found (typed)", (0,[],sel,d,ts):ori, [])
1.288 + (* val (id,vat,sel',d',ts')::oris = ori;
1.289 + val (id,vat,sel',d',ts') = ori;
1.290 + *)
1.291 + | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
1.292 + if sel = sel' andalso d=d' andalso (ts inter ts') <> []
1.293 + then if sel = sel'
1.294 + then ("",(id,vat,sel,d, ts inter(*!overlap!*) ts'):ori, ts')
1.295 + else ((string_of_cterm (comp_dts thy(d,ts)))^
1.296 + " not for "^sel, e_ori_, [])
1.297 + else seek_oridts thy sel (d,ts) oris;
1.298 +
1.299 +(*FIXXXME.WN.11.03: + dont take first inter<>[] .. ev. variants are following:
1.300 + thus take largest intersection !!!
1.301 + if sel NOTok .. then the correct itm should NOT be overwritten by insert_ppc*)
1.302 +(*fun eq7 d (_,_,_,d',_) = d = d';
1.303 +fun inter_length ((_,_,_,_,ts), (_,_,_,_,ts')) = (length ts) < (length ts');
1.304 +fun seek_oridts _ sel (d,ts) [] =
1.305 + ("'"^(string_of_cterm (comp_dts thy (d,ts)))^
1.306 + (*"' not found (typed)", e_ori_:ori, []) ///11.11.03*)
1.307 + "' not found (typed)", (0,[],sel,d,ts):ori, [])
1.308 + (* val (id,vat,sel',d',ts')::oris = ori;
1.309 + val (id,vat,sel',d',ts') = ori;
1.310 + *)
1.311 + | seek_oridts _ sel (d,ts) oris =
1.312 + let val dscOK = filter (eq7 d) oris;
1.313 + in if dscOK = [] then ("'"^(string_of_cterm (comp_dts thy (d,ts)))^
1.314 + "' not found (typed)", (0,[],sel,d,ts):ori, [])
1.315 + else let val (id,vat,sel',d',ts') = gen_max inter_length dscOK;
1.316 + in if sel = sel' then ("",(id,vat,sel,d,ts inter ts'), [])
1.317 + else ("wrong field",(id,vat,sel,d,ts inter ts'), []) end
1.318 + end;
1.319 +--------------------didnt work with Add_Given/_Find/_Relation 11.03*)
1.320 +
1.321 +(*.to an input (_,ts) find the according ori and insert the ts.*)
1.322 +fun seek_orits thy sel ts [] =
1.323 + ("'"^
1.324 + (strs2str (map (Sign.string_of_term (sign_of thy)) ts))^
1.325 + "' not found (typed)", e_ori_, [])
1.326 + | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
1.327 + if sel = sel' andalso (ts inter ts') <> []
1.328 + then if sel = sel'
1.329 + then ("",(id,vat,sel,d,ts inter(*!overlap!*) ts'):ori, ts')
1.330 + else (((strs2str' o map (Sign.string_of_term (sign_of thy))) ts)^
1.331 + " not for "^sel, e_ori_, [])
1.332 + else seek_orits thy sel ts oris;
1.333 +(* false
1.334 +> val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
1.335 +> seek_orits thy sel ts [(id,vat,sel',d,ts')];
1.336 +uncaught exception TYPE
1.337 +> seek_orits thy sel ts [];
1.338 +uncaught exception TYPE
1.339 +*)
1.340 +
1.341 +(*find_first item with #1 equal to id*)
1.342 +fun seek_ppc id [] = None
1.343 + | seek_ppc id (p::(ppc:itm list)) =
1.344 + if id = #1 p then Some p else seek_ppc id ppc;
1.345 +
1.346 +
1.347 +
1.348 +(*---------------------------------------------(3) nach ptyps.sml 23.3.02*)
1.349 +
1.350 +
1.351 +datatype appl = Appl of tac_ | Notappl of string;
1.352 +
1.353 +fun ppc2list ({Given=gis,Where=whs,Find=fis,
1.354 + With=wis,Relate=res}: 'a ppc) =
1.355 + gis @ whs @ fis @ wis @ res;
1.356 +fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =
1.357 + gis @ fis @ res;
1.358 +
1.359 +
1.360 +
1.361 +
1.362 +(* get the number of variants in a problem in 'original',
1.363 + assumes equal descriptions in immediate sequence *)
1.364 +fun variants_in ts =
1.365 + let fun eq(x,y) = head_of x = head_of y;
1.366 + fun cnt eq [] y n = ([n],[])
1.367 + | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)
1.368 + else ([n], x::xs);
1.369 + fun coll eq xs [] = xs
1.370 + | coll eq xs (y::ys) =
1.371 + let val (n,ys') = cnt eq (y::ys) y 0;
1.372 + in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end;
1.373 + val vts = (distinct (coll eq [] ts))\\[1];
1.374 + in case vts of [] => 1 | [n] => n
1.375 + | _ => error "different variants in formalization" end;
1.376 +(*
1.377 +> cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
1.378 +val it = ([3],[4,5,5,5,5,5]) : int list * int list
1.379 +> coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
1.380 +val it = [1,3,1,5] : int list
1.381 +*)
1.382 +
1.383 +fun is_list_type (Type("List.list",_)) = true
1.384 + | is_list_type _ = false;
1.385 +(* fun destr (Type(str,sort)) = (str,sort);
1.386 +> val (Some ct) = parse thy "lll::real list";
1.387 +> val ty = (#T o rep_cterm) ct;
1.388 +> is_list_type ty;
1.389 +val it = true : bool
1.390 +> destr ty;
1.391 +val it = ("List.list",["RealDef.real"]) : string * typ list
1.392 +> atomty ((#t o rep_cterm) ct);
1.393 +*** -------------
1.394 +*** Free ( lll, real list)
1.395 +val it = () : unit
1.396 +
1.397 +> val (Some ct) = parse thy "[lll::real]";
1.398 +> val ty = (#T o rep_cterm) ct;
1.399 +> is_list_type ty;
1.400 +val it = true : bool
1.401 +> destr ty;
1.402 +val it = ("List.list",["'a"]) : string * typ list
1.403 +> atomty ((#t o rep_cterm) ct);
1.404 +*** -------------
1.405 +*** Const ( List.list.Cons, [real, real list] => real list)
1.406 +*** Free ( lll, real)
1.407 +*** Const ( List.list.Nil, real list)
1.408 +
1.409 +> val (Some ct) = parse thy "lll";
1.410 +> val ty = (#T o rep_cterm) ct;
1.411 +> is_list_type ty;
1.412 +val it = false : bool *)
1.413 +
1.414 +
1.415 +fun has_list_type (Free(_,T)) = is_list_type T
1.416 + | has_list_type _ = false;
1.417 +(*
1.418 +> val (Some ct) = parse thy "lll::real list";
1.419 +> has_list_type (term_of ct);
1.420 +val it = true : bool
1.421 +> val (Some ct) = parse thy "[lll::real]";
1.422 +> has_list_type (term_of ct);
1.423 +val it = false : bool *)
1.424 +
1.425 +
1.426 +
1.427 +
1.428 +(*fdcrs = descriptions in formalization
1.429 + unused 22.11.00
1.430 +fun is_already_input thy fdcrs ts t =
1.431 + let
1.432 + val tss = flat (map isalist2list ts);
1.433 +(*28.1. val (dcr,t') = split_dsc_t fdcrs t; *)
1.434 + val (dcr,[t']) = split_dts t;
1.435 + in if (typeless t') mem (map typeless tss)
1.436 + then ("term '"^(Sign.string_of_term (sign_of thy) t')^
1.437 + "' already input")
1.438 + else "" end;
1.439 +
1.440 +> val pts = appc (map (term_of o the o (parse thy))) pbl;
1.441 +> val ts = #Relate pts;
1.442 +> val t = (term_of o the o (parse thy))"(A=#2*a*b - a^^^#2)";
1.443 +> is_already_input thy ts t;
1.444 +val it = "term 'A = #2 * a * b - a ^^^ #2' already input" : string
1.445 +> val t = (term_of o the o (parse thy))"a=#2*R*sin alpha";
1.446 +> is_already_input thy ts t;
1.447 +val it = "term 'a = #2 * R * sin alpha' already input" : string
1.448 +> val t = (term_of o the o (parse thy))"a=R*sin alpha";
1.449 +> is_already_input thy ts t;
1.450 +val it = "" : string
1.451 +*)
1.452 +
1.453 +
1.454 +fun is_parsed (Syn _) = false
1.455 + | is_parsed _ = true;
1.456 +fun parse_ok its = foldl and_ (true, map is_parsed its);
1.457 +
1.458 +fun all_dsc_in itm_s =
1.459 + let
1.460 + fun d_in (Cor ((d,_),_)) = [d]
1.461 + | d_in (Syn c) = []
1.462 + | d_in (Typ c) = []
1.463 + | d_in (Inc ((d,_),_)) = [d]
1.464 + | d_in (Sup (d,_)) = [d]
1.465 + | d_in (Mis (d,_)) = [d];
1.466 + in (flat o (map d_in)) itm_s end;
1.467 +
1.468 +(* 30.1.00 ---
1.469 +fun is_Syn (Syn _) = true
1.470 + | is_Syn (Typ _) = true
1.471 + | is_Syn _ = false;
1.472 + --- *)
1.473 +fun is_error (Cor (_,ts)) = false
1.474 + | is_error (Sup (_,ts)) = false
1.475 + | is_error (Inc (_,ts)) = false
1.476 + | is_error (Mis (_,ts)) = false
1.477 + | is_error _ = true;
1.478 +
1.479 +(* 30.1.00 ---
1.480 +fun ct_in (Syn (c)) = c
1.481 + | ct_in (Typ (c)) = c
1.482 + | ct_in _ = raise error "ct_in called for Cor .. Sup";
1.483 + --- *)
1.484 +
1.485 +(*#############################################################*)
1.486 +(*#############################################################*)
1.487 +(* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)
1.488 +
1.489 +
1.490 +(* testdaten besorgen:
1.491 + use"test-coil-kernel.sml";
1.492 + val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) =
1.493 + get_obj I pt p;
1.494 + *)
1.495 +
1.496 +(* given oris, ppc,
1.497 + variant V: oris union ppc => int, id ID: oris union ppc => int
1.498 +
1.499 + ppc is_complete ==
1.500 + EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i
1.501 +
1.502 + and
1.503 + @vt = max sum(i : ppc) V i
1.504 +*)
1.505 +
1.506 +
1.507 +
1.508 +(*
1.509 +> ((vts_cnt (vts_in itms))) itms;
1.510 +
1.511 +
1.512 +
1.513 +---^^--test 10.3.
1.514 +> val vts = vts_in itms;
1.515 +val vts = [1,2,3] : int list
1.516 +> val nvts = vts_cnt vts itms;
1.517 +val nvts = [(1,6),(2,5),(3,7)] : (int * int) list
1.518 +> val mx = max2 nvts;
1.519 +val mx = (3,7) : int * int
1.520 +> val v = max_vt itms;
1.521 +val v = 3 : int
1.522 +--------------------------
1.523 +>
1.524 +*)
1.525 +
1.526 +(*.get the first term in ts from ori.*)
1.527 +(* val (_,_,fd,d,ts) = hd miss;
1.528 + *)
1.529 +fun getr_ct thy ((_,_,fd,d,ts):ori) =
1.530 + (fd, (string_of_cterm o (comp_dts thy)) (d,[hd ts]):cterm');
1.531 +(* val t = comp_dts thy (d,[hd ts]);
1.532 + *)
1.533 +
1.534 +(* get a term from ori, notyet input in itm *)
1.535 +fun geti_ct thy ((_,_,_,d,ts):ori) ((_,_,_,fd,itm_):itm) =
1.536 + (fd, (string_of_cterm o (comp_dts thy)) (d,ts \\ (ts_in itm_)):cterm');
1.537 +(* test-maximum.sml fmy <> [], Init_Proof ...
1.538 + val (_,_,_,d,ts) = ori; val (_,_,_,fd,itm_) = hd icl;
1.539 + val d' $ ts' = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
1.540 + atomty d;
1.541 + atomty d';
1.542 + atomty (hd ts);
1.543 + atomty ts';
1.544 + cterm_of (sign_of thy) (d $ (hd ts));
1.545 + cterm_of (sign_of thy) (d' $ ts');
1.546 +
1.547 + comp_dts thy (d,ts);
1.548 + *)
1.549 +
1.550 +
1.551 +(* in FE dsc, not dat: this is in itms ...*)
1.552 +fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true
1.553 + | is_untouched _ = false;
1.554 +
1.555 +
1.556 +(* select an item in oris, notyet input in itms
1.557 + (precondition: in itms are only Cor, Sup, Inc) *)
1.558 +fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
1.559 + let
1.560 + fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0;
1.561 + fun is_elem itms (f,(d,t)) =
1.562 + case find_first (test_d d) itms of
1.563 + Some _ => true | None => false;
1.564 + in case filter_out (is_elem itms) pbt of
1.565 +(* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
1.566 + *)
1.567 + (f,(d,_))::itms =>
1.568 + Some (f:string, (string_of_cterm o comp_dts thy) (d,[]):cterm')
1.569 + | _ => None end
1.570 +
1.571 +(* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
1.572 + *)
1.573 + | nxt_add thy oris pbt itms =
1.574 + let
1.575 + fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
1.576 + andalso (#3 ori) <>"#undef";
1.577 + fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
1.578 + fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
1.579 +(* val itm = hd icl; val (_,_,_,d,ts) = v6;
1.580 + *)
1.581 + fun test_subset (itm:itm) ((_,_,_,d,ts):ori) =
1.582 + (d_in (#5 itm)) = d andalso (ts_in (#5 itm)) subset ts;
1.583 + fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
1.584 + | false_and_not_Sup (i,v,false,f, _) = true
1.585 + | false_and_not_Sup _ = false;
1.586 +
1.587 + val v = if itms = [] then 1 else max_vt itms;
1.588 + val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
1.589 + val vits = if v = 0 then itms (*because of dsc without dat*)
1.590 + else filter (testi_vt v) itms; (*itms..vat*)
1.591 + val icl = filter false_and_not_Sup vits; (* incomplete *)
1.592 + in if icl = []
1.593 + then case filter_out (test_id (map #1 vits)) vors of
1.594 + [] => None
1.595 + (* val miss = filter_out (test_id (map #1 vits)) vors;
1.596 + *)
1.597 + | miss => Some (getr_ct thy (hd miss))
1.598 + else
1.599 + case find_first (test_subset (hd icl)) vors of
1.600 + (* val Some ori = find_first (test_subset (hd icl)) vors;
1.601 + *)
1.602 + None => raise error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
1.603 + | Some ori => Some (geti_ct thy ori (hd icl))
1.604 + end;
1.605 +
1.606 +
1.607 +
1.608 +fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_)
1.609 + | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_)
1.610 + | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)
1.611 + | mk_delete thy str _ =
1.612 + raise error ("mk_delete: called with field '"^str^"'");
1.613 +fun mk_additem "#Given" ct = Add_Given ct
1.614 + | mk_additem "#Find" ct = Add_Find ct
1.615 + | mk_additem "#Relate"ct = Add_Relation ct
1.616 + | mk_additem str _ =
1.617 + raise error ("mk_additem: called with field '"^str^"'");
1.618 +
1.619 +
1.620 +
1.621 +
1.622 +
1.623 +(* find the next tac in specify (except nxt_model_pbl)
1.624 + 4.00.: TODO: do not return a pos !!!
1.625 + (sind from DG comes the _OLD_ writepos)*)
1.626 +(*
1.627 +> val (pbl,pbt,mpc) =(pbl',get_pbt cpI,(#ppc o get_met) cmI);
1.628 +> val (dI,pI,mI) = empty_spec;
1.629 +> nxt_spec Pbl (oris:ori list) ((dI',pI',mI'):spec(*original*))
1.630 + ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec);
1.631 +
1.632 +at Init_Proof:
1.633 +> val met = [];val (pbt,mpc) = (get_pbt pI',(#ppc o get_met) mI');
1.634 +> val (dI,pI,mI) = empty_spec;
1.635 +> nxt_spec Pbl (oris:ori list) ((dI',pI',mI'):spec(*original*))
1.636 + ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec);
1.637 + *)
1.638 +
1.639 +(*. determine the next step of specification;
1.640 + not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
1.641 +eg. in rootpbl 'no_met':
1.642 +args:
1.643 + preok predicates are _all_ ok, or problem matches completely
1.644 + oris immediately from formalization
1.645 + (dI',pI',mI') specification coming from author/parent-problem
1.646 + (pbl, item lists specified by user
1.647 + met) -"-, tacitly completed by copy_probl
1.648 + (dI,pI,mI) specification explicitly done by the user
1.649 + (pbt, mpc) problem type, guard of method
1.650 +.*)
1.651 +(* val (preok,pbl,pbt,mpc)=(pb,pbl',(#ppc o get_pbt) cpI,(#ppc o get_met) cmI);
1.652 + val (preok,pbl,pbt,mpc)=(pb,pbl',ppc,(#ppc o get_met) cmI);
1.653 + val (Pbl, preok, oris, (dI',pI',mI'), (pbl,met), (pbt,mpc), (dI,pI,mI)) =
1.654 + (p_, pb, oris, (dI',pI',mI'), (probl,meth),
1.655 + (ppc, (#ppc o get_met) cmI), (dI,pI,mI));
1.656 + *)
1.657 +fun nxt_spec Pbl preok (oris:ori list) ((dI',pI',mI'):spec)
1.658 + ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec) =
1.659 + ((*writeln"### nxt_spec Pbl";*)
1.660 + if dI'=e_domID andalso dI=e_domID then (Pbl, Specify_Theory dI')
1.661 + else if pI'=e_pblID andalso pI=e_pblID then (Pbl, Specify_Problem pI')
1.662 + else case find_first (is_error o #5) (pbl:itm list) of
1.663 + Some (_,_,_,fd,itm_) =>
1.664 + (Pbl, mk_delete
1.665 + (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
1.666 + | None =>
1.667 + ((*writeln"### nxt_spec is_error None";*)
1.668 + case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))
1.669 + oris pbt pbl of
1.670 +(* val Some (fd,ct') = nxt_add (assoc_thy (if dI=e_domID then dI' else dI))
1.671 + oris pbt pbl;
1.672 + *)
1.673 + Some (fd,ct') => ((*writeln"### nxt_spec nxt_add Some";*)
1.674 + (Pbl, mk_additem fd ct'))
1.675 + | None => (*pbl-items complete*)
1.676 + if not preok then (Pbl, Refine_Problem pI')
1.677 + else
1.678 + if dI = e_domID then (Pbl, Specify_Theory dI')
1.679 + else if pI = e_pblID then (Pbl, Specify_Problem pI')
1.680 + else if mI = e_metID then (Pbl, Specify_Method mI')
1.681 + else
1.682 + case find_first (is_error o #5) met of
1.683 + Some (_,_,_,fd,itm_) =>
1.684 + (Met, mk_delete (assoc_thy dI) fd itm_)
1.685 + | None =>
1.686 + (case nxt_add (assoc_thy dI) oris mpc met of
1.687 + Some (fd,ct') => (*30.8.01: pre?!?*)
1.688 + (Met, mk_additem fd ct')
1.689 + | None =>
1.690 + ((*Solv 3.4.00*)Met, Apply_Method mI))))
1.691 +(* val preok=pb; val (pbl, met) = (pbl,met');
1.692 + val (pbt,mpc)=((#ppc o get_pbt) cpI,(#ppc o get_met) cmI);
1.693 + val (Met, preok, oris, (dI',pI',mI'), (pbl,met), (pbt,mpc), (dI,pI,mI)) =
1.694 + (p_, pb, oris, (dI',pI',mI'), (probl,meth),
1.695 + (ppc, (#ppc o get_met) cmI), (dI,pI,mI));
1.696 + *)
1.697 + | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) =
1.698 + ((*writeln"### nxt_spec Met"; *)
1.699 + case find_first (is_error o #5) met of
1.700 + Some (_,_,_,fd,itm_) =>
1.701 + (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)
1.702 + | None =>
1.703 + case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of
1.704 + Some (fd,ct') => (Met, mk_additem fd ct')
1.705 + | None =>
1.706 + ((*writeln"### nxt_spec Met: nxt_add None";*)
1.707 + if dI = e_domID then (Met, Specify_Theory dI')
1.708 + else if pI = e_pblID then (Met, Specify_Problem pI')
1.709 + else if not preok then (Met, Specify_Method mI)
1.710 + else (Met, Apply_Method mI)));
1.711 +
1.712 +(* di_ pI_ mI_ pos_
1.713 +val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,
1.714 + (2,[2],true,"#Find",Syn("empty"))];
1.715 +*)
1.716 +
1.717 +
1.718 +(* ^^^--- aus nnewcode.sml am 30.1.00 ---^^^ *)
1.719 +(*#############################################################*)
1.720 +(*#############################################################*)
1.721 +(* vvv--- aus nnewcode.sml vor 29.1.00 ---vvv *)
1.722 +
1.723 +(*3.3.--
1.724 +fun update_itm (cl,d,ts) ((id,vt,_,sl,Cor (_,_)):itm) =
1.725 + (id,vt,cl,sl,Cor (d,ts)):itm
1.726 + | update_itm (cl,d,ts) (id,vt,_,sl,Syn (_)) =
1.727 + raise error ("update_itm "^(string_of_cterm (comp_dts thy (d,ts)))^
1.728 + " not not for Syn (s:cterm')")
1.729 + | update_itm (cl,d,ts) (id,vt,_,sl,Typ (_)) =
1.730 + raise error ("update_itm "^(string_of_cterm (comp_dts thy (d,ts)))^
1.731 + " not not for Typ (s:cterm')")
1.732 + | update_itm (cl,d,ts) (id,vt,_,sl,Fal (_,_)) =
1.733 + (id,vt,cl,sl,Fal (d,ts))
1.734 + | update_itm (cl,d,ts) (id,vt,_,sl,Inc (_,_)) =
1.735 + (id,vt,cl,sl,Inc (d,ts))
1.736 + | update_itm (cl,d,ts) (id,vt,_,sl,Sup (_,_)) =
1.737 + (id,vt,cl,sl,Sup (d,ts));
1.738 +*)
1.739 +
1.740 +
1.741 +
1.742 +
1.743 +fun is_field_correct sel d dscpbt =
1.744 + case assoc (dscpbt, sel) of
1.745 + None => false
1.746 + | Some ds => d mem ds;
1.747 +
1.748 +(*. update the itm_ already input, all..from ori .*)
1.749 +(* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
1.750 + *)
1.751 +fun ori_2itm thy itm_ pid all ((id,vt,fd,d,ts):ori) =
1.752 + let
1.753 + val ts' = (ts_in itm_) union ts;
1.754 + val pval = pbl_ids' thy d ts'
1.755 + (*WN.9.5.03: FIXXXME [#0, epsilon]
1.756 + here would upd_penv be called for [#0, epsilon] etc. *)
1.757 + val complete = if eq_set (ts', all) then true else false;
1.758 + in case itm_ of
1.759 + (Cor _) =>
1.760 + (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts'))
1.761 + else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm
1.762 + | (Syn c) => raise error ("ori_2itm wants to overwrite "^c)
1.763 + | (Typ c) => raise error ("ori_2itm wants to overwrite "^c)
1.764 + | (Inc _) => if complete
1.765 + then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
1.766 + else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
1.767 + | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)
1.768 + (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
1.769 + (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
1.770 +(* 28.1.00: not completely clear ---^^^ etc.*)
1.771 +(* 4.9.01: Mis just copied---vvv *)
1.772 + | (Mis _) => if complete
1.773 + then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))
1.774 + else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))
1.775 + end;
1.776 +
1.777 +
1.778 +fun eq1 d (_,(d',_)) = (d = d');
1.779 +fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
1.780 +
1.781 +
1.782 +(* 'all' ts from ori; ts is the input; (ori carries rest of info)
1.783 + 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?
1.784 + pval: value for problem-environment _NOT_ checked for 'inter' --
1.785 + -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc
1.786 + (as it has been done for input_icalhd+insert_ppc' in 11.03)*)
1.787 +(*. is_input ori itms <=>
1.788 + EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)
1.789 + (2) ori(ts) subset itm(ts) --- Err "already input"
1.790 + (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)
1.791 + (4) -"- <> empty --- new: ori(ts) \\ inter .*)
1.792 +(* val(itms,(i,v,f,d,ts)) = (ppc,ori');
1.793 + *)
1.794 +fun is_notyet_input thy (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
1.795 + case find_first (eq1 d) pbt of
1.796 + Some (_,(_,pid)) =>(* val Some (_,(_,pid)) = find_first (eq1 d) pbt;
1.797 + val Some (_,_,_,_,itm_)=find_first (eq3 f d) itms;
1.798 + *)
1.799 + (case find_first (eq3 f d) itms of
1.800 + Some (_,_,_,_,itm_) =>
1.801 + let
1.802 + val ts' = (ts_in itm_) inter ts;
1.803 + in if ts subset ts'
1.804 + then (((strs2str' o
1.805 + map (Sign.string_of_term (sign_of thy))) ts')^
1.806 + " already input", e_itm) (*2*)
1.807 + else ("", ori_2itm thy itm_ pid all (i,v,f,d,ts\\ts')) (*3,4*)
1.808 + end
1.809 + | None => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[])))
1.810 + pid all (i,v,f,d,ts)) (*1*)
1.811 + )
1.812 + | None => ("", ori_2itm thy (Sup (d,ts))
1.813 + e_term all (i,v,f,d,ts));
1.814 +(*------------------------------------------------
1.815 +fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_);
1.816 +fun is_notyet_input thy itms pval all ((id,vt,fd,d,ts):ori) pbt =
1.817 + case find_first (eq1 d) pbt of
1.818 + Some (_,(_,pid)) => (* val Some (_,(_,pid)) = find_first (eq1 d) pbt;
1.819 + *)
1.820 + (case seek_ppc id itms of
1.821 + Some (id',_,_,_,itm_) =>
1.822 + let
1.823 + val ts' = (ts_in itm_) inter ts;
1.824 + in if ts'= [] then ("", ori_2itm itm_ (pid, pval) all
1.825 + (id,vt,fd,d,(ts_in itm_)@ts))
1.826 + else (((strs2str' o
1.827 + map (Sign.string_of_term (sign_of thy))) ts')^
1.828 + " already input", e_itm) end
1.829 + | None =>
1.830 + if all = ts
1.831 + then ("", ori_2itm (Cor ((e_term,[]),(pid,[])))
1.832 + (pid, pval) all (id,vt,fd,d,ts))
1.833 + else ("", ori_2itm (Inc ((e_term,[]),(e_term,[])))
1.834 + (pid, pval) all (id,vt,fd,d,ts))
1.835 + )
1.836 + | None => ("", ori_2itm (Sup (e_term,[]))
1.837 + (e_term, []) all (id,vt,fd,d,ts));----*)
1.838 +
1.839 +fun test_types thy (d,ts) =
1.840 + let
1.841 + val s = !show_types; val _ = show_types:= true;
1.842 + val opt = (try (comp_dts thy)) (d,ts);
1.843 + val msg = case opt of
1.844 + Some _ => ""
1.845 + | None => ((Sign.string_of_term (sign_of thy) d)^" "^
1.846 + ((strs2str' o map (Sign.string_of_term(sign_of thy)))ts)
1.847 + ^" is illtyped");
1.848 + val _ = show_types:= s
1.849 + in msg end;
1.850 +
1.851 +
1.852 +
1.853 +fun maxl [] = raise error "maxl of []"
1.854 + | maxl (y::ys) =
1.855 + let fun mx x [] = x
1.856 + | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys
1.857 + in mx y ys end;
1.858 +
1.859 +
1.860 +(*. is the input term t known in oris ?
1.861 + give feedback on all(?) strange input;
1.862 + return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
1.863 +(*WN.11.03: from lists*)
1.864 +fun is_known thy sel ori t =
1.865 +(* val (ori,t)=(oris,term_of ct);
1.866 + *)
1.867 + let
1.868 + val ots = (distinct o flat o (map #5)) (ori:ori list);
1.869 + val oids = ((map (fst o dest_Free)) o distinct o
1.870 + flat o (map vars)) ots;
1.871 + val (d,ts(*,pval*)) = split_dts thy t;
1.872 + val ids = map (fst o dest_Free)
1.873 + ((distinct o (flat o (map vars))) ts);
1.874 + in if (ids \\ oids) <> []
1.875 + then (("identifiers "^(strs2str' (ids \\ oids))^
1.876 + " not in example"), e_ori_, [])
1.877 + else
1.878 + if d = e_term
1.879 + then
1.880 + if not ((map typeless ts) subset (map typeless ots))
1.881 + then (("terms '"^
1.882 + ((strs2str' o (map (Sign.string_of_term
1.883 + (sign_of thy)))) ts)^
1.884 + "' not in example (typeless)"), e_ori_, [])
1.885 + else (case seek_orits thy sel ts ori of
1.886 + ("", ori_ as (_,_,_,d,ts), all) =>
1.887 + (case test_types thy (d,ts) of
1.888 + "" => ("", ori_, all)
1.889 + | msg => (msg, e_ori_, []))
1.890 + | (msg,_,_) => (msg, e_ori_, []))
1.891 + else
1.892 + if d mem (map #4 ori)
1.893 + then seek_oridts thy sel (d,ts) ori
1.894 + else ((Sign.string_of_term (sign_of thy) d)^
1.895 + (*" not in example", e_ori_, []) ///11.11.03*)
1.896 + " not in example", (0,[],sel,d,ts), [])
1.897 + end;
1.898 +
1.899 +
1.900 +(*. for return-value of appl_add .*)
1.901 +datatype additm =
1.902 + Add of itm
1.903 + | Err of string; (*error-message*)
1.904 +
1.905 +
1.906 +(*. add an item; check wrt. oris and pbt .*)
1.907 +
1.908 +(* in contrary to oris<>[] below, this part handles user-input
1.909 + extremely acceptive, i.e. accept input instead error-msg *)
1.910 +fun appl_add thy sel ([]:ori list) ppc pbt ct' =
1.911 +(* val (ppc,pbt,ct',env) = (pbl, (#ppc o get_pbt) cpI, ct, []:envv);
1.912 + !!!! 28.8.01: env tested _minimally_ !!!
1.913 + *)
1.914 + let
1.915 + val i = 1 + (if ppc=[] then 0 else maxl (map #1 ppc));
1.916 + in case parse thy ct' of (*should be done in applicable_in 4.00.FIXME*)
1.917 + None => Add (i,[],false,sel,Syn ct')
1.918 +(* val (Some ct) = parse thy ct';
1.919 + *)
1.920 + | Some ct =>
1.921 + let
1.922 + val (d,ts(*,pval*)) = split_dts thy (term_of ct);
1.923 + in if d = e_term
1.924 + then Add (i,[],false,sel,Mis (dsc_unknown,hd ts(*24.3.02*)))
1.925 +
1.926 + else
1.927 + (case find_first (eq1 d) pbt of
1.928 + None => Add (i,[],true,sel,Sup ((d,ts)))
1.929 + | Some (f,(_,id)) =>
1.930 +(* val Some (f,(_,id)) = find_first (eq1 d) pbt;
1.931 + *)
1.932 + let
1.933 + fun eq2 d ((i,_,_,_,itm_):itm) =
1.934 + (d = (d_in itm_)) andalso i<>0;
1.935 + in case find_first (eq2 d) ppc of
1.936 + None => Add (i,[],true,f, Cor ((d,ts), (id, (*pval*)
1.937 + pbl_ids' thy d ts)))
1.938 + | Some (i',_,_,_,itm_) =>
1.939 +(* val Some (i',_,_,_,itm_) = find_first (eq2 d) ppc;
1.940 + val None = find_first (eq2 d) ppc;
1.941 + *)
1.942 + if is_list_dsc d
1.943 + then let val ts = ts union (ts_in itm_)
1.944 + in Add (if ts_in itm_ = [] then i else i',
1.945 + [],true,f,Cor ((d, ts), (id, (*pval*)
1.946 + pbl_ids' thy d ts)))
1.947 + end
1.948 + else Add (i',[],true,f,Cor ((d,ts),(id, (*pval*)
1.949 + pbl_ids' thy d ts)))
1.950 + end
1.951 + )
1.952 + end
1.953 + end
1.954 +(*. add ct to ppc .*)
1.955 +(*FIXXME: accept items as Sup, Syn here, too (like appl_add..oris=[] above)*)
1.956 +(* val (ppc,pbt) = (pbl, ppc);
1.957 + val (ppc,pbt) = (met, (#ppc o get_met) cmI);
1.958 +
1.959 + val (ppc,pbt) = (pbl, (#ppc o get_pbt) cpI);
1.960 + *)
1.961 + | appl_add thy sel oris ppc pbt(*only for upd_envv*) ct =
1.962 + let
1.963 + val ctopt = parse thy ct;
1.964 + in case ctopt of
1.965 + None => Err ("syntax error in "^ct)
1.966 + | Some ct =>(* val Some ct = ctopt;
1.967 + val (msg,ori',all) = is_known thy sel oris (term_of ct);
1.968 + val (msg,itm) = is_notyet_input thy ppc all ori' pbt;
1.969 + *)
1.970 + (case is_known thy sel oris (term_of ct) of
1.971 + ("",ori'(*ts='ct'*), all) =>
1.972 + (case is_notyet_input thy ppc all ori' pbt of
1.973 + ("",itm) => Add itm
1.974 + | (msg,_) => Err msg)
1.975 + | (msg,_,_) => Err msg)
1.976 + end;
1.977 +(*
1.978 +> val (msg,itm) = is_notyet_input thy ppc all ori';
1.979 +val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
1.980 +> val itm_ = #5 itm;
1.981 +> val ts = ts_in itm_;
1.982 +> map (atomty) ts;
1.983 +*)
1.984 +
1.985 +(*---------------------------------------------(4) nach ptyps.sml 23.3.02*)
1.986 +
1.987 +
1.988 +(** make oris from args of the stac SubProblem and from pbt **)
1.989 +
1.990 +(*.can this formal argument (of a model-pattern) be omitted in the arg-list
1.991 + of a SubProblem ? see ME/ptyps.sml 'type met '.*)
1.992 +fun is_copy_named_idstr str =
1.993 + case (rev o explode) str of
1.994 + "_"::_::"_"::_ => true
1.995 + | _ => false;
1.996 +(*> is_copy_named_idstr "v_i_";
1.997 +val it = true : bool
1.998 + > is_copy_named_idstr "e_";
1.999 +val it = false : bool
1.1000 + > is_copy_named_idstr "L___";
1.1001 +val it = true : bool
1.1002 +*)
1.1003 +(*.should this formal argument (of a model-pattern) create a new identifier?.*)
1.1004 +fun is_copy_named_generating_idstr str =
1.1005 + if is_copy_named_idstr str
1.1006 + then case (rev o explode) str of
1.1007 + "_"::"_"::"_"::_ => false
1.1008 + | _ => true
1.1009 + else false;
1.1010 +(*> is_copy_named_generating_idstr "v_i_";
1.1011 +val it = true : bool
1.1012 + > is_copy_named_generating_idstr "L___";
1.1013 +val it = false : bool
1.1014 +*)
1.1015 +
1.1016 +(*.can this formal argument (of a model-pattern) be omitted in the arg-list
1.1017 + of a SubProblem ? see ME/ptyps.sml 'type met '.*)
1.1018 +fun is_copy_named (_,(_,t)) = (is_copy_named_idstr o free2str) t;
1.1019 +(*.should this formal argument (of a model-pattern) create a new identifier?.*)
1.1020 +fun is_copy_named_generating (_,(_,t)) =
1.1021 + (is_copy_named_generating_idstr o free2str) t;
1.1022 +
1.1023 +
1.1024 +(*.split type-wrapper from scr-arg and build part of an ori;
1.1025 + an type-error is reported immediately, raises an exn,
1.1026 + subsequent handling of exn provides 2nd part of error message.*)
1.1027 +fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
1.1028 + (* val (thy, (str, (dsc, _)), (ty $ var)) =
1.1029 + (thy, p, a);
1.1030 + *)
1.1031 + (cterm_of (sign_of thy) (dsc $ var);(*type check*)
1.1032 + Some ((([1], str, dsc, (*[var]*)
1.1033 + split_dts' (dsc, var))): preori)(*:ori without leading #*))
1.1034 + handle e as TYPE _ =>
1.1035 + (writeln (dashs 70^"\n"
1.1036 + ^"*** ERROR while creating the items for the model of the ->problem\n"
1.1037 + ^"*** from the ->stac with ->typeconstructor in arglist:\n"
1.1038 + ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
1.1039 + ^"*** description: "^(term_detail2str dsc)
1.1040 + ^"*** value: "^(term_detail2str var)
1.1041 + ^"*** typeconstructor in script: "^(term_detail2str ty)
1.1042 + ^"*** checked by theory: "^(theory2str thy)^"\n"
1.1043 + ^"*** "^dots 66);
1.1044 + print_exn e; (*raises exn again*)
1.1045 + None);
1.1046 +(*> val pbt = (#ppc o get_pbt) ["univariate","equation"];
1.1047 +> val Const ("Script.SubProblem",_) $
1.1048 + (Const ("Pair",_) $ Free (thy', _) $
1.1049 + (Const ("Pair",_) $ pblID' $ metID')) $ ags =
1.1050 + str2term"(SubProblem (SqRoot_,[univariate,equation],\
1.1051 + \[SqRoot_,solve_linear]) [bool_ (x+1- 2=0), real_ x])::bool list";
1.1052 +> val ags = isalist2list ags;
1.1053 +> mtc thy (hd pbt) (hd ags);
1.1054 +val it = Some ([1],"#Given",Const (#,#),[# $ #]) *)
1.1055 +
1.1056 +(*.match each pat of the model-pattern with an actual argument;
1.1057 + precondition: copy-named vars are filtered out.*)
1.1058 +fun matc thy ([]:pat list) _ (oris:preori list) = oris
1.1059 + | matc thy pbt [] _ =
1.1060 + (writeln (dashs 70);
1.1061 + raise error ("actual arg(s) missing for '"^pats2str pbt
1.1062 + ^"' i.e. should be 'copy-named' by '*_._'"))
1.1063 + | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =
1.1064 + (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
1.1065 + (thy, pbt', ags, []);
1.1066 + (*recursion..*)
1.1067 + val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =
1.1068 + (thy, pbt, ags, (oris @ [ori]));
1.1069 + *)
1.1070 + (*del?..*)if (is_copy_named_idstr o free2str) t then oris
1.1071 + else(*..del?*) let val opt = mtc thy p a;
1.1072 + in case opt of
1.1073 + (* val Some ori = mtc thy p a;
1.1074 + *)
1.1075 + Some ori => matc thy pbt ags (oris @ [ori])
1.1076 + | None => [](*WN050903 skipped by exn handled in match_ags*)
1.1077 + end;
1.1078 +(* run subp-rooteq.sml until Init_Proof before ...
1.1079 +> val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)
1.1080 +> fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;
1.1081 +
1.1082 + other vars as in mtc ..
1.1083 +> matc thy (drop_last pbt) ags [];
1.1084 +val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
1.1085 +
1.1086 +
1.1087 +(*WN051014 outcommented with redesign copy-named (for omitting '#Find'
1.1088 + in SubProblem);
1.1089 + kept as initial idea for generating x_1, x_2, ... for equations*)
1.1090 +fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
1.1091 +(* val ((pbt:pat list), (oris:preori list), ((field,(dsc,t)):pat)) =
1.1092 + (pbt', oris', hd (*!!!!!*) cy);
1.1093 + *)
1.1094 + (if is_copy_named_generating p
1.1095 + then (*WN051014 kept strange old code ...*)
1.1096 + let fun sel (_,_,d,ts) = comp_ts (d, ts)
1.1097 + val cy' = (implode o drop_last o drop_last o explode o free2str) t
1.1098 + val ext = (last_elem o drop_last o explode o free2str) t
1.1099 + val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*)
1.1100 + val vals = map sel oris
1.1101 + val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
1.1102 + in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
1.1103 + else ([1], field, dsc, [t])
1.1104 + )
1.1105 + handle _ => raise error ("cpy_nam: for "^(term2str t));
1.1106 +
1.1107 +(*> val (field,(dsc,t)) = last_elem pbt;
1.1108 +> cpy_nam pbt (drop_last oris) (field,(dsc,t));
1.1109 +val it = ([1],"#Find",
1.1110 + Const ("Descript.solutions","bool List.list => Tools.toreall"),
1.1111 + [Free ("x_i","bool List.list")]) *)
1.1112 +
1.1113 +
1.1114 +(*.match the actual arguments of a SubProblem with a model-pattern
1.1115 + and create an ori list (in root-pbl created from formalization).
1.1116 + expects ags:pats = 1:1, while copy-named are filtered out of pats;
1.1117 + copy-named pats are appended in order to get them into the model-items.*)
1.1118 +fun match_ags thy (pbt:pat list) ags =
1.1119 +(* val (thy, pbt, ags) = (thy, (#ppc o get_pbt) pI, ags);
1.1120 + val (thy, pbt, ags) = (thy, pats, ags);
1.1121 + *)
1.1122 + let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
1.1123 + val pbt' = filter_out is_copy_named pbt;
1.1124 + val cy = filter is_copy_named pbt;
1.1125 + val oris' = matc thy pbt' ags [];
1.1126 + val cy' = map (cpy_nam pbt' oris') cy;
1.1127 + val ors = add_id (oris' @ cy');
1.1128 + (*appended in order to get ^^^^^ them into the model-items*)
1.1129 + in (map flattup ors):ori list end;
1.1130 +(*vars as above ..
1.1131 +> match_ags thy pbt ags;
1.1132 +val it =
1.1133 + [(1,[1],"#Given",Const ("Descript.equality","bool => Tools.una"),
1.1134 + [Const # $ (# $ #) $ Free (#,#)]),
1.1135 + (2,[1],"#Given",Const ("Descript.solveFor","RealDef.real => Tools.una"),
1.1136 + [Free ("x","RealDef.real")]),
1.1137 + (3,[1],"#Find",
1.1138 + Const ("Descript.solutions","bool List.list => Tools.toreall"),
1.1139 + [Free ("x_i","bool List.list")])] : ori list*)
1.1140 +
1.1141 +(*.report part of the error-msg which is not available in match_args.*)
1.1142 +fun match_ags_msg pI stac ags =
1.1143 + let val s = !show_types
1.1144 + val _ = show_types:= true
1.1145 + val pats = (#ppc o get_pbt) pI
1.1146 + val msg = (dots 70^"\n"
1.1147 + ^"*** problem "^strs2str pI^" has the ...\n"
1.1148 + ^"*** model-pattern "^pats2str pats^"\n"
1.1149 + ^"*** stac '"^term2str stac^"' has the ...\n"
1.1150 + ^"*** arg-list "^terms2str ags^"\n"
1.1151 + ^dashs 70)
1.1152 + val _ = show_types:= s
1.1153 + in writeln msg end;
1.1154 +
1.1155 +
1.1156 +(*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)
1.1157 +fun vars_of_pbl_ pbl_ =
1.1158 + let fun var_of_pbl_ (gfr,(dsc,t)) = t
1.1159 + in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;
1.1160 +fun vars_of_pbl_' pbl_ =
1.1161 + let fun var_of_pbl_ (gfr,(dsc,t)) = t:term
1.1162 + in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;
1.1163 +
1.1164 +fun overwrite_ppc thy itm ppc =
1.1165 + let
1.1166 + fun repl ppc' (_,_,_,_,itm_) [] =
1.1167 + raise error ("overwrite_ppc: "^(itm__2str thy itm_)^" not found")
1.1168 + | repl ppc' itm (p::ppc) =
1.1169 + if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
1.1170 + else repl (ppc' @ [p]) itm ppc
1.1171 + in repl [] itm ppc end;
1.1172 +
1.1173 +(*10.3.00: insert the already compiled itm into model;
1.1174 + ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
1.1175 +(* val ppc=pbl;
1.1176 + *)
1.1177 +fun insert_ppc thy itm ppc =
1.1178 + let
1.1179 + fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)
1.1180 + | eq_untouched _ _ = false;
1.1181 + val ppc' =
1.1182 + (
1.1183 + (*writeln("### insert_ppc: itm= "^(itm2str itm));*)
1.1184 + case seek_ppc (#1 itm) ppc of
1.1185 + (* val Some xxx = seek_ppc (#1 itm) ppc;
1.1186 + *)
1.1187 + Some _ => (*itm updated in is_notyet_input WN.11.03*)
1.1188 + overwrite_ppc thy itm ppc
1.1189 + | None => (ppc @ [itm]));
1.1190 + in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;
1.1191 +
1.1192 +(*from Isabelle/src/Pure/library.ML, _appends_ a new element*)
1.1193 +fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];
1.1194 +
1.1195 +fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) =
1.1196 + (d_in itm_) = (d_in iitm_);
1.1197 +(*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
1.1198 + handles superfluous items carelessly*)
1.1199 +fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);
1.1200 +(* val eee = op=;
1.1201 + > gen_ins' eee (4,[1,3,5,7]);
1.1202 +val it = [1, 3, 5, 7, 4] : int list*)
1.1203 +
1.1204 +
1.1205 +(*. output the headline to a ppc .*)
1.1206 +fun header p_ pI mI =
1.1207 + case p_ of Pbl => Problem (if pI = e_pblID then [] else pI)
1.1208 + | Met => Method mI
1.1209 + | pos => raise error ("header called with "^ pos_2str pos);
1.1210 +
1.1211 +
1.1212 +
1.1213 +(* test-printouts ---
1.1214 +val _=writeln("### insert_ppc: (d,ts)="^(string_of_cterm(comp_dts thy(d,ts))));
1.1215 + val _=writeln("### insert_ppc: pts= "^
1.1216 +(strs2str' o map (Sign.string_of_term (sign_of thy))) pts);
1.1217 +
1.1218 +
1.1219 + val sel = "#Given"; val Add_Given' ct = m;
1.1220 +
1.1221 + val sel = "#Find"; val Add_Find' (ct,_) = m;
1.1222 + val (p,_) = p;
1.1223 + val (_,_,f,nxt',_,pt')= specify_additem sel (ct,[]) (p,Pbl(*!!!!!!!*)) c pt;
1.1224 +--------------
1.1225 + val sel = "#Given"; val Add_Given' (ct,_) = nxt; val (p,_) = p;
1.1226 + *)
1.1227 +fun specify_additem sel (ct,_) (p,Met) c pt =
1.1228 + let
1.1229 + val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.1230 + probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1.1231 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.1232 + (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
1.1233 + val cpI = if pI = e_pblID then pI' else pI;
1.1234 + val cmI = if mI = e_metID then mI' else mI;
1.1235 + val {ppc,pre,prls,...} = get_met cmI
1.1236 + in case appl_add thy sel oris met ppc ct of
1.1237 + Add itm (*..union old input *) =>
1.1238 + let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1.1239 + *)
1.1240 + val met' = insert_ppc thy itm met;
1.1241 + (*val pt' = update_met pt p met';*)
1.1242 + val ((p,Met),_,_,pt') =
1.1243 + generate1 thy (case sel of
1.1244 + "#Given" => Add_Given' (ct, met')
1.1245 + | "#Find" => Add_Find' (ct, met')
1.1246 + | "#Relate"=> Add_Relation'(ct, met'))
1.1247 + Uistate (p,Met) pt
1.1248 + val pre' = check_preconds thy prls pre met'
1.1249 + val pb = foldl and_ (true, map fst pre')
1.1250 + (*val _=writeln("@@@ specify_additem: Met Add before nxt_spec")*)
1.1251 + val (p_,nxt) =
1.1252 + nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1.1253 + ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
1.1254 + in ((p,p_), ((p,p_),Uistate),
1.1255 + Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.1256 + (Method cmI, itms2itemppc thy met' pre'))),
1.1257 + nxt,Safe,pt') end
1.1258 + | Err msg =>
1.1259 + let val pre' = check_preconds thy prls pre met
1.1260 + val pb = foldl and_ (true, map fst pre')
1.1261 + (*val _=writeln("@@@ specify_additem: Met Err before nxt_spec")*)
1.1262 + val (p_,nxt) =
1.1263 + nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1.1264 + ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
1.1265 + in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1.1266 + end
1.1267 +(* val (p,_) = p;
1.1268 + *)
1.1269 +| specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt =
1.1270 + let
1.1271 + val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.1272 + probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1.1273 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.1274 + val cpI = if pI = e_pblID then pI' else pI;
1.1275 + val cmI = if mI = e_metID then mI' else mI;
1.1276 + val {ppc,where_,prls,...} = get_pbt cpI;
1.1277 + in case appl_add thy sel oris pbl ppc ct of
1.1278 + Add itm (*..union old input *) =>
1.1279 + (* val Add itm = appl_add thy sel oris pbl ppc ct;
1.1280 + *)
1.1281 + let
1.1282 + (*val _= writeln("###specify_additem: itm= "^(itm2str itm));*)
1.1283 + val pbl' = insert_ppc thy itm pbl
1.1284 + val ((p,Pbl),_,_,pt') =
1.1285 + generate1 thy (case sel of
1.1286 + "#Given" => Add_Given' (ct, pbl')
1.1287 + | "#Find" => Add_Find' (ct, pbl')
1.1288 + | "#Relate"=> Add_Relation'(ct, pbl'))
1.1289 + Uistate (p,Pbl) pt
1.1290 + val pre = check_preconds thy prls where_ pbl'
1.1291 + val pb = foldl and_ (true, map fst pre)
1.1292 + (*val _=writeln("@@@ specify_additem: Pbl Add before nxt_spec")*)
1.1293 + val (p_,nxt) =
1.1294 + nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met)
1.1295 + (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1.1296 + val ppc = if p_= Pbl then pbl' else met;
1.1297 + in ((p,p_), ((p,p_),Uistate),
1.1298 + Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.1299 + (header p_ pI cmI,
1.1300 + itms2itemppc thy ppc pre))), nxt,Safe,pt') end
1.1301 +
1.1302 + | Err msg =>
1.1303 + let val pre = check_preconds thy prls where_ pbl
1.1304 + val pb = foldl and_ (true, map fst pre)
1.1305 + (*val _=writeln("@@@ specify_additem: Pbl Err before nxt_spec")*)
1.1306 + val (p_,nxt) =
1.1307 + nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1.1308 + (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1.1309 + in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1.1310 + end;
1.1311 +(* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1.1312 + val (_,_,f,nxt',_,pt')= specify_additem sel ct (p,Met) c pt;
1.1313 + *)
1.1314 +
1.1315 +(* ori
1.1316 +val (msg,itm) = appl_add thy sel oris ppc ct;
1.1317 +val (Cor(d,ts)) = #5 itm;
1.1318 +map (atomty) ts;
1.1319 +
1.1320 +pre
1.1321 +*)
1.1322 +
1.1323 +
1.1324 +(* val Init_Proof' (fmz,(dI',pI',mI')) = m;
1.1325 + specify (Init_Proof' (fmz,(dI',pI',mI'))) e_pos' [] EmptyPtree;
1.1326 + *)
1.1327 +fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1.1328 + let (* either """"""""""""""" all empty or complete *)
1.1329 + val thy = assoc_thy dI';
1.1330 + val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
1.1331 + else prep_ori fmz thy ((#ppc o get_pbt) pI');
1.1332 + val (pt,c) = cappend_problem e_ptree [] e_istate (fmz,(dI',pI',mI'))
1.1333 + (oris,(dI',pI',mI'),e_term);
1.1334 + val {ppc,prls,where_,...} = get_pbt pI'
1.1335 + (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1.1336 + val pt = update_pbl pt [] pbl;
1.1337 + val pre = check_preconds thy prls where_ pbl
1.1338 + val pb = foldl and_ (true, map fst pre)*)
1.1339 + val (pbl, pre, pb) = ([], [], false)
1.1340 + in case mI' of
1.1341 + ["no_met"] =>
1.1342 + (([],Pbl), (([],Pbl),Uistate),
1.1343 + Form' (PpcKF (0,EdUndef,(length []),Nundef,
1.1344 + (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.1345 + Refine_Tacitly pI', Safe,pt)
1.1346 + | _ =>
1.1347 + (([],Pbl), (([],Pbl),Uistate),
1.1348 + Form' (PpcKF (0,EdUndef,(length []),Nundef,
1.1349 + (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.1350 + Model_Problem,
1.1351 + Safe,pt)
1.1352 + end
1.1353 + (*ONLY for STARTING modeling phase*)
1.1354 + | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
1.1355 + let (* val (Model_Problem' (_,pbl), pos as (p,p_)) = (m, (p,p_));
1.1356 + *)
1.1357 + val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) =
1.1358 + get_obj I pt p
1.1359 + val thy' = if dI = e_domID then dI' else dI
1.1360 + val thy = assoc_thy thy'
1.1361 + val {ppc,prls,where_,...} = get_pbt pI'
1.1362 + val pre = check_preconds thy prls where_ pbl
1.1363 + val pb = foldl and_ (true, map fst pre)
1.1364 + val ((p,_),_,_,pt) =
1.1365 + generate1 thy (Model_Problem'([],pbl,met)) Uistate pos pt
1.1366 + val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1.1367 + (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1.1368 + in ((p,Pbl), ((p,p_),Uistate),
1.1369 + Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.1370 + (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
1.1371 + nxt, Safe, pt) end
1.1372 +
1.1373 +(*. called only if no_met is specified .*)
1.1374 + | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1.1375 + let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
1.1376 + *)
1.1377 + val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) =
1.1378 + get_obj I pt p;
1.1379 + val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1.1380 + (*val pbl = init_pbl ppc --- Model_Problem recognizes probl=[]*)
1.1381 + (*val pt = update_pbl pt p pbl;
1.1382 + val pt = update_orispec pt p
1.1383 + (string_of_thy thy, pIre,
1.1384 + if length met = 0 then e_metID else hd met);*)
1.1385 + val (domID, metID) = (string_of_thy thy,
1.1386 + if length met = 0 then e_metID else hd met)
1.1387 + val ((p,_),_,_,pt) =
1.1388 + generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1.1389 + Uistate pos pt
1.1390 + (*val pre = check_preconds thy prls where_ pbl
1.1391 + val pb = foldl and_ (true, map fst pre)*)
1.1392 + val (pbl, pre, pb) = ([], [], false)
1.1393 + in ((p,Pbl), (pos,Uistate),
1.1394 + Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.1395 + (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
1.1396 + Model_Problem, Safe, pt) end
1.1397 +
1.1398 + | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1.1399 + let val (pos,_,_,pt) = generate1 (assoc_thy "Isac.thy")
1.1400 + (Refine_Problem' rfd) Uistate pos pt
1.1401 + in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1.1402 + Model_Problem, Safe, pt) end
1.1403 +
1.1404 +(* val (Specify_Problem' (pI, (ok, (itms, pre)))) = nxt; val (p,_) = p;
1.1405 + val (Specify_Problem' (pI, (ok, (itms, pre)))) = m; val (p,_) = p;
1.1406 + *)
1.1407 + | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1.1408 + let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1.1409 + meth=met, ...}) = get_obj I pt p;
1.1410 + (*val pt = update_pbl pt p itms;
1.1411 + val pt = update_pblID pt p pI;*)
1.1412 + val ((p,Pbl),_,_,pt)=
1.1413 + generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate pos pt
1.1414 + val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1.1415 + val mI'' = if mI=e_metID then mI' else mI;
1.1416 + (*val _=writeln("@@@ specify (Specify_Problem) before nxt_spec")*)
1.1417 + val (_,nxt) = nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1.1418 + ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1.1419 + in ((p,Pbl), (pos,Uistate),
1.1420 + Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.1421 + (Problem pI, itms2itemppc dI'' itms pre))),
1.1422 + nxt, Safe, pt) end
1.1423 +(* val Specify_Method' mID = nxt; val (p,_) = p;
1.1424 + val Specify_Method' mID = m;
1.1425 + specify (Specify_Method' mID) (p,p_) c pt;
1.1426 + *)
1.1427 + | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1.1428 + let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1.1429 + meth=met, ...}) = get_obj I pt p;
1.1430 + val {ppc,pre,prls,...} = get_met mID
1.1431 + val thy = assoc_thy dI
1.1432 + val oris = add_field' thy ppc oris;
1.1433 + (*val pt = update_oris pt p oris; 20.3.02: repl. "#undef"*)
1.1434 + val dI'' = if dI=e_domID then dI' else dI;
1.1435 + val pI'' = if pI = e_pblID then pI' else pI;
1.1436 + val met = if met=[] then pbl else met;
1.1437 + val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1.1438 + (*val pt = update_met pt p itms;
1.1439 + val pt = update_metID pt p mID*)
1.1440 + val (pos,_,_,pt)=
1.1441 + generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
1.1442 + (*val _=writeln("@@@ specify (Specify_Method) before nxt_spec")*)
1.1443 + val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1.1444 + ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1.1445 + in (pos, (pos,Uistate),
1.1446 + Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.1447 + (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1.1448 + nxt, Safe, pt) end
1.1449 +(* val Add_Find' ct = nxt; val sel = "#Find";
1.1450 + *)
1.1451 + | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1.1452 + | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1.1453 + | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1.1454 +(* val Specify_Theory' domID = m;
1.1455 + val (Specify_Theory' domID, (p,p_)) = (m, pos);
1.1456 + *)
1.1457 + | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1.1458 + let val p_ = case p_ of Met => Met | _ => Pbl
1.1459 + val thy = assoc_thy domID;
1.1460 + val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1.1461 + probl=pbl, spec=(dI,pI,mI),...}) = get_obj I pt p;
1.1462 + val mppc = case p_ of Met => met | _ => pbl;
1.1463 + val cpI = if pI = e_pblID then pI' else pI;
1.1464 + val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1.1465 + val cmI = if mI = e_metID then mI' else mI;
1.1466 + val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1.1467 + val pre =
1.1468 + case p_ of
1.1469 + Met => (check_preconds thy mer mwh met)
1.1470 + | _ => (check_preconds thy per pwh pbl)
1.1471 + val pb = foldl and_ (true, map fst pre)
1.1472 + in if domID = dI
1.1473 + then let
1.1474 + (*val _=writeln("@@@ specify (Specify_Theory) THEN before nxt_spec")*)
1.1475 + val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1.1476 + (pbl,met) (ppc,mpc) (dI,pI,mI);
1.1477 + in ((p,p_), (pos,Uistate),
1.1478 + Form'(PpcKF (0,EdUndef,(length p), Nundef,
1.1479 + (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.1480 + nxt,Safe,pt) end
1.1481 + else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1.1482 + let
1.1483 + (*val pt = update_domID pt p domID;11.8.03*)
1.1484 + val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
1.1485 + Uistate (p,p_) pt
1.1486 + (*val _=writeln("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
1.1487 + val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
1.1488 + (ppc,mpc) (domID,pI,mI);
1.1489 + in ((p,p_), (pos,Uistate),
1.1490 + Form' (PpcKF (0, EdUndef, (length p),Nundef,
1.1491 + (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.1492 + nxt, Safe,pt) end
1.1493 + end
1.1494 +(* itms2itemppc thy [](*mpc*) pre
1.1495 + *)
1.1496 + | specify m' _ _ _ =
1.1497 + raise error ("specify: not impl. for "^tac_2str m');
1.1498 +
1.1499 +(* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
1.1500 + val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
1.1501 + *)
1.1502 +fun nxt_specif_additem sel ct (ptp as (pt,(p,Pbl))) =
1.1503 + let
1.1504 + val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1.1505 + probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1.1506 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.1507 + val cpI = if pI = e_pblID then pI' else pI;
1.1508 + in case appl_add thy sel oris pbl ((#ppc o get_pbt) cpI) ct of
1.1509 + Add itm (*..union old input *) =>
1.1510 +(* val Add itm = appl_add thy sel oris pbl ppc ct;
1.1511 + *)
1.1512 + let
1.1513 + (*val _=writeln("###nxt_specif_additem: itm= "^(itm2str itm));*)
1.1514 + val pbl' = insert_ppc thy itm pbl
1.1515 + val (tac,tac_) =
1.1516 + case sel of
1.1517 + "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1.1518 + | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1.1519 + | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1.1520 + val ((p,Pbl),c,_,pt') =
1.1521 + generate1 thy tac_ Uistate (p,Pbl) pt
1.1522 + in ([(tac,tac_,((p,Pbl),Uistate))], c, (pt',(p,Pbl))):calcstate' end
1.1523 +
1.1524 + | Err msg =>
1.1525 + (*TODO.WN03 pass error-msgs to the frontend..
1.1526 + FIXME ..and dont abuse a tactic for that purpose*)
1.1527 + ([(Tac msg,
1.1528 + Tac_ (ProtoPure.thy, msg,msg,msg),
1.1529 + (e_pos', e_istate))], [], ptp)
1.1530 + end
1.1531 +
1.1532 +(* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1.1533 + val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt;
1.1534 + *)
1.1535 + | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1.1536 + let
1.1537 + val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.1538 + probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1.1539 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.1540 + val cmI = if mI = e_metID then mI' else mI;
1.1541 + in case appl_add thy sel oris met ((#ppc o get_met) cmI) ct of
1.1542 + Add itm (*..union old input *) =>
1.1543 + let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1.1544 + *)
1.1545 + val met' = insert_ppc thy itm met;
1.1546 + val (tac,tac_) =
1.1547 + case sel of
1.1548 + "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1.1549 + | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1.1550 + | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1.1551 + val ((p,Met),c,_,pt') =
1.1552 + generate1 thy tac_ Uistate (p,Met) pt
1.1553 + in ([(tac,tac_,((p,Met), Uistate))], c, (pt',(p,Met))) end
1.1554 +
1.1555 + | Err msg => ([(*tacis*)], [], ptp)
1.1556 + (*nxt_me collects tacis until not hide; here just no progress*)
1.1557 + end;
1.1558 +
1.1559 +(* ori
1.1560 +val (msg,itm) = appl_add thy sel oris ppc ct;
1.1561 +val (Cor(d,ts)) = #5 itm;
1.1562 +map (atomty) ts;
1.1563 +
1.1564 +pre
1.1565 +*)
1.1566 +fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1.1567 + (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1.1568 + handle _ => raise error ("ori2Coritm: dsc "^
1.1569 + term2str d^
1.1570 + "in ori, but not in pbt")
1.1571 + ,ts))):itm;
1.1572 +fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =
1.1573 + ((i,v,true,f, Cor ((d,ts),((snd o snd o the o
1.1574 + (find_first (eq1 d))) pbt,ts))):itm)
1.1575 + handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)
1.1576 + ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);
1.1577 +
1.1578 +
1.1579 +(*filter out oris which have same description in itms*)
1.1580 +fun filter_outs oris [] = oris
1.1581 + | filter_outs oris (i::itms) =
1.1582 + let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o
1.1583 + (#4:ori -> term)) oris;
1.1584 + in filter_outs ors itms end;
1.1585 +
1.1586 +fun memI a b = b mem a;
1.1587 +(*filter oris which are in pbt, too*)
1.1588 +fun filter_pbt oris pbt =
1.1589 + let val dscs = map (fst o snd) pbt
1.1590 + in filter ((memI dscs) o (#4: ori -> term)) oris end;
1.1591 +
1.1592 +(*.combine itms from pbl + met and complete them wrt. pbt.*)
1.1593 +(*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
1.1594 +fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met =
1.1595 +(* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
1.1596 + *)
1.1597 + let val vat = max_vt pits;
1.1598 + val itms = pits @
1.1599 + (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);
1.1600 + val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
1.1601 + val os = filter_outs ors itms;
1.1602 + (*WN.12.03?: does _NOT_ add itms from met ?!*)
1.1603 + in itms @ (map (ori2Coritm met) os) end;
1.1604 +
1.1605 +
1.1606 +
1.1607 +(*.complete model and guard of a calc-head .*)
1.1608 +fun complete_mod_ (oris, mpc, ppc, probl) =
1.1609 + let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
1.1610 + val vat = if probl = [] then 1 else max_vt probl
1.1611 + val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris
1.1612 + val pors = filter_outs pors pits (*which are in pbl already*)
1.1613 + val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
1.1614 +
1.1615 + val pits = pits @ (map (ori2Coritm ppc) pors)
1.1616 + val mits = complete_metitms oris pits [] mpc
1.1617 + in (pits, mits) end;
1.1618 +
1.1619 +fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
1.1620 + (if dI = e_domID then odI else dI,
1.1621 + if pI = e_pblID then opI else pI,
1.1622 + if mI = e_metID then omI else mI):spec;
1.1623 +
1.1624 +
1.1625 +(*.find a next applicable tac (for calcstate) and update ptree
1.1626 + (for ev. finding several more tacs due to hide).*)
1.1627 +(*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)
1.1628 +(*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1.1629 +(*WN.24.10.03 fun nxt_solv = ...................................??*)
1.1630 +fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1.1631 + let
1.1632 + val (PblObj{origin=(oris,ospec,_),probl,spec,...}) = get_obj I pt p
1.1633 + val (dI,pI,mI) = some_spec ospec spec
1.1634 + val mpc = (#ppc o get_met) mI (*just for reuse complete_mod_*)
1.1635 + val {cas,ppc,...} = get_pbt pI
1.1636 + val pbl = init_pbl ppc (*fill in descriptions*)
1.1637 + (*--------------if you think, this should be done by the Dialog
1.1638 + in the java front-end, search there for WN060225-modelProblem----*)
1.1639 + val (pbl,met) = case cas of None => (pbl,[])
1.1640 + | _ => complete_mod_ (oris, mpc, ppc, probl)
1.1641 + (*----------------------------------------------------------------*)
1.1642 + val tac_ = Model_Problem' (pI, pbl, met)
1.1643 + val (pos,c,_,pt) = generate1 thy tac_ Uistate pos pt
1.1644 + in ([(tac,tac_, (pos, Uistate))], c, (pt,pos)):calcstate' end
1.1645 +
1.1646 +(* val Add_Find ct = tac;
1.1647 + *)
1.1648 + | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1.1649 + | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1.1650 + | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1.1651 +
1.1652 +(*. called only if no_met is specified .*)
1.1653 + | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1.1654 + let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
1.1655 + val opt = refine_ori oris pI
1.1656 + in case opt of
1.1657 + Some pI' =>
1.1658 + let val {met,ppc,...} = get_pbt pI'
1.1659 + val pbl = init_pbl ppc
1.1660 + (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1.1661 + val mI = if length met = 0 then e_metID else hd met
1.1662 + val (pos,c,_,pt) =
1.1663 + generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1.1664 + Uistate pos pt
1.1665 + in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1.1666 + (pos, Uistate))], c, (pt,pos)) end
1.1667 + | None => ([], [], ptp)
1.1668 + end
1.1669 +
1.1670 + | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1.1671 + let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
1.1672 + probl, ...}) = get_obj I pt p
1.1673 + val thy = if dI' = e_domID then dI else dI'
1.1674 + in case refine_pbl (assoc_thy thy) pI probl of
1.1675 + None => ([], [], ptp)
1.1676 + | Some (rfd as (pI',_)) =>
1.1677 + let val (pos,c,_,pt) =
1.1678 + generate1 (assoc_thy thy)
1.1679 + (Refine_Problem' rfd) Uistate pos pt
1.1680 + in ([(Refine_Problem pI, Refine_Problem' rfd,
1.1681 + (pos, Uistate))], c, (pt,pos)) end
1.1682 + end
1.1683 +
1.1684 + | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1.1685 + let val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_),
1.1686 + probl, ...}) = get_obj I pt p;
1.1687 + val thy = assoc_thy (if dI' = e_domID then dI else dI');
1.1688 + val {ppc,where_,prls,...} = get_pbt pI
1.1689 + val pbl as (_,(itms,_)) =
1.1690 + if pI'=e_pblID andalso pI=e_pblID
1.1691 + then (false, (init_pbl ppc, []))
1.1692 + else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1.1693 + (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1.1694 + val ((p,Pbl),c,_,pt)=
1.1695 + generate1 thy (Specify_Problem' (pI, pbl)) Uistate pos pt
1.1696 + in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1.1697 + (pos,Uistate))], c, (pt,pos)) end
1.1698 +
1.1699 + (*transfers oris (not required in pbl) to met-model for script-env
1.1700 + FIXME.WN.8.03: application of several mIDs to SAME model?*)
1.1701 + | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1.1702 + let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1.1703 + meth=met, ...}) = get_obj I pt p;
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;(*WN0602 what if more itms in met?*)
1.1710 + val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1.1711 + val (pos,c,_,pt)=
1.1712 + generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
1.1713 + in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1.1714 + (pos,Uistate))], c, (pt,pos)) end
1.1715 +
1.1716 + | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1.1717 + let val (dI',_,_) = get_obj g_spec pt p
1.1718 + val (pos,c,_,pt) =
1.1719 + generate1 (assoc_thy "Isac.thy") (Specify_Theory' dI)
1.1720 + Uistate pos pt
1.1721 + in (*FIXXXME: check if pbl can still be parsed*)
1.1722 + ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
1.1723 + (pt, pos)) end
1.1724 +
1.1725 + | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1.1726 + let val (dI',_,_) = get_obj g_spec pt p
1.1727 + val (pos,c,_,pt) =
1.1728 + generate1 (assoc_thy "Isac.thy") (Specify_Theory' dI)
1.1729 + Uistate pos pt
1.1730 + in (*FIXXXME: check if met can still be parsed*)
1.1731 + ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
1.1732 + (pt, pos)) end
1.1733 +
1.1734 + | nxt_specif m' _ =
1.1735 + raise error ("nxt_specif: not impl. for "^tac2str m');
1.1736 +
1.1737 +(*.get the values from oris; handle the term list w.r.t. penv.*)
1.1738 +fun vals_of_oris oris =
1.1739 + ((map (mkval' o (#5:ori -> term list))) o
1.1740 + (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris;
1.1741 +
1.1742 +
1.1743 +
1.1744 +(*.create a calc-tree with oris via an cas.refined pbl.*)
1.1745 +fun nxt_specify_init_calc (([],(dI,pI,mI)): fmz) =
1.1746 +(* val ([],(dI,pI,mI)) = (fmz, sp);
1.1747 + *)
1.1748 + if pI <> [] then (*comes from pbl-browser*)
1.1749 + let val {cas,met,ppc,thy,...} = get_pbt pI
1.1750 + val dI = if dI = "" then theory2theory' thy else dI
1.1751 + val thy = assoc_thy dI
1.1752 + val mI = if mI = [] then hd met else mI
1.1753 + val hdl = case cas of None => pblterm dI pI | Some t => t
1.1754 + val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
1.1755 + ([], (dI,pI,mI), hdl)
1.1756 + val pt = update_spec pt [] (dI,pI,mI)
1.1757 + val pits = init_pbl' ppc
1.1758 + val pt = update_pbl pt [] pits
1.1759 + in ((pt,([],Pbl)), []): calcstate end
1.1760 + else if mI <> [] then (*comes from met-browser*)
1.1761 + let val {ppc,...} = get_met mI
1.1762 + val dI = if dI = "" then "Isac.thy" else dI
1.1763 + val thy = assoc_thy dI
1.1764 + val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
1.1765 + ([], (dI,pI,mI), e_term(*FIXME met*))
1.1766 + val pt = update_spec pt [] (dI,pI,mI)
1.1767 + val mits = init_pbl' ppc
1.1768 + val pt = update_met pt [] mits
1.1769 + in ((pt,([],Met)), []) end
1.1770 + else (*completely new example*)
1.1771 + let val (pt,_) = cappend_problem e_ptree [] e_istate ([], e_spec)
1.1772 + ([], e_spec, e_term)
1.1773 + in ((pt,([],Pbl)), []) end
1.1774 +(* val (fmz, (dI,pI,mI)) = (fmz, sp);
1.1775 + *)
1.1776 + | nxt_specify_init_calc (fmz:fmz_,(dI,pI,mI):spec) =
1.1777 + let (* either """"""""""""""" all empty or complete *)
1.1778 + val thy = assoc_thy dI
1.1779 + val (pI, pors, mI) =
1.1780 + if mI = ["no_met"]
1.1781 + then let val pors = prep_ori fmz thy ((#ppc o get_pbt) pI)
1.1782 + val pI' = refine_ori' pors pI;
1.1783 + in (pI', pors (*refinement over models with diff.prec only*),
1.1784 + (hd o #met o get_pbt) pI') end
1.1785 + else (pI, prep_ori fmz thy ((#ppc o get_pbt) pI), mI)
1.1786 + val {cas,ppc,thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1.1787 + val dI = theory2theory' (maxthy thy thy');
1.1788 + val hdl = case cas of
1.1789 + None => pblterm dI pI
1.1790 + | Some t => subst_atomic ((vars_of_pbl_' ppc)
1.1791 + ~~~ vals_of_oris pors) t
1.1792 + val (pt,_) = cappend_problem e_ptree [] e_istate (fmz,(dI,pI,mI))
1.1793 + (pors,(dI,pI,mI),hdl)
1.1794 + (*val pbl = init_pbl ppc WN.9.03: done by Model/Refine_Problem
1.1795 + val pt = update_pbl pt [] pbl*)
1.1796 + in ((pt,([],Pbl)), fst3 (nxt_specif Model_Problem (pt, ([],Pbl))))
1.1797 + end;
1.1798 +
1.1799 +
1.1800 +
1.1801 +(*18.12.99*)
1.1802 +fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) =
1.1803 +(* case appl_spec p pt m of /// 19.1.00
1.1804 + Notappl e => Error' (Error_ e)
1.1805 + | Appl =>
1.1806 +*) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
1.1807 + in f end;
1.1808 +
1.1809 +
1.1810 +
1.1811 +
1.1812 +
1.1813 +
1.1814 +(* --------------------- ME --------------------- *)
1.1815 +fun tag_form thy (formal, given) = cterm_of (sign_of thy)
1.1816 + (((head_of o term_of) given) $ (term_of formal));
1.1817 +(* val formal = (the o (parse thy)) "[R::real]";
1.1818 +> val given = (the o (parse thy)) "fixed_values (cs::real list)";
1.1819 +> tag_form thy (formal, given);
1.1820 +val it = "fixed_values [R]" : cterm
1.1821 +*)
1.1822 +fun chktyp thy (n, fs, gs) =
1.1823 + ((writeln o string_of_cterm o (nth n)) fs;
1.1824 + (writeln o string_of_cterm o (nth n)) gs;
1.1825 + tag_form thy (nth n fs, nth n gs));
1.1826 +
1.1827 +fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
1.1828 +
1.1829 +(* #####################################################
1.1830 + find the failing item:
1.1831 +> val n = 2;
1.1832 +> val tag__form = chktyp (n,formals,givens);
1.1833 +> (type_of o term_of o (nth n)) formals;
1.1834 +> (type_of o term_of o (nth n)) givens;
1.1835 +> atomty ((term_of o (nth n)) formals);
1.1836 +> atomty ((term_of o (nth n)) givens);
1.1837 +> atomty (term_of tag__form);
1.1838 +> use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
1.1839 + ##################################################### *)
1.1840 +
1.1841 +(* #####################################################
1.1842 + testdata setup
1.1843 +val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];
1.1844 +val formals = map (the o (parse thy)) origin;
1.1845 +
1.1846 +val given = ["equation (lhs=rhs)",
1.1847 + "bound_variable bdv", (* TODO type *)
1.1848 + "error_bound apx"];
1.1849 +val where_ = ["e is_root_equation_in bdv",
1.1850 + "bdv is_var",
1.1851 + "apx is_const_expr"];
1.1852 +val find = ["L::rat set"];
1.1853 +val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];
1.1854 +val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
1.1855 +val givens = map (the o (parse thy)) given;
1.1856 +
1.1857 +val tag__forms = chktyps (formals, givens);
1.1858 +map ((atomty) o term_of) tag__forms;
1.1859 + ##################################################### *)
1.1860 +
1.1861 +
1.1862 +(* check pbltypes, announces one failure a time *)
1.1863 +fun chk_vars ctppc =
1.1864 + let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
1.1865 + appc flat (mappc (vars o term_of) ctppc)
1.1866 + in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
1.1867 + else if (re\\(gi union fi)) <> []
1.1868 + then ("re\\(gi union fi)",re\\(gi union fi))
1.1869 + else ("ok",[]) end;
1.1870 +
1.1871 +(* check a new pbltype: variables (Free) unbound by given, find*)
1.1872 +fun unbound_ppc ctppc =
1.1873 + let val {Given=gi,Find=fi,Relate=re,...} =
1.1874 + appc flat (mappc (vars o term_of) ctppc)
1.1875 + in distinct (re\\(gi union fi)) end;
1.1876 +(*
1.1877 +> val org = {Given=["[R=(R::real)]"],Where=[],
1.1878 + Find=["[A::real]"],With=[],
1.1879 + Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]
1.1880 + }:string ppc;
1.1881 +> val ctppc = mappc (the o (parse thy)) org;
1.1882 +> unbound_ppc ctppc;
1.1883 +val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list
1.1884 +*)
1.1885 +
1.1886 +
1.1887 +(* f, a binary operator, is nested rightassociative *)
1.1888 +fun foldr1 f xs =
1.1889 + let
1.1890 + fun fld f (x::[]) = x
1.1891 + | fld f (x::x'::[]) = f (x',x)
1.1892 + | fld f (x::x'::xs) = f (fld f (x'::xs),x);
1.1893 + in ((fld f) o rev) xs end;
1.1894 +(*
1.1895 +> val (Some ct) = parse thy "[a=b,c=d,e=f]";
1.1896 +> val ces = map (cterm_of (sign_of thy)) (isalist2list (term_of ct));
1.1897 +> val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
1.1898 +> cterm_of (sign_of thy) conj;
1.1899 +val it = "(a = b & c = d) & e = f" : cterm
1.1900 +*)
1.1901 +
1.1902 +(* f, a binary operator, is nested leftassociative *)
1.1903 +fun foldl1 f (x::[]) = x
1.1904 + | foldl1 f (x::x'::[]) = f (x,x')
1.1905 + | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
1.1906 +(*
1.1907 +> val (Some ct) = parse thy "[a=b,c=d,e=f,g=h]";
1.1908 +> val ces = map (cterm_of (sign_of thy)) (isalist2list (term_of ct));
1.1909 +> val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
1.1910 +> cterm_of (sign_of thy) conj;
1.1911 +val it = "a = b & c = d & e = f & g = h" : cterm
1.1912 +*)
1.1913 +
1.1914 +
1.1915 +(* called only once, if a Subproblem has been located in the script*)
1.1916 +fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp =
1.1917 +(* val (Subproblem'((_,pblID,metID),_,_,_,_),ptp) = (m', (pt,(p,p_)));
1.1918 + *)
1.1919 + (case metID of
1.1920 + ["no_met"] =>
1.1921 + (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
1.1922 + | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
1.1923 + (*all stored in tac_ itms ^^^^^^^^^^*)
1.1924 + | nxt_model_pbl tac_ _ =
1.1925 + raise error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
1.1926 +(* run subp_rooteq.sml ''
1.1927 + until nxt=("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
1.1928 +> val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
1.1929 + (last_elem o drop_last) ets'';
1.1930 +> val mst = (last_elem o drop_last) ets'';
1.1931 +> nxt_model_pbl mst;
1.1932 +val it = Refine_Tacitly ["univariate","equation"] : tac
1.1933 +*)
1.1934 +
1.1935 +(*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
1.1936 +fun eq4 v (_,vts,_,_,_) = v mem vts;
1.1937 +(*((curry (op mem)) (vat:int)) o (#2:ori -> int list);*)
1.1938 +fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
1.1939 +
1.1940 +
1.1941 +
1.1942 +(*
1.1943 + writeln (oris2str pors);
1.1944 +
1.1945 + writeln (itms2str thy pits);
1.1946 + writeln (itms2str thy mits);
1.1947 + *)
1.1948 +
1.1949 +
1.1950 +(*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris
1.1951 + + met from fmz; assumes pos on PblObj, meth = [].*)
1.1952 +fun complete_mod (pt, pos as (p, p_):pos') =
1.1953 +(* val (pt, (p, _)) = (pt, p);
1.1954 + val (pt, (p, _)) = (pt, pos);
1.1955 + *)
1.1956 + let val _= if p_ <> Pbl
1.1957 + then writeln("###complete_mod: only impl.for Pbl, called with "^
1.1958 + pos'2str pos) else ()
1.1959 + val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) =
1.1960 + get_obj I pt p
1.1961 + val (dI,pI,mI) = some_spec ospec spec
1.1962 + val mpc = (#ppc o get_met) mI
1.1963 + val ppc = (#ppc o get_pbt) pI
1.1964 + val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
1.1965 + val pt = update_pblppc pt p pits
1.1966 + val pt = update_metppc pt p mits
1.1967 + in (pt, (p,Met):pos') end
1.1968 +;
1.1969 +(*| complete_mod (pt, pos as (p, Met):pos') =
1.1970 + raise error ("###complete_mod: only impl.for Pbl, called with "^
1.1971 + pos'2str pos);*)
1.1972 +
1.1973 +(*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1.1974 + oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1.1975 +fun all_modspec (pt, (p,_):pos') =
1.1976 +(* val (pt, (p,_)) = ptp;
1.1977 + *)
1.1978 + let val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
1.1979 + ...}) = get_obj I pt p;
1.1980 + val thy = assoc_thy dI;
1.1981 + val {ppc,...} = get_met mI;
1.1982 + val mors = prep_ori fmz_ thy ppc;
1.1983 + val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1.1984 + val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1.1985 + val pt = update_spec pt p (dI,pI,mI);
1.1986 + in (pt, (p,Met): pos') end;
1.1987 +
1.1988 +(*WN.12.03: use in nxt_spec, too ? what about variants ???*)
1.1989 +fun is_complete_mod_ ([]: itm list) = false
1.1990 + | is_complete_mod_ itms =
1.1991 + foldl and_ (true, (map #3 itms));
1.1992 +fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1.1993 + if (is_pblobj o (get_obj I pt)) p
1.1994 + then (is_complete_mod_ o (get_obj g_pbl pt)) p
1.1995 + else raise error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1.1996 + | is_complete_mod (pt, pos as (p, Met)) =
1.1997 + if (is_pblobj o (get_obj I pt)) p
1.1998 + then (is_complete_mod_ o (get_obj g_met pt)) p
1.1999 + else raise error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1.2000 + | is_complete_mod (_, pos) =
1.2001 + raise error ("is_complete_mod called by "^pos'2str pos^
1.2002 + " (should be Pbl or Met)");
1.2003 +
1.2004 +(*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1.2005 +fun is_complete_spec (pt, pos as (p,_): pos') =
1.2006 + if (not o is_pblobj o (get_obj I pt)) p
1.2007 + then raise error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
1.2008 + else let val (dI,pI,mI) = get_obj g_spec pt p
1.2009 + in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end;
1.2010 +(*.complete empty items in specification from origin (pbl, met ev.refined);
1.2011 + assumes 'is_complete_mod'.*)
1.2012 +fun complete_spec (pt, pos as (p,_): pos') =
1.2013 + let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p
1.2014 + val pt = update_spec pt p (some_spec ospec spec)
1.2015 + in (pt, pos) end;
1.2016 +
1.2017 +fun is_complete_modspec ptp =
1.2018 + is_complete_mod ptp andalso is_complete_spec ptp;
1.2019 +
1.2020 +
1.2021 +
1.2022 +
1.2023 +fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =
1.2024 +(* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);
1.2025 + *)
1.2026 + let val (_,_,metID) = get_somespec' spec spec'
1.2027 + val pre =
1.2028 + if metID = e_metID then []
1.2029 + else let val {prls,pre=where_,...} = get_met metID
1.2030 + val pre = check_preconds' prls where_ meth 0
1.2031 + in pre end
1.2032 + val allcorrect = is_complete_mod_ meth
1.2033 + andalso foldl and_ (true, (map #1 pre))
1.2034 + in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end
1.2035 + | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =
1.2036 +(* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);
1.2037 + *)
1.2038 + let val (_,pI,_) = get_somespec' spec spec'
1.2039 + val pre =
1.2040 + if pI = e_pblID then []
1.2041 + else let val {prls,where_,cas,...} = get_pbt pI
1.2042 + val pre = check_preconds' prls where_ probl 0
1.2043 + in pre end
1.2044 + val allcorrect = is_complete_mod_ probl
1.2045 + andalso foldl and_ (true, (map #1 pre))
1.2046 + in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;
1.2047 +
1.2048 +
1.2049 +fun pt_form (PrfObj {form,...}) = Form form
1.2050 + | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
1.2051 + let val (dI, pI, _) = get_somespec' spec spec'
1.2052 + val {cas,...} = get_pbt pI
1.2053 + in case cas of
1.2054 + None => Form (pblterm dI pI)
1.2055 + | Some t => Form (subst_atomic (mk_env probl) t)
1.2056 + end;
1.2057 +(*vvv takes the tac _generating_ the formula=result, asm ok....
1.2058 +fun pt_result (PrfObj {result=(t,asm), tac,...}) =
1.2059 + (Form t,
1.2060 + if null asm then None else Some asm,
1.2061 + Some tac)
1.2062 + | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =
1.2063 + let val (_,_,metID) = some_spec ospec spec
1.2064 + in (Form t,
1.2065 + if null asm then None else Some asm,
1.2066 + if metID = e_metID then None else Some (Apply_Method metID)) end;
1.2067 +-------------------------------------------------------------------------*)
1.2068 +
1.2069 +
1.2070 +(*.pt_extract returns
1.2071 + # the formula at pos
1.2072 + # the tactic applied to this formula
1.2073 + # the list of assumptions generated at this formula
1.2074 + (by application of another tac to the preceding formula !)
1.2075 + pos is assumed to come from the frontend, ie. generated by moveDown.*)
1.2076 +(*cannot be in ctree.sml, because ModSpec has to be calculated*)
1.2077 +fun pt_extract (pt,([],Res)) =
1.2078 +(* val (pt,([],Res)) = ptp;
1.2079 + *)
1.2080 + let val (f, asm) = get_obj g_result pt []
1.2081 + in (Form f, None, asm) end
1.2082 +(* val p = [3,2];
1.2083 + *)
1.2084 + | pt_extract (pt,(p,Res)) =
1.2085 +(* val (pt,(p,Res)) = ptp;
1.2086 + *)
1.2087 + let val (f, asm) = get_obj g_result pt p
1.2088 + val tac = if last_onlev pt p
1.2089 + then if is_pblobj' pt (lev_up p)
1.2090 + then let val (PblObj{spec=(_,pI,_),...}) =
1.2091 + get_obj I pt (lev_up p)
1.2092 + in if pI = e_pblID then None
1.2093 + else Some (Check_Postcond pI) end
1.2094 + else Some End_Trans (*WN0502 TODO for other branches*)
1.2095 + else let val p' = lev_on p
1.2096 + in if is_pblobj' pt p'
1.2097 + then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
1.2098 + get_obj I pt p'
1.2099 + in Some (Subproblem (dI, pI)) end
1.2100 + else if f = get_obj g_form pt p'
1.2101 + then Some (get_obj g_tac pt p')
1.2102 + (*because this Frm ~~~is not on worksheet*)
1.2103 + else Some (Take (term2str (get_obj g_form pt p')))
1.2104 + end
1.2105 + in (Form f, tac, asm) end
1.2106 +
1.2107 + | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
1.2108 +(* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
1.2109 + val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p);
1.2110 + *)
1.2111 + let val ppobj = get_obj I pt p
1.2112 + val f = if is_pblobj ppobj then pt_model ppobj p_
1.2113 + else get_obj pt_form pt p
1.2114 + val tac = g_tac ppobj
1.2115 + in (f, Some tac, []) end;
1.2116 +
1.2117 +
1.2118 +(**. get the formula from a ctree-node:
1.2119 + take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
1.2120 + take res from all other PrfObj's .**)
1.2121 +(*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)
1.2122 +fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =
1.2123 + [("headline", (p, Frm), h),
1.2124 + ("stepform", (p, Res), r)]
1.2125 + | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) =
1.2126 + [("stepform", (p, Frm), form),
1.2127 + ("stepform", (p, Res), r)];
1.2128 +
1.2129 +fun form p (Nd (PrfObj {result = (r, _),...}, _)) =
1.2130 + [("stepform", (p, Res), r)]
1.2131 +
1.2132 +(*assumes to take whole level, in particular hd -- for use in interSteps*)
1.2133 +fun get_formress fs p [] = flat fs
1.2134 + | get_formress fs p (nd::nds) =
1.2135 + (* start with 'form+res' and continue with trying 'res' only*)
1.2136 + get_forms (fs @ [formres p nd]) (lev_on p) nds
1.2137 +and get_forms fs p [] = flat fs
1.2138 + | get_forms fs p (nd::nds) =
1.2139 + if is_pblnd nd
1.2140 + (* start again with 'form+res' ///ugly repeat with Check_elementwise
1.2141 + then get_formress (fs @ [formres p nd]) (lev_on p) nds *)
1.2142 + then get_forms (fs @ [formres p nd]) (lev_on p) nds
1.2143 + (* continue with trying 'res' only*)
1.2144 + else get_forms (fs @ [form p nd]) (lev_on p) nds;
1.2145 +
1.2146 +(**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
1.2147 +(*WN050219 made robust against _'to' below or after Complete nodes
1.2148 + by handling exn caused by move_dn*)
1.2149 +(*WN0401 this functionality belongs to ctree.sml,
1.2150 +but fetching a calc_head requires calculations defined in modspec.sml
1.2151 +transfer to ME/me.sml !!!
1.2152 +WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head
1.2153 +is returned !!!!!!!!!!!!!
1.2154 +*)
1.2155 +fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2
1.2156 + | eq_pos' (p1,Res) (p2,Res) = p1 = p2
1.2157 + | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of
1.2158 + Pbl => true
1.2159 + | Met => true
1.2160 + | _ => false)
1.2161 + | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of
1.2162 + Pbl => true
1.2163 + | Met => true
1.2164 + | _ => false)
1.2165 + | eq_pos' _ _ = false;
1.2166 +
1.2167 +(*.get an 'interval' from the ctree; 'interval' is w.r.t. the
1.2168 + total ordering Position#compareTo(Position p) in the java-code
1.2169 +val get_interval = fn
1.2170 + : pos' -> : from is "move_up 1st-element" to return
1.2171 + pos' -> : to the last element to be returned; from < to
1.2172 + int -> : level: 0 gets the flattest sub-tree possible
1.2173 + >999 gets the deepest sub-tree possible
1.2174 + ptree -> :
1.2175 + (pos' * : of the formula
1.2176 + Term.term) : the formula
1.2177 + list
1.2178 +.*)
1.2179 +fun get_interval from to level pt =
1.2180 +(* val (from,level) = (f,lev);
1.2181 + val (from, to, level) = (([3, 2, 1], Res), ([],Res), 9999);
1.2182 + *)
1.2183 + let fun get_inter c (from:pos') (to:pos') lev pt =
1.2184 +(* val (c, from, to, lev) = ([], from, to, level);
1.2185 + ------for recursion.......
1.2186 + val (c, from:pos', to:pos') = (c @ [(from, f)], move_dn [] pt from, to);
1.2187 + *)
1.2188 + if eq_pos' from to orelse from = ([],Res)
1.2189 + (*orelse ... avoids Exception- PTREE "end of calculation" raised,
1.2190 + if 'to' has values NOT generated by move_dn, see systest/me.sml
1.2191 + TODO.WN0501: introduce an order on pos' and check "from > to"..
1.2192 + ...there is an order in Java!
1.2193 + WN051224 the hack got worse with returning term instead ptform*)
1.2194 + then let val (f,_,_) = pt_extract (pt, from)
1.2195 + in case f of
1.2196 + ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)]
1.2197 + | Form t => c @ [(from, t)]
1.2198 + end
1.2199 + else
1.2200 + if lev < lev_of from
1.2201 + then (get_inter c (move_dn [] pt from) to lev pt)
1.2202 + handle (PTREE _(*from move_dn too far*)) => c
1.2203 + else let val (f,_,_) = pt_extract (pt, from)
1.2204 + val term = case f of
1.2205 + ModSpec (_,_,headline,_,_,_)=> headline
1.2206 + | Form t => t
1.2207 + in (get_inter (c @ [(from, term)])
1.2208 + (move_dn [] pt from) to lev pt)
1.2209 + handle (PTREE _(*from move_dn too far*))
1.2210 + => c @ [(from, term)] end
1.2211 + in get_inter [] from to level pt end;
1.2212 +
1.2213 +(*for tests*)
1.2214 +fun posform2str (pos:pos', form) =
1.2215 + "("^ pos'2str pos ^", "^
1.2216 + (case form of
1.2217 + Form f => term2str f
1.2218 + | ModSpec c => term2str (#3 c(*the headline*)))
1.2219 + ^")";
1.2220 +fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
1.2221 + (map posform2str)) pfs;
1.2222 +fun posterm2str (pos:pos', t) =
1.2223 + "("^ pos'2str pos ^", "^term2str t^")";
1.2224 +fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
1.2225 + (map posterm2str)) pfs;
1.2226 +
1.2227 +
1.2228 +(*WN050225 omits the last step, if pt is incomplete*)
1.2229 +fun show_pt pt =
1.2230 + writeln (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
1.2231 +
1.2232 +(*.get a calchead from a PblObj-node in the ctree;
1.2233 + preconditions must be calculated.*)
1.2234 +fun get_ocalhd (pt, pos' as (p,Pbl):pos') =
1.2235 + let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} =
1.2236 + get_obj I pt p
1.2237 + val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
1.2238 + val pre = check_preconds (assoc_thy"Isac.thy") prls where_ probl
1.2239 + in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end
1.2240 +| get_ocalhd (pt, pos' as (p,Met):pos') =
1.2241 + let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
1.2242 + spec, meth,...} =
1.2243 + get_obj I pt p
1.2244 + val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
1.2245 + val pre = check_preconds (assoc_thy"Isac.thy") prls pre meth
1.2246 + in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;
1.2247 +
1.2248 +(*.at the activeFormula set the Model, the Guard and the Specification
1.2249 + to empty and return a CalcHead;
1.2250 + the 'origin' remains (for reconstructing all that).*)
1.2251 +fun reset_calchead (pt, pos' as (p,_):pos') =
1.2252 + let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p
1.2253 + val pt = update_pbl pt p []
1.2254 + val pt = update_met pt p []
1.2255 + val pt = update_spec pt p e_spec
1.2256 + in (pt, (p,Pbl):pos') end;
1.2257 +
1.2258 +(*---------------------------------------------------------------------*)
1.2259 +end
1.2260 +
1.2261 +open CalcHead;
1.2262 +(*---------------------------------------------------------------------*)
1.2263 +