1.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu May 14 09:30:40 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu May 14 13:33:47 2020 +0200
1.3 @@ -22,10 +22,10 @@
1.4 val keref2xml : int -> Ptool.ketype -> Ptool.kestoreID -> xml
1.5 val model2xml :
1.6 int -> I_Model.T -> (bool * Term.term) list -> xml
1.7 - val modspec2xml : int -> Ctree.ocalhd -> xml
1.8 + val modspec2xml : int -> Specification.T -> xml
1.9 val pattern2xml : int -> Model_Pattern.T -> Term.term list -> string
1.10 val pos'2xml : int -> string * Pos.pos' -> string
1.11 - val pos'calchead2xml : int -> Pos.pos' * Ctree.ocalhd -> xml
1.12 + val pos'calchead2xml : int -> Pos.pos' * Specification.T -> xml
1.13 val pos_2xml : int -> Pos.pos_ -> string
1.14 val posform2xml : int -> Pos.pos' * Term.term -> xml
1.15 val posformhead2xml : int -> Pos.pos' * Ctree.ptform -> string
1.16 @@ -402,7 +402,7 @@
1.17 fun xml_to_fmz (XML.Elem (("FORMALIZATION", []), vars)) = map xml_to_variant vars
1.18 | xml_to_fmz tree = raise ERROR ("xml_to_fmz: wrong XML.tree \n" ^ xmlstr 0 tree)
1.19
1.20 -fun xml_of_modspec ((b, p_, head, gfr, pre, spec): Ctree.ocalhd) =
1.21 +fun xml_of_modspec ((b, p_, head, gfr, pre, spec): Specification.T) =
1.22 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
1.23 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
1.24 xml_of_model gfr pre,
1.25 @@ -410,7 +410,7 @@
1.26 XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
1.27 xml_of_spec spec])
1.28
1.29 -fun xml_of_posmodspec ((p: Pos.pos', (b, p_, head, gfr, pre, spec): Ctree.ocalhd)) =
1.30 +fun xml_of_posmodspec ((p: Pos.pos', (b, p_, head, gfr, pre, spec): Specification.T)) =
1.31 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
1.32 xml_of_pos "POSITION" p,
1.33 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Thu May 14 09:30:40 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Thu May 14 13:33:47 2020 +0200
2.3 @@ -158,7 +158,7 @@
2.4 " <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
2.5 "@@@@@end@@@@@");
2.6
2.7 -fun modifycalcheadOK2xml (calcid : calcID) (chd as (complete, p_ ,_ ,_ ,_ ,_) : Ctree.ocalhd) =
2.8 +fun modifycalcheadOK2xml (calcid : calcID) (chd as (complete, p_ ,_ ,_ ,_ ,_) : Specification.T) =
2.9 XML.Elem (("MODIFYCALCHEAD", []), [
2.10 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
2.11 XML.Elem (("STATUS", []), [
3.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Thu May 14 09:30:40 2020 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Thu May 14 13:33:47 2020 +0200
3.3 @@ -192,7 +192,7 @@
3.4 fun getTactic cI (p:pos') =
3.5 (let
3.6 val ((pt, _), _) = get_calc cI
3.7 - val (_, tac, _) = Chead.pt_extract (pt, p)
3.8 + val (_, tac, _) = Specification.pt_extract (pt, p)
3.9 in
3.10 case tac of
3.11 SOME ta => gettacticOK2xml cI ta
3.12 @@ -217,7 +217,7 @@
3.13 fun getAssumptions cI (p:pos') =
3.14 (let
3.15 val ((pt, _), _) = get_calc cI
3.16 - val (_, _, asms) = Chead.pt_extract (pt, p)
3.17 + val (_, _, asms) = Specification.pt_extract (pt, p)
3.18 in getasmsOK2xml cI asms end)
3.19 handle _ => sysERROR2xml cI "syserror in getAssumptions"
3.20
3.21 @@ -232,7 +232,7 @@
3.22 fun refFormula cI (p: pos') = (*WN0501 rename to "fun getElement" !*)
3.23 (let
3.24 val ((pt, _), _) = get_calc cI
3.25 - val (form, _, _) = Chead.pt_extract (pt, p)
3.26 + val (form, _, _) = Specification.pt_extract (pt, p)
3.27 in refformulaOK2xml cI p form end)
3.28 handle _ => sysERROR2xml cI ("error in kernel 6: refFormula " ^ int2str cI ^ " " ^ pos'2str p)
3.29
3.30 @@ -244,9 +244,9 @@
3.31 ((let
3.32 val ((pt,_),_) = get_calc cI
3.33 val headline =
3.34 - case Chead.pt_extract (pt, to) of
3.35 + case Specification.pt_extract (pt, to) of
3.36 (ModSpec (_, _, headline, _, _, _), _, _) => headline
3.37 - | _ => raise ERROR "getFormulaeFromTo: uncovered case of Chead.pt_extract"
3.38 + | _ => raise ERROR "getFormulaeFromTo: uncovered case of Specification.pt_extract"
3.39 in getintervalOK cI [(to, headline, NONE)] end)
3.40 handle _ => sysERROR2xml cI "error in kernel 7")
3.41 | getFormulaeFromTo cI ([], Pbl) ([], Met) _ false =
3.42 @@ -265,7 +265,7 @@
3.43 val f = move_dn [] pt from
3.44 fun max (a,b) = if a < b then b else a
3.45 val lev = max (level, max (lev_of from, lev_of to)) (*... must reach margins *)
3.46 - in getintervalOK cI (Chead.get_interval f to lev pt) end)
3.47 + in getintervalOK cI (Specification.get_interval f to lev pt) end)
3.48 handle _ => sysERROR2xml cI "error in getFormulaeFromTo")
3.49 | getFormulaeFromTo cI from to level true =
3.50 sysERROR2xml cI ("getFormulaeFromTo impl.for formulae only, " ^
3.51 @@ -300,17 +300,17 @@
3.52 fun resetCalcHead cI =
3.53 (let
3.54 val (ptp,_) = get_calc cI
3.55 - val ptp = Chead.reset_calchead ptp
3.56 - in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Chead.get_ocalhd ptp)) end)
3.57 + val ptp = Specification.reset_calchead ptp
3.58 + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Specification.get_ocalhd ptp)) end)
3.59 handle _ => sysERROR2xml cI "error in kernel 10";
3.60
3.61 (* at the activeFormula insert all the Descriptions in the Model and return a CalcHead;
3.62 the Descriptions are for user-guidance; the rest of the items are left empty for user-input *)
3.63 fun modelProblem cI =
3.64 (let val (ptp, _) = get_calc cI
3.65 - val ptp = Chead.reset_calchead ptp
3.66 + val ptp = Specification.reset_calchead ptp
3.67 val (_, _, ptp) = Step_Specify.by_tactic_input Tactic.Model_Problem ptp
3.68 - in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Chead.get_ocalhd ptp)) end)
3.69 + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Specification.get_ocalhd ptp)) end)
3.70 handle _ => sysERROR2xml cI "error in kernel 11";
3.71
3.72 (* set the UContext determined on a knowledgebrowser to the current calc
4.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu May 14 09:30:40 2020 +0200
4.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu May 14 13:33:47 2020 +0200
4.3 @@ -25,8 +25,8 @@
4.4 find_next_step calls do_next and is called by by_tactic;
4.5 by_tactic and do_next are mutually recursive via by_tactic..Apply_Method'
4.6 *)
4.7 - val by_tactic: Tactic.T -> Istate.T * Proof.context -> Calc.T -> string * Chead.calcstate'
4.8 - val do_next: Calc.T -> string * Chead.calcstate'
4.9 + val by_tactic: Tactic.T -> Istate.T * Proof.context -> Calc.T -> string * Specification.calcstate'
4.10 + val do_next: Calc.T -> string * Specification.calcstate'
4.11
4.12 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.13 datatype expr_val1 =
4.14 @@ -46,7 +46,7 @@
4.15 val check_tac: Calc.T * Proof.context -> Istate.pstate -> term * term option -> expr_val
4.16 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.17 val check_Let_up: Istate.pstate -> term -> term * term
4.18 - val compare_step: State_Steps.T * Pos.pos' list * Calc.T -> term -> string * Chead.calcstate'
4.19 + val compare_step: State_Steps.T * Pos.pos' list * Calc.T -> term -> string * Specification.calcstate'
4.20
4.21 val scan_dn1: (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1
4.22 val scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
4.23 @@ -504,7 +504,7 @@
4.24 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
4.25 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
4.26 val {ppc, ...} = Method.from_store mI;
4.27 - val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
4.28 + val itms = if itms <> [] then itms else Specification.complete_metitms oris probl [] ppc
4.29 val itms = Step_Specify.hack_until_review_Specify_1 mI itms
4.30 val srls = LItool.get_simplifier (pt, pos)
4.31 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
4.32 @@ -605,7 +605,7 @@
4.33 Tactic.End_Detail' res, (pos, (ist, ctxt)))], [], ptp))
4.34 | _ => (*.. RM*) by_tactic tac (ist, ctxt) ptp
4.35 )
4.36 - | Helpless => ("helpless", Chead.e_calcstate')
4.37 + | Helpless => ("helpless", Specification.e_calcstate')
4.38 end;
4.39
4.40 (*
4.41 @@ -630,14 +630,14 @@
4.42 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
4.43 else
4.44 if pos = ([], Pos.Res) (*TODO: we should stop earlier with trying subproblems *)
4.45 - then ("no derivation found", (tacis, c, ptp): Chead.calcstate')
4.46 + then ("no derivation found", (tacis, c, ptp): Specification.calcstate')
4.47 else
4.48 let
4.49 val msg_cs' as (_, (tacis, c', ptp)) = do_next ptp; (*<---------------------*)
4.50 val (_, (tacis, c'', ptp)) = case tacis of
4.51 ((Tactic.Subproblem _, _, _) :: _) =>
4.52 let
4.53 - val ptp as (pt, (p, _)) = Chead.all_modspec ptp (*<--------------------*)
4.54 + val ptp as (pt, (p, _)) = Specification.all_modspec ptp (*<--------------------*)
4.55 val mI = Ctree.get_obj Ctree.g_metID pt p
4.56 in
4.57 by_tactic (Tactic.Apply_Method' (mI, NONE, empty, ContextC.empty))
5.1 --- a/src/Tools/isac/Interpret/step-solve.sml Thu May 14 09:30:40 2020 +0200
5.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Thu May 14 13:33:47 2020 +0200
5.3 @@ -5,9 +5,9 @@
5.4
5.5 signature STEP_SOLVE =
5.6 sig
5.7 - val do_next: Calc.T -> string * Chead.calcstate'
5.8 - val by_tactic : Tactic.T -> Calc.T -> string * Chead.calcstate'
5.9 - val by_term : Calc.T -> string -> string * Chead.calcstate' (*TODO: string * Calc.T*)
5.10 + val do_next: Calc.T -> string * Specification.calcstate'
5.11 + val by_tactic : Tactic.T -> Calc.T -> string * Specification.calcstate'
5.12 + val by_term : Calc.T -> string -> string * Specification.calcstate' (*TODO: string * Calc.T*)
5.13 end
5.14
5.15 (**)
5.16 @@ -86,10 +86,10 @@
5.17 If "no derivation found" then Error_Pattern.check_for.
5.18 (Error_Pattern.check_for *within* compare_step seems too expensive)
5.19 *)
5.20 -(*fun by_term (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =*)
5.21 +(*fun by_term (next_cs as (_, _, (pt, pos as (p, _))): Specification.calcstate') istr =*)
5.22 fun by_term (pt, pos as (p, _)) istr =
5.23 case TermC.parse (ThyC.get_theory "Isac_Knowledge") istr of
5.24 - NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate')
5.25 + NONE => ("syntax error in '" ^ istr ^ "'", Specification.e_calcstate')
5.26 | SOME f_in =>
5.27 let
5.28 val f_in = Thm.term_of f_in
5.29 @@ -115,8 +115,8 @@
5.30 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
5.31 in
5.32 case Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) of
5.33 - SOME errpatID => ("error pattern #" ^ errpatID ^ "#", Chead.e_calcstate')
5.34 - | NONE => ("no derivation found", Chead.e_calcstate')
5.35 + SOME errpatID => ("error pattern #" ^ errpatID ^ "#", Specification.e_calcstate')
5.36 + | NONE => ("no derivation found", Specification.e_calcstate')
5.37 end
5.38 end
5.39
6.1 --- a/src/Tools/isac/Interpret/sub-problem.sml Thu May 14 09:30:40 2020 +0200
6.2 +++ b/src/Tools/isac/Interpret/sub-problem.sml Thu May 14 13:33:47 2020 +0200
6.3 @@ -23,18 +23,18 @@
6.4 if mI = ["no_met"]
6.5 then
6.6 let
6.7 - val pors = (Chead.match_ags thy ((#ppc o Problem.from_store) pI) ags)
6.8 - (* Chead.match_ags : theory -> pat list -> term list -> ori list
6.9 + val pors = (Specification.match_ags thy ((#ppc o Problem.from_store) pI) ags)
6.10 + (* Specification.match_ags : theory -> pat list -> term list -> ori list
6.11 ^^^ variables ^^^ values *)
6.12 handle ERROR "actual args do not match formal args"
6.13 - => (Chead.match_ags_msg pI stac ags (*raise exn*);[]);
6.14 + => (Specification.match_ags_msg pI stac ags (*raise exn*);[]);
6.15 val pI' = Refine.refine_ori' pors pI;
6.16 in (pI', pors (* refinement over models with diff.prec only *),
6.17 (hd o #met o Problem.from_store) pI') end
6.18 - else (pI, (Chead.match_ags thy ((#ppc o Problem.from_store) pI) ags)
6.19 + else (pI, (Specification.match_ags thy ((#ppc o Problem.from_store) pI) ags)
6.20 handle ERROR "actual args do not match formal args"
6.21 - => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
6.22 - val (fmz_, vals) = Chead.oris2fmz_vals pors;
6.23 + => (Specification.match_ags_msg pI stac ags(*raise exn*); []), mI);
6.24 + val (fmz_, vals) = Specification.oris2fmz_vals pors;
6.25 val {cas, ppc, thy, ...} = Problem.from_store pI
6.26 val dI = Context.theory_name thy (*take dI from _refined_ pbl*)
6.27 val dI = Context.theory_name (ThyC.sub_common (ThyC.get_theory dI, Ctree.rootthy pt))
6.28 @@ -42,7 +42,7 @@
6.29 val hdl =
6.30 case cas of
6.31 NONE => Auto_Prog.pblterm dI pI
6.32 - | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
6.33 + | SOME t => subst_atomic ((Specification.vars_of_pbl_' ppc) ~~~ vals) t
6.34 val f = Auto_Prog.subpbl (strip_thy dI) pI
6.35 in
6.36 (Tactic.Subproblem (dI, pI), Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
7.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Thu May 14 09:30:40 2020 +0200
7.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Thu May 14 13:33:47 2020 +0200
7.3 @@ -24,6 +24,8 @@
7.4 ML_file applicable.sml
7.5
7.6 ML_file position.sml
7.7 + ML_file "specification-def.sml"
7.8 +
7.9 ML_file "ctree-basic.sml"
7.10 ML_file "ctree-access.sml"
7.11 ML_file "ctree-navi.sml"
8.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Thu May 14 09:30:40 2020 +0200
8.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Thu May 14 13:33:47 2020 +0200
8.3 @@ -1,12 +1,13 @@
8.4 (* Title: the calctree, which holds a calculation
8.5 Author: Walther Neuper 1999
8.6 (c) due to copyright terms
8.7 +
8.8 +Definitions required for Ctree, renamed later appropriately
8.9 *)
8.10
8.11 signature BASIC_CALC_TREE =
8.12 sig
8.13 -(** definitions required for datatype ctree, renamed later appropriately **)
8.14 -
8.15 +(**** signature ****)
8.16 (** the basic datatype **)
8.17 type state
8.18 val e_state: state
8.19 @@ -75,10 +76,9 @@
8.20 val get_assumptions : ctree -> Pos.pos' -> term list
8.21
8.22 val new_val : term -> Istate_Def.T -> Istate_Def.T
8.23 - (* for calchead.sml *)
8.24 +
8.25 type cid = cellID list
8.26 - type ocalhd = bool * Pos.pos_ * term * Model_Def.i_model * Pre_Conds_Def.T * References.T
8.27 - datatype ptform = Form of term | ModSpec of ocalhd
8.28 + datatype ptform = Form of term | ModSpec of Specification_Def.T
8.29 val get_somespec' : References.T -> References.T -> References.T
8.30 exception PTREE of string;
8.31
8.32 @@ -127,6 +127,10 @@
8.33 (**)
8.34 open Pos
8.35
8.36 +(**** Ctree ****)
8.37 +
8.38 +(*** general types* **)
8.39 +
8.40 datatype branch =
8.41 NoBranch | AndB | OrB
8.42 | TransitiveB (* FIXXXME.0308: set branch from met in Apply_Method
8.43 @@ -189,6 +193,9 @@
8.44 (int * ets) list * (* assoc-list: tacs etc. already done*)
8.45 (string * pos) list; (* asms * from where*)
8.46
8.47 +
8.48 +(*** type Ctree ***)
8.49 +
8.50 datatype ppobj = (* TODO: arrange according to signature *)
8.51 PrfObj of (* a proof step triggered by a tactic *)
8.52 {form : term, (* where tactic is applied to *)
8.53 @@ -198,8 +205,7 @@
8.54 option * (* both for interpreter location on Frm, Pbl, Met *)
8.55 (Istate_Def.T * (* script interpreter state *)
8.56 Proof.context) (* context for provers, type inference *)
8.57 - option, (* both for interpreter location on Res *)
8.58 - (* (NONE,NONE) <==> empty ! see update_loc, get_loc *)
8.59 + option, (* both for interpreter location on Res, (NONE,NONE) == empty *)
8.60 branch: branch, (* only rudimentary *)
8.61 result: Celem.result, (* result and assumptions *)
8.62 ostate: ostate} (* Complete <=> result is OK *)
8.63 @@ -233,6 +239,9 @@
8.64 type state = ctree * pos'
8.65 val e_state = (EmptyPtree , e_pos')
8.66
8.67 +
8.68 +(*** minimal set of functions on Ctree* **)
8.69 +
8.70 fun is_pblobj (PblObj _) = true
8.71 | is_pblobj _ = false;
8.72
8.73 @@ -246,7 +255,7 @@
8.74 (** convert ctree to a string **)
8.75
8.76 (* convert a pos from list to string *)
8.77 -fun pr_pos ps = (space_implode "." (map string_of_int ps))^". ";
8.78 +fun pr_pos ps = (space_implode "." (map string_of_int ps)) ^ ". ";
8.79 (* show hd origin or form only *)
8.80 fun pr_short p (PblObj _) = pr_pos p ^ " ----- pblobj -----\n" (* for tests only *)
8.81 | pr_short p (PrfObj {form = form, ...}) = pr_pos p ^ UnparseC.term form ^ "\n";
8.82 @@ -432,18 +441,8 @@
8.83 | appl_obj f (Nd (b, bs)) [] = Nd (f b, bs)
8.84 | appl_obj f (Nd (b, bs)) (p :: []) = Nd (b, repl_app bs p (((appl_to_node f) o (nth p)) bs))
8.85 | appl_obj f (Nd (b, bs)) (p :: ps) = Nd (b, repl_app bs p (appl_obj f (nth p bs) (ps:pos)));
8.86 -
8.87
8.88 -type ocalhd =
8.89 - bool * (* ALL itms+preconds true *)
8.90 - pos_ * (* model belongs to Problem | Method *)
8.91 - term * (* header: Problem ... or Cas FIXME.0312: item for marking syntaxerrors*)
8.92 - Model_Def.i_model * (* model: given, find, relate *)
8.93 - (Pre_Conds_Def.T) *(* model: preconds *)
8.94 - References.T; (* specification *)
8.95 -val e_ocalhd = (false, Und, TermC.empty, [Model_Def.i_model_empty], [(false, TermC.empty)], References.empty);
8.96 -
8.97 -datatype ptform = Form of term | ModSpec of ocalhd;
8.98 +datatype ptform = Form of term | ModSpec of Specification_Def.T;
8.99
8.100 (* for cut_level; (deprecated) *)
8.101 fun test_trans (PrfObj {branch, ...}) = true andalso branch = TransitiveB
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/Tools/isac/MathEngBasic/specification-def.sml Thu May 14 13:33:47 2020 +0200
9.3 @@ -0,0 +1,34 @@
9.4 +(* Title: MathEngBasic/specification-def.sml
9.5 + Author: Walther Neuper
9.6 + (c) due to copyright terms
9.7 +
9.8 +Required for Ctree definition.
9.9 +*)
9.10 +signature SPECIFICATION_DEFINITION =
9.11 +sig
9.12 + type T
9.13 + val empty: T
9.14 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
9.15 + (*NONE*)
9.16 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
9.17 + (*NONE*)
9.18 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
9.19 +
9.20 +end
9.21 +
9.22 +(**)
9.23 +structure Specification_Def(**): SPECIFICATION_DEFINITION(**) =
9.24 +struct
9.25 +(**)
9.26 +
9.27 +type T =
9.28 + bool * (* I_Model.T andalso Pre_Conds.T *)
9.29 + Pos.pos_ * (* model belongs to Problem or Method *)
9.30 + term * (* the headline shown on Calc.T *)
9.31 + Model_Def.i_model * (* used by I_Model.T *)
9.32 + (Pre_Conds_Def.T) * (* used by Pre_Conds.T *)
9.33 + References.T; (* into Know_Store *)
9.34 +val empty =
9.35 + (false, Pos.Und, TermC.empty, [Model_Def.i_model_empty], [(false, TermC.empty)], References.empty);
9.36 +
9.37 +(**)end(**)
10.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu May 14 09:30:40 2020 +0200
10.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Thu May 14 13:33:47 2020 +0200
10.3 @@ -14,9 +14,9 @@
10.4 val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * I_Model.T * Pre_Conds.T
10.5 val context_met : Method.id -> Ctree.ctree -> Pos.pos -> bool * Method.id * Program.T * I_Model.T * Pre_Conds.T
10.6 val context_pbl : Problem.id -> Ctree.ctree -> Pos.pos -> bool * Problem.id * term * I_Model.T * Pre_Conds.T
10.7 - val set_method : Method.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd
10.8 - val set_problem : Problem.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd
10.9 - val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd
10.10 + val set_method : Method.id -> Calc.T -> Ctree.ctree * Specification.T
10.11 + val set_problem : Problem.id -> Calc.T -> Ctree.ctree * Specification.T
10.12 + val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * Specification.T
10.13 val tryrefine : Problem.id -> Ctree.ctree -> Pos.pos' -> bool * Problem.id * term * I_Model.T * Pre_Conds.T
10.14 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.15 (*NONE*)
10.16 @@ -52,7 +52,7 @@
10.17 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
10.18 | Ctree.PrfObj _ => raise ERROR "set_method: case 2 uncovered"
10.19 in
10.20 - (pt, (complete, Pos.Met, hdf, mits, pre, spec) : Ctree.ocalhd)
10.21 + (pt, (complete, Pos.Met, hdf, mits, pre, spec) : Specification.T)
10.22 end
10.23
10.24 (* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *)
10.25 @@ -69,7 +69,7 @@
10.26 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
10.27 | Ctree.PrfObj _ => raise ERROR "set_problem: case 2 uncovered"
10.28 in
10.29 - (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd)
10.30 + (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : Specification.T)
10.31 end
10.32
10.33 fun set_theory tI ptp =
10.34 @@ -84,7 +84,7 @@
10.35 case Ctree.get_obj I pt p of
10.36 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
10.37 | Ctree.PrfObj _ => raise ERROR "set_theory: case 2 uncovered"
10.38 - in (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd) end;
10.39 + in (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : Specification.T) end;
10.40
10.41 (* does several steps within one calculation as given by "type auto";
10.42 the steps may arbitrarily go into and leave different phases,
10.43 @@ -104,29 +104,29 @@
10.44 | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto =
10.45 if Solve.autoord auto > 3 andalso Ctree.just_created (pt, pos)
10.46 then
10.47 - let val ptp = Chead.all_modspec (pt, pos);
10.48 + let val ptp = Specification.all_modspec (pt, pos);
10.49 in Solve.all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
10.50 else
10.51 if member op = [Pos.Pbl, Pos.Met] p_
10.52 then
10.53 - if not (Chead.is_complete_mod (pt, pos))
10.54 + if not (Specification.is_complete_mod (pt, pos))
10.55 then
10.56 - let val ptp = Chead.complete_mod (pt, pos) (*... auto = 2 | 3 *)
10.57 + let val ptp = Specification.complete_mod (pt, pos) (*... auto = 2 | 3 *)
10.58 in
10.59 if Solve.autoord auto < 3 then ("ok", c, ptp)
10.60 else
10.61 - if not (Chead.is_complete_spec ptp)
10.62 + if not (Specification.is_complete_spec ptp)
10.63 then
10.64 - let val ptp = Chead.complete_spec ptp
10.65 + let val ptp = Specification.complete_spec ptp
10.66 in
10.67 if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
10.68 end
10.69 else if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
10.70 end
10.71 else
10.72 - if not (Chead.is_complete_spec (pt,pos))
10.73 + if not (Specification.is_complete_spec (pt,pos))
10.74 then
10.75 - let val ptp = Chead.complete_spec (pt, pos)
10.76 + let val ptp = Specification.complete_spec (pt, pos)
10.77 in
10.78 if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
10.79 end
11.1 --- a/src/Tools/isac/MathEngine/solve.sml Thu May 14 09:30:40 2020 +0200
11.2 +++ b/src/Tools/isac/MathEngine/solve.sml Thu May 14 13:33:47 2020 +0200
11.3 @@ -61,7 +61,7 @@
11.4 if member op = [Pbl, Met] p_
11.5 then
11.6 let
11.7 - val ptp = Chead.all_modspec ptp
11.8 + val ptp = Specification.all_modspec ptp
11.9 val (_, c', ptp) = all_solve auto c ptp
11.10 in complete_solve auto (c @ c') ptp end
11.11 else
11.12 @@ -71,7 +71,7 @@
11.13 then ("ok", c @ c', ptp)
11.14 else
11.15 let
11.16 - val ptp = Chead.all_modspec ptp'
11.17 + val ptp = Specification.all_modspec ptp'
11.18 val (_, c'', ptp) = all_solve auto (c @ c') ptp
11.19 in complete_solve auto (c @ c'@ c'') ptp end
11.20 | (_, ((Tactic.Check_Postcond _, _, _) :: _, c', ptp' as (_, p'))) =>
12.1 --- a/src/Tools/isac/MathEngine/states.sml Thu May 14 09:30:40 2020 +0200
12.2 +++ b/src/Tools/isac/MathEngine/states.sml Thu May 14 13:33:47 2020 +0200
12.3 @@ -9,7 +9,7 @@
12.4 (* holds calculations; these are read/updated from the java-frontend at each interaction*)
12.5 val states = Synchronized.var "isac_states" ([] :
12.6 (calcID * (* the id unique for a calculation *)
12.7 - (Chead.calcstate * (* the interpreter state *)
12.8 + (Specification.calcstate * (* the interpreter state *)
12.9 (iterID * (* 1 sets the 'active formula': a calc. can have several visitors*)
12.10 Pos.pos' (* for iterator of a user *)
12.11 (* TODO iterID * pos' should go to java-frontend *)
12.12 @@ -52,7 +52,7 @@
12.13 *)
12.14 (* add users to a calcstate *)
12.15 fun get_iterID (cI: calcID)
12.16 - (p: (calcID * (Chead.calcstate * (iterID * Pos.pos') list)) list) =
12.17 + (p: (calcID * (Specification.calcstate * (iterID * Pos.pos') list)) list) =
12.18 case assoc (p, cI) of
12.19 NONE => raise ERROR ("get_iterID: no iterID " ^ (string_of_int cI))
12.20 | SOME (_, us) => (new_key us 1): iterID;
12.21 @@ -236,7 +236,7 @@
12.22
12.23 (* here is the _only_ critical section on states,
12.24 because a single calculation (with _one_ cI) is sequential *)
12.25 -fun add_calc (cs: Chead.calcstate) = Synchronized.change_result states
12.26 +fun add_calc (cs: Specification.calcstate) = Synchronized.change_result states
12.27 (fn s =>
12.28 let val new_cI = new_key s 1
12.29 in (new_cI: calcID, s @ [(new_cI, (cs, []))]) end);
13.1 --- a/src/Tools/isac/MathEngine/step.sml Thu May 14 09:30:40 2020 +0200
13.2 +++ b/src/Tools/isac/MathEngine/step.sml Thu May 14 13:33:47 2020 +0200
13.3 @@ -8,9 +8,9 @@
13.4
13.5 signature STEP =
13.6 sig
13.7 - val do_next: Pos.pos' -> Chead.calcstate -> string * Chead.calcstate'
13.8 - val by_tactic: Tactic.input -> Calc.T -> string * Chead.calcstate'
13.9 -(*val by_term = Step_Solve.by_term: Calc.T -> term -> string * Chead.calcstate' NOT for specify*)
13.10 + val do_next: Pos.pos' -> Specification.calcstate -> string * Specification.calcstate'
13.11 + val by_tactic: Tactic.input -> Calc.T -> string * Specification.calcstate'
13.12 +(*val by_term = Step_Solve.by_term: Calc.T -> term -> string * Specification.calcstate' NOT for specify*)
13.13 val check: Tactic.input -> Calc.T -> Applicable.T
13.14 val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T
13.15
13.16 @@ -20,8 +20,8 @@
13.17 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
13.18 (*NONE*)
13.19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
13.20 - val specify_do_next: Calc.T -> string * Chead.calcstate'
13.21 - val switch_specify_solve: Pos.pos_ -> Calc.T -> string * Chead.calcstate'
13.22 + val specify_do_next: Calc.T -> string * Specification.calcstate'
13.23 + val switch_specify_solve: Pos.pos_ -> Calc.T -> string * Specification.calcstate'
13.24 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
13.25 end
13.26
13.27 @@ -86,7 +86,7 @@
13.28 val pIopt = Ctree.get_pblID (pt, ip);
13.29 in
13.30 if ip = ([], Pos.Res)
13.31 - then ("end-of-calculation", (tacis, [], ptp): Chead.calcstate')
13.32 + then ("end-of-calculation", (tacis, [], ptp): Specification.calcstate')
13.33 else
13.34 case tacis of
13.35 (_ :: _) =>
13.36 @@ -108,7 +108,7 @@
13.37 fun by_tactic _ (ptp as (_, ([], Pos.Res))) = ("end-of-calculation", ([], [], ptp))
13.38 | by_tactic tac (ptp as (pt, p)) =
13.39 case check tac (pt, p) of
13.40 - Applicable.No _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
13.41 + Applicable.No _ => ("not-applicable", ([],[], ptp): Specification.calcstate')
13.42 | Applicable.Yes tac' =>
13.43 if Tactic.for_specify' tac'
13.44 then Step_Specify.by_tactic tac' ptp
14.1 --- a/src/Tools/isac/Specify/calchead.sml Thu May 14 09:30:40 2020 +0200
14.2 +++ b/src/Tools/isac/Specify/calchead.sml Thu May 14 13:33:47 2020 +0200
14.3 @@ -64,16 +64,17 @@
14.4 and thus is solved numerically.
14.5 #2# TODO
14.6 *)
14.7 -signature CALC_HEAD =
14.8 +signature SPECIFICATION =
14.9 sig
14.10 type calcstate
14.11 type calcstate'
14.12
14.13 + type T = Specification_Def.T
14.14 val nxt_spec : Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->
14.15 (string * (term * 'a)) list * (string * (term * 'b)) list -> References.T -> Pos.pos_ * Tactic.input
14.16
14.17 val reset_calchead : Calc.T -> Calc.T
14.18 - val get_ocalhd : Calc.T -> Ctree.ocalhd
14.19 + val get_ocalhd : Calc.T -> T
14.20 val ocalhd_complete : I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
14.21 val all_modspec : Calc.T -> Calc.T
14.22
14.23 @@ -103,7 +104,8 @@
14.24 val mk_additem: string -> TermC.as_string -> Tactic.input
14.25 val nxt_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> (string * string) option
14.26 val is_error: I_Model.feedback -> bool
14.27 - val complete_mod_: O_Model.T * Model_Pattern.T * Model_Pattern.T * I_Model.T -> I_Model.T * I_Model.T
14.28 + val complete_mod_: O_Model.T * Model_Pattern.T * Model_Pattern.T * I_Model.T ->
14.29 + I_Model.T * I_Model.T
14.30 val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> calcstate'
14.31 val specify_additem: string -> TermC.as_string -> Calc.T -> string * calcstate'
14.32 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
14.33 @@ -140,7 +142,7 @@
14.34 end
14.35
14.36 (**)
14.37 -structure Chead(** ): CALC_HEAD( **) =
14.38 +structure Specification(**): SPECIFICATION(**) =
14.39 struct
14.40 (**)
14.41
14.42 @@ -176,6 +178,8 @@
14.43 Calc.T (* the calc-state resulting from the application of tacis *)
14.44 val e_calcstate' = ([State_Steps.single_empty], [Pos.e_pos'], (Ctree.EmptyPtree, Pos.e_pos')) : calcstate';
14.45
14.46 +type T = Specification_Def.T;
14.47 +
14.48 (* is the calchead complete ? *)
14.49 fun ocalhd_complete its pre (dI, pI, mI) =
14.50 foldl and_ (true, map #3 (its: I_Model.T)) andalso
14.51 @@ -963,7 +967,7 @@
14.52 end
14.53 | get_ocalhd _ = raise ERROR "get_ocalhd: uncovered definition"
14.54
14.55 -(* at the activeFormula set the Model, the Guard and the Specification
14.56 +(* at the activeFormula set the Specification
14.57 to empty and return a CalcHead;
14.58 the 'origin' remains (for reconstructing all that) *)
14.59 fun reset_calchead (pt, (p,_)) =
15.1 --- a/src/Tools/isac/Specify/input-calchead.sml Thu May 14 09:30:40 2020 +0200
15.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Thu May 14 13:33:47 2020 +0200
15.3 @@ -5,46 +5,58 @@
15.4 This will be dropped at switch to Isabelle/PIDE.
15.5 *)
15.6
15.7 -signature INPUT_CALCHEAD =
15.8 +signature INPUT_SPECIFICATION =
15.9 sig
15.10 - type pbt_ = string * (term * term)
15.11 -
15.12 datatype iitem =
15.13 Find of TermC.as_string list
15.14 | Given of TermC.as_string list
15.15 | Relate of TermC.as_string list
15.16 type imodel = iitem list
15.17 type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T
15.18 - val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
15.19 - val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
15.20 + val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Specification.T
15.21 + val cas_input : term -> (Ctree.ctree * Specification.T) option
15.22 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
15.23 (* NONE *)
15.24 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
15.25 - (* NONE *)
15.26 + val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
15.27 + string * TermC.as_string -> I_Model.single
15.28 + val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
15.29 + (string * TermC.as_string) list -> I_Model.T
15.30 + val cas_input_: References.T -> (term * term list) list ->
15.31 + Problem.id * I_Model.T * Method.id * I_Model.T * Pre_Conds.T * Proof.context
15.32 + val dtss2itm_: Model_Pattern.single list -> term * term list ->
15.33 + int list * bool * string * I_Model.feedback (*I_Model.single'*)
15.34 + val e_icalhd: icalhd
15.35 + val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool
15.36 + val filter_sep: ('a -> bool) -> 'a list -> 'a list * 'a list
15.37 + val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e
15.38 + val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string ->
15.39 + int list * bool * ''a * I_Model.feedback (*I_Model.single'*)
15.40 + val imodel2fstr: iitem list -> (string * TermC.as_string) list
15.41 + val is_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*)
15.42 + val is_casinput: TermC.as_string -> Formalise.T -> bool
15.43 + val is_e_ts: term list -> bool
15.44 + val itms2fstr: I_Model.single -> string * string
15.45 + val par2fstr: I_Model.single -> string * TermC.as_string
15.46 + val parsitm: theory -> I_Model.single -> I_Model.single
15.47 + val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T?*)
15.48 + (''a * string) list ->
15.49 + (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T?*)
15.50 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
15.51 -
15.52 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
15.53 - val e_icalhd : icalhd
15.54 - val oris2itms : 'a -> ''b list -> ('c * ''b * 'd * term * term list) list ->
15.55 - ('c * ''b * bool * 'd * I_Model.feedback) list
15.56 end
15.57
15.58 -structure In_Chead(**): INPUT_CALCHEAD(**) =
15.59 +(**)
15.60 +structure In_Chead(**): INPUT_SPECIFICATION(**) =
15.61 struct
15.62 +(**)
15.63
15.64 -(* types for problems models (TODO rename to specification models) *)
15.65 -type pbt_ =
15.66 - (string * (* field "#Given",..*)(*deprecated due to 'type pat'*)
15.67 - (term * (* description *)
15.68 - term)); (* id | struct-var *)
15.69 -
15.70 -(*** handle an input by CAS-command ***)
15.71 +(** handle input **)
15.72
15.73 fun dtss2itm_ ppc (d, ts) =
15.74 let
15.75 val (f, (d, id)) = the (find_first ((curry op= d) o
15.76 (#1: (term * term) -> term) o
15.77 - (#2: pbt_ -> (term * term))) ppc)
15.78 + (#2: Model_Pattern.single -> (term * term))) ppc)
15.79 in
15.80 ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
15.81 end
15.82 @@ -92,28 +104,27 @@
15.83 val pt = Ctree.update_pbl pt [] pits
15.84 val pt = Ctree.update_met pt [] mits
15.85 in
15.86 - SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Ctree.ocalhd)
15.87 + SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Specification.T)
15.88 end
15.89 end
15.90
15.91
15.92 -(*** handle an input calc-head ***)
15.93 +(** handle an input calc-head **)
15.94
15.95 datatype iitem =
15.96 Given of TermC.as_string list
15.97 -(*Where is never input*)
15.98 +(*Where is still not input*)
15.99 | Find of TermC.as_string list
15.100 | Relate of TermC.as_string list
15.101
15.102 type imodel = iitem list
15.103
15.104 -(*calc-head as input*)
15.105 type icalhd =
15.106 - Pos.pos' * (*the position of the calc-head in the calc-tree*)
15.107 - TermC.as_string * (*the headline*)
15.108 - imodel * (*the model (without Find) of the calc-head*)
15.109 - Pos.pos_ * (*model belongs to Pbl or Met*)
15.110 - References.T; (*specification: domID, pblID, metID*)
15.111 + Pos.pos' * (* the position in Ctree *)
15.112 + TermC.as_string * (* the headline shown on Calc.T *)
15.113 + imodel * (* the model *)
15.114 + Pos.pos_ * (* model belongs to Problem or Method *)
15.115 + References.T; (* into Know_Store *)
15.116 val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
15.117
15.118 fun is_casinput (hdf : TermC.as_string) ((fmz_, spec) : Formalise.T) =
15.119 @@ -228,13 +239,7 @@
15.120 | appl_adds _ _ ppc _ [] = ppc
15.121 | appl_adds dI oris ppc pbt (selct :: ss) =
15.122 let val itm = appl_add' dI oris ppc pbt selct;
15.123 - in appl_adds dI oris (Chead.insert_ppc' itm ppc) pbt ss end
15.124 -
15.125 -fun oris2itms _ _ [] = [] (* WN161130: similar in ptyps ?!? *)
15.126 - | oris2itms pbt vat ((i, v, f, d, ts) :: os) =
15.127 - if member op = vat v
15.128 - then (i, v, true, f, I_Model.Cor ((d, ts), (TermC.empty, []))) :: (oris2itms pbt vat os)
15.129 - else oris2itms pbt vat os
15.130 + in appl_adds dI oris (Specification.insert_ppc' itm ppc) pbt ss end
15.131
15.132 fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
15.133 | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)
15.134 @@ -269,38 +274,38 @@
15.135 if dI <> sdI
15.136 then let val its = map (parsitm (ThyC.get_theory dI)) probl;
15.137 val (its, trms) = filter_sep is_Par its;
15.138 - val pbt = (#ppc o Problem.from_store) (#2 (Chead.some_spec ospec sspec))
15.139 + val pbt = (#ppc o Problem.from_store) (#2 (Specification.some_spec ospec sspec))
15.140 in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
15.141 else
15.142 if pI <> spI
15.143 then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
15.144 else
15.145 let val pbt = (#ppc o Problem.from_store) pI
15.146 - val dI' = #1 (Chead.some_spec ospec spec)
15.147 + val dI' = #1 (Specification.some_spec ospec spec)
15.148 val oris = if pI = #2 ospec then oris
15.149 else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*);
15.150 in (Pos.Pbl, appl_adds dI' oris probl pbt
15.151 (map itms2fstr probl), meth) end
15.152 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
15.153 then let val met = (#ppc o Method.from_store) mI
15.154 - val mits = Chead.complete_metitms oris probl meth met
15.155 + val mits = Specification.complete_metitms oris probl meth met
15.156 in if foldl and_ (true, map #3 mits)
15.157 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
15.158 end
15.159 - else (Pos.Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]
15.160 - ((#ppc o Problem.from_store) (#2 (Chead.some_spec ospec spec)))
15.161 + else (Pos.Pbl, appl_adds (#1 (Specification.some_spec ospec spec)) oris [(*!!!*)]
15.162 + ((#ppc o Problem.from_store) (#2 (Specification.some_spec ospec spec)))
15.163 (imodel2fstr imodel), meth)
15.164 val pt = Ctree.update_spec pt p spec;
15.165 in if pos_ = Pos.Pbl
15.166 - then let val {prls,where_,...} = Problem.from_store (#2 (Chead.some_spec ospec spec))
15.167 + then let val {prls,where_,...} = Problem.from_store (#2 (Specification.some_spec ospec spec))
15.168 val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits
15.169 in (Ctree.update_pbl pt p pits,
15.170 - (Chead.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Ctree.ocalhd)
15.171 + (Specification.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T)
15.172 end
15.173 - else let val {prls,pre,...} = Method.from_store (#3 (Chead.some_spec ospec spec))
15.174 + else let val {prls,pre,...} = Method.from_store (#3 (Specification.some_spec ospec spec))
15.175 val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits
15.176 in (Ctree.update_met pt p mits,
15.177 - (Chead.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Ctree.ocalhd)
15.178 + (Specification.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T)
15.179 end
15.180 end
15.181 end
16.1 --- a/src/Tools/isac/Specify/specify.sml Thu May 14 09:30:40 2020 +0200
16.2 +++ b/src/Tools/isac/Specify/specify.sml Thu May 14 13:33:47 2020 +0200
16.3 @@ -14,9 +14,8 @@
16.4 (**)
16.5 open Pos
16.6 open Ctree
16.7 -open Chead
16.8 +open Specification
16.9
16.10 -(* was Chead.nxt_spec *)
16.11 fun find_next_step (pt, (p, p_)) =
16.12 let
16.13 val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) =
17.1 --- a/src/Tools/isac/Specify/step-specify.sml Thu May 14 09:30:40 2020 +0200
17.2 +++ b/src/Tools/isac/Specify/step-specify.sml Thu May 14 13:33:47 2020 +0200
17.3 @@ -6,8 +6,8 @@
17.4 signature STEP_SPECIFY =
17.5 sig
17.6 (*val do_next: Step.specify_do_next requires LI.by_tactic, which is not yet known in Step_Specify*)
17.7 - val by_tactic_input: Tactic.input -> Calc.T -> Chead.calcstate'
17.8 - val by_tactic: Tactic.T -> Calc.T -> string * Chead.calcstate'
17.9 + val by_tactic_input: Tactic.input -> Calc.T -> Specification.calcstate'
17.10 + val by_tactic: Tactic.T -> Calc.T -> string * Specification.calcstate'
17.11
17.12 val hack_until_review_Specify_1: Method.id -> I_Model.T -> I_Model.T
17.13 val hack_until_review_Specify_2: Method.id -> I_Model.T -> I_Model.T
17.14 @@ -24,7 +24,7 @@
17.15 (**)
17.16 open Pos
17.17 open Ctree
17.18 -open Chead
17.19 +open Specification
17.20
17.21 (*
17.22 hack until review of Specify:
17.23 @@ -180,7 +180,7 @@
17.24 (* was fun Math_Engine.nxt_specify_ *)
17.25
17.26
17.27 -(* was fun Chead.specify *)
17.28 +(* was fun Specification.specify *)
17.29 fun by_tactic (Tactic.Model_Problem' (_, pbl, met)) (pt, pos as (p, _)) =
17.30 let
17.31 val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of
17.32 @@ -194,7 +194,7 @@
17.33 val pb = foldl and_ (true, map fst pre)
17.34 val ((p, _), _, _, pt) =
17.35 Specify_Step.add (Tactic.Model_Problem'([],pbl,met)) (Istate_Def.Uistate, ctxt) (pt, pos)
17.36 - val (_, _) = Chead.nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
17.37 + val (_, _) = Specification.nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
17.38 (ppc,(#ppc o Method.from_store) mI') (dI',pI',mI');
17.39 in
17.40 ("ok", ([], [], (pt, (p, Pbl))))
17.41 @@ -256,9 +256,9 @@
17.42 in
17.43 ("ok", ([], [], (pt, pos)))
17.44 end
17.45 - | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p) = Chead.specify_additem "#Given" ct (pt, p)
17.46 - | by_tactic (Tactic.Add_Find' (ct, _)) (pt, p) = Chead.specify_additem "#Find" ct (pt, p)
17.47 - | by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = Chead.specify_additem"#Relate" ct (pt, p)
17.48 + | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p) = Specification.specify_additem "#Given" ct (pt, p)
17.49 + | by_tactic (Tactic.Add_Find' (ct, _)) (pt, p) = Specification.specify_additem "#Find" ct (pt, p)
17.50 + | by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = Specification.specify_additem"#Relate" ct (pt, p)
17.51 | by_tactic (Tactic.Specify_Theory' domID) (pt, (p,p_)) =
17.52 let
17.53 val p_ = case p_ of Met => Met | _ => Pbl
17.54 @@ -292,7 +292,7 @@
17.55 end
17.56 end
17.57 | by_tactic _ _ = raise ERROR "Step_Specify.by_tactic uncovered pattern in fun.def"
17.58 -(* was fun Chead.specify *)
17.59 +(* was fun Specification.specify *)
17.60
17.61 (* create a calc-tree with oris via an cas.refined pbl *)
17.62 fun nxt_specify_init_calc ([], (dI, pI, mI)) =
18.1 --- a/src/Tools/isac/TODO.thy Thu May 14 09:30:40 2020 +0200
18.2 +++ b/src/Tools/isac/TODO.thy Thu May 14 13:33:47 2020 +0200
18.3 @@ -360,7 +360,7 @@
18.4 \item xxx
18.5 \item can lev_on_total replace lev_on ? ..Test_Isac_Short + rename lev_on_total -> lev_on
18.6 \item xxx
18.7 - \item Step* functions should return Calc.T instead of Chead.calcstate'
18.8 + \item Step* functions should return Calc.T instead of Specification.calcstate'
18.9 \item xxx
18.10 \item states.sml: check, when "length tacis > 1"
18.11 \item in Test_Isac.thy there is only 1 error in Interpret/inform.sml
19.1 --- a/src/Tools/isac/Test_Code/test-code.sml Thu May 14 09:30:40 2020 +0200
19.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Thu May 14 13:33:47 2020 +0200
19.3 @@ -36,7 +36,7 @@
19.4 delete as soon as TESTg_form -> _mout_ dropped *)
19.5 fun TESTg_form ptp =
19.6 let
19.7 - val (form, _, _) = Chead.pt_extract ptp
19.8 + val (form, _, _) = Specification.pt_extract ptp
19.9 in
19.10 case form of
19.11 Ctree.Form t => Test_Out.FormKF (UnparseC.term t)
20.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Thu May 14 09:30:40 2020 +0200
20.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Thu May 14 13:33:47 2020 +0200
20.3 @@ -154,7 +154,7 @@
20.4 \<close>
20.5
20.6 ML \<open>
20.7 - Chead.show_pt pt;
20.8 + Specification.show_pt pt;
20.9 \<close>
20.10
20.11 ML \<open>
21.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_1.thy Thu May 14 09:30:40 2020 +0200
21.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_1.thy Thu May 14 13:33:47 2020 +0200
21.3 @@ -37,7 +37,7 @@
21.4
21.5 ML \<open>
21.6 f2str f;
21.7 - Chead.show_pt pt;
21.8 + Specification.show_pt pt;
21.9 \<close>
21.10
21.11 end
22.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu May 14 09:30:40 2020 +0200
22.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu May 14 13:33:47 2020 +0200
22.3 @@ -319,7 +319,7 @@
22.4 (*
22.5 * [z = 1 / 2, z = -1 / 4]
22.6 *)
22.7 - Chead.show_pt pt;
22.8 + Specification.show_pt pt;
22.9 val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]";
22.10 \<close>
22.11
22.12 @@ -1498,7 +1498,7 @@
22.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22.14 \<close>
22.15 ML \<open>
22.16 -Chead.show_pt pt;
22.17 +Specification.show_pt pt;
22.18 \<close>
22.19 ML \<open>
22.20 \<close>
23.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Thu May 14 09:30:40 2020 +0200
23.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Thu May 14 13:33:47 2020 +0200
23.3 @@ -134,7 +134,7 @@
23.4 With 'show_pt' the calculation can be inspected (in a more or less readable
23.5 format) by clicking the checkbox <Tracing> on top of the <Output> window:
23.6 \<close>
23.7 -ML \<open>Chead.show_pt pt\<close>
23.8 +ML \<open>Specification.show_pt pt\<close>
23.9
23.10
23.11 section \<open>Test further examples\<close>
24.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Thu May 14 09:30:40 2020 +0200
24.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Thu May 14 13:33:47 2020 +0200
24.3 @@ -1022,7 +1022,7 @@
24.4 (*+*)if pos = ([1], Res) then () else error "inform with (positive) Error_Pattern.check_for broken 1";
24.5 val ("ok", cs' as (_, _, ptp)) = (*case*) Step.do_next pos cs (*of*);
24.6 (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); (*ERROR WAS: "no derivation found"*)
24.7 -"~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Chead.calcstate'), istr)
24.8 +"~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Specification.calcstate'), istr)
24.9 = (cs', (encode ifo));
24.10 val ctxt = get_ctxt pt pos (*see TODO.thy*)
24.11 val SOME f_in = (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
25.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Thu May 14 09:30:40 2020 +0200
25.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Thu May 14 13:33:47 2020 +0200
25.3 @@ -229,7 +229,7 @@
25.4
25.5 (*val Updated (_, _, (ctree, pos')) =*) loc_specify_ m ptp; (*creates meth-itms*)
25.6 "~~~~~ fun loc_specify_ , args:"; val (m, (pt, pos)) = (m, ptp);
25.7 -(* val (p, _, f, _, _, pt) =*) Chead.specify m pos [] pt;
25.8 +(* val (p, _, f, _, _, pt) =*) Specification.specify m pos [] pt;
25.9
25.10 "~~~~~ fun specify , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pos as (p, _)), _, pt) = (m, pos, [], pt);
25.11 val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
26.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Thu May 14 09:30:40 2020 +0200
26.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Thu May 14 13:33:47 2020 +0200
26.3 @@ -67,7 +67,7 @@
26.4 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
26.5 | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
26.6 val {ppc, ...} = Method.from_store mI;
26.7 - val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
26.8 + val itms = if itms <> [] then itms else Specification.complete_metitms oris probl [] ppc
26.9 val itms = Step_Specify.hack_until_review_Specify_1 mI itms
26.10 val srls = LItool.get_simplifier (pt, pos)
26.11 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
27.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu May 14 09:30:40 2020 +0200
27.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu May 14 13:33:47 2020 +0200
27.3 @@ -217,10 +217,10 @@
27.4 val ags = TermC.isalist2list ags';
27.5 (*if*) mI = ["no_met"] (*else*);
27.6 val (pI, pors, mI) =
27.7 - (pI, (Chead.match_ags thy ((#ppc o Problem.from_store) pI) ags)
27.8 + (pI, (Specification.match_ags thy ((#ppc o Problem.from_store) pI) ags)
27.9 handle ERROR "actual args do not match formal args"
27.10 - => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI)
27.11 - val (fmz_, vals) = Chead.oris2fmz_vals pors;
27.12 + => (Specification.match_ags_msg pI stac ags(*raise exn*); []), mI)
27.13 + val (fmz_, vals) = Specification.oris2fmz_vals pors;
27.14 val {cas,ppc,thy,...} = Problem.from_store pI
27.15 val dI = Context.theory_name thy (*.take dI from _refined_ pbl.*)
27.16 val dI = Context.theory_name (ThyC.sub_common (ThyC.get_theory dI, rootthy pt));
28.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Thu May 14 09:30:40 2020 +0200
28.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Thu May 14 13:33:47 2020 +0200
28.3 @@ -41,7 +41,7 @@
28.4 val pre = Pre_Conds.check' "thy 100820" prls where_ probl;
28.5 val pb = foldl and_ (true, map fst pre);
28.6 val (_, tac) =
28.7 - Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI)
28.8 + Specification.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI)
28.9 val ist_ctxt = get_loc pt (p, p_)
28.10
28.11 val Apply_Method mI = (*case*) tac (*of*);
28.12 @@ -53,7 +53,7 @@
28.13 val (itms, oris, probl) = case get_obj I pt p of
28.14 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
28.15 | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"
28.16 - val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
28.17 + val itms = if itms <> [] then itms else Specification.complete_metitms oris probl [] ppc
28.18 val thy' = get_obj g_domID pt p;
28.19 val thy = ThyC.get_theory thy';
28.20 val srls = LItool.get_simplifier (pt, pos);
29.1 --- a/test/Tools/isac/OLDTESTS/interface-xml.sml Thu May 14 09:30:40 2020 +0200
29.2 +++ b/test/Tools/isac/OLDTESTS/interface-xml.sml Thu May 14 13:33:47 2020 +0200
29.3 @@ -5,7 +5,7 @@
29.4 (*see javatest.isac.util.parse.TestXMLParserDigest#testParseRefFormula*)
29.5 refformulaOK2xml 1 ([1],Frm) (Form (str2term "x+1=2"));
29.6 (*see javatest.isac.util.parse.TestXMLParserDigest#testParseRefCalcHead*)
29.7 -refformulaOK2xml 1 ([1],Pbl) (ModSpec e_ocalhd);
29.8 +refformulaOK2xml 1 ([1],Pbl) (ModSpec Specification_Def.empty);
29.9
29.10 getintervalOK 1 [(([2],Res), str2term "x = 4"),
29.11 (([3],Pbl), str2term "e_headline"),
30.1 --- a/test/Tools/isac/Specify/calchead.sml Thu May 14 09:30:40 2020 +0200
30.2 +++ b/test/Tools/isac/Specify/calchead.sml Thu May 14 13:33:47 2020 +0200
30.3 @@ -607,11 +607,11 @@
30.4 "--------- regression test fun is_copy_named ------------";
30.5 "--------- regression test fun is_copy_named ------------";
30.6 "--------- regression test fun is_copy_named ------------";
30.7 -val trm = (1, (2, @{term "v'i'"}));
30.8 +val trm = ("1", (TermC.empty, @{term "v'i'"}));
30.9 if is_copy_named trm then () else error "regr. is_copy_named 1";
30.10 -val trm = (1, (2, @{term "e_e"}));
30.11 +val trm = ("1", (TermC.empty, @{term "e_e"}));
30.12 if is_copy_named trm then error "regr. is_copy_named 2" else ();
30.13 -val trm = (1, (2, @{term "L'''"}));
30.14 +val trm = ("1", (TermC.empty, @{term "L'''"}));
30.15 if is_copy_named trm then () else error "regr. is_copy_named 3";
30.16
30.17 (* out-comment 'structure CalcHead'...
31.1 --- a/test/Tools/isac/Specify/i-model.sml Thu May 14 09:30:40 2020 +0200
31.2 +++ b/test/Tools/isac/Specify/i-model.sml Thu May 14 13:33:47 2020 +0200
31.3 @@ -42,7 +42,7 @@
31.4 "~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
31.5
31.6 val ("ok", ([], [], _)) =
31.7 - Chead.specify_additem "#Given" ct (pt, p);
31.8 + Specification.specify_additem "#Given" ct (pt, p);
31.9 "~~~~~ fun specify_additem , args:"; val (sel, ct, (pt, pos as (p,_(*Frm, Pbl*)))) =
31.10 ("#Given", ct, (pt, p));
31.11 val (met, oris, dI', pI', mI', pbl, dI, pI, mI, ctxt) = get (pt, pos)
32.1 --- a/test/Tools/isac/Specify/step-specify.sml Thu May 14 09:30:40 2020 +0200
32.2 +++ b/test/Tools/isac/Specify/step-specify.sml Thu May 14 13:33:47 2020 +0200
32.3 @@ -64,7 +64,7 @@
32.4 val pb = foldl and_ (true, map fst pre);
32.5
32.6 val (Pbl, Specify_Theory "Integrate") =
32.7 - Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);
32.8 + Specification.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);
32.9 "~~~~~ fun nxt_spec , args:"; val (Pbl, preok, oris, (dI', pI', mI'), (pbl, met), (pbt, mpc), (dI, pI, mI))
32.10 (* vv----^^*)
32.11 = (p_, pb, oris, (dI', pI', mI'), (probl, meth), (ppc, (#ppc o Method.from_store) cmI), (dI, pI, mI));
33.1 --- a/test/Tools/isac/Test_Isac.thy Thu May 14 09:30:40 2020 +0200
33.2 +++ b/test/Tools/isac/Test_Isac.thy Thu May 14 13:33:47 2020 +0200
33.3 @@ -103,7 +103,7 @@
33.4 open Error_Pattern;
33.5 open Error_Pattern_Def;
33.6 open In_Chead;
33.7 - open Chead; pt_extract;
33.8 + open Specification;
33.9 open Ctree; append_problem;
33.10 open Pos;
33.11 open Program;
34.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu May 14 09:30:40 2020 +0200
34.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu May 14 13:33:47 2020 +0200
34.3 @@ -103,7 +103,7 @@
34.4 open Error_Pattern;
34.5 open Error_Pattern_Def;
34.6 open In_Chead;
34.7 - open Chead; pt_extract;
34.8 + open Specification;
34.9 open Ctree; append_problem;
34.10 open Pos;
34.11 open Program;
35.1 --- a/test/Tools/isac/Test_Some.thy Thu May 14 09:30:40 2020 +0200
35.2 +++ b/test/Tools/isac/Test_Some.thy Thu May 14 13:33:47 2020 +0200
35.3 @@ -20,7 +20,7 @@
35.4 open Error_Pattern;
35.5 open Error_Pattern_Def;
35.6 open In_Chead;
35.7 - open Chead; pt_extract;
35.8 + open Specification;
35.9 open Ctree; append_problem;
35.10 open Pos;
35.11 open Program;
36.1 --- a/test/Tools/isac/Test_Some_meld.thy Thu May 14 09:30:40 2020 +0200
36.2 +++ b/test/Tools/isac/Test_Some_meld.thy Thu May 14 13:33:47 2020 +0200
36.3 @@ -13,7 +13,7 @@
36.4 open Istate;
36.5 open Inform; cas_input;
36.6 open Rtools; .trtas2str;
36.7 - open Chead; pt_extract;
36.8 + open Specification;
36.9 open Generate; (* NONE *)
36.10 open Ctree; append_problem;
36.11 open Program;