155 val add_cases: bool -> (string * RuleCases.T option) list -> context -> context |
155 val add_cases: bool -> (string * RuleCases.T option) list -> context -> context |
156 val apply_case: RuleCases.T -> context -> (string * term list) list * context |
156 val apply_case: RuleCases.T -> context -> (string * term list) list * context |
157 val get_case: context -> string -> string option list -> RuleCases.T |
157 val get_case: context -> string -> string option list -> RuleCases.T |
158 val expand_abbrevs: bool -> context -> context |
158 val expand_abbrevs: bool -> context -> context |
159 val add_const_syntax: string * bool -> (string * mixfix) list -> context -> context |
159 val add_const_syntax: string * bool -> (string * mixfix) list -> context -> context |
160 val add_abbrevs: string * bool -> (bstring * term * mixfix) list -> context -> context |
160 val add_abbrevs: string * bool -> ((bstring * mixfix) * term) list -> context -> context |
161 val verbose: bool ref |
161 val verbose: bool ref |
162 val setmp_verbose: ('a -> 'b) -> 'a -> 'b |
162 val setmp_verbose: ('a -> 'b) -> 'a -> 'b |
163 val print_syntax: context -> unit |
163 val print_syntax: context -> unit |
164 val print_binds: context -> unit |
164 val print_binds: context -> unit |
165 val print_lthms: context -> unit |
165 val print_lthms: context -> unit |
1107 val cert_vars_legacy = prep_vars cert_typ true true; |
1107 val cert_vars_legacy = prep_vars cert_typ true true; |
1108 |
1108 |
1109 end; |
1109 end; |
1110 |
1110 |
1111 |
1111 |
1112 (* const syntax *) |
1112 (* authentic constants *) |
1113 |
1113 |
1114 fun add_const_syntax prmode args ctxt = |
1114 fun add_const_syntax prmode args ctxt = |
1115 ctxt |> map_syntax |
1115 ctxt |> map_syntax |
1116 (LocalSyntax.add_modesyntax (theory_of ctxt) prmode |
1116 (LocalSyntax.add_modesyntax (theory_of ctxt) prmode |
1117 (map (pair false o Consts.syntax (consts_of ctxt)) args)); |
1117 (map (pair false o Consts.syntax (consts_of ctxt)) args)); |
1118 |
1118 |
|
1119 fun context_const_ast_tr context [Syntax.Variable c] = |
|
1120 let |
|
1121 val consts = Context.cases Sign.consts_of consts_of context; |
|
1122 val c' = Consts.intern consts c; |
|
1123 val _ = Consts.constraint consts c' handle TYPE (msg, _, _) => error msg; |
|
1124 in Syntax.Constant (Syntax.constN ^ c') end |
|
1125 | context_const_ast_tr _ asts = raise Syntax.AST ("const_ast_tr", asts); |
|
1126 |
|
1127 val _ = Context.add_setup |
|
1128 (Sign.add_syntax |
|
1129 [("_context_const", "id => 'a", Delimfix "CONST _"), |
|
1130 ("_context_const", "longid => 'a", Delimfix "CONST _")] #> |
|
1131 Sign.add_advanced_trfuns ([("_context_const", context_const_ast_tr)], [], [], [])); |
|
1132 |
1119 |
1133 |
1120 (* abbreviations *) |
1134 (* abbreviations *) |
1121 |
1135 |
1122 val expand_abbrevs = map_consts o apsnd o Consts.expand_abbrevs; |
1136 val expand_abbrevs = map_consts o apsnd o Consts.expand_abbrevs; |
1123 |
1137 |
1124 fun add_abbrevs prmode = fold (fn (raw_c, raw_t, raw_mx) => fn ctxt => |
1138 fun add_abbrevs prmode = fold (fn ((raw_c, raw_mx), raw_t) => fn ctxt => |
1125 let |
1139 let |
1126 val ([(c, _, mx)], _) = cert_vars [(raw_c, NONE, raw_mx)] ctxt; |
1140 val ([(c, _, mx)], _) = cert_vars [(raw_c, NONE, raw_mx)] ctxt; |
1127 val c' = Syntax.constN ^ full_name ctxt c; |
1141 val c' = Syntax.constN ^ full_name ctxt c; |
1128 val [t] = polymorphic ctxt [cert_term (ctxt |> expand_abbrevs false) raw_t]; |
1142 val [t] = polymorphic ctxt [cert_term (ctxt |> expand_abbrevs false) raw_t]; |
1129 val T = Term.fastype_of t; |
1143 val T = Term.fastype_of t; |
1132 else error ("Extra type variables on rhs of abbreviation: " ^ quote c); |
1146 else error ("Extra type variables on rhs of abbreviation: " ^ quote c); |
1133 in |
1147 in |
1134 ctxt |
1148 ctxt |
1135 |> declare_term t |
1149 |> declare_term t |
1136 |> map_consts (apsnd |
1150 |> map_consts (apsnd |
1137 (Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), false))) |
1151 (Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), true))) |
1138 |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt) prmode [(false, (c', T, mx))]) |
1152 |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt) prmode [(false, (c', T, mx))]) |
1139 end); |
1153 end); |
1140 |
1154 |
1141 |
1155 |
1142 (* fixes *) |
1156 (* fixes *) |