# HG changeset patch # User wenzelm # Date 1136633195 -3600 # Node ID b026652ede90d629951ffa5ac176217c9f3a17c1 # Parent 9cdcc2a5c8b36653e0b3d47e953e987a08501d7a support nested cases; tuned apply_case; diff -r 9cdcc2a5c8b3 -r b026652ede90 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Jan 07 12:26:33 2006 +0100 +++ b/src/Pure/Isar/proof_context.ML Sat Jan 07 12:26:35 2006 +0100 @@ -141,10 +141,9 @@ val fix_frees: term list -> context -> context val auto_fix: context * (term list list * 'a) -> context * (term list list * 'a) val bind_skolem: context -> string list -> term -> term - val apply_case: RuleCases.T -> context - -> ((indexname * term option) list * (string * term list) list) * context + val add_cases: bool -> (string * RuleCases.T option) list -> context -> context + val apply_case: RuleCases.T -> context -> (string * term list) list * context val get_case: context -> string -> string option list -> RuleCases.T - val add_cases: bool -> (string * RuleCases.T option) list -> context -> context val verbose: bool ref val setmp_verbose: ('a -> 'b) -> 'a -> 'b val print_syntax: context -> unit @@ -1265,43 +1264,56 @@ (** cases **) -fun apply_case ({fixes, assumes, binds}: RuleCases.T) ctxt = - let - fun bind (x, T) c = (bind_skolem c [x] (Free (x, T)), c |> fix_i [([x], SOME T)]); - val (xs, ctxt') = fold_map bind fixes ctxt; - fun app t = Term.betapplys (t, xs); - in ((map (apsnd (Option.map app)) binds, map (apsnd (map app)) assumes), ctxt') end; - local -fun prep_case ctxt name xs {fixes, assumes, binds} = - let - fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys - | replace [] ys = ys - | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt); - in - if null (fold (Term.add_tvarsT o snd) fixes []) andalso - null (fold (fold Term.add_vars o snd) assumes []) then - {fixes = replace xs fixes, assumes = assumes, binds = map drop_schematic binds} - else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt) - end; - fun rem_case name = remove (fn (x: string, (y, _)) => x = y) name; fun add_case _ ("", _) cases = cases | add_case _ (name, NONE) cases = rem_case name cases | add_case is_proper (name, SOME c) cases = (name, (c, is_proper)) :: rem_case name cases; +val bind_fixes = fold_map (fn (x, T) => fn ctxt => + (bind_skolem ctxt [x] (Free (x, T)), ctxt |> fix_i [([x], SOME T)])); + +fun prep_case ctxt name fxs c = + let + fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys + | replace [] ys = ys + | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt); + val RuleCases.Case {fixes, assumes, binds, cases} = c; + val fixes' = replace fxs fixes; + val binds' = map drop_schematic binds; + in + if null (fold (Term.add_tvarsT o snd) fixes []) andalso + null (fold (fold Term.add_vars o snd) assumes []) then + RuleCases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases} + else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt) + end; + in +fun add_cases is_proper xs = map_context (fn (syntax, asms, binds, thms, cases, defs) => + (syntax, asms, binds, thms, fold (add_case is_proper) xs cases, defs)); + +fun case_result c ctxt = + let + val RuleCases.Case {fixes, ...} = c; + val (xs, ctxt') = bind_fixes fixes ctxt; + val RuleCases.Case {assumes, binds, cases, ...} = RuleCases.apply xs c; + in + ctxt' + |> add_binds_i binds + |> add_cases true (map (apsnd SOME) cases) + |> pair (assumes, (binds, cases)) + end; + +val apply_case = apfst fst oo case_result; + fun get_case ctxt name xs = (case AList.lookup (op =) (cases_of ctxt) name of NONE => raise CONTEXT ("Unknown case: " ^ quote name, ctxt) | SOME (c, _) => prep_case ctxt name xs c); -fun add_cases is_proper xs = map_context (fn (syntax, asms, binds, thms, cases, defs) => - (syntax, asms, binds, thms, fold (add_case is_proper) xs cases, defs)); - end; @@ -1310,7 +1322,6 @@ val verbose = ref false; fun verb f x = if ! verbose then f (x ()) else []; -fun verb_single x = verb Library.single x; fun setmp_verbose f x = Library.setmp verbose true f x; @@ -1368,16 +1379,18 @@ | prt_sect s sep prt xs = [Pretty.block (Pretty.breaks (Pretty.str s :: List.concat (Library.separate sep (map (Library.single o prt) xs))))]; - fun prt_case (name, (fixes, (lets, asms))) = Pretty.block (Pretty.fbreaks + fun prt_case (name, (fixes, (asms, (lets, cs)))) = Pretty.block (Pretty.fbreaks (Pretty.str (name ^ ":") :: prt_sect "fix" [] (Pretty.str o fst) fixes @ prt_sect "let" [Pretty.str "and"] prt_let (List.mapPartial (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @ (if forall (null o #2) asms then [] - else prt_sect "assume" [Pretty.str "and"] prt_asm asms))); + else prt_sect "assume" [Pretty.str "and"] prt_asm asms) @ + prt_sect "subcases:" [] (Pretty.str o fst) cs)); fun add_case (_, (_, false)) = I - | add_case (name, (c, true)) = cons (name, (#fixes c, #1 (apply_case c ctxt))); + | add_case (name, (c as RuleCases.Case {fixes, ...}, true)) = + cons (name, (fixes, #1 (case_result c ctxt))); val cases = fold add_case (cases_of ctxt) []; in if null cases andalso not (! verbose) then [] @@ -1449,14 +1462,14 @@ val (types, sorts, used, _) = defaults_of ctxt; in - verb_single (K pretty_thy) @ + verb single (K pretty_thy) @ pretty_asms ctxt @ verb pretty_binds (K ctxt) @ verb pretty_lthms (K ctxt) @ verb pretty_cases (K ctxt) @ - verb_single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @ - verb_single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) @ - verb_single (fn () => Pretty.strs ("used type variable names:" :: used)) + verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @ + verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) @ + verb single (fn () => Pretty.strs ("used type variable names:" :: used)) end; end;