neuper@38051: (* Title: Specify-phase: specifying and modeling a problem or a subproblem. The neuper@38051: most important types are declared in mstools.sml. e0726734@41962: Author: Walther Neuper 991122, Mathias Lehnfeld neuper@37906: (c) due to copyright terms wneuper@59265: *) wneuper@59265: signature CALC_HEAD = wneuper@59265: sig wneuper@59265: type calcstate wneuper@59265: type calcstate' wneuper@59276: datatype appl = Appl of Ctree.tac_ | Notappl of string wneuper@59276: val nxt_specify_init_calc : Ctree.fmz -> calcstate wneuper@59279: val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ctree -> wneuper@59279: Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ctree wneuper@59279: val nxt_specif : Ctree.tac -> Ctree.ctree * Ctree.pos' -> calcstate' wneuper@59276: val nxt_spec : Ctree.pos_ -> bool -> ori list -> spec -> itm list * itm list -> wneuper@59276: (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Ctree.tac neuper@37906: wneuper@59279: val reset_calchead : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' wneuper@59279: val get_ocalhd : Ctree.ctree * Ctree.pos' -> Ctree.ocalhd wneuper@59265: val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool wneuper@59279: val all_modspec : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' neuper@37906: wneuper@59265: val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list wneuper@59265: val insert_ppc' : itm -> itm list -> itm list neuper@37906: wneuper@59279: val complete_mod : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' wneuper@59279: val is_complete_mod : Ctree.ctree * Ctree.pos' -> bool wneuper@59279: val complete_spec : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' wneuper@59279: val is_complete_spec : Ctree.ctree * Ctree.pos' -> bool wneuper@59265: val some_spec : spec -> spec -> spec wneuper@59265: (* these could go to Ctree ..*) wneuper@59279: val show_pt : Ctree.ctree -> unit wneuper@59279: val pt_extract : Ctree.ctree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list wneuper@59279: val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ctree -> (Ctree.pos' * term) list neuper@37906: wneuper@59265: val match_ags : theory -> pat list -> term list -> ori list wneuper@59265: val match_ags_msg : pblID -> term -> term list -> unit wneuper@59265: val oris2fmz_vals : ori list -> string list * term list wneuper@59265: val vars_of_pbl_' : ('a * ('b * term)) list -> term list wneuper@59265: val is_known : Proof.context -> string -> ori list -> term -> string * ori * term list wneuper@59265: val is_notyet_input : Proof.context -> itm list -> term list -> ori -> ('a * (term * term)) list wneuper@59265: -> string * itm wneuper@59265: val e_calcstate' : calcstate' wneuper@59265: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) wneuper@59265: val vals_of_oris : ori list -> term list wneuper@59265: val is_error : itm_ -> bool wneuper@59265: val is_copy_named : 'a * ('b * term) -> bool wneuper@59265: val ori2Coritm : pat list -> ori -> itm wneuper@59265: val ppc2list : 'a ppc -> 'a list wneuper@59265: val is_copy_named_idstr : string -> bool wneuper@59265: val matc : theory -> (string * (term * term)) list -> term list -> preori list -> preori list wneuper@59265: val mtc : theory -> pat -> term -> preori option wneuper@59265: val cpy_nam : pat list -> preori list -> pat -> preori wneuper@59265: ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) wneuper@59265: end neuper@37906: wneuper@59265: structure Chead(**): CALC_HEAD(**) = neuper@37906: struct wneuper@59276: open Ctree neuper@37906: (* datatypes *) neuper@37906: wneuper@59265: (* the state wich is stored after each step of calculation; it contains neuper@38065: the calc-state and a list of [tac,istate](="tacis") to be applied next. neuper@37906: the last_elem tacis is the first to apply to the calc-state and neuper@37906: the (only) one shown to the front-end as the 'proposed tac'. neuper@37906: the calc-state resulting from the application of tacis is not stored, neuper@38065: because the tacis hold enough information for efficiently rebuilding wneuper@59265: this state just by "fun generate " wneuper@59265: *) neuper@37906: type calcstate = wneuper@59279: (ctree * pos') * (* the calc-state to which the tacis could be applied *) wneuper@59271: (Generate.taci list) (* ev. several (hidden) steps; wneuper@59265: in REVERSE order: first tac_ to apply is last_elem *) wneuper@59271: val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]) : calcstate; neuper@37906: neuper@37906: (*the state used during one calculation within the mathengine; it contains neuper@37906: a list of [tac,istate](="tacis") which generated the the calc-state; neuper@37906: while this state's tacis are extended by each (internal) step, neuper@37906: the calc-state is used for creating new nodes in the calc-tree neuper@37906: (eg. applicable_in requires several particular nodes of the calc-tree) neuper@37906: and then replaced by the the newly created; neuper@37906: on leave of the mathengine the resuing calc-state is dropped anyway, neuper@37906: because the tacis hold enought information for efficiently rebuilding neuper@37906: this state just by "fun generate ".*) neuper@37906: type calcstate' = wneuper@59271: Generate.taci list * (* cas. several (hidden) steps; wneuper@59266: in REVERSE order: first tac_ to apply is last_elem *) wneuper@59266: pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *) wneuper@59279: (ctree * pos') (* the calc-state resulting from the application of tacis *) wneuper@59271: val e_calcstate' = ([Generate.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate'; neuper@37906: wneuper@59265: (* FIXXXME.WN020430 intermediate hack for fun ass_up *) wneuper@59271: fun f_mout thy (Generate.FormKF f) = (Thm.term_of o the o (parse thy)) f wneuper@59265: | f_mout _ _ = error "f_mout: not called with formula"; neuper@37906: wneuper@59265: (* is the calchead complete ? *) wneuper@59265: fun ocalhd_complete its pre (dI, pI, mI) = wneuper@59265: foldl and_ (true, map #3 its) andalso wneuper@59265: foldl and_ (true, map #1 pre) andalso wneuper@59265: dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID neuper@37906: wneuper@59265: (* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris wneuper@59265: --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *) neuper@42092: fun oris2fmz_vals oris = wneuper@59265: let fun ori2fmz_vals ((_, _, _, dsc, ts): ori) = wneuper@59265: ((term2str o comp_dts') (dsc, ts), last_elem ts) wneuper@59265: handle _ => error ("ori2fmz_env called with " ^ terms2str ts) wneuper@59265: in (split_list o (map ori2fmz_vals)) oris end neuper@37906: neuper@37906: (* make a term 'typeless' for comparing with another 'typeless' term; neuper@37906: 'type-less' usually is illtyped *) wneuper@59265: fun typeless (Const (s, _)) = (Const (s, e_type)) wneuper@59265: | typeless (Free (s, _)) = (Free (s, e_type)) wneuper@59265: | typeless (Var (n, _)) = (Var (n, e_type)) neuper@37906: | typeless (Bound i) = (Bound i) wneuper@59265: | typeless (Abs (s, _,t)) = Abs(s, e_type, typeless t) wneuper@59265: | typeless (t1 $ t2) = (typeless t1) $ (typeless t2) neuper@37906: wneuper@59265: (* to an input (d,ts) find the according ori and insert the ts) wneuper@59265: WN.11.03: + dont take first inter<>[] *) wneuper@59265: fun seek_oridts ctxt sel (d, ts) [] = bonzai@41952: ("seek_oridts: input ('" ^ wneuper@59265: (term_to_string' ctxt (comp_dts (d, ts))) ^ "') not found in oris (typed)", bonzai@41952: (0, [], sel, d, ts), bonzai@41952: []) wneuper@59265: | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) = wneuper@59265: if sel = sel' andalso d = d' andalso (inter op = ts ts') <> [] wneuper@59265: then ("", (id, vat, sel, d, inter op = ts ts'), ts') wneuper@59265: else seek_oridts ctxt sel (d, ts) oris neuper@37906: wneuper@59265: (* to an input (_,ts) find the according ori and insert the ts *) wneuper@59265: fun seek_orits ctxt _ ts [] = neuper@52070: ("seek_orits: input (_, '" ^ strs2str (map (term_to_string' ctxt) ts) ^ neuper@52070: "') not found in oris (typed)", e_ori_, []) wneuper@59265: | seek_orits ctxt sel ts ((id, vat, sel', d, ts') :: (oris: ori list)) = neuper@37934: if sel = sel' andalso (inter op = ts ts') <> [] wneuper@59265: then wneuper@59265: if sel = sel' wneuper@59265: then ("", (id, vat, sel, d, inter op = ts ts'): ori, ts') wneuper@59265: else (((strs2str' o map (term_to_string' ctxt)) ts) ^ " not for " ^ sel, e_ori_, []) wneuper@59265: else seek_orits ctxt sel ts oris neuper@37906: wneuper@59265: (* find_first item with #1 equal to id *) wneuper@59265: fun seek_ppc _ [] = NONE wneuper@59265: | seek_ppc id (p :: (ppc: itm list)) = if id = #1 p then SOME p else seek_ppc id ppc neuper@37906: wneuper@59265: datatype appl = wneuper@59265: Appl of tac_ (* tactic is applicable at a certain position in the Ctree *) wneuper@59265: | Notappl of string (* tactic is NOT applicable *) neuper@37906: wneuper@59265: fun ppc2list ({Given = gis, Where = whs, Find = fis, With = wis, Relate = res}: 'a ppc) = wneuper@59265: gis @ whs @ fis @ wis @ res wneuper@59265: fun ppc135list ({Given = gis, Find = fis, Relate = res, ...}: 'a ppc) = gis @ fis @ res neuper@37906: neuper@37906: (* get the number of variants in a problem in 'original', neuper@37906: assumes equal descriptions in immediate sequence *) neuper@37906: fun variants_in ts = wneuper@59265: let wneuper@59265: fun eq (x, y) = head_of x = head_of y wneuper@59265: fun cnt _ [] _ n = ([n], []) wneuper@59265: | cnt eq (x :: xs) y n = if eq (x, y) then cnt eq xs y (n + 1) else ([n], x :: xs) wneuper@59265: fun coll _ xs [] = xs wneuper@59265: | coll eq xs (y :: ys) = wneuper@59265: let val (n, ys') = cnt eq (y :: ys) y 0 wneuper@59265: in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end wneuper@59265: val vts = subtract op = [1] (distinct (coll eq [] ts)) wneuper@59265: in wneuper@59265: case vts of wneuper@59265: [] => 1 wneuper@59265: | [n] => n wneuper@59265: | _ => error "different variants in formalization" wneuper@59265: end neuper@37906: wneuper@59265: fun is_list_type (Type ("List.list", _)) = true wneuper@59265: | is_list_type _ = false wneuper@59265: fun has_list_type (Free (_, T)) = is_list_type T wneuper@59265: | has_list_type _ = false neuper@37906: fun is_parsed (Syn _) = false wneuper@59265: | is_parsed _ = true wneuper@59265: fun parse_ok its = foldl and_ (true, map is_parsed its) neuper@37906: neuper@37906: fun all_dsc_in itm_s = neuper@37906: let wneuper@59265: fun d_in (Cor ((d, _), _)) = [d] wneuper@59265: | d_in (Syn _) = [] wneuper@59265: | d_in (Typ _) = [] neuper@37906: | d_in (Inc ((d,_),_)) = [d] neuper@37906: | d_in (Sup (d,_)) = [d] wneuper@59265: | d_in (Mis (d,_)) = [d] wneuper@59265: | d_in i = error ("all_dsc_in: uncovered case with " ^ itm_2str i) wneuper@59265: in (flat o (map d_in)) itm_s end; neuper@37906: wneuper@59265: fun is_error (Cor _) = false wneuper@59265: | is_error (Sup _) = false wneuper@59265: | is_error (Inc _) = false wneuper@59265: | is_error (Mis _) = false wneuper@59265: | is_error _ = true neuper@37906: wneuper@59265: (* get the first term in ts from ori *) neuper@38051: fun getr_ct thy ((_, _, fd, d, ts) : ori) = wneuper@59265: (fd, ((term_to_string''' thy) o comp_dts) (d,[hd ts]) : cterm') neuper@37906: neuper@38051: (* get a term from ori, notyet input in itm. neuper@38051: the term from ori is thrown back to a string in order to reuse neuper@38051: machinery for immediate input by the user. *) neuper@52070: fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) = neuper@52070: (fd, ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm') neuper@37906: neuper@37906: (* in FE dsc, not dat: this is in itms ...*) wneuper@59265: fun is_untouched ((_, _, false, _, Inc ((_, []), _)): itm) = true wneuper@59265: | is_untouched _ = false neuper@37906: neuper@37906: (* select an item in oris, notyet input in itms neuper@37906: (precondition: in itms are only Cor, Sup, Inc) *) wneuper@59235: (*args of nxt_add wneuper@59235: thy : for? wneuper@59235: oris: from formalization 'type fmz', structured for efficient access wneuper@59235: pbt : the problem-pattern to be matched with oris in order to get itms wneuper@59235: itms: already input items wneuper@59235: *) neuper@37906: fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*) wneuper@59265: let wneuper@59265: fun test_d d ((i, _, _, _, itm_): itm) = (d = (d_in itm_)) andalso i <> 0 wneuper@59265: fun is_elem itms (_, (d, _)) = wneuper@59265: case find_first (test_d d) itms of SOME _ => true | NONE => false wneuper@59265: in wneuper@59265: case filter_out (is_elem itms) pbt of wneuper@59265: (f, (d, _)) :: _ => SOME (f : string, ((term_to_string''' thy) o comp_dts) (d, []) : cterm') wneuper@59265: | _ => NONE wneuper@59265: end wneuper@59265: | nxt_add thy oris _ itms = wneuper@59265: let wneuper@59265: fun testr_vt v ori = member op= (#2 (ori:ori)) v andalso (#3 ori) <> "#undef" wneuper@59265: fun testi_vt v itm =member op= (#2 (itm:itm)) v wneuper@59265: fun test_id ids r = member op= ids (#1 (r:ori)) wneuper@59265: fun test_subset (itm:itm) ((_,_,_,d,ts):ori) = wneuper@59265: (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts) wneuper@59265: fun false_and_not_Sup ((_, _, false, _, Sup _): itm) = false wneuper@59265: | false_and_not_Sup (_, _, false, _, _) = true wneuper@59265: | false_and_not_Sup _ = false wneuper@59265: val v = if itms = [] then 1 else max_vt itms wneuper@59265: val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *) wneuper@59265: val vits = wneuper@59265: if v = 0 wneuper@59265: then itms (* because of dsc without dat *) wneuper@59265: else filter (testi_vt v) itms; (* itms..vat *) wneuper@59265: val icl = filter false_and_not_Sup vits; (* incomplete *) wneuper@59265: in wneuper@59265: if icl = [] wneuper@59265: then case filter_out (test_id (map #1 vits)) vors of wneuper@59265: [] => NONE wneuper@59265: | miss => SOME (getr_ct thy (hd miss)) wneuper@59265: else wneuper@59265: case find_first (test_subset (hd icl)) vors of wneuper@59265: NONE => error "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt" wneuper@59265: | SOME ori => SOME (geti_ct thy ori (hd icl)) wneuper@59265: end neuper@37906: wneuper@59269: fun mk_delete thy "#Given" itm_ = Del_Given (Specify.itm_out thy itm_) wneuper@59269: | mk_delete thy "#Find" itm_ = Del_Find (Specify.itm_out thy itm_) wneuper@59269: | mk_delete thy "#Relate" itm_ = Del_Relation(Specify.itm_out thy itm_) wneuper@59265: | mk_delete _ str _ = error ("mk_delete: called with field \"" ^ str ^ "\"") neuper@37906: fun mk_additem "#Given" ct = Add_Given ct wneuper@59265: | mk_additem "#Find" ct = Add_Find ct neuper@37906: | mk_additem "#Relate"ct = Add_Relation ct wneuper@59265: | mk_additem str _ = error ("mk_additem: called with field \"" ^ str ^ "\"") neuper@37906: neuper@38051: (* determine the next step of specification; neuper@38051: not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met)) neuper@38051: eg. in rootpbl 'no_met': neuper@37906: args: neuper@38051: preok predicates are _all_ ok (and problem matches completely) neuper@37906: oris immediately from formalization neuper@37906: (dI',pI',mI') specification coming from author/parent-problem neuper@37906: (pbl, item lists specified by user neuper@37906: met) -"-, tacitly completed by copy_probl neuper@37906: (dI,pI,mI) specification explicitly done by the user neuper@37906: (pbt, mpc) problem type, guard of method neuper@38051: *) neuper@38051: fun nxt_spec Pbl preok (oris : ori list) ((dI', pI', mI') : spec) wneuper@59265: ((pbl : itm list), (met : itm list)) (pbt, mpc) ((dI, pI, mI) : spec) = wneuper@59265: (if dI' = e_domID andalso dI = e_domID then (Pbl, Specify_Theory dI') neuper@38051: else if pI' = e_pblID andalso pI = e_pblID then (Pbl, Specify_Problem pI') wneuper@59265: else wneuper@59265: case find_first (is_error o #5) (pbl:itm list) of wneuper@59265: SOME (_, _, _, fd, itm_) => wneuper@59265: (Pbl, mk_delete (assoc_thy (if dI = e_domID then dI' else dI)) fd itm_) wneuper@59265: | NONE => wneuper@59265: (case nxt_add (assoc_thy (if dI = e_domID then dI' else dI)) oris pbt pbl of wneuper@59265: SOME (fd,ct') => (Pbl, mk_additem fd ct') wneuper@59265: | NONE => (*pbl-items complete*) wneuper@59265: if not preok then (Pbl, Refine_Problem pI') wneuper@59265: else if dI = e_domID then (Pbl, Specify_Theory dI') wneuper@59265: else if pI = e_pblID then (Pbl, Specify_Problem pI') wneuper@59265: else if mI = e_metID then (Pbl, Specify_Method mI') wneuper@59265: else wneuper@59265: case find_first (is_error o #5) met of wneuper@59265: SOME (_, _, _, fd, itm_) => (Met, mk_delete (assoc_thy dI) fd itm_) wneuper@59265: | NONE => wneuper@59265: (case nxt_add (assoc_thy dI) oris mpc met of wneuper@59265: SOME (fd, ct') => (Met, mk_additem fd ct') (*30.8.01: pre?!?*) wneuper@59265: | NONE => (Met, Apply_Method mI)))) wneuper@59265: | nxt_spec Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) = wneuper@59265: (case find_first (is_error o #5) met of wneuper@59265: SOME (_,_,_,fd,itm_) => (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_) wneuper@59265: | NONE => wneuper@59265: case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of wneuper@59265: SOME (fd,ct') => (Met, mk_additem fd ct') wneuper@59265: | NONE => wneuper@59265: (if dI = e_domID then (Met, Specify_Theory dI') wneuper@59265: else if pI = e_pblID then (Met, Specify_Problem pI') wneuper@59265: else if not preok then (Met, Specify_Method mI) wneuper@59265: else (Met, Apply_Method mI))) wneuper@59265: | nxt_spec p _ _ _ _ _ _ = error ("nxt_spec: uncovered case with " ^ pos_2str p) neuper@37906: neuper@37906: fun is_field_correct sel d dscpbt = neuper@37906: case assoc (dscpbt, sel) of neuper@37926: NONE => false wneuper@59265: | SOME ds => member op = ds d neuper@37906: wneuper@59265: (* update the itm_ already input, all..from ori *) wneuper@59265: fun ori_2itm itm_ pid all ((id, vt, fd, d, ts): ori) = neuper@37906: let neuper@37930: val ts' = union op = (ts_in itm_) ts; bonzai@41949: val pval = pbl_ids' d ts' wneuper@59265: (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *) wneuper@59265: val complete = if eq_set op = (ts', all) then true else false wneuper@59265: in wneuper@59265: case itm_ of wneuper@59265: (Cor _) => wneuper@59265: (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts')) wneuper@59265: else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval)))): itm wneuper@59265: | (Syn c) => error ("ori_2itm wants to overwrite " ^ c) wneuper@59265: | (Typ c) => error ("ori_2itm wants to overwrite " ^ c) wneuper@59265: | (Inc _) => wneuper@59265: if complete wneuper@59265: then (id, vt, true, fd, Cor ((d, ts'), (pid, pval))) wneuper@59265: else (id, vt, false, fd, Inc ((d, ts'), (pid, pval))) wneuper@59265: | (Sup (d,ts')) => (*4.9.01 lost env*) wneuper@59265: (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts')) wneuper@59265: (*else (id,vt,complete,fd,Cor((d,ts'),e))*) wneuper@59265: (* 28.1.00: not completely clear ---^^^ etc.*) wneuper@59265: | (Mis _) => (* 4.9.01: Mis just copied *) wneuper@59265: if complete wneuper@59265: then (id, vt, true, fd, Cor ((d,ts'), (pid, pval))) wneuper@59265: else (id, vt, false, fd, Inc ((d,ts'), (pid, pval))) wneuper@59265: | i => error ("ori_2itm: uncovered case of "^ itm_2str i) wneuper@59265: end neuper@37906: wneuper@59265: fun eq1 d (_, (d', _)) = (d = d') wneuper@59265: fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (d_in itm_) neuper@37906: neuper@37906: (* 'all' ts from ori; ts is the input; (ori carries rest of info) neuper@37906: 9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ? neuper@37906: pval: value for problem-environment _NOT_ checked for 'inter' -- neuper@37906: -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc neuper@37906: (as it has been done for input_icalhd+insert_ppc' in 11.03)*) neuper@37906: (*. is_input ori itms <=> neuper@37906: EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4) neuper@37906: (2) ori(ts) subset itm(ts) --- Err "already input" neuper@37906: (3) ori(ts) inter itm(ts) = empty --- new: ori(ts) neuper@37906: (4) -"- <> empty --- new: ori(ts) \\ inter .*) wneuper@59265: fun is_notyet_input ctxt (itms: itm list) all ((i, v, f, d, ts): ori) pbt = neuper@37906: case find_first (eq1 d) pbt of wneuper@59265: SOME (_, (_, pid)) => neuper@37906: (case find_first (eq3 f d) itms of neuper@52070: SOME (_,_,_,_,itm_) => wneuper@59265: let val ts' = inter op = (ts_in itm_) ts wneuper@59265: in wneuper@59265: if subset op = (ts, ts') wneuper@59265: then (((strs2str' o map (term_to_string' ctxt)) ts') ^ " already input", e_itm) (*2*) wneuper@59265: else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts)) (*3,4*) neuper@52070: end wneuper@59265: | NONE => ("", ori_2itm (Inc ((e_term, []), (pid, []))) pid all (i, v, f, d, ts))) (*1*) wneuper@59265: | NONE => ("", ori_2itm (Sup (d, ts)) e_term all (i, v, f, d, ts)) neuper@37906: bonzai@41949: fun test_types ctxt (d,ts) = neuper@37906: let wneuper@59265: val opt = (try comp_dts) (d, ts) neuper@37906: val msg = case opt of neuper@37926: SOME _ => "" neuper@52070: | NONE => (term_to_string' ctxt d ^ " " ^ wneuper@59265: (strs2str' o map (term_to_string' ctxt)) ts ^ " is illtyped") wneuper@59265: in msg end neuper@37906: wneuper@59265: (* is the input term t known in oris ? wneuper@59265: give feedback on all(?) strange input; wneuper@59265: return _all_ terms already input to this item (e.g. valuesFor a,b) *) bonzai@41949: fun is_known ctxt sel ori t = neuper@37906: let wneuper@59265: val _ = tracing ("RM is_known: t=" ^ term2str t) wneuper@59265: val ots = (distinct o flat o (map #5)) (ori:ori list) wneuper@59265: val oids = ((map (fst o dest_Free)) o distinct o flat o (map vars)) ots wneuper@59265: val (d, ts) = split_dts t wneuper@59265: val ids = map (fst o dest_Free) ((distinct o (flat o (map vars))) ts) wneuper@59265: in wneuper@59265: if (subtract op = oids ids) <> [] wneuper@59265: then (("identifiers "^(strs2str' (subtract op = oids ids)) ^ " not in example"), e_ori_, []) wneuper@59265: else wneuper@59265: if d = e_term wneuper@59265: then wneuper@59265: if not (subset op = (map typeless ts, map typeless ots)) wneuper@59265: then ("terms '" ^ (strs2str' o (map (term_to_string' ctxt))) ts ^ wneuper@59265: "' not in example (typeless)", e_ori_, []) wneuper@59265: else wneuper@59265: (case seek_orits ctxt sel ts ori of wneuper@59265: ("", ori_ as (_,_,_,d,ts), all) => wneuper@59265: (case test_types ctxt (d,ts) of wneuper@59265: "" => ("", ori_, all) wneuper@59265: | msg => (msg, e_ori_, [])) wneuper@59265: | (msg,_,_) => (msg, e_ori_, [])) wneuper@59265: else wneuper@59265: if member op = (map #4 ori) d wneuper@59265: then seek_oridts ctxt sel (d, ts) ori wneuper@59265: else (term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), []) wneuper@59265: end neuper@37906: wneuper@59265: neuper@37906: datatype additm = wneuper@59265: Add of itm (* return-value of appl_add *) wneuper@59265: | Err of string (* error-message *) neuper@37906: wneuper@59265: (* add an item to the model; check wrt. oris and pbt. wneuper@59265: in contrary to oris<>[] below, this part handles user-input wneuper@59265: extremely acceptive, i.e. accept input instead error-msg *) wneuper@59265: fun appl_add ctxt sel [] ppc pbt ct = wneuper@59265: let wneuper@59265: val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl) wneuper@59265: in wneuper@59265: case parseNEW ctxt ct of wneuper@59265: NONE => Add (i, [], false, sel, Syn ct) wneuper@59265: | SOME t => wneuper@59265: let val (d, ts) = split_dts t wneuper@59265: in wneuper@59265: if d = e_term wneuper@59269: then Add (i, [], false, sel, Mis (Specify.dsc_unknown, hd ts)) wneuper@59265: else wneuper@59265: (case find_first (eq1 d) pbt of wneuper@59265: NONE => Add (i, [], true, sel, Sup (d,ts)) wneuper@59265: | SOME (f, (_, id)) => wneuper@59265: let fun eq2 d (i, _, _, _, itm_) = d = (d_in itm_) andalso i <> 0 wneuper@59265: in case find_first (eq2 d) ppc of wneuper@59265: NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts))) wneuper@59265: | SOME (i', _, _, _, itm_) => wneuper@59265: if is_list_dsc d wneuper@59265: then wneuper@59265: let wneuper@59265: val in_itm = ts_in itm_ wneuper@59265: val ts' = union op = ts in_itm wneuper@59265: val i'' = if in_itm = [] then i else i' wneuper@59265: in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts')))end wneuper@59265: else Add (i', [], true, f, Cor ((d, ts), (id, pbl_ids' d ts))) wneuper@59265: end) wneuper@59265: end wneuper@59265: end wneuper@59265: | appl_add ctxt sel oris ppc pbt str = wneuper@59265: case parseNEW ctxt str of wneuper@59265: NONE => Err ("appl_add: syntax error in '" ^ str ^ "'") wneuper@59265: | SOME t => wneuper@59265: case is_known ctxt sel oris t of wneuper@59265: ("", ori', all) => wneuper@59265: (case is_notyet_input ctxt ppc all ori' pbt of wneuper@59265: ("", itm) => Add itm wneuper@59265: | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg)) wneuper@59265: | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg); neuper@37906: wneuper@59265: (* make oris from args of the stac SubProblem and from pbt. wneuper@59265: can this formal argument (of a model-pattern) be omitted in the arg-list wneuper@59265: of a SubProblem ? see calcelems.sml 'type met ' *) wneuper@59265: fun is_copy_named_idstr str = wneuper@59265: case (rev o Symbol.explode) str of wneuper@59265: "'" :: _ :: "'" :: _ => wneuper@59265: (tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " T"); true) wneuper@59265: | _ => wneuper@59265: (tracing ((strs2str o (rev o Symbol.explode)) "is_copy_named_idstr: " ^ str ^ " F"); false) wneuper@59265: fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t neuper@41973: wneuper@59265: (* should this formal argument (of a model-pattern) create a new identifier? *) wneuper@59265: fun is_copy_named_generating_idstr str = wneuper@59265: if is_copy_named_idstr str wneuper@59265: then wneuper@59265: case (rev o Symbol.explode) str of wneuper@59265: "'" :: "'" :: "'" :: _ => false wneuper@59265: | _ => true wneuper@59265: else false wneuper@59265: fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o free2str) t neuper@37906: wneuper@59265: (* split type-wrapper from scr-arg and build part of an ori; wneuper@59265: an type-error is reported immediately, raises an exn, wneuper@59265: subsequent handling of exn provides 2nd part of error message *) wneuper@59265: fun mtc thy ((str, (dsc, _)):pat) (ty $ var) = wneuper@59265: ((Thm.global_cterm_of thy (dsc $ var);(*type check*) wneuper@59265: SOME ((([1], str, dsc, (*[var]*) wneuper@59265: split_dts' (dsc, var))): preori)(*:ori without leading #*)) wneuper@59265: handle e as TYPE _ => wneuper@59265: (tracing (dashs 70 ^ "\n" wneuper@59265: ^ "*** ERROR while creating the items for the model of the ->problem\n" wneuper@59265: ^ "*** from the ->stac with ->typeconstructor in arglist:\n" wneuper@59265: ^ "*** item (->description ->value): " ^ term2str dsc ^ " " ^ term2str var ^ "\n" wneuper@59265: ^ "*** description: " ^ term_detail2str dsc wneuper@59265: ^ "*** value: " ^ term_detail2str var wneuper@59265: ^ "*** typeconstructor in script: " ^ term_detail2str ty wneuper@59265: ^ "*** checked by theory: " ^ theory2str thy ^ "\n" wneuper@59265: ^ "*** " ^ dots 66); wneuper@59265: writeln (PolyML.makestring e); wneuper@59265: reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*) wneuper@59265: NONE)) wneuper@59265: | mtc _ _ t = error ("mtc: uncovered case with" ^ term2str t) neuper@38010: wneuper@59265: (* match each pat of the model-pattern with an actual argument; wneuper@59265: precondition: copy-named vars are filtered out *) wneuper@59265: fun matc _ ([]:pat list) _ (oris:preori list) = oris wneuper@59265: | matc _ pbt [] _ = neuper@38015: (tracing (dashs 70); wneuper@59265: error ("actual arg(s) missing for '" ^ pats2str pbt ^ "' i.e. should be 'copy-named' by '*_._'")) wneuper@59265: | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris = neuper@37906: (*del?..*)if (is_copy_named_idstr o free2str) t then oris wneuper@59265: else(*..del?*) wneuper@59265: let val opt = mtc thy p a wneuper@59265: in wneuper@59265: case opt of wneuper@59265: SOME ori => matc thy pbt ags (oris @ [ori]) neuper@37926: | NONE => [](*WN050903 skipped by exn handled in match_ags*) wneuper@59265: end neuper@38011: neuper@38011: (* generate a new variable "x_i" name from a related given one "x" neuper@38011: by use of oris relating "v_v'i'" (is_copy_named!) to "v_v" neuper@38012: e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i), neuper@38012: but leave is_copy_named_generating as is, e.t. ss''' *) wneuper@59265: fun cpy_nam (pbt: pat list) (oris: preori list) (p as (field, (dsc, t)): pat) = neuper@37906: (if is_copy_named_generating p neuper@37906: then (*WN051014 kept strange old code ...*) wneuper@59265: let fun sel (_,_,d,ts) = comp_ts (d, ts) wneuper@59265: val cy' = (implode o (drop_last_n 3) o Symbol.explode o free2str) t wneuper@59265: val ext = (last_elem o drop_last o Symbol.explode o free2str) t wneuper@59265: val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*) wneuper@59265: val vals = map sel oris wneuper@59265: val cy_ext = (free2str o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext wneuper@59265: in ([1], field, dsc, [mk_free (type_of t) cy_ext]): preori end neuper@37906: else ([1], field, dsc, [t]) wneuper@59265: ) handle _ => error ("cpy_nam: for "^(term2str t)) neuper@37906: wneuper@59265: (* match the actual arguments of a SubProblem with a model-pattern neuper@37906: and create an ori list (in root-pbl created from formalization). neuper@37906: expects ags:pats = 1:1, while copy-named are filtered out of pats; neuper@38011: if no 1:1 the exn raised by matc/mtc and handled at call. wneuper@59265: copy-named pats are appended in order to get them into the model-items *) wneuper@59265: fun match_ags thy (pbt: pat list) ags = wneuper@59265: let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_) wneuper@59265: val pbt' = filter_out is_copy_named pbt wneuper@59265: val cy = filter is_copy_named pbt wneuper@59265: val oris' = matc thy pbt' ags [] wneuper@59265: val cy' = map (cpy_nam pbt' oris') cy wneuper@59269: val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *) wneuper@59265: in (map flattup ors): ori list end neuper@37906: wneuper@59265: (* report part of the error-msg which is not available in match_args *) neuper@37906: fun match_ags_msg pI stac ags = wneuper@59265: let wneuper@59269: val pats = (#ppc o Specify.get_pbt) pI wneuper@59265: val msg = (dots 70^"\n" wneuper@59265: ^ "*** problem "^strs2str pI ^ " has the ...\n" wneuper@59265: ^ "*** model-pattern "^pats2str pats ^ "\n" wneuper@59265: ^ "*** stac '"^term2str stac ^ "' has the ...\n" wneuper@59265: ^ "*** arg-list "^terms2str ags ^ "\n" wneuper@59265: ^ dashs 70) wneuper@59265: (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*) wneuper@59265: in tracing msg end neuper@37906: wneuper@59265: (* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *) neuper@37906: fun vars_of_pbl_ pbl_ = wneuper@59265: let wneuper@59265: fun var_of_pbl_ (_, (_, t)) = t wneuper@59265: in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end neuper@37906: fun vars_of_pbl_' pbl_ = wneuper@59265: let wneuper@59265: fun var_of_pbl_ (_, (_, t)) = t: term wneuper@59265: in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end neuper@37906: neuper@37906: fun overwrite_ppc thy itm ppc = neuper@37906: let wneuper@59265: fun repl _ (_, _, _, _, itm_) [] = wneuper@59265: error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^ " not found") wneuper@59265: | repl ppc' itm (p :: ppc) = wneuper@59265: if (#1 itm) = (#1 (p: itm)) wneuper@59265: then ppc' @ [itm] @ ppc wneuper@59265: else repl (ppc' @ [p]) itm ppc wneuper@59265: in repl [] itm ppc end neuper@37906: wneuper@59265: (* 10.3.00: insert the already compiled itm into model; neuper@37906: ev. filter_out untouched (in FE: (0,...)) item related to insert-item *) neuper@37906: fun insert_ppc thy itm ppc = wneuper@59265: let wneuper@59265: fun eq_untouched d ((0, _, _, _, itm_): itm) = (d = d_in itm_) wneuper@59265: | eq_untouched _ _ = false wneuper@59265: val ppc' = case seek_ppc (#1 itm) ppc of wneuper@59265: SOME _ => overwrite_ppc thy itm ppc (*itm updated in is_notyet_input WN.11.03*) wneuper@59265: | NONE => (ppc @ [itm]) wneuper@59265: in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end neuper@37906: wneuper@59265: fun eq_dsc ((_, _, _, _, itm_): itm, (_, _, _, _, iitm_): itm) = (d_in itm_ = d_in iitm_) neuper@37906: wneuper@59265: (* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03, wneuper@59265: handles superfluous items carelessly *) wneuper@59265: fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *) neuper@37906: wneuper@59265: (* output the headline to a ppc *) wneuper@59265: fun header p_ pI mI = wneuper@59271: case p_ of Pbl => Generate.Problem (if pI = e_pblID then [] else pI) wneuper@59271: | Met => Generate.Method mI wneuper@59265: | pos => error ("header called with "^ pos_2str pos) neuper@37906: wneuper@59265: fun specify_additem sel (ct, _) (p, Met) _ pt = wneuper@59265: let wneuper@59265: val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of wneuper@59265: (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...}) wneuper@59265: => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) wneuper@59265: | _ => error "specify_additem: uncovered case of get_obj I pt p" wneuper@59265: val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI wneuper@59265: val cpI = if pI = e_pblID then pI' else pI wneuper@59265: val cmI = if mI = e_metID then mI' else mI wneuper@59269: val {ppc, pre, prls, ...} = Specify.get_met cmI wneuper@59265: in wneuper@59265: case appl_add ctxt sel oris met ppc ct of wneuper@59265: Add itm => (*..union old input *) wneuper@59265: let wneuper@59265: val met' = insert_ppc thy itm met wneuper@59265: val arg = case sel of wneuper@59265: "#Given" => Add_Given' (ct, met') wneuper@59265: | "#Find" => Add_Find' (ct, met') wneuper@59265: | "#Relate"=> Add_Relation'(ct, met') wneuper@59265: | str => error ("specify_additem: uncovered case with " ^ str) wneuper@59271: val (p, Met, pt') = case Generate.generate1 thy arg (Uistate, ctxt) (p, Met) pt of wneuper@59265: ((p, Met), _, _, pt') => (p, Met, pt') wneuper@59265: | _ => error "specify_additem: uncovered case of generate1 (WARNING WHY ?)" wneuper@59265: val pre' = check_preconds thy prls pre met' wneuper@59265: val pb = foldl and_ (true, map fst pre') wneuper@59265: val (p_, nxt) = wneuper@59265: nxt_spec Met pb oris (dI',pI',mI') (pbl,met') wneuper@59269: ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI); wneuper@59265: in ((p, p_), ((p, p_), Uistate), wneuper@59271: Generate.PpcKF (Generate.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Safe, pt') wneuper@59265: end wneuper@59265: | Err msg => wneuper@59265: let wneuper@59265: val pre' = check_preconds thy prls pre met wneuper@59265: val pb = foldl and_ (true, map fst pre') wneuper@59265: val (p_, nxt) = wneuper@59265: nxt_spec Met pb oris (dI',pI',mI') (pbl,met) wneuper@59269: ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI); wneuper@59271: in ((p,p_), ((p,p_),Uistate), Generate.Error' msg, nxt, Safe,pt) end wneuper@59265: end wneuper@59265: | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt = neuper@41993: let wneuper@59265: val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of wneuper@59265: (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...}) wneuper@59265: => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) wneuper@59265: | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p" wneuper@59265: val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI wneuper@59265: val cpI = if pI = e_pblID then pI' else pI wneuper@59265: val cmI = if mI = e_metID then mI' else mI wneuper@59269: val {ppc, where_, prls, ...} = Specify.get_pbt cpI neuper@41993: in neuper@41993: case appl_add ctxt sel oris pbl ppc ct of wneuper@59265: Add itm => (*..union old input *) neuper@41993: let neuper@41993: val pbl' = insert_ppc thy itm pbl wneuper@59265: val arg = case sel of wneuper@59265: "#Given" => Add_Given' (ct, pbl') wneuper@59265: | "#Find" => Add_Find' (ct, pbl') wneuper@59265: | "#Relate"=> Add_Relation'(ct, pbl') wneuper@59265: | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str) wneuper@59271: val ((p, Pbl), _, _, pt') = Generate.generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*) neuper@41993: val pre = check_preconds thy prls where_ pbl' neuper@41993: val pb = foldl and_ (true, map fst pre) neuper@41993: val (p_, nxt) = wneuper@59269: nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI) wneuper@59265: val ppc = if p_= Pbl then pbl' else met wneuper@59265: in wneuper@59265: ((p, p_), ((p, p_), Uistate), wneuper@59271: Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Safe, pt') neuper@41993: end neuper@41993: | Err msg => neuper@41993: let neuper@41993: val pre = check_preconds thy prls where_ pbl neuper@41993: val pb = foldl and_ (true, map fst pre) neuper@41993: val (p_, nxt) = wneuper@59265: nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met) wneuper@59269: (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI) wneuper@59271: in ((p, p_), ((p, p_), Uistate), Generate.Error' msg, nxt, Safe,pt) end wneuper@59265: end neuper@37906: wneuper@59265: fun specify (Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ = neuper@41994: let (* either """"""""""""""" all empty or complete *) wneuper@59265: val thy = assoc_thy dI' neuper@41994: val (oris, ctxt) = neuper@41994: if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*) neuper@41994: then ([], e_ctxt) wneuper@59269: else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy wneuper@59279: val (pt, _) = cappend_problem e_ctree [] (e_istate, ctxt) (fmz, spec') neuper@42092: (oris, (dI',pI',mI'), e_term) neuper@41994: val pt = update_ctxt pt [] ctxt wneuper@59265: val (pbl, pre) = ([], []) neuper@41994: in neuper@41994: case mI' of neuper@41994: ["no_met"] => neuper@41994: (([], Pbl), (([], Pbl), Uistate), wneuper@59271: Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre), neuper@41994: Refine_Tacitly pI', Safe, pt) neuper@41994: | _ => neuper@41994: (([], Pbl), (([], Pbl), Uistate), wneuper@59271: Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre), neuper@41994: Model_Problem, Safe, pt) wneuper@59265: end wneuper@59265: (* ONLY for STARTING modeling phase *) wneuper@59265: | specify (Model_Problem' (_, pbl, met)) (pos as (p, p_)) _ pt = wneuper@59265: let wneuper@59265: val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of wneuper@59265: PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} => wneuper@59265: (oris, dI',pI',mI', dI, ctxt) wneuper@59265: | _ => error "specify (Model_Problem': uncovered case get_obj" wneuper@59265: val thy' = if dI = e_domID then dI' else dI wneuper@59265: val thy = assoc_thy thy' wneuper@59269: val {ppc, prls, where_, ...} = Specify.get_pbt pI' wneuper@59265: val pre = check_preconds thy prls where_ pbl wneuper@59265: val pb = foldl and_ (true, map fst pre) wneuper@59265: val ((p, _), _, _, pt) = wneuper@59271: Generate.generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt wneuper@59265: val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met) wneuper@59269: (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI'); wneuper@59265: in wneuper@59265: ((p, Pbl), ((p, p_), Uistate), wneuper@59271: Generate.PpcKF (Generate.Problem pI', Specify.itms2itemppc (assoc_thy dI') pbl pre), wneuper@59265: nxt, Safe, pt) wneuper@59265: end wneuper@59265: (* called only if no_met is specified *) wneuper@59265: | specify (Refine_Tacitly' (pI, pIre, _, _, _)) (pos as (p, _)) _ pt = neuper@41980: let wneuper@59265: val (dI', ctxt) = case get_obj I pt p of wneuper@59265: PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt) wneuper@59265: | _ => error "specify (Refine_Tacitly': uncovered case get_obj" wneuper@59269: val {met, thy,...} = Specify.get_pbt pIre wneuper@59265: val (domID, metID) = (string_of_thy thy, if length met = 0 then e_metID else hd met) wneuper@59265: val ((p,_), _, _, pt) = wneuper@59271: Generate.generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt wneuper@59265: val (pbl, pre, _) = ([], [], false) neuper@41980: in ((p, Pbl), (pos, Uistate), wneuper@59271: Generate.PpcKF (Generate.Problem pIre, Specify.itms2itemppc (assoc_thy dI') pbl pre), neuper@41980: Model_Problem, Safe, pt) neuper@41980: end wneuper@59265: | specify (Refine_Problem' rfd) pos _ pt = neuper@42005: let neuper@42005: val ctxt = get_ctxt pt pos wneuper@59265: val (pos, _, _, pt) = wneuper@59271: Generate.generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt wneuper@59265: in wneuper@59271: (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Generate.RefinedKF rfd, Model_Problem, Safe, pt) neuper@41980: end neuper@41994: (*WN110515 initialise ctxt again from itms and add preconds*) wneuper@59265: | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt = neuper@41994: let wneuper@59265: val (oris, dI', pI', mI', dI, mI, ctxt, met) = case get_obj I pt p of wneuper@59265: PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} => wneuper@59265: (oris, dI', pI', mI', dI, mI, ctxt, met) wneuper@59265: | _ => error "specify (Specify_Problem': uncovered case get_obj" neuper@41994: val thy = assoc_thy dI wneuper@59265: val (p, Pbl, pt) = wneuper@59271: case Generate.generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of wneuper@59265: ((p, Pbl), _, _, pt) => (p, Pbl, pt) wneuper@59265: | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)" wneuper@59265: val dI'' = assoc_thy (if dI=e_domID then dI' else dI) wneuper@59265: val mI'' = if mI=e_metID then mI' else mI wneuper@59269: val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o Specify.get_pbt) pI, wneuper@59269: (#ppc o Specify.get_met) mI'') (dI, pI, mI); wneuper@59265: in wneuper@59265: ((p,Pbl), (pos,Uistate), wneuper@59271: Generate.PpcKF (Generate.Problem pI, Specify.itms2itemppc dI'' itms pre), wneuper@59265: nxt, Safe, pt) neuper@41994: end neuper@41994: (*WN110515 initialise ctxt again from itms and add preconds*) wneuper@59265: | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) _ pt = neuper@41994: let wneuper@59265: val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of wneuper@59265: PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} => wneuper@59265: (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) wneuper@59265: | _ => error "specify (Specify_Problem': uncovered case get_obj" wneuper@59269: val {ppc,pre,prls,...} = Specify.get_met mID neuper@41994: val thy = assoc_thy dI wneuper@59269: val oris = Specify.add_field' thy ppc oris wneuper@59265: val dI'' = if dI=e_domID then dI' else dI wneuper@59265: val pI'' = if pI = e_pblID then pI' else pI wneuper@59265: val met = if met = [] then pbl else met wneuper@59269: val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris neuper@41994: val (pos, _, _, pt) = wneuper@59271: Generate.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt wneuper@59265: val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms) wneuper@59269: ((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID) wneuper@59265: in wneuper@59265: (pos, (pos,Uistate), wneuper@59271: Generate.PpcKF (Generate.Method mID, Specify.itms2itemppc (assoc_thy dI'') itms pre'), wneuper@59265: nxt, Safe, pt) neuper@41994: end neuper@37906: | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt neuper@37906: | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt neuper@37906: | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt wneuper@59265: | specify (Specify_Theory' domID) (pos as (p,p_)) _ pt = neuper@41994: let neuper@41994: val p_ = case p_ of Met => Met | _ => Pbl wneuper@59265: val thy = assoc_thy domID wneuper@59265: val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of wneuper@59265: PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} => wneuper@59265: (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) wneuper@59265: | _ => error "specify (Specify_Theory': uncovered case get_obj" wneuper@59265: val mppc = case p_ of Met => met | _ => pbl wneuper@59265: val cpI = if pI = e_pblID then pI' else pI wneuper@59269: val {prls = per, ppc, where_ = pwh, ...} = Specify.get_pbt cpI wneuper@59265: val cmI = if mI = e_metID then mI' else mI wneuper@59269: val {prls = mer, ppc = mpc, pre= mwh, ...} = Specify.get_met cmI wneuper@59265: val pre = case p_ of wneuper@59265: Met => (check_preconds thy mer mwh met) wneuper@59265: | _ => (check_preconds thy per pwh pbl) neuper@41994: val pb = foldl and_ (true, map fst pre) neuper@41994: in neuper@41994: if domID = dI neuper@41994: then wneuper@59265: let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI) wneuper@59265: in wneuper@59265: ((p, p_), (pos, Uistate), wneuper@59271: Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre), wneuper@59265: nxt, Safe, pt) neuper@41994: end neuper@41994: else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*) neuper@41994: let wneuper@59271: val ((p, p_), _, _, pt) = Generate.generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt wneuper@59265: val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI) wneuper@59265: in wneuper@59265: ((p,p_), (pos,Uistate), wneuper@59271: Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre), wneuper@59265: nxt, Safe, pt) neuper@41994: end neuper@41994: end wneuper@59265: | specify m' _ _ _ = error ("specify: not impl. for " ^ tac_2str m') neuper@37906: neuper@41994: (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...} neuper@41994: -- for input from scratch*) neuper@38051: fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) = wneuper@59265: let wneuper@59265: val (oris, dI', pI', dI, pI, pbl, ctxt) = case get_obj I pt p of wneuper@59265: PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} => wneuper@59265: (oris, dI', pI', dI, pI, pbl, ctxt) wneuper@59265: | _ => error "specify (Specify_Theory': uncovered case get_obj" wneuper@59265: val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI; wneuper@59265: val cpI = if pI = e_pblID then pI' else pI; wneuper@59265: in wneuper@59269: case appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of wneuper@59265: Add itm (*..union old input *) => wneuper@59265: let wneuper@59265: val pbl' = insert_ppc thy itm pbl wneuper@59265: val (tac, tac_) = case sel of wneuper@59265: "#Given" => (Add_Given ct, Add_Given' (ct, pbl')) wneuper@59265: | "#Find" => (Add_Find ct, Add_Find' (ct, pbl')) wneuper@59265: | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl')) wneuper@59265: | sel => error ("nxt_specif_additem: uncovered case of" ^ sel) wneuper@59271: val (p, Pbl, c, pt') = case Generate.generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of wneuper@59265: ((p, Pbl), c, _, pt') => (p, Pbl, c, pt') wneuper@59265: | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)" wneuper@59265: in wneuper@59265: ([(tac, tac_, ((p, Pbl), (Uistate, ctxt)))], c, (pt', (p, Pbl))) : calcstate' wneuper@59265: end wneuper@59265: | Err msg => (*TODO.WN03 pass error-msgs to the frontend.. wneuper@59265: FIXME ..and dont abuse a tactic for that purpose*) wneuper@59265: ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg), wneuper@59265: (e_pos', (e_istate, e_ctxt)))], [], ptp) wneuper@59265: end wneuper@59265: | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) = wneuper@59265: let wneuper@59265: val (oris, dI', mI', dI, mI, met, ctxt) = case get_obj I pt p of wneuper@59265: PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} => wneuper@59265: (oris, dI', mI', dI, mI, met, ctxt) wneuper@59265: | _ => error "nxt_specif_additem Met: uncovered case get_obj" wneuper@59265: val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI; wneuper@59265: val cmI = if mI = e_metID then mI' else mI; wneuper@59265: in wneuper@59269: case appl_add ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of wneuper@59265: Add itm (*..union old input *) => wneuper@59265: let wneuper@59265: val met' = insert_ppc thy itm met; wneuper@59265: val (tac,tac_) = case sel of wneuper@59265: "#Given" => (Add_Given ct, Add_Given' (ct, met')) wneuper@59265: | "#Find" => (Add_Find ct, Add_Find' (ct, met')) wneuper@59265: | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met')) wneuper@59265: | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel) wneuper@59271: val (p, Met, c, pt') = case Generate.generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of wneuper@59265: ((p, Met), c, _, pt') => (p, Met, c, pt') wneuper@59265: | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)" wneuper@59265: in wneuper@59265: ([(tac, tac_, ((p, Met), (Uistate, ctxt)))], c, (pt', (p, Met))) wneuper@59265: end wneuper@59265: | Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*) wneuper@59265: end wneuper@59265: | nxt_specif_additem _ _ (_, p) = error ("nxt_specif_additem not impl. for" ^ pos'2str p) neuper@41994: wneuper@59265: fun ori2Coritm (pbt : pat list) ((i, v, f, d, ts) : ori) = wneuper@59265: ((i, v, true, f, Cor ((d,ts),((snd o snd o the o (find_first (eq1 d))) pbt,ts))) : itm) wneuper@59265: handle _ => ((i, v, true, f, Cor ((d, ts), (d, ts))) : itm) wneuper@59265: (*dsc in oris, but not in pbl pat list: keep this dsc*) neuper@37906: wneuper@59265: (* filter out oris which have same description in itms *) neuper@37906: fun filter_outs oris [] = oris neuper@37906: | filter_outs oris (i::itms) = wneuper@59265: let wneuper@59265: val ors = filter_out ((curry op = ((d_in o #5) (i:itm))) o (#4 : ori -> term)) oris wneuper@59265: in wneuper@59265: filter_outs ors itms wneuper@59265: end neuper@37906: wneuper@59265: (* filter oris which are in pbt, too *) neuper@37906: fun filter_pbt oris pbt = wneuper@59265: let wneuper@59265: val dscs = map (fst o snd) pbt wneuper@59265: in wneuper@59265: filter ((member op= dscs) o (#4 : ori -> term)) oris wneuper@59265: end neuper@37906: wneuper@59265: (* combine itms from pbl + met and complete them wrt. pbt *) wneuper@59265: (* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*) wneuper@59265: fun complete_metitms (oris : ori list) (pits : itm list) (mits: itm list) met = wneuper@59265: let wneuper@59265: val vat = max_vt pits; wneuper@59265: val itms = pits @ (filter ((member_swap op = vat) o (#2 : itm -> int list)) mits) wneuper@59265: val ors = filter ((member_swap op= vat) o (#2 : ori -> int list)) oris wneuper@59265: val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*) wneuper@59265: in wneuper@59265: itms @ (map (ori2Coritm met) os) wneuper@59265: end neuper@37906: wneuper@59265: (* complete model and guard of a calc-head *) wneuper@59265: fun complete_mod_ (oris, mpc, ppc, probl) = wneuper@59265: let wneuper@59265: val pits = filter_out ((curry op= false) o (#3 : itm -> bool)) probl wneuper@59265: val vat = if probl = [] then 1 else max_vt probl wneuper@59265: val pors = filter ((member_swap op = vat) o (#2 : ori -> int list)) oris wneuper@59265: val pors = filter_outs pors pits (*which are in pbl already*) wneuper@59265: val pors = (filter_pbt pors ppc) (*which are in pbt, too*) wneuper@59265: val pits = pits @ (map (ori2Coritm ppc) pors) wneuper@59265: val mits = complete_metitms oris pits [] mpc wneuper@59265: in (pits, mits) end neuper@37906: wneuper@59265: fun some_spec ((odI, opI, omI) : spec) ((dI, pI, mI) : spec) = wneuper@59265: (if dI = e_domID then odI else dI, wneuper@59265: if pI = e_pblID then opI else pI, wneuper@59265: if mI = e_metID then omI else mI) : spec neuper@37906: wneuper@59279: (* find a next applicable tac (for calcstate) and update ctree wneuper@59265: (for ev. finding several more tacs due to hide) *) wneuper@59265: (* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *) wneuper@59265: (* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *) wneuper@59265: (* WN.24.10.03 fun nxt_solv = ...................................?? *) wneuper@59265: fun nxt_specif (tac as Model_Problem) (pt, pos as (p, _)) = neuper@41982: let wneuper@59265: val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of wneuper@59265: PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt) wneuper@59265: | _ => error "nxt_specif Model_Problem; uncovered case get_obj" neuper@41982: val (dI, pI, mI) = some_spec ospec spec neuper@41982: val thy = assoc_thy dI wneuper@59269: val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *) wneuper@59269: val {cas, ppc, ...} = Specify.get_pbt pI wneuper@59271: val pbl = Generate.init_pbl ppc (* fill in descriptions *) neuper@41982: (*----------------if you think, this should be done by the Dialog neuper@41982: in the java front-end, search there for WN060225-modelProblem----*) wneuper@59265: val (pbl, met) = case cas of wneuper@59265: NONE => (pbl, []) wneuper@59265: | _ => complete_mod_ (oris, mpc, ppc, probl) neuper@41982: (*----------------------------------------------------------------*) neuper@41982: val tac_ = Model_Problem' (pI, pbl, met) wneuper@59271: val (pos,c,_,pt) = Generate.generate1 thy tac_ (Uistate, ctxt) pos pt wneuper@59265: in ([(tac, tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)) : calcstate' end neuper@37906: | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp neuper@37906: | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp neuper@37906: | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp neuper@41975: (*. called only if no_met is specified .*) neuper@37906: | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) = wneuper@59265: let wneuper@59265: val (oris, dI, ctxt) = case get_obj I pt p of wneuper@59265: (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt) wneuper@59265: | _ => error "nxt_specif Refine_Tacitly: uncovered case get_obj" wneuper@59269: val opt = Specify.refine_ori oris pI wneuper@59265: in wneuper@59265: case opt of wneuper@59265: SOME pI' => wneuper@59265: let wneuper@59269: val {met, ...} = Specify.get_pbt pI' wneuper@59265: (*val pt = update_pbl pt p pbl ..done by Model_Problem*) wneuper@59265: val mI = if length met = 0 then e_metID else hd met wneuper@59265: val thy = assoc_thy dI wneuper@59265: val (pos, c, _, pt) = wneuper@59271: Generate.generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt wneuper@59265: in wneuper@59265: ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]), wneuper@59265: (pos, (Uistate, e_ctxt)))], c, (pt,pos)) wneuper@59265: end wneuper@59265: | NONE => ([], [], ptp) wneuper@59265: end neuper@37906: | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) = wneuper@59265: let wneuper@59265: val (dI, dI', probl, ctxt) = case get_obj I pt p of wneuper@59265: PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} => wneuper@59265: (dI, dI', probl, ctxt) wneuper@59265: | _ => error "nxt_specif Refine_Problem: uncovered case get_obj" wneuper@59265: val thy = if dI' = e_domID then dI else dI' wneuper@59265: in wneuper@59269: case Specify.refine_pbl (assoc_thy thy) pI probl of wneuper@59265: NONE => ([], [], ptp) wneuper@59265: | SOME rfd => wneuper@59265: let wneuper@59271: val (pos,c,_,pt) = Generate.generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt wneuper@59265: in wneuper@59265: ([(Refine_Problem pI, Refine_Problem' rfd, (pos, (Uistate, e_ctxt)))], c, (pt,pos)) wneuper@59265: end wneuper@59265: end neuper@37906: | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) = wneuper@59265: let wneuper@59265: val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of wneuper@59265: PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...} => wneuper@59265: (oris, dI, dI', pI', probl, ctxt) wneuper@59265: | _ => error "" wneuper@59265: val thy = assoc_thy (if dI' = e_domID then dI else dI'); wneuper@59269: val {ppc,where_,prls,...} = Specify.get_pbt pI wneuper@59265: val pbl = wneuper@59265: if pI' = e_pblID andalso pI = e_pblID wneuper@59271: then (false, (Generate.init_pbl ppc, [])) wneuper@59269: else Specify.match_itms_oris thy probl (ppc,where_,prls) oris wneuper@59265: (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*) wneuper@59271: val (c, pt) = case Generate.generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of wneuper@59265: ((_, Pbl), c, _, pt) => (c, pt) wneuper@59265: | _ => error "" wneuper@59265: in wneuper@59265: ([(Specify_Problem pI, Specify_Problem' (pI, pbl), (pos, (Uistate, e_ctxt)))], c, (pt,pos)) wneuper@59265: end wneuper@59265: (* transfers oris (not required in pbl) to met-model for script-env wneuper@59265: FIXME.WN.8.03: application of several mIDs to SAME model? *) wneuper@59265: | nxt_specif (Specify_Method mID) (pt, pos as (p,_)) = wneuper@59265: let wneuper@59265: val (oris, pbl, dI, met, ctxt) = case get_obj I pt p of wneuper@59265: PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...} wneuper@59265: => (oris, pbl, dI, met, ctxt) wneuper@59265: | _ => error "nxt_specif Specify_Method: uncovered case get_obj" wneuper@59269: val {ppc,pre,prls,...} = Specify.get_met mID wneuper@59265: val thy = assoc_thy dI wneuper@59269: val oris = Specify.add_field' thy ppc oris wneuper@59265: val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *) wneuper@59269: val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris wneuper@59265: val (pos, c, _, pt) = wneuper@59271: Generate.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt wneuper@59265: in wneuper@59265: ([(Specify_Method mID, Specify_Method' (mID, oris, itms), (pos, (Uistate, e_ctxt)))], c, (pt, pos)) wneuper@59265: end wneuper@59265: | nxt_specif (Specify_Theory dI) (pt, pos as (_, Pbl)) = wneuper@59265: let wneuper@59265: val ctxt = get_ctxt pt pos wneuper@59265: val (pos, c, _, pt) = wneuper@59271: Generate.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt wneuper@59265: in (*FIXXXME: check if pbl can still be parsed*) wneuper@59265: ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c, wneuper@59265: (pt, pos)) wneuper@59265: end wneuper@59265: | nxt_specif (Specify_Theory dI) (pt, pos as (_, Met)) = wneuper@59265: let wneuper@59265: val ctxt = get_ctxt pt pos wneuper@59271: val (pos, c, _, pt) = Generate.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt wneuper@59265: in (*FIXXXME: check if met can still be parsed*) wneuper@59265: ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c, (pt, pos)) wneuper@59265: end wneuper@59265: | nxt_specif m' _ = error ("nxt_specif: not impl. for "^tac2str m') neuper@37906: neuper@41982: (* get the values from oris; handle the term list w.r.t. penv *) neuper@37906: fun vals_of_oris oris = wneuper@59265: ((map (mkval' o (#5 : ori -> term list))) o wneuper@59265: (filter ((member_swap op= 1) o (#2 : ori -> int list)))) oris neuper@37906: neuper@38056: (* create a calc-tree with oris via an cas.refined pbl *) neuper@38056: fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) = wneuper@59265: if pI <> [] wneuper@59265: then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *) wneuper@59265: let wneuper@59269: val {cas, met, ppc, thy, ...} = Specify.get_pbt pI wneuper@59265: val dI = if dI = "" then theory2theory' thy else dI wneuper@59265: val mI = if mI = [] then hd met else mI wneuper@59265: val hdl = case cas of NONE => pblterm dI pI | SOME t => t wneuper@59279: val (pt,_) = cappend_problem e_ctree [] (Uistate, e_ctxt) ([], (dI, pI, mI)) wneuper@59265: ([], (dI,pI,mI), hdl) wneuper@59265: val pt = update_spec pt [] (dI, pI, mI) wneuper@59271: val pits = Generate.init_pbl' ppc wneuper@59265: val pt = update_pbl pt [] pits wneuper@59265: in ((pt, ([] , Pbl)), []) : calcstate end wneuper@59265: else wneuper@59265: if mI <> [] wneuper@59265: then (* from met-browser *) neuper@41976: let wneuper@59269: val {ppc, ...} = Specify.get_met mI wneuper@59265: val dI = if dI = "" then "Isac" else dI wneuper@59265: val (pt, _) = wneuper@59279: cappend_problem e_ctree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*)) wneuper@59265: val pt = update_spec pt [] (dI, pI, mI) wneuper@59271: val mits = Generate.init_pbl' ppc wneuper@59265: val pt = update_met pt [] mits wneuper@59265: in ((pt, ([], Met)), []) end wneuper@59265: else (* new example, pepare for interactive modeling *) wneuper@59265: let wneuper@59265: val (pt, _) = wneuper@59279: cappend_problem e_ctree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term) wneuper@59265: in ((pt, ([], Pbl)), []) end wneuper@59265: | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) = wneuper@59265: let (* both """"""""""""""""""""""""" either empty or complete *) wneuper@59265: val thy = assoc_thy dI wneuper@59265: val (pI, (pors, pctxt), mI) = wneuper@59265: if mI = ["no_met"] wneuper@59265: then wneuper@59265: let wneuper@59269: val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy; wneuper@59269: val pI' = Specify.refine_ori' pors pI; wneuper@59265: in (pI', (pors(*refinement over models with diff.precond only*), pctxt), wneuper@59269: (hd o #met o Specify.get_pbt) pI') wneuper@59265: end wneuper@59269: else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI) wneuper@59269: val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*) wneuper@59265: val dI = theory2theory' (maxthy thy thy') wneuper@59265: val hdl = case cas of wneuper@59265: NONE => pblterm dI pI wneuper@59265: | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t wneuper@59265: val (pt, _) = wneuper@59279: cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl) wneuper@59265: val pt = update_ctxt pt [] pctxt wneuper@59265: in wneuper@59265: ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate wneuper@59265: end neuper@41976: wneuper@59265: fun get_spec_form m ((p, p_) : pos') pt = wneuper@59265: let val (_, _, f, _, _, _) = specify m (p, p_) [] pt wneuper@59265: in f end neuper@37906: wneuper@59265: (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy wneuper@59265: (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *) neuper@37934: fun tag_form thy (formal, given) = neuper@52070: (let neuper@52070: val gf = (head_of given) $ formal; wneuper@59184: val _ = Thm.global_cterm_of thy gf neuper@52070: in gf end) neuper@52070: handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^ wneuper@59265: " .. " ^ term_to_string''' thy formal ^ " ..types do not match") neuper@38053: neuper@37906: fun chktyp thy (n, fs, gs) = neuper@52070: ((writeln o (term_to_string''' thy) o (nth n)) fs; neuper@52070: (writeln o (term_to_string''' thy) o (nth n)) gs; wneuper@59265: tag_form thy (nth n fs, nth n gs)) wneuper@59265: fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs) neuper@37906: neuper@37906: (* check pbltypes, announces one failure a time *) neuper@37930: fun chk_vars ctppc = wneuper@59265: let wneuper@59269: val {Given = gi, Where = wh, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc vars ctppc) wneuper@59265: val chked = subtract op = gi wh wneuper@59265: in wneuper@59265: if chked <> [] then ("wh\\gi", chked) wneuper@59265: else wneuper@59265: let val chked = subtract op = (union op = gi fi) re wneuper@59265: in wneuper@59265: if chked <> [] wneuper@59265: then ("re\\(gi union fi)", chked) wneuper@59265: else ("ok", []) wneuper@59265: end wneuper@59265: end neuper@37906: neuper@37906: (* check a new pbltype: variables (Free) unbound by given, find*) neuper@37906: fun unbound_ppc ctppc = wneuper@59265: let wneuper@59269: val {Given = gi, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc vars ctppc) wneuper@59265: in wneuper@59265: distinct (subtract op = (union op = gi fi) re) wneuper@59265: end neuper@37906: wneuper@59265: (* f, a binary operator, is nested right associative *) neuper@37906: fun foldr1 f xs = neuper@37906: let wneuper@59265: fun fld _ (x :: []) = x wneuper@59265: | fld f (x :: x' :: []) = f (x', x) wneuper@59265: | fld f (x :: x' :: xs) = f (fld f (x' :: xs), x) wneuper@59265: | fld _ _ = error "foldr1 uncovered definition" wneuper@59265: in ((fld f) o rev) xs end neuper@37906: neuper@37906: (* f, a binary operator, is nested leftassociative *) wneuper@59265: fun foldl1 _ (x :: []) = x wneuper@59265: | foldl1 f (x :: x' :: []) = f (x, x') wneuper@59265: | foldl1 f (x :: x' :: xs) = f (x, foldl1 f (x' :: xs)) wneuper@59265: | foldl1 _ _ = error "foldl1 uncovered definition" neuper@37906: neuper@37906: (* called only once, if a Subproblem has been located in the script*) wneuper@59265: fun nxt_model_pbl (Subproblem' ((_, pblID, metID), _, _, _, _, _)) ptp = wneuper@59265: (case metID of wneuper@59265: ["no_met"] => (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp) wneuper@59265: | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp)) wneuper@59265: (*all stored in tac_ itms^^^^^^^^^^*) wneuper@59265: | nxt_model_pbl tac_ _ = error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_) neuper@37906: wneuper@59265: (* fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml *) wneuper@59265: fun eq4 v (_, vts, _, _, _) = member op = vts v wneuper@59265: fun eq5 (_, _, _, _, itm_) (_, _, _, d, _) = d_in itm_ = d neuper@37906: wneuper@59265: (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris wneuper@59265: + met from fmz; assumes pos on PblObj, meth = [] *) wneuper@59265: fun complete_mod (pt, pos as (p, p_) : pos') = wneuper@59265: let wneuper@59265: val _ = if p_ <> Pbl wneuper@59265: then error ("###complete_mod: only impl.for Pbl, called with " ^ pos'2str pos) wneuper@59265: else () wneuper@59265: val (oris, ospec, probl, spec) = case get_obj I pt p of wneuper@59265: PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec) wneuper@59265: | _ => error "complete_mod: unvered case get_obj" wneuper@59265: val (_, pI, mI) = some_spec ospec spec wneuper@59269: val mpc = (#ppc o Specify.get_met) mI wneuper@59269: val ppc = (#ppc o Specify.get_pbt) pI wneuper@59265: val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl) wneuper@59265: val pt = update_pblppc pt p pits wneuper@59265: val pt = update_metppc pt p mits wneuper@59265: in (pt, (p, Met) : pos') end neuper@37906: neuper@37906: (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz); neuper@37906: oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*) wneuper@59265: fun all_modspec (pt, (p, _) : pos') = wneuper@59265: let wneuper@59265: val (pors, dI, pI, mI) = case get_obj I pt p of wneuper@59265: PblObj {origin = (pors, (dI, pI, mI), _), ...} => (pors, dI, pI, mI) wneuper@59265: | _ => error "all_modspec: uncovered case get_obj" wneuper@59269: val {ppc, ...} = Specify.get_met mI wneuper@59265: val (_, vals) = oris2fmz_vals pors neuper@48761: val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global neuper@42092: |> declare_constraints' vals wneuper@59265: val pt = update_pblppc pt p (map (ori2Coritm ppc) pors) wneuper@59265: val pt = update_metppc pt p (map (ori2Coritm ppc) pors) (*WN110716 = _pblppc ?!?*) wneuper@59265: val pt = update_spec pt p (dI, pI, mI) neuper@42092: val pt = update_ctxt pt p ctxt wneuper@59265: in wneuper@59265: (pt, (p, Met) : pos') wneuper@59265: end neuper@37906: wneuper@59265: (* WN0312: use in nxt_spec, too ? what about variants ??? *) wneuper@59265: fun is_complete_mod_ ([] : itm list) = false wneuper@59265: | is_complete_mod_ itms = foldl and_ (true, (map #3 itms)) neuper@41976: wneuper@59265: fun is_complete_mod (pt, pos as (p, Pbl) : pos') = wneuper@59265: if (is_pblobj o (get_obj I pt)) p wneuper@59265: then (is_complete_mod_ o (get_obj g_pbl pt)) p wneuper@59265: else error ("is_complete_mod: called by PrfObj at "^pos'2str pos) neuper@37906: | is_complete_mod (pt, pos as (p, Met)) = wneuper@59265: if (is_pblobj o (get_obj I pt)) p wneuper@59265: then (is_complete_mod_ o (get_obj g_met pt)) p wneuper@59265: else error ("is_complete_mod: called by PrfObj at "^pos'2str pos) neuper@37906: | is_complete_mod (_, pos) = wneuper@59265: error ("is_complete_mod called by " ^ pos'2str pos ^ " (should be Pbl or Met)") neuper@37906: wneuper@59265: (* have (thy, pbl, met) _all_ been specified explicitly ? *) wneuper@59265: fun is_complete_spec (pt, pos as (p, _) : pos') = wneuper@59265: if (not o is_pblobj o (get_obj I pt)) p wneuper@59265: then error ("is_complete_spec: called by PrfObj at "^pos'2str pos) wneuper@59265: else wneuper@59265: let val (dI,pI,mI) = get_obj g_spec pt p wneuper@59265: in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end neuper@37906: wneuper@59265: (* complete empty items in specification from origin (pbl, met ev.refined); wneuper@59265: assumes 'is_complete_mod' *) wneuper@59265: fun complete_spec (pt, pos as (p, _) : pos') = wneuper@59265: let wneuper@59265: val (ospec, spec) = case get_obj I pt p of wneuper@59265: PblObj {origin = (_,ospec,_), spec,...} => (ospec, spec) wneuper@59265: | _ => error "complete_spec: uncovered case get_obj" wneuper@59265: val pt = update_spec pt p (some_spec ospec spec) wneuper@59265: in wneuper@59265: (pt, pos) wneuper@59265: end neuper@37906: wneuper@59265: fun is_complete_modspec ptp = is_complete_mod ptp andalso is_complete_spec ptp neuper@37906: wneuper@59265: fun pt_model (PblObj {meth, spec, origin = (_, spec', hdl), ...}) Met = wneuper@59265: let wneuper@59265: val (_, _, metID) = get_somespec' spec spec' wneuper@59265: val pre = if metID = e_metID then [] wneuper@59265: else wneuper@59265: let wneuper@59269: val {prls, pre= where_, ...} = Specify.get_met metID wneuper@59265: val pre = check_preconds' prls where_ meth 0 wneuper@59265: in pre end wneuper@59265: val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre)) wneuper@59265: in wneuper@59265: ModSpec (allcorrect, Met, hdl, meth, pre, spec) wneuper@59265: end wneuper@59265: | pt_model (PblObj {probl, spec, origin = (_, spec', hdl), ...}) _(*Frm,Pbl*) = wneuper@59265: let wneuper@59265: val (_, pI, _) = get_somespec' spec spec' wneuper@59265: val pre = if pI = e_pblID then [] wneuper@59265: else wneuper@59265: let wneuper@59269: val {prls, where_, ...} = Specify.get_pbt pI wneuper@59265: val pre = check_preconds' prls where_ probl 0 wneuper@59265: in pre end wneuper@59265: val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre)) wneuper@59265: in wneuper@59265: ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) wneuper@59265: end wneuper@59265: | pt_model _ _ = error "pt_model: uncovered definition" neuper@37906: wneuper@59265: fun pt_form (PrfObj {form, ...}) = Form form wneuper@59265: | pt_form (PblObj {probl, spec, origin = (_, spec', _), ...}) = wneuper@59265: let wneuper@59265: val (dI, pI, _) = get_somespec' spec spec' wneuper@59269: val {cas, ...} = Specify.get_pbt pI wneuper@59265: in case cas of wneuper@59265: NONE => Form (pblterm dI pI) wneuper@59265: | SOME t => Form (subst_atomic (mk_env probl) t) wneuper@59265: end neuper@37906: wneuper@59265: (* pt_extract returns neuper@37906: # the formula at pos neuper@37906: # the tactic applied to this formula neuper@37906: # the list of assumptions generated at this formula neuper@37906: (by application of another tac to the preceding formula !) wneuper@59265: pos is assumed to come from the frontend, ie. generated by moveDown. wneuper@59265: Notes: cannot be in ctree.sml, because ModSpec has to be calculated. wneuper@59265: TODO 110417 get assumptions from ctxt !? wneuper@59265: *) wneuper@59265: fun pt_extract (pt, ([], Res)) = wneuper@59265: (* WN120512: returns Check_Postcondition WRONGLY see --- build fun is_exactly_equal *) wneuper@59265: let wneuper@59265: val (f, asm) = get_obj g_result pt [] wneuper@59265: in (Form f, NONE, asm) end neuper@37906: | pt_extract (pt,(p,Res)) = wneuper@59265: let wneuper@59265: val (f, asm) = get_obj g_result pt p wneuper@59265: val tac = wneuper@59265: if last_onlev pt p wneuper@59265: then wneuper@59265: if is_pblobj' pt (lev_up p) neuper@42437: then wneuper@59265: let wneuper@59265: val pI = case get_obj I pt (lev_up p) of wneuper@59265: PblObj{spec = (_, pI, _), ...} => pI wneuper@59265: | _ => error "pt_extract last_onlev: uncovered case get_obj" wneuper@59265: in if pI = e_pblID then NONE else SOME (Check_Postcond pI) end wneuper@59265: else SOME End_Trans (* WN0502 TODO for other branches *) wneuper@59265: else wneuper@59265: let val p' = lev_on p wneuper@59265: in wneuper@59265: if is_pblobj' pt p' wneuper@59265: then wneuper@59265: let wneuper@59265: val (dI ,pI) = case get_obj I pt p' of wneuper@59265: PblObj{origin = (_, (dI, pI, _), _), ...} => (dI ,pI) wneuper@59265: | _ => error "pt_extract \last_onlev: uncovered case get_obj" wneuper@59265: in SOME (Subproblem (dI, pI)) end wneuper@59265: else wneuper@59265: if f = get_obj g_form pt p' wneuper@59265: then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*) wneuper@59265: else SOME (Take (term2str (get_obj g_form pt p'))) wneuper@59265: end wneuper@59265: in (Form f, tac, asm) end wneuper@59265: | pt_extract (pt, (p,p_(*Frm,Pbl*))) = neuper@42437: let neuper@42437: val ppobj = get_obj I pt p neuper@42437: val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p neuper@42437: val tac = g_tac ppobj wneuper@59265: in (f, SOME tac, []) end neuper@37906: wneuper@59265: (** get the formula from a ctree-node: wneuper@59265: take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj) wneuper@59265: take res from all other PrfObj's wneuper@59265: Designed for interSteps, outcommented 04 in favour of calcChangedEvent **) wneuper@59265: fun formres p (Nd (PblObj {origin = (_, _, h), result = (r, _), ...}, _)) = wneuper@59265: [("headline", (p, Frm), h), ("stepform", (p, Res), r)] wneuper@59265: | formres p (Nd (PrfObj {form, result = (r, _), ...}, _)) = wneuper@59265: [("stepform", (p, Frm), form), ("stepform", (p, Res), r)] wneuper@59265: | formres _ _ = error "formres: uncovered definition" wneuper@59265: fun form p (Nd (PrfObj {result = (r, _), ...}, _)) = wneuper@59265: [("stepform", (p, Res), r)] wneuper@59265: | form _ _ = error "form: uncovered definition" neuper@37906: wneuper@59265: (* assumes to take whole level, in particular hd -- for use in interSteps *) wneuper@59265: fun get_formress fs _ [] = flat fs neuper@37906: | get_formress fs p (nd::nds) = neuper@37906: (* start with 'form+res' and continue with trying 'res' only*) neuper@37906: get_forms (fs @ [formres p nd]) (lev_on p) nds wneuper@59265: and get_forms fs _ [] = flat fs neuper@37906: | get_forms fs p (nd::nds) = neuper@37906: if is_pblnd nd neuper@37906: (* start again with 'form+res' ///ugly repeat with Check_elementwise neuper@37906: then get_formress (fs @ [formres p nd]) (lev_on p) nds *) neuper@37906: then get_forms (fs @ [formres p nd]) (lev_on p) nds neuper@37906: (* continue with trying 'res' only*) neuper@37906: else get_forms (fs @ [form p nd]) (lev_on p) nds; neuper@37906: wneuper@59279: (** get an 'interval' 'from' 'to' of formulae from a ctree **) wneuper@59265: (* WN0401 this functionality belongs to ctree.sml *) wneuper@59265: fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2 wneuper@59265: | eq_pos' (p1, Res) (p2, Res) = p1 = p2 wneuper@59265: | eq_pos' (p1, Pbl) (p2, p2_) = wneuper@59265: p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false) wneuper@59265: | eq_pos' (p1, Met) (p2, p2_) = wneuper@59265: p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false) neuper@37906: | eq_pos' _ _ = false; neuper@37906: wneuper@59265: (* get an 'interval' from the ctree; 'interval' is w.r.t. the neuper@37906: total ordering Position#compareTo(Position p) in the java-code neuper@37906: val get_interval = fn neuper@37906: : pos' -> : from is "move_up 1st-element" to return neuper@37906: pos' -> : to the last element to be returned; from < to neuper@37906: int -> : level: 0 gets the flattest sub-tree possible neuper@37906: >999 gets the deepest sub-tree possible wneuper@59279: ctree -> : neuper@37906: (pos' * : of the formula neuper@37906: Term.term) : the formula wneuper@59265: list *) neuper@37906: fun get_interval from to level pt = neuper@42432: let wneuper@59265: fun get_inter c (from : pos') (to : pos') lev pt = wneuper@59265: if eq_pos' from to orelse from = ([], Res) neuper@42432: then wneuper@59265: let val (f, _, _) = pt_extract (pt, from) wneuper@59265: in case f of wneuper@59265: ModSpec (_,_,headline, _, _, _) => c @ [(from, headline)] wneuper@59265: | Form t => c @ [(from, t)] neuper@42432: end neuper@37906: else neuper@42432: if lev < lev_of from neuper@42432: then (get_inter c (move_dn [] pt from) to lev pt) neuper@42432: handle (PTREE _(*from move_dn too far*)) => c neuper@42432: else neuper@42432: let wneuper@59265: val (f, _, _) = pt_extract (pt, from) neuper@42432: val term = case f of neuper@42432: ModSpec (_,_,headline,_,_,_) => headline neuper@42432: | Form t => t neuper@42432: in (get_inter (c @ [(from, term)]) (move_dn [] pt from) to lev pt) neuper@42432: handle (PTREE _(*from move_dn too far*)) => c @ [(from, term)] neuper@42432: end wneuper@59265: in get_inter [] from to level pt end neuper@37906: wneuper@59265: (* for tests *) wneuper@59265: fun posform2str (pos : pos', form) = wneuper@59265: "(" ^ pos'2str pos ^ ", " ^ wneuper@59265: (case form of Form f => term2str f | ModSpec c => term2str (#3 c(*the headline*))) ^ wneuper@59265: ")" wneuper@59265: fun posforms2str pfs = wneuper@59265: (strs2str' o (map (curry op ^ "\n")) o (map posform2str)) pfs wneuper@59265: fun posterm2str (pos:pos', t) = "(" ^ pos'2str pos ^ ", " ^ term2str t ^ ")" wneuper@59265: fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posterm2str)) pfs neuper@37906: wneuper@59265: (* WN050225 omits the last step, if pt is incomplete *) wneuper@59265: fun show_pt pt = tracing (posterms2str (get_interval ([], Frm) ([], Res) 99999 pt)) neuper@37906: wneuper@59265: (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *) wneuper@59265: fun get_ocalhd (pt, (p, Pbl) : pos') = wneuper@59265: let wneuper@59265: val (ospec, hdf', spec, probl) = case get_obj I pt p of wneuper@59265: PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl) wneuper@59265: | _ => error "get_ocalhd Pbl: uncovered case get_obj" wneuper@59269: val {prls, where_, ...} = Specify.get_pbt (#2 (some_spec ospec spec)) wneuper@59265: val pre = check_preconds (assoc_thy"Isac") prls where_ probl wneuper@59265: in wneuper@59265: (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec) : ocalhd wneuper@59265: end wneuper@59265: | get_ocalhd (pt, (p, Met)) = wneuper@59265: let wneuper@59265: val (ospec, hdf', spec, meth) = case get_obj I pt p of wneuper@59265: PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth) wneuper@59265: | _ => error "get_ocalhd Met: uncovered case get_obj" wneuper@59269: val {prls, pre, ...} = Specify.get_met (#3 (some_spec ospec spec)) wneuper@59265: val pre = check_preconds (assoc_thy"Isac") prls pre meth wneuper@59265: in wneuper@59265: (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec) wneuper@59265: end wneuper@59265: | get_ocalhd _ = error "get_ocalhd: uncovered definition" neuper@37906: wneuper@59265: (* at the activeFormula set the Model, the Guard and the Specification wneuper@59265: to empty and return a CalcHead; wneuper@59265: the 'origin' remains (for reconstructing all that) *) wneuper@59265: fun reset_calchead (pt, (p,_) : pos') = wneuper@59265: let wneuper@59265: val () = case get_obj I pt p of wneuper@59265: PblObj _ => () wneuper@59265: | _ => error "reset_calchead: uncovered case get_obj" wneuper@59265: val pt = update_pbl pt p [] wneuper@59265: val pt = update_met pt p [] wneuper@59265: val pt = update_spec pt p e_spec wneuper@59265: in (pt, (p, Pbl) : pos') end neuper@37906: wneuper@59265: end