1 (* Title: tools for 'modeling' und 'specifying' to be used in
2 modspec.sml. The types are separated into this file,
3 because some of them are stored in the calc-tree, and thus are required
5 TODO: allocate elements of Selem and of Stool appropriately
6 Author: Walther Neuper, Mathias Lehnfeld
7 (c) due to copyright terms
10 signature SPECIFY_TOOL =
12 val check_preconds : 'a -> Celem.rls -> term list -> Model.itm list -> (bool * term) list
13 val check_preconds' : Celem.rls -> term list -> Model.itm list -> 'a -> (bool * term) list
15 val get_assumptions : Proof.context -> term list
16 val insert_assumptions : term list -> Proof.context -> Proof.context
17 val declare_constraints : string -> Proof.context -> Proof.context
18 val declare_constraints' : term list -> Proof.context -> Proof.context
19 val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context
21 datatype match_ = Match_ of Celem.pblID * (Model.itm list * (bool * term) list) | NoMatch_
22 val refined_ : match_ list -> match_ option
23 datatype match = Matches of Celem.pblID * Model.item Model.ppc | NoMatch of Celem.pblID * Model.item Model.ppc
24 val matchs2str : match list -> string
25 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
26 val pres2str : (bool * term) list -> string
27 val refined : match list -> Celem.pblID
28 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
29 val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context
30 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
32 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
33 val pblID_of_match : match -> Celem.pblID
34 val refined_IDitms : match list -> match option
37 structure Stool(**) : SPECIFY_TOOL(**) =
41 Matches of Celem.pblID * Model.item Model.ppc
42 | NoMatch of Celem.pblID * Model.item Model.ppc;
43 fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^ Model.itemppc2str ppc ^ ")"
44 | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^ Model.itemppc2str ppc ^ ")";
45 fun matchs2str ms = (strs2str o (map match2str)) ms;
46 fun pblID_of_match (Matches (pI, _)) = pI
47 | pblID_of_match (NoMatch (pI, _)) = pI;
49 (* 10.03 for Refine_Problem *)
51 Match_ of Celem.pblID * (( Model.itm list) * ((bool * term) list))
54 (* the refined pbt is the last_element Matches in the list *)
55 fun is_matches (Matches _) = true
56 | is_matches _ = false;
57 fun matches_pblID (Matches (pI, _)) = pI
58 | matches_pblID _ = error "matches_pblID: uncovered case in fun.def.";
59 fun refined ms = ((matches_pblID o the o (find_first is_matches) o rev) ms)
61 fun refined_IDitms ms = ((find_first is_matches) o rev) ms;
63 (* the refined pbt is the last_element Matches in the list, for Refine_Problem, tryrefine *)
64 fun is_matches_ (Match_ _) = true
65 | is_matches_ _ = false;
66 fun refined_ ms = ((find_first is_matches_) o rev) ms;
68 (* check a predicate labelled with indication of incomplete substitution;
69 rls -> (* for eval_true *)
70 bool * (* have _all_ variables(Free) from the model-pattern
71 been substituted by a value from the pattern's environment ?*)
72 term -> (* the precondition *)
73 bool * (* has the precondition evaluated to true *)
74 term (* the precondition (for map) *)
76 fun evalprecond _ (false, pre) =
77 (*NOT ALL Free's have been substituted, eg. because of incomplete model*)
79 | evalprecond prls (true, pre) =
80 if Rewrite.eval_true (Celem.assoc_thy "Isac") (* for Pattern.match *)
81 [pre] prls (* pre parsed, prls.thy *)
85 fun pre2str (b, t) = pair2str(bool2str b, Celem.term2str t);
86 fun pres2str pres = strs2str' (map (Celem.linefeed o pre2str) pres);
88 (* check preconditions, return true if all true *)
89 fun check_preconds' _ [] _ _ = [] (* empty preconditions are true *)
90 | check_preconds' prls pres pbl _ (* FIXME.WN0308 mvat re-introduce *) =
92 val env = Model.mk_env pbl;
93 val pres' = map (TermC.subst_atomic_all env) pres;
94 in map (evalprecond prls) pres' end;
96 fun check_preconds _(*thy*) prls pres pbl = check_preconds' prls pres pbl (Model.max_vt pbl);
97 fun declare_constraints' ts ctxt = fold Variable.declare_constraints (flat (map TermC.vars ts)) ctxt;
99 (*WN110613 fun declare_constraints' shall replace fun declare_constraints*)
100 fun declare_constraints t ctxt =
102 fun get_vars ((v, T) :: vs) = (case raw_explode v |> Library.read_int of
103 (_, _ :: _) => (Free (v, T) :: get_vars vs)
104 | (_, [] ) => get_vars vs) (*filter out nums as long as we have Free ("123",_)*)
106 val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
107 in fold Variable.declare_constraints ts ctxt end;
109 structure Context_Data = Proof_Data (type T = term list fun init _ = []);
110 fun get_assumptions ctxt = Context_Data.get ctxt
111 fun insert_assumptions asms = Context_Data.map (fn xs => distinct (asms @ xs))
113 (* transfer assumptions from one to another ctxt.
114 does NOT respect scope: in a calculation identifiers are unique.
115 but environments are scoped as usual in Luacs-interpretation.
116 WN110520 redo (1) take declare_constraints (2) with combinators*)
117 fun transfer_asms_from_to from_ctxt to_ctxt =
119 val to_vars = get_assumptions to_ctxt |> map TermC.vars |> flat
120 fun transfer [] to_ctxt = to_ctxt
121 | transfer (from_asm :: fas) to_ctxt =
122 if inter op = (TermC.vars from_asm) to_vars = []
123 then transfer fas to_ctxt
124 else transfer fas (insert_assumptions [from_asm] to_ctxt)
125 in transfer (get_assumptions from_ctxt) to_ctxt end
127 (* exported from a subproblem to the context of the calling method:
128 # 'scrval': the result of script interpretation and
129 # those assumptions in the subproblem wich contain a variable known
130 in the calling method. *)
131 fun from_subpbl_to_caller sub_ctxt scrval caller_ctxt =
133 val caller_ctxt = (scrval |> Model.dest_list' |> insert_assumptions) caller_ctxt
134 in transfer_asms_from_to sub_ctxt caller_ctxt end;