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