1.1 --- a/src/Tools/isac/Build_Isac.thy Tue Nov 22 10:42:21 2016 +0100
1.2 +++ b/src/Tools/isac/Build_Isac.thy Thu Nov 24 14:33:42 2016 +0100
1.3 @@ -71,6 +71,7 @@
1.4
1.5 section {*check presence of definitions from directories*}
1.6
1.7 +declare [[ML_print_depth = 999]]
1.8 ML {*
1.9 *} ML {*
1.10 *}
2.1 --- a/src/Tools/isac/Frontend/interface.sml Tue Nov 22 10:42:21 2016 +0100
2.2 +++ b/src/Tools/isac/Frontend/interface.sml Thu Nov 24 14:33:42 2016 +0100
2.3 @@ -31,7 +31,7 @@
2.4 val Iterator : calcID -> XML.tree
2.5 val IteratorTEST : calcID -> iterID
2.6 val modelProblem : calcID -> XML.tree
2.7 - val modifyCalcHead : calcID -> icalhd -> XML.tree
2.8 + val modifyCalcHead : calcID -> Inform.icalhd -> XML.tree
2.9 val moveActiveCalcHead : calcID -> XML.tree
2.10 val moveActiveDown : calcID -> XML.tree
2.11 val moveActiveFormula : calcID -> pos' -> XML.tree
2.12 @@ -70,13 +70,13 @@
2.13 encode "^" ---> "^^^"; see Knowledge/Atools.thy;
2.14 called for each cterm', icalhd, fmz in this interface;
2.15 + see "fun en/decode" in xmlsrc/mathml.sml *)
2.16 -fun encode_imodel (imodel:imodel) =
2.17 - let fun enc (Given ifos) = Given (map encode ifos)
2.18 - | enc (Find ifos) = Find (map encode ifos)
2.19 - | enc (Relate ifos) = Relate (map encode ifos)
2.20 - in map enc imodel:imodel end;
2.21 -fun encode_icalhd ((pos', headl, imodel, pos_, spec):icalhd) =
2.22 - (pos', encode headl, encode_imodel imodel, pos_, spec):icalhd;
2.23 +fun encode_imodel (imodel : Inform.imodel) =
2.24 + let fun enc (Inform.Given ifos) = Inform.Given (map encode ifos)
2.25 + | enc (Inform.Find ifos) = Inform.Find (map encode ifos)
2.26 + | enc (Inform.Relate ifos) = Inform.Relate (map encode ifos)
2.27 + in map enc imodel:Inform.imodel end;
2.28 +fun encode_icalhd ((pos', headl, imodel, pos_, spec) : Inform.icalhd) =
2.29 + (pos', encode headl, encode_imodel imodel, pos_, spec) : Inform.icalhd;
2.30 fun encode_fmz ((ifos, spec) : fmz) = (map encode ifos, spec) : fmz;
2.31
2.32
2.33 @@ -162,7 +162,7 @@
2.34 let
2.35 val _= upd_tacis cI tacis
2.36 val (tac, _, _) = last_elem tacis
2.37 - in fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac) end
2.38 + in fetchproposedtacticOK2xml cI tac (Inform.fetchErrorpatterns tac) end
2.39 | ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"
2.40 | ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
2.41 | ("end-of-calculation", _) =>
2.42 @@ -281,10 +281,10 @@
2.43 end)
2.44 handle _ => sysERROR2xml cI "error in kernel 8";
2.45
2.46 -fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_):icalhd) =
2.47 +fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : Inform.icalhd) =
2.48 (let
2.49 val ((pt,_),_) = get_calc cI
2.50 - val (pt, chd as (_,p_,_,_,_,_)) = input_icalhd pt ichd
2.51 + val (pt, chd as (_,p_,_,_,_,_)) = Inform.input_icalhd pt ichd
2.52 in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end)
2.53 handle _ => sysERROR2xml cI "error in kernel 9";
2.54
2.55 @@ -439,7 +439,7 @@
2.56 in
2.57 case Math_Engine.step pos cs of
2.58 ("ok", cs') =>
2.59 - (case inform cs' (encode ifo) of
2.60 + (case Inform.inform cs' (encode ifo) of
2.61 ("ok", (_(*use in DG !!!*), c, ptp as (_, p))) =>
2.62 (upd_calc cI (ptp, []); upd_ipos cI 1 p;
2.63 appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
2.64 @@ -459,7 +459,7 @@
2.65 val ((pt, _), _) = get_calc cI
2.66 val p = get_pos cI 1
2.67 in
2.68 - case inform (([], [], (pt, p)): calcstate') (encode ifo) of
2.69 + case Inform.inform (([], [], (pt, p)): calcstate') (encode ifo) of
2.70 ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) =>
2.71 let
2.72 val unc = if null (fst p) then p else move_up [] pt p
2.73 @@ -653,7 +653,7 @@
2.74 let
2.75 val ((pt, _), _) = get_calc cI
2.76 val pos = get_pos cI 1;
2.77 - val fillpats = find_fillpatterns (pt, pos) errpatID
2.78 + val fillpats = Inform.find_fillpatterns (pt, pos) errpatID
2.79 in findFillpatterns2xml cI (map #1 fillpats) end
2.80
2.81 (* given a fillpatID propose a fillform to the learner on the worksheet;
2.82 @@ -666,7 +666,7 @@
2.83 let
2.84 val ((pt, _), _) = get_calc cI
2.85 val pos = get_pos cI 1
2.86 - val fillforms = find_fillpatterns (pt, pos) errpatID
2.87 + val fillforms = Inform.find_fillpatterns (pt, pos) errpatID
2.88 in
2.89 case filter ((curry op = fillpatID) o
2.90 (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of
2.91 @@ -690,7 +690,7 @@
2.92 val ((pt, _), _) = get_calc cI
2.93 val pos = get_pos cI 1;
2.94 in
2.95 - case is_exactly_equal (pt, pos) ifo of
2.96 + case Inform.is_exactly_equal (pt, pos) ifo of
2.97 ("ok", tac) =>
2.98 let
2.99 in (* cp from applyTactic *)
3.1 --- a/src/Tools/isac/Interpret/inform.sml Tue Nov 22 10:42:21 2016 +0100
3.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu Nov 24 14:33:42 2016 +0100
3.3 @@ -2,137 +2,77 @@
3.4 author: Walther Neuper
3.5 0603
3.6 (c) due to copyright terms
3.7 -
3.8 -use"ME/inform.sml";
3.9 -use"inform.sml";
3.10 *)
3.11
3.12 -signature INFORM =
3.13 - sig
3.14 +signature INPUT_FORMULAS =
3.15 +sig
3.16 + datatype iitem = Find of cterm' list | Given of cterm' list | Relate of cterm' list
3.17 + type imodel = iitem list
3.18 + type icalhd = pos' * cterm' * imodel * pos_ * spec
3.19 + val fetchErrorpatterns : tac -> errpatID list
3.20 + val input_icalhd : ptree -> icalhd -> ptree * ocalhd
3.21 + val inform : calcstate' -> string -> string * calcstate'
3.22 + val find_fillpatterns : ptree * pos' -> errpatID -> (fillpatID * term * thm * subs option) list
3.23 + val is_exactly_equal : ptree * (pos * pos_) -> string -> string * tac
3.24
3.25 - type icalhd
3.26 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.27 + val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
3.28 + val cas_input : term -> (ptree * ocalhd) option
3.29 + val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
3.30 + val compare_step : taci list * pos' list * (ptree * pos') -> term -> string * calcstate'
3.31 + val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option
3.32 + val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
3.33 + rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list
3.34 + val check_error_patterns :
3.35 + term * term ->
3.36 + term * (term * term) list -> (errpatID * term list * 'a list) list * rls -> errpatID option
3.37 + val get_fillform :
3.38 + 'a * (term * term) list -> 'b * term -> errpatID -> fillpat -> (fillpatID * term * 'b * 'a) option
3.39 + val get_fillpats :
3.40 + 'a * (term * term) list -> term -> errpatID -> thm -> (fillpatID * term * thm * 'a) list
3.41 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.42 +end
3.43
3.44 - (* type iitem *)
3.45 - datatype
3.46 - iitem =
3.47 - Find of cterm' list
3.48 - | Given of cterm' list
3.49 - | Relate of cterm' list
3.50 - type imodel
3.51 - val imodel2fstr : iitem list -> (string * cterm') list
3.52 +(**)
3.53 +structure Inform(**): INPUT_FORMULAS(**) =
3.54 +struct
3.55 +(**)
3.56
3.57 -
3.58 - val Isac : 'a -> theory
3.59 - val appl_add' :
3.60 - theory' ->
3.61 - SpecifyTools.ori list ->
3.62 - SpecifyTools.itm list ->
3.63 - ('a * (Term.term * Term.term)) list ->
3.64 - string * cterm' -> SpecifyTools.itm
3.65 - (* val appl_adds :
3.66 - theory' ->
3.67 - SpecifyTools.ori list ->
3.68 - SpecifyTools.itm list ->
3.69 - (string * (Term.term * Term.term)) list ->
3.70 - (string * string) list -> SpecifyTools.itm list *)
3.71 - (* val cas_input : string -> ptree * ocalhd *)
3.72 - (* val cas_input_ :
3.73 - spec ->
3.74 - (Term.term * Term.term list) list ->
3.75 - pblID * SpecifyTools.itm list * metID * SpecifyTools.itm list *
3.76 - (bool * Term.term) list *)
3.77 - val compare_step :
3.78 - calcstate' -> Term.term -> string * calcstate'
3.79 - (* val concat_deriv :
3.80 - 'a * ((Term.term * Term.term) list -> Term.term * Term.term -> bool)
3.81 - ->
3.82 - rls ->
3.83 - rule list ->
3.84 - Term.term ->
3.85 - Term.term ->
3.86 - bool * (Term.term * rule * (Term.term * Term.term list)) list *)
3.87 - val dropwhile' : (* systest/auto-inform.sml *)
3.88 - ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
3.89 - (* val dtss2itm_ :
3.90 - pbt_ list ->
3.91 - Term.term * Term.term list ->
3.92 - int list * bool * string * SpecifyTools.itm_ *)
3.93 - (* val e_icalhd : icalhd *)
3.94 - val eq7 : ''a * ''b -> ''a * (''b * 'c) -> bool
3.95 - val equal : ''a -> ''a -> bool
3.96 - (* val filter_dsc :
3.97 - SpecifyTools.ori list -> SpecifyTools.itm -> SpecifyTools.ori list *)
3.98 - (* val filter_sep : ('a -> bool) -> 'a list -> 'a list * 'a list *)
3.99 - (* val flattup2 : 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e *)
3.100 - (* val fstr2itm_ :
3.101 - theory ->
3.102 - (''a * (Term.term * Term.term)) list ->
3.103 - ''a * string -> int list * bool * ''a * SpecifyTools.itm_ *)
3.104 - val inform :
3.105 - calcstate' -> cterm' -> string * calcstate'
3.106 - val input_icalhd : ptree -> icalhd -> ptree * ocalhd
3.107 - (* val is_Par : SpecifyTools.itm -> bool *)
3.108 - (* val is_casinput : cterm' -> fmz -> bool *)
3.109 - (* val is_e_ts : Term.term list -> bool *)
3.110 - (* val itms2fstr : SpecifyTools.itm -> string * string *)
3.111 - (* val mk_tacis :
3.112 - rew_ord' * 'a ->
3.113 - rls ->
3.114 - Term.term * rule * (Term.term * Term.term list) ->
3.115 - tac * tac_ * (pos' * istate) *)
3.116 - val oris2itms :
3.117 - 'a -> int -> SpecifyTools.ori list -> SpecifyTools.itm list
3.118 - (* val par2fstr : SpecifyTools.itm -> string * cterm' *)
3.119 - (* val parsitm : theory -> SpecifyTools.itm -> SpecifyTools.itm *)
3.120 - val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
3.121 - (* val unknown_expl :
3.122 - theory' ->
3.123 - (string * (Term.term * Term.term)) list ->
3.124 - (string * string) list -> SpecifyTools.itm list *)
3.125 - end
3.126 -
3.127 -
3.128 -
3.129 -
3.130 -
3.131 -
3.132 -(***. handle an input calc-head .***)
3.133 -
3.134 -(*------------------------------------------------------------------(**)
3.135 -structure inform :INFORM =
3.136 -struct
3.137 -(**)------------------------------------------------------------------*)
3.138 +(*** handle an input calc-head ***)
3.139
3.140 datatype iitem =
3.141 Given of cterm' list
3.142 (*Where is never input*)
3.143 | Find of cterm' list
3.144 -| Relate of cterm' list;
3.145 +| Relate of cterm' list
3.146
3.147 -type imodel = iitem list;
3.148 +type imodel = iitem list
3.149
3.150 (*calc-head as input*)
3.151 type icalhd =
3.152 - pos' * (*the position of the calc-head in the calc-tree*)
3.153 - cterm' * (*the headline*)
3.154 - imodel * (*the model (without Find) of the calc-head*)
3.155 - pos_ * (*model belongs to Pbl or Met*)
3.156 - spec; (*specification: domID, pblID, metID*)
3.157 -val e_icalhd = (e_pos', "", [Given [""]], Pbl, e_spec): icalhd;
3.158 + pos' * (*the position of the calc-head in the calc-tree*)
3.159 + cterm' * (*the headline*)
3.160 + imodel * (*the model (without Find) of the calc-head*)
3.161 + pos_ * (*model belongs to Pbl or Met*)
3.162 + spec; (*specification: domID, pblID, metID*)
3.163 +val e_icalhd = (e_pos', "", [Given [""]], Pbl, e_spec) : icalhd
3.164
3.165 -fun is_casinput (hdf: cterm') ((fmz_, spec): fmz) =
3.166 - hdf <> "" andalso fmz_ = [] andalso spec = e_spec;
3.167 +fun is_casinput (hdf : cterm') ((fmz_, spec) : fmz) =
3.168 + hdf <> "" andalso fmz_ = [] andalso spec = e_spec
3.169
3.170 (*.handle an input as into an algebra system.*)
3.171 fun dtss2itm_ ppc (d, ts) =
3.172 - let val (f, (d, id)) = the (find_first ((curry op= d) o
3.173 - (#1: (term * term) -> term) o
3.174 - (#2: pbt_ -> (term * term))) ppc)
3.175 - in ([1], true, f, Cor ((d, ts), (id, ts))) end;
3.176 +let
3.177 + val (f, (d, id)) = the (find_first ((curry op= d) o
3.178 + (#1: (term * term) -> term) o
3.179 + (#2: pbt_ -> (term * term))) ppc)
3.180 +in
3.181 + ([1], true, f, Cor ((d, ts), (id, ts)))
3.182 +end
3.183
3.184 -fun flattup2 (a,(b,c,d,e)) = (a,b,c,d,e);
3.185 +fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
3.186
3.187 -fun cas_input_ ((dI,pI,mI): spec) dtss = (*WN110515 reconsider thy..ctxt*)
3.188 +fun cas_input_ ((dI, pI, mI): spec) dtss = (*WN110515 reconsider thy..ctxt*)
3.189 let
3.190 val thy = assoc_thy dI
3.191 val {ppc, ...} = get_pbt pI
3.192 @@ -157,11 +97,12 @@
3.193
3.194 (* check if the input term is a CAScmd and return a ptree with a _complete_ calchead *)
3.195 fun cas_input hdt =
3.196 - let val (h,argl) = strip_comb hdt
3.197 + let
3.198 + val (h, argl) = strip_comb hdt
3.199 in
3.200 case assoc_cas (assoc_thy "Isac") h of
3.201 - NONE => NONE
3.202 - | SOME (spec as (dI,_,_), argl2dtss) =>
3.203 + NONE => NONE
3.204 + | SOME (spec as (dI,_,_), argl2dtss) =>
3.205 let
3.206 val dtss = argl2dtss argl
3.207 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
3.208 @@ -172,105 +113,104 @@
3.209 val pt = update_pbl pt [] pits
3.210 val pt = update_met pt [] mits
3.211 val pt = update_ctxt pt [] ctxt
3.212 - in SOME (pt, (true, Met, hdt, mits, pre, spec) : ocalhd) end
3.213 - end;
3.214 + in
3.215 + SOME (pt, (true, Met, hdt, mits, pre, spec) : ocalhd)
3.216 + end
3.217 + end
3.218
3.219 (*lazy evaluation for (Thy_Info.get_theory "Isac")*)
3.220 fun Isac _ = assoc_thy "Isac";
3.221
3.222 -(*re-parse itms with a new thy and prepare for checking with ori list*)
3.223 -fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) =
3.224 - (let
3.225 - val t = comp_dts (d,ts);
3.226 - val s = term_to_string''' dI t;
3.227 - (*this ^ should raise the exn on unability of re-parsing dts*)
3.228 +(* re-parse itms with a new thy and prepare for checking with ori list *)
3.229 +fun parsitm dI (itm as (i, v, _, f, Cor ((d, ts), _)) : itm) =
3.230 + (let val t = comp_dts (d, ts)
3.231 + val _ = (term_to_string''' dI t)
3.232 + (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
3.233 in itm end
3.234 - handle _ => ((i,v,false,f, Syn (term2str t)):itm))
3.235 - | parsitm dI (itm as (i,v,b,f, Syn str)) =
3.236 - (let val t = (Thm.term_of o the o (parse dI)) str
3.237 - in (i,v,b,f, Par str) end
3.238 - handle _ => (i,v,b,f, Syn str))
3.239 - | parsitm dI (itm as (i,v,b,f, Typ str)) =
3.240 - (let val t = (Thm.term_of o the o (parse dI)) str
3.241 - in (i,v,b,f, Par str) end
3.242 - handle _ => (i,v,b,f, Syn str))
3.243 - | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) =
3.244 + handle _ => ((i, v, false, f, Syn (term2str t)) : itm))
3.245 + | parsitm dI (i, v, b, f, Syn str) =
3.246 + (let val _ = (Thm.term_of o the o (parse dI)) str
3.247 + in (i, v, b ,f, Par str) end
3.248 + handle _ => (i, v, b, f, Syn str))
3.249 + | parsitm dI (i, v, b, f, Typ str) =
3.250 + (let val _ = (Thm.term_of o the o (parse dI)) str
3.251 + in (i, v, b, f, Par str) end
3.252 + handle _ => (i, v, b, f, Syn str))
3.253 + | parsitm dI (itm as (i, v, _, f, Inc ((d, ts), _))) =
3.254 (let val t = comp_dts (d,ts);
3.255 - val s = term_to_string''' dI t;
3.256 + val _ = term_to_string''' dI t;
3.257 (*this ^ should raise the exn on unability of re-parsing dts*)
3.258 in itm end
3.259 - handle _ => ((i,v,false,f, Syn (term2str t)):itm))
3.260 - | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) =
3.261 + handle _ => (i, v, false, f, Syn (term2str t)))
3.262 + | parsitm dI (itm as (i, v, _, f, Sup (d, ts))) =
3.263 (let val t = comp_dts (d,ts);
3.264 - val s = term_to_string''' dI t;
3.265 + val _ = term_to_string''' dI t;
3.266 (*this ^ should raise the exn on unability of re-parsing dts*)
3.267 in itm end
3.268 - handle _ => ((i,v,false,f, Syn (term2str t)):itm))
3.269 - | parsitm dI (itm as (i,v,_,f, Mis (d,t'))) =
3.270 + handle _ => (i, v, false, f, Syn (term2str t)))
3.271 + | parsitm dI (itm as (i, v, _, f, Mis (d, t'))) =
3.272 (let val t = d $ t';
3.273 - val s = term_to_string''' dI t;
3.274 + val _ = term_to_string''' dI t;
3.275 (*this ^ should raise the exn on unability of re-parsing dts*)
3.276 in itm end
3.277 - handle _ => ((i,v,false,f, Syn (term2str t)):itm))
3.278 - | parsitm dI (itm as (i,v,_,f, Par _)) =
3.279 + handle _ => (i, v, false, f, Syn (term2str t)))
3.280 + | parsitm dI (itm as (_, _, _, _, Par _)) =
3.281 error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm ^ "): Par should be internal");
3.282
3.283 (*separate a list to a pair of elements that do NOT satisfy the predicate,
3.284 and of elements that satisfy the predicate, i.e. (false, true)*)
3.285 fun filter_sep pred xs =
3.286 - let fun filt ab [] = ab
3.287 - | filt (a,b) (x :: xs) = if pred x
3.288 - then filt (a,b@[x]) xs
3.289 - else filt (a@[x],b) xs
3.290 - in filt ([],[]) xs end;
3.291 -fun is_Par ((_,_,_,_,Par _):itm) = true
3.292 + let
3.293 + fun filt ab [] = ab
3.294 + | filt (a, b) (x :: xs) =
3.295 + if pred x
3.296 + then filt (a, b @ [x]) xs
3.297 + else filt (a @ [x], b) xs
3.298 + in filt ([], []) xs end;
3.299 +fun is_Par ((_, _, _, _,Par _) : itm) = true
3.300 | is_Par _ = false;
3.301
3.302 fun is_e_ts [] = true
3.303 | is_e_ts [Const ("List.list.Nil", _)] = true
3.304 | is_e_ts _ = false;
3.305
3.306 -(*WN.9.11.03 copied from fun appl_add (in modspec.sml)*)
3.307 -(* val (sel,ct) = selct;
3.308 - val (dI, oris, ppc, pbt, (sel, ct))=
3.309 - (#1 (some_spec ospec spec), oris, []:itm list,
3.310 - ((#ppc o get_pbt) (#2 (some_spec ospec spec))),
3.311 - hd (imodel2fstr imodel));
3.312 - *)
3.313 +(* WN.9.11.03 copied from fun appl_add *)
3.314 fun appl_add' dI oris ppc pbt (sel, ct) =
3.315 - let
3.316 - val ctxt = assoc_thy dI |> thy2ctxt;
3.317 - in case parseNEW ctxt ct of
3.318 - NONE => (0,[],false,sel, Syn ct):itm
3.319 - | SOME t => (case is_known ctxt sel oris t of
3.320 - ("", ori', all) =>
3.321 - (case is_notyet_input ctxt ppc all ori' pbt of
3.322 - ("",itm) => itm
3.323 - | (msg,_) => error ("appl_add': " ^ msg))
3.324 - | (_, (i, v, _, d, ts), _) => if is_e_ts ts then
3.325 - (i, v, false, sel, Inc ((d, ts), (e_term, []))) else
3.326 - (i, v, false, sel, Sup (d, ts)))
3.327 - end;
3.328 + let
3.329 + val ctxt = assoc_thy dI |> thy2ctxt;
3.330 + in
3.331 + case parseNEW ctxt ct of
3.332 + NONE => (0,[],false,sel, Syn ct):itm
3.333 + | SOME t =>
3.334 + (case is_known ctxt sel oris t of
3.335 + ("", ori', all) =>
3.336 + (case is_notyet_input ctxt ppc all ori' pbt of
3.337 + ("",itm) => itm
3.338 + | (msg,_) => error ("appl_add': " ^ msg))
3.339 + | (_, (i, v, _, d, ts), _) =>
3.340 + if is_e_ts ts
3.341 + then (i, v, false, sel, Inc ((d, ts), (e_term, [])))
3.342 + else (i, v, false, sel, Sup (d, ts)))
3.343 + end
3.344
3.345 -(*.generate preliminary itm_ from a strin (with field "#Given" etc.).*)
3.346 -(* val (f, str) = hd selcts;
3.347 - *)
3.348 -fun eq7 (f, d) (f', (d', _)) = f=f' andalso d=d';
3.349 +(* generate preliminary itm_ from a strin (with field "#Given" etc.) *)
3.350 +fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
3.351 fun fstr2itm_ thy pbt (f, str) =
3.352 - let val topt = parse thy str
3.353 - in case topt of
3.354 - NONE => ([], false, f, Syn str)
3.355 - | SOME ct =>
3.356 -(* val SOME ct = parse thy str;
3.357 - *)
3.358 - let val (d,ts) = (split_dts o Thm.term_of) ct
3.359 - val popt = find_first (eq7 (f,d)) pbt
3.360 - in case popt of
3.361 - NONE => ([1](*??*), true(*??*), f, Sup (d,ts))
3.362 - | SOME (f, (d, id)) => ([1], true, f, Cor ((d,ts), (id, ts)))
3.363 - end
3.364 - end;
3.365 -
3.366 + let
3.367 + val topt = parse thy str
3.368 + in
3.369 + case topt of
3.370 + NONE => ([], false, f, Syn str)
3.371 + | SOME ct =>
3.372 + let
3.373 + val (d, ts) = (split_dts o Thm.term_of) ct
3.374 + val popt = find_first (eq7 (f, d)) pbt
3.375 + in
3.376 + case popt of
3.377 + NONE => ([1](*??*), true(*??*), f, Sup (d, ts))
3.378 + | SOME (f, (d, id)) => ([1], true, f, Cor ((d, ts), (id, ts)))
3.379 + end
3.380 + end
3.381
3.382 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
3.383 fun unknown_expl dI pbt selcts =
3.384 @@ -278,81 +218,41 @@
3.385 val thy = assoc_thy dI
3.386 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
3.387 val its = add_id its_
3.388 -in (map flattup2 its): itm list end;
3.389 + in
3.390 + (map flattup2 its): itm list
3.391 + end
3.392
3.393 +(* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
3.394 + appl_add': generate 1 item
3.395 + appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
3.396 + appl_add' . is_notyet_input: compare with items in model already input
3.397 + insert_ppc': insert this 1 item*)
3.398 +fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
3.399 + (*already present itms in model are being overwritten*)
3.400 + | appl_adds _ _ ppc _ [] = ppc
3.401 + | appl_adds dI oris ppc pbt (selct :: ss) =
3.402 + let val itm = appl_add' dI oris ppc pbt selct;
3.403 + in appl_adds dI oris (insert_ppc' itm ppc) pbt ss end
3.404
3.405 -
3.406 -
3.407 -(*WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
3.408 - appl_add': generate 1 item
3.409 - appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
3.410 - appl_add' . is_notyet_input: compare with items in model already input
3.411 - insert_ppc': insert this 1 item*)
3.412 -(* val (dI,oris,ppc,pbt,selcts) =((#1 (some_spec ospec spec)),oris,[(*!!*)],
3.413 - ((#ppc o get_pbt) (#2 (some_spec ospec spec))),
3.414 - (imodel2fstr imodel));
3.415 - *)
3.416 -fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
3.417 - (*already present itms in model are being overwritten*)
3.418 - | appl_adds dI oris ppc pbt [] = ppc
3.419 - | appl_adds dI oris ppc pbt (selct::ss) =
3.420 - (* val selct = (sel, string_of_cterm ct);
3.421 - *)
3.422 - let val itm = appl_add' dI oris ppc pbt selct;
3.423 - in appl_adds dI oris (insert_ppc' itm ppc) pbt ss end;
3.424 -(* val (dI, oris, ppc, pbt, selct::ss) =
3.425 - (dI, pors, probl, ppc, map itms2fstr probl);
3.426 - ...vvv
3.427 - *)
3.428 -(* val (dI, oris, ppc, pbt, (selct::ss))=
3.429 - (#1 (some_spec ospec spec), oris, []:itm list,
3.430 - ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
3.431 - val iii = appl_adds dI oris ppc pbt (selct::ss);
3.432 - tracing(itms2str_ thy iii);
3.433 -
3.434 - val itm = appl_add' dI oris ppc pbt selct;
3.435 - val ppc = insert_ppc' itm ppc;
3.436 -
3.437 - val _::selct::ss = (selct::ss);
3.438 - val itm = appl_add' dI oris ppc pbt selct;
3.439 - val ppc = insert_ppc' itm ppc;
3.440 -
3.441 - val _::selct::ss = (selct::ss);
3.442 - val itm = appl_add' dI oris ppc pbt selct;
3.443 - val ppc = insert_ppc' itm ppc;
3.444 - tracing(itms2str_ thy ppc);
3.445 -
3.446 - val _::selct::ss = (selct::ss);
3.447 - val itm = appl_add' dI oris ppc pbt selct;
3.448 - val ppc = insert_ppc' itm ppc;
3.449 - *)
3.450 -
3.451 -
3.452 -fun oris2itms _ _ ([]:ori list) = ([]:itm list)
3.453 - | oris2itms pbt vat ((i,v,f,d,ts)::(os: ori list)) =
3.454 +fun oris2itms _ _ [] = ([] : itm list)
3.455 + | oris2itms pbt vat ((i, v, f, d, ts) :: (os: ori list)) =
3.456 if member op = vat v
3.457 - then (i,v,true,f,Cor ((d,ts),(e_term,[])))::(oris2itms pbt vat os)
3.458 - else oris2itms pbt vat os;
3.459 + then (i, v, true, f, Cor ((d, ts), (e_term, []))) :: (oris2itms pbt vat os)
3.460 + else oris2itms pbt vat os
3.461
3.462 fun filter_dsc oris itm =
3.463 - filter_out ((curry op= ((d_in o #5) (itm:itm))) o
3.464 - (#4:ori -> term)) oris;
3.465 + filter_out ((curry op= ((d_in o #5) (itm:itm))) o (#4:ori -> term)) oris
3.466
3.467 -
3.468 -
3.469 -
3.470 -fun par2fstr ((_,_,_,f, Par s):itm) = (f, s)
3.471 - | par2fstr itm = error ("par2fstr: called with " ^
3.472 - itm2str_ (thy2ctxt' "Isac") itm);
3.473 -fun itms2fstr ((_,_,_,f, Cor ((d,ts),_)):itm) = (f, comp_dts'' (d,ts))
3.474 - | itms2fstr (_,_,_,f, Syn str) = (f, str)
3.475 - | itms2fstr (_,_,_,f, Typ str) = (f, str)
3.476 - | itms2fstr (_,_,_,f, Inc ((d,ts),_)) = (f, comp_dts'' (d,ts))
3.477 - | itms2fstr (_,_,_,f, Sup (d,ts)) = (f, comp_dts'' (d,ts))
3.478 - | itms2fstr (_,_,_,f, Mis (d,t)) = (f, term2str (d $ t))
3.479 - | itms2fstr (itm as (_,_,_,f, Par _)) =
3.480 - error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^
3.481 - "): Par should be internal");
3.482 +fun par2fstr ((_, _, _, f, Par s) : itm) = (f, s)
3.483 + | par2fstr itm = error ("par2fstr: called with " ^ itm2str_ (thy2ctxt' "Isac") itm)
3.484 +fun itms2fstr ((_, _, _, f, Cor ((d, ts), _)) : itm) = (f, comp_dts'' (d, ts))
3.485 + | itms2fstr (_, _, _, f, Syn str) = (f, str)
3.486 + | itms2fstr (_, _, _, f, Typ str) = (f, str)
3.487 + | itms2fstr (_, _, _, f, Inc ((d, ts), _)) = (f, comp_dts'' (d,ts))
3.488 + | itms2fstr (_, _, _, f, Sup (d, ts)) = (f, comp_dts'' (d, ts))
3.489 + | itms2fstr (_, _, _, f, Mis (d, t)) = (f, term2str (d $ t))
3.490 + | itms2fstr (itm as (_, _, _, _, Par _)) =
3.491 + error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^ "): Par should be internal");
3.492
3.493 fun imodel2fstr iitems =
3.494 let
3.495 @@ -768,8 +668,6 @@
3.496 | Rrls {errpatts, ...} => errpatts
3.497 | Erls => []
3.498 end
3.499 -
3.500 -(*------------------------------------------------------------------(**)
3.501 +(**)
3.502 end
3.503 -open inform;
3.504 -(**)------------------------------------------------------------------*)
3.505 +(**)
3.506 \ No newline at end of file
4.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Tue Nov 22 10:42:21 2016 +0100
4.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Thu Nov 24 14:33:42 2016 +0100
4.3 @@ -430,9 +430,9 @@
4.4 (*XML.Elem (("WHERE", []), wheres), ... Where is never input*)
4.5 XML.Elem (("FIND", []), finds),
4.6 XML.Elem (("RELATE", []), relates)])) =
4.7 - ([Given (map xml_to_cterm givens),
4.8 - Find (map xml_to_cterm finds),
4.9 - Relate (map xml_to_cterm relates)]): imodel
4.10 + ([Inform.Given (map xml_to_cterm givens),
4.11 + Inform.Find (map xml_to_cterm finds),
4.12 + Inform.Relate (map xml_to_cterm relates)]) : Inform.imodel
4.13 | xml_to_imodel x = raise ERROR ("xml_to_imodel: WRONG arg = " ^ xmlstr 0 x)
4.14 fun xml_to_icalhd
4.15 (XML.Elem (( "ICALCHEAD", []), [
4.16 @@ -442,7 +442,7 @@
4.17 XML.Elem (( "POS", []), [XML.Text belongsto]),
4.18 spec as XML.Elem (( "SPECIFICATION", []), _)])) =
4.19 (xml_to_pos pos, xml_to_term_NEW form |> term2str, xml_to_imodel imodel,
4.20 - str2pos_ belongsto, xml_to_spec spec): icalhd
4.21 + str2pos_ belongsto, xml_to_spec spec) : Inform.icalhd
4.22 | xml_to_icalhd x = raise ERROR ("xml_to_icalhd: WRONG arg = " ^ xmlstr 0 x)
4.23
4.24 fun xml_of_sub (id, value) =
5.1 --- a/test/Tools/isac/Interpret/inform.sml Tue Nov 22 10:42:21 2016 +0100
5.2 +++ b/test/Tools/isac/Interpret/inform.sml Thu Nov 24 14:33:42 2016 +0100
5.3 @@ -38,6 +38,7 @@
5.4 "--------- build fun get_fillpats --------------------------------";
5.5 "--------- embed fun find_fillpatterns ---------------------------";
5.6 "--------- build fun is_exactly_equal, inputFillFormula ----------";
5.7 +"--------- fun appl_adds -----------------------------------------";
5.8 "-----------------------------------------------------------------";
5.9 "-----------------------------------------------------------------";
5.10 "-----------------------------------------------------------------";
5.11 @@ -1292,3 +1293,32 @@
5.12 | _ => error "inputFillFormula changed 112"
5.13 else error "inputFillFormula changed 113";
5.14
5.15 +"--------- fun appl_adds -----------------------------------------";
5.16 +"--------- fun appl_adds -----------------------------------------";
5.17 +"--------- fun appl_adds -----------------------------------------";
5.18 +(* val (dI, oris, ppc, pbt, selct::ss) =
5.19 + (dI, pors, probl, ppc, map itms2fstr probl);
5.20 + ...vvv
5.21 + *)
5.22 +(* val (dI, oris, ppc, pbt, (selct::ss))=
5.23 + (#1 (some_spec ospec spec), oris, []:itm list,
5.24 + ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
5.25 + val iii = appl_adds dI oris ppc pbt (selct::ss);
5.26 + tracing(itms2str_ thy iii);
5.27 +
5.28 + val itm = appl_add' dI oris ppc pbt selct;
5.29 + val ppc = insert_ppc' itm ppc;
5.30 +
5.31 + val _::selct::ss = (selct::ss);
5.32 + val itm = appl_add' dI oris ppc pbt selct;
5.33 + val ppc = insert_ppc' itm ppc;
5.34 +
5.35 + val _::selct::ss = (selct::ss);
5.36 + val itm = appl_add' dI oris ppc pbt selct;
5.37 + val ppc = insert_ppc' itm ppc;
5.38 + tracing(itms2str_ thy ppc);
5.39 +
5.40 + val _::selct::ss = (selct::ss);
5.41 + val itm = appl_add' dI oris ppc pbt selct;
5.42 + val ppc = insert_ppc' itm ppc;
5.43 + *)
6.1 --- a/test/Tools/isac/Interpret/mathengine.sml Tue Nov 22 10:42:21 2016 +0100
6.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Thu Nov 24 14:33:42 2016 +0100
6.3 @@ -660,6 +660,7 @@
6.4 val (form, tac, asms) = pt_extract (pt, p)
6.5 val SOME ta = tac;
6.6 "~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta);
6.7 +val i = 2;
6.8 "~~~~~ fun tac2xml, args:"; val (j, (Rewrite thm')) = (i, tac);
6.9 "~~~~~ fun thm'2xml, args:"; val (j, ((ID, form) : thm'')) = ((j+i), thm');
6.10 ID = "rnorm_equation_add";
7.1 --- a/test/Tools/isac/Test_Isac.thy Tue Nov 22 10:42:21 2016 +0100
7.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Nov 24 14:33:42 2016 +0100
7.3 @@ -68,9 +68,11 @@
7.4
7.5 ML {*
7.6 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
7.7 + (* these vvv test, if additional funs intermediately added to structure *)
7.8 open Kernel;
7.9 - open Math_Engine
7.10 - open Lucin;
7.11 + open Math_Engine; CalcTreeTEST;
7.12 + open Lucin; appy;
7.13 + open Inform; cas_input;
7.14 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.15 *}
7.16 ML {*
8.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Tue Nov 22 10:42:21 2016 +0100
8.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Thu Nov 24 14:33:42 2016 +0100
8.3 @@ -70,6 +70,7 @@
8.4 *)
8.5 ;
8.6 thydata2xml (theID, thydata) (*reported Exception- Match in question*);
8.7 +val i = 2;
8.8 ;
8.9 val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = (theID, thydata);
8.10 rls2xml i thy_rls (*reported Exception- Match in question*);