walther@59938: (* Title: Specify/o-model.sml walther@59938: Author: Walther Neuper 110226 walther@59938: (c) due to copyright terms walther@59953: walther@60004: An \O_Model\ holds \O\riginal data, \descriptor\ and \values\ parsed from \Formalise.model\ walther@60004: selected with respect to a \Model_Pattern\ and combined with respective \m_field\s. walther@60004: \complete_for\ a \Model_Pattern\ is done by \Tactic.Model_Problem\ walther@60004: (with defaults from \Formalise\refs), by \Tactic.Specify_Problem\ and \Tactic.Specify_Method\ walther@60004: walther@60004: \O_Model\ serves efficiency of student's interactive modelling via \I_Model\. walther@60004: walther@60004: \O_Model\ marks elements with \m_field\ \#undef\, which are not required by the \Model_Pattern\ walther@60154: of the \Problem\ or the \MethodC\ .. TODO redes: \m_field\ probably different in root..Subproblem walther@59998: walther@59953: TODO: revise with an example with more than 1 variant. walther@60004: + consider: drop m_field ? walther@59953: *) walther@59938: walther@59938: signature ORIGINAL_MODEL = walther@59938: sig walther@59961: type T Walther@60442: val empty: T walther@59961: type single walther@60018: type variant walther@59961: type variants walther@59961: type m_field walther@59961: type descriptor walther@59998: type values walther@59999: type message Walther@60655: val to_string: Proof.context -> T -> string Walther@60655: val single_to_string: Proof.context -> single -> string walther@59940: val single_empty: single walther@59939: Walther@60653: val init: theory -> Formalise.model -> Model_Pattern.T -> T * Proof.context walther@59969: val values : T -> term list Walther@60609: val values': Proof.context -> T -> Formalise.model * term list walther@60009: val complete_for: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context Walther@60471: val associate_input: Proof.context -> m_field(*del?*) -> descriptor * values -> T -> message * single * values Walther@60471: val associate_input': Proof.context -> m_field -> values -> T -> message * single * values Walther@60471: val contains: Proof.context -> m_field -> T -> term -> message * single * values Walther@60471: val make_typeless: term -> term walther@60000: val test_types: Proof.context -> descriptor * values -> string walther@59969: Walther@60472: val add_enumerate: 'a list -> (int * 'a) list walther@59961: type preori Walther@60473: val copy_name: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori walther@59986: val is_copy_named: Model_Pattern.single -> bool Walther@60475: val is_copy_named': string -> bool Walther@60469: val is_copy_named_generating: Model_Pattern.single -> bool Walther@60469: walther@60251: \<^isac_test>\ walther@59986: val is_copy_named_generating_idstr: string -> bool Walther@60475: val string_of_preoris : preori list -> string walther@59998: val add_field: theory -> Model_Pattern.T -> descriptor * values -> m_field * descriptor * values Walther@60475: walther@59952: val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list Walther@60734: val get_max_variant: variants -> variant Walther@60475: val partition_variants: ('a * 'a -> bool) -> 'a list -> (int * 'a) list Walther@60475: val collect_variants: ('a * ''b) list -> ('a list * ''b) list Walther@60475: walther@59947: val replace_0: int -> int list -> int list walther@59947: val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e wenzelm@60223: \ walther@59938: end walther@59938: walther@59974: (**) walther@59938: structure O_Model(**) : ORIGINAL_MODEL(**) = walther@59938: struct walther@59974: (**) walther@59938: walther@59960: (** types **) walther@59960: walther@60018: type variant = Model_Def.variant; walther@59940: type variants = Model_Def.variants; walther@59952: type m_field = Model_Def.m_field; walther@59952: type descriptor = Model_Def.descriptor; Walther@60766: type values = Model_Def.values; walther@59999: type message = string; walther@59938: walther@59940: type T = Model_Def.o_model; Walther@60442: val empty = [] : Model_Def.o_model; walther@59940: type single = Model_Def.o_model_single walther@59940: val single_empty = Model_Def.o_model_empty; Walther@60655: walther@59957: val single_to_string = Model_Def.o_model_single_to_string; walther@59940: val to_string = Model_Def.o_model_to_string; walther@59940: walther@59952: (* O_Model.single without leading integer *) walther@59952: type preori = (variants * m_field * term * term list); walther@60268: \<^isac_test>\ walther@59942: fun preori2str (vs, fi, t, ts) = walther@59942: "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^ Walther@60678: UnparseC.term (ContextC.for_ERROR ()) t ^ ", " ^ Walther@60678: (strs2str o (map (UnparseC.term (ContextC.for_ERROR ())) ) ) ts ^ ")"; Walther@60475: val string_of_preoris = (strs2str' o (map (linefeed o preori2str))); walther@60268: \ walther@59942: walther@59960: walther@59960: (** initialise O_Model **) walther@59960: Walther@60586: (* compare d and dsc in pbt and transfer field to where_-ori *) Walther@60673: fun add_field thy pbt (d,ts) = walther@59947: let fun eq d pt = (d = (fst o snd) pt); walther@59947: in case filter (eq d) pbt of walther@59947: [(fi, (_, _))] => (fi, d, ts) Walther@60586: | [] => ("#undef", d, ts) (*may come with met.model*) Walther@60673: | _ => raise ERROR ("add_field: " ^ UnparseC.term_in_thy thy d ^ " more than once in pbt") walther@59947: end; walther@59947: walther@59952: (* walther@59952: mark an element with the position within a plateau; walther@59952: a plateau with length 1 is marked with 0 walther@59952: *) Walther@60475: fun partition_variants _ [] = raise ERROR "partition_variants []" Walther@60475: | partition_variants eq xs = walther@59952: let walther@59952: fun mar xx _ [x] n = xx @ [(if n = 1 then 0 else n, x)] Walther@60475: | mar _ _ [] _ = raise ERROR "partition_variants []" Walther@60475: | mar xx eq (x :: x' :: xs) n = Walther@60475: if eq (x, x') then mar (xx @ [(n, x)]) eq (x' :: xs) (n + 1) walther@59952: else mar (xx @ [(if n = 1 then 0 else n, x)]) eq (x' :: xs) 1; walther@59952: in mar [] eq xs 1 end; walther@59952: walther@59952: (* walther@59952: assumes equal descriptions to be in adjacent 'plateaus', walther@59952: items at a certain position within the plateaus form a variant; walther@59952: length = 1 ... marked with 0: covers all variants walther@59952: *) walther@59947: fun add_variants fdts = walther@59947: let walther@59947: fun eq (a, b) = curry op= (snd3 a) (snd3 b); Walther@60475: in partition_variants eq fdts end; walther@59947: Walther@60734: fun get_max_variant [] = raise ERROR "get_max_variant of []" Walther@60734: | get_max_variant (y :: ys) = walther@59947: let fun mx x [] = x walther@59947: | mx x (y :: ys) = if x < y then mx y ys else mx x ys; walther@59947: in mx y ys end; walther@59947: Walther@60475: fun collect_variants (((v,x) :: vxs)) = walther@59947: let walther@59947: fun col xs (vs, x) [] = xs @ [(vs, x)] walther@59947: | col xs (vs, x) ((v', x') :: vxs') = walther@59947: if x = x' then col xs (vs @ [v'], x') vxs' walther@59947: else col (xs @ [(vs, x)]) ([v'], x') vxs'; walther@59947: in col [] ([v], x) vxs end Walther@60475: | collect_variants _ = raise ERROR "collect_variants: called with []"; walther@59947: walther@59947: fun replace_0 vm [0] = intsto vm walther@59947: | replace_0 _ vs = vs; walther@59947: Walther@60472: fun add_enumerate [] = raise ERROR "O_Model.add_enumerate []" Walther@60472: | add_enumerate xs = walther@59947: let walther@59947: fun add _ [] = [] walther@59947: | add n (x :: xs) = (n, x) :: add (n + 1) xs; walther@59947: in add 1 xs end; walther@59947: walther@59947: fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e); walther@59947: Walther@60653: fun init _ [] _ = ([], ContextC.empty) Walther@60470: | init thy fmz pbt = walther@59947: let Walther@60656: val (ts, ctxt) = ContextC.init_while_parsing fmz thy Walther@60651: val model = Walther@60651: (map (fn t => t Walther@60651: |> Input_Descript.split Walther@60651: |> add_field thy pbt) ts) Walther@60651: |> add_variants; Walther@60734: val maxv = model |> map fst |> get_max_variant; Walther@60651: val maxv = if maxv = 0 then 1 else maxv; Walther@60651: val model' = model Walther@60651: |> collect_variants Walther@60651: |> map (replace_0 maxv |> apfst) Walther@60651: |> add_enumerate Walther@60651: |> map flattup Walther@60651: in (model', ctxt) end walther@59960: walther@59969: (** get the values **) walther@59969: walther@59969: fun mkval _(*dsc*) [] = raise ERROR "mkval called with []" walther@59969: | mkval _ [t] = t walther@59969: | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts; walther@59969: fun mkval' x = mkval TermC.empty x; Walther@60470: (* from an O_Model create values for ctxt *) Walther@60475: fun values oris = walther@59969: ((map (mkval' o (#5))) o (filter ((member_swap op= 1) o (#2)))) oris walther@59969: Walther@60470: (* from an O_Model create (Formalise.model, values) Walther@60470: e.g. Subproblem ["BOOL (1+x=2)", "REAL x"] Walther@60470: --match_ags--> O_Model.T Walther@60470: O_Model.T --values'--> (["equality (1+x=2)", "boundVariable x", "solutions L"], values) Walther@60470: *) Walther@60609: fun values' ctxt oris = Walther@60470: let Walther@60470: fun ori2fmz_vals (_, _, _, dsc, ts) = Walther@60675: case \<^try>\(((UnparseC.term ctxt) o Input_Descript.join') (dsc, ts), last_elem ts)\ of Walther@60470: SOME x => x Walther@60675: | NONE => raise ERROR ("O_Model.values' called with " ^ UnparseC.terms ctxt ts) Walther@60470: in (split_list o (map ori2fmz_vals)) oris end Walther@60470: walther@59986: walther@59998: (** complete wrt. Model_Pattern.T by use of root's O_Model.T **) walther@59998: walther@60009: fun complete_for m_patt root_model (o_model, ctxt) = walther@59998: let walther@59998: val missing = m_patt |> filter_out walther@60017: (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor)) walther@60001: val add = (root_model walther@60001: |> filter walther@60017: (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor)) walther@60009: in walther@60009: ((o_model @ add) walther@60011: |> map (fn (a, b, _, descr, e) => walther@60011: case Model_Pattern.get_field descr m_patt of walther@60011: SOME m_field => (a, b, m_field, descr, e) walther@60011: | NONE => (a, b, "#undef", descr, e)) Walther@60760: |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *) Walther@60760: |> add_enumerate (* for correct enumeration *) walther@60001: |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *) walther@59998: ctxt |> ContextC.add_constraints (add |> values |> TermC.vars')) walther@59998: end walther@59998: walther@59998: walther@59986: (** ? ? ? **) walther@59986: walther@59986: (* make oris from args of the stac SubProblem and from pbt. walther@59986: can this formal argument (of a model-pattern) be omitted in the arg-list walther@59986: of a SubProblem ? see calcelems.sml 'type met ' *) Walther@60475: fun is_copy_named' str = walther@59986: case (rev o Symbol.explode) str of walther@59986: "'" :: _ :: "'" :: _ => true walther@59986: | _ => false Walther@60475: fun is_copy_named (_, (_, t)) = (is_copy_named' o TermC.free2str) t walther@59986: walther@59986: (* should this formal argument (of a model-pattern) create a new identifier? *) walther@59986: fun is_copy_named_generating_idstr str = Walther@60475: if is_copy_named' str walther@59986: then walther@59986: case (rev o Symbol.explode) str of walther@59986: "'" :: "'" :: "'" :: _ => false walther@59986: | _ => true walther@59986: else false walther@59986: fun is_copy_named_generating (_, (_, t)) = (is_copy_named_generating_idstr o TermC.free2str) t walther@59986: walther@59986: (* generate a new variable "x_i" name from a related given one "x" walther@59986: by use of oris relating "v_v'i'" (is_copy_named!) to "v_v" walther@59986: e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i), walther@59986: but leave is_copy_named_generating as is, e.t. ss''' *) Walther@60473: fun copy_name pbt oris (p as (field, (dsc, t))) = walther@60265: case \<^try>\ walther@60265: if is_copy_named_generating p walther@60265: then (*WN051014 kept strange old code ...*) walther@60265: let fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts) walther@60265: val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t walther@60265: val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t walther@60265: val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*) walther@60265: val vals = map sel oris walther@60265: val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext walther@60265: in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end walther@60265: else ([1], field, dsc, [t]) walther@60265: \ of walther@60265: SOME x => x Walther@60678: | NONE => raise ERROR ("copy_name: for " ^ UnparseC.term (ContextC.for_ERROR ()) t) walther@59986: walther@59999: walther@60000: (** tools for I_Model **) walther@59999: Walther@60470: (* to an input (_ $ values) find the according O_Model.single and insert the values *) Walther@60471: fun associate_input ctxt m_field (descript, vals) [] = Walther@60471: ("associate_input: input ('" ^ Walther@60675: (UnparseC.term ctxt (Input_Descript.join (descript, vals))) ^ walther@60012: "') not found in oris (typed)", (0, [], m_field, descript, vals), []) Walther@60471: | associate_input ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) = walther@59999: if sel = sel' andalso d = d' andalso (inter op = ts ts') <> [] walther@59999: then ("", (id, vat, sel, d, inter op = ts ts'), ts') Walther@60471: else associate_input ctxt sel (d, ts) oris walther@59999: walther@60012: (* to an input (_ $ values) find the according O_Model.single and insert the values *) Walther@60471: fun associate_input' ctxt _ vals [] = Walther@60675: ("associate_input': input (_, '" ^ strs2str (map (UnparseC.term ctxt) vals) ^ walther@59999: "') not found in oris (typed)", single_empty, []) Walther@60471: | associate_input' ctxt m_field vals ((id, vat, m_field', descr, vals') :: oris) = walther@60012: if m_field = m_field' andalso (inter op = vals vals') <> [] walther@60012: then walther@60012: if m_field = m_field' walther@60012: then ("", (id, vat, m_field, descr, inter op = vals vals'), vals') Walther@60675: else ((strs2str' o map (UnparseC.term ctxt)) vals ^ walther@60012: " not for " ^ m_field, single_empty, []) Walther@60471: else associate_input' ctxt m_field vals oris walther@59999: walther@60000: fun test_types ctxt (d,ts) = walther@60000: let walther@60000: val opt = (try Input_Descript.join) (d, ts) walther@60000: val msg = case opt of walther@60000: SOME _ => "" Walther@60675: | NONE => (UnparseC.term ctxt d ^ " " ^ Walther@60675: (strs2str' o map (UnparseC.term ctxt)) ts ^ " is illtyped") walther@60000: in msg end walther@60000: walther@60000: (* make a term 'typeless' for comparing with another 'typeless' term; walther@60000: 'type-less' usually is illtyped *) Walther@60471: fun make_typeless (Const (s, _)) = (Const (s, TermC.typ_empty)) Walther@60471: | make_typeless (Free (s, _)) = (Free (s, TermC.typ_empty)) Walther@60471: | make_typeless (Var (n, _)) = (Var (n, TermC.typ_empty)) Walther@60471: | make_typeless (Bound i) = (Bound i) Walther@60471: | make_typeless (Abs (s, _,t)) = Abs(s, TermC.typ_empty, make_typeless t) Walther@60471: | make_typeless (t1 $ t2) = (make_typeless t1) $ (make_typeless t2) walther@60000: walther@60000: (* is the term t input (or taken from fmz) known in O_Model ? walther@60000: give feedback on all(?) strange input; walther@60000: return _all_ terms already input to this item (e.g. valuesFor a,b) *) Walther@60471: fun contains ctxt sel ori t = walther@60000: let walther@60017: val ots = ((distinct op =) o flat o (map #5)) ori walther@60017: val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots walther@60000: val (d, ts) = Input_Descript.split t walther@60017: val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts) walther@60000: in walther@60000: if (subtract op = oids ids) <> [] walther@60000: then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", single_empty, []) walther@60000: else walther@60000: if d = TermC.empty walther@60000: then Walther@60471: if not (subset op = (map make_typeless ts, map make_typeless ots)) Walther@60675: then ("terms '" ^ (strs2str' o (map (UnparseC.term ctxt))) ts ^ Walther@60471: "' not in example (make_typeless)", single_empty, []) walther@60000: else Walther@60471: (case associate_input' ctxt sel ts(*..values*) ori of walther@60001: ("", ori_ as (_, _, _, d, ts), all) => walther@60000: (case test_types ctxt (d,ts) of walther@60000: "" => ("", ori_, all) walther@60000: | msg => (msg, single_empty, [])) walther@60000: | (msg, _, _) => (msg, single_empty, [])) walther@60000: else walther@60000: if member op = (map #4 ori) d Walther@60471: then associate_input ctxt sel (d, ts) ori Walther@60675: else (UnparseC.term ctxt d ^ " not in example", (0, [], sel, d, ts), []) walther@60000: end walther@59999: Walther@60474: (**)end(**);