1.1 --- a/src/Tools/isac/Interpret/model.sml Tue Mar 13 15:04:27 2018 +0100
1.2 +++ b/src/Tools/isac/Interpret/model.sml Thu Mar 15 10:17:44 2018 +0100
1.3 @@ -12,11 +12,11 @@
1.4 val oris2str : ori list -> string
1.5 val e_ori : ori
1.6 datatype item
1.7 - = Correct of cterm' | False of cterm' | Incompl of cterm' | Missing of cterm' | Superfl of string
1.8 + = Correct of Celem.cterm' | False of Celem.cterm' | Incompl of Celem.cterm' | Missing of Celem.cterm' | Superfl of string
1.9 | SyntaxE of string | TypeE of string
1.10 datatype itm_ = Cor of (term * (term list)) * (term * (term list))
1.11 - | Syn of cterm' | Typ of cterm' | Inc of (term * (term list)) * (term * (term list))
1.12 - | Sup of (term * (term list)) | Mis of (term * term) | Par of cterm'
1.13 + | Syn of Celem.cterm' | Typ of Celem.cterm' | Inc of (term * (term list)) * (term * (term list))
1.14 + | Sup of (term * (term list)) | Mis of (term * term) | Par of Celem.cterm'
1.15 val itm_2str : itm_ -> string
1.16 val itm_2str_ : Proof.context -> itm_ -> string
1.17 type itm
1.18 @@ -109,7 +109,7 @@
1.19 (b)
1.20 ==========================================================================*)
1.21
1.22 -val script_parse = the o (@{theory Script} |> thy2ctxt |> TermC.parseNEW);
1.23 +val script_parse = the o (@{theory Script} |> Celem.thy2ctxt |> TermC.parseNEW);
1.24 val e_listReal = script_parse "[]::(real list)";
1.25 val e_listBool = script_parse "[]::(bool list)";
1.26
1.27 @@ -149,21 +149,21 @@
1.28 then (d $ e_listReal)
1.29 else if LTool.is_booll_dsc d then (d $ e_listBool) else d
1.30 | comp_dts (d, ts) = (d $ (comp_ts (d, ts)))
1.31 - handle _ => error ("comp_dts: " ^ term2str d ^ " $ " ^ term2str (hd ts));
1.32 + handle _ => error ("comp_dts: " ^ Celem.term2str d ^ " $ " ^ Celem.term2str (hd ts));
1.33 fun comp_dts' (d, []) =
1.34 if LTool.is_reall_dsc d
1.35 then (d $ e_listReal)
1.36 else if LTool.is_booll_dsc d then (d $ e_listBool) else d
1.37 | comp_dts' (d, ts) = (d $ (comp_ts (d, ts)))
1.38 - handle _ => error ("comp_dts': " ^ term2str d ^ " $ " ^ term2str (hd ts));
1.39 + handle _ => error ("comp_dts': " ^ Celem.term2str d ^ " $ " ^ Celem.term2str (hd ts));
1.40 fun comp_dts'' (d, []) =
1.41 if LTool.is_reall_dsc d
1.42 - then term2str (d $ e_listReal)
1.43 + then Celem.term2str (d $ e_listReal)
1.44 else if LTool.is_booll_dsc d
1.45 - then term2str (d $ e_listBool)
1.46 - else term2str d
1.47 - | comp_dts'' (d, ts) = term2str (d $ (comp_ts (d, ts)))
1.48 - handle _ => error ("comp_dts'': " ^ term2str d ^ " $ " ^ term2str (hd ts));
1.49 + then Celem.term2str (d $ e_listBool)
1.50 + else Celem.term2str d
1.51 + | comp_dts'' (d, ts) = Celem.term2str (d $ (comp_ts (d, ts)))
1.52 + handle _ => error ("comp_dts'': " ^ Celem.term2str d ^ " $ " ^ Celem.term2str (hd ts));
1.53
1.54 (* decompose an input into description, terms (ev. elems of lists),
1.55 and the value for the problem-environment; inv to comp_dts *)
1.56 @@ -172,13 +172,13 @@
1.57 then if LTool.is_list_dsc d andalso TermC.is_list arg andalso LTool.is_unl d |> not
1.58 then (d, take_apart arg)
1.59 else (d, [arg])
1.60 - else (e_term, dest_list' t)
1.61 + else (Celem.e_term, dest_list' t)
1.62 | split_dts t =
1.63 let val t' as (h, _) = strip_comb t;
1.64 in
1.65 if LTool.is_dsc h
1.66 then (h, dest_list t')
1.67 - else (e_term, dest_list' t)
1.68 + else (Celem.e_term, dest_list' t)
1.69 end;
1.70 (* version returning ts only *)
1.71 fun split_dts' (d, arg) =
1.72 @@ -228,13 +228,13 @@
1.73 * (term list) (* [#0, epsilon] 9.5.03 outcommented *)
1.74 ) list;
1.75 fun pen2str ctxt (t, ts) =
1.76 - pair2str (term_to_string' ctxt t, (strs2str' o map (term_to_string' ctxt)) ts);
1.77 + pair2str (Celem.term_to_string' ctxt t, (strs2str' o map (Celem.term_to_string' ctxt)) ts);
1.78 fun penv2str_ thy penv = (strs2str' o (map (pen2str thy))) penv;
1.79
1.80 (* get the constant value from a penv *)
1.81 fun getval (id, values) =
1.82 case values of
1.83 - [] => error ("penv_value: no values in '" ^ term2str id)
1.84 + [] => error ("penv_value: no values in '" ^ Celem.term2str id)
1.85 | [v] => (id, v)
1.86 | (v1 :: v2 :: _) => (case v1 of
1.87 Const ("Script.Arbfix",_) => (id, v2)
1.88 @@ -248,7 +248,7 @@
1.89 fun mkval _(*dsc*) [] = error "mkval called with []"
1.90 | mkval _ [t] = t
1.91 | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
1.92 -fun mkval' x = mkval e_term x;
1.93 +fun mkval' x = mkval Celem.e_term x;
1.94
1.95 (* the internal representation of a models' item
1.96 4.9.01: not consistent:
1.97 @@ -259,13 +259,13 @@
1.98 Cor of (term * (* description *)
1.99 (term list)) * (* for list: elem-wise input *)
1.100 (term * (term list)) (* elem of penv ---- penv delayed to future *)
1.101 -| Syn of cterm'
1.102 -| Typ of cterm'
1.103 +| Syn of Celem.cterm'
1.104 +| Typ of Celem.cterm'
1.105 | Inc of (term * (term list)) * (term * (term list)) (*lists,
1.106 + init_pbl WN.11.03 FIXXME: empty penv .. bad; init_pbl should return Mis !!! *)
1.107 | Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*)
1.108 | Mis of (term * term) (* after re-specification pbt-item not found in pbl: only dsc, pid_*)
1.109 -| Par of cterm'; (* internal state from fun parsitm *)
1.110 +| Par of Celem.cterm'; (* internal state from fun parsitm *)
1.111
1.112 type vats = int list; (* variants in formalizations *)
1.113
1.114 @@ -326,19 +326,19 @@
1.115 term * (* description *)
1.116 term list (* isalist2list t | [t] *)
1.117 );
1.118 -val e_ori = (0, [], "", e_term, [e_term]) : ori;
1.119 +val e_ori = (0, [], "", Celem.e_term, [Celem.e_term]) : ori;
1.120
1.121 fun ori2str (i, vs, fi, t, ts) =
1.122 "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ "," ^
1.123 - term2str t ^ ", " ^ (strs2str o (map term2str)) ts ^ ")";
1.124 -val oris2str = strs2str' o (map (linefeed o ori2str));
1.125 + Celem.term2str t ^ ", " ^ (strs2str o (map Celem.term2str)) ts ^ ")";
1.126 +val oris2str = strs2str' o (map (Celem.linefeed o ori2str));
1.127
1.128 (* an or without leading integer *)
1.129 type preori = (vats * string * term * term list);
1.130 fun preori2str (vs, fi, t, ts) =
1.131 "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
1.132 - term2str t ^ ", " ^ (strs2str o (map term2str)) ts ^ ")";
1.133 -val preoris2str = (strs2str' o (map (linefeed o preori2str)));
1.134 + Celem.term2str t ^ ", " ^ (strs2str o (map Celem.term2str)) ts ^ ")";
1.135 +val preoris2str = (strs2str' o (map (Celem.linefeed o preori2str)));
1.136
1.137 (* given the input value (from split_dts)
1.138 make the value in a problem-env according to description-type
1.139 @@ -353,14 +353,14 @@
1.140 then [v] (*eg. [r=Arbfix]*)
1.141 else
1.142 (case v of (*eg. eps=#0*) (Const ("HOL.eq", _) $ l $ r) => [r, l]
1.143 - | _ => error ("pbl_ids Tools.nam: no equality " ^ term_to_string' ctxt v))
1.144 + | _ => error ("pbl_ids Tools.nam: no equality " ^ Celem.term_to_string' ctxt v))
1.145 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.una", _)]))) v = [v]
1.146 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.unl", _)]))) v = [v]
1.147 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.str", _)]))) v = [v]
1.148 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.toreal", _)]))) v = [v]
1.149 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.toreall", _)])))v = [v]
1.150 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.unknown" ,_)])))v = [v]
1.151 - | pbl_ids _ _ v = error ("pbl_ids: not implemented for " ^ term2str v);
1.152 + | pbl_ids _ _ v = error ("pbl_ids: not implemented for " ^ Celem.term2str v);
1.153
1.154 (* given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))
1.155 make the value in a problem-env according to description-type.
1.156 @@ -419,13 +419,13 @@
1.157
1.158 (* for _output_ of the items of a Model *)
1.159 datatype item =
1.160 - Correct of cterm' (* labels a correct formula (type cterm') *)
1.161 + Correct of Celem.cterm' (* labels a correct formula (type cterm') *)
1.162 | SyntaxE of string (**)
1.163 | TypeE of string (**)
1.164 - | False of cterm' (* WN050618 notexistent in itm_: only used in Where *)
1.165 - | Incompl of cterm' (**)
1.166 + | False of Celem.cterm' (* WN050618 notexistent in itm_: only used in Where *)
1.167 + | Incompl of Celem.cterm' (**)
1.168 | Superfl of string (**)
1.169 - | Missing of cterm';
1.170 + | Missing of Celem.cterm';
1.171 fun item2str (Correct s) ="Correct " ^ s
1.172 | item2str (SyntaxE s) ="SyntaxE " ^ s
1.173 | item2str (TypeE s) ="TypeE " ^ s
1.174 @@ -435,21 +435,21 @@
1.175 | item2str (Missing s) ="Missing " ^ s;
1.176 (*make string for error-msgs*)
1.177 fun itm_2str_ ctxt (Cor ((d, ts), penv)) =
1.178 - "Cor " ^ term_to_string' ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
1.179 + "Cor " ^ Celem.term_to_string' ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
1.180 | itm_2str_ _ (Syn c) = "Syn " ^ c
1.181 | itm_2str_ _ (Typ c) = "Typ " ^ c
1.182 | itm_2str_ ctxt (Inc ((d, ts), penv)) =
1.183 - "Inc " ^ term_to_string' ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
1.184 + "Inc " ^ Celem.term_to_string' ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
1.185 | itm_2str_ ctxt (Sup (d, ts)) =
1.186 - "Sup " ^ term_to_string' ctxt (comp_dts (d, ts))
1.187 + "Sup " ^ Celem.term_to_string' ctxt (comp_dts (d, ts))
1.188 | itm_2str_ ctxt (Mis (d, pid)) =
1.189 - "Mis "^ term_to_string' ctxt d ^ " " ^ term_to_string' ctxt pid
1.190 + "Mis "^ Celem.term_to_string' ctxt d ^ " " ^ Celem.term_to_string' ctxt pid
1.191 | itm_2str_ _ (Par s) = "Trm "^s;
1.192 -fun itm_2str t = itm_2str_ (thy2ctxt' "Isac") t;
1.193 +fun itm_2str t = itm_2str_ (Celem.thy2ctxt' "Isac") t;
1.194 fun itm2str_ ctxt ((i, is, b, s, itm_):itm) =
1.195 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
1.196 s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")";
1.197 -fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);
1.198 +fun itms2str_ ctxt itms = strs2str' (map (Celem.linefeed o (itm2str_ ctxt)) itms);
1.199 fun init_item str = SyntaxE str;
1.200
1.201 type 'a ppc =
1.202 @@ -489,14 +489,14 @@
1.203 | d_in (Mis (d, _)) = d
1.204 | d_in _ = error "d_in: uncovered case in fun.def.";
1.205
1.206 -fun dts2str (d, ts) = pair2str (term2str d, terms2str ts);
1.207 +fun dts2str (d, ts) = pair2str (Celem.term2str d, Celem.terms2str ts);
1.208 fun penvval_in (Cor ((d, _), (_, ts))) = [comp_ts (d,ts)]
1.209 | penvval_in (Syn (c)) = (tracing("*** penvval_in: Syn ("^c^")"); [])
1.210 | penvval_in (Typ (c)) = (tracing("*** penvval_in: Typ ("^c^")"); [])
1.211 | penvval_in (Inc (_, (_, ts))) = ts
1.212 | penvval_in (Sup dts) = (tracing ("*** penvval_in: Sup "^(dts2str dts)); [])
1.213 | penvval_in (Mis (d, t)) = (tracing ("*** penvval_in: Mis " ^
1.214 - pair2str(term2str d, term2str t)); [])
1.215 + pair2str(Celem.term2str d, Celem.term2str t)); [])
1.216 | penvval_in _ = error "penvval_in: uncovered case in fun.def.";
1.217
1.218 (* check a predicate labelled with indication of incomplete substitution;
1.219 @@ -507,7 +507,7 @@
1.220 bool * (* has the precondition evaluated to true *)
1.221 term (* the precondition (for map) *)
1.222 *)
1.223 -fun pre2str (b, t) = pair2str(bool2str b, term2str t);
1.224 -fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
1.225 +fun pre2str (b, t) = pair2str(bool2str b, Celem.term2str t);
1.226 +fun pres2str pres = strs2str' (map (Celem.linefeed o pre2str) pres);
1.227
1.228 end;
1.229 \ No newline at end of file