1.1 --- a/src/Tools/isac/Interpret/calchead.sml Tue Sep 14 15:46:56 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Thu Sep 23 08:43:36 2010 +0200
1.3 @@ -922,9 +922,6 @@
1.4 > map (atomty) ts;
1.5 *)
1.6
1.7 -(*---------------------------------------------(4) nach ptyps.sml 23.3.02*)
1.8 -
1.9 -
1.10 (** make oris from args of the stac SubProblem and from pbt **)
1.11
1.12 (*.can this formal argument (of a model-pattern) be omitted in the arg-list
1.13 @@ -932,9 +929,10 @@
1.14 fun is_copy_named_idstr str =
1.15 case (rev o explode) str of
1.16 (*"_":: _ ::"_"::_ => true*)
1.17 - "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o explode)) str ^ " T");
1.18 - true)
1.19 - | _ => (tracing ((strs2str o (rev o explode)) str ^ " F"); false);
1.20 + "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o explode))
1.21 + "is_copy_named_idstr: " ^ str ^ " T"); true)
1.22 + | _ => (tracing ((strs2str o (rev o explode))
1.23 + "is_copy_named_idstr: " ^ str ^ " F"); false);
1.24 fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o free2str) t;
1.25
1.26 (*.should this formal argument (of a model-pattern) create a new identifier?.*)
1.27 @@ -951,25 +949,6 @@
1.28 (*.split type-wrapper from scr-arg and build part of an ori;
1.29 an type-error is reported immediately, raises an exn,
1.30 subsequent handling of exn provides 2nd part of error message.*)
1.31 -(*fun mtc thy ((str, (dsc, _)):pat) (ty $ var) = WN100820 made cterm to term
1.32 - (* val (thy, (str, (dsc, _)), (ty $ var)) =
1.33 - (thy, p, a);
1.34 - *)
1.35 - (cterm_of thy (dsc $ var);(*type check*)
1.36 - SOME ((([1], str, dsc, (*[var]*)
1.37 - split_dts' (dsc, var))): preori)(*:ori without leading #*))
1.38 - handle e as TYPE _ =>
1.39 - (writeln (dashs 70^"\n"
1.40 - ^"*** ERROR while creating the items for the model of the ->problem\n"
1.41 - ^"*** from the ->stac with ->typeconstructor in arglist:\n"
1.42 - ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
1.43 - ^"*** description: "^(term_detail2str dsc)
1.44 - ^"*** value: "^(term_detail2str var)
1.45 - ^"*** typeconstructor in script: "^(term_detail2str ty)
1.46 - ^"*** checked by theory: "^(theory2str thy)^"\n"
1.47 - ^"*** "^dots 66);
1.48 - print_exn e; (*raises exn again*)
1.49 - NONE);*)
1.50 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
1.51 (* val (thy, (str, (dsc, _)), (ty $ var)) =
1.52 (thy, p, a);
1.53 @@ -977,27 +956,19 @@
1.54 (cterm_of thy (dsc $ var);(*type check*)
1.55 SOME ((([1], str, dsc, (*[var]*)
1.56 split_dts' (dsc, var))): preori)(*:ori without leading #*))
1.57 - handle e as TYPE _ =>
1.58 - (writeln (dashs 70^"\n"
1.59 - ^"*** ERROR while creating the items for the model of the ->problem\n"
1.60 - ^"*** from the ->stac with ->typeconstructor in arglist:\n"
1.61 - ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
1.62 - ^"*** description: "^(term_detail2str dsc)
1.63 - ^"*** value: "^(term_detail2str var)
1.64 - ^"*** typeconstructor in script: "^(term_detail2str ty)
1.65 - ^"*** checked by theory: "^(theory2str thy)^"\n"
1.66 - ^"*** "^dots 66);
1.67 - (*WN100820 postponed: print_exn e; raises exn again*)
1.68 - NONE);
1.69 -(*> val pbt = (#ppc o get_pbt) ["univariate","equation"];
1.70 -> val Const ("Script.SubProblem",_) $
1.71 - (Const ("Pair",_) $ Free (thy', _) $
1.72 - (Const ("Pair",_) $ pblID' $ metID')) $ ags =
1.73 - str2term"(SubProblem (SqRoot_,[univariate,equation],\
1.74 - \[SqRoot_,solve_linear]) [BOOL (x+1- 2=0), REAL x])::bool list";
1.75 -> val ags = isalist2list ags;
1.76 -> mtc thy (hd pbt) (hd ags);
1.77 -val it = SOME ([1],"#Given",Const (#,#),[# $ #]) *)
1.78 + handle e as TYPE _ =>
1.79 + (writeln (dashs 70 ^ "\n"
1.80 + ^"*** ERROR while creating the items for the model of the ->problem\n"
1.81 + ^"*** from the ->stac with ->typeconstructor in arglist:\n"
1.82 + ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
1.83 + ^"*** description: "^(term_detail2str dsc)
1.84 + ^"*** value: "^(term_detail2str var)
1.85 + ^"*** typeconstructor in script: "^(term_detail2str ty)
1.86 + ^"*** checked by theory: "^(theory2str thy)^"\n"
1.87 + ^"*** " ^ dots 66);
1.88 + OldGoals.print_exn e; (*raises exn again*)
1.89 + (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
1.90 + NONE);
1.91
1.92 (*.match each pat of the model-pattern with an actual argument;
1.93 precondition: copy-named vars are filtered out.*)
1.94 @@ -1030,19 +1001,20 @@
1.95 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)
1.96
1.97
1.98 -(*WN051014 outcommented with redesign copy-named (for omitting '#Find'
1.99 - in SubProblem);
1.100 - kept as initial idea for generating x_1, x_2, ... for equations*)
1.101 +(* generate a new variable "x_i" name from a related given one "x"
1.102 + by use of oris relating "v_i_" (is_copy_named!) to "v_"
1.103 + e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)
1.104 +
1.105 +(* generate a new variable "x_i" name from a related given one "x"
1.106 + by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"
1.107 + e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i) *)
1.108 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =
1.109 -(* val ((pbt:pat list), (oris:preori list), ((field,(dsc,t)):pat)) =
1.110 - (pbt', oris', hd (*!!!!!*) cy);
1.111 - *)
1.112 (if is_copy_named_generating p
1.113 then (*WN051014 kept strange old code ...*)
1.114 let fun sel (_,_,d,ts) = comp_ts (d, ts)
1.115 - val cy' = (implode o drop_last o drop_last o explode o free2str) t
1.116 + val cy' = (implode o (drop_last_n 3) o explode o free2str) t
1.117 val ext = (last_elem o drop_last o explode o free2str) t
1.118 - val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*)
1.119 + val vars' = map (free2str o snd o snd) pbt (*cpy-nam filtered_out*)
1.120 val vals = map sel oris
1.121 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext
1.122 in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end
1.123 @@ -1050,39 +1022,20 @@
1.124 )
1.125 handle _ => raise error ("cpy_nam: for "^(term2str t));
1.126
1.127 -(*> val (field,(dsc,t)) = last_elem pbt;
1.128 -> cpy_nam pbt (drop_last oris) (field,(dsc,t));
1.129 -val it = ([1],"#Find",
1.130 - Const ("Descript.solutions","bool List.list => Tools.toreall"),
1.131 - [Free ("x_i","bool List.list")]) *)
1.132 -
1.133 -
1.134 (*.match the actual arguments of a SubProblem with a model-pattern
1.135 and create an ori list (in root-pbl created from formalization).
1.136 expects ags:pats = 1:1, while copy-named are filtered out of pats;
1.137 + if no 1:1 the exn raised by matc/mtc and handled at call.
1.138 copy-named pats are appended in order to get them into the model-items.*)
1.139 fun match_ags thy (pbt:pat list) ags =
1.140 -(* val (thy, pbt, ags) = (thy, (#ppc o get_pbt) pI, ags);
1.141 - val (thy, pbt, ags) = (thy, pats, ags);
1.142 - *)
1.143 let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);
1.144 val pbt' = filter_out is_copy_named pbt;
1.145 val cy = filter is_copy_named pbt;
1.146 val oris' = matc thy pbt' ags [];
1.147 val cy' = map (cpy_nam pbt' oris') cy;
1.148 val ors = add_id (oris' @ cy');
1.149 - (*appended in order to get ^^^^^ them into the model-items*)
1.150 + (*appended in order to get ^^^^^ into the model-items*)
1.151 in (map flattup ors):ori list end;
1.152 -(*vars as above ..
1.153 -> match_ags thy pbt ags;
1.154 -val it =
1.155 - [(1,[1],"#Given",Const ("Descript.equality","bool => Tools.una"),
1.156 - [Const # $ (# $ #) $ Free (#,#)]),
1.157 - (2,[1],"#Given",Const ("Descript.solveFor","RealDef.real => Tools.una"),
1.158 - [Free ("x","RealDef.real")]),
1.159 - (3,[1],"#Find",
1.160 - Const ("Descript.solutions","bool List.list => Tools.toreall"),
1.161 - [Free ("x_i","bool List.list")])] : ori list*)
1.162
1.163 (*.report part of the error-msg which is not available in match_args.*)
1.164 fun match_ags_msg pI stac ags =
1.165 @@ -1095,6 +1048,7 @@
1.166 ^"*** stac '"^term2str stac^"' has the ...\n"
1.167 ^"*** arg-list "^terms2str ags^"\n"
1.168 ^dashs 70)
1.169 + (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
1.170 val _ = show_types:= s
1.171 in writeln msg end;
1.172