wneuper/isa: comparison src/Tools/isac/Interpret/model.sml

equal deleted inserted replaced

-:6a2753b8d70c
+:49d7d410b83c
 sig
 type ori
 val oris2str : ori list -> string
 val e_ori : ori
 datatype item
-= Correct of cterm' | False of cterm' | Incompl of cterm' | Missing of cterm' | Superfl of string
+= Correct of Celem.cterm' | False of Celem.cterm' | Incompl of Celem.cterm' | Missing of Celem.cterm' | Superfl of string
 | SyntaxE of string | TypeE of string
 datatype itm_ = Cor of (term * (term list)) * (term * (term list))
-| Syn of cterm' | Typ of cterm' | Inc of (term * (term list))	* (term * (term list))
+| Syn of Celem.cterm' | Typ of Celem.cterm' | Inc of (term * (term list))	* (term * (term list))
-| Sup of (term * (term list)) | Mis of (term * term) | Par of cterm'
+| Sup of (term * (term list)) | Mis of (term * term) | Par of Celem.cterm'
 val itm_2str : itm_ -> string
 val itm_2str_ : Proof.context -> itm_ -> string
 type itm
 val itm2str_ : Proof.context -> itm -> string
 val itms2str_ : Proof.context -> itm list -> string
 wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????:
 (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid)  dh.vt neu  ????
 (b)
 ==========================================================================*)
-val script_parse = the o (@{theory Script} |> thy2ctxt |> TermC.parseNEW);
+val script_parse = the o (@{theory Script} |> Celem.thy2ctxt |> TermC.parseNEW);
 val e_listReal = script_parse "[]::(real list)";
 val e_listBool = script_parse "[]::(bool list)";
 (* take list-term apart w.r.t. handling elementwise input: @{term "[a, b]"} \<rightarrow> ["[a]","[b]"] *)
 fun take_apart t =
 fun comp_dts (d, []) =
 	if LTool.is_reall_dsc d
 	then (d $ e_listReal)
 	else if LTool.is_booll_dsc d then (d $ e_listBool) else d
 | comp_dts (d, ts) = (d $ (comp_ts (d, ts)))
-handle _ => error ("comp_dts: " ^ term2str d ^ " $ " ^ term2str (hd ts));
+handle _ => error ("comp_dts: " ^ Celem.term2str d ^ " $ " ^ Celem.term2str (hd ts));
 fun comp_dts' (d, []) =
 if LTool.is_reall_dsc d
 then (d $ e_listReal)
 else if LTool.is_booll_dsc d then (d $ e_listBool) else d
 | comp_dts' (d, ts) = (d $ (comp_ts (d, ts)))
-handle _ => error ("comp_dts': " ^ term2str d ^ " $ " ^ term2str (hd ts));
+handle _ => error ("comp_dts': " ^ Celem.term2str d ^ " $ " ^ Celem.term2str (hd ts));
 fun comp_dts'' (d, []) =
 if LTool.is_reall_dsc d
-then term2str (d $ e_listReal)
+then Celem.term2str (d $ e_listReal)
 else if LTool.is_booll_dsc d
-then term2str (d $ e_listBool)
+then Celem.term2str (d $ e_listBool)
-else term2str d
+else Celem.term2str d
-| comp_dts'' (d, ts) = term2str (d $ (comp_ts (d, ts)))
+| comp_dts'' (d, ts) = Celem.term2str (d $ (comp_ts (d, ts)))
-handle _ => error ("comp_dts'': " ^ term2str d ^ " $ " ^ term2str (hd ts));
+handle _ => error ("comp_dts'': " ^ Celem.term2str d ^ " $ " ^ Celem.term2str (hd ts));
 (* decompose an input into description, terms (ev. elems of lists),
 and the value for the problem-environment; inv to comp_dts   *)
 fun split_dts (t as d $ arg) =
 if LTool.is_dsc d
 then if LTool.is_list_dsc d andalso TermC.is_list arg andalso LTool.is_unl d |> not
 then (d, take_apart arg)
 else (d, [arg])
