59 [Pretty.big_list ("locale " ^ Locale.extern thy loc ^ " =") |
53 [Pretty.big_list ("locale " ^ Locale.extern thy loc ^ " =") |
60 (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)] |
54 (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)] |
61 end; |
55 end; |
62 |
56 |
63 |
57 |
|
58 (* consts *) |
|
59 |
|
60 fun fork_mixfix is_class is_loc mx = |
|
61 let |
|
62 val mx' = Syntax.unlocalize_mixfix mx; |
|
63 val mx1 = if is_class orelse (is_loc andalso mx = mx') then NoSyn else mx'; |
|
64 val mx2 = if is_loc then mx else NoSyn; |
|
65 in (mx1, mx2) end; |
|
66 |
|
67 fun internal_abbrev ((c, mx), t) = |
|
68 LocalTheory.term_syntax (ProofContext.target_abbrev Syntax.internal_mode ((c, mx), t)) #> |
|
69 ProofContext.add_abbrev (#1 Syntax.internal_mode) (c, t) #> snd; |
|
70 |
|
71 fun consts is_class is_loc depends decls lthy = |
|
72 let |
|
73 val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy))); |
|
74 |
|
75 fun const ((c, T), mx) thy = |
|
76 let |
|
77 val U = map #2 xs ---> T; |
|
78 val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs); |
|
79 val (mx1, mx2) = fork_mixfix is_class is_loc mx; |
|
80 val thy' = Sign.add_consts_authentic [(c, U, mx1)] thy; |
|
81 in (((c, mx2), t), thy') end; |
|
82 |
|
83 val (abbrs, lthy') = lthy |> LocalTheory.theory_result (fold_map const decls); |
|
84 val defs = map (apsnd (pair ("", []))) abbrs; |
|
85 in |
|
86 lthy' |
|
87 |> is_loc ? fold internal_abbrev abbrs |
|
88 |> LocalDefs.add_defs defs |>> map (apsnd snd) |
|
89 end; |
|
90 |
|
91 |
64 (* abbrev *) |
92 (* abbrev *) |
65 |
|
66 val internal_abbrev = |
|
67 LocalTheory.term_syntax o ProofContext.target_abbrev Syntax.internal_mode; |
|
68 |
93 |
69 fun occ_params ctxt ts = |
94 fun occ_params ctxt ts = |
70 #1 (ProofContext.inferred_fixes ctxt) |
95 #1 (ProofContext.inferred_fixes ctxt) |
71 |> filter (member (op =) (fold (Variable.add_fixed ctxt) ts [])); |
96 |> filter (member (op =) (fold (Variable.add_fixed ctxt) ts [])); |
72 |
97 |
73 fun abbrev is_loc prmode ((raw_c, mx), raw_t) lthy = |
98 fun abbrev is_class is_loc prmode ((raw_c, mx), raw_t) lthy = |
74 let |
99 let |
75 val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy); |
100 val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy); |
76 val target = LocalTheory.target_of lthy; |
101 val target = LocalTheory.target_of lthy; |
77 val target_morphism = LocalTheory.target_morphism lthy; |
102 val target_morphism = LocalTheory.target_morphism lthy; |
78 |
103 |
79 val c = Morphism.name target_morphism raw_c; |
104 val c = Morphism.name target_morphism raw_c; |
80 val t = Morphism.term target_morphism raw_t; |
105 val t = Morphism.term target_morphism raw_t; |
81 val xs = map Free (occ_params target [t]); |
106 val xs = map Free (occ_params target [t]); |
82 val u = fold_rev Term.lambda xs t; |
107 val u = fold_rev Term.lambda xs t; |
|
108 val U = Term.fastype_of u; |
83 val u' = singleton (Variable.export_terms (Variable.declare_term u target) thy_ctxt) u; |
109 val u' = singleton (Variable.export_terms (Variable.declare_term u target) thy_ctxt) u; |
84 |
110 |
85 val ((const, _), lthy1) = lthy |
111 val ((lhs as Const (full_c, _), rhs), lthy1) = lthy |
86 |> LocalTheory.theory_result (Sign.add_abbrev (#1 prmode) (c, u')); |
112 |> LocalTheory.theory_result (Sign.add_abbrev (#1 prmode) (c, u')); |
87 val v = Const (#1 const, Term.fastype_of u); |
113 val (mx1, mx2) = fork_mixfix is_class is_loc mx; |
88 val v' = Const const; |
|
89 (* FIXME proper handling of mixfix !? *) |
|
90 val mx' = if is_class lthy then NoSyn else Syntax.unlocalize_mixfix is_loc mx; |
|
91 in |
114 in |
92 lthy1 |
115 lthy1 |
93 |> LocalTheory.theory (Sign.add_notation prmode [(v', mx')]) |
116 |> LocalTheory.theory (Sign.add_notation prmode [(lhs, mx1)]) |
94 |> is_loc ? internal_abbrev ((c, mx), Term.list_comb (v, xs)) |
117 |> is_loc ? internal_abbrev ((c, mx2), Term.list_comb (Const (full_c, U), xs)) |
95 end; |
118 |> ProofContext.local_abbrev (c, rhs) |
96 |
119 end; |
97 |
120 |
98 (* consts *) |
121 |
99 |
|
100 fun consts is_loc depends decls lthy = |
|
101 let |
|
102 val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy))); |
|
103 |
|
104 fun const ((c, T), mx) thy = |
|
105 let |
|
106 val U = map #2 xs ---> T; |
|
107 val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs); |
|
108 (* FIXME proper handling of mixfix !? *) |
|
109 val mx' = if is_class lthy then NoSyn else Syntax.unlocalize_mixfix is_loc mx; |
|
110 val thy' = Sign.add_consts_authentic [(c, U, mx')] thy; |
|
111 in (((c, mx), t), thy') end; |
|
112 |
|
113 val (abbrs, lthy') = lthy |> LocalTheory.theory_result (fold_map const decls); |
|
114 val defs = abbrs (* FIXME proper handling of mixfix !? *) |
|
115 |> map (fn ((c, mx), t) => ((c, if is_loc then mx else NoSyn), (("", []), t))); |
|
116 in |
|
117 lthy' |
|
118 |> is_loc ? fold internal_abbrev abbrs |
|
119 |> LocalDefs.add_defs defs |>> map (apsnd snd) |
|
120 end; |
|
121 |
122 |
122 |
123 |
123 (* defs *) |
124 (* defs *) |
124 |
125 |
125 local |
126 local |
306 |> NameSpace.full; |
307 |> NameSpace.full; |
307 |
308 |
308 |
309 |
309 (* init and exit *) |
310 (* init and exit *) |
310 |
311 |
311 fun begin loc = |
312 fun begin is_class loc = |
312 let val is_loc = loc <> "" in |
313 let val is_loc = loc <> "" in |
313 Data.put (if is_loc then SOME loc else NONE) #> |
314 Data.put (if is_loc then SOME loc else NONE) #> |
314 LocalTheory.init (NameSpace.base loc) |
315 LocalTheory.init (NameSpace.base loc) |
315 {pretty = pretty loc, |
316 {pretty = pretty loc, |
316 consts = consts is_loc, |
317 consts = consts is_class is_loc, |
317 axioms = axioms, |
318 axioms = axioms, |
318 abbrev = abbrev is_loc, |
319 abbrev = abbrev is_class is_loc, |
319 defs = defs, |
320 defs = defs, |
320 notes = notes loc, |
321 notes = notes loc, |
321 type_syntax = type_syntax loc, |
322 type_syntax = type_syntax loc, |
322 term_syntax = term_syntax loc, |
323 term_syntax = term_syntax loc, |
323 declaration = declaration loc, |
324 declaration = declaration loc, |
324 target_morphism = target_morphism loc, |
325 target_morphism = target_morphism loc, |
325 target_name = target_name loc, |
326 target_name = target_name loc, |
326 reinit = fn _ => begin loc o (if is_loc then Locale.init loc else ProofContext.init), |
327 reinit = fn _ => |
|
328 begin is_class loc o (if is_loc then Locale.init loc else ProofContext.init), |
327 exit = LocalTheory.target_of} |
329 exit = LocalTheory.target_of} |
328 end; |
330 end; |
329 |
331 |
330 fun init_i NONE thy = begin "" (ProofContext.init thy) |
332 fun init_i NONE thy = begin false "" (ProofContext.init thy) |
331 | init_i (SOME loc) thy = begin loc (Locale.init loc thy); |
333 | init_i (SOME loc) thy = |
|
334 begin (can (Sign.certify_class thy) loc) (* FIXME approximation *) |
|
335 loc (Locale.init loc thy); |
332 |
336 |
333 fun init (SOME "-") thy = init_i NONE thy |
337 fun init (SOME "-") thy = init_i NONE thy |
334 | init loc thy = init_i (Option.map (Locale.intern thy) loc) thy; |
338 | init loc thy = init_i (Option.map (Locale.intern thy) loc) thy; |
335 |
339 |
336 end; |
340 end; |