diff options
| author | Josh Chen | 2020-07-21 02:16:14 +0200 |
|---|---|---|
| committer | GitHub | 2020-07-21 02:16:14 +0200 |
| commit | dfd241b2d85fc5a4ad4d7ddd64adf0138b05f083 (patch) | |
| tree | b4c4280b1bc4426059ddd184a2258d15d20a0bab /spartan/core/rewrite.ML | |
| parent | 6aaf4d5b28a5284b3b02fa5c410d2d83a711840b (diff) | |
| parent | 12eed8685674b7d5ff7bc45a44a061e01f99ce5f (diff) | |
Merge pull request #8 from jaycech3n/dev
Merge big diff on dev
Diffstat (limited to 'spartan/core/rewrite.ML')
| -rw-r--r-- | spartan/core/rewrite.ML | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/spartan/core/rewrite.ML b/spartan/core/rewrite.ML index f9c5d8e..eba0e81 100644 --- a/spartan/core/rewrite.ML +++ b/spartan/core/rewrite.ML @@ -15,8 +15,8 @@ patterns but has diverged significantly during its development. We also allow introduction of identifiers for bound variables, which can then be used to match arbitrary subterms inside abstractions. -This code is slightly modified from the original at HOL/Library/rewrite.ML, -to incorporate auto-typechecking for type theory. +This code has been slightly modified from the original at HOL/Library/rewrite.ML +to incorporate automatic discharge of type-theoretic side conditions. *) infix 1 then_pconv; @@ -448,18 +448,18 @@ val _ = val subst_parser = let val scan = raw_pattern -- to_parser -- Parse.thms1 in context_lift scan prep_args end + + fun rewrite_export_ctac inputs inthms = + CONTEXT_TACTIC' (fn ctxt => rewrite_export_tac ctxt inputs inthms) in Method.setup \<^binding>\<open>rewr\<close> (subst_parser >> - (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => - SIMPLE_METHOD' - (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms))) - "single-step rewriting, allowing subterm selection via patterns" - #> - (Method.setup \<^binding>\<open>rewrite\<close> (subst_parser >> - (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => - SIMPLE_METHOD' (SIDE_CONDS - (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms) - orig_ctxt))) - "single-step rewriting with auto-typechecking") + (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => SIMPLE_METHOD' + (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms))) + "single-step rewriting, allowing subterm selection via patterns" #> + Method.setup \<^binding>\<open>rewrite\<close> (subst_parser >> + (fn (pattern, inthms, (to, pat_ctxt)) => K (CONTEXT_METHOD ( + CHEADGOAL o SIDE_CONDS + (rewrite_export_ctac ((pattern, to), SOME pat_ctxt) inthms))))) + "single-step rewriting with auto-typechecking" end end |