diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/calchead.sml --- a/src/Tools/isac/Interpret/calchead.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Interpret/calchead.sml Thu Dec 22 11:36:20 2016 +0100 @@ -9,29 +9,29 @@ type calcstate' datatype appl = Appl of Ctree.tac_ | Notappl of string val nxt_specify_init_calc : Ctree.fmz -> calcstate - val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ptree -> - Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ptree - val nxt_specif : Ctree.tac -> Ctree.ptree * Ctree.pos' -> calcstate' + val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ctree -> + Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ctree + val nxt_specif : Ctree.tac -> Ctree.ctree * Ctree.pos' -> calcstate' val nxt_spec : Ctree.pos_ -> bool -> ori list -> spec -> itm list * itm list -> (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Ctree.tac - val reset_calchead : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' - val get_ocalhd : Ctree.ptree * Ctree.pos' -> Ctree.ocalhd + val reset_calchead : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' + val get_ocalhd : Ctree.ctree * Ctree.pos' -> Ctree.ocalhd val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool - val all_modspec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' + val all_modspec : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list val insert_ppc' : itm -> itm list -> itm list - val complete_mod : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' - val is_complete_mod : Ctree.ptree * Ctree.pos' -> bool - val complete_spec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' - val is_complete_spec : Ctree.ptree * Ctree.pos' -> bool + val complete_mod : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' + val is_complete_mod : Ctree.ctree * Ctree.pos' -> bool + val complete_spec : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' + val is_complete_spec : Ctree.ctree * Ctree.pos' -> bool val some_spec : spec -> spec -> spec (* these could go to Ctree ..*) - val show_pt : Ctree.ptree -> unit - val pt_extract : Ctree.ptree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list - val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ptree -> (Ctree.pos' * term) list + val show_pt : Ctree.ctree -> unit + val pt_extract : Ctree.ctree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list + val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ctree -> (Ctree.pos' * term) list val match_ags : theory -> pat list -> term list -> ori list val match_ags_msg : pblID -> term -> term list -> unit @@ -68,7 +68,7 @@ this state just by "fun generate " *) type calcstate = - (ptree * pos') * (* the calc-state to which the tacis could be applied *) + (ctree * pos') * (* the calc-state to which the tacis could be applied *) (Generate.taci list) (* ev. several (hidden) steps; in REVERSE order: first tac_ to apply is last_elem *) val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]) : calcstate; @@ -86,7 +86,7 @@ Generate.taci list * (* cas. several (hidden) steps; in REVERSE order: first tac_ to apply is last_elem *) pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *) - (ptree * pos') (* the calc-state resulting from the application of tacis *) + (ctree * pos') (* the calc-state resulting from the application of tacis *) val e_calcstate' = ([Generate.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate'; (* FIXXXME.WN020430 intermediate hack for fun ass_up *) @@ -697,7 +697,7 @@ if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*) then ([], e_ctxt) else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy - val (pt, _) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz, spec') + val (pt, _) = cappend_problem e_ctree [] (e_istate, ctxt) (fmz, spec') (oris, (dI',pI',mI'), e_term) val pt = update_ctxt pt [] ctxt val (pbl, pre) = ([], []) @@ -951,7 +951,7 @@ if pI = e_pblID then opI else pI, if mI = e_metID then omI else mI) : spec -(* find a next applicable tac (for calcstate) and update ptree +(* find a next applicable tac (for calcstate) and update ctree (for ev. finding several more tacs due to hide) *) (* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *) (* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *) @@ -1087,7 +1087,7 @@ val dI = if dI = "" then theory2theory' thy else dI val mI = if mI = [] then hd met else mI val hdl = case cas of NONE => pblterm dI pI | SOME t => t - val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI, pI, mI)) + val (pt,_) = cappend_problem e_ctree [] (Uistate, e_ctxt) ([], (dI, pI, mI)) ([], (dI,pI,mI), hdl) val pt = update_spec pt [] (dI, pI, mI) val pits = Generate.init_pbl' ppc @@ -1100,7 +1100,7 @@ val {ppc, ...} = Specify.get_met mI val dI = if dI = "" then "Isac" else dI val (pt, _) = - cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*)) + cappend_problem e_ctree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*)) val pt = update_spec pt [] (dI, pI, mI) val mits = Generate.init_pbl' ppc val pt = update_met pt [] mits @@ -1108,7 +1108,7 @@ else (* new example, pepare for interactive modeling *) let val (pt, _) = - cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term) + cappend_problem e_ctree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term) in ((pt, ([], Pbl)), []) end | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) = let (* both """"""""""""""""""""""""" either empty or complete *) @@ -1129,7 +1129,7 @@ NONE => pblterm dI pI | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t val (pt, _) = - cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl) + cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl) val pt = update_ctxt pt [] pctxt in ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate @@ -1396,7 +1396,7 @@ (* continue with trying 'res' only*) else get_forms (fs @ [form p nd]) (lev_on p) nds; -(** get an 'interval' 'from' 'to' of formulae from a ptree **) +(** get an 'interval' 'from' 'to' of formulae from a ctree **) (* WN0401 this functionality belongs to ctree.sml *) fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2 | eq_pos' (p1, Res) (p2, Res) = p1 = p2 @@ -1413,7 +1413,7 @@ pos' -> : to the last element to be returned; from < to int -> : level: 0 gets the flattest sub-tree possible >999 gets the deepest sub-tree possible - ptree -> : + ctree -> : (pos' * : of the formula Term.term) : the formula list *)