1.1 --- a/src/Tools/isac/CalcElements/calcelems.sml Mon Dec 30 11:16:00 2019 +0100
1.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml Wed Jan 15 11:47:38 2020 +0100
1.3 @@ -56,12 +56,9 @@
1.4 val trace_calc: bool Unsynchronized.ref
1.5 eqtype thmID
1.6 type thm'
1.7 - datatype lrd = D | L | R
1.8 val trace_rewrite: bool Unsynchronized.ref
1.9 val depth: int Unsynchronized.ref
1.10 val assoc_thy: Rule.theory' -> theory
1.11 - type path
1.12 - val path2str: path -> string
1.13 type thm''
1.14 val metID2str: string list -> string
1.15 val e_pblID: pblID
1.16 @@ -456,16 +453,6 @@
1.17 set false for editing IsacKnowledge (done at end of ROOT.ML) *)
1.18 val check_guhs_unique = Unsynchronized.ref true;
1.19
1.20 -
1.21 -datatype lrd = L (*t1 in "t1$t2"*)
1.22 - | R (*t2 in "t1$t2"*) | D; (*b in Abs(_,_,b*)
1.23 -type path = lrd list;
1.24 -fun ldr2str L = "L"
1.25 - | ldr2str R = "R"
1.26 - | ldr2str D = "D";
1.27 -fun path2str k = (strs2str' o (map ldr2str)) k;
1.28 -
1.29 -
1.30 (* the pattern for an item of a problems model or a methods guard *)
1.31 type pat =
1.32 (string * (* field *)
2.1 --- a/src/Tools/isac/CalcElements/contextC.sml Mon Dec 30 11:16:00 2019 +0100
2.2 +++ b/src/Tools/isac/CalcElements/contextC.sml Wed Jan 15 11:47:38 2020 +0100
2.3 @@ -13,6 +13,7 @@
2.4 val get_assumptions : Proof.context -> term list
2.5 val insert_assumptions : term list -> Proof.context -> Proof.context
2.6 val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context
2.7 +(*val subpbl_to_caller .. rename according to naming convention TODO*)
2.8 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.9 (*NONE*)
2.10 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.11 @@ -20,163 +21,6 @@
2.12 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.13 end
2.14
2.15 -(* survey on handling contexts:
2.16 --------------------------------
2.17 - theory is required for Pattern.match (and thus for Tactic.Rewrite* ), while
2.18 - ctxt is required for parsing and for managing pre-conditions and assumptions.
2.19 - * model-specify-phase:
2.20 - * Tactic.Model_Problem does declare_constraints for parsing (in Tactic.Add_Given, etc)
2.21 - ("insert_assumptions pres" has to wait for completing Tactic.Add_Given, etc)
2.22 - (Tactic.Refine_Problem uses theory NOT ctxt due to Pattern.match)
2.23 - *
2.24 - *
2.25 - * solve-phase by Lucas-Interpretation:
2.26 - * locate_input_tactic:
2.27 - * Tactic.Apply_Method
2.28 - * initialises ctxt (declare_constraints' + insert_assumptions pres) by init_pstate
2.29 - * in solve for root problem
2.30 - * in by_tactic for subproblem
2.31 - * Tactic.Rewrite* create assumptions; respective insert_assumptions is done by associate
2.32 - * associate..Subproblem' returns ctxt ONLY with declare_constraints',
2.33 - with insert_assumptions wait for Tactic.Apply_Method
2.34 - * storing ctxt is done after return form locate_input_tactic
2.35 - * find_next_tactic:
2.36 - * TODO initialises ctxt by TODO
2.37 - * Tactic.Rewrite* create assumptions; respective insert_assumptions TODO
2.38 - *
2.39 - *
2.40 - *
2.41 - * locate_input_formula: follows sig. of find_next_tactic
2.42 - * changing from one method to another (in find_next_tactic only):
2.43 - * from method to sub-program: just add new preconditions of the guard
2.44 - * locate_input_tactic: init_pstate by by_tactic
2.45 - * find_next_tactic:
2.46 - * from_subpbl_to_caller
2.47 - * finishing a method:
2.48 - * Tactic.Check_Postcond' uses ctxt for proving the post-condition (not yet implemented)
2.49 - *
2.50 - *
2.51 - *
2.52 - *
2.53 -================================================================================================
2.54 -call hierarchy
2.55 -================================================================================================
2.56 -
2.57 - locatetac
2.58 - applicable_in (p, p_) pt (Tactic.Apply_Method pres
2.59 - insert_assumptions
2.60 -
2.61 - context_thy
2.62 - applicable_in (p, p_) pt (Tactic.Apply_Method pres
2.63 - insert_assumptions
2.64 -
2.65 -
2.66 -
2.67 -
2.68 -
2.69 -
2.70 - generate1 _ (Tactic.Rewrite***
2.71 - insert_assumptions
2.72 -
2.73 -
2.74 -
2.75 -
2.76 -
2.77 -------------------------------------------------------------------------------------------------
2.78 -solve phase before LI
2.79 -------------------------------------------------------------------------------------------------
2.80 -autocalc
2.81 - all_modspec
2.82 - declare_constraints'
2.83 - complete_solve
2.84 - all_modspec
2.85 - declare_constraints'
2.86 -
2.87 -all_solve
2.88 - by_tactic (Tactic.Apply_Method'
2.89 - init_pstate
2.90 - declare_constraints'
2.91 - insert_assumptions
2.92 -
2.93 -nxt_specify_
2.94 - by_tactic (Tactic.Apply_Method'
2.95 - init_pstate
2.96 - declare_constraints'
2.97 - insert_assumptions
2.98 -------------------------------------------------------------------------------------------------
2.99 -LI
2.100 -------------------------------------------------------------------------------------------------
2.101 -solve ("Apply_Method" root-program
2.102 - init_pstate
2.103 - declare_constraints'
2.104 - insert_assumptions
2.105 - locate_input_tactic
2.106 - scan_to_tactic1
2.107 - scan_dn1 ..leaf sub-program
2.108 - associate
2.109 - declare_constraints'
2.110 - applicable_in .. Tactic.Apply_Method pres
2.111 - insert_assumptions
2.112 - ? generate1 (look in test with "from ... to..))
2.113 -
2.114 -find_next_tactic
2.115 - scan_to_tactic2
2.116 - scan_dn2 ..leaf
2.117 - stac2tac_
2.118 - declare_constraints'
2.119 - applicable_in (p, p_) pt (Tactic.Apply_Method pres
2.120 - insert_assumptions
2.121 - ? generate1 (look in test with "from ... to..))
2.122 -
2.123 -locate_input_formula uses find_next_tactic
2.124 - compare_step
2.125 - all_modspec
2.126 - declare_constraints'
2.127 - by_tactic (Tactic.Apply_Method'
2.128 - init_pstate
2.129 - declare_constraints'
2.130 - insert_assumptions
2.131 -------------------------------------------------------------------------------------------------
2.132 -specification phase
2.133 -------------------------------------------------------------------------------------------------
2.134 - loc_specify_
2.135 - specify (Tactic.Init_Proof'
2.136 - prep_ori
2.137 - declare_constraints
2.138 -
2.139 - CalcTree
2.140 - nxt_specify_init_calc
2.141 - prep_ori
2.142 - declare_constraints
2.143 -
2.144 - modifyCalcHead
2.145 - input_icalhd
2.146 - prep_ori
2.147 - declare_constraints
2.148 -
2.149 - refine
2.150 - refin'
2.151 - prep_ori
2.152 - declare_constraints
2.153 -------------------------------------------------------------------------------------------------
2.154 -unused ?!
2.155 -------------------------------------------------------------------------------------------------
2.156 - ??
2.157 - match_pbl
2.158 - prep_ori
2.159 - declare_constraints
2.160 - ??
2.161 - from_pblobj'
2.162 - init_pstate
2.163 - declare_constraints'
2.164 - insert_assumptions
2.165 - ??
2.166 - tac2tac_
2.167 - applicable_in (p, p_) pt (Tactic.Apply_Method pres
2.168 - insert_assumptions
2.169 -
2.170 -*)
2.171 -
2.172 structure ContextC(**) : CONTEXT_C(**) =
2.173 struct
2.174
3.1 --- a/src/Tools/isac/CalcElements/termC.sml Mon Dec 30 11:16:00 2019 +0100
3.2 +++ b/src/Tools/isac/CalcElements/termC.sml Wed Jan 15 11:47:38 2020 +0100
3.3 @@ -7,6 +7,10 @@
3.4 (* TERM_C extends Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *)
3.5 signature TERM_C =
3.6 sig
3.7 + datatype lrd = D | L | R
3.8 + type path
3.9 + val path2str: path -> string
3.10 +
3.11 val contains_Var: term -> bool
3.12 val dest_binop_typ: typ -> typ * typ * typ
3.13 val dest_equals: term -> term * term
3.14 @@ -97,6 +101,14 @@
3.15 struct
3.16 (**)
3.17
3.18 +datatype lrd = L (*t1 in "t1$t2"*)
3.19 + | R (*t2 in "t1$t2"*) | D; (*b in Abs(_,_,b*)
3.20 +type path = lrd list;
3.21 +fun ldr2str L = "L"
3.22 + | ldr2str R = "R"
3.23 + | ldr2str D = "D";
3.24 +fun path2str k = (strs2str' o (map ldr2str)) k;
3.25 +
3.26 fun isastr_of_int i = if i >= 0 then string_of_int i else "-" ^ string_of_int (abs i)
3.27
3.28 fun matches thy tm pa =
4.1 --- a/src/Tools/isac/Interpret/istate.sml Mon Dec 30 11:16:00 2019 +0100
4.2 +++ b/src/Tools/isac/Interpret/istate.sml Wed Jan 15 11:47:38 2020 +0100
4.3 @@ -26,14 +26,14 @@
4.4 val trans_ass: pstate -> pstate -> pstate
4.5 val trans_env_act: pstate -> pstate -> pstate
4.6
4.7 - val path_down: Celem.path -> pstate -> pstate
4.8 - val path_down_form: (Celem.path * term) -> pstate -> pstate
4.9 - val path_up': Celem.path -> Celem.path
4.10 + val path_down: TermC.path -> pstate -> pstate
4.11 + val path_down_form: (TermC.path * term) -> pstate -> pstate
4.12 + val path_up': TermC.path -> TermC.path
4.13 val path_up: pstate -> pstate
4.14 - val path_up_down: Celem.path -> pstate -> pstate
4.15 + val path_up_down: TermC.path -> pstate -> pstate
4.16
4.17 val set_form: term -> pstate -> pstate
4.18 - val set_path: Celem.path -> pstate -> pstate
4.19 + val set_path: TermC.path -> pstate -> pstate
4.20 val set_eval: Rule.rls -> pstate -> pstate
4.21 val set_act: term -> pstate -> pstate
4.22 val set_or: asap -> pstate -> pstate
4.23 @@ -80,7 +80,7 @@
4.24 fun topt2str NONE = "NONE"
4.25 | topt2str (SOME t) = "SOME" ^ Rule.term2str t;
4.26 fun scrstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *)
4.27 - "(" ^ Env.env2str env ^ ", " ^ Celem.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^
4.28 + "(" ^ Env.env2str env ^ ", " ^ TermC.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^
4.29 topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^
4.30 appy_2str finish ^ ", " ^ bool2str assoc ^ ")";
4.31
4.32 @@ -107,7 +107,7 @@
4.33 fun get_subst {env, form_arg, act_arg, ...} = (env, (form_arg, act_arg))
4.34
4.35 fun trans_scan_down2 {env, eval, act_arg, or, ...} =
4.36 - {env = env, path = [R], eval = eval, form_arg = NONE, act_arg = act_arg,
4.37 + {env = env, path = [TermC.R], eval = eval, form_arg = NONE, act_arg = act_arg,
4.38 or = or, finish = AppUndef_, assoc = false}
4.39 fun trans_scan_up2 {env, path, eval, form_arg, act_arg, or, ...} =
4.40 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
5.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Dec 30 11:16:00 2019 +0100
5.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Jan 15 11:47:38 2020 +0100
5.3 @@ -39,25 +39,27 @@
5.4 | Reject_Tac1 of Istate.pstate * Proof.context * Tactic.T
5.5 | Term_Val1 of term;
5.6 val assoc2str: expr_val1 -> string
5.7 +(* ---- for paper on Lucas-Interpretation ------------------------------------------- --------- *)
5.8 + val at_location: TermC.path -> term -> term
5.9 + val check_Seq_up: Istate.pstate -> term -> term
5.10 + datatype expr_val2 = Accept_Tac2 of Tactic.T * Istate.pstate * Proof.context
5.11 + | Reject_Tac2 | Term_Val2 of term
5.12 +
5.13 + val scan_dn2: Ctree.state * Proof.context -> Istate.pstate -> term -> expr_val2
5.14 + val scan_up2: term * (Ctree.state * Proof.context) -> Istate.pstate -> term -> expr_val2
5.15 + val go_scan_up2: term * (Ctree.state * Proof.context) -> Istate.pstate -> expr_val2
5.16 + val scan_to_tactic2: term * (Ctree.state * Proof.context) -> Istate.T -> expr_val2
5.17 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.18 - val go: Celem.path -> term -> term
5.19 - val go_up: Celem.path -> term -> term
5.20 + val go_up: TermC.path -> term -> term
5.21 val check_Let_up: Istate.pstate -> term -> term * term
5.22 - val check_Seq_up: Istate.pstate -> term -> term
5.23 val compare_step: Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
5.24
5.25 val scan_dn1: (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1
5.26 val scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
5.27 val go_scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> expr_val1;
5.28 val scan_to_tactic1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.T -> expr_val1
5.29 +
5.30 val interpret_tac1: Ctree.state * Proof.context * Tactic.T -> Istate.pstate -> term option * term -> expr_val1
5.31 -
5.32 - datatype expr_val2 = Accept_Tac2 of Tactic.T * Istate.pstate * Proof.context
5.33 - | Reject_Tac2 | Term_Val2 of term
5.34 - val scan_dn2: Ctree.state * Proof.context -> Istate.pstate -> term -> expr_val2
5.35 - val scan_up2: term * (Ctree.state * Proof.context) -> Istate.pstate -> term -> expr_val2
5.36 - val go_scan_up2: term * (Ctree.state * Proof.context) -> Istate.pstate -> expr_val2
5.37 - val scan_to_tactic2: term * (Ctree.state * Proof.context) -> Istate.T -> expr_val2
5.38 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.39 end
5.40
5.41 @@ -67,26 +69,26 @@
5.42 (**)
5.43 open Ctree
5.44 open Pos
5.45 -open Celem
5.46 +open TermC
5.47 open Istate
5.48
5.49 (*** auxiliary functions ***)
5.50
5.51 (*go to a location in a program and fetch the resective sub-term*)
5.52 -fun go [] t = t
5.53 - | go (D :: p) (Abs(_, _, body)) = go (p : Celem.path) body
5.54 - | go (L :: p) (t1 $ _) = go p t1
5.55 - | go (R :: p) (_ $ t2) = go p t2
5.56 - | go l _ = error ("go: no " ^ Celem.path2str l);
5.57 +fun at_location [] t = t
5.58 + | at_location (D :: p) (Abs(_, _, body)) = at_location (p : TermC.path) body
5.59 + | at_location (L :: p) (t1 $ _) = at_location p t1
5.60 + | at_location (R :: p) (_ $ t2) = at_location p t2
5.61 + | at_location l _ = error ("at_location: no " ^ TermC.path2str l);
5.62 fun go_up l t =
5.63 - if length l > 1 then go (drop_last l) t else raise ERROR ("go_up [] " ^ Rule.term2str t)
5.64 + if length l > 1 then at_location (drop_last l) t else raise ERROR ("go_up [] " ^ Rule.term2str t)
5.65
5.66 fun check_Let_up ({path, ...}: pstate) prog =
5.67 - case go (drop_last path) prog of
5.68 + case at_location (drop_last path) prog of
5.69 Const ("HOL.Let",_) $ _ $ (Abs (i, T, body)) => (TermC.mk_Free (i, T), body)
5.70 | t => raise ERROR ("scan_up1..\"HOL.Let $ _\" with: \"" ^ Rule.term2str t ^ "\"")
5.71 fun check_Seq_up ({path, ...}: pstate) prog =
5.72 - case go (drop_last path) prog of
5.73 + case at_location (drop_last path) prog of
5.74 Const ("Tactical.Chain",_) $ _ $ e2=> e2
5.75 | t => raise ERROR ("scan_up1..\"Tactical.Chain $ _\" with: \"" ^ Rule.term2str t ^ "\"")
5.76
5.77 @@ -207,7 +209,7 @@
5.78
5.79 fun go_scan_up1 (pcct as (prog, _)) (ist as {path, act_arg, ...}) =
5.80 if 1 < length path
5.81 - then scan_up1 pcct (ist |> path_up) (go (path_up' path) prog)
5.82 + then scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog)
5.83 else Term_Val1 act_arg
5.84 and scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
5.85 | scan_up1 pcct ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up1 pcct ist
6.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Mon Dec 30 11:16:00 2019 +0100
6.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Jan 15 11:47:38 2020 +0100
6.3 @@ -22,7 +22,7 @@
6.4 datatype ppobj =
6.5 PblObj of
6.6 {branch: branch,
6.7 - cell: Celem.lrd option,
6.8 + cell: TermC.lrd option,
6.9 loc: (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option,
6.10 ostate: ostate,
6.11 result: Selem.result,
6.12 @@ -36,7 +36,7 @@
6.13 env: (Istate_Def.T * Proof.context) option}
6.14 | PrfObj of
6.15 {branch: branch,
6.16 - cell: Celem.lrd option,
6.17 + cell: TermC.lrd option,
6.18 loc: (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option,
6.19 ostate: ostate,
6.20 result: Selem.result,
6.21 @@ -172,7 +172,7 @@
6.22 (* executed tactics (tac_s) with local environment etc.;
6.23 used for continuing eval script + for generate *)
6.24 type ets =
6.25 - (Celem.path *(* of tactic in scr, tactic (weakly) associated with tac_ *)
6.26 + (TermC.path *(* of tactic in scr, tactic (weakly) associated with tac_ *)
6.27 (Tactic.T * (* (for generate) *)
6.28 Env.T * (* with 'tactic=result' as rule, tactic ev. _not_ ready for 'parallel let' *)
6.29 Env.T * (* with results of (ready) tacs *)
6.30 @@ -182,7 +182,7 @@
6.31 list;
6.32
6.33 fun ets2s (l,(m,eno,env,iar,res,s)) =
6.34 - "\n(" ^ Celem.path2str l ^ ",(" ^ Tactic.string_of m ^
6.35 + "\n(" ^ TermC.path2str l ^ ",(" ^ Tactic.string_of m ^
6.36 ",\n ens= " ^ Env.subst2str eno ^
6.37 ",\n env= " ^ Env.subst2str env ^
6.38 ",\n iar= " ^ Rule.term2str iar ^
6.39 @@ -198,7 +198,7 @@
6.40
6.41 datatype ppobj = (* TODO: arrange according to signature *)
6.42 PrfObj of
6.43 - {cell : Celem.lrd option, (* where in form tac has been applied, FIXME.WN0607 rename field *)
6.44 + {cell : TermC.lrd option, (* where in form tac has been applied, FIXME.WN0607 rename field *)
6.45 form : term, (* where tac is applied to *)
6.46 tac : Tactic.input, (* also in istate *)
6.47 loc : (Istate_Def.T * (* script interpreter state *)
6.48 @@ -212,7 +212,7 @@
6.49 result: Selem.result, (* result and assumptions *)
6.50 ostate: ostate} (* Complete <=> result is OK *)
6.51 | PblObj of
6.52 - {cell : Celem.lrd option, (* unused: meaningful only for some _Prf_Obj *)
6.53 + {cell : TermC.lrd option, (* unused: meaningful only for some _Prf_Obj *)
6.54 fmz : Selem.fmz, (* from init:FIXME never use this spec;-drop *)
6.55 origin: (Model.ori list) *(* representation from fmz+pbt+met
6.56 for efficiently adding items in probl, meth *)
7.1 --- a/src/Tools/isac/MathEngBasic/istate-def.sml Mon Dec 30 11:16:00 2019 +0100
7.2 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml Wed Jan 15 11:47:38 2020 +0100
7.3 @@ -53,7 +53,7 @@
7.4
7.5 type pstate =
7.6 {env: Env.T, (* environment for variables in a program *)
7.7 - path: Celem.path, (* to the current location in a program *)
7.8 + path: TermC.path, (* to the current location in a program *)
7.9 eval: Rule.rls, (* rule-set for evaluating a Prog_Expr *)
7.10 form_arg: term option,(* argument of a curried function *)
7.11 act_arg: term, (* value for the curried argument *)
7.12 @@ -66,7 +66,7 @@
7.13 fun topt2str NONE = "NONE"
7.14 | topt2str (SOME t) = "SOME" ^ Rule.term2str t;
7.15 fun scrstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *)
7.16 - "(" ^ Env.env2str env ^ ", " ^ Celem.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^
7.17 + "(" ^ Env.env2str env ^ ", " ^ TermC.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^
7.18 topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^
7.19 appy_2str finish ^ ", " ^ bool2str assoc ^ ")";
7.20
8.1 --- a/src/Tools/isac/MathEngBasic/position.sml Mon Dec 30 11:16:00 2019 +0100
8.2 +++ b/src/Tools/isac/MathEngBasic/position.sml Wed Jan 15 11:47:38 2020 +0100
8.3 @@ -16,7 +16,7 @@
8.4 val e_pos': pos'
8.5
8.6 val at_first_tactic: pos' -> bool
8.7 -(*val at_first_tactic: term -> Celem.path -> pos' -> bool*)
8.8 +(*val at_first_tactic: term -> TermC.path -> pos' -> bool*)
8.9 val lev_of: pos' -> int
8.10 val lev_dn: pos -> pos (* duplicate in ctree-basic.sml *)
8.11 val lev_dn_: pos' -> pos'
8.12 @@ -87,7 +87,7 @@
8.13 fun at_first_tactic prog path (pos as (p, p_)) =
8.14 (if not (path = []) andalso (last_elem p = 0 andalso p_ = Res)
8.15 then raise ERROR ("at_start_detail: not (path = []) andalso at_start_detail in \n\""
8.16 - ^ Rule.term2str prog ^ "\"\n at \"" ^ Celem.path2str path ^ "\" for \"" ^ pos'2str pos ^ "\"")
8.17 + ^ Rule.term2str prog ^ "\"\n at \"" ^ TermC.path2str path ^ "\" for \"" ^ pos'2str pos ^ "\"")
8.18 else ();
8.19 last_elem p = 0 andalso p_ = Res)
8.20 *)
9.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Mon Dec 30 11:16:00 2019 +0100
9.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Jan 15 11:47:38 2020 +0100
9.3 @@ -3,7 +3,7 @@
9.4 (c) due to copyright terms
9.5 *)
9.6
9.7 -theory Auto_Prog imports Program Prog_Tac Tactical begin
9.8 +theory Auto_Prog imports Prog_Tac Tactical begin
9.9
9.10 text \<open>Abstract:
9.11 The tactics Rewrite_Set* create ONE step in a calculation by application of usually
10.1 --- a/src/Tools/isac/ProgLang/Tactical.thy Mon Dec 30 11:16:00 2019 +0100
10.2 +++ b/src/Tools/isac/ProgLang/Tactical.thy Wed Jan 15 11:47:38 2020 +0100
10.3 @@ -12,7 +12,7 @@
10.4 \<close>
10.5 subsection \<open>Consts for tacticals\<close>
10.6 consts
10.7 - Chain :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "#>" 10) (*@ used*)
10.8 + Chain :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "#>" 10)
10.9 Try :: "['a => 'a, 'a] => 'a"
10.10 Repeat :: "['a => 'a, 'a] => 'a"
10.11 Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)
11.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Mon Dec 30 11:16:00 2019 +0100
11.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Wed Jan 15 11:47:38 2020 +0100
11.3 @@ -12,7 +12,7 @@
11.4 val eval_true: theory -> term list -> Rule.rls -> bool
11.5 val eval_true_: theory -> Rule.rls -> term -> bool
11.6 val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
11.7 - -> Rule.rls -> bool -> Celem.lrd list -> term -> term -> term * term list * Celem.lrd list * bool
11.8 + -> Rule.rls -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
11.9 val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule.rls -> bool -> thm ->
11.10 term -> (term * term list) option
11.11 val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule.rls -> bool
11.12 @@ -49,7 +49,7 @@
11.13
11.14 fun rewrite__ thy i bdv tless rls put_asm thm ct =
11.15 let
11.16 - val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: Celem.lrd list)
11.17 + val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
11.18 (((TermC.inst_bdv bdv) o Calc.norm o #prop o Thm.rep_thm) thm) ct
11.19 in if rew then SOME (t', distinct asms) else NONE end
11.20 (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
11.21 @@ -95,14 +95,14 @@
11.22 | Var(n,T) => (Var(n,T),[],lrd,false)
11.23 | Bound i => (Bound i,[],lrd,false)
11.24 | Abs(s,T,body) =>
11.25 - let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [Celem.D]) r body
11.26 + let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.D]) r body
11.27 in (Abs(s, T, t'), asms, [], rew) end
11.28 | t1 $ t2 =>
11.29 - let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [Celem.R]) r t2
11.30 + let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
11.31 in
11.32 if rew2 then (t1 $ t2', asm2, lrd, true)
11.33 else
11.34 - let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [Celem.L]) r t1
11.35 + let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
11.36 in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
11.37 end)
11.38 and eval__true thy i asms bdv rls = (* simplify asumptions until one evaluates to false *)
12.1 --- a/src/Tools/isac/ROOT Mon Dec 30 11:16:00 2019 +0100
12.2 +++ b/src/Tools/isac/ROOT Wed Jan 15 11:47:38 2020 +0100
12.3 @@ -2,8 +2,6 @@
12.4 Author: Walther Neuper, TU Graz, 130715
12.5 (c) due to copyright terms
12.6
12.7 -$ export ISABELLE_VERSION=2018 # for libisabelle
12.8 -
12.9 see ~~/etc/settings
12.10 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
12.11 before out-outcommenting (*, browser_info = true*) below and ...
12.12 @@ -26,3 +24,12 @@
12.13 options [document = false (*, browser_info = true*)]
12.14 theories
12.15 Build_Isac
12.16 +
12.17 +(* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
12.18 +session Lucas_Interpreter = HOL +
12.19 + description \<open>
12.20 + Session Isac restricted to code required for Lucas_Interpreter.
12.21 + \<close>
12.22 + options [document = false (*, browser_info = true*)]
12.23 + theories
12.24 + "Interpret/Interpret"
13.1 --- a/src/Tools/isac/TODO.thy Mon Dec 30 11:16:00 2019 +0100
13.2 +++ b/src/Tools/isac/TODO.thy Wed Jan 15 11:47:38 2020 +0100
13.3 @@ -16,7 +16,7 @@
13.4 \item xxx
13.5 \item ??????????? WHY CAN LucinNEW.by_tactic NOT BE REPLACED BY Step_Solve.by_tactic ???????????
13.6 \item xxx
13.7 - \item xxx
13.8 + \item ? datatype Tactic.input: MathEngBasic/tactic-def.sml + tactic.sml ?!?
13.9 \item xxx
13.10 \item rm test/..--- check Scripts ---
13.11 \item xxx
14.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Dec 30 11:16:00 2019 +0100
14.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Jan 15 11:47:38 2020 +0100
14.3 @@ -298,19 +298,19 @@
14.4 = ((prog, cctt), ist);
14.5 (*if*) 1 < length path (*then*);
14.6
14.7 - scan_up1 yyy (ist |> path_up) (go (path_up' path) prog);
14.8 + scan_up1 yyy (ist |> path_up) (at_location (path_up' path) prog);
14.9 "~~~~~ fun scan_up1 , args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _))
14.10 - = (yyy, (ist |> path_up), (go (path_up' path) prog));
14.11 + = (yyy, (ist |> path_up), (at_location (path_up' path) prog));
14.12
14.13 go_scan_up1 yyy ist;
14.14 "~~~~~ and go_scan_up1 , args:"; val ((yyy as (prog, _)), (ist as {path, ...}))
14.15 = (yyy, ist);
14.16 (*if*) 1 < length path (*then*);
14.17
14.18 - scan_up1 yyy (ist |> path_up) (go (path_up' path) prog);
14.19 + scan_up1 yyy (ist |> path_up) (at_location (path_up' path) prog);
14.20 "~~~~~ fun scan_up1 , args:"; val ((yyy as (prog, xxx as (cstate, _, _))), ist,
14.21 (Const ("Tactical.Chain"(*3*), _) $ _ ))
14.22 - = (yyy, (ist |> path_up), (go (path_up' path) prog));
14.23 + = (yyy, (ist |> path_up), (at_location (path_up' path) prog));
14.24 val e2 = check_Seq_up ist prog
14.25 ;
14.26 (*case*) scan_dn1 xxx (ist |> path_up_down [R] |> set_or ORundef) e (*of*);
15.1 --- a/test/Tools/isac/Interpret/script.sml Mon Dec 30 11:16:00 2019 +0100
15.2 +++ b/test/Tools/isac/Interpret/script.sml Wed Jan 15 11:47:38 2020 +0100
15.3 @@ -241,17 +241,17 @@
15.4 (*
15.5 > val t = (Thm.term_of o the o (parse thy)) "a+b";
15.6 val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term
15.7 -> val plus_a = go [L] t;
15.8 -> val b = go [R] t;
15.9 -> val plus = go [L,L] t;
15.10 -> val a = go [L,R] t;
15.11 +> val plus_a = at_location [L] t;
15.12 +> val b = at_location [R] t;
15.13 +> val plus = at_location [L,L] t;
15.14 +> val a = at_location [L,R] t;
15.15
15.16 > val t = (Thm.term_of o the o (parse thy)) "a+b+c";
15.17 val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term
15.18 -> val pl_pl_a_b = go [L] t;
15.19 -> val c = go [R] t;
15.20 -> val a = go [L,R,L,R] t;
15.21 -> val b = go [L,R,R] t;
15.22 +> val pl_pl_a_b = at_location [L] t;
15.23 +> val c = at_location [R] t;
15.24 +> val a = at_location [L,R,L,R] t;
15.25 +> val b = at_location [L,R,R] t;
15.26 *)
15.27
15.28 "----------- fun formal_args -------------------------------------";
16.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Dec 30 11:16:00 2019 +0100
16.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed Jan 15 11:47:38 2020 +0100
16.3 @@ -218,14 +218,14 @@
16.4 ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
16.5 1 < length l (*true*);
16.6 val up = drop_last l;
16.7 - term2str (go up sc);
16.8 - (go up sc);
16.9 -(*WAS val Term_Val1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (go up sc)
16.10 + term2str (at_location up sc);
16.11 + (at_location up sc);
16.12 +(*WAS val Term_Val1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (at_location up sc)
16.13 ... ???? ... is correct*)
16.14 "~~~~~ fun scan_up1, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss),
16.15 - (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (go up sc));
16.16 + (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (at_location up sc));
16.17 val l = drop_last l; (*comes from e, goes to Abs*)
16.18 - val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
16.19 + val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = at_location l sc;
16.20 val i = mk_Free (i, T);
16.21 val E = Env.update E (i, v);
16.22 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
17.1 --- a/test/Tools/isac/Knowledge/rateq.sml Mon Dec 30 11:16:00 2019 +0100
17.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Jan 15 11:47:38 2020 +0100
17.3 @@ -63,7 +63,7 @@
17.4 case nxt of ("Rewrite_Set", Rewrite_Set "RatEq_eliminate") => () | _ => ((*not checked before*));
17.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
17.6 (*
17.7 -WN120317.TODO dropped rateq: here "x ~= 0 should go to ctxt, but it does not:
17.8 +WN120317.TODO dropped rateq: here "x ~= 0 should at_location to ctxt, but it does not:
17.9 --- repair NO asms from rls RatEq_eliminate --- shows why.
17.10 so it needs more effort to find out, how Check_elementwise worked in 2002, see below.
17.11 *)
17.12 @@ -109,12 +109,12 @@
17.13 (thy, ptp, sc, E, l, Skip_, a, v);
17.14 1 < length l; (*true*)
17.15 val up = drop_last l;
17.16 -go up sc; (* = Const ("HOL.Let", *)
17.17 +at_location up sc; (* = Const ("HOL.Let", *)
17.18 "~~~~~ fun scan_up2, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay,
17.19 - (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
17.20 + (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (at_location up sc), a, v);
17.21 ay = Napp_; (*false*)
17.22 val up = drop_last l;
17.23 -val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; (*Const ("Prog_Tac.SubProblem",..*)
17.24 +val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = at_location up sc; (*Const ("Prog_Tac.SubProblem",..*)
17.25 val i = mk_Free (i, T);
17.26 val E = Env.update E (i, v);
17.27 "~~~~~ fun scan_dn2, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) =
17.28 @@ -297,24 +297,24 @@
17.29 (thy, ptp, sc, E, l, Skip_, a, v);
17.30 1 < length l; (* = true*)
17.31 val up = drop_last l;
17.32 -(*val (t as Abs (_,_,_)) = *)(go up sc);
17.33 +(*val (t as Abs (_,_,_)) = *)(at_location up sc);
17.34 "~~~~~ fun scan_up2, args:"; val (thy, ptp, scr, E, l, ay, (t as Abs (_,_,_)), a, v) =
17.35 - (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
17.36 + (thy, ptp, (Prog sc), E, up, ay, (at_location up sc), a, v);
17.37 term2str t = "%L_La. Check_elementwise L_L {v_v. Assumptions}";
17.38 "~~~~~ and go_scan_up2, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
17.39 (thy, ptp, scr, E, l, ay, a, v);
17.40 1 < length l; (* = true*)
17.41 val up = drop_last l;
17.42 -(*val (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) = *)(go up sc);
17.43 +(*val (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) = *)(at_location up sc);
17.44 "~~~~~ fun scan_up2, args:"; val (thy, ptp, scr, E, l, ay,
17.45 - (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) = (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
17.46 + (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) = (thy, ptp, (Prog sc), E, up, ay, (at_location up sc), a, v);
17.47
17.48 term2str t = "let L_La =\n SubProblem (RatEqX, [univariate, equation], [no_met])\n [BOOL e_e, REAL v_v]\nin Check_elementwise L_L {v_v. Assumptions}";
17.49
17.50 (* comment from BEFORE Isabelle2002 --> 2011:
17.51 -scan_up2 thy ptp (Prog sc) E up ay (go up sc) a v;
17.52 +scan_up2 thy ptp (Prog sc) E up ay (at_location up sc) a v;
17.53 go_scan_up2 thy ptp scr E l ay a v;
17.54 -scan_up2 thy ptp (Prog sc) E up ay (go up sc) a v;
17.55 +scan_up2 thy ptp (Prog sc) E up ay (at_location up sc) a v;
17.56 go_scan_up2 thy ptp sc E l Skip_ a v;
17.57 find_next_tactic sc (pt,pos) is (*is as (ist, ctxt) ---> ist ctxt*);
17.58 Step_Solve.do_next (pt,ip);
18.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Mon Dec 30 11:16:00 2019 +0100
18.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Jan 15 11:47:38 2020 +0100
18.3 @@ -53,36 +53,36 @@
18.4 = ((prog, cctt), ist);
18.5 (*if*) 1 < length path (*true*);
18.6
18.7 - scan_up1 yyy (ist |> path_up) (go (path_up' path) prog);
18.8 + scan_up1 yyy (ist |> path_up) (at_location (path_up' path) prog);
18.9 "~~~~~ fun scan_up1, args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _))
18.10 - = (yyy, (ist |> path_up), (go (path_up' path) prog));
18.11 + = (yyy, (ist |> path_up), (at_location (path_up' path) prog));
18.12
18.13 go_scan_up1 yyy ist;
18.14 "~~~~~ and go_scan_up1, args:"; val ((yyy as (prog, _)), (ist as {path, ...}))
18.15 = (yyy, ist);
18.16 (*if*) 1 < length path (*true*);
18.17
18.18 - scan_up1 yyy (ist |> path_up) (go (path_up' path) prog);
18.19 + scan_up1 yyy (ist |> path_up) (at_location (path_up' path) prog);
18.20 "~~~~~ fun scan_up1 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
18.21 - = (yyy, (ist |> path_up), (go (path_up' path) prog));
18.22 + = (yyy, (ist |> path_up), (at_location (path_up' path) prog));
18.23
18.24 go_scan_up1 yyy ist (*2*: comes from e2*);
18.25 "~~~~~ and go_scan_up1, args:"; val ((yyy as (prog, _)), (ist as {path, ...}))
18.26 = (yyy, ist);
18.27 (*if*) 1 < length path (*true*);
18.28
18.29 - scan_up1 yyy (ist |> path_up) (go (path_up' path) prog);
18.30 + scan_up1 yyy (ist |> path_up) (at_location (path_up' path) prog);
18.31 "~~~~~ fun scan_up1 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _))
18.32 - = (yyy, (ist |> path_up), (go (path_up' path) prog));
18.33 + = (yyy, (ist |> path_up), (at_location (path_up' path) prog));
18.34
18.35 go_scan_up1 yyy ist (*all has been done in (*2*) below*);
18.36 "~~~~~ and go_scan_up1, args:"; val ((yyy as (prog, _)), (ist as {path, ...}))
18.37 = (yyy, ist);
18.38 (*if*) 1 < length path (*true*);
18.39
18.40 - scan_up1 yyy (ist |> path_up) (go (path_up' path) prog);
18.41 + scan_up1 yyy (ist |> path_up) (at_location (path_up' path) prog);
18.42 "~~~~~ fun scan_up1 , args:"; val ((yyy as (prog, xxx as (cstate, _, _))), ist, (Const ("HOL.Let"(*1*), _) $ _))
18.43 - = ( yyy, (ist |> path_up), (go (path_up' path) prog));
18.44 + = ( yyy, (ist |> path_up), (at_location (path_up' path) prog));
18.45 val (i, body) = check_Let_up ist prog
18.46 ;
18.47 (*case*) scan_dn1 xxx (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef) body (*of*);