neuper@37906: (* Specify-phase: specifying and modeling a problem or a subproblem. The neuper@37906: most important types are declared in mstools.sml. neuper@37906: author: Walther Neuper neuper@37906: 991122 neuper@37906: (c) due to copyright terms neuper@37906: neuper@37906: use"ME/calchead.sml"; neuper@37906: use"calchead.sml"; neuper@37934: 12345678901234567890123456789012345678901234567890123456789012345678901234567890 neuper@37934: 10 20 30 40 50 60 70 80 neuper@37906: *) neuper@37906: neuper@37906: (* TODO interne Funktionen aus sig entfernen *) neuper@37906: signature CALC_HEAD = neuper@37906: sig neuper@37906: datatype additm = Add of SpecifyTools.itm | Err of string neuper@37906: val all_dsc_in : SpecifyTools.itm_ list -> Term.term list neuper@37906: val all_modspec : ptree * pos' -> ptree * pos' neuper@37906: datatype appl = Appl of tac_ | Notappl of string neuper@37906: val appl_add : neuper@37931: theory -> neuper@37906: string -> neuper@37906: SpecifyTools.ori list -> neuper@37906: SpecifyTools.itm list -> neuper@37906: (string * (Term.term * Term.term)) list -> cterm' -> additm neuper@37906: type calcstate neuper@37906: type calcstate' neuper@37934: val chk_vars : term ppc -> string * Term.term list neuper@37906: val chktyp : neuper@37934: theory -> int * term list * term list -> term neuper@37906: val chktyps : neuper@37934: theory -> term list * term list -> term list neuper@37906: val complete_metitms : neuper@37906: SpecifyTools.ori list -> neuper@37906: SpecifyTools.itm list -> neuper@37906: SpecifyTools.itm list -> pat list -> SpecifyTools.itm list neuper@37906: val complete_mod_ : ori list * pat list * pat list * itm list -> neuper@37906: itm list * itm list neuper@37906: val complete_mod : ptree * pos' -> ptree * (pos * pos_) neuper@37906: val complete_spec : ptree * pos' -> ptree * pos' neuper@37906: val cpy_nam : neuper@37906: pat list -> preori list -> pat -> preori neuper@37906: val e_calcstate : calcstate neuper@37906: val e_calcstate' : calcstate' neuper@37906: val eq1 : ''a -> 'b * (''a * 'c) -> bool neuper@37906: val eq3 : neuper@37906: ''a -> Term.term -> 'b * 'c * 'd * ''a * SpecifyTools.itm_ -> bool neuper@37906: val eq4 : ''a -> 'b * ''a list * 'c * 'd * 'e -> bool neuper@37906: val eq5 : neuper@37906: 'a * 'b * 'c * 'd * SpecifyTools.itm_ -> neuper@37906: 'e * 'f * 'g * Term.term * 'h -> bool neuper@37906: val eq_dsc : SpecifyTools.itm * SpecifyTools.itm -> bool neuper@37906: val eq_pos' : ''a * pos_ -> ''a * pos_ -> bool neuper@37931: val f_mout : theory -> mout -> Term.term neuper@37906: val filter_outs : neuper@37906: SpecifyTools.ori list -> neuper@37906: SpecifyTools.itm list -> SpecifyTools.ori list neuper@37906: val filter_pbt : neuper@37906: SpecifyTools.ori list -> neuper@37906: ('a * (Term.term * 'b)) list -> SpecifyTools.ori list neuper@37906: val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a neuper@37906: val foldr1 : ('a * 'a -> 'a) -> 'a list -> 'a neuper@37906: val form : 'a -> ptree -> (string * ('a * pos_) * Term.term) list neuper@37906: val formres : 'a -> ptree -> (string * ('a * pos_) * Term.term) list neuper@37906: val gen_ins' : ('a * 'a -> bool) -> 'a * 'a list -> 'a list neuper@37906: val get_formress : neuper@37906: (string * (pos * pos_) * Term.term) list list -> neuper@37906: pos -> ptree list -> (string * (pos * pos_) * Term.term) list neuper@37906: val get_forms : neuper@37906: (string * (pos * pos_) * Term.term) list list -> neuper@37906: posel list -> ptree list -> (string * (pos * pos_) * Term.term) list neuper@37906: val get_interval : pos' -> pos' -> int -> ptree -> (pos' * term) list neuper@37906: val get_ocalhd : ptree * pos' -> ocalhd neuper@37906: val get_spec_form : tac_ -> pos' -> ptree -> mout neuper@37906: val geti_ct : neuper@37931: theory -> neuper@37906: SpecifyTools.ori -> SpecifyTools.itm -> string * cterm' neuper@37931: val getr_ct : theory -> SpecifyTools.ori -> string * cterm' neuper@37906: val has_list_type : Term.term -> bool neuper@37906: val header : pos_ -> pblID -> metID -> pblmet neuper@37906: val insert_ppc : neuper@37931: theory -> neuper@37906: int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ -> neuper@37906: SpecifyTools.itm list -> SpecifyTools.itm list neuper@37906: val insert_ppc' : neuper@37906: SpecifyTools.itm -> SpecifyTools.itm list -> SpecifyTools.itm list neuper@37906: val is_complete_mod : ptree * pos' -> bool neuper@37906: val is_complete_mod_ : SpecifyTools.itm list -> bool neuper@37906: val is_complete_modspec : ptree * pos' -> bool neuper@37906: val is_complete_spec : ptree * pos' -> bool neuper@37906: val is_copy_named : 'a * ('b * Term.term) -> bool neuper@37906: val is_copy_named_idstr : string -> bool neuper@37906: val is_error : SpecifyTools.itm_ -> bool neuper@37906: val is_field_correct : ''a -> ''b -> (''a * ''b list) list -> bool neuper@37906: val is_known : neuper@37931: theory -> neuper@37906: string -> neuper@37906: SpecifyTools.ori list -> neuper@37906: Term.term -> string * SpecifyTools.ori * Term.term list neuper@37906: val is_list_type : Term.typ -> bool neuper@37906: val is_notyet_input : neuper@37931: theory -> neuper@37906: SpecifyTools.itm list -> neuper@37906: Term.term list -> neuper@37906: SpecifyTools.ori -> neuper@37906: ('a * (Term.term * Term.term)) list -> string * SpecifyTools.itm neuper@37906: val is_parsed : SpecifyTools.itm_ -> bool neuper@37906: val is_untouched : SpecifyTools.itm -> bool neuper@37906: val matc : neuper@37931: theory -> neuper@37906: pat list -> neuper@37906: Term.term list -> neuper@37906: (int list * string * Term.term * Term.term list) list -> neuper@37906: (int list * string * Term.term * Term.term list) list neuper@37906: val match_ags : neuper@37931: theory -> pat list -> Term.term list -> SpecifyTools.ori list neuper@37906: val maxl : int list -> int neuper@37906: val match_ags_msg : string list -> Term.term -> Term.term list -> unit neuper@37906: val memI : ''a list -> ''a -> bool neuper@37906: val mk_additem : string -> cterm' -> tac neuper@37931: val mk_delete : theory -> string -> SpecifyTools.itm_ -> tac neuper@37906: val mtc : neuper@37931: theory -> pat -> Term.term -> SpecifyTools.preori option neuper@37906: val nxt_add : neuper@37931: theory -> neuper@37906: SpecifyTools.ori list -> neuper@37906: (string * (Term.term * 'a)) list -> neuper@37931: SpecifyTools.itm list -> (string * cterm') option neuper@37906: val nxt_model_pbl : tac_ -> ptree * (int list * pos_) -> tac_ neuper@37906: val nxt_spec : neuper@37906: pos_ -> neuper@37906: bool -> neuper@37906: SpecifyTools.ori list -> neuper@37906: spec -> neuper@37906: SpecifyTools.itm list * SpecifyTools.itm list -> neuper@37906: (string * (Term.term * 'a)) list * (string * (Term.term * 'b)) list -> neuper@37906: spec -> pos_ * tac neuper@37906: val nxt_specif : tac -> ptree * (int list * pos_) -> calcstate' neuper@37906: val nxt_specif_additem : neuper@37906: string -> cterm' -> ptree * (int list * pos_) -> calcstate' neuper@37906: val nxt_specify_init_calc : fmz -> calcstate neuper@37906: val ocalhd_complete : neuper@37906: SpecifyTools.itm list -> neuper@37906: (bool * Term.term) list -> domID * pblID * metID -> bool neuper@37906: val ori2Coritm : neuper@37906: pat list -> ori -> itm neuper@37906: val ori_2itm : neuper@37906: 'a -> neuper@37906: SpecifyTools.itm_ -> neuper@37906: Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm neuper@37906: val overwrite_ppc : neuper@37931: theory -> neuper@37906: int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ -> neuper@37906: SpecifyTools.itm list -> neuper@37906: (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list neuper@37906: val parse_ok : SpecifyTools.itm_ list -> bool neuper@37906: val posform2str : pos' * ptform -> string neuper@37906: val posforms2str : (pos' * ptform) list -> string neuper@37906: val posterms2str : (pos' * term) list -> string (*tests only*) neuper@37906: val ppc135list : 'a SpecifyTools.ppc -> 'a list neuper@37906: val ppc2list : 'a SpecifyTools.ppc -> 'a list neuper@37906: val pt_extract : neuper@37906: ptree * (int list * pos_) -> neuper@37931: ptform * tac option * Term.term list neuper@37906: val pt_form : ppobj -> ptform neuper@37906: val pt_model : ppobj -> pos_ -> ptform neuper@37906: val reset_calchead : ptree * pos' -> ptree * pos' neuper@37906: val seek_oridts : neuper@37931: theory -> neuper@37906: string -> neuper@37906: Term.term * Term.term list -> neuper@37906: (int * SpecifyTools.vats * string * Term.term * Term.term list) list neuper@37906: -> string * SpecifyTools.ori * Term.term list neuper@37906: val seek_orits : neuper@37931: theory -> neuper@37906: string -> neuper@37906: Term.term list -> neuper@37906: (int * SpecifyTools.vats * string * Term.term * Term.term list) list neuper@37906: -> string * SpecifyTools.ori * Term.term list neuper@37906: val seek_ppc : neuper@37931: int -> SpecifyTools.itm list -> SpecifyTools.itm option neuper@37906: val show_pt : ptree -> unit neuper@37906: val some_spec : spec -> spec -> spec neuper@37906: val specify : neuper@37906: tac_ -> neuper@37906: pos' -> neuper@37906: cid -> neuper@37906: ptree -> neuper@37906: (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac * neuper@37906: safe * ptree neuper@37906: val specify_additem : neuper@37906: string -> neuper@37906: cterm' * 'a -> neuper@37906: int list * pos_ -> neuper@37906: 'b -> neuper@37906: ptree -> neuper@37906: (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree neuper@37934: val tag_form : theory -> term * term -> term neuper@37931: val test_types : theory -> Term.term * Term.term list -> string neuper@37906: val typeless : Term.term -> Term.term neuper@37934: val unbound_ppc : term SpecifyTools.ppc -> Term.term list neuper@37906: val vals_of_oris : SpecifyTools.ori list -> Term.term list neuper@37906: val variants_in : Term.term list -> int neuper@37906: val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list neuper@37906: val vars_of_pbl_' : ('a * ('b * Term.term)) list -> Term.term list neuper@37906: end neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*---------------------------------------------------------------------*) neuper@37906: structure CalcHead (**): CALC_HEAD(**) = neuper@37906: neuper@37906: struct neuper@37906: (*---------------------------------------------------------------------*) neuper@37906: neuper@37906: (* datatypes *) neuper@37906: neuper@37906: (*.the state wich is stored after each step of calculation; it contains neuper@37906: the calc-state and a list of [tac,istate](="tacis") to be applied. 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@37906: because the tacis hold enought information for efficiently rebuilding neuper@37906: this state just by "fun generate ".*) neuper@37906: type calcstate = neuper@37906: (ptree * pos') * (*the calc-state to which the tacis could be applied*) neuper@37906: (taci list); (*ev. several (hidden) steps; neuper@37906: in REVERSE order: first tac_ to apply is last_elem*) neuper@37906: val e_calcstate = ((EmptyPtree, e_pos'), [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' = neuper@37906: taci list * (*cas. several (hidden) steps; neuper@37906: in REVERSE order: first tac_ to apply is last_elem*) neuper@37906: pos' list * (*a "continuous" sequence of pos', neuper@37906: deleted by application of taci list*) neuper@37906: (ptree * pos'); (*the calc-state resulting from the application of tacis*) neuper@37906: val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate'; neuper@37906: neuper@37906: (*FIXXXME.WN020430 intermediate hack for fun ass_up*) neuper@37906: fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f neuper@37906: | f_mout thy _ = raise error "f_mout: not called with formula"; neuper@37906: neuper@37906: neuper@37906: (*.is the calchead complete ?.*) neuper@37906: fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) = neuper@37906: foldl and_ (true, map #3 its) andalso neuper@37906: foldl and_ (true, map #1 pre) andalso neuper@37906: dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID; neuper@37906: neuper@37906: neuper@37906: (* make a term 'typeless' for comparing with another 'typeless' term; neuper@37906: 'type-less' usually is illtyped *) neuper@37906: fun typeless (Const(s,_)) = (Const(s,e_type)) neuper@37906: | typeless (Free(s,_)) = (Free(s,e_type)) neuper@37906: | typeless (Var(n,_)) = (Var(n,e_type)) neuper@37906: | typeless (Bound i) = (Bound i) neuper@37906: | typeless (Abs(s,_,t)) = Abs(s,e_type, typeless t) neuper@37906: | typeless (t1 $ t2) = (typeless t1) $ (typeless t2); neuper@37906: (* neuper@37926: > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)"; neuper@37906: > val (_,t1) = split_dsc_t hs (term_of ct); neuper@37926: > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2"; neuper@37906: > val (_,t2) = split_dsc_t hs (term_of ct); neuper@37906: > typeless t1 = typeless t2; neuper@37906: val it = true : bool neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*.to an input (d,ts) find the according ori and insert the ts.*) neuper@37906: (*WN.11.03: + dont take first inter<>[]*) neuper@37906: fun seek_oridts thy sel (d,ts) [] = neuper@37934: ("'"^(Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts)))^ neuper@37906: "' not found (typed)", (0,[],sel,d,ts):ori, []) neuper@37906: (* val (id,vat,sel',d',ts')::oris = ori; neuper@37906: val (id,vat,sel',d',ts') = ori; neuper@37906: *) neuper@37906: | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) = neuper@37934: if sel = sel' andalso d=d' andalso (inter op = ts ts') <> [] neuper@37934: then if sel = sel' neuper@37934: then ("", neuper@37934: (id,vat,sel,d, inter op = ts ts'):ori, neuper@37934: ts') neuper@37934: else ((Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts))) neuper@37934: ^ " not for " ^ sel, neuper@37934: e_ori_, neuper@37934: []) neuper@37906: else seek_oridts thy sel (d,ts) oris; neuper@37906: neuper@37906: (*.to an input (_,ts) find the according ori and insert the ts.*) neuper@37906: fun seek_orits thy sel ts [] = neuper@37906: ("'"^ neuper@37934: (strs2str (map (Syntax.string_of_term (thy2ctxt thy)) ts))^ neuper@37906: "' not found (typed)", e_ori_, []) neuper@37906: | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) = neuper@37934: if sel = sel' andalso (inter op = ts ts') <> [] neuper@37906: then if sel = sel' neuper@37934: then ("", neuper@37934: (id,vat,sel,d, inter op = ts ts'):ori, neuper@37934: ts') neuper@37934: else (((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts) neuper@37934: ^ " not for "^sel, neuper@37934: e_ori_, neuper@37934: []) neuper@37906: else seek_orits thy sel ts oris; neuper@37906: (* false neuper@37906: > val ((id,vat,sel',d,ts')::(ori':ori)) = ori; neuper@37906: > seek_orits thy sel ts [(id,vat,sel',d,ts')]; neuper@37906: uncaught exception TYPE neuper@37906: > seek_orits thy sel ts []; neuper@37906: uncaught exception TYPE neuper@37906: *) neuper@37906: neuper@37906: (*find_first item with #1 equal to id*) neuper@37926: fun seek_ppc id [] = NONE neuper@37906: | seek_ppc id (p::(ppc:itm list)) = neuper@37926: if id = #1 p then SOME p else seek_ppc id ppc; neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*---------------------------------------------(3) nach ptyps.sml 23.3.02*) neuper@37906: neuper@37906: neuper@37906: datatype appl = Appl of tac_ | Notappl of string; neuper@37906: neuper@37906: fun ppc2list ({Given=gis,Where=whs,Find=fis, neuper@37906: With=wis,Relate=res}: 'a ppc) = neuper@37906: gis @ whs @ fis @ wis @ res; neuper@37906: fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) = neuper@37906: gis @ fis @ res; neuper@37906: neuper@37906: neuper@37906: 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 = neuper@37906: let fun eq(x,y) = head_of x = head_of y; neuper@37906: fun cnt eq [] y n = ([n],[]) neuper@37906: | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1) neuper@37906: else ([n], x::xs); neuper@37906: fun coll eq xs [] = xs neuper@37906: | coll eq xs (y::ys) = neuper@37906: let val (n,ys') = cnt eq (y::ys) y 0; neuper@37906: in if ys' = [] then xs @ n else coll eq (xs @ n) ys' end; neuper@37934: val vts = subtract op = [1] (distinct (coll eq [] ts)); neuper@37906: in case vts of [] => 1 | [n] => n neuper@37906: | _ => error "different variants in formalization" end; neuper@37906: (* neuper@37906: > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0; neuper@37906: val it = ([3],[4,5,5,5,5,5]) : int list * int list neuper@37906: > coll (op=) [] [1,2,2,2,4,5,5,5,5,5]; neuper@37906: val it = [1,3,1,5] : int list neuper@37906: *) neuper@37906: neuper@37906: fun is_list_type (Type("List.list",_)) = true neuper@37906: | is_list_type _ = false; neuper@37906: (* fun destr (Type(str,sort)) = (str,sort); neuper@37926: > val (SOME ct) = parse thy "lll::real list"; neuper@37906: > val ty = (#T o rep_cterm) ct; neuper@37906: > is_list_type ty; neuper@37906: val it = true : bool neuper@37906: > destr ty; neuper@37906: val it = ("List.list",["RealDef.real"]) : string * typ list neuper@37906: > atomty ((#t o rep_cterm) ct); neuper@37906: *** ------------- neuper@37906: *** Free ( lll, real list) neuper@37906: val it = () : unit neuper@37906: neuper@37926: > val (SOME ct) = parse thy "[lll::real]"; neuper@37906: > val ty = (#T o rep_cterm) ct; neuper@37906: > is_list_type ty; neuper@37906: val it = true : bool neuper@37906: > destr ty; neuper@37906: val it = ("List.list",["'a"]) : string * typ list neuper@37906: > atomty ((#t o rep_cterm) ct); neuper@37906: *** ------------- neuper@37906: *** Const ( List.list.Cons, [real, real list] => real list) neuper@37906: *** Free ( lll, real) neuper@37906: *** Const ( List.list.Nil, real list) neuper@37906: neuper@37926: > val (SOME ct) = parse thy "lll"; neuper@37906: > val ty = (#T o rep_cterm) ct; neuper@37906: > is_list_type ty; neuper@37906: val it = false : bool *) neuper@37906: neuper@37906: neuper@37906: fun has_list_type (Free(_,T)) = is_list_type T neuper@37906: | has_list_type _ = false; neuper@37906: (* neuper@37926: > val (SOME ct) = parse thy "lll::real list"; neuper@37906: > has_list_type (term_of ct); neuper@37906: val it = true : bool neuper@37926: > val (SOME ct) = parse thy "[lll::real]"; neuper@37906: > has_list_type (term_of ct); neuper@37906: val it = false : bool *) neuper@37906: neuper@37906: fun is_parsed (Syn _) = false neuper@37906: | is_parsed _ = true; neuper@37906: fun parse_ok its = foldl and_ (true, map is_parsed its); neuper@37906: neuper@37906: fun all_dsc_in itm_s = neuper@37906: let neuper@37906: fun d_in (Cor ((d,_),_)) = [d] neuper@37906: | d_in (Syn c) = [] neuper@37906: | d_in (Typ c) = [] neuper@37906: | d_in (Inc ((d,_),_)) = [d] neuper@37906: | d_in (Sup (d,_)) = [d] neuper@37906: | d_in (Mis (d,_)) = [d]; neuper@37906: in (flat o (map d_in)) itm_s end; neuper@37906: neuper@37906: (* 30.1.00 --- neuper@37906: fun is_Syn (Syn _) = true neuper@37906: | is_Syn (Typ _) = true neuper@37906: | is_Syn _ = false; neuper@37906: --- *) neuper@37906: fun is_error (Cor (_,ts)) = false neuper@37906: | is_error (Sup (_,ts)) = false neuper@37906: | is_error (Inc (_,ts)) = false neuper@37906: | is_error (Mis (_,ts)) = false neuper@37906: | is_error _ = true; neuper@37906: neuper@37906: (* 30.1.00 --- neuper@37906: fun ct_in (Syn (c)) = c neuper@37906: | ct_in (Typ (c)) = c neuper@37906: | ct_in _ = raise error "ct_in called for Cor .. Sup"; neuper@37906: --- *) neuper@37906: neuper@37906: (*#############################################################*) neuper@37906: (*#############################################################*) neuper@37906: (* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *) neuper@37906: neuper@37906: neuper@37906: (* testdaten besorgen: neuper@37906: use"test-coil-kernel.sml"; neuper@37906: val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) = neuper@37906: get_obj I pt p; neuper@37906: *) neuper@37906: neuper@37906: (* given oris, ppc, neuper@37906: variant V: oris union ppc => int, id ID: oris union ppc => int neuper@37906: neuper@37906: ppc is_complete == neuper@37906: EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i & complete i neuper@37906: neuper@37906: and neuper@37906: @vt = max sum(i : ppc) V i neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: neuper@37906: (* neuper@37906: > ((vts_cnt (vts_in itms))) itms; neuper@37906: neuper@37906: neuper@37906: neuper@37906: ---^^--test 10.3. neuper@37906: > val vts = vts_in itms; neuper@37906: val vts = [1,2,3] : int list neuper@37906: > val nvts = vts_cnt vts itms; neuper@37906: val nvts = [(1,6),(2,5),(3,7)] : (int * int) list neuper@37906: > val mx = max2 nvts; neuper@37906: val mx = (3,7) : int * int neuper@37906: > val v = max_vt itms; neuper@37906: val v = 3 : int neuper@37906: -------------------------- neuper@37906: > neuper@37906: *) neuper@37906: neuper@37906: (*.get the first term in ts from ori.*) neuper@37906: (* val (_,_,fd,d,ts) = hd miss; neuper@37906: *) neuper@37906: fun getr_ct thy ((_,_,fd,d,ts):ori) = neuper@37934: (fd, ((Syntax.string_of_term (thy2ctxt thy)) o neuper@37934: (comp_dts thy)) (d,[hd ts]):cterm'); neuper@37906: (* val t = comp_dts thy (d,[hd ts]); neuper@37906: *) neuper@37906: neuper@37906: (* get a term from ori, notyet input in itm *) neuper@37906: fun geti_ct thy ((_,_,_,d,ts):ori) ((_,_,_,fd,itm_):itm) = neuper@37934: (fd, ((Syntax.string_of_term (thy2ctxt thy)) o (comp_dts thy)) neuper@37934: (d, subtract op = (ts_in itm_) ts):cterm'); neuper@37906: (* test-maximum.sml fmy <> [], Init_Proof ... neuper@37906: val (_,_,_,d,ts) = ori; val (_,_,_,fd,itm_) = hd icl; neuper@37906: val d' $ ts' = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]"; neuper@37906: atomty d; neuper@37906: atomty d'; neuper@37906: atomty (hd ts); neuper@37906: atomty ts'; neuper@37938: cterm_of thy (d $ (hd ts)); neuper@37938: cterm_of thy (d' $ ts'); neuper@37906: neuper@37906: comp_dts thy (d,ts); neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: (* in FE dsc, not dat: this is in itms ...*) neuper@37906: fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true neuper@37906: | is_untouched _ = false; neuper@37906: neuper@37906: neuper@37906: (* select an item in oris, notyet input in itms neuper@37906: (precondition: in itms are only Cor, Sup, Inc) *) neuper@37936: local infix mem; neuper@37934: fun x mem [] = false neuper@37934: | x mem (y :: ys) = x = y orelse x mem ys; neuper@37934: in neuper@37906: fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*) neuper@37906: let neuper@37906: fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0; neuper@37906: fun is_elem itms (f,(d,t)) = neuper@37906: case find_first (test_d d) itms of neuper@37926: SOME _ => true | NONE => false; neuper@37906: in case filter_out (is_elem itms) pbt of neuper@37906: (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt; neuper@37906: *) neuper@37906: (f,(d,_))::itms => neuper@37934: SOME (f:string, ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts thy) (d,[]):cterm') neuper@37926: | _ => NONE end neuper@37906: neuper@37906: (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl); neuper@37906: *) neuper@37906: | nxt_add thy oris pbt itms = neuper@37906: let neuper@37906: fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori)) neuper@37906: andalso (#3 ori) <>"#undef"; neuper@37906: fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm)); neuper@37906: fun test_id ids r = curry (op mem) (#1 (r:ori)) ids; neuper@37906: (* val itm = hd icl; val (_,_,_,d,ts) = v6; neuper@37906: *) neuper@37906: fun test_subset (itm:itm) ((_,_,_,d,ts):ori) = neuper@37934: (d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts); neuper@37906: fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false neuper@37906: | false_and_not_Sup (i,v,false,f, _) = true neuper@37906: | false_and_not_Sup _ = false; neuper@37906: neuper@37906: val v = if itms = [] then 1 else max_vt itms; neuper@37906: val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*) neuper@37906: val vits = if v = 0 then itms (*because of dsc without dat*) neuper@37906: else filter (testi_vt v) itms; (*itms..vat*) neuper@37906: val icl = filter false_and_not_Sup vits; (* incomplete *) neuper@37906: in if icl = [] neuper@37906: then case filter_out (test_id (map #1 vits)) vors of neuper@37926: [] => NONE neuper@37906: (* val miss = filter_out (test_id (map #1 vits)) vors; neuper@37906: *) neuper@37926: | miss => SOME (getr_ct thy (hd miss)) neuper@37906: else neuper@37906: case find_first (test_subset (hd icl)) vors of neuper@37926: (* val SOME ori = find_first (test_subset (hd icl)) vors; neuper@37906: *) neuper@37926: NONE => raise error "nxt_add: EX itm. not(dat(itm)<=dat(ori))" neuper@37926: | SOME ori => SOME (geti_ct thy ori (hd icl)) neuper@37934: end neuper@37934: end; neuper@37906: neuper@37906: neuper@37906: neuper@37906: fun mk_delete thy "#Given" itm_ = Del_Given (itm_out thy itm_) neuper@37906: | mk_delete thy "#Find" itm_ = Del_Find (itm_out thy itm_) neuper@37906: | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_) neuper@37906: | mk_delete thy str _ = neuper@37906: raise error ("mk_delete: called with field '"^str^"'"); neuper@37906: fun mk_additem "#Given" ct = Add_Given ct neuper@37906: | mk_additem "#Find" ct = Add_Find ct neuper@37906: | mk_additem "#Relate"ct = Add_Relation ct neuper@37906: | mk_additem str _ = neuper@37906: raise error ("mk_additem: called with field '"^str^"'"); neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: (* find the next tac in specify (except nxt_model_pbl) neuper@37906: 4.00.: TODO: do not return a pos !!! neuper@37906: (sind from DG comes the _OLD_ writepos)*) neuper@37906: (* neuper@37906: > val (pbl,pbt,mpc) =(pbl',get_pbt cpI,(#ppc o get_met) cmI); neuper@37906: > val (dI,pI,mI) = empty_spec; neuper@37906: > nxt_spec Pbl (oris:ori list) ((dI',pI',mI'):spec(*original*)) neuper@37906: ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec); neuper@37906: neuper@37906: at Init_Proof: neuper@37906: > val met = [];val (pbt,mpc) = (get_pbt pI',(#ppc o get_met) mI'); neuper@37906: > val (dI,pI,mI) = empty_spec; neuper@37906: > nxt_spec Pbl (oris:ori list) ((dI',pI',mI'):spec(*original*)) neuper@37906: ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec); neuper@37906: *) neuper@37906: neuper@37906: (*. determine the next step of specification; neuper@37906: not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met)) neuper@37906: eg. in rootpbl 'no_met': neuper@37906: args: neuper@37906: preok predicates are _all_ ok, or 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@37906: .*) neuper@37906: (* val (preok,pbl,pbt,mpc)=(pb,pbl',(#ppc o get_pbt) cpI,(#ppc o get_met) cmI); neuper@37906: val (preok,pbl,pbt,mpc)=(pb,pbl',ppc,(#ppc o get_met) cmI); neuper@37906: val (Pbl, preok, oris, (dI',pI',mI'), (pbl,met), (pbt,mpc), (dI,pI,mI)) = neuper@37906: (p_, pb, oris, (dI',pI',mI'), (probl,meth), neuper@37906: (ppc, (#ppc o get_met) cmI), (dI,pI,mI)); neuper@37906: *) neuper@37906: fun nxt_spec Pbl preok (oris:ori list) ((dI',pI',mI'):spec) neuper@37906: ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec) = neuper@37906: ((*writeln"### nxt_spec Pbl";*) neuper@37906: if dI'=e_domID andalso dI=e_domID then (Pbl, Specify_Theory dI') neuper@37906: else if pI'=e_pblID andalso pI=e_pblID then (Pbl, Specify_Problem pI') neuper@37906: else case find_first (is_error o #5) (pbl:itm list) of neuper@37926: SOME (_,_,_,fd,itm_) => neuper@37906: (Pbl, mk_delete neuper@37906: (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_) neuper@37926: | NONE => neuper@37926: ((*writeln"### nxt_spec is_error NONE";*) neuper@37906: case nxt_add (assoc_thy (if dI=e_domID then dI' else dI)) neuper@37906: oris pbt pbl of neuper@37926: (* val SOME (fd,ct') = nxt_add (assoc_thy (if dI=e_domID then dI' else dI)) neuper@37906: oris pbt pbl; neuper@37906: *) neuper@37926: SOME (fd,ct') => ((*writeln"### nxt_spec nxt_add SOME";*) neuper@37906: (Pbl, mk_additem fd ct')) neuper@37926: | NONE => (*pbl-items complete*) neuper@37906: if not preok then (Pbl, Refine_Problem pI') neuper@37906: else neuper@37906: if dI = e_domID then (Pbl, Specify_Theory dI') neuper@37906: else if pI = e_pblID then (Pbl, Specify_Problem pI') neuper@37906: else if mI = e_metID then (Pbl, Specify_Method mI') neuper@37906: else neuper@37906: case find_first (is_error o #5) met of neuper@37926: SOME (_,_,_,fd,itm_) => neuper@37906: (Met, mk_delete (assoc_thy dI) fd itm_) neuper@37926: | NONE => neuper@37906: (case nxt_add (assoc_thy dI) oris mpc met of neuper@37926: SOME (fd,ct') => (*30.8.01: pre?!?*) neuper@37906: (Met, mk_additem fd ct') neuper@37926: | NONE => neuper@37906: ((*Solv 3.4.00*)Met, Apply_Method mI)))) neuper@37906: (* val preok=pb; val (pbl, met) = (pbl,met'); neuper@37906: val (pbt,mpc)=((#ppc o get_pbt) cpI,(#ppc o get_met) cmI); neuper@37906: val (Met, preok, oris, (dI',pI',mI'), (pbl,met), (pbt,mpc), (dI,pI,mI)) = neuper@37906: (p_, pb, oris, (dI',pI',mI'), (probl,meth), neuper@37906: (ppc, (#ppc o get_met) cmI), (dI,pI,mI)); neuper@37906: *) neuper@37906: | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) = neuper@37906: ((*writeln"### nxt_spec Met"; *) neuper@37906: case find_first (is_error o #5) met of neuper@37926: SOME (_,_,_,fd,itm_) => neuper@37906: (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_) neuper@37926: | NONE => neuper@37906: case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of neuper@37926: SOME (fd,ct') => (Met, mk_additem fd ct') neuper@37926: | NONE => neuper@37926: ((*writeln"### nxt_spec Met: nxt_add NONE";*) neuper@37906: if dI = e_domID then (Met, Specify_Theory dI') neuper@37906: else if pI = e_pblID then (Met, Specify_Problem pI') neuper@37906: else if not preok then (Met, Specify_Method mI) neuper@37906: else (Met, Apply_Method mI))); neuper@37906: neuper@37906: (* di_ pI_ mI_ pos_ neuper@37906: val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm, neuper@37906: (2,[2],true,"#Find",Syn("empty"))]; neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: (* ^^^--- aus nnewcode.sml am 30.1.00 ---^^^ *) neuper@37906: (*#############################################################*) neuper@37906: (*#############################################################*) neuper@37906: (* vvv--- aus nnewcode.sml vor 29.1.00 ---vvv *) neuper@37906: neuper@37906: (*3.3.-- neuper@37906: fun update_itm (cl,d,ts) ((id,vt,_,sl,Cor (_,_)):itm) = neuper@37906: (id,vt,cl,sl,Cor (d,ts)):itm neuper@37906: | update_itm (cl,d,ts) (id,vt,_,sl,Syn (_)) = neuper@37934: raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^ neuper@37906: " not not for Syn (s:cterm')") neuper@37906: | update_itm (cl,d,ts) (id,vt,_,sl,Typ (_)) = neuper@37934: raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^ neuper@37906: " not not for Typ (s:cterm')") neuper@37906: | update_itm (cl,d,ts) (id,vt,_,sl,Fal (_,_)) = neuper@37906: (id,vt,cl,sl,Fal (d,ts)) neuper@37906: | update_itm (cl,d,ts) (id,vt,_,sl,Inc (_,_)) = neuper@37906: (id,vt,cl,sl,Inc (d,ts)) neuper@37906: | update_itm (cl,d,ts) (id,vt,_,sl,Sup (_,_)) = neuper@37906: (id,vt,cl,sl,Sup (d,ts)); neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: fun is_field_correct sel d dscpbt = neuper@37906: case assoc (dscpbt, sel) of neuper@37926: NONE => false neuper@37934: | SOME ds => member op = ds d; neuper@37906: neuper@37906: (*. update the itm_ already input, all..from ori .*) neuper@37906: (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts'); neuper@37906: *) neuper@37906: fun ori_2itm thy itm_ pid all ((id,vt,fd,d,ts):ori) = neuper@37906: let neuper@37930: val ts' = union op = (ts_in itm_) ts; neuper@37906: val pval = pbl_ids' thy d ts' neuper@37906: (*WN.9.5.03: FIXXXME [#0, epsilon] neuper@37906: here would upd_penv be called for [#0, epsilon] etc. *) neuper@37934: val complete = if eq_set op = (ts', all) then true else false; neuper@37906: in case itm_ of neuper@37906: (Cor _) => neuper@37906: (if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts')) neuper@37906: else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm neuper@37906: | (Syn c) => raise error ("ori_2itm wants to overwrite "^c) neuper@37906: | (Typ c) => raise error ("ori_2itm wants to overwrite "^c) neuper@37906: | (Inc _) => if complete neuper@37906: then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval))) neuper@37906: else (id,vt,false,fd, Inc ((d,ts'),(pid, pval))) neuper@37906: | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*) neuper@37906: (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts')) neuper@37906: (*else (id,vt,complete,fd,Cor((d,ts'),e))*) neuper@37906: (* 28.1.00: not completely clear ---^^^ etc.*) neuper@37906: (* 4.9.01: Mis just copied---vvv *) neuper@37906: | (Mis _) => if complete neuper@37906: then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval))) neuper@37906: else (id,vt,false,fd, Inc ((d,ts'),(pid, pval))) neuper@37906: end; neuper@37906: neuper@37906: neuper@37906: fun eq1 d (_,(d',_)) = (d = d'); neuper@37906: fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_); neuper@37906: 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 .*) neuper@37906: (* val(itms,(i,v,f,d,ts)) = (ppc,ori'); neuper@37906: *) neuper@37906: fun is_notyet_input thy (itms:itm list) all ((i,v,f,d,ts):ori) pbt = neuper@37906: case find_first (eq1 d) pbt of neuper@37926: SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt; neuper@37926: val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms; neuper@37906: *) neuper@37906: (case find_first (eq3 f d) itms of neuper@37926: SOME (_,_,_,_,itm_) => neuper@37906: let neuper@37934: val ts' = inter op = (ts_in itm_) ts; neuper@37934: in if subset op = (ts, ts') neuper@37906: then (((strs2str' o neuper@37934: map (Syntax.string_of_term (thy2ctxt thy))) ts')^ neuper@37906: " already input", e_itm) (*2*) neuper@37934: else ("", neuper@37934: ori_2itm thy itm_ pid all (i,v,f,d, neuper@37934: subtract op = ts' ts)) (*3,4*) neuper@37906: end neuper@37926: | NONE => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[]))) neuper@37906: pid all (i,v,f,d,ts)) (*1*) neuper@37906: ) neuper@37926: | NONE => ("", ori_2itm thy (Sup (d,ts)) neuper@37906: e_term all (i,v,f,d,ts)); neuper@37906: neuper@37906: fun test_types thy (d,ts) = neuper@37906: let neuper@37906: val s = !show_types; val _ = show_types:= true; neuper@37906: val opt = (try (comp_dts thy)) (d,ts); neuper@37906: val msg = case opt of neuper@37926: SOME _ => "" neuper@37934: | NONE => ((Syntax.string_of_term (thy2ctxt thy) d)^" "^ neuper@37934: ((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts) neuper@37934: ^ " is illtyped"); neuper@37906: val _ = show_types:= s neuper@37906: in msg end; neuper@37906: neuper@37906: neuper@37906: neuper@37906: fun maxl [] = raise error "maxl of []" neuper@37906: | maxl (y::ys) = neuper@37906: let fun mx x [] = x neuper@37906: | mx x (y::ys) = if x < (y:int) then mx y ys else mx x ys neuper@37906: in mx y ys end; neuper@37906: neuper@37906: neuper@37906: (*. is the input term t known in oris ? neuper@37906: give feedback on all(?) strange input; neuper@37906: return _all_ terms already input to this item (e.g. valuesFor a,b) .*) neuper@37906: (*WN.11.03: from lists*) neuper@37906: fun is_known thy sel ori t = neuper@37906: (* val (ori,t)=(oris,term_of ct); neuper@37906: *) neuper@37906: let neuper@37906: val ots = (distinct o flat o (map #5)) (ori:ori list); neuper@37906: val oids = ((map (fst o dest_Free)) o distinct o neuper@37906: flat o (map vars)) ots; neuper@37906: val (d,ts(*,pval*)) = split_dts thy t; neuper@37906: val ids = map (fst o dest_Free) neuper@37906: ((distinct o (flat o (map vars))) ts); neuper@37934: in if (subtract op = oids ids) <> [] neuper@37934: then (("identifiers "^(strs2str' (subtract op = oids ids))^ neuper@37906: " not in example"), e_ori_, []) neuper@37906: else neuper@37906: if d = e_term neuper@37906: then neuper@37934: if not (subset op = (map typeless ts, map typeless ots)) neuper@37906: then (("terms '"^ neuper@37934: ((strs2str' o (map (Syntax.string_of_term neuper@37934: (thy2ctxt thy)))) ts)^ neuper@37906: "' not in example (typeless)"), e_ori_, []) neuper@37906: else (case seek_orits thy sel ts ori of neuper@37906: ("", ori_ as (_,_,_,d,ts), all) => neuper@37906: (case test_types thy (d,ts) of neuper@37906: "" => ("", ori_, all) neuper@37906: | msg => (msg, e_ori_, [])) neuper@37906: | (msg,_,_) => (msg, e_ori_, [])) neuper@37906: else neuper@37934: if member op = (map #4 ori) d neuper@37906: then seek_oridts thy sel (d,ts) ori neuper@37934: else ((Syntax.string_of_term (thy2ctxt thy) d)^ neuper@37906: (*" not in example", e_ori_, []) ///11.11.03*) neuper@37906: " not in example", (0,[],sel,d,ts), []) neuper@37906: end; neuper@37906: neuper@37906: neuper@37906: (*. for return-value of appl_add .*) neuper@37906: datatype additm = neuper@37906: Add of itm neuper@37906: | Err of string; (*error-message*) neuper@37906: neuper@37906: neuper@37906: (*. add an item; check wrt. oris and pbt .*) neuper@37906: neuper@37906: (* in contrary to oris<>[] below, this part handles user-input neuper@37906: extremely acceptive, i.e. accept input instead error-msg *) neuper@37906: fun appl_add thy sel ([]:ori list) ppc pbt ct' = neuper@37906: (* val (ppc,pbt,ct',env) = (pbl, (#ppc o get_pbt) cpI, ct, []:envv); neuper@37906: !!!! 28.8.01: env tested _minimally_ !!! neuper@37906: *) neuper@37906: let neuper@37906: val i = 1 + (if ppc=[] then 0 else maxl (map #1 ppc)); neuper@37906: in case parse thy ct' of (*should be done in applicable_in 4.00.FIXME*) neuper@37926: NONE => Add (i,[],false,sel,Syn ct') neuper@37926: (* val (SOME ct) = parse thy ct'; neuper@37906: *) neuper@37926: | SOME ct => neuper@37906: let neuper@37906: val (d,ts(*,pval*)) = split_dts thy (term_of ct); neuper@37906: in if d = e_term neuper@37906: then Add (i,[],false,sel,Mis (dsc_unknown,hd ts(*24.3.02*))) neuper@37906: neuper@37906: else neuper@37906: (case find_first (eq1 d) pbt of neuper@37926: NONE => Add (i,[],true,sel,Sup ((d,ts))) neuper@37926: | SOME (f,(_,id)) => neuper@37926: (* val SOME (f,(_,id)) = find_first (eq1 d) pbt; neuper@37906: *) neuper@37906: let neuper@37906: fun eq2 d ((i,_,_,_,itm_):itm) = neuper@37906: (d = (d_in itm_)) andalso i<>0; neuper@37906: in case find_first (eq2 d) ppc of neuper@37926: NONE => Add (i,[],true,f, Cor ((d,ts), (id, (*pval*) neuper@37906: pbl_ids' thy d ts))) neuper@37926: | SOME (i',_,_,_,itm_) => neuper@37926: (* val SOME (i',_,_,_,itm_) = find_first (eq2 d) ppc; neuper@37926: val NONE = find_first (eq2 d) ppc; neuper@37906: *) neuper@37906: if is_list_dsc d neuper@37930: then let val ts = union op = ts (ts_in itm_) neuper@37906: in Add (if ts_in itm_ = [] then i else i', neuper@37906: [],true,f,Cor ((d, ts), (id, (*pval*) neuper@37906: pbl_ids' thy d ts))) neuper@37906: end neuper@37906: else Add (i',[],true,f,Cor ((d,ts),(id, (*pval*) neuper@37906: pbl_ids' thy d ts))) neuper@37906: end neuper@37906: ) neuper@37906: end neuper@37906: end neuper@37906: (*. add ct to ppc .*) neuper@37906: (*FIXXME: accept items as Sup, Syn here, too (like appl_add..oris=[] above)*) neuper@37906: (* val (ppc,pbt) = (pbl, ppc); neuper@37906: val (ppc,pbt) = (met, (#ppc o get_met) cmI); neuper@37906: neuper@37906: val (ppc,pbt) = (pbl, (#ppc o get_pbt) cpI); neuper@37906: *) neuper@37906: | appl_add thy sel oris ppc pbt(*only for upd_envv*) ct = neuper@37906: let neuper@37906: val ctopt = parse thy ct; neuper@37906: in case ctopt of neuper@37926: NONE => Err ("syntax error in "^ct) neuper@37926: | SOME ct =>(* val SOME ct = ctopt; neuper@37906: val (msg,ori',all) = is_known thy sel oris (term_of ct); neuper@37906: val (msg,itm) = is_notyet_input thy ppc all ori' pbt; neuper@37906: *) neuper@37906: (case is_known thy sel oris (term_of ct) of neuper@37906: ("",ori'(*ts='ct'*), all) => neuper@37906: (case is_notyet_input thy ppc all ori' pbt of neuper@37906: ("",itm) => Add itm neuper@37906: | (msg,_) => Err msg) neuper@37906: | (msg,_,_) => Err msg) neuper@37906: end; neuper@37906: (* neuper@37906: > val (msg,itm) = is_notyet_input thy ppc all ori'; neuper@37906: val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm neuper@37906: > val itm_ = #5 itm; neuper@37906: > val ts = ts_in itm_; neuper@37906: > map (atomty) ts; neuper@37906: *) neuper@37906: neuper@37906: (*---------------------------------------------(4) nach ptyps.sml 23.3.02*) neuper@37906: neuper@37906: neuper@37906: (** make oris from args of the stac SubProblem and from pbt **) neuper@37906: neuper@37906: (*.can this formal argument (of a model-pattern) be omitted in the arg-list neuper@37906: of a SubProblem ? see ME/ptyps.sml 'type met '.*) neuper@37906: fun is_copy_named_idstr str = neuper@37906: case (rev o explode) str of neuper@38009: (*"_"::_ ::"_"::_ => true*) neuper@38009: "'"::"'"::"'"::_ => true neuper@37906: | _ => false; neuper@38009: (*> is_copy_named_idstr "v_i'''"; neuper@37906: val it = true : bool neuper@37906: > is_copy_named_idstr "e_"; neuper@37906: val it = false : bool neuper@37906: > is_copy_named_idstr "L___"; neuper@37906: val it = true : bool neuper@37906: *) neuper@37906: (*.should this formal argument (of a model-pattern) create a new identifier?.*) neuper@37906: fun is_copy_named_generating_idstr str = neuper@37906: if is_copy_named_idstr str neuper@37906: then case (rev o explode) str of neuper@37906: "_"::"_"::"_"::_ => false neuper@37906: | _ => true neuper@37906: else false; neuper@38009: (*> is_copy_named_generating_idstr "v_i'''"; neuper@37906: val it = true : bool neuper@37906: > is_copy_named_generating_idstr "L___"; neuper@37906: val it = false : bool neuper@37906: *) neuper@37906: neuper@37906: (*.can this formal argument (of a model-pattern) be omitted in the arg-list neuper@37906: of a SubProblem ? see ME/ptyps.sml 'type met '.*) neuper@37906: fun is_copy_named (_,(_,t)) = (is_copy_named_idstr o free2str) t; neuper@37906: (*.should this formal argument (of a model-pattern) create a new identifier?.*) neuper@37906: fun is_copy_named_generating (_,(_,t)) = neuper@37906: (is_copy_named_generating_idstr o free2str) t; neuper@37906: neuper@37906: neuper@37906: (*.split type-wrapper from scr-arg and build part of an ori; neuper@37906: an type-error is reported immediately, raises an exn, neuper@37906: subsequent handling of exn provides 2nd part of error message.*) neuper@37934: (*fun mtc thy ((str, (dsc, _)):pat) (ty $ var) = WN100820 made cterm to term neuper@37906: (* val (thy, (str, (dsc, _)), (ty $ var)) = neuper@37906: (thy, p, a); neuper@37906: *) neuper@37938: (cterm_of thy (dsc $ var);(*type check*) neuper@37926: SOME ((([1], str, dsc, (*[var]*) neuper@37906: split_dts' (dsc, var))): preori)(*:ori without leading #*)) neuper@37906: handle e as TYPE _ => neuper@37906: (writeln (dashs 70^"\n" neuper@37906: ^"*** ERROR while creating the items for the model of the ->problem\n" neuper@37906: ^"*** from the ->stac with ->typeconstructor in arglist:\n" neuper@37906: ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n" neuper@37906: ^"*** description: "^(term_detail2str dsc) neuper@37906: ^"*** value: "^(term_detail2str var) neuper@37906: ^"*** typeconstructor in script: "^(term_detail2str ty) neuper@37906: ^"*** checked by theory: "^(theory2str thy)^"\n" neuper@37906: ^"*** "^dots 66); neuper@37906: print_exn e; (*raises exn again*) neuper@37934: NONE);*) neuper@37934: fun mtc thy ((str, (dsc, _)):pat) (ty $ var) = neuper@37934: (* val (thy, (str, (dsc, _)), (ty $ var)) = neuper@37934: (thy, p, a); neuper@37934: *) neuper@37938: (cterm_of thy (dsc $ var);(*type check*) neuper@37934: SOME ((([1], str, dsc, (*[var]*) neuper@37934: split_dts' (dsc, var))): preori)(*:ori without leading #*)) neuper@37934: handle e as TYPE _ => neuper@37934: (writeln (dashs 70^"\n" neuper@37934: ^"*** ERROR while creating the items for the model of the ->problem\n" neuper@37934: ^"*** from the ->stac with ->typeconstructor in arglist:\n" neuper@37934: ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n" neuper@37934: ^"*** description: "^(term_detail2str dsc) neuper@37934: ^"*** value: "^(term_detail2str var) neuper@37934: ^"*** typeconstructor in script: "^(term_detail2str ty) neuper@37934: ^"*** checked by theory: "^(theory2str thy)^"\n" neuper@37934: ^"*** "^dots 66); neuper@37934: (*WN100820 postponed: print_exn e; raises exn again*) neuper@37926: NONE); neuper@37906: (*> val pbt = (#ppc o get_pbt) ["univariate","equation"]; neuper@37906: > val Const ("Script.SubProblem",_) $ neuper@37906: (Const ("Pair",_) $ Free (thy', _) $ neuper@37906: (Const ("Pair",_) $ pblID' $ metID')) $ ags = neuper@37906: str2term"(SubProblem (SqRoot_,[univariate,equation],\ neuper@37984: \[SqRoot_,solve_linear]) [BOOL (x+1- 2=0), REAL x])::bool list"; neuper@37906: > val ags = isalist2list ags; neuper@37906: > mtc thy (hd pbt) (hd ags); neuper@37926: val it = SOME ([1],"#Given",Const (#,#),[# $ #]) *) neuper@37906: neuper@37906: (*.match each pat of the model-pattern with an actual argument; neuper@37906: precondition: copy-named vars are filtered out.*) neuper@37906: fun matc thy ([]:pat list) _ (oris:preori list) = oris neuper@37906: | matc thy pbt [] _ = neuper@37906: (writeln (dashs 70); neuper@37906: raise error ("actual arg(s) missing for '"^pats2str pbt neuper@37906: ^"' i.e. should be 'copy-named' by '*_._'")) neuper@37906: | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris = neuper@37906: (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) = neuper@37906: (thy, pbt', ags, []); neuper@37906: (*recursion..*) neuper@37906: val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) = neuper@37906: (thy, pbt, ags, (oris @ [ori])); neuper@37906: *) neuper@37906: (*del?..*)if (is_copy_named_idstr o free2str) t then oris neuper@37906: else(*..del?*) let val opt = mtc thy p a; neuper@37906: in case opt of neuper@37926: (* val SOME ori = mtc thy p a; neuper@37906: *) neuper@37926: SOME ori => matc thy pbt ags (oris @ [ori]) neuper@37926: | NONE => [](*WN050903 skipped by exn handled in match_ags*) neuper@37906: end; neuper@37906: (* run subp-rooteq.sml until Init_Proof before ... neuper@37906: > val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*) neuper@37906: > fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris; neuper@37906: neuper@37906: other vars as in mtc .. neuper@37906: > matc thy (drop_last pbt) ags []; neuper@37906: val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*) neuper@37906: neuper@37906: neuper@37906: (*WN051014 outcommented with redesign copy-named (for omitting '#Find' neuper@37906: in SubProblem); neuper@37906: kept as initial idea for generating x_1, x_2, ... for equations*) neuper@37906: fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) = neuper@37906: (* val ((pbt:pat list), (oris:preori list), ((field,(dsc,t)):pat)) = neuper@37906: (pbt', oris', hd (*!!!!!*) cy); neuper@37906: *) neuper@37906: (if is_copy_named_generating p neuper@37906: then (*WN051014 kept strange old code ...*) neuper@37906: let fun sel (_,_,d,ts) = comp_ts (d, ts) neuper@37906: val cy' = (implode o drop_last o drop_last o explode o free2str) t neuper@37906: val ext = (last_elem o drop_last o explode o free2str) t neuper@37906: val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*) neuper@37906: val vals = map sel oris neuper@37906: val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext neuper@37906: in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end neuper@37906: else ([1], field, dsc, [t]) neuper@37906: ) neuper@37906: handle _ => raise error ("cpy_nam: for "^(term2str t)); neuper@37906: neuper@37906: (*> val (field,(dsc,t)) = last_elem pbt; neuper@37906: > cpy_nam pbt (drop_last oris) (field,(dsc,t)); neuper@37906: val it = ([1],"#Find", neuper@37906: Const ("Descript.solutions","bool List.list => Tools.toreall"), neuper@37906: [Free ("x_i","bool List.list")]) *) neuper@37906: neuper@37906: neuper@37906: (*.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@37906: copy-named pats are appended in order to get them into the model-items.*) neuper@37906: fun match_ags thy (pbt:pat list) ags = neuper@37906: (* val (thy, pbt, ags) = (thy, (#ppc o get_pbt) pI, ags); neuper@37906: val (thy, pbt, ags) = (thy, pats, ags); neuper@37906: *) neuper@37906: let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_); neuper@37906: val pbt' = filter_out is_copy_named pbt; neuper@37906: val cy = filter is_copy_named pbt; neuper@37906: val oris' = matc thy pbt' ags []; neuper@37906: val cy' = map (cpy_nam pbt' oris') cy; neuper@37906: val ors = add_id (oris' @ cy'); neuper@37906: (*appended in order to get ^^^^^ them into the model-items*) neuper@37906: in (map flattup ors):ori list end; neuper@37906: (*vars as above .. neuper@37906: > match_ags thy pbt ags; neuper@37906: val it = neuper@37906: [(1,[1],"#Given",Const ("Descript.equality","bool => Tools.una"), neuper@37906: [Const # $ (# $ #) $ Free (#,#)]), neuper@37906: (2,[1],"#Given",Const ("Descript.solveFor","RealDef.real => Tools.una"), neuper@37906: [Free ("x","RealDef.real")]), neuper@37906: (3,[1],"#Find", neuper@37906: Const ("Descript.solutions","bool List.list => Tools.toreall"), neuper@37906: [Free ("x_i","bool List.list")])] : ori list*) neuper@37906: neuper@37906: (*.report part of the error-msg which is not available in match_args.*) neuper@37906: fun match_ags_msg pI stac ags = neuper@37906: let val s = !show_types neuper@37906: val _ = show_types:= true neuper@37906: val pats = (#ppc o get_pbt) pI neuper@37906: val msg = (dots 70^"\n" neuper@37906: ^"*** problem "^strs2str pI^" has the ...\n" neuper@37906: ^"*** model-pattern "^pats2str pats^"\n" neuper@37906: ^"*** stac '"^term2str stac^"' has the ...\n" neuper@37906: ^"*** arg-list "^terms2str ags^"\n" neuper@37906: ^dashs 70) neuper@37906: val _ = show_types:= s neuper@37906: in writeln msg end; neuper@37906: neuper@37906: neuper@37906: (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*) neuper@37906: fun vars_of_pbl_ pbl_ = neuper@37906: let fun var_of_pbl_ (gfr,(dsc,t)) = t neuper@37906: in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end; neuper@37906: fun vars_of_pbl_' pbl_ = neuper@37906: let fun var_of_pbl_ (gfr,(dsc,t)) = t:term neuper@37906: 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 neuper@37906: fun repl ppc' (_,_,_,_,itm_) [] = neuper@37934: raise error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^ neuper@37934: " not found") neuper@37906: | repl ppc' itm (p::ppc) = neuper@37906: if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc neuper@37906: else repl (ppc' @ [p]) itm ppc neuper@37906: in repl [] itm ppc end; neuper@37906: neuper@37906: (*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: (* val ppc=pbl; neuper@37906: *) neuper@37906: fun insert_ppc thy itm ppc = neuper@37906: let neuper@37906: fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_) neuper@37906: | eq_untouched _ _ = false; neuper@37906: val ppc' = neuper@37906: ( neuper@37924: (*writeln("### insert_ppc: itm= "^(itm2str_ itm));*) neuper@37906: case seek_ppc (#1 itm) ppc of neuper@37926: (* val SOME xxx = seek_ppc (#1 itm) ppc; neuper@37906: *) neuper@37926: SOME _ => (*itm updated in is_notyet_input WN.11.03*) neuper@37906: overwrite_ppc thy itm ppc neuper@37926: | NONE => (ppc @ [itm])); neuper@37906: in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end; neuper@37906: neuper@37906: (*from Isabelle/src/Pure/library.ML, _appends_ a new element*) neuper@37906: fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x]; neuper@37906: neuper@37906: fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) = neuper@37906: (d_in itm_) = (d_in iitm_); neuper@37906: (*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03, neuper@37906: handles superfluous items carelessly*) neuper@37906: fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms); neuper@37906: (* val eee = op=; neuper@37906: > gen_ins' eee (4,[1,3,5,7]); neuper@37906: val it = [1, 3, 5, 7, 4] : int list*) neuper@37906: neuper@37906: neuper@37906: (*. output the headline to a ppc .*) neuper@37906: fun header p_ pI mI = neuper@37906: case p_ of Pbl => Problem (if pI = e_pblID then [] else pI) neuper@37906: | Met => Method mI neuper@37906: | pos => raise error ("header called with "^ pos_2str pos); neuper@37906: neuper@37906: neuper@37906: neuper@37906: (* test-printouts --- neuper@37934: val _=writeln("### insert_ppc: (d,ts)="^((Syntax.string_of_term (thy2ctxt thy))(comp_dts thy(d,ts)))); neuper@37906: val _=writeln("### insert_ppc: pts= "^ neuper@37934: (strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) pts); neuper@37906: neuper@37906: neuper@37906: val sel = "#Given"; val Add_Given' ct = m; neuper@37906: neuper@37906: val sel = "#Find"; val Add_Find' (ct,_) = m; neuper@37906: val (p,_) = p; neuper@37906: val (_,_,f,nxt',_,pt')= specify_additem sel (ct,[]) (p,Pbl(*!!!!!!!*)) c pt; neuper@37906: -------------- neuper@37906: val sel = "#Given"; val Add_Given' (ct,_) = nxt; val (p,_) = p; neuper@37906: *) neuper@37906: fun specify_additem sel (ct,_) (p,Met) c pt = neuper@37906: let neuper@37906: val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_), neuper@37906: probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p; neuper@37906: val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI; neuper@37906: (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*) neuper@37906: val cpI = if pI = e_pblID then pI' else pI; neuper@37906: val cmI = if mI = e_metID then mI' else mI; neuper@37906: val {ppc,pre,prls,...} = get_met cmI neuper@37906: in case appl_add thy sel oris met ppc ct of neuper@37906: Add itm (*..union old input *) => neuper@37906: let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct; neuper@37906: *) neuper@37906: val met' = insert_ppc thy itm met; neuper@37906: (*val pt' = update_met pt p met';*) neuper@37906: val ((p,Met),_,_,pt') = neuper@37906: generate1 thy (case sel of neuper@37906: "#Given" => Add_Given' (ct, met') neuper@37906: | "#Find" => Add_Find' (ct, met') neuper@37906: | "#Relate"=> Add_Relation'(ct, met')) neuper@37906: Uistate (p,Met) pt neuper@37906: val pre' = check_preconds thy prls pre met' neuper@37906: val pb = foldl and_ (true, map fst pre') neuper@37906: (*val _=writeln("@@@ specify_additem: Met Add before nxt_spec")*) neuper@37906: val (p_,nxt) = neuper@37906: nxt_spec Met pb oris (dI',pI',mI') (pbl,met') neuper@37906: ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI); neuper@37906: in ((p,p_), ((p,p_),Uistate), neuper@37906: Form' (PpcKF (0,EdUndef,(length p),Nundef, neuper@37906: (Method cmI, itms2itemppc thy met' pre'))), neuper@37906: nxt,Safe,pt') end neuper@37906: | Err msg => neuper@37906: let val pre' = check_preconds thy prls pre met neuper@37906: val pb = foldl and_ (true, map fst pre') neuper@37906: (*val _=writeln("@@@ specify_additem: Met Err before nxt_spec")*) neuper@37906: val (p_,nxt) = neuper@37906: nxt_spec Met pb oris (dI',pI',mI') (pbl,met) neuper@37906: ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI); neuper@37906: in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end neuper@37906: end neuper@37906: (* val (p,_) = p; neuper@37906: *) neuper@37906: | specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt = neuper@37906: let neuper@37906: val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_), neuper@37906: probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p; neuper@37906: val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI; neuper@37906: val cpI = if pI = e_pblID then pI' else pI; neuper@37906: val cmI = if mI = e_metID then mI' else mI; neuper@37906: val {ppc,where_,prls,...} = get_pbt cpI; neuper@37906: in case appl_add thy sel oris pbl ppc ct of neuper@37906: Add itm (*..union old input *) => neuper@37906: (* val Add itm = appl_add thy sel oris pbl ppc ct; neuper@37906: *) neuper@37906: let neuper@37924: (*val _= writeln("###specify_additem: itm= "^(itm2str_ itm));*) neuper@37906: val pbl' = insert_ppc thy itm pbl neuper@37906: val ((p,Pbl),_,_,pt') = neuper@37906: generate1 thy (case sel of neuper@37906: "#Given" => Add_Given' (ct, pbl') neuper@37906: | "#Find" => Add_Find' (ct, pbl') neuper@37906: | "#Relate"=> Add_Relation'(ct, pbl')) neuper@37906: Uistate (p,Pbl) pt neuper@37906: val pre = check_preconds thy prls where_ pbl' neuper@37906: val pb = foldl and_ (true, map fst pre) neuper@37906: (*val _=writeln("@@@ specify_additem: Pbl Add before nxt_spec")*) neuper@37906: val (p_,nxt) = neuper@37906: nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) neuper@37906: (ppc,(#ppc o get_met) cmI) (dI,pI,mI); neuper@37906: val ppc = if p_= Pbl then pbl' else met; neuper@37906: in ((p,p_), ((p,p_),Uistate), neuper@37906: Form' (PpcKF (0,EdUndef,(length p),Nundef, neuper@37906: (header p_ pI cmI, neuper@37906: itms2itemppc thy ppc pre))), nxt,Safe,pt') end neuper@37906: neuper@37906: | Err msg => neuper@37906: let val pre = check_preconds thy prls where_ pbl neuper@37906: val pb = foldl and_ (true, map fst pre) neuper@37906: (*val _=writeln("@@@ specify_additem: Pbl Err before nxt_spec")*) neuper@37906: val (p_,nxt) = neuper@37906: nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met) neuper@37906: (ppc,(#ppc o get_met) cmI) (dI,pI,mI); neuper@37906: in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end neuper@37906: end; neuper@37906: (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt; neuper@37906: val (_,_,f,nxt',_,pt')= specify_additem sel ct (p,Met) c pt; neuper@37906: *) neuper@37906: neuper@37906: (* ori neuper@37906: val (msg,itm) = appl_add thy sel oris ppc ct; neuper@37906: val (Cor(d,ts)) = #5 itm; neuper@37906: map (atomty) ts; neuper@37906: neuper@37906: pre neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: (* val Init_Proof' (fmz,(dI',pI',mI')) = m; neuper@37906: specify (Init_Proof' (fmz,(dI',pI',mI'))) e_pos' [] EmptyPtree; neuper@37906: *) neuper@37906: fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)= neuper@37906: let (* either """"""""""""""" all empty or complete *) neuper@37906: val thy = assoc_thy dI'; neuper@37906: val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list) neuper@37906: else prep_ori fmz thy ((#ppc o get_pbt) pI'); neuper@37906: val (pt,c) = cappend_problem e_ptree [] e_istate (fmz,(dI',pI',mI')) neuper@37906: (oris,(dI',pI',mI'),e_term); neuper@37906: val {ppc,prls,where_,...} = get_pbt pI' neuper@37906: (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem neuper@37906: val pt = update_pbl pt [] pbl; neuper@37906: val pre = check_preconds thy prls where_ pbl neuper@37906: val pb = foldl and_ (true, map fst pre)*) neuper@37906: val (pbl, pre, pb) = ([], [], false) neuper@37906: in case mI' of neuper@37906: ["no_met"] => neuper@37906: (([],Pbl), (([],Pbl),Uistate), neuper@37906: Form' (PpcKF (0,EdUndef,(length []),Nundef, neuper@37906: (Problem [], itms2itemppc (assoc_thy dI') pbl pre))), neuper@37906: Refine_Tacitly pI', Safe,pt) neuper@37906: | _ => neuper@37906: (([],Pbl), (([],Pbl),Uistate), neuper@37906: Form' (PpcKF (0,EdUndef,(length []),Nundef, neuper@37906: (Problem [], itms2itemppc (assoc_thy dI') pbl pre))), neuper@37906: Model_Problem, neuper@37906: Safe,pt) neuper@37906: end neuper@37906: (*ONLY for STARTING modeling phase*) neuper@37906: | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt = neuper@37906: let (* val (Model_Problem' (_,pbl), pos as (p,p_)) = (m, (p,p_)); neuper@37906: *) neuper@37906: val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) = neuper@37906: get_obj I pt p neuper@37906: val thy' = if dI = e_domID then dI' else dI neuper@37906: val thy = assoc_thy thy' neuper@37906: val {ppc,prls,where_,...} = get_pbt pI' neuper@37906: val pre = check_preconds thy prls where_ pbl neuper@37906: val pb = foldl and_ (true, map fst pre) neuper@37906: val ((p,_),_,_,pt) = neuper@37906: generate1 thy (Model_Problem'([],pbl,met)) Uistate pos pt neuper@37906: val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met) neuper@37906: (ppc,(#ppc o get_met) mI') (dI',pI',mI'); neuper@37906: in ((p,Pbl), ((p,p_),Uistate), neuper@37906: Form' (PpcKF (0,EdUndef,(length p),Nundef, neuper@37906: (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))), neuper@37906: nxt, Safe, pt) end neuper@37906: neuper@37906: (*. called only if no_met is specified .*) neuper@37906: | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt = neuper@37906: let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m; neuper@37906: *) neuper@37906: val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) = neuper@37906: get_obj I pt p; neuper@37906: val {prls,met,ppc,thy,where_,...} = get_pbt pIre neuper@37906: (*val pbl = init_pbl ppc --- Model_Problem recognizes probl=[]*) neuper@37906: (*val pt = update_pbl pt p pbl; neuper@37906: val pt = update_orispec pt p neuper@37906: (string_of_thy thy, pIre, neuper@37906: if length met = 0 then e_metID else hd met);*) neuper@37906: val (domID, metID) = (string_of_thy thy, neuper@37906: if length met = 0 then e_metID else hd met) neuper@37906: val ((p,_),_,_,pt) = neuper@37906: generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[])) neuper@37906: Uistate pos pt neuper@37906: (*val pre = check_preconds thy prls where_ pbl neuper@37906: val pb = foldl and_ (true, map fst pre)*) neuper@37906: val (pbl, pre, pb) = ([], [], false) neuper@37906: in ((p,Pbl), (pos,Uistate), neuper@37906: Form' (PpcKF (0,EdUndef,(length p),Nundef, neuper@37906: (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))), neuper@37906: Model_Problem, Safe, pt) end neuper@37906: neuper@37906: | specify (Refine_Problem' (rfd as (pI,_))) pos c pt = neuper@37906: let val (pos,_,_,pt) = generate1 (assoc_thy "Isac.thy") neuper@37906: (Refine_Problem' rfd) Uistate pos pt neuper@37906: in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd), neuper@37906: Model_Problem, Safe, pt) end neuper@37906: neuper@37906: (* val (Specify_Problem' (pI, (ok, (itms, pre)))) = nxt; val (p,_) = p; neuper@37906: val (Specify_Problem' (pI, (ok, (itms, pre)))) = m; val (p,_) = p; neuper@37906: *) neuper@37906: | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt = neuper@37906: let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI), neuper@37906: meth=met, ...}) = get_obj I pt p; neuper@37906: (*val pt = update_pbl pt p itms; neuper@37906: val pt = update_pblID pt p pI;*) neuper@37934: val thy = assoc_thy dI neuper@37906: val ((p,Pbl),_,_,pt)= neuper@37906: generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate pos pt neuper@37906: val dI'' = assoc_thy (if dI=e_domID then dI' else dI); neuper@37906: val mI'' = if mI=e_metID then mI' else mI; neuper@37906: (*val _=writeln("@@@ specify (Specify_Problem) before nxt_spec")*) neuper@37906: val (_,nxt) = nxt_spec Pbl ok oris (dI',pI',mI') (itms, met) neuper@37906: ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI); neuper@37906: in ((p,Pbl), (pos,Uistate), neuper@37906: Form' (PpcKF (0,EdUndef,(length p),Nundef, neuper@37906: (Problem pI, itms2itemppc dI'' itms pre))), neuper@37906: nxt, Safe, pt) end neuper@37906: (* val Specify_Method' mID = nxt; val (p,_) = p; neuper@37906: val Specify_Method' mID = m; neuper@37906: specify (Specify_Method' mID) (p,p_) c pt; neuper@37906: *) neuper@37906: | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt = neuper@37906: let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI), neuper@37906: meth=met, ...}) = get_obj I pt p; neuper@37906: val {ppc,pre,prls,...} = get_met mID neuper@37906: val thy = assoc_thy dI neuper@37906: val oris = add_field' thy ppc oris; neuper@37906: (*val pt = update_oris pt p oris; 20.3.02: repl. "#undef"*) neuper@37906: val dI'' = if dI=e_domID then dI' else dI; neuper@37906: val pI'' = if pI = e_pblID then pI' else pI; neuper@37906: val met = if met=[] then pbl else met; neuper@37906: val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris; neuper@37906: (*val pt = update_met pt p itms; neuper@37906: val pt = update_metID pt p mID*) neuper@37906: val (pos,_,_,pt)= neuper@37906: generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt neuper@37906: (*val _=writeln("@@@ specify (Specify_Method) before nxt_spec")*) neuper@37906: val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms) neuper@37906: ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID); neuper@37906: in (pos, (pos,Uistate), neuper@37906: Form' (PpcKF (0,EdUndef,(length p),Nundef, neuper@37906: (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))), neuper@37906: nxt, Safe, pt) end neuper@37906: (* val Add_Find' ct = nxt; val sel = "#Find"; neuper@37906: *) 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 neuper@37906: (* val Specify_Theory' domID = m; neuper@37906: val (Specify_Theory' domID, (p,p_)) = (m, pos); neuper@37906: *) neuper@37906: | specify (Specify_Theory' domID) (pos as (p,p_)) c pt = neuper@37906: let val p_ = case p_ of Met => Met | _ => Pbl neuper@37906: val thy = assoc_thy domID; neuper@37906: val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, neuper@37906: probl=pbl, spec=(dI,pI,mI),...}) = get_obj I pt p; neuper@37906: val mppc = case p_ of Met => met | _ => pbl; neuper@37906: val cpI = if pI = e_pblID then pI' else pI; neuper@37906: val {prls=per,ppc,where_=pwh,...} = get_pbt cpI neuper@37906: val cmI = if mI = e_metID then mI' else mI; neuper@37906: val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI neuper@37906: val pre = neuper@37906: case p_ of neuper@37906: Met => (check_preconds thy mer mwh met) neuper@37906: | _ => (check_preconds thy per pwh pbl) neuper@37906: val pb = foldl and_ (true, map fst pre) neuper@37906: in if domID = dI neuper@37906: then let neuper@37906: (*val _=writeln("@@@ specify (Specify_Theory) THEN before nxt_spec")*) neuper@37906: val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') neuper@37906: (pbl,met) (ppc,mpc) (dI,pI,mI); neuper@37906: in ((p,p_), (pos,Uistate), neuper@37906: Form'(PpcKF (0,EdUndef,(length p), Nundef, neuper@37906: (header p_ pI cmI, itms2itemppc thy mppc pre))), neuper@37906: nxt,Safe,pt) end neuper@37906: else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*) neuper@37906: let neuper@37906: (*val pt = update_domID pt p domID;11.8.03*) neuper@37906: val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID) neuper@37906: Uistate (p,p_) pt neuper@37906: (*val _=writeln("@@@ specify (Specify_Theory) ELSE before nxt_spec")*) neuper@37906: val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met) neuper@37906: (ppc,mpc) (domID,pI,mI); neuper@37906: in ((p,p_), (pos,Uistate), neuper@37906: Form' (PpcKF (0, EdUndef, (length p),Nundef, neuper@37906: (header p_ pI cmI, itms2itemppc thy mppc pre))), neuper@37906: nxt, Safe,pt) end neuper@37906: end neuper@37906: (* itms2itemppc thy [](*mpc*) pre neuper@37906: *) neuper@37906: | specify m' _ _ _ = neuper@37906: raise error ("specify: not impl. for "^tac_2str m'); neuper@37906: neuper@37906: (* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp); neuper@37906: val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp); neuper@37906: *) neuper@37906: fun nxt_specif_additem sel ct (ptp as (pt,(p,Pbl))) = neuper@37906: let neuper@37906: val (PblObj{meth=met,origin=(oris,(dI',pI',_),_), neuper@37906: probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p; neuper@37906: val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI; neuper@37906: val cpI = if pI = e_pblID then pI' else pI; neuper@37906: in case appl_add thy sel oris pbl ((#ppc o get_pbt) cpI) ct of neuper@37906: Add itm (*..union old input *) => neuper@37906: (* val Add itm = appl_add thy sel oris pbl ppc ct; neuper@37906: *) neuper@37906: let neuper@37924: (*val _=writeln("###nxt_specif_additem: itm= "^(itm2str_ itm));*) neuper@37906: val pbl' = insert_ppc thy itm pbl neuper@37906: val (tac,tac_) = neuper@37906: case sel of neuper@37906: "#Given" => (Add_Given ct, Add_Given' (ct, pbl')) neuper@37906: | "#Find" => (Add_Find ct, Add_Find' (ct, pbl')) neuper@37906: | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl')) neuper@37906: val ((p,Pbl),c,_,pt') = neuper@37906: generate1 thy tac_ Uistate (p,Pbl) pt neuper@37906: in ([(tac,tac_,((p,Pbl),Uistate))], c, (pt',(p,Pbl))):calcstate' end neuper@37906: neuper@37906: | Err msg => neuper@37906: (*TODO.WN03 pass error-msgs to the frontend.. neuper@37906: FIXME ..and dont abuse a tactic for that purpose*) neuper@37906: ([(Tac msg, neuper@37934: Tac_ (theory "Pure", msg,msg,msg), neuper@37906: (e_pos', e_istate))], [], ptp) neuper@37906: end neuper@37906: neuper@37906: (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt; neuper@37906: val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt; neuper@37906: *) neuper@37906: | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) = neuper@37906: let neuper@37906: val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_), neuper@37906: probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p; neuper@37906: val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI; neuper@37906: val cmI = if mI = e_metID then mI' else mI; neuper@37906: in case appl_add thy sel oris met ((#ppc o get_met) cmI) ct of neuper@37906: Add itm (*..union old input *) => neuper@37906: let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct; neuper@37906: *) neuper@37906: val met' = insert_ppc thy itm met; neuper@37906: val (tac,tac_) = neuper@37906: case sel of neuper@37906: "#Given" => (Add_Given ct, Add_Given' (ct, met')) neuper@37906: | "#Find" => (Add_Find ct, Add_Find' (ct, met')) neuper@37906: | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met')) neuper@37906: val ((p,Met),c,_,pt') = neuper@37906: generate1 thy tac_ Uistate (p,Met) pt neuper@37906: in ([(tac,tac_,((p,Met), Uistate))], c, (pt',(p,Met))) end neuper@37906: neuper@37906: | Err msg => ([(*tacis*)], [], ptp) neuper@37906: (*nxt_me collects tacis until not hide; here just no progress*) neuper@37906: end; neuper@37906: neuper@37906: (* ori neuper@37906: val (msg,itm) = appl_add thy sel oris ppc ct; neuper@37906: val (Cor(d,ts)) = #5 itm; neuper@37906: map (atomty) ts; neuper@37906: neuper@37906: pre neuper@37906: *) neuper@37906: fun ori2Coritm pbt ((i,v,f,d,ts):ori) = neuper@37906: (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt) neuper@37906: handle _ => raise error ("ori2Coritm: dsc "^ neuper@37906: term2str d^ neuper@37906: "in ori, but not in pbt") neuper@37906: ,ts))):itm; neuper@37906: fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) = neuper@37906: ((i,v,true,f, Cor ((d,ts),((snd o snd o the o neuper@37906: (find_first (eq1 d))) pbt,ts))):itm) neuper@37906: handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*) neuper@37906: ((i,v,true,f, Cor ((d,ts),(d,ts))):itm); neuper@37906: neuper@37906: neuper@37906: (*filter out oris which have same description in itms*) neuper@37906: fun filter_outs oris [] = oris neuper@37906: | filter_outs oris (i::itms) = neuper@37906: let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o neuper@37906: (#4:ori -> term)) oris; neuper@37906: in filter_outs ors itms end; neuper@37906: neuper@37934: fun memI a b = member op = a b; neuper@37906: (*filter oris which are in pbt, too*) neuper@37906: fun filter_pbt oris pbt = neuper@37906: let val dscs = map (fst o snd) pbt neuper@37906: in filter ((memI dscs) o (#4: ori -> term)) oris end; neuper@37906: neuper@37906: (*.combine itms from pbl + met and complete them wrt. pbt.*) neuper@37906: (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*) neuper@37936: local infix mem; neuper@37934: fun x mem [] = false neuper@37934: | x mem (y :: ys) = x = y orelse x mem ys; neuper@37934: in neuper@37906: fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met = neuper@37906: (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"]; neuper@37906: *) neuper@37906: let val vat = max_vt pits; neuper@37906: val itms = pits @ neuper@37906: (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits); neuper@37906: val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris; neuper@37906: val os = filter_outs ors itms; neuper@37906: (*WN.12.03?: does _NOT_ add itms from met ?!*) neuper@37934: in itms @ (map (ori2Coritm met) os) end neuper@37934: end; neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*.complete model and guard of a calc-head .*) neuper@37936: local infix mem; neuper@37934: fun x mem [] = false neuper@37934: | x mem (y :: ys) = x = y orelse x mem ys; neuper@37934: in neuper@37906: fun complete_mod_ (oris, mpc, ppc, probl) = neuper@37906: let val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl neuper@37906: val vat = if probl = [] then 1 else max_vt probl neuper@37906: val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris neuper@37906: val pors = filter_outs pors pits (*which are in pbl already*) neuper@37906: val pors = (filter_pbt pors ppc) (*which are in pbt, too*) neuper@37906: neuper@37906: val pits = pits @ (map (ori2Coritm ppc) pors) neuper@37906: val mits = complete_metitms oris pits [] mpc neuper@37934: in (pits, mits) end neuper@37934: end; neuper@37906: neuper@37906: fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) = neuper@37906: (if dI = e_domID then odI else dI, neuper@37906: if pI = e_pblID then opI else pI, neuper@37906: if mI = e_metID then omI else mI):spec; neuper@37906: neuper@37906: neuper@37906: (*.find a next applicable tac (for calcstate) and update ptree neuper@37906: (for ev. finding several more tacs due to hide).*) neuper@37906: (*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*) neuper@37906: (*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*) neuper@37906: (*WN.24.10.03 fun nxt_solv = ...................................??*) neuper@37906: fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) = neuper@37906: let neuper@37906: val (PblObj{origin=(oris,ospec,_),probl,spec,...}) = get_obj I pt p neuper@37906: val (dI,pI,mI) = some_spec ospec spec neuper@37934: val thy = assoc_thy dI neuper@37906: val mpc = (#ppc o get_met) mI (*just for reuse complete_mod_*) neuper@37906: val {cas,ppc,...} = get_pbt pI neuper@37906: val pbl = init_pbl ppc (*fill in descriptions*) neuper@37906: (*--------------if you think, this should be done by the Dialog neuper@37906: in the java front-end, search there for WN060225-modelProblem----*) neuper@37926: val (pbl,met) = case cas of NONE => (pbl,[]) neuper@37906: | _ => complete_mod_ (oris, mpc, ppc, probl) neuper@37906: (*----------------------------------------------------------------*) neuper@37906: val tac_ = Model_Problem' (pI, pbl, met) neuper@37906: val (pos,c,_,pt) = generate1 thy tac_ Uistate pos pt neuper@37906: in ([(tac,tac_, (pos, Uistate))], c, (pt,pos)):calcstate' end neuper@37906: neuper@37906: (* val Add_Find ct = tac; neuper@37906: *) 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@37906: neuper@37906: (*. called only if no_met is specified .*) neuper@37906: | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) = neuper@37906: let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p neuper@37906: val opt = refine_ori oris pI neuper@37906: in case opt of neuper@37926: SOME pI' => neuper@37906: let val {met,ppc,...} = get_pbt pI' neuper@37906: val pbl = init_pbl ppc neuper@37906: (*val pt = update_pbl pt p pbl ..done by Model_Problem*) neuper@37906: val mI = if length met = 0 then e_metID else hd met neuper@37934: val thy = assoc_thy dI neuper@37906: val (pos,c,_,pt) = neuper@37906: generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[])) neuper@37906: Uistate pos pt neuper@37906: in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]), neuper@37906: (pos, Uistate))], c, (pt,pos)) end neuper@37926: | NONE => ([], [], ptp) neuper@37906: end neuper@37906: neuper@37906: | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) = neuper@37906: let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_), neuper@37906: probl, ...}) = get_obj I pt p neuper@37906: val thy = if dI' = e_domID then dI else dI' neuper@37906: in case refine_pbl (assoc_thy thy) pI probl of neuper@37926: NONE => ([], [], ptp) neuper@37926: | SOME (rfd as (pI',_)) => neuper@37906: let val (pos,c,_,pt) = neuper@37906: generate1 (assoc_thy thy) neuper@37906: (Refine_Problem' rfd) Uistate pos pt neuper@37906: in ([(Refine_Problem pI, Refine_Problem' rfd, neuper@37906: (pos, Uistate))], c, (pt,pos)) end neuper@37906: end neuper@37906: neuper@37906: | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) = neuper@37906: let val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), neuper@37906: probl, ...}) = get_obj I pt p; neuper@37906: val thy = assoc_thy (if dI' = e_domID then dI else dI'); neuper@37906: val {ppc,where_,prls,...} = get_pbt pI neuper@37906: val pbl as (_,(itms,_)) = neuper@37906: if pI'=e_pblID andalso pI=e_pblID neuper@37906: then (false, (init_pbl ppc, [])) neuper@37906: else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*) neuper@37906: (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*) neuper@37906: val ((p,Pbl),c,_,pt)= neuper@37906: generate1 thy (Specify_Problem' (pI, pbl)) Uistate pos pt neuper@37906: in ([(Specify_Problem pI, Specify_Problem' (pI, pbl), neuper@37906: (pos,Uistate))], c, (pt,pos)) end neuper@37906: neuper@37906: (*transfers oris (not required in pbl) to met-model for script-env neuper@37906: FIXME.WN.8.03: application of several mIDs to SAME model?*) neuper@37906: | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) = neuper@37906: let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI), neuper@37906: meth=met, ...}) = get_obj I pt p; neuper@37906: val {ppc,pre,prls,...} = get_met mID neuper@37906: val thy = assoc_thy dI neuper@37906: val oris = add_field' thy ppc oris; neuper@37906: val dI'' = if dI=e_domID then dI' else dI; neuper@37906: val pI'' = if pI = e_pblID then pI' else pI; neuper@37906: val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*) neuper@37906: val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris; neuper@37906: val (pos,c,_,pt)= neuper@37906: generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt neuper@37906: in ([(Specify_Method mID, Specify_Method' (mID, oris, itms), neuper@37906: (pos,Uistate))], c, (pt,pos)) end neuper@37906: neuper@37906: | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) = neuper@37906: let val (dI',_,_) = get_obj g_spec pt p neuper@37906: val (pos,c,_,pt) = neuper@37906: generate1 (assoc_thy "Isac.thy") (Specify_Theory' dI) neuper@37906: Uistate pos pt neuper@37906: in (*FIXXXME: check if pbl can still be parsed*) neuper@37906: ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c, neuper@37906: (pt, pos)) end neuper@37906: neuper@37906: | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) = neuper@37906: let val (dI',_,_) = get_obj g_spec pt p neuper@37906: val (pos,c,_,pt) = neuper@37906: generate1 (assoc_thy "Isac.thy") (Specify_Theory' dI) neuper@37906: Uistate pos pt neuper@37906: in (*FIXXXME: check if met can still be parsed*) neuper@37906: ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c, neuper@37906: (pt, pos)) end neuper@37906: neuper@37906: | nxt_specif m' _ = neuper@37906: raise error ("nxt_specif: not impl. for "^tac2str m'); neuper@37906: neuper@37906: (*.get the values from oris; handle the term list w.r.t. penv.*) neuper@37934: neuper@37936: local infix mem; neuper@37934: fun x mem [] = false neuper@37934: | x mem (y :: ys) = x = y orelse x mem ys; neuper@37934: in neuper@37906: fun vals_of_oris oris = neuper@37906: ((map (mkval' o (#5:ori -> term list))) o neuper@37934: (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris neuper@37934: end; neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*.create a calc-tree with oris via an cas.refined pbl.*) neuper@37906: fun nxt_specify_init_calc (([],(dI,pI,mI)): fmz) = neuper@37906: (* val ([],(dI,pI,mI)) = (fmz, sp); neuper@37906: *) neuper@37906: if pI <> [] then (*comes from pbl-browser*) neuper@37906: let val {cas,met,ppc,thy,...} = get_pbt pI neuper@37906: val dI = if dI = "" then theory2theory' thy else dI neuper@37906: val thy = assoc_thy dI neuper@37906: val mI = if mI = [] then hd met else mI neuper@37926: val hdl = case cas of NONE => pblterm dI pI | SOME t => t neuper@37906: val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI)) neuper@37906: ([], (dI,pI,mI), hdl) neuper@37906: val pt = update_spec pt [] (dI,pI,mI) neuper@37906: val pits = init_pbl' ppc neuper@37906: val pt = update_pbl pt [] pits neuper@37906: in ((pt,([],Pbl)), []): calcstate end neuper@37906: else if mI <> [] then (*comes from met-browser*) neuper@37906: let val {ppc,...} = get_met mI neuper@37906: val dI = if dI = "" then "Isac.thy" else dI neuper@37906: val thy = assoc_thy dI neuper@37906: val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI)) neuper@37906: ([], (dI,pI,mI), e_term(*FIXME met*)) neuper@37906: val pt = update_spec pt [] (dI,pI,mI) neuper@37906: val mits = init_pbl' ppc neuper@37906: val pt = update_met pt [] mits neuper@37906: in ((pt,([],Met)), []) end neuper@37906: else (*completely new example*) neuper@37906: let val (pt,_) = cappend_problem e_ptree [] e_istate ([], e_spec) neuper@37906: ([], e_spec, e_term) neuper@37906: in ((pt,([],Pbl)), []) end neuper@37906: (* val (fmz, (dI,pI,mI)) = (fmz, sp); neuper@37906: *) neuper@37906: | nxt_specify_init_calc (fmz:fmz_,(dI,pI,mI):spec) = neuper@37906: let (* either """"""""""""""" all empty or complete *) neuper@37906: val thy = assoc_thy dI neuper@37906: val (pI, pors, mI) = neuper@37906: if mI = ["no_met"] neuper@37906: then let val pors = prep_ori fmz thy ((#ppc o get_pbt) pI) neuper@37906: val pI' = refine_ori' pors pI; neuper@37906: in (pI', pors (*refinement over models with diff.prec only*), neuper@37906: (hd o #met o get_pbt) pI') end neuper@37906: else (pI, prep_ori fmz thy ((#ppc o get_pbt) pI), mI) neuper@37906: val {cas,ppc,thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*) neuper@37906: val dI = theory2theory' (maxthy thy thy'); neuper@37906: val hdl = case cas of neuper@37926: NONE => pblterm dI pI neuper@37926: | SOME t => subst_atomic ((vars_of_pbl_' ppc) neuper@37906: ~~~ vals_of_oris pors) t neuper@37906: val (pt,_) = cappend_problem e_ptree [] e_istate (fmz,(dI,pI,mI)) neuper@37906: (pors,(dI,pI,mI),hdl) neuper@37906: (*val pbl = init_pbl ppc WN.9.03: done by Model/Refine_Problem neuper@37906: val pt = update_pbl pt [] pbl*) neuper@37906: in ((pt,([],Pbl)), fst3 (nxt_specif Model_Problem (pt, ([],Pbl)))) neuper@37906: end; neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*18.12.99*) neuper@37906: fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) = neuper@37906: (* case appl_spec p pt m of /// 19.1.00 neuper@37906: Notappl e => Error' (Error_ e) neuper@37906: | Appl => neuper@37906: *) let val (_,_,f,_,_,_) = specify m (p,p_) [] pt neuper@37906: in f end; neuper@37906: neuper@37906: neuper@37938: (*fun tag_form thy (formal, given) = cterm_of thy neuper@37934: (((head_of o term_of) given) $ (term_of formal)); WN100819*) neuper@37934: fun tag_form thy (formal, given) = neuper@37934: (let val gf = (head_of given) $ formal; neuper@37938: val _ = cterm_of thy gf neuper@37934: in gf end) neuper@37934: handle _ => raise error ("calchead.tag_form: " ^ neuper@37934: Syntax.string_of_term (thy2ctxt thy) given ^ neuper@37934: " .. " ^ neuper@37934: Syntax.string_of_term (thy2ctxt thy) formal ^ neuper@37934: " ..types do not match"); neuper@37906: (* val formal = (the o (parse thy)) "[R::real]"; neuper@37906: > val given = (the o (parse thy)) "fixed_values (cs::real list)"; neuper@37906: > tag_form thy (formal, given); neuper@37906: val it = "fixed_values [R]" : cterm neuper@37906: *) neuper@37906: fun chktyp thy (n, fs, gs) = neuper@37934: ((writeln o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) fs; neuper@37934: (writeln o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) gs; neuper@37906: tag_form thy (nth n fs, nth n gs)); neuper@37906: neuper@37906: fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs); neuper@37906: neuper@37906: (* ##################################################### neuper@37906: find the failing item: neuper@37906: > val n = 2; neuper@37906: > val tag__form = chktyp (n,formals,givens); neuper@37906: > (type_of o term_of o (nth n)) formals; neuper@37906: > (type_of o term_of o (nth n)) givens; neuper@37906: > atomty ((term_of o (nth n)) formals); neuper@37906: > atomty ((term_of o (nth n)) givens); neuper@37906: > atomty (term_of tag__form); neuper@37906: > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl"; neuper@37906: ##################################################### *) neuper@37906: neuper@37906: (* ##################################################### neuper@37906: testdata setup neuper@37906: val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"]; neuper@37906: val formals = map (the o (parse thy)) origin; neuper@37906: neuper@37906: val given = ["equation (lhs=rhs)", neuper@37906: "bound_variable bdv", (* TODO type *) neuper@37906: "error_bound apx"]; neuper@37906: val where_ = ["e is_root_equation_in bdv", neuper@37906: "bdv is_var", neuper@37906: "apx is_const_expr"]; neuper@37906: val find = ["L::rat set"]; neuper@37906: val with_ = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"]; neuper@37906: val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); neuper@37906: val givens = map (the o (parse thy)) given; neuper@37906: neuper@37906: val tag__forms = chktyps (formals, givens); neuper@37906: map ((atomty) o term_of) tag__forms; neuper@37906: ##################################################### *) neuper@37906: neuper@37906: neuper@37906: (* check pbltypes, announces one failure a time *) neuper@37930: (*fun chk_vars ctppc = neuper@37906: let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} = neuper@37906: appc flat (mappc (vars o term_of) ctppc) neuper@37906: in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi) neuper@37906: else if (re\\(gi union fi)) <> [] neuper@37906: then ("re\\(gi union fi)",re\\(gi union fi)) neuper@37930: else ("ok",[]) end;*) neuper@37930: fun chk_vars ctppc = neuper@37930: let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} = neuper@37934: appc flat (mappc vars ctppc) neuper@37932: val chked = subtract op = gi wh neuper@37932: in if chked <> [] then ("wh\\gi", chked) neuper@37930: else let val chked = subtract op = (union op = gi fi) re neuper@37932: in if chked <> [] neuper@37932: then ("re\\(gi union fi)", chked) neuper@37932: else ("ok", []) neuper@37932: end neuper@37932: end; neuper@37906: neuper@37906: (* check a new pbltype: variables (Free) unbound by given, find*) neuper@37906: fun unbound_ppc ctppc = neuper@37906: let val {Given=gi,Find=fi,Relate=re,...} = neuper@37934: appc flat (mappc vars ctppc) neuper@37930: in distinct (*re\\(gi union fi)*) neuper@37930: (subtract op = (union op = gi fi) re) end; neuper@37906: (* neuper@37906: > val org = {Given=["[R=(R::real)]"],Where=[], neuper@37906: Find=["[A::real]"],With=[], neuper@37906: Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"] neuper@37906: }:string ppc; neuper@37906: > val ctppc = mappc (the o (parse thy)) org; neuper@37906: > unbound_ppc ctppc; neuper@37906: val it = [("a","RealDef.real"),("b","RealDef.real")] : (string * typ) list neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: (* f, a binary operator, is nested rightassociative *) neuper@37906: fun foldr1 f xs = neuper@37906: let neuper@37906: fun fld f (x::[]) = x neuper@37906: | fld f (x::x'::[]) = f (x',x) neuper@37906: | fld f (x::x'::xs) = f (fld f (x'::xs),x); neuper@37906: in ((fld f) o rev) xs end; neuper@37906: (* neuper@37926: > val (SOME ct) = parse thy "[a=b,c=d,e=f]"; neuper@37938: > val ces = map (cterm_of thy) (isalist2list (term_of ct)); neuper@37906: > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct)); neuper@37938: > cterm_of thy conj; neuper@37906: val it = "(a = b & c = d) & e = f" : cterm neuper@37906: *) neuper@37906: neuper@37906: (* f, a binary operator, is nested leftassociative *) neuper@37906: fun foldl1 f (x::[]) = x neuper@37906: | foldl1 f (x::x'::[]) = f (x,x') neuper@37906: | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs)); neuper@37906: (* neuper@37926: > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]"; neuper@37938: > val ces = map (cterm_of thy) (isalist2list (term_of ct)); neuper@37906: > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct)); neuper@37938: > cterm_of thy conj; neuper@37906: val it = "a = b & c = d & e = f & g = h" : cterm neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: (* called only once, if a Subproblem has been located in the script*) neuper@37906: fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp = neuper@37906: (* val (Subproblem'((_,pblID,metID),_,_,_,_),ptp) = (m', (pt,(p,p_))); neuper@37906: *) neuper@37906: (case metID of neuper@37906: ["no_met"] => neuper@37906: (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp) neuper@37906: | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp)) neuper@37906: (*all stored in tac_ itms ^^^^^^^^^^*) neuper@37906: | nxt_model_pbl tac_ _ = neuper@37906: raise error ("nxt_model_pbl: called by tac= "^tac_2str tac_); neuper@37906: (* run subp_rooteq.sml '' neuper@37906: until nxt=("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"])) neuper@37906: > val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) = neuper@37906: (last_elem o drop_last) ets''; neuper@37906: > val mst = (last_elem o drop_last) ets''; neuper@37906: > nxt_model_pbl mst; neuper@37906: val it = Refine_Tacitly ["univariate","equation"] : tac neuper@37906: *) neuper@37906: neuper@37906: (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*) neuper@37934: fun eq4 v (_,vts,_,_,_) = member op = vts v; neuper@37906: fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d; neuper@37906: neuper@37906: neuper@37906: neuper@37906: (* neuper@37906: writeln (oris2str pors); neuper@37906: neuper@37924: writeln (itms2str_ thy pits); neuper@37924: writeln (itms2str_ thy mits); neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris neuper@37906: + met from fmz; assumes pos on PblObj, meth = [].*) neuper@37906: fun complete_mod (pt, pos as (p, p_):pos') = neuper@37906: (* val (pt, (p, _)) = (pt, p); neuper@37906: val (pt, (p, _)) = (pt, pos); neuper@37906: *) neuper@37906: let val _= if p_ <> Pbl neuper@37906: then writeln("###complete_mod: only impl.for Pbl, called with "^ neuper@37906: pos'2str pos) else () neuper@37906: val (PblObj{origin=(oris, ospec, hdl), probl, spec,...}) = neuper@37906: get_obj I pt p neuper@37906: val (dI,pI,mI) = some_spec ospec spec neuper@37906: val mpc = (#ppc o get_met) mI neuper@37906: val ppc = (#ppc o get_pbt) pI neuper@37906: val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl) neuper@37906: val pt = update_pblppc pt p pits neuper@37906: val pt = update_metppc pt p mits neuper@37906: in (pt, (p,Met):pos') end neuper@37906: ; neuper@37906: (*| complete_mod (pt, pos as (p, Met):pos') = neuper@37906: raise error ("###complete_mod: only impl.for Pbl, called with "^ neuper@37906: pos'2str pos);*) 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 .*) neuper@37906: fun all_modspec (pt, (p,_):pos') = neuper@37906: (* val (pt, (p,_)) = ptp; neuper@37906: *) neuper@37906: let val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl), neuper@37906: ...}) = get_obj I pt p; neuper@37906: val thy = assoc_thy dI; neuper@37906: val {ppc,...} = get_met mI; neuper@37906: val mors = prep_ori fmz_ thy ppc; neuper@37906: val pt = update_pblppc pt p (map (ori2Coritm ppc) pors); neuper@37906: val pt = update_metppc pt p (map (ori2Coritm ppc) mors); neuper@37906: val pt = update_spec pt p (dI,pI,mI); neuper@37906: in (pt, (p,Met): pos') end; neuper@37906: neuper@37906: (*WN.12.03: use in nxt_spec, too ? what about variants ???*) neuper@37906: fun is_complete_mod_ ([]: itm list) = false neuper@37906: | is_complete_mod_ itms = neuper@37906: foldl and_ (true, (map #3 itms)); neuper@37906: fun is_complete_mod (pt, pos as (p, Pbl): pos') = neuper@37906: if (is_pblobj o (get_obj I pt)) p neuper@37906: then (is_complete_mod_ o (get_obj g_pbl pt)) p neuper@37906: else raise error ("is_complete_mod: called by PrfObj at "^pos'2str pos) neuper@37906: | is_complete_mod (pt, pos as (p, Met)) = neuper@37906: if (is_pblobj o (get_obj I pt)) p neuper@37906: then (is_complete_mod_ o (get_obj g_met pt)) p neuper@37906: else raise error ("is_complete_mod: called by PrfObj at "^pos'2str pos) neuper@37906: | is_complete_mod (_, pos) = neuper@37906: raise error ("is_complete_mod called by "^pos'2str pos^ neuper@37906: " (should be Pbl or Met)"); neuper@37906: neuper@37906: (*.have (thy, pbl, met) _all_ been specified explicitly ?.*) neuper@37906: fun is_complete_spec (pt, pos as (p,_): pos') = neuper@37906: if (not o is_pblobj o (get_obj I pt)) p neuper@37906: then raise error ("is_complete_spec: called by PrfObj at "^pos'2str pos) neuper@37906: else let val (dI,pI,mI) = get_obj g_spec pt p neuper@37906: in dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID end; neuper@37906: (*.complete empty items in specification from origin (pbl, met ev.refined); neuper@37906: assumes 'is_complete_mod'.*) neuper@37906: fun complete_spec (pt, pos as (p,_): pos') = neuper@37906: let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p neuper@37906: val pt = update_spec pt p (some_spec ospec spec) neuper@37906: in (pt, pos) end; neuper@37906: neuper@37906: fun is_complete_modspec ptp = neuper@37906: is_complete_mod ptp andalso is_complete_spec ptp; neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met = neuper@37906: (* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_); neuper@37906: *) neuper@37906: let val (_,_,metID) = get_somespec' spec spec' neuper@37906: val pre = neuper@37906: if metID = e_metID then [] neuper@37906: else let val {prls,pre=where_,...} = get_met metID neuper@37906: val pre = check_preconds' prls where_ meth 0 neuper@37906: in pre end neuper@37906: val allcorrect = is_complete_mod_ meth neuper@37906: andalso foldl and_ (true, (map #1 pre)) neuper@37906: in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end neuper@37906: | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) = neuper@37906: (* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_); neuper@37906: *) neuper@37906: let val (_,pI,_) = get_somespec' spec spec' neuper@37906: val pre = neuper@37906: if pI = e_pblID then [] neuper@37906: else let val {prls,where_,cas,...} = get_pbt pI neuper@37906: val pre = check_preconds' prls where_ probl 0 neuper@37906: in pre end neuper@37906: val allcorrect = is_complete_mod_ probl neuper@37906: andalso foldl and_ (true, (map #1 pre)) neuper@37906: in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end; neuper@37906: neuper@37906: neuper@37906: fun pt_form (PrfObj {form,...}) = Form form neuper@37906: | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) = neuper@37906: let val (dI, pI, _) = get_somespec' spec spec' neuper@37906: val {cas,...} = get_pbt pI neuper@37906: in case cas of neuper@37926: NONE => Form (pblterm dI pI) neuper@37926: | SOME t => Form (subst_atomic (mk_env probl) t) neuper@37906: end; neuper@37906: (*vvv takes the tac _generating_ the formula=result, asm ok.... neuper@37906: fun pt_result (PrfObj {result=(t,asm), tac,...}) = neuper@37906: (Form t, neuper@37926: if null asm then NONE else SOME asm, neuper@37926: SOME tac) neuper@37906: | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) = neuper@37906: let val (_,_,metID) = some_spec ospec spec neuper@37906: in (Form t, neuper@37926: if null asm then NONE else SOME asm, neuper@37926: if metID = e_metID then NONE else SOME (Apply_Method metID)) end; neuper@37906: -------------------------------------------------------------------------*) neuper@37906: neuper@37906: neuper@37906: (*.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 !) neuper@37906: pos is assumed to come from the frontend, ie. generated by moveDown.*) neuper@37906: (*cannot be in ctree.sml, because ModSpec has to be calculated*) neuper@37906: fun pt_extract (pt,([],Res)) = neuper@37906: (* val (pt,([],Res)) = ptp; neuper@37906: *) neuper@37906: let val (f, asm) = get_obj g_result pt [] neuper@37926: in (Form f, NONE, asm) end neuper@37906: (* val p = [3,2]; neuper@37906: *) neuper@37906: | pt_extract (pt,(p,Res)) = neuper@37906: (* val (pt,(p,Res)) = ptp; neuper@37906: *) neuper@37906: let val (f, asm) = get_obj g_result pt p neuper@37906: val tac = if last_onlev pt p neuper@37906: then if is_pblobj' pt (lev_up p) neuper@37906: then let val (PblObj{spec=(_,pI,_),...}) = neuper@37906: get_obj I pt (lev_up p) neuper@37926: in if pI = e_pblID then NONE neuper@37926: else SOME (Check_Postcond pI) end neuper@37926: else SOME End_Trans (*WN0502 TODO for other branches*) neuper@37906: else let val p' = lev_on p neuper@37906: in if is_pblobj' pt p' neuper@37906: then let val (PblObj{origin = (_,(dI,pI,_),_),...}) = neuper@37906: get_obj I pt p' neuper@37926: in SOME (Subproblem (dI, pI)) end neuper@37906: else if f = get_obj g_form pt p' neuper@37926: then SOME (get_obj g_tac pt p') neuper@37906: (*because this Frm ~~~is not on worksheet*) neuper@37926: else SOME (Take (term2str (get_obj g_form pt p'))) neuper@37906: end neuper@37906: in (Form f, tac, asm) end neuper@37906: neuper@37906: | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) = neuper@37906: (* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp; neuper@37906: val (pt, pos as (p,p_(*Frm,Pbl*))) = (pt, p); neuper@37906: *) neuper@37906: let val ppobj = get_obj I pt p neuper@37906: val f = if is_pblobj ppobj then pt_model ppobj p_ neuper@37906: else get_obj pt_form pt p neuper@37906: val tac = g_tac ppobj neuper@37926: in (f, SOME tac, []) end; neuper@37906: neuper@37906: neuper@37906: (**. get the formula from a ctree-node: neuper@37906: take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj) neuper@37906: take res from all other PrfObj's .**) neuper@37906: (*designed for interSteps, outcommented 04 in favour of calcChangedEvent*) neuper@37906: fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) = neuper@37906: [("headline", (p, Frm), h), neuper@37906: ("stepform", (p, Res), r)] neuper@37906: | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) = neuper@37906: [("stepform", (p, Frm), form), neuper@37906: ("stepform", (p, Res), r)]; neuper@37906: neuper@37906: fun form p (Nd (PrfObj {result = (r, _),...}, _)) = neuper@37906: [("stepform", (p, Res), r)] neuper@37906: neuper@37906: (*assumes to take whole level, in particular hd -- for use in interSteps*) neuper@37906: fun get_formress fs p [] = 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 neuper@37906: and get_forms fs p [] = 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: neuper@37906: (**.get an 'interval' 'from' 'to' of formulae from a ptree.**) neuper@37906: (*WN050219 made robust against _'to' below or after Complete nodes neuper@37906: by handling exn caused by move_dn*) neuper@37906: (*WN0401 this functionality belongs to ctree.sml, neuper@37906: but fetching a calc_head requires calculations defined in modspec.sml neuper@37906: transfer to ME/me.sml !!! neuper@37906: WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head neuper@37906: is returned !!!!!!!!!!!!! neuper@37906: *) neuper@37906: fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2 neuper@37906: | eq_pos' (p1,Res) (p2,Res) = p1 = p2 neuper@37906: | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of neuper@37906: Pbl => true neuper@37906: | Met => true neuper@37906: | _ => false) neuper@37906: | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of neuper@37906: Pbl => true neuper@37906: | Met => true neuper@37906: | _ => false) neuper@37906: | eq_pos' _ _ = false; neuper@37906: neuper@37906: (*.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 neuper@37906: ptree -> : neuper@37906: (pos' * : of the formula neuper@37906: Term.term) : the formula neuper@37906: list neuper@37906: .*) neuper@37906: fun get_interval from to level pt = neuper@37906: (* val (from,level) = (f,lev); neuper@37906: val (from, to, level) = (([3, 2, 1], Res), ([],Res), 9999); neuper@37906: *) neuper@37906: let fun get_inter c (from:pos') (to:pos') lev pt = neuper@37906: (* val (c, from, to, lev) = ([], from, to, level); neuper@37906: ------for recursion....... neuper@37906: val (c, from:pos', to:pos') = (c @ [(from, f)], move_dn [] pt from, to); neuper@37906: *) neuper@37906: if eq_pos' from to orelse from = ([],Res) neuper@37906: (*orelse ... avoids Exception- PTREE "end of calculation" raised, neuper@37906: if 'to' has values NOT generated by move_dn, see systest/me.sml neuper@37906: TODO.WN0501: introduce an order on pos' and check "from > to".. neuper@37906: ...there is an order in Java! neuper@37906: WN051224 the hack got worse with returning term instead ptform*) neuper@37906: then let val (f,_,_) = pt_extract (pt, from) neuper@37906: in case f of neuper@37906: ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)] neuper@37906: | Form t => c @ [(from, t)] neuper@37906: end neuper@37906: else neuper@37906: if lev < lev_of from neuper@37906: then (get_inter c (move_dn [] pt from) to lev pt) neuper@37906: handle (PTREE _(*from move_dn too far*)) => c neuper@37906: else let val (f,_,_) = pt_extract (pt, from) neuper@37906: val term = case f of neuper@37906: ModSpec (_,_,headline,_,_,_)=> headline neuper@37906: | Form t => t neuper@37906: in (get_inter (c @ [(from, term)]) neuper@37906: (move_dn [] pt from) to lev pt) neuper@37906: handle (PTREE _(*from move_dn too far*)) neuper@37906: => c @ [(from, term)] end neuper@37906: in get_inter [] from to level pt end; neuper@37906: neuper@37906: (*for tests*) neuper@37906: fun posform2str (pos:pos', form) = neuper@37906: "("^ pos'2str pos ^", "^ neuper@37906: (case form of neuper@37906: Form f => term2str f neuper@37906: | ModSpec c => term2str (#3 c(*the headline*))) neuper@37906: ^")"; neuper@37906: fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o neuper@37906: (map posform2str)) pfs; neuper@37906: fun posterm2str (pos:pos', t) = neuper@37906: "("^ pos'2str pos ^", "^term2str t^")"; neuper@37906: fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o neuper@37906: (map posterm2str)) pfs; neuper@37906: neuper@37906: neuper@37906: (*WN050225 omits the last step, if pt is incomplete*) neuper@37906: fun show_pt pt = neuper@37906: writeln (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt)); neuper@37906: neuper@37906: (*.get a calchead from a PblObj-node in the ctree; neuper@37906: preconditions must be calculated.*) neuper@37906: fun get_ocalhd (pt, pos' as (p,Pbl):pos') = neuper@37906: let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} = neuper@37906: get_obj I pt p neuper@37906: val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec)) neuper@37906: val pre = check_preconds (assoc_thy"Isac.thy") prls where_ probl neuper@37906: in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end neuper@37906: | get_ocalhd (pt, pos' as (p,Met):pos') = neuper@37906: let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), neuper@37906: spec, meth,...} = neuper@37906: get_obj I pt p neuper@37906: val {prls,pre,...} = get_met (#3 (some_spec ospec spec)) neuper@37906: val pre = check_preconds (assoc_thy"Isac.thy") prls pre meth neuper@37906: in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end; neuper@37906: neuper@37906: (*.at the activeFormula set the Model, the Guard and the Specification neuper@37906: to empty and return a CalcHead; neuper@37906: the 'origin' remains (for reconstructing all that).*) neuper@37906: fun reset_calchead (pt, pos' as (p,_):pos') = neuper@37906: let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p neuper@37906: val pt = update_pbl pt p [] neuper@37906: val pt = update_met pt p [] neuper@37906: val pt = update_spec pt p e_spec neuper@37906: in (pt, (p,Pbl):pos') end; neuper@37906: neuper@37906: (*---------------------------------------------------------------------*) neuper@37906: end neuper@37906: neuper@37906: open CalcHead; neuper@37906: (*---------------------------------------------------------------------*) neuper@37906: