113 val note_thmss_i: |
114 val note_thmss_i: |
114 ((bstring * context attribute list) * (thm list * context attribute list) list) list -> |
115 ((bstring * context attribute list) * (thm list * context attribute list) list) list -> |
115 context -> (bstring * thm list) list * context |
116 context -> (bstring * thm list) list * context |
116 val export_assume: exporter |
117 val export_assume: exporter |
117 val export_presume: exporter |
118 val export_presume: exporter |
118 val cert_def: context -> term -> string * term |
|
119 val export_def: exporter |
|
120 val assume: exporter |
119 val assume: exporter |
121 -> ((string * context attribute list) * (string * (string list * string list)) list) list |
120 -> ((string * context attribute list) * (string * (string list * string list)) list) list |
122 -> context -> (bstring * thm list) list * context |
121 -> context -> (bstring * thm list) list * context |
123 val assume_i: exporter |
122 val assume_i: exporter |
124 -> ((string * context attribute list) * (term * (term list * term list)) list) list |
123 -> ((string * context attribute list) * (term * (term list * term list)) list) list |
125 -> context -> (bstring * thm list) list * context |
124 -> context -> (bstring * thm list) list * context |
|
125 val mk_def: context -> string * term -> term |
|
126 val cert_def: context -> term -> string * term |
|
127 val export_def: exporter |
|
128 val add_def: string * term -> context -> ((string * typ) * thm) * context |
126 val add_view: context -> cterm list -> context -> context |
129 val add_view: context -> cterm list -> context -> context |
127 val export_view: cterm list -> context -> context -> thm -> thm |
130 val export_view: cterm list -> context -> context -> thm -> thm |
128 val read_vars: (string list * string option) -> context -> (string list * typ option) * context |
131 val read_vars: (string list * string option) -> context -> (string list * typ option) * context |
129 val cert_vars: (string list * typ option) -> context -> (string list * typ option) * context |
132 val cert_vars: (string list * typ option) -> context -> (string list * typ option) * context |
130 val read_vars_liberal: (string list * string option) -> context -> |
133 val read_vars_liberal: (string list * string option) -> context -> |
430 | intern (Abs (x, T, t)) = Abs (x, T, intern t) |
433 | intern (Abs (x, T, t)) = Abs (x, T, intern t) |
431 | intern a = a; |
434 | intern a = a; |
432 in intern end; |
435 in intern end; |
433 |
436 |
434 |
437 |
435 (* externalize Skolem constants -- for printing purposes only *) |
438 (* externalize Skolem constants -- approximation only! *) |
|
439 |
|
440 fun revert_skolem ctxt = |
|
441 let val rev_fixes = map Library.swap (fixes_of ctxt) |
|
442 in AList.lookup (op =) rev_fixes end; |
436 |
443 |
437 fun extern_skolem ctxt = |
444 fun extern_skolem ctxt = |
438 let |
445 let |
439 val rev_fixes = map Library.swap (fixes_of ctxt); |
446 val revert = revert_skolem ctxt; |
440 |
|
441 fun extern (t as Free (x, T)) = |
447 fun extern (t as Free (x, T)) = |
442 (case AList.lookup (op =) rev_fixes x of |
448 (case revert x of |
443 SOME x' => Free (if lookup_skolem ctxt x' = SOME x then x' else NameSpace.hidden x', T) |
449 SOME x' => Free (if lookup_skolem ctxt x' = SOME x then x' else NameSpace.hidden x', T) |
444 | NONE => t) |
450 | NONE => t) |
445 | extern (t $ u) = extern t $ extern u |
451 | extern (t $ u) = extern t $ extern u |
446 | extern (Abs (x, T, t)) = Abs (x, T, extern t) |
452 | extern (Abs (x, T, t)) = Abs (x, T, extern t) |
447 | extern a = a; |
453 | extern a = a; |
448 in extern end |
454 in extern end |
|
455 |
449 |
456 |
450 |
457 |
451 (** prepare terms and propositions **) |
458 (** prepare terms and propositions **) |
452 |
459 |
453 (* |
460 (* |
712 val gen = generalize_tfrees inner outer; |
719 val gen = generalize_tfrees inner outer; |
713 val fixes = fixed_names_of inner \\ fixed_names_of outer; |
720 val fixes = fixed_names_of inner \\ fixed_names_of outer; |
714 val asms = Library.drop (length (assumptions_of outer), assumptions_of inner); |
721 val asms = Library.drop (length (assumptions_of outer), assumptions_of inner); |
715 val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms; |
722 val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms; |
716 in |
723 in |
717 Goal.norm_hhf |
724 Goal.norm_hhf' |
718 #> Seq.EVERY (rev exp_asms) |
725 #> Seq.EVERY (rev exp_asms) |
719 #> Seq.map (fn rule => |
726 #> Seq.map (fn rule => |
720 let |
727 let |
721 val thy = Thm.theory_of_thm rule; |
728 val thy = Thm.theory_of_thm rule; |
722 val prop = Thm.full_prop_of rule; |
729 val prop = Thm.full_prop_of rule; |
723 val frees = map (Thm.cterm_of thy) (List.mapPartial (Term.find_free prop) fixes); |
730 val frees = map (Thm.cterm_of thy) (List.mapPartial (Term.find_free prop) fixes); |
724 val tfrees = gen (Term.add_term_tfree_names (prop, [])); |
731 val tfrees = gen (Term.add_term_tfree_names (prop, [])); |
725 in |
732 in |
726 rule |
733 rule |
727 |> Drule.forall_intr_list frees |
734 |> Drule.forall_intr_list frees |
728 |> Goal.norm_hhf |
735 |> Goal.norm_hhf' |
729 |> Drule.tvars_intr_list tfrees |> #2 |
736 |> Drule.tvars_intr_list tfrees |> #2 |
730 end) |
737 end) |
731 end; |
738 end; |
732 |
739 |
733 fun export inner outer = |
740 fun export inner outer = |
1030 |
1037 |
1031 |
1038 |
1032 |
1039 |
1033 (** assumptions **) |
1040 (** assumptions **) |
1034 |
1041 |
|
1042 |
|
1043 (* variables *) |
|
1044 |
|
1045 local |
|
1046 |
|
1047 fun prep_vars prep_typ internal liberal (xs, raw_T) ctxt = |
|
1048 let |
|
1049 fun cond_tvars T = |
|
1050 if internal then T |
|
1051 else Type.no_tvars T handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt); |
|
1052 |
|
1053 val _ = if liberal then () else |
|
1054 (case List.filter (not o Syntax.is_identifier) (map (no_skolem internal ctxt) xs) of |
|
1055 [] => () | bads => raise CONTEXT ("Bad variable name(s): " ^ commas_quote bads, ctxt)); |
|
1056 |
|
1057 val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T; |
|
1058 val T = the_default TypeInfer.logicT opt_T; |
|
1059 val ctxt' = ctxt |> fold declare_term_syntax (map (fn x => Free (x, T)) xs); |
|
1060 in ((xs, opt_T), ctxt') end; |
|
1061 |
|
1062 in |
|
1063 |
|
1064 val read_vars = prep_vars read_typ false false; |
|
1065 val cert_vars = prep_vars cert_typ true false; |
|
1066 val read_vars_liberal = prep_vars read_typ false true; |
|
1067 val cert_vars_liberal = prep_vars cert_typ true true; |
|
1068 |
|
1069 end; |
|
1070 |
|
1071 |
|
1072 (* fix *) |
|
1073 |
|
1074 local |
|
1075 |
|
1076 fun map_fixes f = |
|
1077 map_context (fn (syntax, (assumes, fixes), binds, thms, cases, defs) => |
|
1078 (syntax, (assumes, f fixes), binds, thms, cases, defs)); |
|
1079 |
|
1080 fun err_dups ctxt xs = raise CONTEXT ("Duplicate variable(s): " ^ commas_quote xs, ctxt); |
|
1081 |
|
1082 val declare = |
|
1083 fold declare_term_syntax o |
|
1084 List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (Free (x, T))); |
|
1085 |
|
1086 fun add_vars xs Ts ctxt = |
|
1087 let val xs' = Term.variantlist (map Syntax.skolem xs, map #2 (fixes_of ctxt)) in |
|
1088 ctxt |
|
1089 |> declare (xs' ~~ Ts) |
|
1090 |> map_fixes (append (xs ~~ xs')) |
|
1091 end; |
|
1092 |
|
1093 fun add_vars_direct xs Ts ctxt = |
|
1094 ctxt |
|
1095 |> declare (xs ~~ Ts) |
|
1096 |> map_fixes (fn fixes => |
|
1097 (case xs inter_string map #1 fixes of |
|
1098 [] => (xs ~~ xs) @ fixes |
|
1099 | dups => err_dups ctxt dups)); |
|
1100 |
|
1101 |
|
1102 fun gen_fix prep add raw_vars ctxt = |
|
1103 let |
|
1104 val (varss, ctxt') = fold_map prep raw_vars ctxt; |
|
1105 val vars = rev (List.concat (map (fn (xs, T) => map (rpair T) xs) varss)); |
|
1106 val xs = map #1 vars; |
|
1107 val Ts = map #2 vars; |
|
1108 in |
|
1109 (case Library.duplicates xs of [] => () | dups => err_dups ctxt dups); |
|
1110 ctxt' |> add xs Ts |
|
1111 end; |
|
1112 |
|
1113 fun prep_type (x, NONE, SOME mx) = ([x], SOME (mixfix_type mx)) |
|
1114 | prep_type (x, opt_T, _) = ([x], opt_T); |
|
1115 |
|
1116 in |
|
1117 |
|
1118 val fix = gen_fix read_vars add_vars; |
|
1119 val fix_i = gen_fix cert_vars add_vars; |
|
1120 |
|
1121 fun fix_direct liberal = |
|
1122 gen_fix (if liberal then cert_vars_liberal else cert_vars) add_vars_direct; |
|
1123 |
|
1124 fun add_fixes decls = add_syntax decls o fix_direct false (map prep_type decls); |
|
1125 fun add_fixes_liberal decls = add_syntax decls o fix_direct true (map prep_type decls); |
|
1126 |
|
1127 end; |
|
1128 |
|
1129 fun fix_frees ts ctxt = |
|
1130 let |
|
1131 val frees = fold Term.add_frees ts []; |
|
1132 fun new (x, T) = if is_fixed ctxt x then NONE else SOME ([x], SOME T); |
|
1133 in fix_direct false (rev (List.mapPartial new frees)) ctxt end; |
|
1134 |
|
1135 fun auto_fix (ctxt, (propss, x)) = (ctxt |> fix_frees (List.concat propss), (propss, x)); |
|
1136 |
|
1137 |
|
1138 (*Note: improper use may result in variable capture / dynamic scoping!*) |
|
1139 fun bind_skolem ctxt xs = |
|
1140 let |
|
1141 val ctxt' = ctxt |> fix_i [(xs, NONE)]; |
|
1142 fun bind (t as Free (x, T)) = |
|
1143 if x mem_string xs then |
|
1144 (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t) |
|
1145 else t |
|
1146 | bind (t $ u) = bind t $ bind u |
|
1147 | bind (Abs (x, T, t)) = Abs (x, T, bind t) |
|
1148 | bind a = a; |
|
1149 in bind end; |
|
1150 |
|
1151 |
1035 (* basic exporters *) |
1152 (* basic exporters *) |
1036 |
1153 |
1037 fun export_assume true = Seq.single oo Drule.implies_intr_protected |
1154 fun export_assume true = Seq.single oo Drule.implies_intr_protected |
1038 | export_assume false = Seq.single oo Drule.implies_intr_list; |
1155 | export_assume false = Seq.single oo Drule.implies_intr_list; |
1039 |
1156 |
1040 fun export_presume _ = export_assume false; |
1157 fun export_presume _ = export_assume false; |
1041 |
1158 |
1042 |
1159 |
|
1160 (* assume *) |
|
1161 |
|
1162 local |
|
1163 |
|
1164 fun add_assm ((name, attrs), props) ctxt = |
|
1165 let |
|
1166 val cprops = map (Thm.cterm_of (theory_of ctxt)) props; |
|
1167 val asms = map (Goal.norm_hhf o Thm.assume) cprops; |
|
1168 |
|
1169 val ths = map (fn th => ([th], [])) asms; |
|
1170 val ([(_, thms)], ctxt') = |
|
1171 ctxt |
|
1172 |> auto_bind_facts props |
|
1173 |> note_thmss_i [((name, attrs), ths)]; |
|
1174 in ((cprops, (name, asms), (name, thms)), ctxt') end; |
|
1175 |
|
1176 fun gen_assms prepp exp args ctxt = |
|
1177 let |
|
1178 val (ctxt1, propss) = prepp (ctxt, map snd args); |
|
1179 val (results, ctxt2) = fold_map add_assm (map fst args ~~ propss) ctxt1; |
|
1180 |
|
1181 val cprops = List.concat (map #1 results); |
|
1182 val asmss = map #2 results; |
|
1183 val thmss = map #3 results; |
|
1184 val ctxt3 = ctxt2 |> map_context |
|
1185 (fn (syntax, ((asms_ct, asms_th), fixes), binds, thms, cases, defs) => |
|
1186 (syntax, ((asms_ct @ [(cprops, exp)], asms_th @ asmss), fixes), binds, thms, |
|
1187 cases, defs)); |
|
1188 val ctxt4 = ctxt3 |> put_thms ("prems", SOME (prems_of ctxt3)); |
|
1189 in (thmss, warn_extra_tfrees ctxt ctxt4) end; |
|
1190 |
|
1191 in |
|
1192 |
|
1193 val assume = gen_assms (apsnd #1 o bind_propp); |
|
1194 val assume_i = gen_assms (apsnd #1 o bind_propp_i); |
|
1195 |
|
1196 end; |
|
1197 |
|
1198 |
1043 (* defs *) |
1199 (* defs *) |
|
1200 |
|
1201 fun mk_def ctxt (x, rhs) = |
|
1202 let val lhs = bind_skolem ctxt [x] (Free (x, Term.fastype_of rhs)); |
|
1203 in Logic.mk_equals (lhs, rhs) end; |
1044 |
1204 |
1045 fun cert_def ctxt eq = |
1205 fun cert_def ctxt eq = |
1046 let |
1206 let |
1047 fun err msg = raise CONTEXT (msg ^ |
1207 fun err msg = raise CONTEXT (msg ^ |
1048 "\nThe error(s) above occurred in local definition: " ^ string_of_term ctxt eq, ctxt); |
1208 "\nThe error(s) above occurred in local definition: " ^ string_of_term ctxt eq, ctxt); |
1074 |> Drule.implies_intr_list cprops |
1234 |> Drule.implies_intr_list cprops |
1075 |> Drule.forall_intr_list (map head_of_def cprops) |
1235 |> Drule.forall_intr_list (map head_of_def cprops) |
1076 |> Drule.forall_elim_vars 0 |
1236 |> Drule.forall_elim_vars 0 |
1077 |> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1; |
1237 |> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1; |
1078 |
1238 |
1079 |
1239 fun add_def (x, t) ctxt = |
1080 (* assume *) |
1240 let |
1081 |
1241 val eq = mk_def ctxt (x, t); |
1082 local |
1242 val x' = Term.dest_Free (fst (Logic.dest_equals eq)); |
1083 |
1243 in |
1084 fun add_assm ((name, attrs), props) ctxt = |
1244 ctxt |
1085 let |
1245 |> fix_i [([x], NONE)] |
1086 val cprops = map (Thm.cterm_of (theory_of ctxt)) props; |
1246 |> assume_i export_def [(("", []), [(eq, ([], []))])] |
1087 val asms = map (Goal.norm_hhf o Thm.assume) cprops; |
1247 |>> (fn [(_, [th])] => (x', th)) |
1088 |
1248 end; |
1089 val ths = map (fn th => ([th], [])) asms; |
|
1090 val ([(_, thms)], ctxt') = |
|
1091 ctxt |
|
1092 |> auto_bind_facts props |
|
1093 |> note_thmss_i [((name, attrs), ths)]; |
|
1094 in ((cprops, (name, asms), (name, thms)), ctxt') end; |
|
1095 |
|
1096 fun gen_assms prepp exp args ctxt = |
|
1097 let |
|
1098 val (ctxt1, propss) = prepp (ctxt, map snd args); |
|
1099 val (results, ctxt2) = fold_map add_assm (map fst args ~~ propss) ctxt1; |
|
1100 |
|
1101 val cprops = List.concat (map #1 results); |
|
1102 val asmss = map #2 results; |
|
1103 val thmss = map #3 results; |
|
1104 val ctxt3 = ctxt2 |> map_context |
|
1105 (fn (syntax, ((asms_ct, asms_th), fixes), binds, thms, cases, defs) => |
|
1106 (syntax, ((asms_ct @ [(cprops, exp)], asms_th @ asmss), fixes), binds, thms, |
|
1107 cases, defs)); |
|
1108 val ctxt4 = ctxt3 |> put_thms ("prems", SOME (prems_of ctxt3)); |
|
1109 in (thmss, warn_extra_tfrees ctxt ctxt4) end; |
|
1110 |
|
1111 in |
|
1112 |
|
1113 val assume = gen_assms (apsnd #1 o bind_propp); |
|
1114 val assume_i = gen_assms (apsnd #1 o bind_propp_i); |
|
1115 |
|
1116 end; |
|
1117 |
1249 |
1118 |
1250 |
1119 (* views *) |
1251 (* views *) |
1120 |
1252 |
1121 fun add_view outer view = |
1253 fun add_view outer view = |
1126 in (syntax, ((asms', prems), fixes), binds, thms, cases, defs) end); |
1258 in (syntax, ((asms', prems), fixes), binds, thms, cases, defs) end); |
1127 |
1259 |
1128 fun export_view view inner outer = export (add_view outer view inner) outer; |
1260 fun export_view view inner outer = export (add_view outer view inner) outer; |
1129 |
1261 |
1130 |
1262 |
1131 (* variables *) |
|
1132 |
|
1133 local |
|
1134 |
|
1135 fun prep_vars prep_typ internal liberal (xs, raw_T) ctxt = |
|
1136 let |
|
1137 fun cond_tvars T = |
|
1138 if internal then T |
|
1139 else Type.no_tvars T handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt); |
|
1140 |
|
1141 val _ = if liberal then () else |
|
1142 (case List.filter (not o Syntax.is_identifier) (map (no_skolem internal ctxt) xs) of |
|
1143 [] => () | bads => raise CONTEXT ("Bad variable name(s): " ^ commas_quote bads, ctxt)); |
|
1144 |
|
1145 val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T; |
|
1146 val T = if_none opt_T TypeInfer.logicT; |
|
1147 val ctxt' = ctxt |> fold declare_term_syntax (map (fn x => Free (x, T)) xs); |
|
1148 in ((xs, opt_T), ctxt') end; |
|
1149 |
|
1150 in |
|
1151 |
|
1152 val read_vars = prep_vars read_typ false false; |
|
1153 val cert_vars = prep_vars cert_typ true false; |
|
1154 val read_vars_liberal = prep_vars read_typ false true; |
|
1155 val cert_vars_liberal = prep_vars cert_typ true true; |
|
1156 |
|
1157 end; |
|
1158 |
|
1159 |
|
1160 (* fix *) |
|
1161 |
|
1162 local |
|
1163 |
|
1164 fun map_fixes f = |
|
1165 map_context (fn (syntax, (assumes, fixes), binds, thms, cases, defs) => |
|
1166 (syntax, (assumes, f fixes), binds, thms, cases, defs)); |
|
1167 |
|
1168 fun err_dups ctxt xs = raise CONTEXT ("Duplicate variable(s): " ^ commas_quote xs, ctxt); |
|
1169 |
|
1170 val declare = |
|
1171 fold declare_term_syntax o |
|
1172 List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (Free (x, T))); |
|
1173 |
|
1174 fun add_vars xs Ts ctxt = |
|
1175 let val xs' = Term.variantlist (map Syntax.skolem xs, map #2 (fixes_of ctxt)) in |
|
1176 ctxt |
|
1177 |> declare (xs' ~~ Ts) |
|
1178 |> map_fixes (append (xs ~~ xs')) |
|
1179 end; |
|
1180 |
|
1181 fun add_vars_direct xs Ts ctxt = |
|
1182 ctxt |
|
1183 |> declare (xs ~~ Ts) |
|
1184 |> map_fixes (fn fixes => |
|
1185 (case xs inter_string map #1 fixes of |
|
1186 [] => (xs ~~ xs) @ fixes |
|
1187 | dups => err_dups ctxt dups)); |
|
1188 |
|
1189 |
|
1190 fun gen_fix prep add raw_vars ctxt = |
|
1191 let |
|
1192 val (varss, ctxt') = fold_map prep raw_vars ctxt; |
|
1193 val vars = rev (List.concat (map (fn (xs, T) => map (rpair T) xs) varss)); |
|
1194 val xs = map #1 vars; |
|
1195 val Ts = map #2 vars; |
|
1196 in |
|
1197 (case Library.duplicates xs of [] => () | dups => err_dups ctxt dups); |
|
1198 ctxt' |> add xs Ts |
|
1199 end; |
|
1200 |
|
1201 fun prep_type (x, NONE, SOME mx) = ([x], SOME (mixfix_type mx)) |
|
1202 | prep_type (x, opt_T, _) = ([x], opt_T); |
|
1203 |
|
1204 in |
|
1205 |
|
1206 val fix = gen_fix read_vars add_vars; |
|
1207 val fix_i = gen_fix cert_vars add_vars; |
|
1208 |
|
1209 fun fix_direct liberal = |
|
1210 gen_fix (if liberal then cert_vars_liberal else cert_vars) add_vars_direct; |
|
1211 |
|
1212 fun add_fixes decls = add_syntax decls o fix_direct false (map prep_type decls); |
|
1213 fun add_fixes_liberal decls = add_syntax decls o fix_direct true (map prep_type decls); |
|
1214 |
|
1215 end; |
|
1216 |
|
1217 fun fix_frees ts ctxt = |
|
1218 let |
|
1219 val frees = fold Term.add_frees ts []; |
|
1220 fun new (x, T) = if is_fixed ctxt x then NONE else SOME ([x], SOME T); |
|
1221 in fix_direct false (rev (List.mapPartial new frees)) ctxt end; |
|
1222 |
|
1223 fun auto_fix (ctxt, (propss, x)) = (ctxt |> fix_frees (List.concat propss), (propss, x)); |
|
1224 |
|
1225 |
|
1226 (*Note: improper use may result in variable capture / dynamic scoping!*) |
|
1227 fun bind_skolem ctxt xs = |
|
1228 let |
|
1229 val ctxt' = ctxt |> fix_i [(xs, NONE)]; |
|
1230 fun bind (t as Free (x, T)) = |
|
1231 if x mem_string xs then |
|
1232 (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t) |
|
1233 else t |
|
1234 | bind (t $ u) = bind t $ bind u |
|
1235 | bind (Abs (x, T, t)) = Abs (x, T, bind t) |
|
1236 | bind a = a; |
|
1237 in bind end; |
|
1238 |
|
1239 |
|
1240 |
1263 |
1241 (** cases **) |
1264 (** cases **) |
1242 |
1265 |
1243 fun apply_case ({fixes, assumes, binds}: RuleCases.T) ctxt = |
1266 fun apply_case ({fixes, assumes, binds}: RuleCases.T) ctxt = |
1244 let |
1267 let |
1245 fun bind (x, T) c = (bind_skolem c [x] (Free (x, T)), c |> fix_i [([x], SOME T)]); |
1268 fun bind (x, T) c = (bind_skolem c [x] (Free (x, T)), c |> fix_i [([x], SOME T)]); |
1246 val (xs, ctxt') = fold_map bind fixes ctxt; |
1269 val (xs, ctxt') = fold_map bind fixes ctxt; |
1247 fun app t = Library.foldl Term.betapply (t, xs); |
1270 fun app t = Term.betapplys (t, xs); |
1248 in ((map (apsnd (Option.map app)) binds, map (apsnd (map app)) assumes), ctxt') end; |
1271 in ((map (apsnd (Option.map app)) binds, map (apsnd (map app)) assumes), ctxt') end; |
1249 |
1272 |
1250 local |
1273 local |
1251 |
1274 |
1252 fun prep_case ctxt name xs {fixes, assumes, binds} = |
1275 fun prep_case ctxt name xs {fixes, assumes, binds} = |
1253 let |
1276 let |
1254 fun replace (opt_x :: xs) ((y, T) :: ys) = (if_none opt_x y, T) :: replace xs ys |
1277 fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys |
1255 | replace [] ys = ys |
1278 | replace [] ys = ys |
1256 | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt); |
1279 | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt); |
1257 in |
1280 in |
1258 if null (foldr Term.add_typ_tvars [] (map snd fixes)) andalso |
1281 if null (fold (Term.add_tvarsT o snd) fixes []) andalso |
1259 null (foldr Term.add_term_vars [] (List.concat (map snd assumes))) then |
1282 null (fold (fold Term.add_vars o snd) assumes []) then |
1260 {fixes = replace xs fixes, assumes = assumes, binds = map drop_schematic binds} |
1283 {fixes = replace xs fixes, assumes = assumes, binds = map drop_schematic binds} |
1261 else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt) |
1284 else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt) |
1262 end; |
1285 end; |
1263 |
1286 |
1264 fun rem_case name = remove (fn (x: string, (y, _)) => x = y) name; |
1287 fun rem_case name = remove (fn (x: string, (y, _)) => x = y) name; |