768 in |
768 in |
769 Seq.map apply_text texts |
769 Seq.map apply_text texts |
770 end) |
770 end) |
771 end; |
771 end; |
772 |
772 |
773 val match_parser = |
|
774 parse_match_kind :-- (fn kind => |
|
775 Scan.lift @{keyword "in"} |-- Parse.enum1' "\<bar>" (parse_named_pats kind)) >> |
|
776 (fn (matches, bodies) => fn ctxt => fn using => |
|
777 Method.RUNTIME (fn st => |
|
778 let |
|
779 fun exec (pats, fixes, text) goal = |
|
780 let |
|
781 val ctxt' = |
|
782 fold Variable.declare_term fixes ctxt |
|
783 |> fold (fn (_, t) => Variable.declare_term t) pats; (*Is this a good idea? We really only care about the maxidx*) |
|
784 in real_match using ctxt' fixes matches text pats goal end; |
|
785 in Seq.flat (Seq.FIRST (map exec bodies) st) end)); |
|
786 |
|
787 val _ = |
773 val _ = |
788 Theory.setup |
774 Theory.setup |
789 (Method.setup @{binding match} |
775 (Method.setup @{binding match} |
790 (match_parser >> (fn m => fn ctxt => METHOD_CASES (m ctxt))) |
776 (parse_match_kind :-- |
|
777 (fn kind => Scan.lift @{keyword "in"} |-- Parse.enum1' "\<bar>" (parse_named_pats kind)) >> |
|
778 (fn (matches, bodies) => fn ctxt => |
|
779 METHOD_CASES (fn using => Method.RUNTIME (fn st => |
|
780 let |
|
781 fun exec (pats, fixes, text) goal = |
|
782 let |
|
783 val ctxt' = |
|
784 fold Variable.declare_term fixes ctxt |
|
785 (*FIXME Is this a good idea? We really only care about the maxidx*) |
|
786 |> fold (fn (_, t) => Variable.declare_term t) pats; |
|
787 in real_match using ctxt' fixes matches text pats goal end; |
|
788 in Seq.flat (Seq.FIRST (map exec bodies) st) end)))) |
791 "structural analysis/matching on goals"); |
789 "structural analysis/matching on goals"); |
792 |
790 |
793 end; |
791 end; |