merged
authorhaftmann
Thu Aug 26 13:56:35 2010 +0200 (2010-08-26 ago)
changeset 387816b356e3687d2
parent 38776 95df565aceb7
parent 38780 910cedb62327
child 38782 3865cbe5d2be
merged
src/HOL/Library/Code_Natural.thy
     1.1 --- a/src/HOL/Library/Code_Natural.thy	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Library/Code_Natural.thy	Thu Aug 26 13:56:35 2010 +0200
     1.3 @@ -9,9 +9,7 @@
     1.4  section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
     1.5  
     1.6  code_include Haskell "Natural"
     1.7 -{*import Data.Array.ST;
     1.8 -
     1.9 -newtype Natural = Natural Integer deriving (Eq, Show, Read);
    1.10 +{*newtype Natural = Natural Integer deriving (Eq, Show, Read);
    1.11  
    1.12  instance Num Natural where {
    1.13    fromInteger k = Natural (if k >= 0 then k else 0);
     2.1 --- a/src/Tools/Code/code_haskell.ML	Thu Aug 26 13:44:50 2010 +0200
     2.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Aug 26 13:56:35 2010 +0200
     2.3 @@ -261,9 +261,8 @@
     2.4            end;
     2.5    in print_stmt end;
     2.6  
     2.7 -fun haskell_program_of_program labelled_name module_name module_prefix reserved raw_module_alias program =
     2.8 +fun haskell_program_of_program labelled_name module_prefix reserved module_alias program =
     2.9    let
    2.10 -    val module_alias = if is_some module_name then K module_name else raw_module_alias;
    2.11      val reserved = Name.make_context reserved;
    2.12      val mk_name_module = mk_name_module reserved module_prefix module_alias program;
    2.13      fun add_stmt (name, (stmt, deps)) =
    2.14 @@ -314,15 +313,14 @@
    2.15        handle Option => error ("Unknown statement name: " ^ labelled_name name);
    2.16    in (deresolver, hs_program) end;
    2.17  
    2.18 -fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
    2.19 -    raw_reserved includes raw_module_alias
    2.20 -    syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
    2.21 +fun serialize_haskell module_prefix module_name string_classes labelled_name
    2.22 +    raw_reserved includes module_alias
    2.23 +    syntax_class syntax_tyco syntax_const (code_of_pretty, code_writeln) program
    2.24 +    (stmt_names, presentation_stmt_names) destination =
    2.25    let
    2.26 -    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
    2.27 -    val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
    2.28      val reserved = fold (insert (op =) o fst) includes raw_reserved;
    2.29      val (deresolver, hs_program) = haskell_program_of_program labelled_name
    2.30 -      module_name module_prefix reserved raw_module_alias program;
    2.31 +      module_prefix reserved module_alias program;
    2.32      val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
    2.33      fun deriving_show tyco =
    2.34        let
     3.1 --- a/src/Tools/Code/code_ml.ML	Thu Aug 26 13:44:50 2010 +0200
     3.2 +++ b/src/Tools/Code/code_ml.ML	Thu Aug 26 13:56:35 2010 +0200
     3.3 @@ -489,7 +489,7 @@
     3.4                    |> intro_vars ((fold o Code_Thingol.fold_varnames)
     3.5                        (insert (op =)) ts []);
     3.6                in concat [
     3.7 -                (Pretty.block o Pretty.commas)
     3.8 +                (Pretty.block o commas)
     3.9                    (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
    3.10                  str "->",
    3.11                  print_term is_pseudo_fun some_thm vars NOBR t
    3.12 @@ -535,7 +535,7 @@
    3.13                        :: Pretty.brk 1
    3.14                        :: str "match"
    3.15                        :: Pretty.brk 1
    3.16 -                      :: (Pretty.block o Pretty.commas) dummy_parms
    3.17 +                      :: (Pretty.block o commas) dummy_parms
    3.18                        :: Pretty.brk 1
    3.19                        :: str "with"
    3.20                        :: Pretty.brk 1
    3.21 @@ -722,9 +722,8 @@
    3.22  
    3.23  in
    3.24  
    3.25 -fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
    3.26 +fun ml_node_of_program labelled_name module_name reserved module_alias program =
    3.27    let
    3.28 -    val module_alias = if is_some module_name then K module_name else raw_module_alias;
    3.29      val reserved = Name.make_context reserved;
    3.30      val empty_module = ((reserved, reserved), Graph.empty);
    3.31      fun map_node [] f = f
    3.32 @@ -813,7 +812,7 @@
    3.33          ) stmts
    3.34        #>> (split_list #> apsnd (map_filter I
    3.35          #> (fn [] => error ("Datatype block without data statement: "
    3.36 -                  ^ (commas o map (labelled_name o fst)) stmts)
    3.37 +                  ^ (Library.commas o map (labelled_name o fst)) stmts)
    3.38               | stmts => ML_Datas stmts)));
    3.39      fun add_class stmts =
    3.40        fold_map
    3.41 @@ -828,7 +827,7 @@
    3.42          ) stmts
    3.43        #>> (split_list #> apsnd (map_filter I
    3.44          #> (fn [] => error ("Class block without class statement: "
    3.45 -                  ^ (commas o map (labelled_name o fst)) stmts)
    3.46 +                  ^ (Library.commas o map (labelled_name o fst)) stmts)
    3.47               | [stmt] => ML_Class stmt)));
    3.48      fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
    3.49            add_fun stmt
    3.50 @@ -849,7 +848,7 @@
    3.51        | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
    3.52            add_funs stmts
    3.53        | add_stmts stmts = error ("Illegal mutual dependencies: " ^
    3.54 -          (commas o map (labelled_name o fst)) stmts);
    3.55 +          (Library.commas o map (labelled_name o fst)) stmts);
    3.56      fun add_stmts' stmts nsp_nodes =
    3.57        let
    3.58          val names as (name :: names') = map fst stmts;
    3.59 @@ -858,9 +857,9 @@
    3.60          val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
    3.61            handle Empty =>
    3.62              error ("Different namespace prefixes for mutual dependencies:\n"
    3.63 -              ^ commas (map labelled_name names)
    3.64 +              ^ Library.commas (map labelled_name names)
    3.65                ^ "\n"
    3.66 -              ^ commas module_names);
    3.67 +              ^ Library.commas module_names);
    3.68          val module_name_path = Long_Name.explode module_name;
    3.69          fun add_dep name name' =
    3.70            let
    3.71 @@ -907,15 +906,14 @@
    3.72          error ("Unknown statement name: " ^ labelled_name name);
    3.73    in (deresolver, nodes) end;
    3.74  
    3.75 -fun serialize_ml target print_module print_stmt raw_module_name with_signatures labelled_name
    3.76 -  reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
    3.77 +fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
    3.78 +  reserved includes module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program
    3.79 +  (stmt_names, presentation_stmt_names) =
    3.80    let
    3.81      val is_cons = Code_Thingol.is_cons program;
    3.82 -    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
    3.83      val is_presentation = not (null presentation_stmt_names);
    3.84 -    val module_name = if is_presentation then SOME "Code" else raw_module_name;
    3.85      val (deresolver, nodes) = ml_node_of_program labelled_name module_name
    3.86 -      reserved raw_module_alias program;
    3.87 +      reserved module_alias program;
    3.88      val reserved = make_vars reserved;
    3.89      fun print_node prefix (Dummy _) =
    3.90            NONE
    3.91 @@ -939,7 +937,7 @@
    3.92    in
    3.93      Code_Target.mk_serialization target
    3.94        (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
    3.95 -      (rpair stmt_names' o code_of_pretty) p destination
    3.96 +      (rpair stmt_names' o code_of_pretty) p
    3.97    end;
    3.98  
    3.99  end; (*local*)
     4.1 --- a/src/Tools/Code/code_printer.ML	Thu Aug 26 13:44:50 2010 +0200
     4.2 +++ b/src/Tools/Code/code_printer.ML	Thu Aug 26 13:56:35 2010 +0200
     4.3 @@ -19,6 +19,7 @@
     4.4    val concat: Pretty.T list -> Pretty.T
     4.5    val brackets: Pretty.T list -> Pretty.T
     4.6    val enclose: string -> string -> Pretty.T list -> Pretty.T
     4.7 +  val commas: Pretty.T list -> Pretty.T list
     4.8    val enum: string -> string -> string -> Pretty.T list -> Pretty.T
     4.9    val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
    4.10    val semicolon: Pretty.T list -> Pretty.T
    4.11 @@ -112,6 +113,7 @@
    4.12  fun xs @| y = xs @ [y];
    4.13  val str = Print_Mode.setmp [] Pretty.str;
    4.14  val concat = Pretty.block o Pretty.breaks;
    4.15 +val commas = Print_Mode.setmp [] Pretty.commas;
    4.16  fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
    4.17  val brackets = enclose "(" ")" o Pretty.breaks;
    4.18  fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
     5.1 --- a/src/Tools/Code/code_scala.ML	Thu Aug 26 13:44:50 2010 +0200
     5.2 +++ b/src/Tools/Code/code_scala.ML	Thu Aug 26 13:56:35 2010 +0200
     5.3 @@ -25,7 +25,7 @@
     5.4  (** Scala serializer **)
     5.5  
     5.6  fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
     5.7 -    args_num is_singleton_constr deresolve =
     5.8 +    args_num is_singleton_constr (deresolve, deresolve_full) =
     5.9    let
    5.10      val deresolve_base = Long_Name.base_name o deresolve;
    5.11      fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
    5.12 @@ -195,7 +195,7 @@
    5.13                (map print_clause eqs)
    5.14            end;
    5.15      val print_method = str o Library.enclose "`" "`" o space_implode "+"
    5.16 -      o fst o split_last o Long_Name.explode;
    5.17 +      o Long_Name.explode o deresolve_full;
    5.18      fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
    5.19            print_def name (vs, ty) (filter (snd o snd) raw_eqs)
    5.20        | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
    5.21 @@ -293,11 +293,10 @@
    5.22  
    5.23  in
    5.24  
    5.25 -fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
    5.26 +fun scala_program_of_program labelled_name reserved module_alias program =
    5.27    let
    5.28  
    5.29      (* building module name hierarchy *)
    5.30 -    val module_alias = if is_some module_name then K module_name else raw_module_alias;
    5.31      fun alias_fragments name = case module_alias name
    5.32       of SOME name' => Long_Name.explode name'
    5.33        | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
    5.34 @@ -403,20 +402,15 @@
    5.35  
    5.36    in (deresolve, sca_program) end;
    5.37  
    5.38 -fun serialize_scala raw_module_name labelled_name
    5.39 -    raw_reserved includes raw_module_alias
    5.40 +fun serialize_scala labelled_name raw_reserved includes module_alias
    5.41      _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
    5.42 -    program stmt_names destination =
    5.43 +    program (stmt_names, presentation_stmt_names) destination =
    5.44    let
    5.45  
    5.46 -    (* generic nonsense *)
    5.47 -    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
    5.48 -    val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
    5.49 -
    5.50      (* preprocess program *)
    5.51      val reserved = fold (insert (op =) o fst) includes raw_reserved;
    5.52      val (deresolve, sca_program) = scala_program_of_program labelled_name
    5.53 -      module_name (Name.make_context reserved) raw_module_alias program;
    5.54 +      (Name.make_context reserved) module_alias program;
    5.55  
    5.56      (* print statements *)
    5.57      fun lookup_constr tyco constr = case Graph.get_node program tyco
    5.58 @@ -436,12 +430,13 @@
    5.59       of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
    5.60        | _ => false;
    5.61      val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
    5.62 -      (make_vars reserved) args_num is_singleton_constr deresolve;
    5.63 +      (make_vars reserved) args_num is_singleton_constr
    5.64 +      (deresolve, Long_Name.implode o fst o split_last o Long_Name.explode (*FIXME full*));
    5.65  
    5.66      (* print nodes *)
    5.67      fun print_implicits [] = NONE
    5.68        | print_implicits implicits = (SOME o Pretty.block)
    5.69 -          (str "import /*implicits*/" :: Pretty.brk 1 :: Pretty.commas (map (str o deresolve) implicits));
    5.70 +          (str "import /*implicits*/" :: Pretty.brk 1 :: commas (map (str o deresolve) implicits));
    5.71      fun print_module base implicits p = Pretty.chunks2
    5.72        ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
    5.73          @ [p, str ("} /* object " ^ base ^ " */")]);
    5.74 @@ -498,9 +493,9 @@
    5.75  
    5.76  (** Isar setup **)
    5.77  
    5.78 -fun isar_serializer module_name =
    5.79 +fun isar_serializer _ =
    5.80    Code_Target.parse_args (Scan.succeed ())
    5.81 -  #> (fn () => serialize_scala module_name);
    5.82 +  #> (fn () => serialize_scala);
    5.83  
    5.84  val setup =
    5.85    Code_Target.add_target
     6.1 --- a/src/Tools/Code/code_target.ML	Thu Aug 26 13:44:50 2010 +0200
     6.2 +++ b/src/Tools/Code/code_target.ML	Thu Aug 26 13:56:35 2010 +0200
     6.3 @@ -111,7 +111,7 @@
     6.4    -> (string -> Code_Printer.activated_const_syntax option)
     6.5    -> ((Pretty.T -> string) * (Pretty.T -> unit))
     6.6    -> Code_Thingol.program
     6.7 -  -> string list                        (*selected statements*)
     6.8 +  -> (string list * string list)        (*selected statements*)
     6.9    -> serialization;
    6.10  
    6.11  datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
    6.12 @@ -254,7 +254,7 @@
    6.13    |>> map_filter I;
    6.14  
    6.15  fun invoke_serializer thy abortable serializer literals reserved abs_includes 
    6.16 -    module_alias class instance tyco const module width args naming program2 names1 =
    6.17 +    module_alias class instance tyco const module_name width args naming program2 (names1, presentation_names) =
    6.18    let
    6.19      val (names_class, class') =
    6.20        activate_syntax (Code_Thingol.lookup_class naming) class;
    6.21 @@ -275,14 +275,14 @@
    6.22      val _ = if null empty_funs then () else error ("No code equations for "
    6.23        ^ commas (map (Sign.extern_const thy) empty_funs));
    6.24    in
    6.25 -    serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
    6.26 -      (Symtab.lookup module_alias) (Symtab.lookup class')
    6.27 -      (Symtab.lookup tyco') (Symtab.lookup const')
    6.28 +    serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes
    6.29 +      (if is_some module_name then K module_name else Symtab.lookup module_alias)
    6.30 +      (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
    6.31        (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
    6.32 -      program4 names1
    6.33 +      program4 (names1, presentation_names)
    6.34    end;
    6.35  
    6.36 -fun mount_serializer thy alt_serializer target some_width module args naming program names =
    6.37 +fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
    6.38    let
    6.39      val ((targets, abortable), default_width) = Targets.get thy;
    6.40      fun collapse_hierarchy target =
    6.41 @@ -299,6 +299,9 @@
    6.42      val (modify, data) = collapse_hierarchy target;
    6.43      val serializer = the_default (case the_description data
    6.44       of Fundamental seri => #serializer seri) alt_serializer;
    6.45 +    val presentation_names = stmt_names_of_destination destination;
    6.46 +    val module_name = if null presentation_names
    6.47 +      then raw_module_name else SOME "Code";
    6.48      val reserved = the_reserved data;
    6.49      fun select_include names_all (name, (content, cs)) =
    6.50        if null cs then SOME (name, content)
    6.51 @@ -308,13 +311,14 @@
    6.52        then SOME (name, content) else NONE;
    6.53      fun includes names_all = map_filter (select_include names_all)
    6.54        ((Symtab.dest o the_includes) data);
    6.55 -    val module_alias = the_module_alias data;
    6.56 +    val module_alias = the_module_alias data 
    6.57      val { class, instance, tyco, const } = the_name_syntax data;
    6.58      val literals = the_literals thy target;
    6.59      val width = the_default default_width some_width;
    6.60    in
    6.61      invoke_serializer thy abortable serializer literals reserved
    6.62 -      includes module_alias class instance tyco const module width args naming (modify program) names
    6.63 +      includes module_alias class instance tyco const module_name width args
    6.64 +        naming (modify program) (names, presentation_names) destination
    6.65    end;
    6.66  
    6.67  in