1.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed May 04 09:01:10 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Wed May 04 14:04:53 2011 +0200
1.3 @@ -773,54 +773,49 @@
1.4 fun appl_add ctxt sel [] ppc pbt ct =
1.5 let
1.6 val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
1.7 - in case parseNEW ctxt ct of
1.8 - NONE => Add (i, [], false, sel, Syn ct)
1.9 - | SOME t =>
1.10 - let val (d, ts) = split_dts t;
1.11 - in if d = e_term then
1.12 - Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else
1.13 - (case find_first (eq1 d) pbt of
1.14 - NONE => Add (i, [], true, sel, Sup (d,ts))
1.15 - | SOME (f, (_, id)) =>
1.16 - let fun eq2 d (i, _, _, _, itm_) =
1.17 - d = (d_in itm_) andalso i <> 0;
1.18 - in case find_first (eq2 d) ppc of
1.19 - NONE => Add (i, [], true, f,
1.20 - Cor ((d, ts), (id, pbl_ids' d ts))
1.21 - )
1.22 - | SOME (i', _, _, _, itm_) => if is_list_dsc d then
1.23 - let
1.24 - val in_itm = ts_in itm_;
1.25 - val ts' = union op = ts in_itm;
1.26 - val i'' = if in_itm = [] then i else i';
1.27 - in Add (i'', [], true, f,
1.28 - Cor ((d, ts'), (id, pbl_ids' d ts'))
1.29 - )
1.30 - end else
1.31 - Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
1.32 - end)
1.33 - end
1.34 + in
1.35 + case parseNEW ctxt ct of
1.36 + NONE => Add (i, [], false, sel, Syn ct)
1.37 + | SOME t =>
1.38 + let val (d, ts) = split_dts t;
1.39 + in
1.40 + if d = e_term
1.41 + then Add (i, [], false, sel, Mis (dsc_unknown, hd ts))
1.42 + else
1.43 + (case find_first (eq1 d) pbt of
1.44 + NONE => Add (i, [], true, sel, Sup (d,ts))
1.45 + | SOME (f, (_, id)) =>
1.46 + let fun eq2 d (i, _, _, _, itm_) =
1.47 + d = (d_in itm_) andalso i <> 0;
1.48 + in case find_first (eq2 d) ppc of
1.49 + NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
1.50 + | SOME (i', _, _, _, itm_) =>
1.51 + if is_list_dsc d
1.52 + then
1.53 + let
1.54 + val in_itm = ts_in itm_;
1.55 + val ts' = union op = ts in_itm;
1.56 + val i'' = if in_itm = [] then i else i';
1.57 + in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts'))) end
1.58 + else Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
1.59 + end)
1.60 + end
1.61 end
1.62 | appl_add ctxt sel oris ppc pbt str =
1.63 case parseNEW ctxt str of
1.64 - NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
1.65 - | SOME t => case is_known ctxt sel oris t of
1.66 - ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
1.67 - ("", itm) => Add itm
1.68 - | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
1.69 + NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
1.70 + | SOME t =>
1.71 + case is_known ctxt sel oris t of
1.72 + ("", ori', all) =>
1.73 + (case is_notyet_input ctxt ppc all ori' pbt of
1.74 + ("", itm) => Add itm
1.75 + | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
1.76 | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
1.77 -(*
1.78 -> val (msg,itm) = is_notyet_input thy ppc all ori';
1.79 -val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
1.80 -> val itm_ = #5 itm;
1.81 -> val ts = ts_in itm_;
1.82 -> map (atomty) ts;
1.83 -*)
1.84 +
1.85
1.86 (** make oris from args of the stac SubProblem and from pbt **)
1.87 -
1.88 -(*.can this formal argument (of a model-pattern) be omitted in the arg-list
1.89 - of a SubProblem ? see ME/ptyps.sml 'type met '.*)
1.90 +(* can this formal argument (of a model-pattern) be omitted in the arg-list
1.91 + of a SubProblem ? see ME/ptyps.sml 'type met ' *)
1.92 fun is_copy_named_idstr str =
1.93 case (rev o Symbol.explode) str of
1.94 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))