0

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" ("([])")

289

31 
"$" :: "[i,i]=>i" (infixr 80)

0

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 

610

40 
"@let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)" [] 60)


41 
"@letrec" :: "[idt,idt,i,i]=>i" ("(3letrec _ _ be _/ in _)" [] 60)


42 
"@letrec2" :: "[idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ be _/ in _)" [] 60)


43 
"@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" [] 60)

0

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)"

289

63 
cons_def "h$t == inr(<h,t>)"

0

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 
];
