new syntax translations for continuous lambda abstraction
authorhuffman
Mon Oct 10 05:30:02 2005 +0200 (2005-10-10)
changeset 178169942c5ed866a
parent 17815 ccf54e3cabfa
child 17817 405fb812e738
new syntax translations for continuous lambda abstraction
src/HOLCF/Cfun.thy
src/HOLCF/Cprod.thy
src/HOLCF/Fix.thy
src/HOLCF/domain/syntax.ML
     1.1 --- a/src/HOLCF/Cfun.thy	Mon Oct 10 04:38:26 2005 +0200
     1.2 +++ b/src/HOLCF/Cfun.thy	Mon Oct 10 05:30:02 2005 +0200
     1.3 @@ -25,20 +25,56 @@
     1.4  cpodef (CFun)  ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}"
     1.5  by (simp add: Ex_cont adm_cont)
     1.6  
     1.7 +syntax (xsymbols)
     1.8 +  "->"     :: "[type, type] => type"      ("(_ \<rightarrow>/ _)" [1,0]0)
     1.9 +
    1.10  syntax
    1.11 -  Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("_$_" [999,1000] 999)
    1.12 -                                                (* application *)
    1.13 -  Abs_CFun :: "('a => 'b) => ('a -> 'b)" (binder "LAM " 10)
    1.14 -                                                (* abstraction *)
    1.15 +  Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("_$_" [999,1000] 999)
    1.16 +  "_Lambda" :: "[pttrns, 'a] \<Rightarrow> logic"  ("(3LAM _./ _)" [0, 10] 10)
    1.17  
    1.18  syntax (xsymbols)
    1.19 -  "->"     :: "[type, type] => type"      ("(_ \<rightarrow>/ _)" [1,0]0)
    1.20 -  "LAM "   :: "[idts, 'a => 'b] => ('a -> 'b)"
    1.21 -					("(3\<Lambda>_./ _)" [0, 10] 10)
    1.22 -  Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("(_\<cdot>_)" [999,1000] 999)
    1.23 +  "_Lambda"   :: "[pttrns, 'a] \<Rightarrow> logic" ("(3\<Lambda>_./ _)" [0, 10] 10)
    1.24 +  Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_\<cdot>_)" [999,1000] 999)
    1.25  
    1.26  syntax (HTML output)
    1.27 -  Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("(_\<cdot>_)" [999,1000] 999)
    1.28 +  Rep_CFun :: "('a \<rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" ("(_\<cdot>_)" [999,1000] 999)
    1.29 +
    1.30 +syntax
    1.31 +  "_cabs" :: "[pttrn, 'a] \<Rightarrow> logic"
    1.32 +translations
    1.33 +  "_cabs x t" == "Abs_CFun (%x. t)"
    1.34 +
    1.35 +(* To avoid eta-contraction of body: *)
    1.36 +print_translation {*
    1.37 +let
    1.38 +  fun cabs_tr' [Abs abs] =
    1.39 +    let val (x,t) = atomic_abs_tr' abs
    1.40 +    in Syntax.const "_cabs" $ x $ t end
    1.41 +in [("Abs_CFun", cabs_tr')] end
    1.42 +*}
    1.43 +
    1.44 +parse_ast_translation {*
    1.45 +(* rewrites (LAM x y z. t) --> (LAM x. LAM y. LAM z. t) *)
    1.46 +(* c.f. Syntax.lambda_ast_tr from Syntax/syn_trans.ML *)
    1.47 +let
    1.48 +  fun Lambda_ast_tr [pats, body] =
    1.49 +        Syntax.fold_ast_p "_cabs" (Syntax.unfold_ast "_pttrns" pats, body)
    1.50 +    | Lambda_ast_tr asts = raise Syntax.AST ("lambda_ast_tr", asts);
    1.51 +in [("_Lambda", Lambda_ast_tr)] end
    1.52 +*}
    1.53 +
    1.54 +print_ast_translation {*
    1.55 +(* rewrites (LAM x. LAM y. LAM z. t) --> (LAM x y z. t) *)
    1.56 +(* c.f. Syntax.abs_ast_tr' from Syntax/syn_trans.ML *)
    1.57 +let
    1.58 +  fun cabs_ast_tr' asts =
    1.59 +    (case Syntax.unfold_ast_p "_cabs"
    1.60 +        (Syntax.Appl (Syntax.Constant "_cabs" :: asts)) of
    1.61 +      ([], _) => raise Syntax.AST ("abs_ast_tr'", asts)
    1.62 +    | (xs, body) => Syntax.Appl
    1.63 +        [Syntax.Constant "_Lambda", Syntax.fold_ast "_pttrns" xs, body]);
    1.64 +in [("_cabs", cabs_ast_tr')] end
    1.65 +*}
    1.66  
    1.67  subsection {* Class instances *}
    1.68  
    1.69 @@ -448,4 +484,17 @@
    1.70  lemma strictify2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strictify\<cdot>f\<cdot>x = f\<cdot>x"
    1.71  by (simp add: strictify_conv_if)
    1.72  
    1.73 +subsection {* Continuous let-bindings *}
    1.74 +
    1.75 +constdefs
    1.76 +  CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b"
    1.77 +  "CLet \<equiv> \<Lambda> s f. f\<cdot>s"
    1.78 +
    1.79 +syntax
    1.80 +  "_CLet" :: "[letbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10)
    1.81 +
    1.82 +translations
    1.83 +  "_CLet (_binds b bs) e" == "_CLet b (_CLet bs e)"
    1.84 +  "Let x = a in e" == "CLet$a$(LAM x. e)"
    1.85 +
    1.86  end
     2.1 --- a/src/HOLCF/Cprod.thy	Mon Oct 10 04:38:26 2005 +0200
     2.2 +++ b/src/HOLCF/Cprod.thy	Mon Oct 10 05:30:02 2005 +0200
     2.3 @@ -195,49 +195,19 @@
     2.4    "<x, y, z>" == "<x, <y, z>>"
     2.5    "<x, y>"    == "cpair$x$y"
     2.6  
     2.7 +syntax
     2.8 +  "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn"  ("<_,/ _>")
     2.9 +
    2.10 +translations
    2.11 +  "LAM <x,y,zs>. t"       == "csplit$(LAM x <y,zs>. t)"
    2.12 +  "LAM <x,y>. t"          == "csplit$(LAM x y. t)"
    2.13 +
    2.14  defs
    2.15    cpair_def:  "cpair  \<equiv> (\<Lambda> x y. (x, y))"
    2.16    cfst_def:   "cfst   \<equiv> (\<Lambda> p. fst p)"
    2.17    csnd_def:   "csnd   \<equiv> (\<Lambda> p. snd p)"      
    2.18    csplit_def: "csplit \<equiv> (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
    2.19  
    2.20 -subsection {* Syntax *}
    2.21 -
    2.22 -text {* syntax for @{text "LAM <x,y,z>.e"} *}
    2.23 -
    2.24 -syntax
    2.25 -  "_LAM" :: "[patterns, 'a \<Rightarrow> 'b] \<Rightarrow> ('a \<rightarrow> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
    2.26 -
    2.27 -translations
    2.28 -  "LAM <x,y,zs>. b"       == "csplit$(LAM x. LAM <y,zs>. b)"
    2.29 -  "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
    2.30 -  "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
    2.31 -
    2.32 -syntax (xsymbols)
    2.33 -  "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
    2.34 -
    2.35 -text {* syntax for Let *}
    2.36 -
    2.37 -constdefs
    2.38 -  CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b"
    2.39 -  "CLet \<equiv> \<Lambda> s f. f\<cdot>s"
    2.40 -
    2.41 -nonterminals
    2.42 -  Cletbinds  Cletbind
    2.43 -
    2.44 -syntax
    2.45 -  "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
    2.46 -  "_Cbindp" :: "[patterns, 'a] => Cletbind"          ("(2<_> =/ _)" 10)
    2.47 -  ""        :: "Cletbind => Cletbinds"               ("_")
    2.48 -  "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
    2.49 -  "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)
    2.50 -
    2.51 -translations
    2.52 -  "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
    2.53 -  "Let x = a in LAM ys. e"  == "CLet$a$(LAM x ys. e)"
    2.54 -  "Let x = a in e"          == "CLet$a$(LAM x. e)"
    2.55 -  "Let <xs> = a in e"       == "CLet$a$(LAM <xs>. e)"
    2.56 -
    2.57  subsection {* Convert all lemmas to the continuous versions *}
    2.58  
    2.59  lemma cpair_eq_pair: "<x, y> = (x, y)"
     3.1 --- a/src/HOLCF/Fix.thy	Mon Oct 10 04:38:26 2005 +0200
     3.2 +++ b/src/HOLCF/Fix.thy	Mon Oct 10 05:30:02 2005 +0200
     3.3 @@ -35,17 +35,13 @@
     3.4  subsection {* Binder syntax for @{term fix} *}
     3.5  
     3.6  syntax
     3.7 -  "@FIX" :: "('a => 'a) => 'a"  (binder "FIX " 10)
     3.8 -  "@FIXP" :: "[patterns, 'a] => 'a"  ("(3FIX <_>./ _)" [0, 10] 10)
     3.9 +  "_FIX" :: "[pttrn, 'a] => 'a" ("(3FIX _./ _)" [0, 10] 10)
    3.10  
    3.11  syntax (xsymbols)
    3.12 -  "FIX " :: "[idt, 'a] => 'a"  ("(3\<mu>_./ _)" [0, 10] 10)
    3.13 -  "@FIXP" :: "[patterns, 'a] => 'a"  ("(3\<mu>()<_>./ _)" [0, 10] 10)
    3.14 +  "_FIX" :: "[pttrn, 'a] => 'a" ("(3\<mu>_./ _)" [0, 10] 10)
    3.15  
    3.16  translations
    3.17 -  "FIX x. LAM y. t" == "fix\<cdot>(LAM x y. t)"
    3.18 -  "FIX x. t" == "fix\<cdot>(LAM x. t)"
    3.19 -  "FIX <xs>. t" == "fix\<cdot>(LAM <xs>. t)"
    3.20 +  "FIX x. t" == "fix$(LAM x. t)"
    3.21  
    3.22  subsection {* Properties of @{term iterate} and @{term fix} *}
    3.23  
     4.1 --- a/src/HOLCF/domain/syntax.ML	Mon Oct 10 04:38:26 2005 +0200
     4.2 +++ b/src/HOLCF/domain/syntax.ML	Mon Oct 10 05:30:02 2005 +0200
     4.3 @@ -75,9 +75,8 @@
     4.4  	fun case1 n (con,mx,args) = mk_appl (Constant "_case1")
     4.5  		 [Library.foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)),
     4.6  		  expvar n];
     4.7 -	fun arg1 n (con,_,args) = if args = [] then expvar n 
     4.8 -				  else mk_appl (Constant "LAM ") 
     4.9 -		 [foldr1 (app "_idts") (mapn (argvar n) 1 args) , expvar n];
    4.10 +	fun cabs (x,t) = mk_appl (Constant "_cabs") [x,t];
    4.11 +	fun arg1 n (con,_,args) = foldr cabs (expvar n) (mapn (argvar n) 1 args);
    4.12    in
    4.13      ParsePrintRule
    4.14        (mk_appl (Constant "_case_syntax") [Variable "x", foldr1