src/CCL/Term.thy
author clasohm
Wed, 21 Jun 1995 15:01:07 +0200
changeset 1149 5750eba8820d
parent 998 91d09e262799
child 1474 3f7d67927fe2
permissions -rw-r--r--
removed \...\ inside strings
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	CCL/terms.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Martin Coen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Definitions of usual program constructs in CCL.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
Term = CCL +
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
consts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    14
  one        :: "i"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    16
  if         :: "[i,i,i]=>i"           ("(3if _/ then _/ else _)" [0,0,60] 60)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    18
  inl,inr    :: "i=>i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    19
  when       :: "[i,i=>i,i=>i]=>i" 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    21
  split      :: "[i,[i,i]=>i]=>i"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  fst,snd,   
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    23
  thd        :: "i=>i"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    25
  zero       :: "i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    26
  succ       :: "i=>i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    27
  ncase      :: "[i,i,i=>i]=>i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    28
  nrec       :: "[i,i,[i,i]=>i]=>i"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    30
  nil        :: "i"                        ("([])")
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    31
  "$"        :: "[i,i]=>i"                 (infixr 80)
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    32
  lcase      :: "[i,i,[i,i]=>i]=>i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    33
  lrec       :: "[i,i,[i,i,i]=>i]=>i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    34
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    35
  let        :: "[i,i=>i]=>i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    36
  letrec     :: "[[i,i=>i]=>i,(i=>i)=>i]=>i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    37
  letrec2    :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    38
  letrec3    :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"  
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    40
  "@let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    41
  			[0,0,60] 60)
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    42
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    43
  "@letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    44
  			[0,0,0,60] 60)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    46
  "@letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    47
  			[0,0,0,0,60] 60)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    49
  "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    50
  			[0,0,0,0,0,60] 60)
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    51
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    52
  napply     :: "[i=>i,i,i]=>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
  one_def                    "one == true"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
  if_def     "if b then t else u  == case(b,t,u,% x y.bot,%v.bot)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
  inl_def                 "inl(a) == <true,a>"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
  inr_def                 "inr(b) == <false,b>"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
  when_def           "when(t,f,g) == split(t,%b x.if b then f(x) else g(x))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
  split_def           "split(t,f) == case(t,bot,bot,f,%u.bot)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
  fst_def                 "fst(t) == split(t,%x y.x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
  snd_def                 "snd(t) == split(t,%x y.y)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
  thd_def                 "thd(t) == split(t,%x p.split(p,%y z.z))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
  zero_def                  "zero == inl(one)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
  succ_def               "succ(n) == inr(n)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
  ncase_def         "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
  nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
  nil_def	              "[] == inl(one)"
289
78541329ff35 changed "." to "$" to eliminate ambiguity
clasohm
parents: 0
diff changeset
    70
  cons_def                   "h$t == inr(<h,t>)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
  lcase_def         "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
  lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
  let_def  "let x be t in f(x) == case(t,f(true),f(false),%x y.f(<x,y>),%u.f(lam x.u(x)))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
  letrec_def    
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
  "letrec g x be h(x,g) in b(g) == b(%x.fix(%f.lam x.h(x,%y.f`y))`x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
1149
5750eba8820d removed \...\ inside strings
clasohm
parents: 998
diff changeset
    78
  letrec2_def  "letrec g x y be h(x,y,g) in f(g)== 
5750eba8820d removed \...\ inside strings
clasohm
parents: 998
diff changeset
    79
               letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>))) 
5750eba8820d removed \...\ inside strings
clasohm
parents: 998
diff changeset
    80
                          in f(%x y.g'(<x,y>))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
1149
5750eba8820d removed \...\ inside strings
clasohm
parents: 998
diff changeset
    82
  letrec3_def  "letrec g x y z be h(x,y,z,g) in f(g) == 
5750eba8820d removed \...\ inside strings
clasohm
parents: 998
diff changeset
    83
             letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>)))) 
5750eba8820d removed \...\ inside strings
clasohm
parents: 998
diff changeset
    84
                          in f(%x y z.g'(<x,<y,z>>))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
  napply_def "f ^n` a == nrec(n,a,%x g.f(g))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
(** Quantifier translations: variable binding **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
fun let_tr' [a,Abs(id,T,b)] =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
     let val (id',b') = variant_abs(id,T,b)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
     in Const("@let",dummyT) $ Free(id',T) $ a $ b' end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
fun letrec_tr [Free(f,S),Free(x,T),a,b] = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
      Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
      Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
      Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
     let val (f',b')  = variant_abs(ff,SS,b)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
         val (_,a'') = variant_abs(f,S,a)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
         val (x',a')  = variant_abs(x,T,a'')
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
     in Const("@letrec",dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
     let val (f',b') = variant_abs(ff,SS,b)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
         val ( _,a1) = variant_abs(f,S,a)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
         val (y',a2) = variant_abs(y,U,a1)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
         val (x',a') = variant_abs(x,T,a2)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
     in Const("@letrec2",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
      end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
     let val (f',b') = variant_abs(ff,SS,b)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
         val ( _,a1) = variant_abs(f,S,a)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
         val (z',a2) = variant_abs(z,V,a1)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
         val (y',a3) = variant_abs(y,U,a2)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
         val (x',a') = variant_abs(x,T,a3)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
     in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
      end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
val  parse_translation=
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
    [("@let",       let_tr),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
     ("@letrec",    letrec_tr),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
     ("@letrec2",   letrec2_tr),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
     ("@letrec3",   letrec3_tr)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
    ];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
val print_translation=
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
    [("let",       let_tr'),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
     ("letrec",    letrec_tr'),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
     ("letrec2",   letrec2_tr'),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
     ("letrec3",   letrec3_tr')
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
    ];