1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Fri Oct 08 18:58:24 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Sat Oct 09 16:03:49 2010 +0200
1.3 @@ -15,16 +15,15 @@
1.4 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*)
1.5
1.6 fun itm_2item thy (Cor ((d,ts),_)) =
1.7 - Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
1.8 + Correct (term2str (comp_dts thy (d,ts)))
1.9 | itm_2item _ (Syn c) = SyntaxE c
1.10 | itm_2item _ (Typ c) = TypeE c
1.11 | itm_2item thy (Inc ((d,ts),_)) =
1.12 - Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
1.13 + Incompl (term2str (comp_dts thy (d,ts)))
1.14 | itm_2item thy (Sup (d,ts)) =
1.15 - Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
1.16 + Superfl (term2str (comp_dts thy (d,ts)))
1.17 | itm_2item _ (Mis (d,pid)) =
1.18 - Missing (Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^
1.19 - Syntax.string_of_term (thy2ctxt' "Isac") pid);
1.20 + Missing (term2str d ^ " " ^ term2str pid);
1.21
1.22
1.23 (* --- 8.3.00
1.24 @@ -98,8 +97,7 @@
1.25 then (hd, args)
1.26 else (e_term, [t]) (*??? 9.01 just copied*)
1.27 end)
1.28 - handle _ => error ("split_dsc: called with "^
1.29 - (Syntax.string_of_term (thy2ctxt' "Isac") t));
1.30 + handle _ => error ("split_dsc: called with " ^ term2str t);
1.31 (*
1.32 > val t1 = (term_of o the o (parse thy)) "errorBound err_";
1.33 > split_dsc t1;
1.34 @@ -128,51 +126,18 @@
1.35 fun split_did t =
1.36 (let val (hd,[arg]) = strip_comb t
1.37 in (hd,arg) end)
1.38 - handle _ => error ("split_did: doesn't match (hd,[arg]) for t = "
1.39 - ^(Syntax.string_of_term (thy2ctxt' "Script") t));
1.40 + handle _ =>
1.41 + error ("split_did: doesn't match (hd,[arg]) for t = " ^term2str t);
1.42
1.43
1.44
1.45 (*create output-string for itm_*)
1.46 -fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
1.47 +fun itm_out thy (Cor ((d,ts),_)) = term2str (comp_dts thy(d,ts))
1.48 | itm_out thy (Syn c) = c
1.49 | itm_out thy (Typ c) = c
1.50 - | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
1.51 - | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
1.52 - | itm_out thy (Mis (d,pid)) =
1.53 - Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^
1.54 - Syntax.string_of_term (thy2ctxt' "Isac") pid;
1.55 -
1.56 -(*22.11.00 unused
1.57 -fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*)
1.58 -
1.59 -
1.60 -(*--3.3.
1.61 -fun itms2dts itms =
1.62 - let
1.63 - fun coll itms' [] = itms'
1.64 - | coll itms' (i::itms) =
1.65 - case i of
1.66 - (Cor (d,ts)) => coll (itms' @ [(d,ts)]) itms
1.67 - | (Syn c) => coll (itms' ) itms
1.68 - | (Typ c) => coll (itms' ) itms
1.69 - | (Fal (d,ts)) => coll (itms' @ [(d,ts)]) itms
1.70 - | (Inc (d,ts)) => coll (itms' @ [(d,ts)]) itms
1.71 - | (Sup (d,ts)) => coll (itms' @ [(d,ts)]) itms
1.72 - in coll [] itms end;
1.73 -*)
1.74 -(*--3.3.00
1.75 -fun itm2item ((_,_,_,_,Cor (d,ts)):itm) =
1.76 - Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
1.77 - | itm2item (_,_,_,_,Syn (c)) = SyntaxE c
1.78 - | itm2item (_,_,_,_,Typ (c)) = TypeE c
1.79 - | itm2item (_,_,_,_,Fal (d,ts)) =
1.80 - False (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
1.81 - | itm2item (_,_,_,_,Inc (d,ts)) =
1.82 - Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
1.83 - | itm2item (_,_,_,_,Sup (d,ts)) =
1.84 - Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)));
1.85 -*)
1.86 + | itm_out thy (Inc ((d,ts),_)) = term2str (comp_dts thy(d,ts))
1.87 + | itm_out thy (Sup (d,ts)) = term2str (comp_dts thy(d,ts))
1.88 + | itm_out thy (Mis (d,pid)) = term2str d ^ " " ^ term2str pid;
1.89
1.90 fun boolterm2item (true, term) = Correct (term2str term)
1.91 | boolterm2item (false, term) = False (term2str term);
1.92 @@ -186,22 +151,6 @@
1.93 coll (add_sel_ppc thy field ppc (itm_2item thy itm_)) itms;
1.94 val gfr = coll empty_ppc itms;
1.95 in add_where gfr (map boolterm2item pre) end;
1.96 -(*-----------------------------------------^^^-(3) aus modspec.sml 23.3.02*)
1.97 -
1.98 -(*-----------------------------------------vvv-(4) aus modspec.sml 23.3.02*)
1.99 -
1.100 -(* --- 9.3.fun add_field dscs (d,ts) =
1.101 - if d mem (get_dsc_in dscs "#Given")
1.102 - then ("#Given",d,ts:term list)
1.103 - else if d mem (get_dsc_in dscs "#Find")
1.104 - then ("#Find",d,ts)
1.105 - else if d mem (get_dsc_in dscs "#Relate")
1.106 - then ("#Relate",d,ts)
1.107 - else ("#undef",d,ts);
1.108 -(* 28.1.00 error ("add_field: '"^
1.109 - (Syntax.string_of_term (thy2ctxt' "Isac") d)^
1.110 - "' not in ppc-description "); *)
1.111 - ------9.3. *)
1.112
1.113 (* 9.3.00
1.114 compare d and dsc in pbt and transfer field to pre-ori *)
1.115 @@ -210,9 +159,7 @@
1.116 in case filter (eq d) pbt of
1.117 [(fi,(dsc,_))] => (fi,d,ts)
1.118 | [] => ("#undef",d,ts) (*may come with met.ppc*)
1.119 - | _ => error ("add_field: "^
1.120 - (Syntax.string_of_term (thy2ctxt' "Isac") d)^
1.121 - " more than once in pbt")
1.122 + | _ => error ("add_field: " ^ term2str d ^ " more than once in pbt")
1.123 end;
1.124
1.125 (*. take over field from met.ppc at 'Specify_Method' into ori,
1.126 @@ -225,12 +172,7 @@
1.127 case filter (eq d) mpc of
1.128 [(fi,(dsc,_))] => [(i,v,fi,d,ts)]
1.129 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
1.130 - (*error ("add_field': "^
1.131 - (Syntax.string_of_term (thy2ctxt' "Isac") d)^
1.132 - " not in met"*)
1.133 - | _ => error ("add_field': "^
1.134 - (Syntax.string_of_term (thy2ctxt' "Isac") d)^
1.135 - " more than once in met");
1.136 + | _ => error ("add_field': " ^ term2str d ^ " more than once in met");
1.137 in (flat ((map (repl mpc)) ori)):ori list end;
1.138
1.139