1 (* Title: ../contextC.sml
2 Author: Walther Neuper, Mathias Lehnfeld
3 (c) due to copyright terms
5 (* Extension to Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *)
8 val empty : Proof.context
9 val is_empty : Proof.context -> bool
10 val for_ERROR: 'a -> Proof.context
12 val declare_constraints: term -> Proof.context -> Proof.context
13 val add_constraints: term list -> Proof.context -> Proof.context
14 val init_while_parsing: Formalise.model -> theory -> term list * Proof.context
15 val init_for_prog: Proof.context -> term list -> Proof.context
17 val get_assumptions : Proof.context -> term list
18 val insert_assumptions : term list -> Proof.context -> Proof.context
19 val avoid_contradict: term -> term list -> term * term list
20 val subpbl_to_caller : Proof.context -> term -> Proof.context -> term * Proof.context
23 val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context
24 val contradict : term list -> term -> bool
25 val insert_assumptions_cao : Proof.context -> term list -> Proof.context
29 structure ContextC(**) : CONTEXT_C(**) =
32 val empty = Proof_Context.init_global @{theory "Pure"};
33 (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)
35 fun is_empty ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});
36 fun for_ERROR _ = "Isac_Knowledge" |> Know_Store.get_via_last_thy |> Proof_Context.init_global
38 val declare_constraints = Variable.declare_constraints
39 fun add_constraints ts ctxt =
40 fold Variable.declare_constraints (TermC.vars' ts) ctxt
42 fun build_while_parsing_ [] (ts, ctxt) = (ts, ctxt)
43 | build_while_parsing_ (str :: strs) (ts, ctxt) =
45 val t as (_ $ tm) = Syntax.read_term ctxt str
46 handle ERROR msg => raise ERROR ("ContextC.init_while_parsing " ^ quote str ^ " " ^ msg)
47 val vars = TermC.vars tm
48 val ctxt' = add_constraints vars ctxt
49 in build_while_parsing_ strs (ts @ [t], ctxt') end
50 (* shouldn't that be done by fold ?
51 fn: string * Proof.context -> term list * Proof.context -> term list * Proof.context *)
52 fun init_while_parsing strs thy = build_while_parsing_ strs ([], Proof_Context.init_global thy)
54 (* in Subproblem take respective actual arguments from program *)
55 fun init_for_prog ctxt ts =
57 val frees = TermC.vars' ts
58 val _ = TermC.raise_type_conflicts frees
60 fold Variable.declare_constraints frees ctxt
63 structure Context_Data = Proof_Data (type T = term list fun init _ = []);
64 fun get_assumptions ctxt = Context_Data.get ctxt
65 fun insert_assumptions asms = Context_Data.map (fn xs => distinct op = (asms @ xs))
68 transfer assumptions from one to another ctxt.
69 does NOT respect scope: in a calculation identifiers are unique.
70 but environments are scoped as usual in Luacs-interpretation.
72 fun transfer_asms_from_to from_ctxt to_ctxt =
74 val to_vars = get_assumptions to_ctxt |> map TermC.vars |> flat
75 fun transfer [] to_ctxt = to_ctxt
76 | transfer (from_asm :: fas) to_ctxt =
77 if inter op = (TermC.vars from_asm) to_vars = []
78 then transfer fas to_ctxt
79 else transfer fas (insert_assumptions [from_asm] to_ctxt)
81 transfer (get_assumptions from_ctxt) to_ctxt
84 (* there is still much TODO: factorise polynomials, etc *)
85 fun contradict asm res = fold (curry or_) (map (fn p => TermC.negates res p) asm) false;
88 Check a term for contradiction with a predicate list.
89 This makes only sense for types bool and bool list. In these cases return
90 the probably updated term together with
91 a respective list of non-contradicting predicates
93 fun avoid_contradict t preds =
94 if TermC.is_bool_list t then
96 val no_contra = t |> TermC.dest_list' |> filter_out (contradict preds)
98 (no_contra |> TermC.list2isalist HOLogic.boolT, no_contra)
100 else if Term.type_of t = HOLogic.boolT then
101 if contradict preds t then (@{term bool_undef}, []) else (t, [t])
102 else (t (* type_of t \<noteq> bool *), [(* no predicate to add *)])
104 (* for Canonical Argument Order used by |> below *)
105 fun insert_assumptions_cao ctxt tms = insert_assumptions tms ctxt
107 fun subpbl_to_caller sub_ctxt expr_val caller_ctxt = caller_ctxt
109 |> avoid_contradict expr_val
110 |> apsnd (insert_assumptions_cao caller_ctxt)
111 |> apsnd (transfer_asms_from_to sub_ctxt)