4 *) |
4 *) |
5 (* Extension to Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *) |
5 (* Extension to Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *) |
6 signature CONTEXT_C = |
6 signature CONTEXT_C = |
7 sig |
7 sig |
8 val e_ctxt : Proof.context |
8 val e_ctxt : Proof.context |
9 val declare_constraints : string -> Proof.context -> Proof.context |
|
10 val declare_constraints' : term list -> Proof.context -> Proof.context |
|
11 val initialise : string -> term list -> Proof.context |
9 val initialise : string -> term list -> Proof.context |
12 val initialise' : theory -> string list -> Proof.context |
10 val initialise' : theory -> string list -> Proof.context |
13 val get_assumptions : Proof.context -> term list |
11 val get_assumptions : Proof.context -> term list |
14 val insert_assumptions : term list -> Proof.context -> Proof.context |
12 val insert_assumptions : term list -> Proof.context -> Proof.context |
15 val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context |
13 val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context |
180 structure ContextC(**) : CONTEXT_C(**) = |
178 structure ContextC(**) : CONTEXT_C(**) = |
181 struct |
179 struct |
182 |
180 |
183 val e_ctxt = Proof_Context.init_global @{theory "Pure"}; |
181 val e_ctxt = Proof_Context.init_global @{theory "Pure"}; |
184 |
182 |
185 fun declare_constraints' ts ctxt = fold Variable.declare_constraints (flat (map TermC.vars ts)) ctxt; |
183 (* in root-problem take respective formalisation *) |
186 (*WN110613 fun declare_constraints' shall replace fun declare_constraints*) |
184 fun initialise' thy fmz = |
187 fun declare_constraints t ctxt = |
185 let |
|
186 val ctxt = thy |> Proof_Context.init_global |
|
187 val frees = map (TermC.parseNEW' ctxt) fmz |> map TermC.vars |> flat |> distinct |
|
188 val _ = TermC.raise_type_conflicts frees |
|
189 in |
|
190 fold Variable.declare_constraints frees ctxt |
|
191 end |
|
192 (* in Subproblem take respective actual arguments from program *) |
|
193 fun initialise thy' ts = |
188 let |
194 let |
189 fun get_vars ((v, T) :: vs) = (case raw_explode v |> Library.read_int of |
195 val ctxt = Rule.Thy_Info_get_theory thy' |> Proof_Context.init_global |
190 (_, _ :: _) => (Free (v, T) :: get_vars vs) |
196 val frees = map TermC.vars ts |> flat |> distinct |
191 | (_, [] ) => get_vars vs) (*filter out nums as long as we have Free ("123",_)*) |
197 val _ = TermC.raise_type_conflicts frees |
192 | get_vars [] = []; |
|
193 val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars; |
|
194 in fold Variable.declare_constraints ts ctxt end; |
|
195 |
|
196 (* replace fun initialise' ..*) |
|
197 fun initialise thy' ts = |
|
198 (TermC.raise_type_conflicts ts; |
|
199 fold Variable.declare_constraints ts (Rule.Thy_Info_get_theory thy' |> Proof_Context.init_global)) |
|
200 (* context initialised from theories, still given as strings in a formalisation or a program*) |
|
201 fun initialise' thy' fmz = |
|
202 let |
|
203 val ctxt = thy' |> Proof_Context.init_global |
|
204 val ts = |
|
205 (filter is_some (map (TermC.parseNEW ctxt) fmz)) |
|
206 |> map the |> map TermC.vars |> flat |> distinct |
|
207 val _ = TermC.raise_type_conflicts ts |
|
208 in |
198 in |
209 fold Variable.declare_constraints ts ctxt |
199 fold Variable.declare_constraints frees ctxt |
210 end |
200 end |
211 |
201 |
212 structure Context_Data = Proof_Data (type T = term list fun init _ = []); |
202 structure Context_Data = Proof_Data (type T = term list fun init _ = []); |
213 fun get_assumptions ctxt = Context_Data.get ctxt |
203 fun get_assumptions ctxt = Context_Data.get ctxt |
214 fun insert_assumptions asms = Context_Data.map (fn xs => distinct (asms @ xs)) |
204 fun insert_assumptions asms = Context_Data.map (fn xs => distinct (asms @ xs)) |