rudimentary user-syntax for terms
authorhaftmann
Wed Apr 09 08:10:09 2008 +0200 (2008-04-09)
changeset 2658758fb6e033c00
parent 26586 a2255b130fd9
child 26588 d83271bfaba5
rudimentary user-syntax for terms
src/HOL/Library/Eval.thy
     1.1 --- a/src/HOL/Library/Eval.thy	Wed Apr 09 05:44:14 2008 +0200
     1.2 +++ b/src/HOL/Library/Eval.thy	Wed Apr 09 08:10:09 2008 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  subsection {* Term representation *}
     1.6  
     1.7 -subsubsection {* Definitions *}
     1.8 +subsubsection {* Terms and class @{text term_of} *}
     1.9  
    1.10  datatype "term" = dummy_term
    1.11  
    1.12 @@ -29,9 +29,6 @@
    1.13  
    1.14  code_datatype Const App
    1.15  
    1.16 -
    1.17 -subsubsection {* Class @{term term_of} *}
    1.18 -
    1.19  class term_of = rtype +
    1.20    fixes term_of :: "'a \<Rightarrow> term"
    1.21  
    1.22 @@ -47,13 +44,17 @@
    1.23    | mk_term f g (t1 $ t2) =
    1.24        @{term App} $ mk_term f g t1 $ mk_term f g t2
    1.25    | mk_term f g (Free v) = f v
    1.26 -  | mk_term f g (Bound i) = Bound i;
    1.27 +  | mk_term f g (Bound i) = Bound i
    1.28 +  | mk_term f g (Abs (v, _, t)) = Abs (v, @{typ term}, mk_term f g t);
    1.29  
    1.30  fun mk_term_of ty t = Const (@{const_name term_of}, ty --> @{typ term}) $ t;
    1.31  
    1.32  end;
    1.33  *}
    1.34  
    1.35 +
    1.36 +subsubsection {* @{text term_of} instances *}
    1.37 +
    1.38  setup {*
    1.39  let
    1.40    fun add_term_of_def ty vs tyco thy =
    1.41 @@ -130,6 +131,7 @@
    1.42  end
    1.43  *}
    1.44  
    1.45 +
    1.46  subsubsection {* Code generator setup *}
    1.47  
    1.48  lemmas [code func del] = term.recs term.cases term.size
    1.49 @@ -153,6 +155,72 @@
    1.50    (SML "Message'_String.mk")
    1.51  
    1.52  
    1.53 +subsubsection {* Syntax *}
    1.54 +
    1.55 +print_translation {*
    1.56 +let
    1.57 +  val term = Const ("<TERM>", dummyT);
    1.58 +  fun tr1' [_, _] = term;
    1.59 +  fun tr2' [] = term;
    1.60 +in
    1.61 +  [(@{const_syntax Const}, tr1'),
    1.62 +    (@{const_syntax App}, tr1'),
    1.63 +    (@{const_syntax dummy_term}, tr2')]
    1.64 +end
    1.65 +*}
    1.66 +setup {*
    1.67 +  Sign.declare_const [] ("rterm_of", @{typ "'a \<Rightarrow> 'b"}, NoSyn)
    1.68 +  #> snd
    1.69 +*}
    1.70 +
    1.71 +notation (output)
    1.72 +  rterm_of ("\<guillemotleft>_\<guillemotright>")
    1.73 +
    1.74 +locale (open) rterm_syntax =
    1.75 +  fixes rterm_of_syntax :: "'a \<Rightarrow> 'b" ("\<guillemotleft>_\<guillemotright>")
    1.76 +
    1.77 +parse_translation {*
    1.78 +let
    1.79 +  fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t
    1.80 +    | rterm_of_tr ts = raise TERM ("rterm_of_tr", ts);
    1.81 +in
    1.82 +  [("\<^fixed>rterm_of_syntax", rterm_of_tr)]
    1.83 +end
    1.84 +*}
    1.85 +
    1.86 +setup {*
    1.87 +let
    1.88 +  val subst_rterm_of = Eval.mk_term
    1.89 +    (fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v))
    1.90 +    (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort))));
    1.91 +  fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t
    1.92 +    | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) =
    1.93 +        error ("illegal number of arguments for " ^ quote @{const_name rterm_of})
    1.94 +    | subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts);
    1.95 +  fun subst_rterm_of'' t = 
    1.96 +    let
    1.97 +      val t' = subst_rterm_of' (strip_comb t);
    1.98 +    in if t aconv t'
    1.99 +      then NONE
   1.100 +      else SOME t'
   1.101 +    end;
   1.102 +  fun check_rterm_of ts ctxt =
   1.103 +    let
   1.104 +      val ts' = map subst_rterm_of'' ts;
   1.105 +    in if exists is_some ts'
   1.106 +      then SOME (map2 the_default ts ts', ctxt)
   1.107 +      else NONE
   1.108 +    end;
   1.109 +in
   1.110 +  Context.theory_map (Syntax.add_term_check 0 "rterm_of" check_rterm_of)
   1.111 +end;
   1.112 +*}
   1.113 +
   1.114 +hide const dummy_term
   1.115 +hide (open) const Const App
   1.116 +hide (open) const term_of
   1.117 +
   1.118 +
   1.119  subsection {* Evaluation setup *}
   1.120  
   1.121  ML {*
   1.122 @@ -223,20 +291,4 @@
   1.123             (Eval.evaluate_cmd some_name t)));
   1.124  *}
   1.125  
   1.126 -print_translation {*
   1.127 -let
   1.128 -  val term = Const ("<TERM>", dummyT);
   1.129 -  fun tr1' [_, _] = term;
   1.130 -  fun tr2' [] = term;
   1.131 -in
   1.132 -  [(@{const_syntax Const}, tr1'),
   1.133 -    (@{const_syntax App}, tr1'),
   1.134 -    (@{const_syntax dummy_term}, tr2')]
   1.135  end
   1.136 -*}
   1.137 -
   1.138 -hide (open) const term_of
   1.139 -hide (open) const Const App
   1.140 -hide const dummy_term
   1.141 -
   1.142 -end