1.1 --- a/src/Tools/isac/Frontend/interface.sml Wed Dec 21 11:27:22 2016 +0100
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Thu Dec 22 10:25:49 2016 +0100
1.3 @@ -13,47 +13,47 @@
1.4 sig
1.5 val appendFormula : calcID -> cterm' -> XML.tree (*unit future*)
1.6 val autoCalculate : calcID -> Solve.auto -> XML.tree (*unit future*)
1.7 - val applyTactic : calcID -> pos' -> tac -> XML.tree
1.8 - val CalcTree : fmz list -> XML.tree
1.9 - val checkContext : calcID -> pos' -> guh -> XML.tree
1.10 + val applyTactic : calcID -> Ctree.pos' -> Ctree.tac -> XML.tree
1.11 + val CalcTree : Ctree.fmz list -> XML.tree
1.12 + val checkContext : calcID -> Ctree.pos' -> guh -> XML.tree
1.13 val DEconstrCalcTree : calcID -> XML.tree
1.14 - val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree
1.15 + val fetchApplicableTactics : calcID -> int -> Ctree.pos' -> XML.tree
1.16 val fetchProposedTactic : calcID -> XML.tree
1.17 val findFillpatterns : calcID -> errpatID -> XML.tree
1.18 - val getAccumulatedAsms : calcID -> pos' -> XML.tree
1.19 + val getAccumulatedAsms : calcID -> Ctree.pos' -> XML.tree
1.20 val getActiveFormula : calcID -> XML.tree
1.21 - val getAssumptions : calcID -> pos' -> XML.tree
1.22 - val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree
1.23 - val getTactic : calcID -> pos' -> XML.tree
1.24 - val initContext : calcID -> ketype -> pos' -> XML.tree
1.25 + val getAssumptions : calcID -> Ctree.pos' -> XML.tree
1.26 + val getFormulaeFromTo : calcID -> Ctree.pos' -> Ctree.pos' -> int -> bool -> XML.tree
1.27 + val getTactic : calcID -> Ctree.pos' -> XML.tree
1.28 + val initContext : calcID -> ketype -> Ctree.pos' -> XML.tree
1.29 val inputFillFormula: calcID -> string -> XML.tree
1.30 - val interSteps : calcID -> pos' -> XML.tree
1.31 + val interSteps : calcID -> Ctree.pos' -> XML.tree
1.32 val Iterator : calcID -> XML.tree
1.33 val IteratorTEST : calcID -> iterID
1.34 val modelProblem : calcID -> XML.tree
1.35 val modifyCalcHead : calcID -> Inform.icalhd -> XML.tree
1.36 val moveActiveCalcHead : calcID -> XML.tree
1.37 val moveActiveDown : calcID -> XML.tree
1.38 - val moveActiveFormula : calcID -> pos' -> XML.tree
1.39 + val moveActiveFormula : calcID -> Ctree.pos' -> XML.tree
1.40 val moveActiveLevelDown : calcID -> XML.tree
1.41 val moveActiveLevelUp : calcID -> XML.tree
1.42 val moveActiveRoot : calcID -> XML.tree
1.43 val moveActiveRootTEST : calcID -> XML.tree
1.44 val moveActiveUp : calcID -> XML.tree
1.45 - val moveCalcHead : calcID -> pos' -> XML.tree
1.46 - val moveDown : calcID -> pos' -> XML.tree
1.47 - val moveLevelDown : calcID -> pos' -> XML.tree
1.48 - val moveLevelUp : calcID -> pos' -> XML.tree
1.49 + val moveCalcHead : calcID -> Ctree.pos' -> XML.tree
1.50 + val moveDown : calcID -> Ctree.pos' -> XML.tree
1.51 + val moveLevelDown : calcID -> Ctree.pos' -> XML.tree
1.52 + val moveLevelUp : calcID -> Ctree.pos' -> XML.tree
1.53 val moveRoot : calcID -> XML.tree
1.54 - val moveUp : calcID -> pos' -> XML.tree
1.55 - val refFormula : calcID -> pos' -> XML.tree
1.56 - val refineProblem : calcID -> pos' -> guh -> XML.tree
1.57 + val moveUp : calcID -> Ctree.pos' -> XML.tree
1.58 + val refFormula : calcID -> Ctree.pos' -> XML.tree
1.59 + val refineProblem : calcID -> Ctree.pos' -> guh -> XML.tree
1.60 val replaceFormula : calcID -> cterm' -> XML.tree
1.61 val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree
1.62 val resetCalcHead : calcID -> XML.tree
1.63 - val setContext : calcID -> pos' -> guh -> XML.tree
1.64 + val setContext : calcID -> Ctree.pos' -> guh -> XML.tree
1.65 val setMethod : calcID -> metID -> XML.tree
1.66 - val setNextTactic : calcID -> tac -> XML.tree
1.67 + val setNextTactic : calcID -> Ctree.tac -> XML.tree
1.68 val setProblem : calcID -> pblID -> XML.tree
1.69 val setTheory : calcID -> thyID -> XML.tree
1.70 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.71 @@ -64,6 +64,7 @@
1.72 (**)
1.73 structure Kernel(**): KERNEL(**) =
1.74 struct
1.75 +open Ctree
1.76 (**)
1.77 (* encode "Isabelle"-strings as seen by the user to the
1.78 format accepted by Isabelle.
2.1 --- a/src/Tools/isac/Frontend/states.sml Wed Dec 21 11:27:22 2016 +0100
2.2 +++ b/src/Tools/isac/Frontend/states.sml Thu Dec 22 10:25:49 2016 +0100
2.3 @@ -143,7 +143,7 @@
2.4 (calcID * (* the id unique for a calculation *)
2.5 (Chead.calcstate * (* the interpreter state *)
2.6 (iterID * (* 1 sets the 'active formula': a calc. can have several visitors*)
2.7 - pos' (* for iterator of a user *)
2.8 + Ctree.pos' (* for iterator of a user *)
2.9 (* TODO iterID * pos' should go to java-frontend *)
2.10 ) list)) list);
2.11
2.12 @@ -184,7 +184,7 @@
2.13 *)
2.14 (* add users to a calcstate *)
2.15 fun get_iterID (cI:calcID)
2.16 - (p:(calcID * (Chead.calcstate * (iterID * pos') list)) list) =
2.17 + (p:(calcID * (Chead.calcstate * (iterID * Ctree.pos') list)) list) =
2.18 case assoc (p, cI) of
2.19 NONE => error ("get_iterID: no iterID " ^ (string_of_int cI))
2.20 | SOME (_, us) => (new_key us 1):iterID;
2.21 @@ -310,7 +310,7 @@
2.22 fun upd_ipos (uI:iterID) (pI:calcID) (ip:pos') =
2.23 let val (_, calc) = get_state uI pI
2.24 in states:= overwrite2 ((!states), ((uI, pI), (ip, calc))) end;*)
2.25 -fun upd_ipos (cI:calcID) (uI:iterID) (ip:pos') = Synchronized.change states
2.26 +fun upd_ipos (cI:calcID) (uI:iterID) (ip: Ctree.pos') = Synchronized.change states
2.27 (fn s => case assoc (s, cI) of
2.28 NONE =>
2.29 error ("upd_ipos: calctree " ^ (string_of_int cI) ^ " not existent")
2.30 @@ -350,7 +350,7 @@
2.31 | SOME (cs, us) =>
2.32 let
2.33 val new_uI = new_key us 1
2.34 - in (new_uI:iterID, overwrite2 (s, ((cI, new_uI), e_pos'))) end);
2.35 + in (new_uI:iterID, overwrite2 (s, ((cI, new_uI), Ctree.e_pos'))) end);
2.36
2.37 (*///10.10.
2.38 fun del_calc (uI:iterID) (pI:calcID) =
3.1 --- a/src/Tools/isac/Interpret/appl.sml Wed Dec 21 11:27:22 2016 +0100
3.2 +++ b/src/Tools/isac/Interpret/appl.sml Thu Dec 22 10:25:49 2016 +0100
3.3 @@ -7,7 +7,7 @@
3.4
3.5 structure Applicable = (* intermediately to avoid too many "Ctree." *)
3.6 struct
3.7 -(*open Ctree*)
3.8 +open Ctree
3.9
3.10 val e_cterm' = empty_cterm';
3.11
4.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed Dec 21 11:27:22 2016 +0100
4.2 +++ b/src/Tools/isac/Interpret/calchead.sml Thu Dec 22 10:25:49 2016 +0100
4.3 @@ -7,31 +7,31 @@
4.4 sig
4.5 type calcstate
4.6 type calcstate'
4.7 - datatype appl = Appl of tac_ | Notappl of string
4.8 - val nxt_specify_init_calc : fmz -> calcstate
4.9 - val specify : tac_ -> pos' -> cid -> ptree ->
4.10 - (posel list * pos_) * ((posel list * pos_) * istate) * Generate.mout * tac * safe * ptree
4.11 - val nxt_specif : tac -> ptree * (pos * pos_) -> calcstate'
4.12 - val nxt_spec : pos_ -> bool -> ori list -> spec -> itm list * itm list ->
4.13 - (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> pos_ * tac
4.14 + datatype appl = Appl of Ctree.tac_ | Notappl of string
4.15 + val nxt_specify_init_calc : Ctree.fmz -> calcstate
4.16 + val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ptree ->
4.17 + Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ptree
4.18 + val nxt_specif : Ctree.tac -> Ctree.ptree * Ctree.pos' -> calcstate'
4.19 + val nxt_spec : Ctree.pos_ -> bool -> ori list -> spec -> itm list * itm list ->
4.20 + (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Ctree.tac
4.21
4.22 - val reset_calchead : ptree * pos' -> ptree * pos'
4.23 - val get_ocalhd : ptree * pos' -> ocalhd
4.24 + val reset_calchead : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
4.25 + val get_ocalhd : Ctree.ptree * Ctree.pos' -> Ctree.ocalhd
4.26 val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool
4.27 - val all_modspec : ptree * pos' -> ptree * pos'
4.28 + val all_modspec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
4.29
4.30 val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list
4.31 val insert_ppc' : itm -> itm list -> itm list
4.32
4.33 - val complete_mod : ptree * pos' -> ptree * pos'
4.34 - val is_complete_mod : ptree * pos' -> bool
4.35 - val complete_spec : ptree * pos' -> ptree * pos'
4.36 - val is_complete_spec : ptree * pos' -> bool
4.37 + val complete_mod : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
4.38 + val is_complete_mod : Ctree.ptree * Ctree.pos' -> bool
4.39 + val complete_spec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
4.40 + val is_complete_spec : Ctree.ptree * Ctree.pos' -> bool
4.41 val some_spec : spec -> spec -> spec
4.42 (* these could go to Ctree ..*)
4.43 - val show_pt : ptree -> unit
4.44 - val pt_extract : ptree * (posel list * pos_) -> ptform * tac option * term list
4.45 - val get_interval : int list * pos_ -> pos' -> int -> ptree -> (pos' * term) list
4.46 + val show_pt : Ctree.ptree -> unit
4.47 + val pt_extract : Ctree.ptree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list
4.48 + val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ptree -> (Ctree.pos' * term) list
4.49
4.50 val match_ags : theory -> pat list -> term list -> ori list
4.51 val match_ags_msg : pblID -> term -> term list -> unit
4.52 @@ -56,7 +56,7 @@
4.53
4.54 structure Chead(**): CALC_HEAD(**) =
4.55 struct
4.56 -
4.57 +open Ctree
4.58 (* datatypes *)
4.59
4.60 (* the state wich is stored after each step of calculation; it contains
5.1 --- a/src/Tools/isac/Interpret/generate.sml Wed Dec 21 11:27:22 2016 +0100
5.2 +++ b/src/Tools/isac/Interpret/generate.sml Thu Dec 22 10:25:49 2016 +0100
5.3 @@ -1,9 +1,12 @@
5.4 -(* use"ME/generate.sml";
5.5 - use"generate.sml";
5.6 - *)
5.7 +(* Title: generate specific entries into Ctree
5.8 + Author: Walther Neuper
5.9 + (c) due to copyright terms
5.10 +*)
5.11 +
5.12 signature GENERATE_CALC_TREE =
5.13 -sig (*vvv request into signature is incremental with *.sml *)
5.14 - (* for calchead.sml -------------------------------------------------------------- vvv *)
5.15 +sig
5.16 + (* vvv request into signature is incremental with *.sml *)
5.17 + (* for calchead.sml --------------------------------------------------------------- vvv *)
5.18 type taci
5.19 val e_taci : taci
5.20 datatype pblmet = Method of metID | Problem of pblID | Upblmet
5.21 @@ -13,18 +16,18 @@
5.22 | FormKF of cterm'
5.23 | PpcKF of pblmet * item ppc
5.24 | RefinedKF of pblID * (itm list * (bool * term) list)
5.25 - val generate1 : theory -> tac_ -> istate * Proof.context ->
5.26 - pos' -> ptree -> pos' * pos' list * mout * ptree (* for calchead.sml ^^^ *)
5.27 - val init_istate : tac -> term -> istate (* for solve.sml *)
5.28 + val generate1 : theory -> Ctree.tac_ -> Ctree.istate * Proof.context ->
5.29 + Ctree.pos' -> Ctree.ptree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ptree (* for calchead.sml------------- ^^^ *)
5.30 + val init_istate : Ctree.tac -> term -> Ctree.istate (* for solve.sml *)
5.31 val init_pbl : (string * (term * 'a)) list -> itm list
5.32 val init_pbl' : (string * (term * term)) list -> itm list
5.33 - val embed_deriv : taci list -> ptree * pos' -> pos' list * (ptree * pos') (* for inform.sml *)
5.34 + val embed_deriv : taci list -> Ctree.ptree * Ctree.pos' -> Ctree.pos' list * (Ctree.ptree * Ctree.pos') (* for inform.sml *)
5.35 val generate_hard : (* for solve.sml *)
5.36 - theory -> tac_ -> pos' -> ptree -> pos' * pos' list * mout * ptree
5.37 - val generate : (tac * tac_ * (pos' * (istate * Proof.context))) list ->
5.38 - ptree * pos' list * pos' -> ptree * pos' list * pos' (* for mathengine.sml *)
5.39 - val generate_inconsistent_rew : subs option * thm'' -> term -> istate * Proof.context ->
5.40 - pos' -> ptree -> ptree * pos' (* for interface.sml *)
5.41 + theory -> Ctree.tac_ -> Ctree.pos' -> Ctree.ptree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ptree
5.42 + val generate : (Ctree.tac * Ctree.tac_ * (Ctree.pos' * (Ctree.istate * Proof.context))) list ->
5.43 + Ctree.ptree * Ctree.pos' list * Ctree.pos' -> Ctree.ptree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
5.44 + val generate_inconsistent_rew : Ctree.subs option * thm'' -> term -> Ctree.istate * Proof.context ->
5.45 + Ctree.pos' -> Ctree.ptree -> Ctree.ptree * Ctree.pos' (* for interface.sml *)
5.46 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.47 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.48 end
5.49 @@ -33,6 +36,7 @@
5.50 structure Generate(**): GENERATE_CALC_TREE(**) =
5.51 (**)
5.52 struct
5.53 +open Ctree
5.54 (* initialize istate for Detail_Set *)
5.55 fun init_istate (Rewrite_Set rls) t =
5.56 (case assoc_rls rls of
6.1 --- a/src/Tools/isac/Interpret/inform.sml Wed Dec 21 11:27:22 2016 +0100
6.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu Dec 22 10:25:49 2016 +0100
6.3 @@ -8,18 +8,18 @@
6.4 sig
6.5 datatype iitem = Find of cterm' list | Given of cterm' list | Relate of cterm' list
6.6 type imodel = iitem list
6.7 - type icalhd = pos' * cterm' * imodel * pos_ * spec
6.8 - val fetchErrorpatterns : tac -> errpatID list
6.9 - val input_icalhd : ptree -> icalhd -> ptree * ocalhd
6.10 + type icalhd = Ctree.pos' * cterm' * imodel * Ctree.pos_ * spec
6.11 + val fetchErrorpatterns : Ctree.tac -> errpatID list
6.12 + val input_icalhd : Ctree.ptree -> icalhd -> Ctree.ptree * Ctree.ocalhd
6.13 val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
6.14 - val find_fillpatterns : ptree * pos' -> errpatID -> (fillpatID * term * thm * subs option) list
6.15 - val is_exactly_equal : ptree * (pos * pos_) -> string -> string * tac
6.16 + val find_fillpatterns : Ctree.ptree * Ctree.pos' -> errpatID -> (fillpatID * term * thm * Ctree.subs option) list
6.17 + val is_exactly_equal : Ctree.ptree * Ctree.pos' -> string -> string * Ctree.tac
6.18
6.19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.20 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
6.21 - val cas_input : term -> (ptree * ocalhd) option
6.22 + val cas_input : term -> (Ctree.ptree * Ctree.ocalhd) option
6.23 val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
6.24 - val compare_step : Generate.taci list * pos' list * (ptree * pos') -> term -> string * Chead.calcstate'
6.25 + val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos') -> term -> string * Chead.calcstate'
6.26 val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option
6.27 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
6.28 rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list
6.29 @@ -50,14 +50,14 @@
6.30
6.31 (*calc-head as input*)
6.32 type icalhd =
6.33 - pos' * (*the position of the calc-head in the calc-tree*)
6.34 + Ctree.pos' * (*the position of the calc-head in the calc-tree*)
6.35 cterm' * (*the headline*)
6.36 imodel * (*the model (without Find) of the calc-head*)
6.37 - pos_ * (*model belongs to Pbl or Met*)
6.38 + Ctree.pos_ * (*model belongs to Pbl or Met*)
6.39 spec; (*specification: domID, pblID, metID*)
6.40 -val e_icalhd = (e_pos', "", [Given [""]], Pbl, e_spec) : icalhd
6.41 +val e_icalhd = (Ctree.e_pos', "", [Given [""]], Ctree.Pbl, e_spec) : icalhd
6.42
6.43 -fun is_casinput (hdf : cterm') ((fmz_, spec) : fmz) =
6.44 +fun is_casinput (hdf : cterm') ((fmz_, spec) : Ctree.fmz) =
6.45 hdf <> "" andalso fmz_ = [] andalso spec = e_spec
6.46
6.47 (*.handle an input as into an algebra system.*)
6.48 @@ -91,7 +91,7 @@
6.49 val its = Specify.add_id its_
6.50 val mits = map flattup2 its
6.51 val pre = check_preconds thy prls pre mits
6.52 - val ctxt = e_ctxt (*WN110515 cas_input_ DOESNT WORK*)
6.53 + val ctxt = Ctree.e_ctxt (*WN110515 cas_input_ DOESNT WORK*)
6.54 in (pI, pits: itm list, mI, mits: itm list, pre, ctxt) end;
6.55
6.56
6.57 @@ -108,13 +108,13 @@
6.58 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
6.59 val spec = (dI, pI, mI)
6.60 val (pt,_) =
6.61 - cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, hdt)
6.62 - val pt = update_spec pt [] spec
6.63 - val pt = update_pbl pt [] pits
6.64 - val pt = update_met pt [] mits
6.65 - val pt = update_ctxt pt [] ctxt
6.66 + Ctree.cappend_problem Ctree.e_ptree [] (Ctree.e_istate, Ctree.e_ctxt) ([], e_spec) ([], e_spec, hdt)
6.67 + val pt = Ctree.update_spec pt [] spec
6.68 + val pt = Ctree.update_pbl pt [] pits
6.69 + val pt = Ctree.update_met pt [] mits
6.70 + val pt = Ctree.update_ctxt pt [] ctxt
6.71 in
6.72 - SOME (pt, (true, Met, hdt, mits, pre, spec) : ocalhd)
6.73 + SOME (pt, (true, Ctree.Met, hdt, mits, pre, spec) : Ctree.ocalhd)
6.74 end
6.75 end
6.76
6.77 @@ -262,8 +262,8 @@
6.78 (* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
6.79 fun input_icalhd pt (((p, _), hdf, imodel, Pbl, spec as (dI, pI, mI)) : icalhd) =
6.80 let
6.81 - val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case get_obj I pt p of
6.82 - PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
6.83 + val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
6.84 + Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
6.85 spec = sspec as (sdI, spI, smI), probl, meth, ...}
6.86 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
6.87 | _ => error "input_icalhd: uncovered case of get_obj I pt p"
6.88 @@ -289,22 +289,22 @@
6.89 then let val met = (#ppc o Specify.get_met) mI
6.90 val mits = Chead.complete_metitms oris probl meth met
6.91 in if foldl and_ (true, map #3 mits)
6.92 - then (Pbl, probl, mits) else (Met, probl, mits)
6.93 + then (Pbl, probl, mits) else (Ctree.Met, probl, mits)
6.94 end
6.95 else (Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]
6.96 ((#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec spec)))
6.97 (imodel2fstr imodel), meth)
6.98 - val pt = update_spec pt p spec;
6.99 + val pt = Ctree.update_spec pt p spec;
6.100 in if pos_ = Pbl
6.101 then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec))
6.102 val pre =check_preconds(assoc_thy"Isac")prls where_ pits
6.103 - in (update_pbl pt p pits,
6.104 - (Chead.ocalhd_complete pits pre spec, Pbl, hdf', pits, pre, spec):ocalhd)
6.105 + in (Ctree.update_pbl pt p pits,
6.106 + (Chead.ocalhd_complete pits pre spec, Pbl, hdf', pits, pre, spec): Ctree.ocalhd)
6.107 end
6.108 else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec))
6.109 val pre = check_preconds (assoc_thy"Isac") prls pre mits
6.110 - in (update_met pt p mits,
6.111 - (Chead.ocalhd_complete mits pre spec, Met, hdf', mits, pre, spec) : ocalhd)
6.112 + in (Ctree.update_met pt p mits,
6.113 + (Chead.ocalhd_complete mits pre spec, Ctree.Met, hdf', mits, pre, spec) : Ctree.ocalhd)
6.114 end
6.115 end
6.116 end
6.117 @@ -337,13 +337,13 @@
6.118 fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a));
6.119
6.120 fun mk_tacis ro erls (t, r as Thm (id, thm), (t', a)) =
6.121 - (Rewrite (id, thm),
6.122 - Rewrite' ("Isac", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
6.123 - (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
6.124 + (Ctree.Rewrite (id, thm),
6.125 + Ctree.Rewrite' ("Isac", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
6.126 + (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Ctree.Uistate, Ctree.e_ctxt)))
6.127 | mk_tacis _ _ (t, r as Rls_ rls, (t', a)) =
6.128 - (Rewrite_Set (Lucin.rule2rls' r),
6.129 - Rewrite_Set' ("Isac", false, rls, t, (t', a)),
6.130 - (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
6.131 + (Ctree.Rewrite_Set (Lucin.rule2rls' r),
6.132 + Ctree.Rewrite_Set' ("Isac", false, rls, t, (t', a)),
6.133 + (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Ctree.Uistate, Ctree.e_ctxt)))
6.134 | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ rule2str r ^ " at " ^ term2str t)
6.135
6.136 (* fo = ifo excluded already in inform *)
6.137 @@ -378,10 +378,10 @@
6.138 let
6.139 val fo =
6.140 case p_ of
6.141 - Frm => get_obj g_form pt p
6.142 - | Res => (fst o (get_obj g_result pt)) p
6.143 + Frm => Ctree.get_obj Ctree.g_form pt p
6.144 + | Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
6.145 | _ => e_term (*on PblObj is fo <> ifo*);
6.146 - val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
6.147 + val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
6.148 val {rew_ord, erls, rules, ...} = rep_rls nrls
6.149 val (found, der) = concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
6.150 in
6.151 @@ -392,18 +392,18 @@
6.152 val (c', ptp) = Generate.embed_deriv tacis' ptp;
6.153 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
6.154 else
6.155 - if pos = ([], Res) (*TODO: we should stop earlier with trying subproblems *)
6.156 + if pos = ([], Ctree.Res) (*TODO: we should stop earlier with trying subproblems *)
6.157 then ("no derivation found", (tacis, c, ptp): Chead.calcstate')
6.158 else
6.159 let
6.160 val cs' as (tacis, c', ptp) = Solve.nxt_solve_ ptp; (*<---------------------*)
6.161 val (tacis, c'', ptp) = case tacis of
6.162 - ((Subproblem _, _, _)::_) =>
6.163 + ((Ctree.Subproblem _, _, _)::_) =>
6.164 let
6.165 val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)
6.166 - val mI = get_obj g_metID pt p
6.167 + val mI = Ctree.get_obj Ctree.g_metID pt p
6.168 in
6.169 - Solve.nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
6.170 + Solve.nxt_solv (Ctree.Apply_Method' (mI, NONE, Ctree.e_istate, Ctree.e_ctxt)) (Ctree.e_istate, Ctree.e_ctxt) ptp
6.171 end
6.172 | _ => cs';
6.173 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
6.174 @@ -460,29 +460,29 @@
6.175 SOME f_in =>
6.176 let
6.177 val f_in = Thm.term_of f_in
6.178 - val f_succ = get_curr_formula (pt, pos);
6.179 + val f_succ = Ctree.get_curr_formula (pt, pos);
6.180 in
6.181 if f_succ = f_in
6.182 then ("same-formula", cs) (* ctree not cut with replaceFormula *)
6.183 else
6.184 case cas_input f_in of
6.185 - SOME (pt, _) => ("ok",([], [], (pt, (p, Met))))
6.186 + SOME (pt, _) => ("ok",([], [], (pt, (p, Ctree.Met))))
6.187 | NONE =>
6.188 let
6.189 - val pos_pred = lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
6.190 - val f_pred = get_curr_formula (pt, pos_pred)
6.191 + val pos_pred = Ctree.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
6.192 + val f_pred = Ctree.get_curr_formula (pt, pos_pred)
6.193 val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*)
6.194 (*last step re-calc in compare_step TODO before WN09*)
6.195 in
6.196 case msg_calcstate' of
6.197 ("no derivation found", calcstate') =>
6.198 let
6.199 - val pp = par_pblobj pt p
6.200 - val (errpats, nrls, prog) = case Specify.get_met (get_obj g_metID pt pp) of
6.201 + val pp = Ctree.par_pblobj pt p
6.202 + val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
6.203 {errpats, nrls, scr = Prog prog, ...} => (errpats, nrls, prog)
6.204 | _ => error "inform: uncovered case of get_met"
6.205 - val env = case get_istate pt pos of
6.206 - ScrState (env, _, _, _, _, _) => env
6.207 + val env = case Ctree.get_istate pt pos of
6.208 + Ctree.ScrState (env, _, _, _, _, _) => env
6.209 | _ => error "inform: uncovered case of get_istate"
6.210 in
6.211 case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
6.212 @@ -517,15 +517,15 @@
6.213 val some = map (get_fillform subst (thm, form) errpatID) fillpats
6.214 in some |> filter is_some |> map the end
6.215
6.216 -fun find_fillpatterns (pt, pos as (p, _): pos') errpatID =
6.217 +fun find_fillpatterns (pt, pos as (p, _): Ctree.pos') errpatID =
6.218 let
6.219 - val f_curr = get_curr_formula (pt, pos);
6.220 - val pp = par_pblobj pt p
6.221 - val (errpats, prog) = case Specify.get_met (get_obj g_metID pt pp) of
6.222 + val f_curr = Ctree.get_curr_formula (pt, pos);
6.223 + val pp = Ctree.par_pblobj pt p
6.224 + val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
6.225 {errpats, scr = Prog prog, ...} => (errpats, prog)
6.226 | _ => error "find_fillpatterns: uncovered case of get_met"
6.227 - val env = case get_istate pt pos of
6.228 - ScrState (env, _, _, _, _, _) => env
6.229 + val env = case Ctree.get_istate pt pos of
6.230 + Ctree.ScrState (env, _, _, _, _, _) => env
6.231 | _ => error "inform: uncovered case of get_istate"
6.232 val subst = Rtools.get_bdv_subst prog env
6.233 val errpatthms = errpats
6.234 @@ -538,23 +538,23 @@
6.235 which is stored at the pos where the input is stored of "ok". *)
6.236 fun is_exactly_equal (pt, pos as (p, _)) istr =
6.237 case parseNEW (assoc_thy "Isac" |> thy2ctxt) istr of
6.238 - NONE => ("syntax error in '" ^ istr ^ "'", Tac "")
6.239 + NONE => ("syntax error in '" ^ istr ^ "'", Ctree.Tac "")
6.240 | SOME ifo =>
6.241 let
6.242 - val p' = lev_on p;
6.243 - val tac = get_obj g_tac pt p';
6.244 + val p' = Ctree.lev_on p;
6.245 + val tac = Ctree.get_obj Ctree.g_tac pt p';
6.246 in
6.247 case Applicable.applicable_in pos pt tac of
6.248 - Chead.Notappl msg => (msg, Tac "")
6.249 + Chead.Notappl msg => (msg, Ctree.Tac "")
6.250 | Chead.Appl rew =>
6.251 let
6.252 val res = case rew of
6.253 - Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
6.254 - | Rewrite' (_, _, _, _, _, _, (res, _)) => res
6.255 - | t => error ("is_exactly_equal: uncovered case for " ^ tac_2str t)
6.256 + Ctree.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
6.257 + | Ctree.Rewrite' (_, _, _, _, _, _, (res, _)) => res
6.258 + | t => error ("is_exactly_equal: uncovered case for " ^ Ctree.tac_2str t)
6.259 in
6.260 if not (ifo = res)
6.261 - then ("input does not exactly fill the gaps", Tac "")
6.262 + then ("input does not exactly fill the gaps", Ctree.Tac "")
6.263 else ("ok", tac)
6.264 end
6.265 end
6.266 @@ -564,8 +564,8 @@
6.267 let
6.268 val rlsID =
6.269 case tac of
6.270 - Rewrite_Set rlsID => rlsID
6.271 - | Rewrite_Set_Inst (_, rlsID) => rlsID
6.272 + Ctree.Rewrite_Set rlsID => rlsID
6.273 + | Ctree.Rewrite_Set_Inst (_, rlsID) => rlsID
6.274 | _ => "e_rls"
6.275 val (part, thyID) = Rtools.thy_containing_rls "Isac" rlsID;
6.276 val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
7.1 --- a/src/Tools/isac/Interpret/mathengine.sml Wed Dec 21 11:27:22 2016 +0100
7.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Thu Dec 22 10:25:49 2016 +0100
7.3 @@ -9,30 +9,32 @@
7.4 signature MATH_ENGINE =
7.5 sig
7.6 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
7.7 - val me : Solve.tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Generate.mout * Solve.tac'_ * safe * ptree
7.8 + val me : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ptree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Ctree.safe * Ctree.ptree
7.9 val autocalc :
7.10 - pos' list -> pos' -> (ptree * pos') * Generate.taci list -> Solve.auto -> string * pos' list * (ptree * pos')
7.11 + Ctree.pos' list -> Ctree.pos' -> (Ctree.ptree * Ctree.pos') * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.ptree * Ctree.pos')
7.12 val locatetac :
7.13 - tac -> ptree * (posel list * pos_) -> string * (Generate.taci list * pos' list * (ptree * pos'))
7.14 - val step : pos' -> Chead.calcstate -> string * Chead.calcstate'
7.15 + Ctree.tac -> Ctree.ptree * Ctree.pos' -> string * (Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos'))
7.16 + val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'
7.17 val detailstep :
7.18 - ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option
7.19 + Ctree.ptree -> Ctree.pos' -> string * Ctree.ptree * Ctree.pos'
7.20 + val get_pblID : Ctree.ptree * Ctree.pos' -> pblID option
7.21
7.22 - val initcontext_met : ptree -> pos' -> bool * string list * scr * itm list * (bool * term) list
7.23 - val initcontext_pbl : ptree -> pos' -> bool * string list * term * itm list * (bool * term) list
7.24 - val context_met : metID -> ptree -> pos -> bool * metID * scr * itm list * (bool * term) list
7.25 - val context_pbl : pblID -> ptree -> pos -> bool * pblID * term * itm list * (bool * term) list
7.26 - val set_method : metID -> ptree * pos' -> ptree * ocalhd
7.27 - val set_problem : pblID -> ptree * pos' -> ptree * ocalhd
7.28 - val set_theory : thyID -> ptree * pos' -> ptree * ocalhd
7.29 - val tryrefine : pblID -> ptree -> pos' -> bool * pblID * term * itm list * (bool * term) list
7.30 + val initcontext_met : Ctree.ptree -> Ctree.pos' -> bool * string list * scr * itm list * (bool * term) list
7.31 + val initcontext_pbl : Ctree.ptree -> Ctree.pos' -> bool * string list * term * itm list * (bool * term) list
7.32 + val context_met : metID -> Ctree.ptree -> Ctree.pos -> bool * metID * scr * itm list * (bool * term) list
7.33 + val context_pbl : pblID -> Ctree.ptree -> Ctree.pos -> bool * pblID * term * itm list * (bool * term) list
7.34 + val set_method : metID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
7.35 + val set_problem : pblID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
7.36 + val set_theory : thyID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
7.37 + val tryrefine : pblID -> Ctree.ptree -> Ctree.pos' -> bool * pblID * term * itm list * (bool * term) list
7.38
7.39 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.40 type nxt_
7.41 type lOc_
7.42 - val CalcTreeTEST : fmz list -> pos' * NEW * Generate.mout * (string * tac) * safe * ptree
7.43 + val CalcTreeTEST : Ctree.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Ctree.tac) * Ctree.safe * Ctree.ptree
7.44 val f2str : Generate.mout -> cterm'
7.45 - val loc_solve_ : string * tac_ -> ptree * (pos * pos_) -> lOc_
7.46 + val loc_solve_ : string * Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_
7.47 + val loc_specify_ : Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_
7.48 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.49 end
7.50
7.51 @@ -41,10 +43,10 @@
7.52 struct
7.53 (**)
7.54
7.55 -fun get_pblID (pt, (p, _):pos') =
7.56 - let val p' = par_pblobj pt p
7.57 - val (_, pI, _) = get_obj g_spec pt p'
7.58 - val (_, (_, oI, _), _) = get_obj g_origin pt p'
7.59 +fun get_pblID (pt, (p, _): Ctree.pos') =
7.60 + let val p' = Ctree.par_pblobj pt p
7.61 + val (_, pI, _) = Ctree.get_obj Ctree.g_spec pt p'
7.62 + val (_, (_, oI, _), _) = Ctree.get_obj Ctree.g_origin pt p'
7.63 in
7.64 if pI <> e_pblID
7.65 then SOME pI
7.66 @@ -52,7 +54,7 @@
7.67 if oI <> e_pblID then SOME oI else NONE end;
7.68
7.69 (* introduced for test only *)
7.70 -val e_tac_ = Tac_ (Pure.thy, "", "", "");
7.71 +val e_tac_ = Ctree.Tac_ (Pure.thy, "", "", "");
7.72 datatype lOc_ =
7.73 ERror of string (*after loc_specify, loc_solve*)
7.74 | UNsafe of Chead.calcstate' (*after loc_specify, loc_solve*)
7.75 @@ -96,7 +98,7 @@
7.76 (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
7.77 | UNsafe cs' => ("unsafe-ok", cs')
7.78 | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*)
7.79 - (if p' = ([],Res) then "end-of-calculation" else "ok", cs')
7.80 + (if p' = ([], Ctree.Res) then "end-of-calculation" else "ok", cs')
7.81 (*for SEVER.tacs user to ask ? *)
7.82 end
7.83 end
7.84 @@ -106,16 +108,16 @@
7.85 fun nxt_specify_ (ptp as (pt, (p, p_))) =
7.86 let
7.87 val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) =
7.88 - case get_obj I pt p of
7.89 - pblobj as (PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
7.90 + case Ctree.get_obj I pt p of
7.91 + pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
7.92 probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
7.93 - | PrfObj _ => error "nxt_specify_: not on PrfObj"
7.94 + | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj"
7.95 in
7.96 - if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
7.97 + if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin
7.98 then
7.99 case mI' of
7.100 - ["no_met"] => Chead.nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
7.101 - | _ => Chead.nxt_specif Model_Problem (pt, (p,Pbl))
7.102 + ["no_met"] => Chead.nxt_specif (Ctree.Refine_Tacitly pI') (pt, (p, Ctree.Pbl))
7.103 + | _ => Chead.nxt_specif Ctree.Model_Problem (pt, (p, Ctree.Pbl))
7.104 else
7.105 let
7.106 val cpI = if pI = e_pblID then pI' else pI;
7.107 @@ -128,67 +130,67 @@
7.108 Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
7.109 in
7.110 case tac of
7.111 - Apply_Method mI =>
7.112 - Solve.nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
7.113 + Ctree.Apply_Method mI =>
7.114 + Solve.nxt_solv (Ctree.Apply_Method' (mI, NONE, Ctree.e_istate, Ctree.e_ctxt)) (Ctree.e_istate, Ctree.e_ctxt) ptp
7.115 | _ => Chead.nxt_specif tac ptp
7.116 end
7.117 end
7.118
7.119 (* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *)
7.120 -fun set_method (mI:metID) ptp =
7.121 +fun set_method mI ptp =
7.122 let
7.123 val (mits, pt, p) =
7.124 - case Chead.nxt_specif (Specify_Method mI) ptp of
7.125 - ([(_, Specify_Method' (_, _, mits), _)], [], (pt, (p,_))) => (mits, pt, p)
7.126 + case Chead.nxt_specif (Ctree.Specify_Method mI) ptp of
7.127 + ([(_, Ctree.Specify_Method' (_, _, mits), _)], [], (pt, (p,_))) => (mits, pt, p)
7.128 | _ => error "set_method: case 1 uncovered"
7.129 val pre = [] (*...from Specify_Method'*)
7.130 val complete = true (*...from Specify_Method'*)
7.131 (*from Specify_Method' ? vvv, vvv ?*)
7.132 val (hdf, spec) =
7.133 - case get_obj I pt p of
7.134 - PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
7.135 - | PrfObj _ => error "set_method: case 2 uncovered"
7.136 + case Ctree.get_obj I pt p of
7.137 + Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
7.138 + | Ctree.PrfObj _ => error "set_method: case 2 uncovered"
7.139 in
7.140 - (pt, (complete, Met, hdf, mits, pre, spec) : ocalhd)
7.141 + (pt, (complete, Ctree.Met, hdf, mits, pre, spec) : Ctree.ocalhd)
7.142 end
7.143
7.144 (* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *)
7.145 -fun set_problem pI (ptp: ptree * pos') =
7.146 +fun set_problem pI ptp =
7.147 let
7.148 val (complete, pits, pre, pt, p) =
7.149 - case Chead.nxt_specif (Specify_Problem pI) ptp of
7.150 - ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_)))
7.151 + case Chead.nxt_specif (Ctree.Specify_Problem pI) ptp of
7.152 + ([(_, Ctree.Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_)))
7.153 => (complete, pits, pre, pt, p)
7.154 | _ => error "set_problem: case 1 uncovered"
7.155 (*from Specify_Problem' ? vvv, vvv ?*)
7.156 val (hdf, spec) =
7.157 - case get_obj I pt p of
7.158 - PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
7.159 - | PrfObj _ => error "set_problem: case 2 uncovered"
7.160 + case Ctree.get_obj I pt p of
7.161 + Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
7.162 + | Ctree.PrfObj _ => error "set_problem: case 2 uncovered"
7.163 in
7.164 - (pt, (complete, Pbl, hdf, pits, pre, spec) : ocalhd)
7.165 + (pt, (complete, Ctree.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd)
7.166 end
7.167
7.168 -fun set_theory (tI:thyID) (ptp: ptree * pos') =
7.169 +fun set_theory tI ptp =
7.170 let
7.171 val (complete, pits, pre, pt, p) =
7.172 - case Chead.nxt_specif (Specify_Theory tI) ptp of
7.173 - ([(_, Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _)))
7.174 + case Chead.nxt_specif (Ctree.Specify_Theory tI) ptp of
7.175 + ([(_, Ctree.Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _)))
7.176 => (complete, pits, pre, pt, p)
7.177 | _ => error "set_theory: case 1 uncovered"
7.178 (*from Specify_Theory' ? vvv, vvv ?*)
7.179 val (hdf, spec) =
7.180 - case get_obj I pt p of
7.181 - PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
7.182 - | PrfObj _ => error "set_theory: case 2 uncovered"
7.183 - in (pt, (complete, Pbl, hdf, pits, pre, spec) : ocalhd) end;
7.184 + case Ctree.get_obj I pt p of
7.185 + Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
7.186 + | Ctree.PrfObj _ => error "set_theory: case 2 uncovered"
7.187 + in (pt, (complete, Ctree.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd) end;
7.188
7.189 (* does a step forward; returns tactic used, ctree updated.
7.190 TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
7.191 -fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis): Chead.calcstate) =
7.192 +fun step (ip as (_, p_)) (ptp as (pt,p), tacis) =
7.193 let val pIopt = get_pblID (pt,ip);
7.194 in
7.195 - if ip = ([],Res)
7.196 + if ip = ([], Ctree.Res)
7.197 then ("end-of-calculation", (tacis, [], ptp): Chead.calcstate')
7.198 else
7.199 case tacis of
7.200 @@ -197,7 +199,7 @@
7.201 then
7.202 let val (pt',c',p') = Generate.generate tacis (pt,[],p)
7.203 in ("ok", (tacis, c', (pt', p'))) end
7.204 - else (case (if member op = [Pbl, Met] p_
7.205 + else (case (if member op = [Ctree.Pbl, Ctree.Met] p_
7.206 then nxt_specify_ (pt, ip) else Solve.nxt_solve_ (pt, ip))
7.207 handle ERROR msg => (writeln ("*** " ^ msg);
7.208 ([], [], ptp)) (*e.g. Add_Given "equality///"*) of
7.209 @@ -206,7 +208,7 @@
7.210 | _ => (case pIopt of
7.211 NONE => ("no-fmz-spec", ([], [], ptp))
7.212 | SOME _ => (*vvvvvv: Apply_Method without init_form*)
7.213 - (case if member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p))
7.214 + (case if member op = [Ctree.Pbl, Ctree.Met] p_ andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p))
7.215 then nxt_specify_ (pt, ip)
7.216 else (Solve.nxt_solve_ (pt,ip))
7.217 handle ERROR msg => (writeln ("*** " ^ msg);
7.218 @@ -234,12 +236,12 @@
7.219 else (str, c@c', ptp) end
7.220 (* handles autoord <= 3, autoord > 3 handled by all_solve, complete_solve *)
7.221 | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto =
7.222 - if Solve.autoord auto > 3 andalso just_created (pt, pos)
7.223 + if Solve.autoord auto > 3 andalso Ctree.just_created (pt, pos)
7.224 then
7.225 let val ptp = Chead.all_modspec (pt, pos);
7.226 in Solve.all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
7.227 else
7.228 - if member op = [Pbl, Met] p_
7.229 + if member op = [Ctree.Pbl, Ctree.Met] p_
7.230 then
7.231 if not (Chead.is_complete_mod (pt, pos))
7.232 then
7.233 @@ -271,10 +273,10 @@
7.234 fun initcontext_pbl pt (p, _) =
7.235 let
7.236 val (probl, os, pI, hdl, pI') =
7.237 - case get_obj I pt p of
7.238 - PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...}
7.239 + case Ctree.get_obj I pt p of
7.240 + Ctree.PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...}
7.241 => (probl, os, pI, hdl, pI')
7.242 - | PrfObj _ => error "initcontext_pbl: uncovered case"
7.243 + | Ctree.PrfObj _ => error "initcontext_pbl: uncovered case"
7.244 val pblID =
7.245 if pI' = e_pblID
7.246 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
7.247 @@ -288,9 +290,9 @@
7.248 fun initcontext_met pt (p,_) =
7.249 let
7.250 val (meth, os, mI, mI') =
7.251 - case get_obj I pt p of
7.252 - PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
7.253 - | PrfObj _ => error "initcontext_met: uncovered case"
7.254 + case Ctree.get_obj I pt p of
7.255 + Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
7.256 + | Ctree.PrfObj _ => error "initcontext_met: uncovered case"
7.257 val metID = if mI' = e_metID
7.258 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
7.259 else mI'
7.260 @@ -301,24 +303,24 @@
7.261 end
7.262
7.263 (* match the model of a problem at pos p with the model-pattern of the problem with pblID *)
7.264 -fun context_pbl pI pt (p:pos) =
7.265 +fun context_pbl pI pt p =
7.266 let
7.267 val (probl, os, hdl) =
7.268 - case get_obj I pt p of
7.269 - PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
7.270 - | PrfObj _ => error "context_pbl: uncovered case"
7.271 + case Ctree.get_obj I pt p of
7.272 + Ctree.PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
7.273 + | Ctree.PrfObj _ => error "context_pbl: uncovered case"
7.274 val {ppc,where_,prls,...} = Specify.get_pbt pI
7.275 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
7.276 in
7.277 (model_ok, pI, hdl, pbl, pre)
7.278 end
7.279
7.280 -fun context_met mI pt (p:pos) =
7.281 +fun context_met mI pt p =
7.282 let
7.283 val (meth, os) =
7.284 - case get_obj I pt p of
7.285 - PblObj {meth, origin = (os, _, _),...} => (meth, os)
7.286 - | PrfObj _ => error "context_met: uncovered case"
7.287 + case Ctree.get_obj I pt p of
7.288 + Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
7.289 + | Ctree.PrfObj _ => error "context_met: uncovered case"
7.290 val {ppc,pre,prls,scr,...} = Specify.get_met mI
7.291 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
7.292 in
7.293 @@ -328,9 +330,9 @@
7.294 fun tryrefine pI pt (p,_) =
7.295 let
7.296 val (probl, os, hdl) =
7.297 - case get_obj I pt p of
7.298 - PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
7.299 - | PrfObj _ => error "context_met: uncovered case"
7.300 + case Ctree.get_obj I pt p of
7.301 + Ctree.PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
7.302 + | Ctree.PrfObj _ => error "context_met: uncovered case"
7.303 in
7.304 case Specify.refine_pbl (assoc_thy "Isac") pI probl of
7.305 NONE => (*copy from context_pbl*)
7.306 @@ -343,17 +345,17 @@
7.307 | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre)
7.308 end
7.309
7.310 -fun detailstep pt (pos as (p, _):pos') =
7.311 +fun detailstep pt (pos as (p, _)) =
7.312 let
7.313 - val nd = get_nd pt p
7.314 - val cn = children nd
7.315 + val nd = Ctree.get_nd pt p
7.316 + val cn = Ctree.children nd
7.317 in
7.318 if null cn
7.319 then
7.320 - if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
7.321 + if (Ctree.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)]
7.322 then Solve.detailrls pt pos
7.323 - else ("no-Rewrite_Set...", EmptyPtree, e_pos')
7.324 - else ("donesteps", pt, (p @ [length (children (get_nd pt p))], Res))
7.325 + else ("no-Rewrite_Set...", Ctree.EmptyPtree, Ctree.e_pos')
7.326 + else ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Ctree.Res))
7.327 end;
7.328
7.329
7.330 @@ -368,8 +370,8 @@
7.331 val (form, _, _) = Chead.pt_extract ptp
7.332 in
7.333 case form of
7.334 - Form t => Generate.FormKF (term2str t)
7.335 - | ModSpec (_, p_, _, gfr, pre, _) =>
7.336 + Ctree.Form t => Generate.FormKF (term2str t)
7.337 + | Ctree.ModSpec (_, p_, _, gfr, pre, _) =>
7.338 Generate.PpcKF (
7.339 (case p_ of Pbl => Generate.Problem [] | Met => Generate.Method []
7.340 | _ => error "TESTg_form: uncovered case",
7.341 @@ -381,9 +383,9 @@
7.342 fun CalcTreeTEST [(fmz, sp)] =
7.343 let
7.344 val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)
7.345 - val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
7.346 + val tac = case tacis of [] => Ctree.Empty_Tac | _ => (#1 o hd) tacis
7.347 val f = TESTg_form (pt,p)
7.348 - in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end
7.349 + in (p, []:NEW, f, (Ctree.tac2IDstr tac, tac), Ctree.Sundef, pt) end
7.350 | CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"
7.351
7.352 (*for tests > 15.8.03 after separation setnexttactic / nextTac:
7.353 @@ -406,7 +408,7 @@
7.354 | ("failure", _) => error "sys-error"
7.355 | _ => error "me: uncovered case"
7.356 val (_, ts) =
7.357 - (case step p ((pt, e_pos'),[]) of
7.358 + (case step p ((pt, Ctree.e_pos'),[]) of
7.359 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
7.360 | ("helpless", _) => ("helpless: cannot propose tac", [])
7.361 | ("no-fmz-spec", _) => error "no-fmz-spec"
7.362 @@ -416,9 +418,9 @@
7.363 val tac =
7.364 case ts of
7.365 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
7.366 - | _ => if p = ([], Res) then End_Proof' else Empty_Tac;
7.367 + | _ => if p = ([], Ctree.Res) then Ctree.End_Proof' else Ctree.Empty_Tac;
7.368 in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
7.369 - (tac2IDstr tac, tac): Solve.tac'_, Sundef, pt)
7.370 + (Ctree.tac2IDstr tac, tac), Ctree.Sundef, pt)
7.371 end
7.372
7.373 (* for quick test-print-out, until 'type inout' is removed *)
8.1 --- a/src/Tools/isac/Interpret/ptyps.sml Wed Dec 21 11:27:22 2016 +0100
8.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Thu Dec 22 10:25:49 2016 +0100
8.3 @@ -7,7 +7,7 @@
8.4 sig
8.5 type field
8.6 (* for calchead.sml, if below at left margin *)
8.7 - val prep_ori : fmz_ -> theory -> field list -> ori list * Proof.context
8.8 + val prep_ori : Ctree.fmz_ -> theory -> field list -> ori list * Proof.context
8.9 val add_id : 'a list -> (int * 'a) list
8.10 val add_field' : theory -> field list -> ori list -> ori list
8.11 val match_itms_oris : theory -> itm list -> field list * term list * rls ->
8.12 @@ -45,10 +45,10 @@
8.13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.14 val show_ptyps : unit -> unit
8.15 val show_mets : unit -> unit
8.16 - val refine : fmz_ -> pblID -> match list
8.17 + val refine : Ctree.fmz_ -> pblID -> match list
8.18 val e_errpat : errpat
8.19 datatype match' = Matches' of item ppc | NoMatch' of item ppc
8.20 - val match_pbl : fmz_ -> pbt -> match'
8.21 + val match_pbl : Ctree.fmz_ -> pbt -> match'
8.22 val show_pblguhs : unit -> unit
8.23 val sort_pblguhs : unit -> unit
8.24 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.25 @@ -181,7 +181,7 @@
8.26
8.27 fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e);
8.28
8.29 -fun prep_ori [] _ _ = ([], e_ctxt)
8.30 +fun prep_ori [] _ _ = ([], Ctree.e_ctxt)
8.31 | prep_ori fmz thy pbt =
8.32 let
8.33 val ctxt = Proof_Context.init_global thy |> fold declare_constraints fmz;
8.34 @@ -511,7 +511,7 @@
8.35 | NoMatch' of item ppc;
8.36
8.37 (* match a formalization with a problem type, for tests *)
8.38 -fun match_pbl (fmz: fmz_) ({thy = thy, where_ = pre, ppc, prls = er, ...}: pbt) =
8.39 +fun match_pbl (fmz: Ctree.fmz_) ({thy = thy, where_ = pre, ppc, prls = er, ...}: pbt) =
8.40 let
8.41 val oris = prep_ori fmz thy ppc |> #1;
8.42 val (bool, (itms, pre')) = match_oris' thy oris (ppc, pre, er);
8.43 @@ -630,7 +630,7 @@
8.44
8.45 (* for math-experts and test;
8.46 FIXME.WN021019: needs thy for parsing fmz *)
8.47 -fun refine (fmz: fmz_) (pblID: pblID) =
8.48 +fun refine (fmz: Ctree.fmz_) (pblID: pblID) =
8.49 app_ptyp (refin' ((rev o tl) pblID) fmz []) pblID (rev pblID);
8.50
8.51 (* make a guh from a reference to an element in the kestore;
9.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Dec 21 11:27:22 2016 +0100
9.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Dec 22 10:25:49 2016 +0100
9.3 @@ -7,7 +7,7 @@
9.4 sig
9.5 type deriv
9.6 val contains_rule : rule -> rls -> bool
9.7 - val atomic_appl_tacs : theory -> string -> rls -> term -> tac -> tac list
9.8 + val atomic_appl_tacs : theory -> string -> rls -> term -> Ctree.tac -> Ctree.tac list
9.9 val thy_containing_rls : theory' -> rls' -> string * theory'
9.10 val thy_containing_cal : theory' -> prog_calcID -> string * string
9.11 datatype contthy
9.12 @@ -29,17 +29,17 @@
9.13 val thms_of_rls : rls -> rule list
9.14 val theID2filename : theID -> filename
9.15 val no_thycontext : guh -> bool
9.16 - val subs_from : istate -> 'a -> guh -> subs
9.17 - val guh2rewtac : guh -> subs -> tac
9.18 - val get_tac_checked : ptree -> pos' -> tac
9.19 - val context_thy : ptree * (pos * pos_) -> tac -> contthy
9.20 + val subs_from : Ctree.istate -> 'a -> guh -> Ctree.subs
9.21 + val guh2rewtac : guh -> Ctree.subs -> Ctree.tac
9.22 + val get_tac_checked : Ctree.ptree -> Ctree.pos' -> Ctree.tac
9.23 + val context_thy : Ctree.ptree * Ctree.pos' -> Ctree.tac -> contthy
9.24 val distinct_Thm : rule list -> rule list
9.25 val eq_Thms : string list -> rule -> bool
9.26 val make_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->
9.27 term option -> term -> deriv
9.28 val reverse_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->
9.29 term option -> term -> (rule * (term * term list)) list
9.30 - val get_bdv_subst : term -> (term * term) list -> subs option * subst
9.31 + val get_bdv_subst : term -> (term * term) list -> Ctree.subs option * subst
9.32 val thy_containing_thm : string -> string * string val thypart2filename : theID -> filename
9.33 val guh2theID : guh -> theID
9.34 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
9.35 @@ -353,18 +353,18 @@
9.36
9.37 (*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718
9.38 pass other tacs unchanged.*)
9.39 -fun get_tac_checked pt ((p, _) : pos') = get_obj g_tac pt p;
9.40 +fun get_tac_checked pt ((p, _) : Ctree.pos') = Ctree.get_obj Ctree.g_tac pt p;
9.41
9.42 (* create a derivation-name, eg. ("refl", _) --> "HOL.refl"*)
9.43 fun deriv_of_thm'' ((thmID, _) : thm'') =
9.44 thmID |> Global_Theory.get_thm (Isac ()) |> Thm.get_name_hint
9.45
9.46 (* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)
9.47 -fun context_thy (pt, pos as (p,p_)) (tac as Rewrite thm'') =
9.48 +fun context_thy (pt, pos as (p,p_)) (tac as Ctree.Rewrite thm'') =
9.49 let val thm_deriv = deriv_of_thm'' thm''
9.50 in
9.51 (case Applicable.applicable_in pos pt tac of
9.52 - Chead.Appl (Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
9.53 + Chead.Appl (Ctree.Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
9.54 ContThm
9.55 {thyID = theory'2thyID thy',
9.56 thm = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
9.57 @@ -373,11 +373,11 @@
9.58 result = res, resasms = asm, asmrls = id_rls erls}
9.59 | Chead.Notappl _ =>
9.60 let
9.61 - val pp = par_pblobj pt p
9.62 - val thy' = get_obj g_domID pt pp
9.63 + val pp = Ctree.par_pblobj pt p
9.64 + val thy' = Ctree.get_obj Ctree.g_domID pt pp
9.65 val f = case p_ of
9.66 - Frm => get_obj g_form pt p
9.67 - | Res => (fst o (get_obj g_result pt)) p | _ => error "context_thy: uncovered position"
9.68 + Frm => Ctree.get_obj Ctree.g_form pt p
9.69 + | Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p | _ => error "context_thy: uncovered position"
9.70 in
9.71 ContNOrew
9.72 {thyID = theory'2thyID thy',
9.73 @@ -387,11 +387,11 @@
9.74 end
9.75 | _ => error "context_thy..Rewrite: uncovered case 2")
9.76 end
9.77 - | context_thy (pt, pos as (p, p_)) (tac as Rewrite_Inst (subs, (thmID, _))) =
9.78 + | context_thy (pt, pos as (p, p_)) (tac as Ctree.Rewrite_Inst (subs, (thmID, _))) =
9.79 let val thm = Global_Theory.get_thm (Isac ()) thmID
9.80 in
9.81 (case Applicable.applicable_in pos pt tac of
9.82 - Chead.Appl (Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
9.83 + Chead.Appl (Ctree.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
9.84 let
9.85 val thm_deriv = Thm.get_name_hint thm
9.86 val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)
9.87 @@ -408,13 +408,13 @@
9.88 let
9.89 val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
9.90 val thm_deriv = Thm.get_name_hint thm
9.91 - val pp = par_pblobj pt p
9.92 - val thy' = get_obj g_domID pt pp
9.93 - val subst = subs2subst (assoc_thy thy') subs
9.94 + val pp = Ctree.par_pblobj pt p
9.95 + val thy' = Ctree.get_obj Ctree.g_domID pt pp
9.96 + val subst = Ctree.subs2subst (assoc_thy thy') subs
9.97 val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)
9.98 val f = case p_ of
9.99 - Frm => get_obj g_form pt p
9.100 - | Res => (fst o (get_obj g_result pt)) p | _ => error "context_thy: uncovered case 3"
9.101 + Frm => Ctree.get_obj Ctree.g_form pt p
9.102 + | Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p | _ => error "context_thy: uncovered case 3"
9.103 in
9.104 ContNOrewInst
9.105 {thyID = theory'2thyID thy',
9.106 @@ -423,24 +423,24 @@
9.107 end
9.108 | _ => error "context_thy..Rewrite_Inst: uncovered case 4")
9.109 end
9.110 - | context_thy (pt, p) (tac as Rewrite_Set rls') =
9.111 + | context_thy (pt, p) (tac as Ctree.Rewrite_Set rls') =
9.112 (case Applicable.applicable_in p pt tac of
9.113 - Chead.Appl (Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
9.114 + Chead.Appl (Ctree.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
9.115 ContRls
9.116 {thyID = theory'2thyID thy',
9.117 rls = rls2guh (thy_containing_rls thy' rls') rls',
9.118 applto = f, result = res, asms = asm}
9.119 | _ => error ("context_thy Rewrite_Set: not for Chead.Notappl"))
9.120 - | context_thy (pt,p) (tac as Rewrite_Set_Inst (_(*subs*), rls')) =
9.121 + | context_thy (pt,p) (tac as Ctree.Rewrite_Set_Inst (_(*subs*), rls')) =
9.122 (case Applicable.applicable_in p pt tac of
9.123 - Chead.Appl (Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
9.124 + Chead.Appl (Ctree.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
9.125 ContRlsInst
9.126 {thyID = theory'2thyID thy',
9.127 rls = rls2guh (thy_containing_rls thy' rls') rls',
9.128 bdvs = subst, applto = f, result = res, asms = asm}
9.129 | _ => error ("context_thy Rewrite_Set_Inst: not for Chead.Notappl"))
9.130 | context_thy (_, p) tac =
9.131 - error ("context_thy: not for tac " ^ tac2str tac ^ " at " ^ pos'2str p)
9.132 + error ("context_thy: not for tac " ^ Ctree.tac2str tac ^ " at " ^ Ctree.pos'2str p)
9.133
9.134 (* get all theorems in a rule set (recursivley containing rule sets) *)
9.135 fun thm_of_rule Erule = []
9.136 @@ -470,43 +470,43 @@
9.137 fun try_rew thy ((_, ro) : rew_ord) erls (subst : subst) f (thm' as Thm (_, thm)) =
9.138 if contains_bdv thm
9.139 then case rewrite_inst_ thy ro erls false subst thm f of
9.140 - SOME _ => [rule2tac thy subst thm']
9.141 + SOME _ => [Ctree.rule2tac thy subst thm']
9.142 | NONE => []
9.143 else (case rewrite_ thy ro erls false thm f of
9.144 - SOME _ => [rule2tac thy [] thm']
9.145 + SOME _ => [Ctree.rule2tac thy [] thm']
9.146 | NONE => [])
9.147 | try_rew thy _ _ _ f (cal as Calc c) =
9.148 (case adhoc_thm thy c f of
9.149 - SOME _ => [rule2tac thy [] cal]
9.150 + SOME _ => [Ctree.rule2tac thy [] cal]
9.151 | NONE => [])
9.152 | try_rew thy _ _ _ f (cal as Cal1 c) =
9.153 (case adhoc_thm thy c f of
9.154 - SOME _ => [rule2tac thy [] cal]
9.155 + SOME _ => [Ctree.rule2tac thy [] cal]
9.156 | NONE => [])
9.157 | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls
9.158 | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"
9.159 and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules, ...}) =
9.160 - gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
9.161 + gen_distinct Ctree.eq_tac (flat (map (try_rew thy ro erls subst f) rules))
9.162 | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) =
9.163 - gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
9.164 + gen_distinct Ctree.eq_tac (flat (map (try_rew thy ro erls subst f) rules))
9.165 | filter_appl_rews _ _ _ (Rrls _) = []
9.166 | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"
9.167
9.168 (* decide if a tactic is applicable to a given formula;
9.169 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
9.170 -fun atomic_appl_tacs thy _ _ f (Calculate scrID) =
9.171 +fun atomic_appl_tacs thy _ _ f (Ctree.Calculate scrID) =
9.172 try_rew thy e_rew_ordX e_rls [] f (Calc (assoc_calc' thy scrID |> snd))
9.173 - | atomic_appl_tacs thy ro erls f (Rewrite thm'') =
9.174 + | atomic_appl_tacs thy ro erls f (Ctree.Rewrite thm'') =
9.175 try_rew thy (ro, assoc_rew_ord ro) erls [] f (Thm thm'')
9.176 - | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm'')) =
9.177 - try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f (Thm thm'')
9.178 + | atomic_appl_tacs thy ro erls f (Ctree.Rewrite_Inst (subs, thm'')) =
9.179 + try_rew thy (ro, assoc_rew_ord ro) erls (Ctree.subs2subst thy subs) f (Thm thm'')
9.180
9.181 - | atomic_appl_tacs thy _ _ f (Rewrite_Set rls') =
9.182 + | atomic_appl_tacs thy _ _ f (Ctree.Rewrite_Set rls') =
9.183 filter_appl_rews thy [] f (assoc_rls rls')
9.184 - | atomic_appl_tacs thy _ _ f (Rewrite_Set_Inst (subs, rls')) =
9.185 - filter_appl_rews thy (subs2subst thy subs) f (assoc_rls rls')
9.186 + | atomic_appl_tacs thy _ _ f (Ctree.Rewrite_Set_Inst (subs, rls')) =
9.187 + filter_appl_rews thy (Ctree.subs2subst thy subs) f (assoc_rls rls')
9.188 | atomic_appl_tacs _ _ _ _ tac =
9.189 - (tracing ("### atomic_appl_tacs: not impl. for tac = '" ^ tac2str tac ^ "'"); []);
9.190 + (tracing ("### atomic_appl_tacs: not impl. for tac = '" ^ Ctree.tac2str tac ^ "'"); []);
9.191
9.192 (* filenames not only for thydata, but also for thy's etc *)
9.193 fun theID2filename (theID : theID) = theID2guh theID ^ ".xml" : filename
9.194 @@ -554,14 +554,14 @@
9.195
9.196 fun guh2filename (guh : guh) = guh ^ ".xml" : filename;
9.197
9.198 -fun guh2rewtac (guh : guh) ([] : subs) =
9.199 +fun guh2rewtac (guh : guh) ([] : Ctree.subs) =
9.200 let
9.201 val (_, thy, sect, xstr) = case guh2theID guh of
9.202 [isa, thy, sect, xstr] => (isa, thy, sect, xstr)
9.203 | _ => error "guh2rewtac: uncovered case"
9.204 in case sect of
9.205 - "Theorems" => Rewrite (xstr, assoc_thm'' (assoc_thy thy) xstr)
9.206 - | "Rulesets" => Rewrite_Set xstr
9.207 + "Theorems" => Ctree.Rewrite (xstr, assoc_thm'' (assoc_thy thy) xstr)
9.208 + | "Rulesets" => Ctree.Rewrite_Set xstr
9.209 | _ => error ("guh2rewtac: not impl. for '"^xstr^"'")
9.210 end
9.211 | guh2rewtac guh subs =
9.212 @@ -571,8 +571,8 @@
9.213 | _ => error "guh2rewtac: uncovered case"
9.214 in case sect of
9.215 "Theorems" =>
9.216 - Rewrite_Inst (subs, (xstr, assoc_thm'' (assoc_thy thy) xstr))
9.217 - | "Rulesets" => Rewrite_Set_Inst (subs, xstr)
9.218 + Ctree.Rewrite_Inst (subs, (xstr, assoc_thm'' (assoc_thy thy) xstr))
9.219 + | "Rulesets" => Ctree.Rewrite_Set_Inst (subs, xstr)
9.220 | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'")
9.221 end
9.222
9.223 @@ -587,7 +587,7 @@
9.224 # otherwise []
9.225 WN060617 hack assuming that all scripts use only one bound variable
9.226 and use 'v_' as the formal argument for this bound variable*)
9.227 -fun subs_from (ScrState (env, _, _, _, _, _)) _ (guh : guh) =
9.228 +fun subs_from (Ctree.ScrState (env, _, _, _, _, _)) _ (guh : guh) =
9.229 let
9.230 val (_, _, thyID, sect, xstr) = case guh2theID guh of
9.231 theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)
9.232 @@ -602,7 +602,7 @@
9.233 let
9.234 val formal_arg = str2term "v_"
9.235 val value = subst_atomic env formal_arg
9.236 - in ["(bdv," ^ term2str value ^ ")"] : subs end
9.237 + in ["(bdv," ^ term2str value ^ ")"] : Ctree.subs end
9.238 else []
9.239 end
9.240 | "Rulesets" =>
9.241 @@ -614,7 +614,7 @@
9.242 let
9.243 val formal_arg = str2term "v_"
9.244 val value = subst_atomic env formal_arg
9.245 - in ["(bdv," ^ term2str value ^ ")"] : subs end
9.246 + in ["(bdv," ^ term2str value ^ ")"] : Ctree.subs end
9.247 else []
9.248 end
9.249 | str => error ("subs_from: uncovered case with " ^ str)
9.250 @@ -635,13 +635,13 @@
9.251 | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst
9.252 in
9.253 case scan prog of
9.254 - NONE => (NONE: subs option, []: subst)
9.255 + NONE => (NONE: Ctree.subs option, []: subst)
9.256 | SOME tm =>
9.257 let val subst = tm |> subst_atomic env |> isalist2list |> map isapair2pair
9.258 (* "[(bdv,v_v)]": term
9.259 |> "[(bdv,x)]": term |> ["(bdv,x)"]: term list
9.260 |> [("bdv","x")]: (term * term) list *)
9.261 - in (SOME (subst2subs subst), subst) end
9.262 + in (SOME (Ctree.subst2subs subst), subst) end
9.263 (*"SOME [(bdv,v_v)]": term --> ["(bdv,v_v)"]: string list*)
9.264 end
9.265
10.1 --- a/src/Tools/isac/Interpret/script.sml Wed Dec 21 11:27:22 2016 +0100
10.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Dec 22 10:25:49 2016 +0100
10.3 @@ -8,43 +8,43 @@
10.4 signature LUCAS_INTERPRETER =
10.5 sig
10.6
10.7 - type step = tac_ * Generate.mout * ptree * pos' * pos' list
10.8 - datatype locate = NotLocatable | Steps of istate * step list
10.9 + type step = Ctree.tac_ * Generate.mout * Ctree.ptree * Ctree.pos' * Ctree.pos' list
10.10 + datatype locate = NotLocatable | Steps of Ctree.istate * step list
10.11
10.12 val next_tac : (*diss: next-tactic-function*)
10.13 - theory' * rls -> ptree * pos' -> scr -> istate * 'a -> tac_ * (istate * 'a) * (term * safe)
10.14 + theory' * rls -> Ctree.ptree * Ctree.pos' -> scr -> Ctree.istate * 'a -> Ctree.tac_ * (Ctree.istate * 'a) * (term * Ctree.safe)
10.15 val locate_gen : (*diss: locate-function*)
10.16 - theory' * rls -> tac_ -> ptree * pos' -> scr * 'a -> istate * Proof.context -> locate
10.17 + theory' * rls -> Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> scr * 'a -> Ctree.istate * Proof.context -> locate
10.18
10.19 (* can these functions be local to Lucin or part of LItools ? *)
10.20 - val sel_rules : ptree -> pos' -> tac list
10.21 + val sel_rules : Ctree.ptree -> Ctree.pos' -> Ctree.tac list
10.22 val init_form : 'a -> scr -> (term * term) list -> term option
10.23 - val tac_2tac : tac_ -> tac
10.24 - val init_scrstate : theory -> itm list -> metID -> istate * Proof.context * scr
10.25 - val from_pblobj' : theory' -> pos * pos_ -> ptree -> rls * (istate * Proof.context) * scr
10.26 - val from_pblobj_or_detail' : theory' -> pos * pos_ -> ptree ->
10.27 - rls * (istate * Proof.context) * scr
10.28 + val tac_2tac : Ctree.tac_ -> Ctree.tac
10.29 + val init_scrstate : theory -> itm list -> metID -> Ctree.istate * Proof.context * scr
10.30 + val from_pblobj' : theory' -> Ctree.pos' -> Ctree.ptree -> rls * (Ctree.istate * Proof.context) * scr
10.31 + val from_pblobj_or_detail' : theory' -> Ctree.pos' -> Ctree.ptree ->
10.32 + rls * (Ctree.istate * Proof.context) * scr
10.33 val rule2thm'' : rule -> thm''
10.34 val rule2rls' : rule -> string
10.35
10.36 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.37 datatype asap = Aundef | AssOnly | AssGen
10.38 - datatype appy = Appy of tac_ * scrstate | Napp of env | Skip of term * env
10.39 + datatype appy = Appy of Ctree.tac_ * Ctree.scrstate | Napp of env | Skip of term * env
10.40 datatype appy_ = Napp_ | Skip_
10.41 - val appy : theory' * rls -> ptree * pos' -> env -> lrd list -> term -> term option -> term -> appy
10.42 + val appy : theory' * rls -> Ctree.ptree * Ctree.pos' -> env -> lrd list -> term -> term option -> term -> appy
10.43 val formal_args : term -> term list
10.44 val get_stac : 'a -> term -> term option
10.45 val go : loc_ -> term -> term
10.46 val handle_leaf : string -> theory' -> rls -> env -> term option -> term -> term ->
10.47 term option * stacexpr
10.48 val id_of_scr : term -> string
10.49 - val is_spec_pos : pos_ -> bool
10.50 + val is_spec_pos : Ctree.pos_ -> bool
10.51 val itms2args : 'a -> metID -> itm list -> term list
10.52 - val nstep_up : theory' * rls -> ptree * pos' -> scr -> env -> lrd list -> appy_ ->
10.53 + val nstep_up : theory' * rls -> Ctree.ptree * Ctree.pos' -> scr -> env -> lrd list -> appy_ ->
10.54 term option -> term -> appy
10.55 - val sel_appl_atomic_tacs : ptree -> pos' -> tac list
10.56 - val stac2tac : ptree -> theory -> term -> tac
10.57 - val stac2tac_ : ptree -> theory -> term -> tac * tac_
10.58 + val sel_appl_atomic_tacs : Ctree.ptree -> Ctree.pos' -> Ctree.tac list
10.59 + val stac2tac : Ctree.ptree -> theory -> term -> Ctree.tac
10.60 + val stac2tac_ : Ctree.ptree -> theory -> term -> Ctree.tac * Ctree.tac_
10.61 val upd_env_opt : env -> term option * term -> env
10.62 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.63 end
10.64 @@ -55,6 +55,8 @@
10.65 (**)
10.66 structure Lucin(**): LUCAS_INTERPRETER(**) =
10.67 struct
10.68 +open Ctree
10.69 +
10.70 (**)
10.71 (* data for creating a new node in ctree; designed for use as:
10.72 fun ass* scrstate steps = / ... case ass* scrstate steps of /
11.1 --- a/src/Tools/isac/Interpret/solve.sml Wed Dec 21 11:27:22 2016 +0100
11.2 +++ b/src/Tools/isac/Interpret/solve.sml Thu Dec 22 10:25:49 2016 +0100
11.3 @@ -7,7 +7,7 @@
11.4
11.5 structure Solve =
11.6 struct
11.7 -(*open Ctree;*)
11.8 +open Ctree;
11.9
11.10 fun safe (ScrState (_,_,_,_,s,_)) = s
11.11 | safe (RrlsState _) = Safe;
11.12 @@ -137,7 +137,7 @@
11.13
11.14
11.15 fun step2taci ((tac_, _, pt, p, _) : Lucin.step) = (*FIXXME.040312: redesign step*)
11.16 - (Lucin.tac_2tac tac_, tac_, (p, get_loc pt p)): Generate.taci;
11.17 + (Lucin.tac_2tac tac_, tac_, (p, Ctree.get_loc pt p)): Generate.taci;
11.18
11.19
11.20 (*FIXME.WN050821 compare solve ... nxt_solv*)
12.1 --- a/src/Tools/isac/print_exn_G.sml Wed Dec 21 11:27:22 2016 +0100
12.2 +++ b/src/Tools/isac/print_exn_G.sml Thu Dec 22 10:25:49 2016 +0100
12.3 @@ -6,7 +6,7 @@
12.4
12.5 fun print_exn_unit e =
12.6 case e of
12.7 - PTREE str =>
12.8 + Applicable.PTREE str =>
12.9 (tracing ("Exception PTREE raised:\n" ^ str))
12.10 (* | SCRIPT str =>
12.11 (tracing ("Exception SCRIPT raised:\n" ^ str))
13.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Wed Dec 21 11:27:22 2016 +0100
13.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Thu Dec 22 10:25:49 2016 +0100
13.3 @@ -25,18 +25,18 @@
13.4 val keref2xml : int -> ketype -> kestoreID -> xml
13.5 val model2xml :
13.6 int -> SpecifyTools.itm list -> (bool * Term.term) list -> xml
13.7 - val modspec2xml : int -> ocalhd -> xml
13.8 + val modspec2xml : int -> Ctree.ocalhd -> xml
13.9 val pattern2xml :
13.10 int ->
13.11 (string * (Term.term * Term.term)) list -> Term.term list -> string
13.12 - val pos'2xml : int -> string * (int list * pos_) -> string
13.13 - val pos'calchead2xml : int -> pos' * ocalhd -> xml
13.14 - val pos_2xml : int -> pos_ -> string
13.15 - val posform2xml : int -> pos' * Term.term -> xml
13.16 - val posformhead2xml : int -> pos' * ptform -> string
13.17 - val posformheads2xml : int -> (pos' * ptform) list -> xml
13.18 - val posforms2xml : int -> (pos' * Term.term) list -> xml
13.19 - val posterms2xml : int -> (pos' * term) list -> xml
13.20 + val pos'2xml : int -> string * (int list * Ctree.pos_) -> string
13.21 + val pos'calchead2xml : int -> Ctree.pos' * Ctree.ocalhd -> xml
13.22 + val pos_2xml : int -> Ctree.pos_ -> string
13.23 + val posform2xml : int -> Ctree.pos' * Term.term -> xml
13.24 + val posformhead2xml : int -> Ctree.pos' * Ctree.ptform -> string
13.25 + val posformheads2xml : int -> (Ctree.pos' * Ctree.ptform) list -> xml
13.26 + val posforms2xml : int -> (Ctree.pos' * Term.term) list -> xml
13.27 + val posterms2xml : int -> (Ctree.pos' * term) list -> xml
13.28 val precond2xml : int -> bool * Term.term -> xml
13.29 val preconds2xml : int -> (bool * Term.term) list -> xml
13.30 val rls2xml : int -> thyID * rls -> xml
13.31 @@ -45,10 +45,10 @@
13.32 val scr2xml : int -> scr -> xml
13.33 val spec2xml : int -> spec -> xml
13.34 val sub2xml : int -> Term.term * Term.term -> xml
13.35 - val subs2xml : int -> subs -> xml
13.36 + val subs2xml : int -> Ctree.subs -> xml
13.37 val subst2xml : int -> subst -> xml
13.38 - val tac2xml : int -> tac -> xml
13.39 - val tacs2xml : int -> tac list -> xml
13.40 + val tac2xml : int -> Ctree.tac -> xml
13.41 + val tacs2xml : int -> Ctree.tac list -> xml
13.42 val theref2xml : int -> thyID -> string -> xstring -> string
13.43 val thm'2xml : int -> thm' -> xml
13.44 val thm''2xml : int -> thm -> xml
13.45 @@ -319,8 +319,8 @@
13.46 fun xml_of_pos tag (is, pp) =
13.47 XML.Elem ((tag, []), [
13.48 xml_of_ints is,
13.49 - XML.Elem (("POS", []), [XML.Text (pos_2str pp)])])
13.50 -fun xml_to_pos_ (XML.Elem (("POS", []), [XML.Text pp])) = str2pos_ pp
13.51 + XML.Elem (("POS", []), [XML.Text (Ctree.pos_2str pp)])])
13.52 +fun xml_to_pos_ (XML.Elem (("POS", []), [XML.Text pp])) = Ctree.str2pos_ pp
13.53 | xml_to_pos_ tree = raise ERROR ("xml_to_pos_: wrong XML.tree \n" ^ xmlstr 0 tree)
13.54 fun xml_to_pos (XML.Elem (("POSITION", []), [is, pp])) = (xml_to_ints is, xml_to_pos_ pp) (*: pos'*)
13.55 | xml_to_pos tree = raise ERROR ("xml_to_pos: wrong XML.tree \n" ^ xmlstr 0 tree)
13.56 @@ -403,12 +403,12 @@
13.57 (xml_to_strs items, xml_to_spec spec)
13.58 | xml_to_variant tree = raise ERROR ("xml_to_variant: wrong XML.tree \n" ^ xmlstr 0 tree)
13.59
13.60 -fun xml_of_fmz [] = xml_of_fmz [e_fmz]
13.61 +fun xml_of_fmz [] = xml_of_fmz [Ctree.e_fmz]
13.62 | xml_of_fmz vs = XML.Elem (("FORMALIZATION", []), map xml_of_variant vs)
13.63 fun xml_to_fmz (XML.Elem (("FORMALIZATION", []), vars)) = map xml_to_variant vars
13.64 | xml_to_fmz tree = raise ERROR ("xml_to_fmz: wrong XML.tree \n" ^ xmlstr 0 tree)
13.65
13.66 -fun xml_of_modspec ((b, p_, head, gfr, pre, spec): ocalhd) =
13.67 +fun xml_of_modspec ((b, p_, head, gfr, pre, spec): Ctree.ocalhd) =
13.68 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
13.69 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
13.70 xml_of_model gfr pre,
13.71 @@ -416,7 +416,7 @@
13.72 XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
13.73 xml_of_spec spec])
13.74
13.75 -fun xml_of_posmodspec ((p: pos', (b, p_, head, gfr, pre, spec): ocalhd)) =
13.76 +fun xml_of_posmodspec ((p: Ctree.pos', (b, p_, head, gfr, pre, spec): Ctree.ocalhd)) =
13.77 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
13.78 xml_of_pos "POSITION" p,
13.79 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
13.80 @@ -442,7 +442,7 @@
13.81 XML.Elem (( "POS", []), [XML.Text belongsto]),
13.82 spec as XML.Elem (( "SPECIFICATION", []), _)])) =
13.83 (xml_to_pos pos, xml_to_term_NEW form |> term2str, xml_to_imodel imodel,
13.84 - str2pos_ belongsto, xml_to_spec spec) : Inform.icalhd
13.85 + Ctree.str2pos_ belongsto, xml_to_spec spec) : Inform.icalhd
13.86 | xml_to_icalhd x = raise ERROR ("xml_to_icalhd: WRONG arg = " ^ xmlstr 0 x)
13.87
13.88 fun xml_of_sub (id, value) =
13.89 @@ -454,17 +454,17 @@
13.90 XML.Elem (("VARIABLE", []), [id]),
13.91 XML.Elem (("VALUE", []), [value])])) = (xml_to_term id, xml_to_term value)
13.92 | xml_to_sub x = raise ERROR ("xml_to_sub wrong arg: " ^ xmlstr 0 x)
13.93 -fun xml_of_subs (subs : subs) =
13.94 - XML.Elem (("SUBSTITUTION", []), map xml_of_sub (subs2subst (assoc_thy "Isac") subs))
13.95 +fun xml_of_subs (subs : Ctree.subs) =
13.96 + XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Ctree.subs2subst (assoc_thy "Isac") subs))
13.97 fun xml_to_subs
13.98 (XML.Elem (("SUBSTITUTION", []),
13.99 - subs)) = (subst2subs (map xml_to_sub subs) : subs)
13.100 + subs)) = (Ctree.subst2subs (map xml_to_sub subs) : Ctree.subs)
13.101 | xml_to_subs x = raise ERROR ("xml_to_subs wrong arg: " ^ xmlstr 0 x)
13.102 -fun xml_of_sube (sube : sube) =
13.103 - XML.Elem (("SUBSTITUTION", []), map xml_of_sub (sube2subst (assoc_thy "Isac") sube))
13.104 +fun xml_of_sube (sube : Ctree.sube) =
13.105 + XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Ctree.sube2subst (assoc_thy "Isac") sube))
13.106 fun xml_to_sube
13.107 (XML.Elem (("SUBSTITUTION", []),
13.108 - xml_var_val_pairs)) = subst2sube (map xml_to_sub xml_var_val_pairs)
13.109 + xml_var_val_pairs)) = Ctree.subst2sube (map xml_to_sub xml_var_val_pairs)
13.110 | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
13.111
13.112 fun thm''2xml j (thm : thm) =
13.113 @@ -520,134 +520,134 @@
13.114 XML.Elem (("NOCODE", []), [XML.Text "reverse rewrite functions"])
13.115
13.116 (*.convert a tactic into xml-format .*)
13.117 -fun xml_of_tac (Subproblem (dI, pI)) =
13.118 +fun xml_of_tac (Ctree.Subproblem (dI, pI)) =
13.119 XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
13.120 XML.Elem (("THEORY", []), [XML.Text dI]),
13.121 XML.Elem (("PROBLEM", []), [xml_of_strs pI])])
13.122 - | xml_of_tac (Substitute cterms) =
13.123 + | xml_of_tac (Ctree.Substitute cterms) =
13.124 (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
13.125 XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
13.126 (*----- Rewrite* -----------------------------------------------------*)
13.127 - | xml_of_tac (Rewrite thm'') =
13.128 + | xml_of_tac (Ctree.Rewrite thm'') =
13.129 XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm'' thm''])
13.130 - | xml_of_tac (Rewrite_Inst (subs, thm'')) =
13.131 + | xml_of_tac (Ctree.Rewrite_Inst (subs, thm'')) =
13.132 XML.Elem (("REWRITEINSTTACTIC", [("name", "Rewrite_Inst")]), (
13.133 xml_of_subs subs ::
13.134 xml_of_thm'' thm'' :: []))
13.135 - | xml_of_tac (Rewrite_Set rls') =
13.136 + | xml_of_tac (Ctree.Rewrite_Set rls') =
13.137 XML.Elem (("REWRITESETTACTIC", [("name", "Rewrite_Set")]), [XML.Text rls'])
13.138 - | xml_of_tac (Rewrite_Set_Inst (subs, rls')) =
13.139 + | xml_of_tac (Ctree.Rewrite_Set_Inst (subs, rls')) =
13.140 XML.Elem (("REWRITESETINSTTACTIC", [("name", "Rewrite_Set_Inst")]), ([
13.141 xml_of_subs subs,
13.142 XML.Elem (("RULESET", []), [XML.Text rls'])]))
13.143 (*----- FORMTACTIC ---------------------------------------------------*)
13.144 - | xml_of_tac (Add_Find ct) =
13.145 + | xml_of_tac (Ctree.Add_Find ct) =
13.146 XML.Elem (("FORMTACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])
13.147 - | xml_of_tac (Add_Given ct) =
13.148 + | xml_of_tac (Ctree.Add_Given ct) =
13.149 XML.Elem (("FORMTACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])
13.150 - | xml_of_tac (Add_Relation ct) =
13.151 + | xml_of_tac (Ctree.Add_Relation ct) =
13.152 XML.Elem (("FORMTACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])
13.153 - | xml_of_tac (Check_elementwise ct) =
13.154 + | xml_of_tac (Ctree.Check_elementwise ct) =
13.155 XML.Elem (("FORMTACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])
13.156 - | xml_of_tac (Take ct) =
13.157 + | xml_of_tac (Ctree.Take ct) =
13.158 XML.Elem (("FORMTACTIC", [("name", "Take")]), [xml_of_cterm ct])
13.159 (*----- SIMPLETACTIC -------------------------------------------------*)
13.160 - | xml_of_tac (Calculate opstr) =
13.161 + | xml_of_tac (Ctree.Calculate opstr) =
13.162 XML.Elem (("SIMPLETACTIC", [("name", "Calculate")]), [XML.Text opstr])
13.163 - | xml_of_tac (Or_to_List) =
13.164 + | xml_of_tac (Ctree.Or_to_List) =
13.165 XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [(*//////////*)])
13.166 - | xml_of_tac (Specify_Theory ct) =
13.167 + | xml_of_tac (Ctree.Specify_Theory ct) =
13.168 XML.Elem (("SIMPLETACTIC", [("name", "Specify_Theory")]), [XML.Text ct])
13.169 (*----- STRINGLISTTACTIC ---------------------------------------------*)
13.170 - | xml_of_tac (Apply_Method mI) =
13.171 + | xml_of_tac (Ctree.Apply_Method mI) =
13.172 XML.Elem (("STRINGLISTTACTIC", [("name", "Apply_Method")]), [xml_of_strs mI])
13.173 - | xml_of_tac (Check_Postcond pI) =
13.174 + | xml_of_tac (Ctree.Check_Postcond pI) =
13.175 XML.Elem (("STRINGLISTTACTIC", [("name", "Check_Postcond")]), [xml_of_strs pI])
13.176 | xml_of_tac Model_Problem =
13.177 XML.Elem (("STRINGLISTTACTIC", [("name", "Model_Problem")]), [])
13.178 - | xml_of_tac (Refine_Tacitly pI) =
13.179 + | xml_of_tac (Ctree.Refine_Tacitly pI) =
13.180 XML.Elem (("STRINGLISTTACTIC", [("name", "Refine_Tacitly")]), [xml_of_strs pI])
13.181 - | xml_of_tac (Specify_Method ct) =
13.182 + | xml_of_tac (Ctree.Specify_Method ct) =
13.183 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct])
13.184 - | xml_of_tac (Specify_Problem ct) =
13.185 + | xml_of_tac (Ctree.Specify_Problem ct) =
13.186 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
13.187 - | xml_of_tac tac = raise ERROR ("xml_of_tac: not impl. for " ^ tac2str tac);
13.188 + | xml_of_tac tac = raise ERROR ("xml_of_tac: not impl. for " ^ Ctree.tac2str tac);
13.189
13.190 fun xml_to_tac
13.191 (XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
13.192 XML.Elem (("THEORY", []), [XML.Text dI]),
13.193 - XML.Elem (("PROBLEM", []), [pI])])) = Subproblem (dI, xml_to_strs pI)
13.194 + XML.Elem (("PROBLEM", []), [pI])])) = Ctree.Subproblem (dI, xml_to_strs pI)
13.195 | xml_to_tac
13.196 (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
13.197 (XML.Elem (("STRINGLISTTACTIC", [
13.198 - ("name", "Substitute")]), [cterms])) = Substitute (xml_to_sube cterms)
13.199 + ("name", "Substitute")]), [cterms])) = Ctree.Substitute (xml_to_sube cterms)
13.200 (*----- Rewrite* -----------------------------------------------------*)
13.201 | xml_to_tac
13.202 (XML.Elem (("REWRITETACTIC", [
13.203 - ("name", "Rewrite")]), [thm])) = Rewrite (xml_to_thm'' thm)
13.204 + ("name", "Rewrite")]), [thm])) = Ctree.Rewrite (xml_to_thm'' thm)
13.205 | xml_to_tac
13.206 (XML.Elem (("REWRITEINSTTACTIC", [
13.207 ("name", "Rewrite_Inst")]), [
13.208 - subs, thm])) = Rewrite_Inst (xml_to_subs subs, xml_to_thm'' thm)
13.209 + subs, thm])) = Ctree.Rewrite_Inst (xml_to_subs subs, xml_to_thm'' thm)
13.210 | xml_to_tac
13.211 (XML.Elem (("REWRITESETTACTIC", [
13.212 - ("name", "Rewrite_Set")]), [XML.Text rls'])) = Rewrite_Set (rls')
13.213 + ("name", "Rewrite_Set")]), [XML.Text rls'])) = Ctree.Rewrite_Set (rls')
13.214 | xml_to_tac
13.215 (XML.Elem (("REWRITESETINSTTACTIC", [
13.216 ("name", "Rewrite_Set_Inst")]), [
13.217 subs,
13.218 - XML.Elem (("RULESET", []), [XML.Text rls'])])) = Rewrite_Set_Inst (xml_to_subs subs, rls')
13.219 + XML.Elem (("RULESET", []), [XML.Text rls'])])) = Ctree.Rewrite_Set_Inst (xml_to_subs subs, rls')
13.220 (*----- FORMTACTIC ---------------------------------------------------*)
13.221 | xml_to_tac
13.222 (XML.Elem (("FORMTACTIC", [
13.223 - ("name", "Add_Find")]), [ct])) = Add_Find (xml_to_cterm ct)
13.224 + ("name", "Add_Find")]), [ct])) = Ctree.Add_Find (xml_to_cterm ct)
13.225 | xml_to_tac
13.226 (XML.Elem (("FORMTACTIC", [
13.227 - ("name", "Add_Given")]), [ct])) = Add_Given (xml_to_cterm ct)
13.228 + ("name", "Add_Given")]), [ct])) = Ctree.Add_Given (xml_to_cterm ct)
13.229 | xml_to_tac
13.230 (XML.Elem (("FORMTACTIC", [
13.231 - ("name", "Add_Relation")]), [ct])) = Add_Relation (xml_to_cterm ct)
13.232 + ("name", "Add_Relation")]), [ct])) = Ctree.Add_Relation (xml_to_cterm ct)
13.233 | xml_to_tac
13.234 (XML.Elem (("FORMTACTIC", [
13.235 - ("name", "Take")]), [ct])) = Take (xml_to_cterm ct)
13.236 + ("name", "Take")]), [ct])) = Ctree.Take (xml_to_cterm ct)
13.237 | xml_to_tac
13.238 (XML.Elem (("FORMTACTIC", [
13.239 - ("name", "Check_elementwise")]), [ct])) = Check_elementwise (xml_to_cterm ct)
13.240 + ("name", "Check_elementwise")]), [ct])) = Ctree.Check_elementwise (xml_to_cterm ct)
13.241 (*----- SIMPLETACTIC -------------------------------------------------*)
13.242 | xml_to_tac
13.243 (XML.Elem (("SIMPLETACTIC", [
13.244 - ("name", "Calculate")]), [XML.Text opstr])) = Calculate opstr
13.245 + ("name", "Calculate")]), [XML.Text opstr])) = Ctree.Calculate opstr
13.246 | xml_to_tac
13.247 - (XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [])) = Or_to_List
13.248 + (XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [])) = Ctree.Or_to_List
13.249 | xml_to_tac
13.250 (XML.Elem (("SIMPLETACTIC", [
13.251 - ("name", "Specify_Theory")]), [XML.Text ct])) = Specify_Theory ct
13.252 + ("name", "Specify_Theory")]), [XML.Text ct])) = Ctree.Specify_Theory ct
13.253 (*----- STRINGLISTTACTIC ---------------------------------------------*)
13.254 | xml_to_tac
13.255 (XML.Elem (("STRINGLISTTACTIC", [
13.256 - ("name", "Apply_Method")]), [mI])) = Apply_Method (xml_to_strs mI)
13.257 + ("name", "Apply_Method")]), [mI])) = Ctree.Apply_Method (xml_to_strs mI)
13.258 | xml_to_tac
13.259 (XML.Elem (("STRINGLISTTACTIC", [
13.260 - ("name", "Check_Postcond")]), [pI])) = Check_Postcond (xml_to_strs pI)
13.261 + ("name", "Check_Postcond")]), [pI])) = Ctree.Check_Postcond (xml_to_strs pI)
13.262 | xml_to_tac
13.263 (XML.Elem (("STRINGLISTTACTIC", [
13.264 - ("name", "Model_Problem")]), [])) = Model_Problem
13.265 + ("name", "Model_Problem")]), [])) = Ctree.Model_Problem
13.266 | xml_to_tac
13.267 (XML.Elem (("STRINGLISTTACTIC", [
13.268 - ("name", "Refine_Tacitly")]), [pI])) = Refine_Tacitly (xml_to_strs pI)
13.269 + ("name", "Refine_Tacitly")]), [pI])) = Ctree.Refine_Tacitly (xml_to_strs pI)
13.270 | xml_to_tac
13.271 (XML.Elem (("STRINGLISTTACTIC", [
13.272 - ("name", "Specify_Method")]), [ct])) = Specify_Method (xml_to_strs ct)
13.273 + ("name", "Specify_Method")]), [ct])) = Ctree.Specify_Method (xml_to_strs ct)
13.274 | xml_to_tac
13.275 (XML.Elem (("STRINGLISTTACTIC", [
13.276 - ("name", "Specify_Problem")]), [ct])) = Specify_Problem (xml_to_strs ct)
13.277 + ("name", "Specify_Problem")]), [ct])) = Ctree.Specify_Problem (xml_to_strs ct)
13.278 | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);
13.279
13.280 val e_pblterm = (Thm.term_of o the o (parse @{theory Script}))
13.281 ("Problem (" ^ e_domID ^ "," ^ strs2str' e_pblID ^ ")");
13.282
13.283 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
13.284 -fun xml_of_posterm ((p : pos'), t) =
13.285 +fun xml_of_posterm ((p : Ctree.pos'), t) =
13.286 let val input_request = Free ("________________________________________________", dummyT)
13.287 in
13.288 XML.Elem (("CALCFORMULA", []),
14.1 --- a/src/Tools/isac/xmlsrc/interface-xml.sml Wed Dec 21 11:27:22 2016 +0100
14.2 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml Thu Dec 22 10:25:49 2016 +0100
14.3 @@ -27,7 +27,7 @@
14.4 XML.Elem (("DELCALC", []),
14.5 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)])])
14.6
14.7 -fun iteratorOK2xml (calcid : calcID) (p : pos')=
14.8 +fun iteratorOK2xml (calcid : calcID) (p : Ctree.pos')=
14.9 XML.Elem (("CALCITERATOR", []),
14.10 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
14.11 xml_of_pos "POSITION" p])
14.12 @@ -41,13 +41,13 @@
14.13 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
14.14 XML.Elem (("ERROR", []), [XML.Text (if str = "" then " ERROR in kernel " else str)])])
14.15
14.16 -fun refformulaOK2xml (calcid : calcID) p (Form t) =
14.17 +fun refformulaOK2xml (calcid : calcID) p (Ctree.Form t) =
14.18 XML.Elem (("REFFORMULA", []),
14.19 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
14.20 XML.Elem (("CALCFORMULA", []), [
14.21 xml_of_pos "POSITION" p,
14.22 xml_of_term_NEW t])])
14.23 - | refformulaOK2xml (calcid : calcID) p (ModSpec modspec) =
14.24 + | refformulaOK2xml (calcid : calcID) p (Ctree.ModSpec modspec) =
14.25 XML.Elem (("REFFORMULA", []), [
14.26 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
14.27 (*L.Elem (("CALCHEAD*) xml_of_posmodspec (p, modspec)])
14.28 @@ -100,14 +100,14 @@
14.29 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
14.30 XML.Elem (("FORMHEADS", []), map xml_of_posterm fs)])
14.31
14.32 -fun appendformulaOK2xml (calcid : calcID) (old : pos') (del : pos') (new : pos') =
14.33 +fun appendformulaOK2xml (calcid : calcID) (old : Ctree.pos') (del : Ctree.pos') (new : Ctree.pos') =
14.34 xml_of_calcchanged calcid "APPENDFORMULA" old del new
14.35 fun appendformulaERROR2xml (calcid : calcID) e =
14.36 XML.Elem (("APPENDFORMULA", []), [
14.37 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
14.38 XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
14.39
14.40 -fun replaceformulaOK2xml (calcid : calcID) (old : pos') (del : pos') (new : pos') =
14.41 +fun replaceformulaOK2xml (calcid : calcID) (old : Ctree.pos') (del : Ctree.pos') (new : Ctree.pos') =
14.42 xml_of_calcchanged calcid "REPLACEFORMULA" old del new
14.43 fun replaceformulaERROR2xml (calcid : calcID) e =
14.44 XML.Elem (("REPLACEFORMULA", []), [
14.45 @@ -139,14 +139,14 @@
14.46 DELETED: last pos' of the succesional sequence of formulae prob. deleted
14.47 GENERATED: the pos' of the new active formula
14.48 .*)
14.49 -fun autocalculateOK2xml (calcid : calcID) (old : pos') (del : pos') (new : pos') =
14.50 +fun autocalculateOK2xml (calcid : calcID) (old : Ctree.pos') (del : Ctree.pos') (new : Ctree.pos') =
14.51 xml_of_calcchanged calcid "AUTOCALC" old del new
14.52 fun autocalculateERROR2xml (calcid : calcID) e =
14.53 XML.Elem (("AUTOCALC", []), [
14.54 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
14.55 XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
14.56
14.57 -fun interStepsOK (calcid : calcID) (old : pos') (del : pos') (new : pos') =
14.58 +fun interStepsOK (calcid : calcID) (old : Ctree.pos') (del : Ctree.pos') (new : Ctree.pos') =
14.59 xml_of_calcchanged calcid "INTERSTEPS" old del new
14.60 fun interStepsERROR (calcid : calcID) e =
14.61 XML.Elem (("INTERSTEPS", []), [
14.62 @@ -158,7 +158,7 @@
14.63 " <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
14.64 "@@@@@end@@@@@");
14.65
14.66 -fun modifycalcheadOK2xml (calcid : calcID) (chd as (complete, p_ ,_ ,_ ,_ ,_) : ocalhd) =
14.67 +fun modifycalcheadOK2xml (calcid : calcID) (chd as (complete, p_ ,_ ,_ ,_ ,_) : Ctree.ocalhd) =
14.68 XML.Elem (("MODIFYCALCHEAD", []), [
14.69 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
14.70 XML.Elem (("STATUS", []), [
15.1 --- a/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Wed Dec 21 11:27:22 2016 +0100
15.2 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Thu Dec 22 10:25:49 2016 +0100
15.3 @@ -34,51 +34,51 @@
15.4 fun hierarchy pm(*"pbl" | "met"*) h =
15.5 let val j = indentation
15.6 fun nd i p (Ptyp (id,_,ns)) =
15.7 - let val p' = lev_on p
15.8 + let val p' = Ctree.lev_on p
15.9 in (indt i) ^ "<NODE>\n" ^
15.10 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
15.11 (indt (i+j)) ^ "<NO> " (*on this level*) ^
15.12 (string_of_int o last_elem) p' ^ " </NO>\n" ^
15.13 (indt (i+j)) ^ "<CONTENTREF> " ^ pm ^ pos2filename p' ^
15.14 " </CONTENTREF>\n" ^
15.15 - (nds (i+j) (lev_dn p') ns) ^
15.16 + (nds (i+j) (Ctree.lev_dn p') ns) ^
15.17 (indt i) ^ "</NODE>\n"
15.18 end
15.19 and nds _ _ [] = ""
15.20 - | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns);
15.21 + | nds i p (n::ns) = (nd i p n) ^ (nds i (Ctree.lev_on p) ns);
15.22 in nds j [0] h end;
15.23 (*.create a hierarchy with references to the guh's.*)
15.24 fun hierarchy_pbl h =
15.25 let val j = indentation
15.26 fun nd i p (Ptyp (id,[n as {guh,...} : pbt],ns)) =
15.27 - let val p' = lev_on p
15.28 + let val p' = Ctree.lev_on p
15.29 in (indt i) ^ "<NODE>\n" ^
15.30 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
15.31 (indt (i+j)) ^ "<NO> " (*on this level*) ^
15.32 (string_of_int o last_elem) p' ^ " </NO>\n" ^
15.33 (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^
15.34 " </CONTENTREF>\n" ^
15.35 - (nds (i+j) (lev_dn p') ns) ^
15.36 + (nds (i+j) (Ctree.lev_dn p') ns) ^
15.37 (indt i) ^ "</NODE>\n"
15.38 end
15.39 and nds _ _ [] = ""
15.40 - | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns);
15.41 + | nds i p (n::ns) = (nd i p n) ^ (nds i (Ctree.lev_on p) ns);
15.42 in nds j [0] h : xml end;
15.43 fun hierarchy_met h =
15.44 let val j = indentation
15.45 fun nd i p (Ptyp (id,[n as {guh,...} : met],ns)) =
15.46 - let val p' = lev_on p
15.47 + let val p' = Ctree.lev_on p
15.48 in (indt i) ^ "<NODE>\n" ^
15.49 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
15.50 (indt (i+j)) ^ "<NO> " (*on this level*) ^
15.51 (string_of_int o last_elem) p' ^ " </NO>\n" ^
15.52 (indt (i+j)) ^ "<CONTENTREF> " ^ guh ^
15.53 " </CONTENTREF>\n" ^
15.54 - (nds (i+j) (lev_dn p') ns) ^
15.55 + (nds (i+j) (Ctree.lev_dn p') ns) ^
15.56 (indt i) ^ "</NODE>\n"
15.57 end
15.58 and nds _ _ [] = ""
15.59 - | nds i p (n::ns) = (nd i p n) ^ (nds i (lev_on p) ns);
15.60 + | nds i p (n::ns) = (nd i p n) ^ (nds i (Ctree.lev_on p) ns);
15.61 in nds j [0] h : xml end;
15.62 (* (writeln o hierarchy_pbl) (!ptyps);
15.63 *)
15.64 @@ -181,8 +181,8 @@
15.65
15.66
15.67 (**. write pbls from hierarchy to files.**)
15.68 -fun pbl2file (path:path) (pos:pos) (id:metID) (pbl as {guh,...}) =
15.69 - (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ pos2str pos);
15.70 +fun pbl2file (path:path) (pos: Ctree.pos) (id:metID) (pbl as {guh,...}) =
15.71 + (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ Ctree.pos2str pos);
15.72 ((str2file (path ^ Rtools.guh2filename guh)) o (pbl2xml id)) pbl
15.73 );
15.74
15.75 @@ -254,25 +254,25 @@
15.76 *)
15.77
15.78 (*.write the files using an int-key (pos') as filename.*)
15.79 -fun met2file (path:path) (pos:pos) (id:metID) met =
15.80 +fun met2file (path:path) (pos: Ctree.pos) (id:metID) met =
15.81 (writeln ("### met2file: id = " ^ strs2str id);
15.82 ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met);
15.83
15.84 (*.write the files using the guh as filename.*)
15.85 -fun met2file (path:path) (pos:pos) (id:metID) (met as {guh,...}) =
15.86 +fun met2file (path:path) (pos: Ctree.pos) (id:metID) (met as {guh,...}) =
15.87 (writeln ("### met2file: id = " ^ strs2str id);
15.88 ((str2file (path ^ Rtools.guh2filename guh)) o (met2xml id)) met);
15.89
15.90 (*.scan the mtree Ptyp and print the nodes using wfn.*)
15.91 fun node (pa:path) ids po wfn (Ptyp (id,[n],ns)) =
15.92 - let val po' = lev_on po
15.93 + let val po' = Ctree.lev_on po
15.94 in
15.95 wfn pa po' (ids@[id]) n;
15.96 - nodes pa (ids@[id]) ((lev_dn po'):pos) wfn ns
15.97 + nodes pa (ids@[id]) (Ctree.lev_dn po') wfn ns
15.98 end
15.99 and nodes _ _ _ _ [] = ()
15.100 | nodes pa ids po wfn (n::ns) =
15.101 - (node pa ids po wfn n; nodes pa ids (lev_on po) wfn ns);
15.102 + (node pa ids po wfn n; nodes pa ids (Ctree.lev_on po) wfn ns);
15.103
15.104 fun pbls2file (p:path) = nodes p [] [0] pbl2file (get_ptyps ());
15.105 fun mets2file (p:path) = nodes p [] [0] met2file (get_mets ());
16.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml Wed Dec 21 11:27:22 2016 +0100
16.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml Thu Dec 22 10:25:49 2016 +0100
16.3 @@ -95,18 +95,18 @@
16.4 val j = indentation
16.5 fun node i p theID (Ptyp (id, _, ns)) =
16.6 let
16.7 - val p' = lev_on p
16.8 + val p' = Ctree.lev_on p
16.9 val theID' = theID @ [id]
16.10 in
16.11 (indt i) ^ "<NODE>\n" ^
16.12 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
16.13 (indt (i+j)) ^ "<NO> " (*on this level*) ^ (string_of_int o last_elem) p' ^ " </NO>\n" ^
16.14 (indt (i+j)) ^ "<CONTENTREF> " ^ theID2guh theID' ^ " </CONTENTREF>\n" ^
16.15 - (nodes (i+j) (lev_dn p') theID' ns) ^
16.16 + (nodes (i+j) (Ctree.lev_dn p') theID' ns) ^
16.17 (indt i) ^ "</NODE>\n"
16.18 end
16.19 and nodes _ _ _ [] = ""
16.20 - | nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (lev_on p) theID ns);
16.21 + | nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (Ctree.lev_on p) theID ns);
16.22 in nodes j [0] [] h end;
16.23
16.24 fun thy_hierarchy2file (path:path) =
16.25 @@ -165,17 +165,17 @@
16.26 error ("thydata2xml: not implemented for "^ strs2str' theID);
16.27
16.28 (* analoguous to 'fun met2file' *)
16.29 -fun thydata2file (path : path) (pos : pos) (theID : theID) thydata =
16.30 +fun thydata2file (path : path) (pos : Ctree.pos) (theID : theID) thydata =
16.31 (writeln ("### thes2file: id = " ^ strs2str theID);
16.32 str2file (path ^ Rtools.theID2filename theID) (thydata2xml (theID, thydata)));
16.33
16.34 (* analoguous to 'fun node' *)
16.35 fun thenode (pa : path) ids po wfn (Ptyp (id, [n], ns)) =
16.36 - let val po' = lev_on po
16.37 - in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns end
16.38 + let val po' = Ctree.lev_on po
16.39 + in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) (Ctree.lev_dn po') wfn ns end
16.40 and thenodes _ _ _ _ [] = ()
16.41 | thenodes pa ids po wfn (n::ns) =
16.42 - (thenode pa ids po wfn n; thenodes pa ids (lev_on po) wfn ns);
16.43 + (thenode pa ids po wfn n; thenodes pa ids (Ctree.lev_on po) wfn ns);
16.44
16.45 (* analoguous to 'fun mets2file' *)
16.46 fun thes2file (p : path) = thenodes p [] [0] thydata2file (get_thes ());
17.1 --- a/src/Tools/isac/xmlsrc/xmlsrc.thy Wed Dec 21 11:27:22 2016 +0100
17.2 +++ b/src/Tools/isac/xmlsrc/xmlsrc.thy Thu Dec 22 10:25:49 2016 +0100
17.3 @@ -13,7 +13,7 @@
17.4 ML_file "~~/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml"
17.5 ML_file "~~/src/Tools/isac/xmlsrc/thy-hierarchy.sml"
17.6 ML_file "~~/src/Tools/isac/xmlsrc/interface-xml.sml"
17.7 -
17.8 +(*declare [[ML_print_depth = 999]]*)
17.9 ML {*
17.10 *} ML {*
17.11 *}
18.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Wed Dec 21 11:27:22 2016 +0100
18.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Thu Dec 22 10:25:49 2016 +0100
18.3 @@ -24,7 +24,7 @@
18.4 for further input *}
18.5
18.6 ML {*
18.7 - val ctxt = get_ctxt pt p;
18.8 + val ctxt = Ctree.get_ctxt pt p;
18.9 val SOME known_x = parseNEW ctxt "x + y + z";
18.10 val SOME unknown = parseNEW ctxt "a + b + c";
18.11 if type_of known_x = HOLogic.realT andalso
18.12 @@ -47,7 +47,7 @@
18.13 text {* preconditions are known at start of interpretation of (root-)method *}
18.14
18.15 ML {*
18.16 - if terms2strs (get_assumptions_ pt p) = ["precond_rootmet x"]
18.17 + if terms2strs (Ctree.get_assumptions_ pt p) = ["precond_rootmet x"]
18.18 then () else error "All_Ctx: asms after start interpretation of root-method";
18.19 *}
18.20
18.21 @@ -63,7 +63,7 @@
18.22 and extended with the types of the variables in args. *}
18.23
18.24 ML {* (*not significant in this example*)
18.25 - val ctxt = get_ctxt pt p;
18.26 + val ctxt = Ctree.get_ctxt pt p;
18.27 val SOME known_x = parseNEW ctxt "x+y+z";
18.28 val SOME unknown = parseNEW ctxt "a+b+c";
18.29 if type_of known_x = HOLogic.realT andalso
18.30 @@ -87,7 +87,7 @@
18.31 text {* preconds are known at start of interpretation of (sub-)method *}
18.32
18.33 ML {*
18.34 - if terms2strs (get_assumptions_ pt p) = ["matches (?a = ?b) (-1 + x = 0)"]
18.35 + if terms2strs (Ctree.get_assumptions_ pt p) = ["matches (?a = ?b) (-1 + x = 0)"]
18.36 then () else error "All_Ctx: asms after start interpretation of SubProblem";
18.37 *}
18.38
18.39 @@ -97,7 +97,7 @@
18.40
18.41 ML {*
18.42 "artifically inject assumptions";
18.43 - val (SOME (iform, cform), SOME (ires, cres)) = get_obj g_loc pt (fst p);
18.44 + val (SOME (iform, cform), SOME (ires, cres)) = Ctree.get_obj Ctree.g_loc pt (fst p);
18.45 val ctxt = insert_assumptions [str2term "x < sub_asm_out",
18.46 str2term "a < sub_asm_local"] cres;
18.47 val pt = Ctree.update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
18.48 @@ -130,7 +130,7 @@
18.49 text {* assumptions collected during lucas-interpretation for proof of postcondition *}
18.50
18.51 ML {*
18.52 - if terms2strs (get_assumptions_ pt p) =
18.53 + if terms2strs (Ctree.get_assumptions_ pt p) =
18.54 ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
18.55 then () else error "All_Ctx at final result";
18.56 *}
19.1 --- a/test/Tools/isac/Test_Isac.thy Wed Dec 21 11:27:22 2016 +0100
19.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Dec 22 10:25:49 2016 +0100
19.3 @@ -76,7 +76,7 @@
19.4 open Rtools; trtas2str;
19.5 open Chead; pt_extract;
19.6 open Generate; (*NONE*)
19.7 -(*open Ctree; (*? ?*) *)
19.8 + open Ctree; append_problem;
19.9 open Specify; show_ptyps;
19.10 open Applicable; (*TODO*)
19.11 open Solve; (*TODO*)
20.1 --- a/test/Tools/isac/Test_Some.thy Wed Dec 21 11:27:22 2016 +0100
20.2 +++ b/test/Tools/isac/Test_Some.thy Thu Dec 22 10:25:49 2016 +0100
20.3 @@ -10,7 +10,7 @@
20.4 open Rtools; trtas2str;
20.5 open Chead; pt_extract;
20.6 open Generate; (*NONE*)
20.7 -(*open Ctree; (*? ?*) *)
20.8 + open Ctree; append_problem;
20.9 open Specify; show_ptyps;
20.10 open Applicable; (*TODO*)
20.11 open Solve; (*TODO*)