1.1 --- a/src/Tools/isac/Interpret/inform.sml Tue Nov 22 10:42:21 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu Nov 24 14:33:42 2016 +0100
1.3 @@ -2,137 +2,77 @@
1.4 author: Walther Neuper
1.5 0603
1.6 (c) due to copyright terms
1.7 -
1.8 -use"ME/inform.sml";
1.9 -use"inform.sml";
1.10 *)
1.11
1.12 -signature INFORM =
1.13 - sig
1.14 +signature INPUT_FORMULAS =
1.15 +sig
1.16 + datatype iitem = Find of cterm' list | Given of cterm' list | Relate of cterm' list
1.17 + type imodel = iitem list
1.18 + type icalhd = pos' * cterm' * imodel * pos_ * spec
1.19 + val fetchErrorpatterns : tac -> errpatID list
1.20 + val input_icalhd : ptree -> icalhd -> ptree * ocalhd
1.21 + val inform : calcstate' -> string -> string * calcstate'
1.22 + val find_fillpatterns : ptree * pos' -> errpatID -> (fillpatID * term * thm * subs option) list
1.23 + val is_exactly_equal : ptree * (pos * pos_) -> string -> string * tac
1.24
1.25 - type icalhd
1.26 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.27 + val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
1.28 + val cas_input : term -> (ptree * ocalhd) option
1.29 + val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
1.30 + val compare_step : taci list * pos' list * (ptree * pos') -> term -> string * calcstate'
1.31 + val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option
1.32 + val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
1.33 + rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list
1.34 + val check_error_patterns :
1.35 + term * term ->
1.36 + term * (term * term) list -> (errpatID * term list * 'a list) list * rls -> errpatID option
1.37 + val get_fillform :
1.38 + 'a * (term * term) list -> 'b * term -> errpatID -> fillpat -> (fillpatID * term * 'b * 'a) option
1.39 + val get_fillpats :
1.40 + 'a * (term * term) list -> term -> errpatID -> thm -> (fillpatID * term * thm * 'a) list
1.41 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.42 +end
1.43
1.44 - (* type iitem *)
1.45 - datatype
1.46 - iitem =
1.47 - Find of cterm' list
1.48 - | Given of cterm' list
1.49 - | Relate of cterm' list
1.50 - type imodel
1.51 - val imodel2fstr : iitem list -> (string * cterm') list
1.52 +(**)
1.53 +structure Inform(**): INPUT_FORMULAS(**) =
1.54 +struct
1.55 +(**)
1.56
1.57 -
1.58 - val Isac : 'a -> theory
1.59 - val appl_add' :
1.60 - theory' ->
1.61 - SpecifyTools.ori list ->
1.62 - SpecifyTools.itm list ->
1.63 - ('a * (Term.term * Term.term)) list ->
1.64 - string * cterm' -> SpecifyTools.itm
1.65 - (* val appl_adds :
1.66 - theory' ->
1.67 - SpecifyTools.ori list ->
1.68 - SpecifyTools.itm list ->
1.69 - (string * (Term.term * Term.term)) list ->
1.70 - (string * string) list -> SpecifyTools.itm list *)
1.71 - (* val cas_input : string -> ptree * ocalhd *)
1.72 - (* val cas_input_ :
1.73 - spec ->
1.74 - (Term.term * Term.term list) list ->
1.75 - pblID * SpecifyTools.itm list * metID * SpecifyTools.itm list *
1.76 - (bool * Term.term) list *)
1.77 - val compare_step :
1.78 - calcstate' -> Term.term -> string * calcstate'
1.79 - (* val concat_deriv :
1.80 - 'a * ((Term.term * Term.term) list -> Term.term * Term.term -> bool)
1.81 - ->
1.82 - rls ->
1.83 - rule list ->
1.84 - Term.term ->
1.85 - Term.term ->
1.86 - bool * (Term.term * rule * (Term.term * Term.term list)) list *)
1.87 - val dropwhile' : (* systest/auto-inform.sml *)
1.88 - ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
1.89 - (* val dtss2itm_ :
1.90 - pbt_ list ->
1.91 - Term.term * Term.term list ->
1.92 - int list * bool * string * SpecifyTools.itm_ *)
1.93 - (* val e_icalhd : icalhd *)
1.94 - val eq7 : ''a * ''b -> ''a * (''b * 'c) -> bool
1.95 - val equal : ''a -> ''a -> bool
1.96 - (* val filter_dsc :
1.97 - SpecifyTools.ori list -> SpecifyTools.itm -> SpecifyTools.ori list *)
1.98 - (* val filter_sep : ('a -> bool) -> 'a list -> 'a list * 'a list *)
1.99 - (* val flattup2 : 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e *)
1.100 - (* val fstr2itm_ :
1.101 - theory ->
1.102 - (''a * (Term.term * Term.term)) list ->
1.103 - ''a * string -> int list * bool * ''a * SpecifyTools.itm_ *)
1.104 - val inform :
1.105 - calcstate' -> cterm' -> string * calcstate'
1.106 - val input_icalhd : ptree -> icalhd -> ptree * ocalhd
1.107 - (* val is_Par : SpecifyTools.itm -> bool *)
1.108 - (* val is_casinput : cterm' -> fmz -> bool *)
1.109 - (* val is_e_ts : Term.term list -> bool *)
1.110 - (* val itms2fstr : SpecifyTools.itm -> string * string *)
1.111 - (* val mk_tacis :
1.112 - rew_ord' * 'a ->
1.113 - rls ->
1.114 - Term.term * rule * (Term.term * Term.term list) ->
1.115 - tac * tac_ * (pos' * istate) *)
1.116 - val oris2itms :
1.117 - 'a -> int -> SpecifyTools.ori list -> SpecifyTools.itm list
1.118 - (* val par2fstr : SpecifyTools.itm -> string * cterm' *)
1.119 - (* val parsitm : theory -> SpecifyTools.itm -> SpecifyTools.itm *)
1.120 - val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
1.121 - (* val unknown_expl :
1.122 - theory' ->
1.123 - (string * (Term.term * Term.term)) list ->
1.124 - (string * string) list -> SpecifyTools.itm list *)
1.125 - end
1.126 -
1.127 -
1.128 -
1.129 -
1.130 -
1.131 -
1.132 -(***. handle an input calc-head .***)
1.133 -
1.134 -(*------------------------------------------------------------------(**)
1.135 -structure inform :INFORM =
1.136 -struct
1.137 -(**)------------------------------------------------------------------*)
1.138 +(*** handle an input calc-head ***)
1.139
1.140 datatype iitem =
1.141 Given of cterm' list
1.142 (*Where is never input*)
1.143 | Find of cterm' list
1.144 -| Relate of cterm' list;
1.145 +| Relate of cterm' list
1.146
1.147 -type imodel = iitem list;
1.148 +type imodel = iitem list
1.149
1.150 (*calc-head as input*)
1.151 type icalhd =
1.152 - pos' * (*the position of the calc-head in the calc-tree*)
1.153 - cterm' * (*the headline*)
1.154 - imodel * (*the model (without Find) of the calc-head*)
1.155 - pos_ * (*model belongs to Pbl or Met*)
1.156 - spec; (*specification: domID, pblID, metID*)
1.157 -val e_icalhd = (e_pos', "", [Given [""]], Pbl, e_spec): icalhd;
1.158 + pos' * (*the position of the calc-head in the calc-tree*)
1.159 + cterm' * (*the headline*)
1.160 + imodel * (*the model (without Find) of the calc-head*)
1.161 + pos_ * (*model belongs to Pbl or Met*)
1.162 + spec; (*specification: domID, pblID, metID*)
1.163 +val e_icalhd = (e_pos', "", [Given [""]], Pbl, e_spec) : icalhd
1.164
1.165 -fun is_casinput (hdf: cterm') ((fmz_, spec): fmz) =
1.166 - hdf <> "" andalso fmz_ = [] andalso spec = e_spec;
1.167 +fun is_casinput (hdf : cterm') ((fmz_, spec) : fmz) =
1.168 + hdf <> "" andalso fmz_ = [] andalso spec = e_spec
1.169
1.170 (*.handle an input as into an algebra system.*)
1.171 fun dtss2itm_ ppc (d, ts) =
1.172 - let val (f, (d, id)) = the (find_first ((curry op= d) o
1.173 - (#1: (term * term) -> term) o
1.174 - (#2: pbt_ -> (term * term))) ppc)
1.175 - in ([1], true, f, Cor ((d, ts), (id, ts))) end;
1.176 +let
1.177 + val (f, (d, id)) = the (find_first ((curry op= d) o
1.178 + (#1: (term * term) -> term) o
1.179 + (#2: pbt_ -> (term * term))) ppc)
1.180 +in
1.181 + ([1], true, f, Cor ((d, ts), (id, ts)))
1.182 +end
1.183
1.184 -fun flattup2 (a,(b,c,d,e)) = (a,b,c,d,e);
1.185 +fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
1.186
1.187 -fun cas_input_ ((dI,pI,mI): spec) dtss = (*WN110515 reconsider thy..ctxt*)
1.188 +fun cas_input_ ((dI, pI, mI): spec) dtss = (*WN110515 reconsider thy..ctxt*)
1.189 let
1.190 val thy = assoc_thy dI
1.191 val {ppc, ...} = get_pbt pI
1.192 @@ -157,11 +97,12 @@
1.193
1.194 (* check if the input term is a CAScmd and return a ptree with a _complete_ calchead *)
1.195 fun cas_input hdt =
1.196 - let val (h,argl) = strip_comb hdt
1.197 + let
1.198 + val (h, argl) = strip_comb hdt
1.199 in
1.200 case assoc_cas (assoc_thy "Isac") h of
1.201 - NONE => NONE
1.202 - | SOME (spec as (dI,_,_), argl2dtss) =>
1.203 + NONE => NONE
1.204 + | SOME (spec as (dI,_,_), argl2dtss) =>
1.205 let
1.206 val dtss = argl2dtss argl
1.207 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
1.208 @@ -172,105 +113,104 @@
1.209 val pt = update_pbl pt [] pits
1.210 val pt = update_met pt [] mits
1.211 val pt = update_ctxt pt [] ctxt
1.212 - in SOME (pt, (true, Met, hdt, mits, pre, spec) : ocalhd) end
1.213 - end;
1.214 + in
1.215 + SOME (pt, (true, Met, hdt, mits, pre, spec) : ocalhd)
1.216 + end
1.217 + end
1.218
1.219 (*lazy evaluation for (Thy_Info.get_theory "Isac")*)
1.220 fun Isac _ = assoc_thy "Isac";
1.221
1.222 -(*re-parse itms with a new thy and prepare for checking with ori list*)
1.223 -fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) =
1.224 - (let
1.225 - val t = comp_dts (d,ts);
1.226 - val s = term_to_string''' dI t;
1.227 - (*this ^ should raise the exn on unability of re-parsing dts*)
1.228 +(* re-parse itms with a new thy and prepare for checking with ori list *)
1.229 +fun parsitm dI (itm as (i, v, _, f, Cor ((d, ts), _)) : itm) =
1.230 + (let val t = comp_dts (d, ts)
1.231 + val _ = (term_to_string''' dI t)
1.232 + (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
1.233 in itm end
1.234 - handle _ => ((i,v,false,f, Syn (term2str t)):itm))
1.235 - | parsitm dI (itm as (i,v,b,f, Syn str)) =
1.236 - (let val t = (Thm.term_of o the o (parse dI)) str
1.237 - in (i,v,b,f, Par str) end
1.238 - handle _ => (i,v,b,f, Syn str))
1.239 - | parsitm dI (itm as (i,v,b,f, Typ str)) =
1.240 - (let val t = (Thm.term_of o the o (parse dI)) str
1.241 - in (i,v,b,f, Par str) end
1.242 - handle _ => (i,v,b,f, Syn str))
1.243 - | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) =
1.244 + handle _ => ((i, v, false, f, Syn (term2str t)) : itm))
1.245 + | parsitm dI (i, v, b, f, Syn str) =
1.246 + (let val _ = (Thm.term_of o the o (parse dI)) str
1.247 + in (i, v, b ,f, Par str) end
1.248 + handle _ => (i, v, b, f, Syn str))
1.249 + | parsitm dI (i, v, b, f, Typ str) =
1.250 + (let val _ = (Thm.term_of o the o (parse dI)) str
1.251 + in (i, v, b, f, Par str) end
1.252 + handle _ => (i, v, b, f, Syn str))
1.253 + | parsitm dI (itm as (i, v, _, f, Inc ((d, ts), _))) =
1.254 (let val t = comp_dts (d,ts);
1.255 - val s = term_to_string''' dI t;
1.256 + val _ = term_to_string''' dI t;
1.257 (*this ^ should raise the exn on unability of re-parsing dts*)
1.258 in itm end
1.259 - handle _ => ((i,v,false,f, Syn (term2str t)):itm))
1.260 - | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) =
1.261 + handle _ => (i, v, false, f, Syn (term2str t)))
1.262 + | parsitm dI (itm as (i, v, _, f, Sup (d, ts))) =
1.263 (let val t = comp_dts (d,ts);
1.264 - val s = term_to_string''' dI t;
1.265 + val _ = term_to_string''' dI t;
1.266 (*this ^ should raise the exn on unability of re-parsing dts*)
1.267 in itm end
1.268 - handle _ => ((i,v,false,f, Syn (term2str t)):itm))
1.269 - | parsitm dI (itm as (i,v,_,f, Mis (d,t'))) =
1.270 + handle _ => (i, v, false, f, Syn (term2str t)))
1.271 + | parsitm dI (itm as (i, v, _, f, Mis (d, t'))) =
1.272 (let val t = d $ t';
1.273 - val s = term_to_string''' dI t;
1.274 + val _ = term_to_string''' dI t;
1.275 (*this ^ should raise the exn on unability of re-parsing dts*)
1.276 in itm end
1.277 - handle _ => ((i,v,false,f, Syn (term2str t)):itm))
1.278 - | parsitm dI (itm as (i,v,_,f, Par _)) =
1.279 + handle _ => (i, v, false, f, Syn (term2str t)))
1.280 + | parsitm dI (itm as (_, _, _, _, Par _)) =
1.281 error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm ^ "): Par should be internal");
1.282
1.283 (*separate a list to a pair of elements that do NOT satisfy the predicate,
1.284 and of elements that satisfy the predicate, i.e. (false, true)*)
1.285 fun filter_sep pred xs =
1.286 - let fun filt ab [] = ab
1.287 - | filt (a,b) (x :: xs) = if pred x
1.288 - then filt (a,b@[x]) xs
1.289 - else filt (a@[x],b) xs
1.290 - in filt ([],[]) xs end;
1.291 -fun is_Par ((_,_,_,_,Par _):itm) = true
1.292 + let
1.293 + fun filt ab [] = ab
1.294 + | filt (a, b) (x :: xs) =
1.295 + if pred x
1.296 + then filt (a, b @ [x]) xs
1.297 + else filt (a @ [x], b) xs
1.298 + in filt ([], []) xs end;
1.299 +fun is_Par ((_, _, _, _,Par _) : itm) = true
1.300 | is_Par _ = false;
1.301
1.302 fun is_e_ts [] = true
1.303 | is_e_ts [Const ("List.list.Nil", _)] = true
1.304 | is_e_ts _ = false;
1.305
1.306 -(*WN.9.11.03 copied from fun appl_add (in modspec.sml)*)
1.307 -(* val (sel,ct) = selct;
1.308 - val (dI, oris, ppc, pbt, (sel, ct))=
1.309 - (#1 (some_spec ospec spec), oris, []:itm list,
1.310 - ((#ppc o get_pbt) (#2 (some_spec ospec spec))),
1.311 - hd (imodel2fstr imodel));
1.312 - *)
1.313 +(* WN.9.11.03 copied from fun appl_add *)
1.314 fun appl_add' dI oris ppc pbt (sel, ct) =
1.315 - let
1.316 - val ctxt = assoc_thy dI |> thy2ctxt;
1.317 - in case parseNEW ctxt ct of
1.318 - NONE => (0,[],false,sel, Syn ct):itm
1.319 - | SOME t => (case is_known ctxt sel oris t of
1.320 - ("", ori', all) =>
1.321 - (case is_notyet_input ctxt ppc all ori' pbt of
1.322 - ("",itm) => itm
1.323 - | (msg,_) => error ("appl_add': " ^ msg))
1.324 - | (_, (i, v, _, d, ts), _) => if is_e_ts ts then
1.325 - (i, v, false, sel, Inc ((d, ts), (e_term, []))) else
1.326 - (i, v, false, sel, Sup (d, ts)))
1.327 - end;
1.328 + let
1.329 + val ctxt = assoc_thy dI |> thy2ctxt;
1.330 + in
1.331 + case parseNEW ctxt ct of
1.332 + NONE => (0,[],false,sel, Syn ct):itm
1.333 + | SOME t =>
1.334 + (case is_known ctxt sel oris t of
1.335 + ("", ori', all) =>
1.336 + (case is_notyet_input ctxt ppc all ori' pbt of
1.337 + ("",itm) => itm
1.338 + | (msg,_) => error ("appl_add': " ^ msg))
1.339 + | (_, (i, v, _, d, ts), _) =>
1.340 + if is_e_ts ts
1.341 + then (i, v, false, sel, Inc ((d, ts), (e_term, [])))
1.342 + else (i, v, false, sel, Sup (d, ts)))
1.343 + end
1.344
1.345 -(*.generate preliminary itm_ from a strin (with field "#Given" etc.).*)
1.346 -(* val (f, str) = hd selcts;
1.347 - *)
1.348 -fun eq7 (f, d) (f', (d', _)) = f=f' andalso d=d';
1.349 +(* generate preliminary itm_ from a strin (with field "#Given" etc.) *)
1.350 +fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
1.351 fun fstr2itm_ thy pbt (f, str) =
1.352 - let val topt = parse thy str
1.353 - in case topt of
1.354 - NONE => ([], false, f, Syn str)
1.355 - | SOME ct =>
1.356 -(* val SOME ct = parse thy str;
1.357 - *)
1.358 - let val (d,ts) = (split_dts o Thm.term_of) ct
1.359 - val popt = find_first (eq7 (f,d)) pbt
1.360 - in case popt of
1.361 - NONE => ([1](*??*), true(*??*), f, Sup (d,ts))
1.362 - | SOME (f, (d, id)) => ([1], true, f, Cor ((d,ts), (id, ts)))
1.363 - end
1.364 - end;
1.365 -
1.366 + let
1.367 + val topt = parse thy str
1.368 + in
1.369 + case topt of
1.370 + NONE => ([], false, f, Syn str)
1.371 + | SOME ct =>
1.372 + let
1.373 + val (d, ts) = (split_dts o Thm.term_of) ct
1.374 + val popt = find_first (eq7 (f, d)) pbt
1.375 + in
1.376 + case popt of
1.377 + NONE => ([1](*??*), true(*??*), f, Sup (d, ts))
1.378 + | SOME (f, (d, id)) => ([1], true, f, Cor ((d, ts), (id, ts)))
1.379 + end
1.380 + end
1.381
1.382 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
1.383 fun unknown_expl dI pbt selcts =
1.384 @@ -278,81 +218,41 @@
1.385 val thy = assoc_thy dI
1.386 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
1.387 val its = add_id its_
1.388 -in (map flattup2 its): itm list end;
1.389 + in
1.390 + (map flattup2 its): itm list
1.391 + end
1.392
1.393 +(* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
1.394 + appl_add': generate 1 item
1.395 + appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
1.396 + appl_add' . is_notyet_input: compare with items in model already input
1.397 + insert_ppc': insert this 1 item*)
1.398 +fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
1.399 + (*already present itms in model are being overwritten*)
1.400 + | appl_adds _ _ ppc _ [] = ppc
1.401 + | appl_adds dI oris ppc pbt (selct :: ss) =
1.402 + let val itm = appl_add' dI oris ppc pbt selct;
1.403 + in appl_adds dI oris (insert_ppc' itm ppc) pbt ss end
1.404
1.405 -
1.406 -
1.407 -(*WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
1.408 - appl_add': generate 1 item
1.409 - appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
1.410 - appl_add' . is_notyet_input: compare with items in model already input
1.411 - insert_ppc': insert this 1 item*)
1.412 -(* val (dI,oris,ppc,pbt,selcts) =((#1 (some_spec ospec spec)),oris,[(*!!*)],
1.413 - ((#ppc o get_pbt) (#2 (some_spec ospec spec))),
1.414 - (imodel2fstr imodel));
1.415 - *)
1.416 -fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
1.417 - (*already present itms in model are being overwritten*)
1.418 - | appl_adds dI oris ppc pbt [] = ppc
1.419 - | appl_adds dI oris ppc pbt (selct::ss) =
1.420 - (* val selct = (sel, string_of_cterm ct);
1.421 - *)
1.422 - let val itm = appl_add' dI oris ppc pbt selct;
1.423 - in appl_adds dI oris (insert_ppc' itm ppc) pbt ss end;
1.424 -(* val (dI, oris, ppc, pbt, selct::ss) =
1.425 - (dI, pors, probl, ppc, map itms2fstr probl);
1.426 - ...vvv
1.427 - *)
1.428 -(* val (dI, oris, ppc, pbt, (selct::ss))=
1.429 - (#1 (some_spec ospec spec), oris, []:itm list,
1.430 - ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
1.431 - val iii = appl_adds dI oris ppc pbt (selct::ss);
1.432 - tracing(itms2str_ thy iii);
1.433 -
1.434 - val itm = appl_add' dI oris ppc pbt selct;
1.435 - val ppc = insert_ppc' itm ppc;
1.436 -
1.437 - val _::selct::ss = (selct::ss);
1.438 - val itm = appl_add' dI oris ppc pbt selct;
1.439 - val ppc = insert_ppc' itm ppc;
1.440 -
1.441 - val _::selct::ss = (selct::ss);
1.442 - val itm = appl_add' dI oris ppc pbt selct;
1.443 - val ppc = insert_ppc' itm ppc;
1.444 - tracing(itms2str_ thy ppc);
1.445 -
1.446 - val _::selct::ss = (selct::ss);
1.447 - val itm = appl_add' dI oris ppc pbt selct;
1.448 - val ppc = insert_ppc' itm ppc;
1.449 - *)
1.450 -
1.451 -
1.452 -fun oris2itms _ _ ([]:ori list) = ([]:itm list)
1.453 - | oris2itms pbt vat ((i,v,f,d,ts)::(os: ori list)) =
1.454 +fun oris2itms _ _ [] = ([] : itm list)
1.455 + | oris2itms pbt vat ((i, v, f, d, ts) :: (os: ori list)) =
1.456 if member op = vat v
1.457 - then (i,v,true,f,Cor ((d,ts),(e_term,[])))::(oris2itms pbt vat os)
1.458 - else oris2itms pbt vat os;
1.459 + then (i, v, true, f, Cor ((d, ts), (e_term, []))) :: (oris2itms pbt vat os)
1.460 + else oris2itms pbt vat os
1.461
1.462 fun filter_dsc oris itm =
1.463 - filter_out ((curry op= ((d_in o #5) (itm:itm))) o
1.464 - (#4:ori -> term)) oris;
1.465 + filter_out ((curry op= ((d_in o #5) (itm:itm))) o (#4:ori -> term)) oris
1.466
1.467 -
1.468 -
1.469 -
1.470 -fun par2fstr ((_,_,_,f, Par s):itm) = (f, s)
1.471 - | par2fstr itm = error ("par2fstr: called with " ^
1.472 - itm2str_ (thy2ctxt' "Isac") itm);
1.473 -fun itms2fstr ((_,_,_,f, Cor ((d,ts),_)):itm) = (f, comp_dts'' (d,ts))
1.474 - | itms2fstr (_,_,_,f, Syn str) = (f, str)
1.475 - | itms2fstr (_,_,_,f, Typ str) = (f, str)
1.476 - | itms2fstr (_,_,_,f, Inc ((d,ts),_)) = (f, comp_dts'' (d,ts))
1.477 - | itms2fstr (_,_,_,f, Sup (d,ts)) = (f, comp_dts'' (d,ts))
1.478 - | itms2fstr (_,_,_,f, Mis (d,t)) = (f, term2str (d $ t))
1.479 - | itms2fstr (itm as (_,_,_,f, Par _)) =
1.480 - error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^
1.481 - "): Par should be internal");
1.482 +fun par2fstr ((_, _, _, f, Par s) : itm) = (f, s)
1.483 + | par2fstr itm = error ("par2fstr: called with " ^ itm2str_ (thy2ctxt' "Isac") itm)
1.484 +fun itms2fstr ((_, _, _, f, Cor ((d, ts), _)) : itm) = (f, comp_dts'' (d, ts))
1.485 + | itms2fstr (_, _, _, f, Syn str) = (f, str)
1.486 + | itms2fstr (_, _, _, f, Typ str) = (f, str)
1.487 + | itms2fstr (_, _, _, f, Inc ((d, ts), _)) = (f, comp_dts'' (d,ts))
1.488 + | itms2fstr (_, _, _, f, Sup (d, ts)) = (f, comp_dts'' (d, ts))
1.489 + | itms2fstr (_, _, _, f, Mis (d, t)) = (f, term2str (d $ t))
1.490 + | itms2fstr (itm as (_, _, _, _, Par _)) =
1.491 + error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^ "): Par should be internal");
1.492
1.493 fun imodel2fstr iitems =
1.494 let
1.495 @@ -768,8 +668,6 @@
1.496 | Rrls {errpatts, ...} => errpatts
1.497 | Erls => []
1.498 end
1.499 -
1.500 -(*------------------------------------------------------------------(**)
1.501 +(**)
1.502 end
1.503 -open inform;
1.504 -(**)------------------------------------------------------------------*)
1.505 +(**)
1.506 \ No newline at end of file