src/CCL/term.thy
changeset 0 a5a9c433f639
child 289 78541329ff35
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/term.thy	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,131 @@
     1.4 +(*  Title: 	CCL/terms.thy
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Martin Coen
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Definitions of usual program constructs in CCL.
    1.10 +
    1.11 +*)
    1.12 +
    1.13 +Term = CCL +
    1.14 +
    1.15 +consts
    1.16 +
    1.17 +  one        ::	      "i"
    1.18 +
    1.19 +  if         ::       "[i,i,i]=>i"           ("(3if _/ then _/ else _)" [] 60)
    1.20 +
    1.21 +  inl,inr    ::	      "i=>i"
    1.22 +  when       ::	      "[i,i=>i,i=>i]=>i" 
    1.23 +
    1.24 +  split      ::	      "[i,[i,i]=>i]=>i"
    1.25 +  fst,snd,   
    1.26 +  thd        ::       "i=>i"
    1.27 +
    1.28 +  zero       ::	      "i"
    1.29 +  succ       ::	      "i=>i"
    1.30 +  ncase      ::	      "[i,i,i=>i]=>i"
    1.31 +  nrec       ::	      "[i,i,[i,i]=>i]=>i"
    1.32 +
    1.33 +  nil        ::       "i"                    ("([])")
    1.34 +  "."        ::       "[i,i]=>i"             (infixr 80)
    1.35 +  lcase      ::	      "[i,i,[i,i]=>i]=>i"
    1.36 +  lrec       ::	      "[i,i,[i,i,i]=>i]=>i"
    1.37 +
    1.38 +  let        ::       "[i,i=>i]=>i"
    1.39 +  letrec     ::       "[[i,i=>i]=>i,(i=>i)=>i]=>i"
    1.40 +  letrec2    ::       "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
    1.41 +  letrec3    ::       "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"  
    1.42 +
    1.43 +  "@let"     ::       "[id,i,i]=>i"             ("(3let _ be _/ in _)" [] 60)
    1.44 +  "@letrec"  ::       "[id,id,i,i]=>i"          ("(3letrec _ _ be _/ in _)"  [] 60)
    1.45 +  "@letrec2" ::       "[id,id,id,i,i]=>i"       ("(3letrec _ _ _ be _/ in _)"  [] 60)
    1.46 +  "@letrec3" ::       "[id,id,id,id,i,i]=>i"    ("(3letrec _ _ _ _ be _/ in _)"  [] 60)
    1.47 +
    1.48 +  napply    :: "[i=>i,i,i]=>i"      ("(_ ^ _ ` _)")
    1.49 +
    1.50 +rules
    1.51 +
    1.52 +  one_def                    "one == true"
    1.53 +  if_def     "if b then t else u  == case(b,t,u,% x y.bot,%v.bot)"
    1.54 +  inl_def                 "inl(a) == <true,a>"
    1.55 +  inr_def                 "inr(b) == <false,b>"
    1.56 +  when_def           "when(t,f,g) == split(t,%b x.if b then f(x) else g(x))"
    1.57 +  split_def           "split(t,f) == case(t,bot,bot,f,%u.bot)"
    1.58 +  fst_def                 "fst(t) == split(t,%x y.x)"
    1.59 +  snd_def                 "snd(t) == split(t,%x y.y)"
    1.60 +  thd_def                 "thd(t) == split(t,%x p.split(p,%y z.z))"
    1.61 +  zero_def                  "zero == inl(one)"
    1.62 +  succ_def               "succ(n) == inr(n)"
    1.63 +  ncase_def         "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
    1.64 +  nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
    1.65 +  nil_def	              "[] == inl(one)"
    1.66 +  cons_def                   "h.t == inr(<h,t>)"
    1.67 +  lcase_def         "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
    1.68 +  lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
    1.69 +
    1.70 +  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)))"
    1.71 +  letrec_def    
    1.72 +  "letrec g x be h(x,g) in b(g) == b(%x.fix(%f.lam x.h(x,%y.f`y))`x)"
    1.73 +
    1.74 +  letrec2_def  "letrec g x y be h(x,y,g) in f(g)== \
    1.75 +\               letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>))) \
    1.76 +\                          in f(%x y.g'(<x,y>))"
    1.77 +
    1.78 +  letrec3_def  "letrec g x y z be h(x,y,z,g) in f(g) == \
    1.79 +\             letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>)))) \
    1.80 +\                          in f(%x y z.g'(<x,<y,z>>))"
    1.81 +
    1.82 +  napply_def "f ^n` a == nrec(n,a,%x g.f(g))"
    1.83 +
    1.84 +end
    1.85 +
    1.86 +ML
    1.87 +
    1.88 +(** Quantifier translations: variable binding **)
    1.89 +
    1.90 +fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b);
    1.91 +fun let_tr' [a,Abs(id,T,b)] =
    1.92 +     let val (id',b') = variant_abs(id,T,b)
    1.93 +     in Const("@let",dummyT) $ Free(id',T) $ a $ b' end;
    1.94 +
    1.95 +fun letrec_tr [Free(f,S),Free(x,T),a,b] = 
    1.96 +      Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
    1.97 +fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] = 
    1.98 +      Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
    1.99 +fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] = 
   1.100 +      Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
   1.101 +
   1.102 +fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
   1.103 +     let val (f',b')  = variant_abs(ff,SS,b)
   1.104 +         val (_,a'') = variant_abs(f,S,a)
   1.105 +         val (x',a')  = variant_abs(x,T,a'')
   1.106 +     in Const("@letrec",dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
   1.107 +fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
   1.108 +     let val (f',b') = variant_abs(ff,SS,b)
   1.109 +         val ( _,a1) = variant_abs(f,S,a)
   1.110 +         val (y',a2) = variant_abs(y,U,a1)
   1.111 +         val (x',a') = variant_abs(x,T,a2)
   1.112 +     in Const("@letrec2",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
   1.113 +      end;
   1.114 +fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
   1.115 +     let val (f',b') = variant_abs(ff,SS,b)
   1.116 +         val ( _,a1) = variant_abs(f,S,a)
   1.117 +         val (z',a2) = variant_abs(z,V,a1)
   1.118 +         val (y',a3) = variant_abs(y,U,a2)
   1.119 +         val (x',a') = variant_abs(x,T,a3)
   1.120 +     in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
   1.121 +      end;
   1.122 +
   1.123 +val  parse_translation=
   1.124 +    [("@let",       let_tr),
   1.125 +     ("@letrec",    letrec_tr),
   1.126 +     ("@letrec2",   letrec2_tr),
   1.127 +     ("@letrec3",   letrec3_tr)
   1.128 +    ];
   1.129 +val print_translation=
   1.130 +    [("let",       let_tr'),
   1.131 +     ("letrec",    letrec_tr'),
   1.132 +     ("letrec2",   letrec2_tr'),
   1.133 +     ("letrec3",   letrec3_tr')
   1.134 +    ];