src/CCL/Term.thy
changeset 35113 1a0c129bb2e0
parent 32154 9721e8e4d48c
child 42051 dbdd4790da34
--- a/src/CCL/Term.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/CCL/Term.thy	Thu Feb 11 22:19:58 2010 +0100
@@ -40,16 +40,16 @@
   letrec3    :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"
 
 syntax
-  "@let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
+  "_let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
                         [0,0,60] 60)
 
-  "@letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
+  "_letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
                         [0,0,0,60] 60)
 
-  "@letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
+  "_letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
                         [0,0,0,0,60] 60)
 
-  "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
+  "_letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
                         [0,0,0,0,0,60] 60)
 
 ML {*
@@ -58,29 +58,30 @@
 (* FIXME does not handle "_idtdummy" *)
 (* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *)
 
-fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b);
+fun let_tr [Free(id,T),a,b] = Const(@{const_syntax let},dummyT) $ a $ absfree(id,T,b);
 fun let_tr' [a,Abs(id,T,b)] =
      let val (id',b') = variant_abs(id,T,b)
-     in Const("@let",dummyT) $ Free(id',T) $ a $ b' end;
+     in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end;
 
 fun letrec_tr [Free(f,S),Free(x,T),a,b] =
-      Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
+      Const(@{const_syntax letrec},dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
 fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] =
-      Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
+      Const(@{const_syntax letrec2},dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
 fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] =
-      Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
+      Const(@{const_syntax letrec3},dummyT) $
+        absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
 
 fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
      let val (f',b')  = variant_abs(ff,SS,b)
          val (_,a'') = variant_abs(f,S,a)
          val (x',a')  = variant_abs(x,T,a'')
-     in Const("@letrec",dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
+     in Const(@{syntax_const "_letrec"},dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
 fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
      let val (f',b') = variant_abs(ff,SS,b)
          val ( _,a1) = variant_abs(f,S,a)
          val (y',a2) = variant_abs(y,U,a1)
          val (x',a') = variant_abs(x,T,a2)
-     in Const("@letrec2",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
+     in Const(@{syntax_const "_letrec2"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
       end;
 fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
      let val (f',b') = variant_abs(ff,SS,b)
@@ -88,22 +89,24 @@
          val (z',a2) = variant_abs(z,V,a1)
          val (y',a3) = variant_abs(y,U,a2)
          val (x',a') = variant_abs(x,T,a3)
-     in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
+     in Const(@{syntax_const "_letrec3"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
       end;
 
 *}
 
 parse_translation {*
-  [("@let",       let_tr),
-   ("@letrec",    letrec_tr),
-   ("@letrec2",   letrec2_tr),
-   ("@letrec3",   letrec3_tr)] *}
+ [(@{syntax_const "_let"}, let_tr),
+  (@{syntax_const "_letrec"}, letrec_tr),
+  (@{syntax_const "_letrec2"}, letrec2_tr),
+  (@{syntax_const "_letrec3"}, letrec3_tr)]
+*}
 
 print_translation {*
-  [("let",       let_tr'),
-   ("letrec",    letrec_tr'),
-   ("letrec2",   letrec2_tr'),
-   ("letrec3",   letrec3_tr')] *}
+ [(@{const_syntax let}, let_tr'),
+  (@{const_syntax letrec}, letrec_tr'),
+  (@{const_syntax letrec2}, letrec2_tr'),
+  (@{const_syntax letrec3}, letrec3_tr')]
+*}
 
 consts
   napply     :: "[i=>i,i,i]=>i"            ("(_ ^ _ ` _)" [56,56,56] 56)