src/CCL/Term.thy
author wenzelm
Fri Oct 10 17:10:12 1997 +0200 (1997-10-10)
changeset 3837 d7f033c74b38
parent 2709 241fffc25284
child 14765 bafb24c150c1
permissions -rw-r--r--
fixed dots;
     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 _)" [0,0,60] 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"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
    41                         [0,0,60] 60)
    42 
    43   "@letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
    44                         [0,0,0,60] 60)
    45 
    46   "@letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
    47                         [0,0,0,0,60] 60)
    48 
    49   "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
    50                         [0,0,0,0,0,60] 60)
    51 
    52   napply     :: "[i=>i,i,i]=>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
    53 
    54 rules
    55 
    56   one_def                    "one == true"
    57   if_def     "if b then t else u  == case(b,t,u,% x y. bot,%v. bot)"
    58   inl_def                 "inl(a) == <true,a>"
    59   inr_def                 "inr(b) == <false,b>"
    60   when_def           "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))"
    61   split_def           "split(t,f) == case(t,bot,bot,f,%u. bot)"
    62   fst_def                 "fst(t) == split(t,%x y. x)"
    63   snd_def                 "snd(t) == split(t,%x y. y)"
    64   thd_def                 "thd(t) == split(t,%x p. split(p,%y z. z))"
    65   zero_def                  "zero == inl(one)"
    66   succ_def               "succ(n) == inr(n)"
    67   ncase_def         "ncase(n,b,c) == when(n,%x. b,%y. c(y))"
    68   nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)"
    69   nil_def                     "[] == inl(one)"
    70   cons_def                   "h$t == inr(<h,t>)"
    71   lcase_def         "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))"
    72   lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)"
    73 
    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)))"
    75   letrec_def    
    76   "letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)"
    77 
    78   letrec2_def  "letrec g x y be h(x,y,g) in f(g)== 
    79                letrec g' p be split(p,%x y. h(x,y,%u v. g'(<u,v>))) 
    80                           in f(%x y. g'(<x,y>))"
    81 
    82   letrec3_def  "letrec g x y z be h(x,y,z,g) in f(g) == 
    83              letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(<u,<v,w>>)))) 
    84                           in f(%x y z. g'(<x,<y,z>>))"
    85 
    86   napply_def "f ^n` a == nrec(n,a,%x g. f(g))"
    87 
    88 end
    89 
    90 ML
    91 
    92 (** Quantifier translations: variable binding **)
    93 
    94 (* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *)
    95 
    96 fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b);
    97 fun let_tr' [a,Abs(id,T,b)] =
    98      let val (id',b') = variant_abs(id,T,b)
    99      in Const("@let",dummyT) $ Free(id',T) $ a $ b' end;
   100 
   101 fun letrec_tr [Free(f,S),Free(x,T),a,b] = 
   102       Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
   103 fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] = 
   104       Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
   105 fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] = 
   106       Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
   107 
   108 fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
   109      let val (f',b')  = variant_abs(ff,SS,b)
   110          val (_,a'') = variant_abs(f,S,a)
   111          val (x',a')  = variant_abs(x,T,a'')
   112      in Const("@letrec",dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
   113 fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
   114      let val (f',b') = variant_abs(ff,SS,b)
   115          val ( _,a1) = variant_abs(f,S,a)
   116          val (y',a2) = variant_abs(y,U,a1)
   117          val (x',a') = variant_abs(x,T,a2)
   118      in Const("@letrec2",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
   119       end;
   120 fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
   121      let val (f',b') = variant_abs(ff,SS,b)
   122          val ( _,a1) = variant_abs(f,S,a)
   123          val (z',a2) = variant_abs(z,V,a1)
   124          val (y',a3) = variant_abs(y,U,a2)
   125          val (x',a') = variant_abs(x,T,a3)
   126      in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
   127       end;
   128 
   129 val  parse_translation=
   130     [("@let",       let_tr),
   131      ("@letrec",    letrec_tr),
   132      ("@letrec2",   letrec2_tr),
   133      ("@letrec3",   letrec3_tr)
   134     ];
   135 val print_translation=
   136     [("let",       let_tr'),
   137      ("letrec",    letrec_tr'),
   138      ("letrec2",   letrec2_tr'),
   139      ("letrec3",   letrec3_tr')
   140     ];