explicit check that abstract constructors cannot be part of official interface
authorhaftmann
Sun May 29 14:43:18 2016 +0200 (2016-05-29)
changeset 63175d191892b1c23
parent 63174 57c0d60e491c
child 63184 dd6cd88cebd9
explicit check that abstract constructors cannot be part of official interface
NEWS
src/Doc/Codegen/Evaluation.thy
src/Tools/Code/code_thingol.ML
     1.1 --- a/NEWS	Sun May 29 14:43:17 2016 +0200
     1.2 +++ b/NEWS	Sun May 29 14:43:18 2016 +0200
     1.3 @@ -103,6 +103,10 @@
     1.4  * Command 'code_reflect' accepts empty constructor lists for datatypes,
     1.5  which renders those abstract effectively.
     1.6  
     1.7 +* Command 'export_code' checks given constants for abstraction violations:
     1.8 +a small guarantee that given constants specify a safe interface for the
     1.9 +generated code.
    1.10 +
    1.11  * Probability/Random_Permutations.thy contains some theory about 
    1.12  choosing a permutation of a set uniformly at random and folding over a 
    1.13  list in random order.
     2.1 --- a/src/Doc/Codegen/Evaluation.thy	Sun May 29 14:43:17 2016 +0200
     2.2 +++ b/src/Doc/Codegen/Evaluation.thy	Sun May 29 14:43:18 2016 +0200
     2.3 @@ -344,7 +344,7 @@
     2.4  \<close>
     2.5  
     2.6  code_reflect %quote Rat
     2.7 -  datatypes rat = Frct
     2.8 +  datatypes rat
     2.9    functions Fract
    2.10      "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
    2.11      "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
     3.1 --- a/src/Tools/Code/code_thingol.ML	Sun May 29 14:43:17 2016 +0200
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Sun May 29 14:43:18 2016 +0200
     3.3 @@ -786,11 +786,23 @@
     3.4  
     3.5  (* program generation *)
     3.6  
     3.7 +fun check_abstract_constructors thy consts =
     3.8 +  case filter (Code.is_abstr thy) consts of
     3.9 +    [] => ()
    3.10 +  | abstrs => error ("Cannot export abstract constructor(s): "
    3.11 +      ^ commas (map (Code.string_of_const thy) abstrs));
    3.12 +
    3.13  fun invoke_generation_for_consts ctxt { ignore_cache, permissive } { algebra, eqngr } consts =
    3.14 -  Code_Preproc.timed "translating program" #ctxt
    3.15 -  (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt
    3.16 -    (fold_map (ensure_const ctxt algebra eqngr permissive)) consts)
    3.17 -    { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts };
    3.18 +  let
    3.19 +    val thy = Proof_Context.theory_of ctxt;
    3.20 +    val _ = if permissive then ()
    3.21 +      else check_abstract_constructors thy consts;
    3.22 +  in
    3.23 +    Code_Preproc.timed "translating program" #ctxt
    3.24 +    (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt
    3.25 +      (fold_map (ensure_const ctxt algebra eqngr permissive)) consts)
    3.26 +      { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts }
    3.27 +  end;
    3.28  
    3.29  fun invoke_generation_for_consts' ctxt ignore_cache_and_permissive consts =
    3.30    invoke_generation_for_consts ctxt
    3.31 @@ -914,7 +926,8 @@
    3.32      val thy = Proof_Context.theory_of ctxt;
    3.33      fun consts_of thy' =
    3.34        fold (fn (c, (_, NONE)) => cons c | _ => I)
    3.35 -        (#constants (Consts.dest (Sign.consts_of thy'))) [];
    3.36 +        (#constants (Consts.dest (Sign.consts_of thy'))) []
    3.37 +      |> filter_out (Code.is_abstr thy);
    3.38      fun belongs_here thy' c = forall
    3.39        (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
    3.40      fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
    3.41 @@ -934,8 +947,10 @@
    3.42    let
    3.43      val (consts, consts_permissive) =
    3.44        read_const_exprs_internal ctxt const_exprs;
    3.45 -    val consts' = implemented_deps
    3.46 -      (consts_program_permissive ctxt consts_permissive);
    3.47 +    val consts' = 
    3.48 +      consts_program_permissive ctxt consts_permissive
    3.49 +      |> implemented_deps
    3.50 +      |> filter_out (Code.is_abstr (Proof_Context.theory_of ctxt));
    3.51    in union (op =) consts' consts end;
    3.52  
    3.53