# HG changeset patch
# User huffman
# Date 1128915002 -7200
# Node ID 9942c5ed866aa614950fb945ec166b938476c810
# Parent  ccf54e3cabfa1f6d040c9e51c31e7eaf416e4301
new syntax translations for continuous lambda abstraction

diff -r ccf54e3cabfa -r 9942c5ed866a src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Mon Oct 10 04:38:26 2005 +0200
+++ b/src/HOLCF/Cfun.thy	Mon Oct 10 05:30:02 2005 +0200
@@ -25,20 +25,56 @@
 cpodef (CFun)  ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}"
 by (simp add: Ex_cont adm_cont)
 
+syntax (xsymbols)
+  "->"     :: "[type, type] => type"      ("(_ \<rightarrow>/ _)" [1,0]0)
+
 syntax
-  Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("_$_" [999,1000] 999)
-                                                (* application *)
-  Abs_CFun :: "('a => 'b) => ('a -> 'b)" (binder "LAM " 10)
-                                                (* abstraction *)
+  Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("_$_" [999,1000] 999)
+  "_Lambda" :: "[pttrns, 'a] \<Rightarrow> logic"  ("(3LAM _./ _)" [0, 10] 10)
 
 syntax (xsymbols)
-  "->"     :: "[type, type] => type"      ("(_ \<rightarrow>/ _)" [1,0]0)
-  "LAM "   :: "[idts, 'a => 'b] => ('a -> 'b)"
-					("(3\<Lambda>_./ _)" [0, 10] 10)
-  Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("(_\<cdot>_)" [999,1000] 999)
+  "_Lambda"   :: "[pttrns, 'a] \<Rightarrow> logic" ("(3\<Lambda>_./ _)" [0, 10] 10)
+  Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_\<cdot>_)" [999,1000] 999)
 
 syntax (HTML output)
