do not export abstract constructors in code_reflect
authorhaftmann
Sun May 29 14:43:17 2016 +0200 (2016-05-29)
changeset 6317457c0d60e491c
parent 63173 3413b1cf30cd
child 63175 d191892b1c23
do not export abstract constructors in code_reflect
NEWS
src/HOL/Code_Numeral.thy
src/Tools/Code/code_ml.ML
src/Tools/Code/code_runtime.ML
     1.1 --- a/NEWS	Sun May 29 14:10:48 2016 +0200
     1.2 +++ b/NEWS	Sun May 29 14:43:17 2016 +0200
     1.3 @@ -100,6 +100,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Command 'code_reflect' accepts empty constructor lists for datatypes,
     1.8 +which renders those abstract effectively.
     1.9 +
    1.10  * Probability/Random_Permutations.thy contains some theory about 
    1.11  choosing a permutation of a set uniformly at random and folding over a 
    1.12  list in random order.
     2.1 --- a/src/HOL/Code_Numeral.thy	Sun May 29 14:10:48 2016 +0200
     2.2 +++ b/src/HOL/Code_Numeral.thy	Sun May 29 14:43:17 2016 +0200
     2.3 @@ -893,9 +893,9 @@
     2.4    "Nat (integer_of_natural n) = n"
     2.5    by transfer simp
     2.6  
     2.7 -lemma [code abstract]:
     2.8 -  "integer_of_natural (natural_of_nat n) = of_nat n"
     2.9 -  by simp
    2.10 +lemma [code]:
    2.11 +  "natural_of_nat n = natural_of_integer (integer_of_nat n)"
    2.12 +  by transfer simp
    2.13  
    2.14  lemma [code abstract]:
    2.15    "integer_of_natural (natural_of_integer k) = max 0 k"
    2.16 @@ -969,7 +969,11 @@
    2.17  lifting_forget natural.lifting
    2.18  
    2.19  code_reflect Code_Numeral
    2.20 -  datatypes natural = _
    2.21 -  functions integer_of_natural natural_of_integer
    2.22 +  datatypes natural
    2.23 +  functions "Code_Numeral.Suc" "0 :: natural" "1 :: natural"
    2.24 +    "plus :: natural \<Rightarrow> _" "minus :: natural \<Rightarrow> _"
    2.25 +    "times :: natural \<Rightarrow> _" "divide :: natural \<Rightarrow> _"
    2.26 +    "Divides.mod :: natural \<Rightarrow> _"
    2.27 +    integer_of_natural natural_of_integer
    2.28  
    2.29  end
     3.1 --- a/src/Tools/Code/code_ml.ML	Sun May 29 14:10:48 2016 +0200
     3.2 +++ b/src/Tools/Code/code_ml.ML	Sun May 29 14:43:17 2016 +0200
     3.3 @@ -772,13 +772,18 @@
     3.4      fun modify_funs stmts = single (SOME
     3.5        (Code_Namespace.Opaque, ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
     3.6      fun modify_datatypes stmts =
     3.7 -      map_filter
     3.8 -        (fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt)) | _ => NONE) stmts
     3.9 -      |> split_list
    3.10 -      |> apfst Code_Namespace.join_exports
    3.11 -      |> apsnd ML_Datas
    3.12 -      |> SOME
    3.13 -      |> single;
    3.14 +      let
    3.15 +        val datas = map_filter
    3.16 +          (fn (Type_Constructor tyco, (export, Code_Thingol.Datatype stmt)) => SOME (export, (tyco, stmt)) | _ => NONE) stmts
    3.17 +      in
    3.18 +        if null datas then [] (*for abstract types wrt. code_reflect*)
    3.19 +        else datas
    3.20 +          |> split_list
    3.21 +          |> apfst Code_Namespace.join_exports
    3.22 +          |> apsnd ML_Datas
    3.23 +          |> SOME
    3.24 +          |> single
    3.25 +      end;
    3.26      fun modify_class stmts =
    3.27        the_single (map_filter
    3.28          (fn (Type_Class class, (export, Code_Thingol.Class stmt)) => SOME (export, (class, stmt)) | _ => NONE) stmts)
     4.1 --- a/src/Tools/Code/code_runtime.ML	Sun May 29 14:10:48 2016 +0200
     4.2 +++ b/src/Tools/Code/code_runtime.ML	Sun May 29 14:43:17 2016 +0200
     4.3 @@ -375,20 +375,21 @@
     4.4  
     4.5  fun check_datatype thy tyco some_consts =
     4.6    let
     4.7 -    val constrs = (map fst o snd o fst o Code.get_type thy) tyco;
     4.8 -    val _ = case some_consts
     4.9 -     of SOME consts =>
    4.10 +    val declared_constrs = (map fst o snd o fst o Code.get_type thy) tyco;
    4.11 +    val constrs = case some_consts
    4.12 +     of SOME [] => []
    4.13 +      | SOME consts =>
    4.14            let
    4.15 -            val missing_constrs = subtract (op =) consts constrs;
    4.16 +            val missing_constrs = subtract (op =) consts declared_constrs;
    4.17              val _ = if null missing_constrs then []
    4.18                else error ("Missing constructor(s) " ^ commas_quote missing_constrs
    4.19                  ^ " for datatype " ^ quote tyco);
    4.20 -            val false_constrs = subtract (op =) constrs consts;
    4.21 +            val false_constrs = subtract (op =) declared_constrs consts;
    4.22              val _ = if null false_constrs then []
    4.23                else error ("Non-constructor(s) " ^ commas_quote false_constrs
    4.24                  ^ " for datatype " ^ quote tyco)
    4.25 -          in () end
    4.26 -      | NONE => ();
    4.27 +          in consts end
    4.28 +      | NONE => declared_constrs;
    4.29    in (tyco, constrs) end;
    4.30  
    4.31  fun add_eval_tyco (tyco, tyco') thy =
    4.32 @@ -465,16 +466,16 @@
    4.33  local
    4.34  
    4.35  val parse_datatype =
    4.36 -  Parse.name --| @{keyword "="} --
    4.37 +  Parse.name -- Scan.optional (@{keyword "="} |--
    4.38      (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
    4.39 -    || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME));
    4.40 +    || ((Parse.term ::: (Scan.repeat (@{keyword "|"} |-- Parse.term))) >> SOME))) (SOME []);
    4.41  
    4.42  in
    4.43  
    4.44  val _ =
    4.45    Outer_Syntax.command @{command_keyword code_reflect}
    4.46      "enrich runtime environment with generated code"
    4.47 -    (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!!  (parse_datatype
    4.48 +    (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- Parse.!!! (parse_datatype
    4.49        ::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
    4.50      -- Scan.optional (@{keyword "functions"} |-- Parse.!!!  (Scan.repeat1 Parse.name)) []
    4.51      -- Scan.option (@{keyword "file"} |-- Parse.!!! Parse.name)