simplified syntax for class parameters
authorhaftmann
Fri Oct 24 17:48:40 2008 +0200 (2008-10-24)
changeset 28687150a8a1eae1a
parent 28686 5d63184c10c7
child 28688 1a9fabb515cd
simplified syntax for class parameters
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
src/HOL/Code_Setup.thy
src/Tools/code/code_haskell.ML
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 24 17:48:39 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 24 17:48:40 2008 +0200
     1.3 @@ -1050,9 +1050,7 @@
     1.4      ;
     1.5  
     1.6      'code\_class' (class + 'and') \\
     1.7 -      ( ( '(' target \\
     1.8 -        ( ( string ('where' \\
     1.9 -          ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + )
    1.10 +      ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
    1.11      ;
    1.12  
    1.13      'code\_instance' (( typeconstructor '::' class ) + 'and') \\
    1.14 @@ -1135,10 +1133,9 @@
    1.15    serialization deletes an existing serialization.
    1.16  
    1.17    \item [@{command (HOL) "code_class"}] associates a list of classes
    1.18 -  with target-specific class names; in addition, constants associated
    1.19 -  with this class may be given target-specific names used for instance
    1.20 -  declarations; omitting a serialization deletes an existing
    1.21 -  serialization.  This applies only to \emph{Haskell}.
    1.22 +  with target-specific class names; omitting a
    1.23 +  serialization deletes an existing serialization.
    1.24 +  This applies only to \emph{Haskell}.
    1.25  
    1.26    \item [@{command (HOL) "code_instance"}] declares a list of type
    1.27    constructor / class instance relations as ``already present'' for a
     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 24 17:48:39 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 24 17:48:40 2008 +0200
     2.3 @@ -1053,9 +1053,7 @@
     2.4      ;
     2.5  
     2.6      'code\_class' (class + 'and') \\
     2.7 -      ( ( '(' target \\
     2.8 -        ( ( string ('where' \\
     2.9 -          ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + )
    2.10 +      ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
    2.11      ;
    2.12  
    2.13      'code\_instance' (( typeconstructor '::' class ) + 'and') \\
    2.14 @@ -1135,10 +1133,9 @@
    2.15    serialization deletes an existing serialization.
    2.16  
    2.17    \item [\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes
    2.18 -  with target-specific class names; in addition, constants associated
    2.19 -  with this class may be given target-specific names used for instance
    2.20 -  declarations; omitting a serialization deletes an existing
    2.21 -  serialization.  This applies only to \emph{Haskell}.
    2.22 +  with target-specific class names; omitting a
    2.23 +  serialization deletes an existing serialization.
    2.24 +  This applies only to \emph{Haskell}.
    2.25  
    2.26    \item [\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type
    2.27    constructor / class instance relations as ``already present'' for a
     3.1 --- a/src/HOL/Code_Setup.thy	Fri Oct 24 17:48:39 2008 +0200
     3.2 +++ b/src/HOL/Code_Setup.thy	Fri Oct 24 17:48:40 2008 +0200
     3.3 @@ -123,7 +123,7 @@
     3.4  text {* using built-in Haskell equality *}
     3.5  
     3.6  code_class eq
     3.7 -  (Haskell "Eq" where "eq_class.eq" \<equiv> "(==)")
     3.8 +  (Haskell "Eq")
     3.9  
    3.10  code_const "eq_class.eq"
    3.11    (Haskell infixl 4 "==")
     4.1 --- a/src/Tools/code/code_haskell.ML	Fri Oct 24 17:48:39 2008 +0200
     4.2 +++ b/src/Tools/code/code_haskell.ML	Fri Oct 24 17:48:40 2008 +0200
     4.3 @@ -38,12 +38,7 @@
     4.4      val deresolve_base = NameSpace.base o deresolve;
     4.5      fun class_name class = case syntax_class class
     4.6       of NONE => deresolve class
     4.7 -      | SOME (class, _) => class;
     4.8 -    fun classparam_name class classparam = case syntax_class class
     4.9 -     of NONE => deresolve_base classparam
    4.10 -      | SOME (_, classparam_syntax) => case classparam_syntax classparam
    4.11 -         of NONE => (snd o Code_Name.dest_name) classparam
    4.12 -          | SOME classparam => classparam;
    4.13 +      | SOME class => class;
    4.14      fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
    4.15       of [] => []
    4.16        | classbinds => Pretty.enum "," "(" ")" (
    4.17 @@ -231,7 +226,7 @@
    4.18              val tyvars = Code_Name.intro_vars [v] init_syms;
    4.19              fun pr_classparam (classparam, ty) =
    4.20                semicolon [
    4.21 -                (str o classparam_name name) classparam,
    4.22 +                (str o deresolve_base) classparam,
    4.23                  str "::",
    4.24                  pr_typ tyvars NOBR ty
    4.25                ]
    4.26 @@ -248,13 +243,34 @@
    4.27            end
    4.28        | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
    4.29            let
    4.30 +            val split_abs_pure = (fn (v, _) `|-> t => SOME (v, t) | _ => NONE);
    4.31 +            val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
    4.32              val tyvars = Code_Name.intro_vars (map fst vs) init_syms;
    4.33 -            fun pr_instdef ((classparam, c_inst), (thm, _)) =
    4.34 -              semicolon [
    4.35 -                (str o classparam_name class) classparam,
    4.36 -                str "=",
    4.37 -                pr_app tyvars thm false init_syms NOBR (c_inst, [])
    4.38 -              ];
    4.39 +            fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
    4.40 +             of NONE => semicolon [
    4.41 +                    (str o deresolve_base) classparam,
    4.42 +                    str "=",
    4.43 +                    pr_app tyvars thm false init_syms NOBR (c_inst, [])
    4.44 +                  ]
    4.45 +              | SOME (k, pr) =>
    4.46 +                  let
    4.47 +                    val (c_inst_name, (_, tys)) = c_inst;
    4.48 +                    val const = if (is_some o syntax_const) c_inst_name
    4.49 +                      then NONE else (SOME o NameSpace.base o deresolve) c_inst_name;
    4.50 +                    val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
    4.51 +                    val (vs, rhs) = unfold_abs_pure proto_rhs;
    4.52 +                    val vars = init_syms
    4.53 +                      |> Code_Name.intro_vars (the_list const)
    4.54 +                      |> Code_Name.intro_vars vs;
    4.55 +                    val lhs = IConst (classparam, ([], tys)) `$$ map IVar vs;
    4.56 +                      (*dictionaries are not relevant at this late stage*)
    4.57 +                  in
    4.58 +                    semicolon [
    4.59 +                      pr_term tyvars thm false vars NOBR lhs,
    4.60 +                      str "=",
    4.61 +                      pr_term tyvars thm false vars NOBR rhs
    4.62 +                    ]
    4.63 +                  end;
    4.64            in
    4.65              Pretty.block_enclose (
    4.66                Pretty.block [