-  Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("(_\<cdot>_)" [999,1000] 999)
+  Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_\<cdot>_)" [999,1000] 999)
+
+syntax
+  "_cabs" :: "[pttrn, 'a] \<Rightarrow> logic"
+translations
+  "_cabs x t" == "Abs_CFun (%x. t)"
+
+(* To avoid eta-contraction of body: *)
+print_translation {*
+let
+  fun cabs_tr' [Abs abs] =
+    let val (x,t) = atomic_abs_tr' abs
+    in Syntax.const "_cabs" $ x $ t end
+in [("Abs_CFun", cabs_tr')] end
+*}
+
+parse_ast_translation {*
+(* rewrites (LAM x y z. t) --> (LAM x. LAM y. LAM z. t) *)
+(* c.f. Syntax.lambda_ast_tr from Syntax/syn_trans.ML *)
+let
+  fun Lambda_ast_tr [pats, body] =
+        Syntax.fold_ast_p "_cabs" (Syntax.unfold_ast "_pttrns" pats, body)
+    | Lambda_ast_tr asts = raise Syntax.AST ("lambda_ast_tr", asts);
+in [("_Lambda", Lambda_ast_tr)] end
+*}
+
+print_ast_translation {*
+(* rewrites (LAM x. LAM y. LAM z. t) --> (LAM x y z. t) *)
+(* c.f. Syntax.abs_ast_tr' from Syntax/syn_trans.ML *)
+let
+  fun cabs_ast_tr' asts =
+    (case Syntax.unfold_ast_p "_cabs"
+        (Syntax.Appl (Syntax.Constant "_cabs" :: asts)) of
+      ([], _) => raise Syntax.AST ("abs_ast_tr'", asts)
+    | (xs, body) => Syntax.Appl
+        [Syntax.Constant "_Lambda", Syntax.fold_ast "_pttrns" xs, body]);
+in [("_cabs", cabs_ast_tr')] end
+*}
 
 subsection {* Class instances *}
 
@@ -448,4 +484,17 @@
 lemma strictify2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strictify\<cdot>f\<cdot>x = f\<cdot>x"
 by (simp add: strictify_conv_if)
 
+subsection {* Continuous let-bindings *}
+
+constdefs
+  CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b"
+  "CLet \<equiv> \<Lambda> s f. f\<cdot>s"
+
+syntax
+  "_CLet" :: "[letbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10)
+
+translations
+  "_CLet (_binds b bs) e" == "_CLet b (_CLet bs e)"
+  "Let x = a in e" == "CLet$a$(LAM x. e)"
+
 end
diff -r ccf54e3cabfa -r 9942c5ed866a src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Mon Oct 10 04:38:26 2005 +0200
+++ b/src/HOLCF/Cprod.thy	Mon Oct 10 05:30:02 2005 +0200
@@ -195,49 +195,19 @@
   "<x, y, z>" == "<x, <y, z>>"
   "<x, y>"    == "cpair$x$y"
 
+syntax
+  "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn"  ("<_,/ _>")
+
+translations
+  "LAM <x,y,zs>. t"       == "csplit$(LAM x <y,zs>. t)"
+  "LAM <x,y>. t"          == "csplit$(LAM x y. t)"
+
 defs
   cpair_def:  "cpair  \<equiv> (\<Lambda> x y. (x, y))"
   cfst_def:   "cfst   \<equiv> (\<Lambda> p. fst p)"
   csnd_def:   "csnd   \<equiv> (\<Lambda> p. snd p)"      
   csplit_def: "csplit \<equiv> (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
 
-subsection {* Syntax *}
-
-text {* syntax for @{text "LAM <x,y,z>.e"} *}
-
-syntax
-  "_LAM" :: "[patterns, 'a \<Rightarrow> 'b] \<Rightarrow> ('a \<rightarrow> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
-
-translations
-  "LAM <x,y,zs>. b"       == "csplit$(LAM x. LAM <y,zs>. b)"
-  "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
-  "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
-
-syntax (xsymbols)
-  "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
-
-text {* syntax for Let *}
-
-constdefs
-  CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b"
-  "CLet \<equiv> \<Lambda> s f. f\<cdot>s"
-
-nonterminals
-  Cletbinds  Cletbind
-
-syntax
-  "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
-  "_Cbindp" :: "[patterns, 'a] => Cletbind"          ("(2<_> =/ _)" 10)
-  ""        :: "Cletbind => Cletbinds"               ("_")
-  "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
-  "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)
-
-translations
-  "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
-  "Let x = a in LAM ys. e"  == "CLet$a$(LAM x ys. e)"
-  "Let x = a in e"          == "CLet$a$(LAM x. e)"
-  "Let <xs> = a in e"       == "CLet$a$(LAM <xs>. e)"
-
 subsection {* Convert all lemmas to the continuous versions *}
 
 lemma cpair_eq_pair: "<x, y> = (x, y)"
diff -r ccf54e3cabfa -r 9942c5ed866a src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Mon Oct 10 04:38:26 2005 +0200
+++ b/src/HOLCF/Fix.thy	Mon Oct 10 05:30:02 2005 +0200
@@ -35,17 +35,13 @@
 subsection {* Binder syntax for @{term fix} *}
 
 syntax
-  "@FIX" :: "('a => 'a) => 'a"  (binder "FIX " 10)
-  "@FIXP" :: "[patterns, 'a] => 'a"  ("(3FIX <_>./ _)" [0, 10] 10)
+  "_FIX" :: "[pttrn, 'a] => 'a" ("(3FIX _./ _)" [0, 10] 10)
 
 syntax (xsymbols)
-  "FIX " :: "[idt, 'a] => 'a"  ("(3\<mu>_./ _)" [0, 10] 10)
-  "@FIXP" :: "[patterns, 'a] => 'a"  ("(3\<mu>()<_>./ _)" [0, 10] 10)
+  "_FIX" :: "[pttrn, 'a] => 'a" ("(3\<mu>_./ _)" [0, 10] 10)
 
 translations
-  "FIX x. LAM y. t" == "fix\<cdot>(LAM x y. t)"
-  "FIX x. t" == "fix\<cdot>(LAM x. t)"
-  "FIX <xs>. t" == "fix\<cdot>(LAM <xs>. t)"
+  "FIX x. t" == "fix$(LAM x. t)"
 
 subsection {* Properties of @{term iterate} and @{term fix} *}
 
diff -r ccf54e3cabfa -r 9942c5ed866a src/HOLCF/domain/syntax.ML
--- a/src/HOLCF/domain/syntax.ML	Mon Oct 10 04:38:26 2005 +0200
+++ b/src/HOLCF/domain/syntax.ML	Mon Oct 10 05:30:02 2005 +0200
@@ -75,9 +75,8 @@
 	fun case1 n (con,mx,args) = mk_appl (Constant "_case1")
 		 [Library.foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)),
 		  expvar n];
-	fun arg1 n (con,_,args) = if args = [] then expvar n 
-				  else mk_appl (Constant "LAM ") 
-		 [foldr1 (app "_idts") (mapn (argvar n) 1 args) , expvar n];
+	fun cabs (x,t) = mk_appl (Constant "_cabs") [x,t];
+	fun arg1 n (con,_,args) = foldr cabs (expvar n) (mapn (argvar n) 1 args);
   in
     ParsePrintRule
       (mk_appl (Constant "_case_syntax") [Variable "x", foldr1