src/HOL/ex/Term_Of_Syntax.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 28965 1de908189869
child 31139 0b615ac7eeaf
permissions -rw-r--r--
added lemmas
haftmann@28258
     1
(*  Title:      HOL/ex/Term_Of_Syntax.thy
haftmann@28258
     2
    ID:         $Id$
haftmann@28258
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@28258
     4
*)
haftmann@28258
     5
haftmann@28258
     6
header {* Input syntax for term_of functions *}
haftmann@28258
     7
haftmann@28258
     8
theory Term_Of_Syntax
haftmann@28258
     9
imports Code_Eval
haftmann@28258
    10
begin
haftmann@28258
    11
haftmann@28258
    12
setup {*
haftmann@28965
    13
  Sign.declare_const [] ((Binding.name "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn)
haftmann@28258
    14
  #> snd
haftmann@28258
    15
*}
haftmann@28258
    16
haftmann@28258
    17
notation (output)
haftmann@28258
    18
  rterm_of ("\<guillemotleft>_\<guillemotright>")
haftmann@28258
    19
haftmann@28258
    20
locale rterm_syntax =
haftmann@28258
    21
  fixes rterm_of_syntax :: "'a \<Rightarrow> 'b" ("\<guillemotleft>_\<guillemotright>")
haftmann@28258
    22
haftmann@28258
    23
parse_translation {*
haftmann@28258
    24
let
haftmann@28258
    25
  fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t
haftmann@28258
    26
    | rterm_of_tr ts = raise TERM ("rterm_of_tr", ts);
haftmann@28258
    27
in
haftmann@28258
    28
  [(Syntax.fixedN ^ "rterm_of_syntax", rterm_of_tr)]
haftmann@28258
    29
end
haftmann@28258
    30
*}
haftmann@28258
    31
haftmann@28258
    32
setup {*
haftmann@28258
    33
let
haftmann@28258
    34
  val subst_rterm_of = Eval.mk_term
haftmann@28258
    35
    (fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v))
haftmann@28335
    36
    (Typerep.mk (fn (v, sort) => Typerep.typerep (TFree (v, sort))));
haftmann@28258
    37
  fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t
haftmann@28258
    38
    | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) =
haftmann@28258
    39
        error ("illegal number of arguments for " ^ quote @{const_name rterm_of})
haftmann@28258
    40
    | subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts);
haftmann@28258
    41
  fun subst_rterm_of'' t = 
haftmann@28258
    42
    let
haftmann@28258
    43
      val t' = subst_rterm_of' (strip_comb t);
haftmann@28258
    44
    in if t aconv t'
haftmann@28258
    45
      then NONE
haftmann@28258
    46
      else SOME t'
haftmann@28258
    47
    end;
haftmann@28258
    48
  fun check_rterm_of ts ctxt =
haftmann@28258
    49
    let
haftmann@28258
    50
      val ts' = map subst_rterm_of'' ts;
haftmann@28258
    51
    in if exists is_some ts'
haftmann@28258
    52
      then SOME (map2 the_default ts ts', ctxt)
haftmann@28258
    53
      else NONE
haftmann@28258
    54
    end;
haftmann@28258
    55
in
haftmann@28258
    56
  Context.theory_map (Syntax.add_term_check 0 "rterm_of" check_rterm_of)
haftmann@28258
    57
end;
haftmann@28258
    58
*}
haftmann@28258
    59
haftmann@28258
    60
end