# HG changeset patch # User haftmann # Date 1262702101 -3600 # Node ID 5b3958210c35d228fe7773db4e509cc8b4ed43ac # Parent 8e36b3ac6083ad8d891f4cfd3d92a6ac7ded6f44# Parent 95df5e6dd41c82383039a41b63d56f6e339309e9 merged diff -r 8e36b3ac6083 -r 5b3958210c35 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Tue Jan 05 13:34:53 2010 +0100 +++ b/src/Pure/Isar/code.ML Tue Jan 05 15:35:01 2010 +0100 @@ -317,9 +317,14 @@ let val (tycos, _) = (the_signatures o the_exec) thy; val decls = (#types o Type.rep_tsig o Sign.tsig_of) thy - |> apsnd (Symtab.fold (fn (tyco, n) => - Symtab.update (tyco, Type.LogicalType n)) tycos); - in Type.build_tsig ((Name_Space.empty "", Sorts.empty_algebra), [], decls) end; + |> snd + |> Symtab.fold (fn (tyco, n) => + Symtab.update (tyco, Type.LogicalType n)) tycos; + in + Type.empty_tsig + |> Symtab.fold (fn (tyco, Type.LogicalType n) => Type.add_type Name_Space.default_naming + (Binding.qualified_name tyco, n) | _ => I) decls + end; fun cert_signature thy = Logic.varifyT o Type.cert_typ (build_tsig thy) o Type.no_tvars; diff -r 8e36b3ac6083 -r 5b3958210c35 src/Pure/type.ML --- a/src/Pure/type.ML Tue Jan 05 13:34:53 2010 +0100 +++ b/src/Pure/type.ML Tue Jan 05 15:35:01 2010 +0100 @@ -19,7 +19,6 @@ types: decl Name_Space.table, log_types: string list} val empty_tsig: tsig - val build_tsig: (Name_Space.T * Sorts.algebra) * sort * decl Name_Space.table -> tsig val defaultS: tsig -> sort val logical_types: tsig -> string list val eq_sort: tsig -> sort * sort -> bool diff -r 8e36b3ac6083 -r 5b3958210c35 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Tue Jan 05 13:34:53 2010 +0100 +++ b/src/Tools/Code/code_haskell.ML Tue Jan 05 15:35:01 2010 +0100 @@ -116,16 +116,10 @@ end | print_case tyvars thm vars fxy ((_, []), _) = (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]; - fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) = + fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = let val tyvars = intro_vars (map fst vs) reserved; - val n = (length o fst o Code_Thingol.unfold_fun) ty; - in - Pretty.chunks [ - semicolon [ - (str o suffix " ::" o deresolve_base) name, - print_typscheme tyvars (vs, ty) - ], + fun print_err n = semicolon ( (str o deresolve_base) name :: map str (replicate n "_") @@ -133,13 +127,7 @@ :: str "error" @@ (str o ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name - ) - ] - end - | print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = - let - val eqs = filter (snd o snd) raw_eqs; - val tyvars = intro_vars (map fst vs) reserved; + ); fun print_eqn ((ts, t), (thm, _)) = let val consts = fold Code_Thingol.add_constnames (t :: ts) []; @@ -162,7 +150,9 @@ (str o suffix " ::" o deresolve_base) name, print_typscheme tyvars (vs, ty) ] - :: map print_eqn eqs + :: (case filter (snd o snd) raw_eqs + of [] => [print_err ((length o fst o Code_Thingol.unfold_fun) ty)] + | eqs => map print_eqn eqs) ) end | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) = diff -r 8e36b3ac6083 -r 5b3958210c35 src/Tools/Code/lib/Tools/codegen --- a/src/Tools/Code/lib/Tools/codegen Tue Jan 05 13:34:53 2010 +0100 +++ b/src/Tools/Code/lib/Tools/codegen Tue Jan 05 15:35:01 2010 +0100 @@ -62,4 +62,4 @@ FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD" -"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1 +"$ISABELLE_PROCESS" -q -e "$FULL_CMD" "$IMAGE" || exit 1