1.1 --- a/src/Tools/isac/Interpret/mathengine.sml Wed Nov 30 13:05:08 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Mon Dec 12 18:08:13 2016 +0100
1.3 @@ -14,7 +14,7 @@
1.4 pos' list -> pos' -> (ptree * pos') * taci list -> auto -> string * pos' list * (ptree * pos')
1.5 val locatetac :
1.6 tac -> ptree * (posel list * pos_) -> string * (taci list * pos' list * (ptree * pos'))
1.7 - val step : pos' -> calcstate -> string * calcstate'
1.8 + val step : pos' -> Chead.calcstate -> string * Chead.calcstate'
1.9 val detailstep :
1.10 ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option
1.11
1.12 @@ -54,13 +54,13 @@
1.13 (* introduced for test only *)
1.14 val e_tac_ = Tac_ (Pure.thy, "", "", "");
1.15 datatype lOc_ =
1.16 - ERror of string (*after loc_specify, loc_solve*)
1.17 -| UNsafe of calcstate' (*after loc_specify, loc_solve*)
1.18 -| Updated of calcstate'; (*after loc_specify, loc_solve*)
1.19 + ERror of string (*after loc_specify, loc_solve*)
1.20 +| UNsafe of Chead.calcstate' (*after loc_specify, loc_solve*)
1.21 +| Updated of Chead.calcstate' (*after loc_specify, loc_solve*)
1.22
1.23 fun loc_specify_ m (pt,pos) =
1.24 let
1.25 - val (p, _, f, _, _, pt) = specify m pos [] pt;
1.26 + val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
1.27 in
1.28 case f of (Error' (Error_ e)) => ERror e | _ => Updated ([], [], (pt,p))
1.29 end
1.30 @@ -75,7 +75,7 @@
1.31
1.32 datatype nxt_ =
1.33 HElpless (**)
1.34 -| Nexts of calcstate; (**)
1.35 +| Nexts of Chead.calcstate (**)
1.36
1.37 (* locate a tactic in a script and apply it if possible;
1.38 report of tacs' applicability in tacis; pt is dropped in setNextTactic*)
1.39 @@ -85,8 +85,8 @@
1.40 val (mI, m) = mk_tac'_ tac;
1.41 in
1.42 case applicable_in p pt m of
1.43 - Notappl _ => ("not-applicable", ([],[], ptp):calcstate')
1.44 - | Appl m =>
1.45 + Chead.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
1.46 + | Chead.Appl m =>
1.47 let
1.48 val x = if member op = specsteps mI
1.49 then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
1.50 @@ -114,8 +114,8 @@
1.51 if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
1.52 then
1.53 case mI' of
1.54 - ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
1.55 - | _ => nxt_specif Model_Problem (pt, (p,Pbl))
1.56 + ["no_met"] => Chead.nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
1.57 + | _ => Chead.nxt_specif Model_Problem (pt, (p,Pbl))
1.58 else
1.59 let
1.60 val cpI = if pI = e_pblID then pI' else pI;
1.61 @@ -125,12 +125,12 @@
1.62 val pb = foldl and_ (true, map fst pre);
1.63 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
1.64 val (_, tac) =
1.65 - nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
1.66 + Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
1.67 in
1.68 case tac of
1.69 Apply_Method mI =>
1.70 nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
1.71 - | _ => nxt_specif tac ptp
1.72 + | _ => Chead.nxt_specif tac ptp
1.73 end
1.74 end
1.75
1.76 @@ -138,7 +138,7 @@
1.77 fun set_method (mI:metID) ptp =
1.78 let
1.79 val (mits, pt, p) =
1.80 - case nxt_specif (Specify_Method mI) ptp of
1.81 + case Chead.nxt_specif (Specify_Method mI) ptp of
1.82 ([(_, Specify_Method' (_, _, mits), _)], [], (pt, (p,_))) => (mits, pt, p)
1.83 | _ => error "set_method: case 1 uncovered"
1.84 val pre = [] (*...from Specify_Method'*)
1.85 @@ -156,7 +156,7 @@
1.86 fun set_problem pI (ptp: ptree * pos') =
1.87 let
1.88 val (complete, pits, pre, pt, p) =
1.89 - case nxt_specif (Specify_Problem pI) ptp of
1.90 + case Chead.nxt_specif (Specify_Problem pI) ptp of
1.91 ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_)))
1.92 => (complete, pits, pre, pt, p)
1.93 | _ => error "set_problem: case 1 uncovered"
1.94 @@ -172,7 +172,7 @@
1.95 fun set_theory (tI:thyID) (ptp: ptree * pos') =
1.96 let
1.97 val (complete, pits, pre, pt, p) =
1.98 - case nxt_specif (Specify_Theory tI) ptp of
1.99 + case Chead.nxt_specif (Specify_Theory tI) ptp of
1.100 ([(_, Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _)))
1.101 => (complete, pits, pre, pt, p)
1.102 | _ => error "set_theory: case 1 uncovered"
1.103 @@ -185,11 +185,11 @@
1.104
1.105 (* does a step forward; returns tactic used, ctree updated.
1.106 TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
1.107 -fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
1.108 +fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis): Chead.calcstate) =
1.109 let val pIopt = get_pblID (pt,ip);
1.110 in
1.111 if ip = ([],Res)
1.112 - then ("end-of-calculation", (tacis, [], ptp):calcstate')
1.113 + then ("end-of-calculation", (tacis, [], ptp): Chead.calcstate')
1.114 else
1.115 case tacis of
1.116 (_::_) =>
1.117 @@ -236,29 +236,29 @@
1.118 | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto =
1.119 if autoord auto > 3 andalso just_created (pt, pos)
1.120 then
1.121 - let val ptp = all_modspec (pt, pos);
1.122 + let val ptp = Chead.all_modspec (pt, pos);
1.123 in all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
1.124 else
1.125 if member op = [Pbl, Met] p_
1.126 then
1.127 - if not (is_complete_mod (pt, pos))
1.128 + if not (Chead.is_complete_mod (pt, pos))
1.129 then
1.130 - let val ptp = complete_mod (pt, pos) (*... auto = 2 | 3 *)
1.131 + let val ptp = Chead.complete_mod (pt, pos) (*... auto = 2 | 3 *)
1.132 in
1.133 if autoord auto < 3 then ("ok", c, ptp)
1.134 else
1.135 - if not (is_complete_spec ptp)
1.136 + if not (Chead.is_complete_spec ptp)
1.137 then
1.138 - let val ptp = complete_spec ptp
1.139 + let val ptp = Chead.complete_spec ptp
1.140 in
1.141 if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
1.142 end
1.143 else if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
1.144 end
1.145 else
1.146 - if not (is_complete_spec (pt,pos))
1.147 + if not (Chead.is_complete_spec (pt,pos))
1.148 then
1.149 - let val ptp = complete_spec (pt, pos)
1.150 + let val ptp = Chead.complete_spec (pt, pos)
1.151 in
1.152 if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
1.153 end
1.154 @@ -365,7 +365,7 @@
1.155 delete as soon as TESTg_form -> _mout_ dropped *)
1.156 fun TESTg_form ptp =
1.157 let
1.158 - val (form, _, _) = pt_extract ptp
1.159 + val (form, _, _) = Chead.pt_extract ptp
1.160 in
1.161 case form of
1.162 Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
1.163 @@ -379,7 +379,7 @@
1.164 compare "fun CalcTree" which DOES decode *)
1.165 fun CalcTreeTEST [(fmz, sp)] =
1.166 let
1.167 - val ((pt, p), tacis) = nxt_specify_init_calc (fmz, sp)
1.168 + val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)
1.169 val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
1.170 val f = TESTg_form (pt,p)
1.171 in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end