# HG changeset patch # User haftmann # Date 1224863320 -7200 # Node ID 150a8a1eae1a7657f440535f786d5de9f1df3424 # Parent 5d63184c10c7c259c277dfe620719830b6293976 simplified syntax for class parameters diff -r 5d63184c10c7 -r 150a8a1eae1a doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Oct 24 17:48:39 2008 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Oct 24 17:48:40 2008 +0200 @@ -1050,9 +1050,7 @@ ; 'code\_class' (class + 'and') \\ - ( ( '(' target \\ - ( ( string ('where' \\ - ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + ) + ( ( '(' target \\ ( string ? + 'and' ) ')' ) + ) ; 'code\_instance' (( typeconstructor '::' class ) + 'and') \\ @@ -1135,10 +1133,9 @@ serialization deletes an existing serialization. \item [@{command (HOL) "code_class"}] associates a list of classes - with target-specific class names; in addition, constants associated - with this class may be given target-specific names used for instance - declarations; omitting a serialization deletes an existing - serialization. This applies only to \emph{Haskell}. + with target-specific class names; omitting a + serialization deletes an existing serialization. + This applies only to \emph{Haskell}. \item [@{command (HOL) "code_instance"}] declares a list of type constructor / class instance relations as ``already present'' for a diff -r 5d63184c10c7 -r 150a8a1eae1a doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 24 17:48:39 2008 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 24 17:48:40 2008 +0200 @@ -1053,9 +1053,7 @@ ; 'code\_class' (class + 'and') \\ - ( ( '(' target \\ - ( ( string ('where' \\ - ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + ) + ( ( '(' target \\ ( string ? + 'and' ) ')' ) + ) ; 'code\_instance' (( typeconstructor '::' class ) + 'and') \\ @@ -1135,10 +1133,9 @@ serialization deletes an existing serialization. \item [\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes - with target-specific class names; in addition, constants associated - with this class may be given target-specific names used for instance - declarations; omitting a serialization deletes an existing - serialization. This applies only to \emph{Haskell}. + with target-specific class names; omitting a + serialization deletes an existing serialization. + This applies only to \emph{Haskell}. \item [\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type constructor / class instance relations as ``already present'' for a diff -r 5d63184c10c7 -r 150a8a1eae1a src/HOL/Code_Setup.thy --- a/src/HOL/Code_Setup.thy Fri Oct 24 17:48:39 2008 +0200 +++ b/src/HOL/Code_Setup.thy Fri Oct 24 17:48:40 2008 +0200 @@ -123,7 +123,7 @@ text {* using built-in Haskell equality *} code_class eq - (Haskell "Eq" where "eq_class.eq" \ "(==)") + (Haskell "Eq") code_const "eq_class.eq" (Haskell infixl 4 "==") diff -r 5d63184c10c7 -r 150a8a1eae1a src/Tools/code/code_haskell.ML --- a/src/Tools/code/code_haskell.ML Fri Oct 24 17:48:39 2008 +0200 +++ b/src/Tools/code/code_haskell.ML Fri Oct 24 17:48:40 2008 +0200 @@ -38,12 +38,7 @@ val deresolve_base = NameSpace.base o deresolve; fun class_name class = case syntax_class class of NONE => deresolve class - | SOME (class, _) => class; - fun classparam_name class classparam = case syntax_class class - of NONE => deresolve_base classparam - | SOME (_, classparam_syntax) => case classparam_syntax classparam - of NONE => (snd o Code_Name.dest_name) classparam - | SOME classparam => classparam; + | SOME class => class; fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs of [] => [] | classbinds => Pretty.enum "," "(" ")" ( @@ -231,7 +226,7 @@ val tyvars = Code_Name.intro_vars [v] init_syms; fun pr_classparam (classparam, ty) = semicolon [ - (str o classparam_name name) classparam, + (str o deresolve_base) classparam, str "::", pr_typ tyvars NOBR ty ] @@ -248,13 +243,34 @@ end | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) = let + val split_abs_pure = (fn (v, _) `|-> t => SOME (v, t) | _ => NONE); + val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure; val tyvars = Code_Name.intro_vars (map fst vs) init_syms; - fun pr_instdef ((classparam, c_inst), (thm, _)) = - semicolon [ - (str o classparam_name class) classparam, - str "=", - pr_app tyvars thm false init_syms NOBR (c_inst, []) - ]; + fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam + of NONE => semicolon [ + (str o deresolve_base) classparam, + str "=", + pr_app tyvars thm false init_syms NOBR (c_inst, []) + ] + | SOME (k, pr) => + let + val (c_inst_name, (_, tys)) = c_inst; + val const = if (is_some o syntax_const) c_inst_name + then NONE else (SOME o NameSpace.base o deresolve) c_inst_name; + val proto_rhs = Code_Thingol.eta_expand k (c_inst, []); + val (vs, rhs) = unfold_abs_pure proto_rhs; + val vars = init_syms + |> Code_Name.intro_vars (the_list const) + |> Code_Name.intro_vars vs; + val lhs = IConst (classparam, ([], tys)) `$$ map IVar vs; + (*dictionaries are not relevant at this late stage*) + in + semicolon [ + pr_term tyvars thm false vars NOBR lhs, + str "=", + pr_term tyvars thm false vars NOBR rhs + ] + end; in Pretty.block_enclose ( Pretty.block [