# HG changeset patch # User wneuper # Date 1666168984 -7200 # Node ID bb3140a02f3d593119b152b61a9925822a4a062e # Parent 04f8699d2c9d219317ecb6e3e63ddc8beaaca225 eliminate term2str in src, Prog_Tac.*_adapt_to_type diff -r 04f8699d2c9d -r bb3140a02f3d TODO.md --- a/TODO.md Sun Oct 09 09:01:29 2022 +0200 +++ b/TODO.md Wed Oct 19 10:43:04 2022 +0200 @@ -69,6 +69,9 @@ * WN: improve naming in refine.sml, m-match.sml * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store› +* WN: review Prog_Tac: + (*+isa==isa2*)@{term "Substitution []"}; (*Free ("Subproblem",.. ALSO Subproblem, ?!*) + (*+isa==isa2*)@{term "Rewrite_Set ''norm_Rational''"}; (*Const ("Prog_Tac.Rewrite_Set",..*) * WN: KEStore_Elems.get_thes, add_thes still required for Error_Patterns, we want to eliminate thes: (1) Error_Pattern.T are already stored by MethodC -- place them in respective thys (2) Error_Pattern.fill_in stored with thm (in thes): instead introduce new Thy_Data for them. diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/BaseDefinitions/BaseDefinitions.thy --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Wed Oct 19 10:43:04 2022 +0200 @@ -64,5 +64,7 @@ ML \ \ ML \ \ ML \ +\ ML \ +\ ML \ \ end diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/BaseDefinitions/substitution.sml --- a/src/Tools/isac/BaseDefinitions/substitution.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/BaseDefinitions/substitution.sml Wed Oct 19 10:43:04 2022 +0200 @@ -27,7 +27,7 @@ val T_from_string_eqs: theory -> as_string_eqs -> T val T_from_input: Proof.context -> input -> T - val input_to_terms: input -> term list + val input_to_terms: Proof.context -> input -> as_eqs val eqs_to_input: as_eqs -> as_string_eqs val program_to_input: program -> input val for_bdv: program -> T -> input option * T @@ -78,8 +78,11 @@ handle TERM _ => raise TERM ("T_from_input: wrong argument " ^ strs2str' input, []) val eqs_to_input = map UnparseC.term; -(*TODO: input requires parse _: _ -> _ option*) -val input_to_terms = map TermC.str2term; + +(* TermC.parse ctxt fails with "c_2 = 0" \ \c_2 = (0 :: 'a)\ and thus requires adapt_to_type *) +fun input_to_terms ctxt strs = strs + |> map (TermC.parse ctxt) + |> map (Model_Pattern.adapt_term_to_type ctxt) fun program_to_input sub = (sub |> HOLogic.dest_list diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/BaseDefinitions/termC.sml --- a/src/Tools/isac/BaseDefinitions/termC.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Wed Oct 19 10:43:04 2022 +0200 @@ -83,7 +83,6 @@ (*for test/* *) (*goal*)val parse_test: Proof.context -> string -> term (*goal*)val parse_patt_test: theory -> string -> term - val str2term: string -> term (*to be replaced by parse/_patt in src*, by parse/_patt in test/**) val str_of_free_opt: term -> string option val str_of_int: int -> string @@ -590,7 +589,6 @@ |>> Proof_Context.init_global |-> Proof_Context.read_term_pattern |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy) -fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str fun is_atom (Const _) = true diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/BridgeLibisabelle/mathml.sml --- a/src/Tools/isac/BridgeLibisabelle/mathml.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/BridgeLibisabelle/mathml.sml Wed Oct 19 10:43:04 2022 +0200 @@ -67,7 +67,7 @@ indt (j+i) ^ "\n" ^ indt (j+2*i) ^ " " ^ (decode o UnparseC.term) t ^ " \n" ^ indt (j+i) ^ ""; -(*val t = str2term "equality e_"; +(*val t = TermC.parse_test @{context} "equality e_"; writeln (term2xml 8 t); equality e_ diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/Build_Isac.thy --- a/src/Tools/isac/Build_Isac.thy Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/Build_Isac.thy Wed Oct 19 10:43:04 2022 +0200 @@ -109,10 +109,10 @@ ML_file istate.sml ML_file "sub-problem.sml" ML_file "thy-read.sml" + ML_file "li-tool.sml" ML_file "solve-step.sml" ML_file "error-pattern.sml" ML_file derive.sml - ML_file "li-tool.sml" ML_file "lucas-interpreter.sml" ML_file "step-solve.sml" ( ** ) "Interpret/Interpret"( **) diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/Interpret/Interpret.thy --- a/src/Tools/isac/Interpret/Interpret.thy Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/Interpret/Interpret.thy Wed Oct 19 10:43:04 2022 +0200 @@ -32,5 +32,20 @@ end \ ML \ \ ML \ +\ ML \ +fun tac_from_prog _ thy (Const (\<^const_name>\Prog_Tac.Rewrite_Inst\, _) $ sub $ thmID $ _) = + let + val tid = HOLogic.dest_string thmID + val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub + in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end + | tac_from_prog _ _ (Const (\<^const_name>\Prog_Tac.Rewrite_Set\,_) $ rls $ _) = + (Tactic.Rewrite_Set (HOLogic.dest_string rls)) + | tac_from_prog _ thy (Const (\<^const_name>\Prog_Tac.Rewrite_Set_Inst\, _) $ sub $ rls $ _) = + let + val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub + in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end +\ ML \ +\ ML \ +\ ML \ \ end diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/Interpret/li-tool.sml --- a/src/Tools/isac/Interpret/li-tool.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Oct 19 10:43:04 2022 +0200 @@ -73,16 +73,19 @@ | tac_from_prog _ thy (Const (\<^const_name>\Prog_Tac.Rewrite_Inst\, _) $ sub $ thmID $ _) = let val tid = HOLogic.dest_string thmID - in (Tactic.Rewrite_Inst (Subst.program_to_input sub, (tid, ThmC.thm_from_thy thy tid))) end + val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub + in (Tactic.Rewrite_Inst (sub', (tid, ThmC.thm_from_thy thy tid))) end | tac_from_prog _ _ (Const (\<^const_name>\Prog_Tac.Rewrite_Set\,_) $ rls $ _) = (Tactic.Rewrite_Set (HOLogic.dest_string rls)) - | tac_from_prog _ _ (Const (\<^const_name>\Prog_Tac.Rewrite_Set_Inst\, _) $ sub $ rls $ _) = - (Tactic.Rewrite_Set_Inst (Subst.program_to_input sub, HOLogic.dest_string rls)) + | tac_from_prog _ thy (Const (\<^const_name>\Prog_Tac.Rewrite_Set_Inst\, _) $ sub $ rls $ _) = + let + val sub' = (**)Subst.program_to_input(** )Prog_Tac.Rewrite_Inst_adapt_to_type thy( **) sub + in (Tactic.Rewrite_Set_Inst (sub', HOLogic.dest_string rls)) end | tac_from_prog _ _ (Const (\<^const_name>\Prog_Tac.Calculate\, _) $ op_ $ _) = (Tactic.Calculate (HOLogic.dest_string op_)) | tac_from_prog _ _ (Const (\<^const_name>\Prog_Tac.Take\, _) $ t) = (Tactic.Take (UnparseC.term t)) - | tac_from_prog _ _ (Const (\<^const_name>\Prog_Tac.Substitute\, _) $ isasub $ _) = - (Tactic.Substitute ((Subst.eqs_to_input o TermC.isalist2list) isasub)) + | tac_from_prog _ thy (Const (\<^const_name>\Prog_Tac.Substitute\, _) $ isasub $ _) = + Tactic.Substitute (Prog_Tac.Substitute_adapt_to_type thy isasub) | tac_from_prog _ thy (Const (\<^const_name>\Prog_Tac.Check_elementwise\, _) $ _ $ (Const (\<^const_name>\Collect\, _) $ Abs (_, _, pred))) = (Tactic.Check_elementwise (UnparseC.term_in_thy thy pred)) @@ -341,7 +344,7 @@ else (); (* check a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr. - snd of return value is the formal arguments in case of currying. + snd of return value are the formal arguments in case of currying. *) fun check_leaf call ctxt srls (E, (a, v)) t = case Prog_Tac.eval_leaf E a v t of diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/Interpret/lucas-interpreter.sml --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Oct 19 10:43:04 2022 +0200 @@ -175,15 +175,16 @@ then scan_dn cc (ist |> path_down [L, R]) e1 else scan_dn cc (ist |> path_down [R]) e2 - | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t = + | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t (*fall-through*) = if Tactical.contained_in t then raise TERM ("scan_dn expects Prog_Tac or Prog_Expr", [t]) else case LItool.check_leaf "next " ctxt eval (get_subst ist) t of (Program.Expr s, _) => Term_Val s (*TODO?: include set_found here and drop those after call*) | (Program.Tac prog_tac, form_arg) => - check_tac cc ist (prog_tac, form_arg) - + (tracing ("### scan_dn fall-through, prog_tac = " ^ quote (UnparseC.term prog_tac) ^ " |"); +check_tac cc ist (prog_tac, form_arg)) + fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept, ...}) = if path = [R] (*root of the program body*) then if found_accept then diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/Interpret/solve-step.sml --- a/src/Tools/isac/Interpret/solve-step.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/Interpret/solve-step.sml Wed Oct 19 10:43:04 2022 +0200 @@ -21,6 +21,7 @@ val get_eval: string -> Pos.pos' -> Ctree.ctree -> string * ThyC.id * Eval.ml \<^isac_test>\ + val get_ctxt: Ctree.ctree -> Pos.pos' -> Proof.context val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Eval.ml_from_prog list \ end @@ -84,6 +85,31 @@ end end; +(** get context reliably at switch_specify_solve **) + +fun at_begin_program (is, Pos.Res) = last_elem is = 0 + | at_begin_program _ = false; + +(* strange special case at Apply_Method *) +fun get_ctxt_from_PblObj pt (p_, Pos.Res) = + let + val pp = Ctree.par_pblobj pt p_ (*drops the "0"*) + val {ctxt, ...} = Ctree.get_obj I pt pp |> Ctree.rep_specify_data + in ctxt end + | get_ctxt_from_PblObj _ _ = raise ERROR "get_ctxt_from_PblObj called by PrfObj or EmptyPtree"; + +fun get_ctxt pt (p_, Pos.Pbl) = + let + val pp = Ctree.par_pblobj pt p_ (*drops the "0"*) + val {ctxt, ...} = Ctree.get_obj I pt pp |> Ctree.rep_specify_data + in ctxt end + | get_ctxt pt pos = + if at_begin_program pos + then get_ctxt_from_PblObj pt pos + else Ctree.get_ctxt pt pos + + + (** Solve_Step.check **) (* @@ -94,7 +120,7 @@ let val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt) - | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj" + | _ => raise ERROR "Solve_Step.check Apply_Method: uncovered case Ctree.get_obj" val {where_, ...} = Problem.from_store ctxt pI val pres = map (I_Model.environment probl |> subst_atomic) where_ val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*) @@ -196,7 +222,7 @@ val thy = Proof_Context.theory_of ctxt val f = Calc.current_formula cs; val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) - val subte = Subst.input_to_terms sube (*?TODO: input requires parse _: _ -> _ option?*) + val subte = Subst.input_to_terms ctxt sube (*?TODO: input requires parse _: _ -> _ option?*) val ro = get_rew_ord ctxt rew_ord' in if foldl and_ (true, map TermC.contains_Var subte) @@ -218,7 +244,17 @@ in Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f)) end - | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*) +(*/----------------- updated----------------------------------* ) + | check (Tactic.Take str) (pt, pos) = + Applicable.Yes (Tactic.Take' + (TermC.parse ((*Solve_Step.*)get_ctxt pt pos) str)) (*always applicable*) +( *------------------- updated----------------------------------*) + | check (Tactic.Take str) (pt, pos) = + let + val ctxt = (*Solve_Step.*)get_ctxt pt pos + val t = Prog_Tac.Take_adapt_to_type ctxt str + in Applicable.Yes (Tactic.Take' t) end +(*\----------------- updated----------------------------------*) | check (Tactic.Begin_Trans) cs = Applicable.Yes (Tactic.Begin_Trans' (Calc.current_formula cs)) | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*) @@ -327,9 +363,11 @@ Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term t'), pt) end - | add (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) = + | add (Tactic.Tac_ (_, f, id, f')) l (pt, pos as (p, _)) = let - val (pt, c) = Ctree.cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Ctree.Complete + val ctxt = Ctree.get_ctxt pt pos + val (pt, c) = Ctree.cappend_atomic pt p l + (TermC.parse ctxt f) (Tactic.Tac id) (TermC.parse ctxt f', []) Ctree.Complete in ((p,Pos.Res), c, Test_Out.FormKF f', pt) end diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/Knowledge/Diff.thy --- a/src/Tools/isac/Knowledge/Diff.thy Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed Oct 19 10:43:04 2022 +0200 @@ -244,7 +244,7 @@ (** CAS-commands **) (*.handle cas-input like "Diff (a * x^3 + b, x)".*) -(* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)"); +(* val (t, pairl) = strip_comb (TermC.parse_test @{context} "Diff (a * x^3 + b, x)"); val [Const (\<^const_name>\Pair\, _) $ t $ bdv] = pairl; *) fun argl2dtss [Const (\<^const_name>\Pair\, _) $ t $ bdv] = @@ -390,7 +390,7 @@ ML \ (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*) -(* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)"); +(* val (t, pairl) = strip_comb (TermC.parse_test @{context} "Differentiate (A = s * (a - s), s)"); val [Const (\<^const_name>\Pair\, _) $ t $ bdv] = pairl; *) fun argl2dtss [Const (\<^const_name>\Pair\, _) $ t $ bdv] = diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/Knowledge/Root.thy --- a/src/Tools/isac/Knowledge/Root.thy Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Oct 19 10:43:04 2022 +0200 @@ -69,7 +69,7 @@ | NONE => NONE) | _ => NONE); -(*val (thmid, op_, t as Const(op0,t0) $ arg) = ("", "", str2term "sqrt 0"); +(*val (thmid, op_, t as Const(op0,t0) $ arg) = ("", "", TermC.parse_test @{context} "sqrt 0"); > eval_sqrt thmid op_ t thy; > val Free (n1,t1) = arg; > val SOME ni = int_of_str n1; diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/Knowledge/Simplify.thy --- a/src/Tools/isac/Knowledge/Simplify.thy Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/Knowledge/Simplify.thy Wed Oct 19 10:43:04 2022 +0200 @@ -43,7 +43,7 @@ (*.function for handling the cas-input "Simplify (2*a + 3*a)": make a model which is already in ctree-internal format.*) -(* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)"); +(* val (h,argl) = strip_comb (TermC.parse_test @{context} "Simplify (2*a + 3*a)"); val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info_get_theory "Simplify"))) "Simplify (2*a + 3*a)"); *) diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/MathEngBasic/ctree-basic.sml --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Oct 19 10:43:04 2022 +0200 @@ -22,6 +22,9 @@ datatype ppobj = PblObj of specify_data | PrfObj of solve_data datatype ctree = EmptyPtree | Nd of ppobj * ctree list + val rep_solve_data: ppobj -> solve_data + val rep_specify_data: ppobj -> specify_data + (** basic functions **) val e_ctree : ctree (* TODO: replace by EmptyPtree*) val existpt' : Pos.pos' -> ctree -> bool @@ -226,6 +229,11 @@ type state = ctree * pos' val e_state = (EmptyPtree , e_pos') +fun rep_solve_data (PrfObj solve_data) = solve_data + | rep_solve_data _ = raise ERROR "rep_solve_data ONLY for solve_data" +fun rep_specify_data (PblObj specify_data) = specify_data + | rep_specify_data _ = raise ERROR "rep_solve_data ONLY for solve_data" + (*** minimal set of functions on Ctree* **) diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/MathEngine/step.sml --- a/src/Tools/isac/MathEngine/step.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/MathEngine/step.sml Wed Oct 19 10:43:04 2022 +0200 @@ -16,6 +16,7 @@ val inconsistent: Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context -> Pos.pos' -> Ctree.ctree -> Calc.T + \<^isac_test>\ val specify_do_next: Calc.T -> string * Calc.state_post val switch_specify_solve: Pos.pos_ -> Calc.T -> string * Calc.state_post diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/ProgLang/Prog_Expr.thy --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Wed Oct 19 10:43:04 2022 +0200 @@ -262,18 +262,18 @@ (*evaluate identity > reflI; val it = "(?t = ?t) = True" -> val t = str2term "x = 0"; +> val t = TermC.parse_test @{context} "x = 0"; > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; -> val t = str2term "1 = 0"; +> val t = TermC.parse_test @{context} "1 = 0"; > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; ----------- thus needs Rule.Eval ! -> val t = str2term "0 = 0"; +> val t = TermC.parse_test @{context} "0 = 0"; > val SOME (t',_) = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t; > UnparseC.term t'; val it = \<^const_name>\True\ -val t = str2term "Not (x = 0)"; +val t = TermC.parse_test @{context} "Not (x = 0)"; atomt t; UnparseC.term t; *** ------------- *** Const ( Not) @@ -298,17 +298,17 @@ HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))) | eval_ident _ _ _ _ = NONE; (* TODO -> val t = str2term "x =!= 0"; +> val t = TermC.parse_test @{context} "x =!= 0"; > val SOME (str, t') = eval_ident "ident_" "b" t thy; > UnparseC.term t'; val str = "ident_(x)_(0)" : string val it = "(x =!= 0) = False" : string -> val t = str2term "1 =!= 0"; +> val t = TermC.parse_test @{context} "1 =!= 0"; > val SOME (str, t') = eval_ident "ident_" "b" t thy; > UnparseC.term t'; val str = "ident_(1)_(0)" : string val it = "(1 =!= 0) = False" : string -> val t = str2term "0 =!= 0"; +> val t = TermC.parse_test @{context} "0 =!= 0"; > val SOME (str, t') = eval_ident "ident_" "b" t thy; > UnparseC.term t'; val str = "ident_(0)_(0)" : string diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/ProgLang/Prog_Tac.thy --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Oct 19 10:43:04 2022 +0200 @@ -63,7 +63,11 @@ val get_first_argument : term -> term option (*TODO rename get_first_argument*) val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option val is: term -> bool -end + + val Substitute_adapt_to_type: theory -> term -> Subst.as_string_eqs +(**)val Rewrite_Inst_adapt_to_type: theory -> term -> TermC.as_string list(**) +(**)val Take_adapt_to_type: Proof.context -> TermC.as_string -> term(**) +end \ ML \ (**) structure Prog_Tac(**): PROGAM_TACTIC(**) = @@ -208,9 +212,36 @@ SubProblem, Substitute, Take, Check_elementwise, Assumptions] fun is t = TermC.contains_Const_typeless all_Consts t -(**)end(**) + + +(** adapt_to_type arguments of specific tactics **) +(* + Programs are stored as terms typed by the theory they are defined in. + Specific Prog_Tac take substitutions as arguments; these substitutions have + the variables to be substituted typed with the program; + these variables need to be adapt_to_type from the user-context in order to conform + with the terms input by the user. +*) +fun Substitute_adapt_to_type thy isasub = + isasub + |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy) + |> TermC.isalist2list + |> Subst.eqs_to_input; + +fun Rewrite_Inst_adapt_to_type thy sub = + sub +(*|> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy)*) + |> Subst.program_to_input + +(*eliminated ERROR: c_2 = (0 :: 'a)*) +fun Take_adapt_to_type ctxt arg = arg + |> TermC.parse ctxt + |> Model_Pattern.adapt_term_to_type ctxt + +(**)end(*struct*) \ ML \ \ + subsection \TODO\ ML \ \ ML \ diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/Specify/p-spec.sml --- a/src/Tools/isac/Specify/p-spec.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/Specify/p-spec.sml Wed Oct 19 10:43:04 2022 +0200 @@ -221,7 +221,7 @@ => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p" val ctxt = Proof_Context.init_global (ThyC.get_theory sdI) - in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.str2term hdf)) + in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.parse ctxt hdf)) else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*) let val (pos_, pits, mits) = if dI <> sdI diff -r 04f8699d2c9d -r bb3140a02f3d src/Tools/isac/Test_Code/test-code.sml --- a/src/Tools/isac/Test_Code/test-code.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/src/Tools/isac/Test_Code/test-code.sml Wed Oct 19 10:43:04 2022 +0200 @@ -86,7 +86,7 @@ | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next" | _ => raise ERROR "me: uncovered case Step.do_next") val tac = - case ts of + case ts of tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac; in diff -r 04f8699d2c9d -r bb3140a02f3d test/Tools/isac/BaseDefinitions/substitution.sml --- a/test/Tools/isac/BaseDefinitions/substitution.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/test/Tools/isac/BaseDefinitions/substitution.sml Wed Oct 19 10:43:04 2022 +0200 @@ -83,10 +83,9 @@ "-------- fun input_to_terms -------------------------------------------------"; "-------- fun input_to_terms -------------------------------------------------"; "-------- fun input_to_terms -------------------------------------------------"; -Subst.input_to_terms: Subst.input -> term list; val input = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(aaa, bbb + 2)"]; -case Subst.input_to_terms input of +case Subst.input_to_terms @{context} input of [Const (\<^const_name>\Pair\, _) $ (Const (\<^const_name>\Cons\, _) $ (Const (\<^const_name>\Char\, _) $ Const (\<^const_name>\False\, _) $ _ $ _ $ _ $ _ $ _ $ _ $ _) $ _) $ diff -r 04f8699d2c9d -r bb3140a02f3d test/Tools/isac/Interpret/lucas-interpreter.sml --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Oct 19 10:43:04 2022 +0200 @@ -24,13 +24,103 @@ CalcTreeTEST [(["functionTerm (x \ 2 + 1)", "integrateBy x", "antiDerivative FF"], ("Integrate", ["integrate", "function"], ["diff", "integration"]))]; -val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\ Add_Given "functionTerm (x \ 2 + 1)"*) val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; + +val (p''',_,f,nxt''',_,pt''') = me nxt p c pt; (*nxt'''= Specify_Method ["diff", "integration"]*) +(*/------------------- step into me Specify_Method ["diff", "integration"] -----------------\*) +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt'''); + val (pt, p) = + (*Step.by_tactic is here for testing by me; do_next would suffice in me*) + case Step.by_tactic tac (pt, p) of + ("ok", (_, _, ptp)) => ptp + +val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) = (*case*) + Step.do_next p ((pt, Pos.e_pos'), []) (*of*); +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) + = (p, ((pt, Pos.e_pos'), [])); + (*if*) Pos.on_calc_end ip (*else*); + val (_, probl_id, _) = Calc.references (pt, p); +val _ = + (*case*) tacis (*of*); + (*if*) probl_id = Problem.id_empty (*else*); + +val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) = + Step.switch_specify_solve p_ (pt, ip); +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip)); + (*if*) Pos.on_specification ([], state_pos) (*then*); + + Step.specify_do_next (pt, input_pos); +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos); + val (_, (p_', tac)) = Specify.find_next_step ptp + val ist_ctxt = Ctree.get_loc pt (p, p_) +val Tactic.Apply_Method mI = + (*case*) tac (*of*); + +val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) = + LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) + ist_ctxt (pt, (p, p_')); +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) + = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), + ist_ctxt, (pt, (p, p_'))); + val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*) + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl) + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj" + val {ppc, ...} = MethodC.from_store ctxt mI; + val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc + val srls = LItool.get_simplifier (pt, pos) + val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of + (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr) + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate" + val ini = LItool.implicit_take prog env; + val pos = start_new_level pos +val NONE = + (*case*) ini (*of*); + +val Next_Step (iii, ccc, ttt) = (*case*) + LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt (*of*); +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt) + = (prog, (pt, (lev_dn p, Res)), is, ctxt); + + (*case*) + scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*); +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) + = ((prog, (ptp, ctxt)), (Pstate ist)); + (*if*) path = [] (*then*); + +val Accept_Tac (ttt, sss, ccc) = + scan_dn cc (trans_scan_dn ist) (Program.body_of prog); +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\Let\(*1*), _) $ e $ (Abs (i, T, b)))) + = (cc, (trans_scan_dn ist), (Program.body_of prog)); + +val Accept_Tac (ttt, sss, ccc) = (*case*) + scan_dn cc (ist |> path_down [L, R]) e (*of*); +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t) + = (cc, (ist |> path_down [L, R]), e); + (*if*) Tactical.contained_in t (*else*); +val (Program.Tac prog_tac, form_arg) = + (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*); + +val Accept_Tac (ttt, sss, ccc) = + check_tac cc ist (prog_tac, form_arg); +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) + = (cc, ist, (prog_tac, form_arg)); + val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac +val _ = + (*case*) m (*of*); + + (*case*) +Solve_Step.check m (pt, p) (*of*); +"~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos as (p_, p))) = (m, (pt, p)); + +(*+*)val ([0], Res) = pos; (*<<<-------------------------*) +(*-------------------- stop step into me Specify_Method ["diff", "integration"] -------------*) +(*\------------------- step into me Specify_Method ["diff", "integration"] -----------------/*) + +val (p,_,f,nxt,_,pt) = me nxt''' p''' c pt'''; case nxt of (Apply_Method ["diff", "integration"]) => () | _ => error "integrate.sml -- me method [diff,integration] -- spec"; "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")"; diff -r 04f8699d2c9d -r bb3140a02f3d test/Tools/isac/Knowledge/algein.sml --- a/test/Tools/isac/Knowledge/algein.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/test/Tools/isac/Knowledge/algein.sml Wed Oct 19 10:43:04 2022 +0200 @@ -107,7 +107,9 @@ UnparseC.term t' = "0 = ?a1 * 0"; (* = true*) val sube = ["?a1 = (3::real)"]; -val subte = Subst.input_to_terms sube; +(*----------------vvvvvvvvvvvvvv ERROR Unbound schematic variable: ?a1 + --------------- review together with development of Widerspruch 3 = 77* ) +val subte = Subst.input_to_terms @{context} sube; UnparseC.terms_short subte = "[?a1 = 3]"; (* = true*) val subst = Subst.T_from_string_eqs thy sube; foldl and_ (true, map TermC.contains_Var subte); @@ -119,4 +121,4 @@ (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!! val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t''; *) - +( *----------------^^^^^^^^^^^^^^ ERROR Unbound schematic variable: ?a1*) diff -r 04f8699d2c9d -r bb3140a02f3d test/Tools/isac/Knowledge/eqsystem-1.sml --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Wed Oct 19 10:43:04 2022 +0200 @@ -3,29 +3,27 @@ (c) due to copyright terms *) -"-----------------------------------------------------------------"; -"table of contents -----------------------------------------------"; -"-----------------------------------------------------------------"; -"----------- occur_exactly_in ------------------------------------"; -"----------- problems --------------------------------------------"; -"----------- rewrite-order ord_simplify_System -------------------"; -"----------- rewrite in [EqSystem,normalise,2x2] -----------------"; -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---"; -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----"; -"----------- rewrite in [EqSystem,normalise,4x4] -----------------"; -"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --"; -"----------- refine [linear,system]-------------------------------"; -"----------- refine [2x2,linear,system] search error--------------"; -(*^^^--- eqsystem-1.sml #####################################################################*) -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; -(*^^^--- eqsystem-1a.sml ##################################################################### - vvv--- eqsystem-2.sml #####################################################################*) -"----------- me [linear,system] ..normalise..top_down_sub..-------"; -"----------- all systems from Biegelinie -------------------------"; -"----------- 4x4 systems from Biegelinie -------------------------"; -"-----------------------------------------------------------------"; -"-----------------------------------------------------------------"; -"-----------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"table of contents -----------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml"; +"----------- problems -----------------------------------------------------------equsystem-1.sml"; +"----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml"; +"----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml"; +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml"; +"----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml"; +"----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml"; +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml"; +"----------- refine [linear,system]----------------------------------------------equsystem-1.sml"; +"----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml"; +"----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml"; +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml"; +"----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml"; +"----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml"; +"----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml"; +"-----------------------------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; val thy = @{theory "EqSystem"}; val ctxt = Proof_Context.init_global thy; @@ -176,6 +174,7 @@ if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2]" then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3"; + "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---"; "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---"; "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---"; @@ -285,6 +284,8 @@ \ c + (c_2 + (c_3 + c_4)) = 0]" then () else error "eqsystem.sml rewrite in 4x4 order_system"; + + "----------- refine [linear,system]-------------------------------"; "----------- refine [linear,system]-------------------------------"; "----------- refine [linear,system]-------------------------------"; @@ -423,6 +424,8 @@ val TermC.matches = Refine.refine fmz ["LINEAR", "system"]; ============ inhibit exn WN120314 ==============================================*) + + "----------- Refine.refine [2x2,linear,system] search error--------------"; "----------- Refine.refine [2x2,linear,system] search error--------------"; "----------- Refine.refine [2x2,linear,system] search error--------------"; @@ -512,11 +515,12 @@ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *) + "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; -val fmz = ["equalities [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2,\ - \0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2]", +val fmz = ["equalities [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2," ^ + "0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2]", "solveForVars [c, c_2]", "solution LL"]; val (dI',pI',mI') = ("Biegelinie",["normalise", "2x2", "LINEAR", "system"], @@ -532,7 +536,7 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*); +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; @@ -549,13 +553,6 @@ | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution"; val (p,_,f,nxt,_,pt) = me nxt p c pt; -val PblObj {probl,...} = get_obj I pt [5]; - (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl; -(*[ -(1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2]])), -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])), -(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))] -*) val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; @@ -569,8 +566,33 @@ | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished"; val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; +(* final test ... ----------------------------------------------------------------------------*) if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f"; + case nxt of (End_Proof') => () | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'"; + +Test_Tool.show_pt pt (*[ +(([], Frm), solveSystem + [[0 = - 1 * q_0 * 0 \ 2 div 2 + 0 * c + c_2], + [0 = - 1 * q_0 * L \ 2 div 2 + L * c + c_2]] + [[c], [c_2]]), +(([1], Frm), [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2, + 0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2]), +(([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \ 2 * q_0) / 2]), +(([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \ 2 / 2 + (L * c + c_2)]), +(([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \ 2 / 2)]), +(([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2]), +(([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \ 2 / 2] [c_2]), +(([5, 1], Frm), L * c + c_2 = q_0 * L \ 2 / 2), +(([5, 1], Res), L * c + 0 = q_0 * L \ 2 / 2), +(([5, 2], Res), L * c = q_0 * L \ 2 / 2), +(([5, 3], Res), c = q_0 * L \ 2 / 2 / L), +(([5, 4], Res), c = L * q_0 / 2), +(([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]), +(([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]), +(([5], Res), [c = L * q_0 / 2, c_2 = 0]), +(([], Res), [c = L * q_0 / 2, c_2 = 0])] +*) diff -r 04f8699d2c9d -r bb3140a02f3d test/Tools/isac/Knowledge/eqsystem-1a.sml --- a/test/Tools/isac/Knowledge/eqsystem-1a.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/test/Tools/isac/Knowledge/eqsystem-1a.sml Wed Oct 19 10:43:04 2022 +0200 @@ -2,34 +2,32 @@ author: Walther Neuper 050826, *) -"-----------------------------------------------------------------"; -"table of contents -----------------------------------------------"; -"-----------------------------------------------------------------"; -"----------- occur_exactly_in ------------------------------------"; -"----------- problems --------------------------------------------"; -"----------- rewrite-order ord_simplify_System -------------------"; -"----------- rewrite in [EqSystem,normalise,2x2] -----------------"; -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---"; -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----"; -"----------- rewrite in [EqSystem,normalise,4x4] -----------------"; -"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --"; -"----------- refine [linear,system]-------------------------------"; -"----------- refine [2x2,linear,system] search error--------------"; -(*^^^--- eqsystem-1.sml #####################################################################*) -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; -(*^^^--- eqsystem-1a.sml ##################################################################### - vvv--- eqsystem-2.sml #####################################################################*) -"----------- me [linear,system] ..normalise..top_down_sub..-------"; -"----------- all systems from Biegelinie -------------------------"; -"----------- 4x4 systems from Biegelinie -------------------------"; -"-----------------------------------------------------------------"; -"-----------------------------------------------------------------"; -"-----------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"table of contents -----------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml"; +"----------- problems -----------------------------------------------------------equsystem-1.sml"; +"----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml"; +"----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml"; +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml"; +"----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml"; +"----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml"; +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml"; +"----------- refine [linear,system]----------------------------------------------equsystem-1.sml"; +"----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml"; +"----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml"; +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml"; +"----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml"; +"----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml"; +"----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml"; +"-----------------------------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml"; +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml"; +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml"; val fmz = ["equalities [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2,\ \0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2]", "solveForVars [c, c_2]", "solution LL"]; diff -r 04f8699d2c9d -r bb3140a02f3d test/Tools/isac/Knowledge/eqsystem-2.sml --- a/test/Tools/isac/Knowledge/eqsystem-2.sml Sun Oct 09 09:01:29 2022 +0200 +++ b/test/Tools/isac/Knowledge/eqsystem-2.sml Wed Oct 19 10:43:04 2022 +0200 @@ -2,30 +2,27 @@ author: Walther Neuper 050826, (c) due to copyright terms *) - -"-----------------------------------------------------------------"; -"table of contents -----------------------------------------------"; -"-----------------------------------------------------------------"; -"----------- occur_exactly_in ------------------------------------"; -"----------- problems --------------------------------------------"; -"----------- rewrite-order ord_simplify_System -------------------"; -"----------- rewrite in [EqSystem,normalise,2x2] -----------------"; -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---"; -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----"; -"----------- rewrite in [EqSystem,normalise,4x4] -----------------"; -"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --"; -"----------- refine [linear,system]-------------------------------"; -"----------- refine [2x2,linear,system] search error--------------"; -(*^^^--- eqsystem-1.sml #####################################################################*) -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; -(*^^^--- eqsystem-1a.sml ##################################################################### - vvv--- eqsystem-2.sml #####################################################################*) -"----------- me [linear,system] ..normalise..top_down_sub..-------"; -"----------- all systems from Biegelinie -------------------------"; -"----------- 4x4 systems from Biegelinie -------------------------"; -"-----------------------------------------------------------------"; -"-----------------------------------------------------------------"; -"-----------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"table of contents -----------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml"; +"----------- problems -----------------------------------------------------------equsystem-1.sml"; +"----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml"; +"----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml"; +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml"; +"----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml"; +"----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml"; +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml"; +"----------- refine [linear,system]----------------------------------------------equsystem-1.sml"; +"----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml"; +"----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml"; +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml"; +"----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml"; +"----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml"; +"----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml"; +"-----------------------------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; val thy = @{theory "EqSystem"}; val ctxt = Proof_Context.init_global thy; diff -r 04f8699d2c9d -r bb3140a02f3d test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Sun Oct 09 09:01:29 2022 +0200 +++ b/test/Tools/isac/Test_Isac.thy Wed Oct 19 10:43:04 2022 +0200 @@ -140,10 +140,11 @@ "~~~~~ from fun xxx \fun yyy \fun zzz , return:"; val () = (); (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*); "xx" -^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**) -\ ML \ (*//---------------- adhoc inserted ------------------------------------------------\\*) -\ ML \ -\ ML \ (*\\---------------- adhoc inserted ------------------------------------------------//*) +^ "xxx" (*+*) (*+++*) (* keep for continuation*) (*isa*) (*isa2*) (**) +\ ML \ (*//----------- adhoc inserted n ----------------------------------------------------\\*) + (*//----------------- adhoc inserted n ----------------------------------------------------\\*) +(*\\------------------ adhoc inserted n ----------------------------------------------------//*) +\ ML \ (*\\----------- adhoc inserted n ----------------------------------------------------//*) \ ML \ \ ML \ diff -r 04f8699d2c9d -r bb3140a02f3d test/Tools/isac/Test_Isac_Short.thy --- a/test/Tools/isac/Test_Isac_Short.thy Sun Oct 09 09:01:29 2022 +0200 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Oct 19 10:43:04 2022 +0200 @@ -142,9 +142,10 @@ (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*); "xx" ^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**) -\ ML \ (*//---------------- adhoc inserted ------------------------------------------------\\*) -\ ML \ -\ ML \ (*\\---------------- adhoc inserted ------------------------------------------------//*) +\ ML \ (*//----------- adhoc inserted n ----------------------------------------------------\\*) + (*//----------------- adhoc inserted n ----------------------------------------------------\\*) +(*\\------------------ adhoc inserted n ----------------------------------------------------//*) +\ ML \ (*\\----------- adhoc inserted n ----------------------------------------------------//*) \ ML \ \ ML \ @@ -299,7 +300,7 @@ ML_file "Knowledge/eqsystem-1a.sml" ML_file "Knowledge/eqsystem-2.sml" ML_file "Knowledge/test.sml" - ML_file "Knowledge/polyminus.sml" + ML_file "Knowledge/polyminus.sml" ML_file "Knowledge/vect.sml" ML_file "Knowledge/diff-app.sml" (* postponed to dev. specification | TP-prog. *) ML_file "Knowledge/biegelinie-1.sml" diff -r 04f8699d2c9d -r bb3140a02f3d test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Sun Oct 09 09:01:29 2022 +0200 +++ b/test/Tools/isac/Test_Some.thy Wed Oct 19 10:43:04 2022 +0200 @@ -57,30 +57,31 @@ "~~~~~ from fun xxx \fun yyy \fun zzz , return:"; val () = (); (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*); "xx" -^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**) -\ ML \ (*//---------------- adhoc inserted ------------------------------------------------\\*) -\ ML \ -\ ML \ (*\\---------------- adhoc inserted ------------------------------------------------//*) -\ ML \ (*//---------------- adhoc copied up -----------------------------------------------\\*) -\ ML \ -\ ML \ (*\\---------------- adhoc copied up -----------------------------------------------//*) -(*/------------------- step into XXXXX -----------------------------------------------------\*) -(*-------------------- stop step into XXXXX -------------------------------------------------*) -(*\------------------- step into XXXXX -----------------------------------------------------/*) -(*-------------------- contiue step into XXXXX ----------------------------------------------*) -(*/------------------- check entry to XXXXX ------------------------------------------------\*) -(*\------------------- check entry to XXXXX ------------------------------------------------/*) -(*/------------------- check within XXXXX --------------------------------------------------\*) -(*\------------------- check within XXXXX --------------------------------------------------/*) -(*/------------------- check result of XXXXX -----------------------------------------------\*) -(*\------------------- check result of XXXXX -----------------------------------------------/*) -(* final test ...*) -(*/------------------- build new fun XXXXX -------------------------------------------------\*) -(*\------------------- build new fun XXXXX -------------------------------------------------/*) -(**** chapter ############################################################################ ****) -(*** section ============================================================================== ***) -(** subsection ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ **) -(* subsubsection ............................................................................ *) +^ "xxx" (*+*) (*+++*) (* keep for continuation*) (*isa*) (*isa2*) (**) +\ ML \ (*//----------- adhoc inserted n ----------------------------------------------------\\*) + (*//----------------- adhoc inserted n ----------------------------------------------------\\*) +(*\\------------------ adhoc inserted n ----------------------------------------------------//*) +\ ML \ (*\\----------- adhoc inserted n ----------------------------------------------------//*) + +\ ML \ (*//----------- step into XXXXX -----------------------------------------------------\\*) +(*//------------------ step into XXXXX -----------------------------------------------------\\*) +(*-------------------- stop step into XXXXX --------------------------------------------------*) +\ ML \ (*------------- stop step into XXXXX --------------------------------------------------*) +(*\\------------------ step into XXXXX -----------------------------------------------------//*) +\ ML \ (*\\----------- step into XXXXX -----------------------------------------------------//*) + +(*/------------------- check entry to XXXXX -------------------------------------------------\*) +(*\------------------- check entry to XXXXX -------------------------------------------------/*) +(*/------------------- check within XXXXX ---------------------------------------------------\*) +(*\------------------- check within XXXXX ---------------------------------------------------/*) +(*/------------------- check result of XXXXX ------------------------------------------------\*) +(*\------------------- check result of XXXXX ------------------------------------------------/*) +(* final test ... ----------------------------------------------------------------------------*) + +\ ML \ (*//----------- build new fun XXXXX -------------------------------------------------\\*) +(*//------------------ build new fun XXXXX -------------------------------------------------\\*) +(*\\------------------ build new fun XXXXX -------------------------------------------------//*) +\ ML \ (*\\----------- build new fun XXXXX -------------------------------------------------//*) \ ML \ \ ML \ @@ -108,10 +109,476 @@ \ ML \ \ -section \===================================================================================\ +section \========= test/../Knowlegde/equsystem-1a.sml ======================================\ ML \ \ ML \ +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml"; +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml"; +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml"; +val fmz = ["equalities [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2,\ + \0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2]", + "solveForVars [c, c_2]", "solution LL"]; +val (dI',pI',mI') = + ("Biegelinie",["normalise", "2x2", "LINEAR", "system"], + ["EqSystem", "normalise", "2x2"]); +val p = e_pos'; val c = []; +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => () + | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify"; + +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; + +(*+*)if f2str f = + "[0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2,\n" ^ + " 0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2]" then () else error ""; +(*+*)(Ctree.get_istate_LI pt p |> Istate.string_of) = + "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)"; + +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; + +(*+isa==isa2*)val "[c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2]" = f2str f; + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\"], [R, L, R, L, R, R, R, L, R, R], srls_normalise_2x2, SOME e_s, \n[c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2], ORundef, true, false)" = +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of); + +case nxt of + (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => () + | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem"; + +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; +case nxt of + (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => () + | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution"; + +val (p,_,f,nxt,_,pt) = me nxt p c pt; + + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" = +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of); + +val (p''',_,f,nxt''',_,pt''') = me nxt p c pt;f2str f; +(*/------------------- step into me Apply_Method -------------------------------------------\*) +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt); \ ML \ + val (pt'''', p'''') = (* keep for continuation*) + (*Step.by_tactic is here for testing by me; do_next would suffice in me*) + + case Step.by_tactic tac (pt, p) of + ("ok", (_, _, ptp)) => ptp; +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p)); + +(*+isa==isa2*)val ([5], Met) = p; +(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt (fst p); + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" = +(*+isa==isa2*)is1 |> Istate.string_of; + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" = +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of); + + (*case*) + Step.check tac (pt, p) (*of*); +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p) ); + +(*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" = +(*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of); + + (*if*) Tactic.for_specify tac (*else*); +val Applicable.Yes xxx = + +Solve_Step.check tac (ctree, pos); + +(*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" = +(*+isa==isa2*)(Ctree.get_istate_LI ctree pos |> Istate.string_of); + +"~~~~~ from Step.check to Step.by_tactic return val:"; val (Applicable.Yes tac') = (Applicable.Yes xxx); + (*if*) Tactic.for_specify' tac' (*else*); + +Step_Solve.by_tactic tac' ptp;; +"~~~~~ fun by_tactic , args:"; val ((tac as Tactic.Apply_Method' _), (ptp as (pt, p))) + = (tac', ptp); + +(*+*)val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" = +(*+isa==isa2*)(Ctree.get_istate_LI pt p |> Istate.string_of); + + LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp; +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) + = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp); + val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*) + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl) + val {ppc, ...} = MethodC.from_store ctxt mI; + val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc + val srls = LItool.get_simplifier (pt, pos) + val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of + (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr) + +(*+*)val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)" = +(*+isa==isa2*)is |> Istate.string_of + + val ini = LItool.implicit_take prog env; + val pos = start_new_level pos +val NONE = + (*case*) ini (*of*); + val (tac''', ist''', ctxt''') = + case LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt of + Next_Step (ist, ctxt, tac) => (tac, ist, ctxt) + + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" = +(*+isa==isa2*)ist''' |> Istate.string_of; + +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt) + = (prog ,(pt, (lev_dn p, Res)), is, ctxt); +val Accept_Tac + (Take' ttt, iii, _) = + (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*); + +(*+isa==isa2*)val "c_2 = 0" = (ttt |> UnparseC.term); + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" = +(*+isa==isa2*)(Pstate iii |> Istate.string_of); + +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) + = ((prog, (ptp, ctxt)), (Pstate ist)); + (*if*) path = [] (*then*); + + scan_dn cc (trans_scan_dn ist) (Program.body_of prog); +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\Let\(*1*), _) $ e $ (Abs (i, T, b)))) + = (cc, (trans_scan_dn ist), (Program.body_of prog)); + + (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*); +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t) + = (cc ,(ist |> path_down [L, R]), e); + + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" = +(*+isa==isa2*)(Pstate ist |> Istate.string_of); + + (*if*) Tactical.contained_in t (*else*); + + (*case*) + LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*); +"~~~~~ fun check_leaf , args:"; val (call, ctxt, srls, (E, (a, v)), t) + = ("next ", ctxt, eval, (get_subst ist), t); + + (*case*) + Prog_Tac.eval_leaf E a v t (*of*); +"~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const (\<^const_name>\Prog_Tac.Take\, _) $ _))) + = (E, a, v, t); + +val return = + (Program.Tac (subst_atomic E t), NONE:term option); +"~~~~~ from fun eval_leaf \fun check_leaf , return:"; val (Program.Tac stac, a') = return; + val stac' = Rewrite.eval_prog_expr ctxt srls + (subst_atomic (Env.update_opt E (a, v)) stac) + +val return = + (Program.Tac stac', a'); +"~~~~~ from fun check_leaf \fun scan_dn , return:"; val (Program.Tac prog_tac, form_arg) = return; + + check_tac cc ist (prog_tac, form_arg); +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) + = (cc, ist, (prog_tac, form_arg)); + val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac +val _ = + (*case*) m (*of*); (*tac as string/input*) + + (*case*) +Solve_Step.check m (pt, p) (*of*); +"~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos)) = (m, (pt, p)); + +val return = + check_tac cc ist (prog_tac, form_arg) + + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, false)" = +(*+isa==isa2*)(Pstate ist |> Istate.string_of); + +"~~~~~ from fun scan_dn \fun scan_to_tactic \fun find_next_step , return:"; + val (Accept_Tac (tac, ist, ctxt)) = return; + + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" = +(*+isa==isa2*)(Pstate ist |> Istate.string_of) + +val return = + Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac); +"~~~~~ from fun find_next_step \fun by_tactic , return:"; val Next_Step (ist, ctxt, tac) = return; + val (tac', ist', ctxt') = (tac, ist, ctxt) +val Tactic.Take' t = + (*case*) tac' (*of*); + val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt'); + +(*+isa==isa2*)pos; (*from check_tac*) +(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt [5]; + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nSubproblem\n (''Biegelinie'',\n ??.\<^const>String.char.Char ''triangular'' ''2x2'' ''LINEAR'' ''system''), ORundef, true, true)" = +(*+isa==isa2*)is1 |> Istate.string_of; + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" = +(*+isa==isa2*)(ist' |> Istate.string_of) +(*-------------------- stop step into me Apply_Method ----------------------------------------*) +(*+isa==isa2*)val "c_2 = 0" = f2str f; + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\", \"\n(v_s, [c, c_2])\"], [R, L, R], srls_normalise_2x2, NONE, \nc_2 = 0, ORundef, true, false)" = +(*+isa==isa2*)(Ctree.get_istate_LI pt''' p''' |> Istate.string_of) +(*\\------------------- step into me Apply_Method ------------------------------------------//*) + +\ ML \ +val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' c pt''';f2str f; +\ ML \ +(*+isa==isa2*)val ([5, 1], Frm) = p''''; +(*+isa==isa2*)val "L * c + c_2 = q_0 * L \ 2 / 2" = f2str f; +(*+isa<>isa2*)val (**)Check_Postcond ["triangular", "2x2", "LINEAR", "system"](** ) + Substitute ["c_2 = 0"]( **) = nxt''''; +(*+isa==isa2*)val (SOME (is1, _), NONE) = get_obj g_loc pt'''' (fst p''''); + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \ 2 / 2, ORundef, true, true)" = +(*+isa==isa2*)is1 |> Istate.string_of; + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \ 2 / 2, ORundef, true, true)" = +(*+isa==isa2*)Ctree.get_istate_LI pt'''' p'''' |> Istate.string_of; +\ ML \ (*//----------- step into me Take ---------------------------------------------------\\*) +(*//------------------ step into me Take ---------------------------------------------------\\*) +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt'''); +\ ML \ + val (pt, p) = (* keep for continuation*) + (*Step.by_tactic is here for testing by me; do_next would suffice in me*) + + case Step.by_tactic tac (pt, p) of + ("ok", (_, _, ptp)) => ptp; +\ ML \ + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \ 2 / 2, ORundef, true, true)" = +(*isa==isa2*)Ctree.get_istate_LI pt p |> Istate.string_of; +\ ML \ + (*case*) + Step.do_next p ((pt, Pos.e_pos'), []) (*of*); +\ ML \ +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), [])); +\ ML \ + (*if*) Pos.on_calc_end ip (*else*); +\ ML \ + val (_, probl_id, _) = Calc.references (pt, p); +\ ML \ +val _ = + (*case*) tacis (*of*); +\ ML \ + (*if*) probl_id = Problem.id_empty (*else*); +\ ML \ + switch_specify_solve p_ (pt, ip); +\ ML \ +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip)); +\ ML \ + (*if*) Pos.on_specification ([], state_pos) (*else*); +\ ML \ + LI.do_next (pt, input_pos); +\ ML \ +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos); +\ ML \ + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); +\ ML \ + val thy' = get_obj g_domID pt (par_pblobj pt p); + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt; +\ ML \ + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \ 2 / 2, ORundef, true, true)" = +(*+isa==isa2*)ist |> Istate.string_of; +\ ML \ + (*case*) + LI.find_next_step sc (pt, pos) ist ctxt (*of*); +\ ML \ +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt) + = (sc, (pt, pos), ist, ctxt); +\ ML \ + (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*); +\ ML \ +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) + = ((prog, (ptp, ctxt)), (Pstate ist)); +\ ML \ + (*if*) path = [] (*else*); +\ ML \ + go_scan_up (prog, cc) (trans_scan_up ist); +\ ML \ +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) + = ((prog, cc), (trans_scan_up ist)); +\ ML \ + val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\"], [R, R, D, R, D, L, R], srls_top_down_2x2, NONE, \nL * c + c_2 = q_0 * L \ 2 / 2, ORundef, true, false)" = +(*+isa==isa2*)Pstate ist |> Istate.string_of; +(*+isa==isa2*)val "L * c + c_2 = q_0 * L \ 2 / 2" = act_arg |> UnparseC.term; +\ ML \ + (*if*) path = [R] (*root of the program body*) (*else*); +\ ML \ + scan_up pcc (ist |> path_up) (go_up path sc); +\ ML \ +"~~~~~ and scan_up , args:"; val ((pcc as (sc, cc)), ist, (Const (\<^const_name>\Let\(*1*), _) $ _)) + = (pcc, (ist |> path_up), (go_up path sc)); +\ ML \ + val (i, body) = check_Let_up ist sc +\ ML \ + (*case*) scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body (*of*); +\ ML \ +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\Let\(*1*), _) $ e $ (Abs (i, T, b)))) + = (cc, (ist |> path_up_down [R, D] |> upd_env i), body); +\ ML \ +val goback = + (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*); +\ ML \ +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\Tactical.Chain\(*1*), _) $ e1 $ e2 $ a)) + = (cc, (ist |> path_down [L, R]), e); +\ ML \ + (*case*) scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 (*of*); +\ ML \ +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t) + = (cc, (ist |> path_down_form ([L, L, R], a)), e1); +\ ML \ + (*if*) Tactical.contained_in t (*else*); +\ ML \ + (*case*) + LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*); +\ ML \ +"~~~~~ fun check_leaf , args:"; val (call, ctxt, srls, (E, (a, v)), t) + = ("next ", ctxt, eval, (get_subst ist), t); +\ ML \ +val (Program.Tac stac, a') = + (*case*) Prog_Tac.eval_leaf E a v t (*of*); +\ ML \ + val stac' = Rewrite.eval_prog_expr ctxt srls + (subst_atomic (Env.update_opt E (a, v)) stac) +\ ML \ +(*+*)val "Substitute [c_2 = 0] (L * c + c_2 = q_0 * L \ 2 / 2)" = stac' |> UnparseC.term; +\ ML \ +val return = + (Program.Tac stac', a') +\ ML \ +"~~~~~ from fun check_leaf \fun scan_dn , return:"; val ((Program.Tac prog_tac, form_arg)) + = (return); +\ ML \ + check_tac cc ist (prog_tac, form_arg); +\ ML \ +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) + = (cc, ist, (prog_tac, form_arg)); +\ ML \ + val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac +\ ML \ +val _ = + (*case*) m (*of*); +\ ML \ + (*case*) +Solve_Step.check m (pt, p) (*of*); +\ ML \ +"~~~~~ fun check , args:"; val ((Tactic.Substitute sube), (cs as (pt, pos as (p, _)))) + = (m, (pt, p)); +\ ML \ + val pp = Ctree.par_pblobj pt p + val ctxt = Ctree.get_loc pt pos |> snd + val thy = Proof_Context.theory_of ctxt + val f = Calc.current_formula cs; + val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) + val subte = Subst.input_to_terms ctxt sube (*?TODO: input requires parse _: _ -> _ option?*) + val ro = get_rew_ord ctxt rew_ord' +\ ML \ + (*if*) foldl and_ (true, map TermC.contains_Var subte) (*else*); +\ ML \ +(*+isa==isa2*)sube : TermC.as_string list +\ ML \ +(*+isa==isa2*)val "L * c + c_2 = q_0 * L \ 2 / 2" = f |> UnparseC.term +\ ML \ +(*+isa<>isa2*)val (** )["c_2 = (0::'a)"]( **)["c_2 = 0"](**) = subte |> map UnparseC.term +\ ML \ +val SOME ttt = + (*case*) Rewrite.rewrite_terms_ ctxt ro erls subte f (*of*); +\ ML \ +\ ML \ (*//----------- build new fun Subst.input_to_terms ----------------------------------\\*) +(*//------------------ build new fun XXXXX -------------------------------------------------\\*) +\ ML \ +fun input_to_terms ctxt strs = map (TermC.parse ctxt) strs; +\ ML \ +input_to_terms: Proof.context -> Subst.input -> Subst.as_eqs +\ ML \ +(* TermC.parse ctxt fails with "c_2 = 0" \ \c_2 = (0 :: 'a)\ and thus requires adapt_to_type*) +fun input_to_terms ctxt strs = strs + |> map (TermC.parse ctxt) + |> map (Model_Pattern.adapt_term_to_type ctxt) +\ ML \ +\ ML \ +\ ML \ +\ ML \ +(*\\------------------ build new fun XXXXX -------------------------------------------------//*) +\ ML \ (*\\----------- build new fun Subst.input_to_terms ----------------------------------//*) +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ text \ +"~~~~~ from fun scan_dn \fun scan_up , return:"; val (Accept_Tac ict) = (goback); +\ text \ +"~~~~~ from fun scan_up \fun go_scan_up" ^ + " \fun scan_to_tactic \fun find_next_step , return:"; val (Accept_Tac (tac, ist, ctxt)) + = (Accept_Tac ict); +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +\ ML \ +(*-------------------- stop step into me Take ------------------------------------------------*) +\ ML \ (*------------- stop step into me Take ------------------------------------------------*) +(*\\------------------ step into me Take ---------------------------------------------------//*) +\ ML \ (*\\----------- step into me Take ---------------------------------------------------//*) +\ ML \ +val (p,_,f,nxt,_,pt) = me nxt'''' p'''' c pt'''';f2str f; +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; +\ ML \ +(*+*)val (**)"L * c + c_2 = q_0 * L \ 2 / 2"(** ) + "[c = L * q_0 / 2, c_2 = 0]"( **) = f2str f; +\ ML \ + val "Pstate ([\"\n(e_s, [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2])\", \"\n(v_s, [c, c_2])\", \"\n(e__s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\"], [R, R, D], srls_normalise_2x2, NONE, \nL * c + c_2 = q_0 * L \ 2 / 2, ORundef, true, true)" = +(*val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2])\", \"\n(v_s, [c, c_2])\", \"\n(e_1, c_2 = 0)\", \"\n(e_2, c = L * q_0 / 2)\", \"\n(e__s, [c_2 = 0, c = L * q_0 / 2])\"], [R, R, D, R, D, R, D, R, D, R, D, L, R], srls_top_down_2x2, SOME e__s, \n[c = L * q_0 / 2, c_2 = 0], ORundef, true, true)" =*) +(*+*)(Ctree.get_istate_LI pt p |> Istate.string_of) +\ text \ +case nxt of + (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => () + | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished"; +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; + +(* final test ... ----------------------------------------------------------------------------*) +if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then () +else error "eqsystem.sml me [EqSys...2x2] finished f2str f"; + +case nxt of + (End_Proof') => () + | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'"; +\ ML \ +Test_Tool.show_pt pt (*[ +(([], Frm), solveSystem + [[0 = - 1 * q_0 * 0 \ 2 div 2 + 0 * c + c_2], + [0 = - 1 * q_0 * L \ 2 div 2 + L * c + c_2]] + [[c], [c_2]]), +(([1], Frm), [0 = - 1 * q_0 * 0 \ 2 / 2 + 0 * c + c_2, + 0 = - 1 * q_0 * L \ 2 / 2 + L * c + c_2]), +(([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \ 2 * q_0) / 2]), +(([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \ 2 / 2 + (L * c + c_2)]), +(([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \ 2 / 2)]), +(([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \ 2 / 2]), +(([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \ 2 / 2] [c_2]), +(([5, 1], Frm), L * c + c_2 = q_0 * L \ 2 / 2), + +(([5, 1], Res), L * c + 0 = q_0 * L \ 2 / 2), +(([5, 2], Res), L * c = q_0 * L \ 2 / 2), +(([5, 3], Res), c = q_0 * L \ 2 / 2 / L), +(([5, 4], Res), c = L * q_0 / 2), +(([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]), +(([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]), +(([5], Res), [c = L * q_0 / 2, c_2 = 0]), +(([], Res), [c = L * q_0 / 2, c_2 = 0])] +*) \ ML \ \ @@ -125,10 +592,26 @@ section \code for copy & paste ===============================================================\ ML \ "~~~~~ fun xxx , args:"; val () = (); -"~~~~~ and xxx , args:"; val () = (); -"~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*)); +"~~~~~ and xxx , args:"; val () = (); +"~~~~~ from fun xxx \fun yyy \fun zzz , return:"; val () = (); (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*); "xx" -^ "xxx" (*+*) +^ "xxx" (*+*) (*+++*) (* keep for continuation*) (*+isa<>isa2*) (**) +\ ML \ (*//----------- adhoc inserted n ----------------------------------------------------\\*) + (*//----------------- adhoc inserted n ----------------------------------------------------\\*) +(*\\------------------ adhoc inserted n ----------------------------------------------------//*) +\ ML \ (*\\----------- adhoc inserted n ----------------------------------------------------//*) + +\ ML \ (*//----------- step into XXXXX -----------------------------------------------------\\*) +(*//------------------ step into XXXXX -----------------------------------------------------\\*) +(*-------------------- stop step into XXXXX --------------------------------------------------*) +\ ML \ (*------------- stop step into XXXXX --------------------------------------------------*) +(*\\------------------ step into XXXXX -----------------------------------------------------//*) +\ ML \ (*\\----------- step into XXXXX -----------------------------------------------------//*) + +\ ML \ (*//----------- build new fun XXXXX -------------------------------------------------\\*) +(*//------------------ build new fun XXXXX -------------------------------------------------\\*) +(*\\------------------ build new fun XXXXX -------------------------------------------------//*) +\ ML \ (*\\----------- build new fun XXXXX -------------------------------------------------//*) \ end