# HG changeset patch
# User haftmann
# Date 1464525798 -7200
# Node ID d191892b1c23dffd7eb70376dcc873a42c96c7cc
# Parent  57c0d60e491c219ad366891f6e72aca6b6936341
explicit check that abstract constructors cannot be part of official interface

diff -r 57c0d60e491c -r d191892b1c23 NEWS
--- a/NEWS	Sun May 29 14:43:17 2016 +0200
+++ b/NEWS	Sun May 29 14:43:18 2016 +0200
@@ -103,6 +103,10 @@
 * Command 'code_reflect' accepts empty constructor lists for datatypes,
 which renders those abstract effectively.
 
+* Command 'export_code' checks given constants for abstraction violations:
+a small guarantee that given constants specify a safe interface for the
+generated code.
+
 * 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 57c0d60e491c -r d191892b1c23 src/Doc/Codegen/Evaluation.thy
--- a/src/Doc/Codegen/Evaluation.thy	Sun May 29 14:43:17 2016 +0200
+++ b/src/Doc/Codegen/Evaluation.thy	Sun May 29 14:43:18 2016 +0200
@@ -344,7 +344,7 @@
 \<close>
 
 code_reflect %quote Rat
-  datatypes rat = Frct
+  datatypes rat
   functions Fract
     "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
     "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
diff -r 57c0d60e491c -r d191892b1c23 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun May 29 14:43:17 2016 +0200
+++ b/src/Tools/Code/code_thingol.ML	Sun May 29 14:43:18 2016 +0200
@@ -786,11 +786,23 @@
 
 (* program generation *)
 
+fun check_abstract_constructors thy consts =
+  case filter (Code.is_abstr thy) consts of
+    [] => ()
+  | abstrs => error ("Cannot export abstract constructor(s): "
+      ^ commas (map (Code.string_of_const thy) abstrs));
+
 fun invoke_generation_for_consts ctxt { ignore_cache, permissive } { algebra, eqngr } consts =
-  Code_Preproc.timed "translating program" #ctxt
-  (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt
-    (fold_map (ensure_const ctxt algebra eqngr permissive)) consts)
-    { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts };
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val _ = if permissive then ()
+      else check_abstract_constructors thy consts;
+  in
+    Code_Preproc.timed "translating program" #ctxt
+    (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt
+      (fold_map (ensure_const ctxt algebra eqngr permissive)) consts)
+      { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts }
+  end;
 
 fun invoke_generation_for_consts' ctxt ignore_cache_and_permissive consts =
   invoke_generation_for_consts ctxt
@@ -914,7 +926,8 @@
     val thy = Proof_Context.theory_of ctxt;
     fun consts_of thy' =
       fold (fn (c, (_, NONE)) => cons c | _ => I)
-        (#constants (Consts.dest (Sign.consts_of thy'))) [];
+        (#constants (Consts.dest (Sign.consts_of thy'))) []
+      |> filter_out (Code.is_abstr thy);
     fun belongs_here thy' c = forall
       (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
     fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
@@ -934,8 +947,10 @@
   let
     val (consts, consts_permissive) =
       read_const_exprs_internal ctxt const_exprs;
-    val consts' = implemented_deps
-      (consts_program_permissive ctxt consts_permissive);
+    val consts' = 
+      consts_program_permissive ctxt consts_permissive
+      |> implemented_deps
+      |> filter_out (Code.is_abstr (Proof_Context.theory_of ctxt));
   in union (op =) consts' consts end;