# HG changeset patch # User wenzelm # Date 1165510722 -3600 # Node ID 44cc5b3bb5bfab1ba69c73f343653c9b01e40a24 # Parent 6947e32b61717093dc8843399e53eb34754e7b9b Common term syntax declarations. diff -r 6947e32b6171 -r 44cc5b3bb5bf src/Pure/Isar/term_syntax.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/term_syntax.ML Thu Dec 07 17:58:42 2006 +0100 @@ -0,0 +1,49 @@ +(* Title: Pure/Isar/term_syntax.ML + ID: $Id$ + Author: Makarius + +Common term syntax declarations. +*) + +signature TERM_SYNTAX = +sig + val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory + val abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> local_theory -> local_theory +end; + +structure TermSyntax: TERM_SYNTAX = +struct + +(* notation *) (* FIXME dynamic scoping!? *) + +fun target_notation mode args phi = + let val args' = filter (fn (t, _) => t aconv Morphism.term phi t) args + in Context.mapping (Sign.add_notation mode args') (ProofContext.add_notation mode args') end; + +fun notation mode raw_args lthy = + let val args = map (apfst (Morphism.term (LocalTheory.target_morphism lthy))) raw_args + in LocalTheory.term_syntax (target_notation mode args) lthy end; + + +(* abbrevs *) + +fun morph_abbrev phi ((c, mx), rhs) = ((Morphism.name phi c, mx), Morphism.term phi rhs); + +fun abbrevs prmode raw_args lthy = + let + val mode = #1 prmode; + val args = map (morph_abbrev (LocalTheory.target_morphism lthy)) raw_args; + in + lthy |> LocalTheory.term_syntax (fn phi => + let + val args' = map (morph_abbrev phi) args; + val (abbrs, mxs) = (args ~~ args') |> map_filter (fn ((_, rhs), ((c', mx'), rhs')) => + if rhs aconv rhs' then SOME ((c', rhs'), mx') else NONE) + |> split_list; + in + Context.mapping_result (Sign.add_abbrevs mode abbrs) (ProofContext.add_abbrevs mode abbrs) + #-> (fn res => target_notation prmode (map (Const o #1) res ~~ mxs) phi) + end) + end; + +end;