50 |
50 |
51 (* reading of locale expressions with rewrite morphisms *) |
51 (* reading of locale expressions with rewrite morphisms *) |
52 |
52 |
53 local |
53 local |
54 |
54 |
55 fun prep_interpretation prep_expr prep_term prep_prop prep_attr expression raw_defs raw_eqns initial_ctxt = |
55 fun prep_mixins prep_term prep_prop expr_ctxt deps_ctxt raw_defs raw_eqns = |
56 let |
56 let |
57 (*reading*) |
|
58 val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt; |
|
59 val deps_ctxt = fold Locale.activate_declarations deps expr_ctxt; |
|
60 val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt expr_ctxt; |
57 val prep = Syntax.check_terms deps_ctxt #> Variable.export_terms deps_ctxt expr_ctxt; |
61 val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs; |
58 val rhss = (prep o map (prep_term deps_ctxt o snd o snd)) raw_defs; |
62 val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns; |
|
63 |
|
64 (*defining*) |
|
65 val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs => |
59 val pre_defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs => |
66 ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss; |
60 ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss; |
67 val (defs, forked_ctxt) = fold_map Local_Theory.define pre_defs expr_ctxt; |
61 val eqns = (prep o map (prep_prop deps_ctxt o snd)) raw_eqns; |
68 val def_ctxt = Proof_Context.transfer (Proof_Context.theory_of forked_ctxt) expr_ctxt; |
62 in (pre_defs, eqns) end; |
69 val def_eqns = defs |
63 |
70 |> map (Thm.symmetric o |
64 fun define_mixins [] expr_ctxt = ([], expr_ctxt) |
71 Morphism.thm (Local_Theory.standard_morphism forked_ctxt def_ctxt) o snd o snd); |
65 (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*) |
72 |
66 | define_mixins pre_defs expr_lthy = |
73 (*setting up proof*) |
67 let |
|
68 val (defs, forked_lthy) = fold_map Local_Theory.define pre_defs expr_lthy; |
|
69 val def_lthy = |
|
70 Proof_Context.transfer (Proof_Context.theory_of forked_lthy) expr_lthy; |
|
71 val def_eqns = defs |
|
72 |> map (Thm.symmetric o |
|
73 Morphism.thm (Local_Theory.standard_morphism forked_lthy def_lthy) o snd o snd); |
|
74 in (def_eqns, def_lthy) end; |
|
75 |
|
76 fun prep_interpretation prep_expr prep_term prep_prop prep_attr |
|
77 expression raw_defs raw_eqns initial_ctxt = |
|
78 let |
|
79 val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt; |
|
80 val (pre_defs, eqns) = |
|
81 prep_mixins prep_term prep_prop expr_ctxt |
|
82 (fold Locale.activate_declarations deps expr_ctxt) raw_defs raw_eqns; |
|
83 val (def_eqns, def_ctxt) = define_mixins pre_defs expr_ctxt; |
74 val attrss = map (apsnd (map (prep_attr def_ctxt)) o fst) raw_eqns; |
84 val attrss = map (apsnd (map (prep_attr def_ctxt)) o fst) raw_eqns; |
75 val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt; |
85 val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt; |
76 val export' = Variable.export_morphism goal_ctxt def_ctxt; |
86 val export' = Variable.export_morphism goal_ctxt def_ctxt; |
77 in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end; |
87 in (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end; |
78 |
88 |