-else (e_term, dest_list' t)
+else (Celem.e_term, dest_list' t)
 | split_dts t =
 let val t' as (h, _) = strip_comb t;
 in
 if LTool.is_dsc h
 then (h, dest_list t')
-else (e_term, dest_list' t)
+else (Celem.e_term, dest_list' t)
 end;
 (* version returning ts only *)
 fun split_dts' (d, arg) =
 if LTool.is_dsc d
 then if LTool.is_list_dsc d
 type penv = (* problem-environment *)
 (term           (* err_                              *)
 	 * (term list)  (* [#0, epsilon] 9.5.03 outcommented *)
 	) list;
 fun pen2str ctxt (t, ts) =
-pair2str (term_to_string'  ctxt t, (strs2str' o map (term_to_string'  ctxt)) ts);
+pair2str (Celem.term_to_string' ctxt t, (strs2str' o map (Celem.term_to_string'  ctxt)) ts);
 fun penv2str_ thy penv = (strs2str' o (map (pen2str thy))) penv;
 (* get the constant value from a penv *)
 fun getval (id, values) =
 case values of
-	  [] => error ("penv_value: no values in '" ^ term2str id)
+	  [] => error ("penv_value: no values in '" ^ Celem.term2str id)
 | [v] => (id, v)
 | (v1 :: v2 :: _) => (case v1 of
 	      Const ("Script.Arbfix",_) => (id, v2)
 	    | _ => (id, v1));
 (* 14.9.01: not used after putting penv-values into itm_
 make the result of split_* a value of problem-environment *)
 fun mkval _(*dsc*) [] = error "mkval called with []"
 | mkval _ [t] = t
 | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
-fun mkval' x = mkval e_term x;
+fun mkval' x = mkval Celem.e_term x;
 (* the internal representation of a models' item
 4.9.01: not consistent:
 after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation
 (involves 'is_error');
 bool in itm really necessary ???*)
 datatype itm_ =
 Cor of (term *              (* description                                                     *)
 (term list)) *            (* for list: elem-wise input                                       *)
 (term * (term list))       (* elem of penv ---- penv delayed to future                        *)
-| Syn of cterm'
+| Syn of Celem.cterm'
-| Typ of cterm'
+| Typ of Celem.cterm'
 | Inc of (term * (term list))	* (term * (term list)) (*lists,
 			+ init_pbl WN.11.03 FIXXME: empty penv .. bad; init_pbl should return Mis !!!              *)
 | Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*)
 | Mis of (term * term)        (* after re-specification pbt-item not found in pbl: only dsc, pid_*)
-| Par of cterm';              (* internal state from fun parsitm                                 *)
+| Par of Celem.cterm';              (* internal state from fun parsitm                                 *)
 type vats = int list; (* variants in formalizations *)
 (* data-type for working on pbl/met-ppc:
 in pbl initially holds descriptions (only) for user guidance *)
 	vats *     (* variants 21.3.02: related to pbt..discard ?                             *)
 	string *   (* #Given | #Find | #Relate 21.3.02: discard ?                             *)
 	term *     (* description                                                             *)
 	term list  (* isalist2list t | [t]                                                    *)
 	);
-val e_ori = (0, [], "", e_term, [e_term]) : ori;
+val e_ori = (0, [], "", Celem.e_term, [Celem.e_term]) : ori;
 fun ori2str (i, vs, fi, t, ts) =
 "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ "," ^
-term2str t ^ ", " ^ (strs2str o (map term2str)) ts ^ ")";
+Celem.term2str t ^ ", " ^ (strs2str o (map Celem.term2str)) ts ^ ")";
-val oris2str = strs2str' o (map (linefeed o ori2str));
+val oris2str = strs2str' o (map (Celem.linefeed o ori2str));
 (* an or without leading integer *)
 type preori = (vats * string * term * term list);
 fun preori2str (vs, fi, t, ts) =
 "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
-term2str t ^ ", " ^ (strs2str o (map term2str)) ts ^ ")";
+Celem.term2str t ^ ", " ^ (strs2str o (map Celem.term2str)) ts ^ ")";
-val preoris2str = (strs2str' o (map (linefeed o preori2str)));
+val preoris2str = (strs2str' o (map (Celem.linefeed o preori2str)));
 (* given the input value (from split_dts)
 make the value in a problem-env according to description-type
 28.8.01: .nam and .una impl. properly, others copied .. TODO.
 19/03/15 17:33, Makarius wrote:
 fun pbl_ids ctxt (Const(_, Type ("fun", [_, Type ("Tools.nam", _)]))) v =
 if TermC.is_list v
 then [v]      (*eg. [r=Arbfix]*)
 else
 (case v of  (*eg. eps=#0*) (Const ("HOL.eq", _) $ l $ r) => [r, l]
-	    | _ => error ("pbl_ids Tools.nam: no equality " ^ term_to_string' ctxt v))
+	    | _ => error ("pbl_ids Tools.nam: no equality " ^ Celem.term_to_string' ctxt v))
 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.una", _)]))) v = [v]
 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.unl", _)]))) v = [v]
 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.str", _)]))) v = [v]
 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.toreal", _)]))) v = [v]
 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.toreall", _)])))v = [v]
 | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Tools.unknown" ,_)])))v = [v]
-| pbl_ids _ _ v = error ("pbl_ids: not implemented for " ^ term2str v);
+| pbl_ids _ _ v = error ("pbl_ids: not implemented for " ^ Celem.term2str v);
 (* given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))
 make the value in a problem-env according to description-type.
 28.8.01: .nam and .una impl. properly, others copied .. TODO
 fun pbl_ids' (Const(_, Type ("fun", [_, Type ("Tools.nam", _)]))) vs =
 | upds_envv thy envv ((vs, dsc, id, vl) :: ps) =
 upds_envv thy (upd_envv thy envv vs dsc id vl) ps;
 (* for _output_ of the items of a Model *)
 datatype item =
-Correct of cterm' (* labels a correct formula (type cterm') *)
+Correct of Celem.cterm' (* labels a correct formula (type cterm') *)
 | SyntaxE of string (**)
 | TypeE   of string (**)
-| False   of cterm' (* WN050618 notexistent in itm_: only used in Where *)
+| False   of Celem.cterm' (* WN050618 notexistent in itm_: only used in Where *)
-| Incompl of cterm' (**)
+| Incompl of Celem.cterm' (**)
 | Superfl of string (**)
-| Missing of cterm';
+| Missing of Celem.cterm';
 fun item2str (Correct  s) ="Correct " ^ s
 | item2str (SyntaxE  s) ="SyntaxE " ^ s
 | item2str (TypeE    s) ="TypeE " ^ s
 | item2str (False    s) ="False " ^ s
 | item2str (Incompl  s) ="Incompl " ^ s
 | item2str (Superfl  s) ="Superfl " ^ s
 | item2str (Missing  s) ="Missing " ^ s;
 (*make string for error-msgs*)
 fun itm_2str_ ctxt (Cor ((d, ts), penv)) =
-"Cor " ^ term_to_string'  ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
+"Cor " ^ Celem.term_to_string'  ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
 | itm_2str_ _ (Syn c) = "Syn " ^ c
 | itm_2str_ _ (Typ c) = "Typ " ^ c
 | itm_2str_ ctxt (Inc ((d, ts), penv)) =
-"Inc " ^ term_to_string'  ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
+"Inc " ^ Celem.term_to_string'  ctxt (comp_dts (d, ts)) ^ " ," ^ pen2str ctxt penv
 | itm_2str_ ctxt (Sup (d, ts)) =
-"Sup " ^ term_to_string'  ctxt (comp_dts (d, ts))
+"Sup " ^ Celem.term_to_string'  ctxt (comp_dts (d, ts))
 | itm_2str_ ctxt (Mis (d, pid)) =
-"Mis "^ term_to_string'  ctxt d ^ " " ^ term_to_string'  ctxt pid
+"Mis "^ Celem.term_to_string'  ctxt d ^ " " ^ Celem.term_to_string'  ctxt pid
 | itm_2str_ _ (Par s) = "Trm "^s;
-fun itm_2str t = itm_2str_ (thy2ctxt' "Isac") t;
+fun itm_2str t = itm_2str_ (Celem.thy2ctxt' "Isac") t;
 fun itm2str_ ctxt ((i, is, b, s, itm_):itm) =
 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
 s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")";
-fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);
+fun itms2str_ ctxt itms = strs2str' (map (Celem.linefeed o (itm2str_ ctxt)) itms);
 fun init_item str = SyntaxE str;
 type 'a ppc =
 {Given : 'a list, Where: 'a list, Find  : 'a list, With : 'a list, Relate: 'a list};
 fun ppc2str {Given = Given, Where = Where, Find = Find, With = With, Relate = Relate}=
 | d_in (Inc ((d, _), _)) = d
 | d_in (Sup (d, _)) = d
 | d_in (Mis (d, _)) = d
 | d_in _ = error "d_in: uncovered case in fun.def.";
-fun dts2str (d, ts) = pair2str (term2str d, terms2str ts);
+fun dts2str (d, ts) = pair2str (Celem.term2str d, Celem.terms2str ts);
 fun penvval_in (Cor ((d, _), (_, ts))) = [comp_ts (d,ts)]
 | penvval_in (Syn  (c)) = (tracing("*** penvval_in: Syn ("^c^")"); [])
 | penvval_in (Typ  (c)) = (tracing("*** penvval_in: Typ ("^c^")"); [])
 | penvval_in (Inc (_, (_, ts))) = ts
 | penvval_in (Sup dts) = (tracing ("*** penvval_in: Sup "^(dts2str dts)); [])
 | penvval_in (Mis (d, t)) = (tracing ("*** penvval_in: Mis " ^
-			pair2str(term2str d, term2str t)); [])
+			pair2str(Celem.term2str d, Celem.term2str t)); [])
 	| penvval_in _ = error "penvval_in: uncovered case in fun.def.";
 (* check a predicate labelled with indication of incomplete substitution;
 rls ->    (* for eval_true                                               *)
 bool * 	  (* have _all_ variables(Free) from the model-pattern
 been substituted by a value from the pattern's environment ?*)
 term ->   (* the precondition                                            *)
 bool * 	  (* has the precondition evaluated to true                      *)
 term      (* the precondition (for map)                                  *)
 *)
-fun pre2str (b, t) = pair2str(bool2str b, term2str t);
+fun pre2str (b, t) = pair2str(bool2str b, Celem.term2str t);
-fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);
+fun pres2str pres = strs2str' (map (Celem.linefeed o pre2str) pres);
 end;

changeset 59405	49d7d410b83c
parent 59389	627d25067f2f
child 59416	229e5c9cf78b