# HG changeset patch
# User haftmann
# Date 1464525797 -7200
# Node ID 57c0d60e491c219ad366891f6e72aca6b6936341
# Parent  3413b1cf30cd651caafc104381712da27f75653a
do not export abstract constructors in code_reflect

diff -r 3413b1cf30cd -r 57c0d60e491c NEWS
--- 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.
diff -r 3413b1cf30cd -r 57c0d60e491c src/HOL/Code_Numeral.thy
--- 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
diff -r 3413b1cf30cd -r 57c0d60e491c src/Tools/Code/code_ml.ML
--- 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)
diff -r 3413b1cf30cd -r 57c0d60e491c src/Tools/Code/code_runtime.ML
--- 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)