--- a/NEWS Sun May 29 14:10:48 2016 +0200
+++ b/NEWS Sun May 29 14:43:17 2016 +0200
@@ -100,6 +100,9 @@
*** HOL ***
+* Command 'code_reflect' accepts empty constructor lists for datatypes,
+which renders those abstract effectively.
+
* Probability/Random_Permutations.thy contains some theory about
choosing a permutation of a set uniformly at random and folding over a
list in random order.
--- a/src/HOL/Code_Numeral.thy Sun May 29 14:10:48 2016 +0200
+++ b/src/HOL/Code_Numeral.thy Sun May 29 14:43:17 2016 +0200
@@ -893,9 +893,9 @@
"Nat (integer_of_natural n) = n"
by transfer simp
-lemma [code abstract]:
- "integer_of_natural (natural_of_nat n) = of_nat n"
- by simp
+lemma [code]:
+ "natural_of_nat n = natural_of_integer (integer_of_nat n)"
+ by transfer simp
lemma [code abstract]:
"integer_of_natural (natural_of_integer k) = max 0 k"
@@ -969,7 +969,11 @@
lifting_forget natural.lifting
code_reflect Code_Numeral
- datatypes natural = _
- functions integer_of_natural natural_of_integer
+ datatypes natural
+ functions "Code_Numeral.Suc" "0 :: natural" "1 :: natural"
+ "plus :: natural \<Rightarrow> _" "minus :: natural \<Rightarrow> _"
+ "times :: natural \<Rightarrow> _" "divide :: natural \<Rightarrow> _"
+ "Divides.mod :: natural \<Rightarrow> _"
+ integer_of_natural natural_of_integer
end
--- a/src/Tools/Code/code_ml.ML Sun May 29 14:10:48 2016 +0200
+++ b/src/Tools/Code/code_ml.ML Sun May 29 14:43:17 2016 +0200
@@ -772,13 +772,18 @@
fun modify_funs stmts = single (SOME
(Code_Namespace.Opaque, ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
fun modify_datatypes stmts =
- map_filter
- (fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt)) | _ => NONE) stmts
- |> split_list
- |> apfst Code_Namespace.join_exports
- |> apsnd ML_Datas
- |> SOME
- |> single;
+ let
+ val datas = map_filter
+ (fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt)) | _ => NONE) stmts
+ in
+ if null datas then [] (*for abstract types wrt. code_reflect*)
+ else datas
+ |> split_list
+ |> apfst Code_Namespace.join_exports
+ |> apsnd ML_Datas
+ |> SOME
+ |> single
+ end;
fun modify_class stmts =
the_single (map_filter
(fn (Type_Class class, (export, Code_Thingol.Class stmt)) => SOME (export, (class, stmt)) | _ => NONE) stmts)
--- a/src/Tools/Code/code_runtime.ML Sun May 29 14:10:48 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML Sun May 29 14:43:17 2016 +0200
@@ -375,20 +375,21 @@
fun check_datatype thy tyco some_consts =
let
- val constrs = (map fst o snd o fst o Code.get_type thy) tyco;
- val _ = case some_consts
- of SOME consts =>
+ val declared_constrs = (map fst o snd o fst o Code.get_type thy) tyco;
+ val constrs = case some_consts
+ of SOME [] => []
+ | SOME consts =>
let
- val missing_constrs = subtract (op =) consts constrs;
+ val missing_constrs = subtract (op =) consts declared_constrs;
val _ = if null missing_constrs then []
else error ("Missing constructor(s) " ^ commas_quote missing_constrs
^ " for datatype " ^ quote tyco);
- val false_constrs = subtract (op =) constrs consts;
+ val false_constrs = subtract (op =) declared_constrs consts;
val _ = if null false_constrs then []
else error ("Non-constructor(s) " ^ commas_quote false_constrs
^ " for datatype " ^ quote tyco)
- in () end
- | NONE => ();
+ in consts end
+ | NONE => declared_constrs;
in (tyco, constrs) end;
fun add_eval_tyco (tyco, tyco') thy =
@@ -465,16 +466,16 @@
local
val parse_datatype =
- Parse.name --| @{keyword "="} --
+ Parse.name -- Scan.optional (@{keyword "="} |--
(((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
- || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME));
+ || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME))) (SOME []);
in
val _ =
Outer_Syntax.command @{command_keyword code_reflect}
"enrich runtime environment with generated code"
- (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!! (parse_datatype
+ (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!! (parse_datatype
::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
-- Scan.optional (@{keyword "functions"} |-- Parse.!!! (Scan.repeat1 Parse.name)) []
-- Scan.option (@{keyword "file"} |-- Parse.!!! Parse.name)