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