fundamental treatment of undefined vs. universally partial replaces code_abort
authorhaftmann
Wed Jan 01 01:05:48 2014 +0100 (2014-01-01)
changeset 54890cb892d835803
parent 54889 4121d64fde90
child 54891 2f4491f15fe6
child 54893 4061ec8adb1c
fundamental treatment of undefined vs. universally partial replaces code_abort
NEWS
src/Doc/Codegen/Foundations.thy
src/Doc/IsarRef/HOL_Specific.thy
src/HOL/Enum.thy
src/HOL/HOL.thy
src/HOL/Library/Product_Vector.thy
src/HOL/List.thy
src/HOL/Real_Vector_Spaces.thy
src/Tools/Code/code_target.ML
src/Tools/Code_Generator.thy
     1.1 --- a/NEWS	Wed Jan 01 01:05:46 2014 +0100
     1.2 +++ b/NEWS	Wed Jan 01 01:05:48 2014 +0100
     1.3 @@ -33,6 +33,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* "declare [[code abort: …]]" replaces "code_abort …".
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10 +* "declare [[code drop: …]]" drops all code equations associated
    1.11 +with the given constants.
    1.12 +
    1.13  * Abolished slightly odd global lattice interpretation for min/max.
    1.14  
    1.15  Fact consolidations:
     2.1 --- a/src/Doc/Codegen/Foundations.thy	Wed Jan 01 01:05:46 2014 +0100
     2.2 +++ b/src/Doc/Codegen/Foundations.thy	Wed Jan 01 01:05:48 2014 +0100
     2.3 @@ -308,10 +308,11 @@
     2.4    of as function definitions which always fail,
     2.5    since there is never a successful pattern match on the left hand
     2.6    side.  In order to categorise a constant into that category
     2.7 -  explicitly, use @{command_def "code_abort"}:
     2.8 +  explicitly, use the @{attribute code} attribute with
     2.9 +  @{text abort}:
    2.10  *}
    2.11  
    2.12 -code_abort %quote empty_queue
    2.13 +declare %quote [[code abort: empty_queue]]
    2.14  
    2.15  text {*
    2.16    \noindent Then the code generator will just insert an error or
    2.17 @@ -324,9 +325,9 @@
    2.18  
    2.19  text {*
    2.20    \noindent This feature however is rarely needed in practice.  Note
    2.21 -  also that the HOL default setup already declares @{const undefined}
    2.22 -  as @{command "code_abort"}, which is most likely to be used in such
    2.23 -  situations.
    2.24 +  also that the HOL default setup already declares @{const undefined},
    2.25 +  which is most likely to be used in such situations, as
    2.26 +  @{text "code abort"}.
    2.27  *}
    2.28  
    2.29  
     3.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Wed Jan 01 01:05:46 2014 +0100
     3.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Wed Jan 01 01:05:48 2014 +0100
     3.3 @@ -2391,7 +2391,6 @@
     3.4    \begin{matharray}{rcl}
     3.5      @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     3.6      @{attribute_def (HOL) code} & : & @{text attribute} \\
     3.7 -    @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
     3.8      @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
     3.9      @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    3.10      @{attribute_def (HOL) code_unfold} & : & @{text attribute} \\
    3.11 @@ -2435,10 +2434,8 @@
    3.12      target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
    3.13      ;
    3.14  
    3.15 -    @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract' )?
    3.16 -    ;
    3.17 -
    3.18 -    @@{command (HOL) code_abort} ( const + )
    3.19 +    @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract'
    3.20 +      | 'drop:' ( const + ) | 'abort:' ( const + ) )?
    3.21      ;
    3.22  
    3.23      @@{command (HOL) code_datatype} ( const + )
    3.24 @@ -2600,13 +2597,15 @@
    3.25    of the underlying equation.  Variant @{text "code del"}
    3.26    deselects a code equation for code generation.
    3.27  
    3.28 +  Variants @{text "code drop:"} and @{text "code abort:"} take
    3.29 +  a list of constant as arguments and drop all code equations declared
    3.30 +  for them.  In the case of {text abort}, these constants then are
    3.31 +  are not required to have a definition by means of code equations;
    3.32 +  if needed these are implemented by program abort (exception) instead.
    3.33 +
    3.34    Usually packages introducing code equations provide a reasonable
    3.35    default setup for selection.  
    3.36  
    3.37 -  \item @{command (HOL) "code_abort"} declares constants which are not
    3.38 -  required to have a definition by means of code equations; if needed
    3.39 -  these are implemented by program abort instead.
    3.40 -
    3.41    \item @{command (HOL) "code_datatype"} specifies a constructor set
    3.42    for a logical type.
    3.43  
     4.1 --- a/src/HOL/Enum.thy	Wed Jan 01 01:05:46 2014 +0100
     4.2 +++ b/src/HOL/Enum.thy	Wed Jan 01 01:05:48 2014 +0100
     4.3 @@ -116,7 +116,7 @@
     4.4      unfolding enum_the_def by (auto split: list.split)
     4.5  qed
     4.6  
     4.7 -code_abort enum_the
     4.8 +declare [[code abort: enum_the]]
     4.9  
    4.10  code_printing
    4.11    constant enum_the \<rightharpoonup> (Eval) "(fn '_ => raise Match)"
     5.1 --- a/src/HOL/HOL.thy	Wed Jan 01 01:05:46 2014 +0100
     5.2 +++ b/src/HOL/HOL.thy	Wed Jan 01 01:05:48 2014 +0100
     5.3 @@ -1832,7 +1832,7 @@
     5.4    #> Code.add_undefined @{const_name undefined}
     5.5  *}
     5.6  
     5.7 -code_abort undefined
     5.8 +declare [[code abort: undefined]]
     5.9  
    5.10  
    5.11  subsubsection {* Generic code generator target languages *}
     6.1 --- a/src/HOL/Library/Product_Vector.thy	Wed Jan 01 01:05:46 2014 +0100
     6.2 +++ b/src/HOL/Library/Product_Vector.thy	Wed Jan 01 01:05:48 2014 +0100
     6.3 @@ -87,7 +87,7 @@
     6.4  
     6.5  end
     6.6  
     6.7 -code_abort "open::('a::topological_space*'b::topological_space) set \<Rightarrow> bool"
     6.8 +declare [[code abort: "open::('a::topological_space*'b::topological_space) set \<Rightarrow> bool"]]
     6.9  
    6.10  lemma open_Times: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<times> T)"
    6.11  unfolding open_prod_def by auto
    6.12 @@ -346,7 +346,7 @@
    6.13  
    6.14  end
    6.15  
    6.16 -code_abort "dist::('a::metric_space*'b::metric_space)\<Rightarrow>('a*'b) \<Rightarrow> real"
    6.17 +declare [[code abort: "dist::('a::metric_space*'b::metric_space)\<Rightarrow>('a*'b) \<Rightarrow> real"]]
    6.18  
    6.19  lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
    6.20    unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
    6.21 @@ -426,7 +426,7 @@
    6.22  
    6.23  end
    6.24  
    6.25 -code_abort "norm::('a::real_normed_vector*'b::real_normed_vector) \<Rightarrow> real"
    6.26 +declare [[code abort: "norm::('a::real_normed_vector*'b::real_normed_vector) \<Rightarrow> real"]]
    6.27  
    6.28  instance prod :: (banach, banach) banach ..
    6.29  
     7.1 --- a/src/HOL/List.thy	Wed Jan 01 01:05:46 2014 +0100
     7.2 +++ b/src/HOL/List.thy	Wed Jan 01 01:05:48 2014 +0100
     7.3 @@ -6133,7 +6133,7 @@
     7.4  
     7.5  definition "abort_Bleast S P = (LEAST x. x \<in> S \<and> P x)"
     7.6  
     7.7 -code_abort abort_Bleast
     7.8 +declare [[code abort: abort_Bleast]]
     7.9  
    7.10  lemma Bleast_code [code]:
    7.11   "Bleast (set xs) P = (case filter P (sort xs) of
     8.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Jan 01 01:05:46 2014 +0100
     8.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Jan 01 01:05:48 2014 +0100
     8.3 @@ -968,7 +968,7 @@
     8.4  
     8.5  end
     8.6  
     8.7 -code_abort "open :: real set \<Rightarrow> bool"
     8.8 +declare [[code abort: "open :: real set \<Rightarrow> bool"]]
     8.9  
    8.10  instance real :: linorder_topology
    8.11  proof
     9.1 --- a/src/Tools/Code/code_target.ML	Wed Jan 01 01:05:46 2014 +0100
     9.2 +++ b/src/Tools/Code/code_target.ML	Wed Jan 01 01:05:48 2014 +0100
     9.3 @@ -64,7 +64,6 @@
     9.4    val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
     9.5    val add_reserved: string -> string -> theory -> theory
     9.6    val add_include: string -> string * (string * string list) option -> theory -> theory
     9.7 -  val allow_abort: string -> theory -> theory
     9.8  
     9.9    val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
    9.10  
    9.11 @@ -231,23 +230,20 @@
    9.12  
    9.13  structure Targets = Theory_Data
    9.14  (
    9.15 -  type T = (target Symtab.table * string list) * int;
    9.16 -  val empty = ((Symtab.empty, []), 80);
    9.17 +  type T = target Symtab.table * int;
    9.18 +  val empty = (Symtab.empty, 80);
    9.19    val extend = I;
    9.20 -  fun merge (((target1, exc1), width1), ((target2, exc2), width2)) : T =
    9.21 -    ((Symtab.join (merge_target true) (target1, target2),
    9.22 -      Library.merge (op =) (exc1, exc2)), Int.max (width1, width2));
    9.23 +  fun merge ((target1, width1), (target2, width2)) : T =
    9.24 +    (Symtab.join (merge_target true) (target1, target2), Int.max (width1, width2));
    9.25  );
    9.26  
    9.27 -val abort_allowed = snd o fst o Targets.get;
    9.28 -
    9.29 -fun assert_target thy target = if Symtab.defined ((fst o fst) (Targets.get thy)) target
    9.30 +fun assert_target thy target = if Symtab.defined (fst (Targets.get thy)) target
    9.31    then target
    9.32    else error ("Unknown code target language: " ^ quote target);
    9.33  
    9.34  fun put_target (target, seri) thy =
    9.35    let
    9.36 -    val lookup_target = Symtab.lookup ((fst o fst) (Targets.get thy));
    9.37 +    val lookup_target = Symtab.lookup (fst (Targets.get thy));
    9.38      val _ = case seri
    9.39       of Extension (super, _) => if is_some (lookup_target super) then ()
    9.40            else error ("Unknown code target language: " ^ quote super)
    9.41 @@ -263,7 +259,7 @@
    9.42        else ();
    9.43    in
    9.44      thy
    9.45 -    |> (Targets.map o apfst o apfst o Symtab.update)
    9.46 +    |> (Targets.map o apfst o Symtab.update)
    9.47          (target, make_target ((serial (), seri),
    9.48            ([], (Code_Symbol.empty_data, Code_Symbol.empty_data))))
    9.49    end;
    9.50 @@ -277,7 +273,7 @@
    9.51      val _ = assert_target thy target;
    9.52    in
    9.53      thy
    9.54 -    |> (Targets.map o apfst o apfst o Symtab.map_entry target o map_target o apsnd) f
    9.55 +    |> (Targets.map o apfst o Symtab.map_entry target o map_target o apsnd) f
    9.56    end;
    9.57  
    9.58  fun map_reserved target =
    9.59 @@ -296,7 +292,7 @@
    9.60  
    9.61  fun the_fundamental thy =
    9.62    let
    9.63 -    val ((targets, _), _) = Targets.get thy;
    9.64 +    val (targets, _) = Targets.get thy;
    9.65      fun fundamental target = case Symtab.lookup targets target
    9.66       of SOME data => (case the_description data
    9.67           of Fundamental data => data
    9.68 @@ -308,7 +304,7 @@
    9.69  
    9.70  fun collapse_hierarchy thy =
    9.71    let
    9.72 -    val ((targets, _), _) = Targets.get thy;
    9.73 +    val (targets, _) = Targets.get thy;
    9.74      fun collapse target =
    9.75        let
    9.76          val data = case Symtab.lookup targets target
    9.77 @@ -326,9 +322,9 @@
    9.78  
    9.79  fun activate_target thy target =
    9.80    let
    9.81 -    val ((_, abortable), default_width) = Targets.get thy;
    9.82 +    val (_, default_width) = Targets.get thy;
    9.83      val (modify, data) = collapse_hierarchy thy target;
    9.84 -  in (default_width, abortable, data, modify) end;
    9.85 +  in (default_width, data, modify) end;
    9.86  
    9.87  fun activate_const_syntax thy literals cs_data naming =
    9.88    (Symtab.empty, naming)
    9.89 @@ -363,14 +359,13 @@
    9.90        (const_syntax, tyco_syntax, class_syntax))
    9.91    end;
    9.92  
    9.93 -fun project_program thy abortable names_hidden names1 program2 =
    9.94 +fun project_program thy names_hidden names1 program2 =
    9.95    let
    9.96      val ctxt = Proof_Context.init_global thy;
    9.97      val names2 = subtract (op =) names_hidden names1;
    9.98      val program3 = Graph.restrict (not o member (op =) names_hidden) program2;
    9.99      val names4 = Graph.all_succs program3 names2;
   9.100 -    val unimplemented = filter_out (member (op =) abortable)
   9.101 -      (Code_Thingol.unimplemented program3);
   9.102 +    val unimplemented = Code_Thingol.unimplemented program3;
   9.103      val _ =
   9.104        if null unimplemented then ()
   9.105        else error ("No code equations for " ^
   9.106 @@ -378,12 +373,12 @@
   9.107      val program4 = Graph.restrict (member (op =) names4) program3;
   9.108    in (names4, program4) end;
   9.109  
   9.110 -fun prepare_serializer thy abortable (serializer : serializer) literals reserved identifiers
   9.111 +fun prepare_serializer thy (serializer : serializer) literals reserved identifiers
   9.112      printings module_name args naming proto_program names =
   9.113    let
   9.114      val (names_hidden, (const_syntax, tyco_syntax, class_syntax)) =
   9.115        activate_symbol_syntax thy literals naming printings;
   9.116 -    val (names_all, program) = project_program thy abortable names_hidden names proto_program;
   9.117 +    val (names_all, program) = project_program thy names_hidden names proto_program;
   9.118      fun select_include (name, (content, cs)) =
   9.119        if null cs orelse exists (fn c => case Code_Thingol.lookup_const naming c
   9.120         of SOME name => member (op =) names_all name
   9.121 @@ -405,11 +400,11 @@
   9.122  
   9.123  fun mount_serializer thy target some_width module_name args naming program names =
   9.124    let
   9.125 -    val (default_width, abortable, data, modify) = activate_target thy target;
   9.126 +    val (default_width, data, modify) = activate_target thy target;
   9.127      val serializer = case the_description data
   9.128       of Fundamental seri => #serializer seri;
   9.129      val (prepared_serializer, prepared_program) =
   9.130 -      prepare_serializer thy abortable serializer (the_literals thy target)
   9.131 +      prepare_serializer thy serializer (the_literals thy target)
   9.132          (the_reserved data) (the_identifiers data) (the_printings data)
   9.133          module_name args naming (modify naming program) names
   9.134      val width = the_default default_width some_width;
   9.135 @@ -502,7 +497,7 @@
   9.136  
   9.137  fun implemented_functions thy naming program =
   9.138    let
   9.139 -    val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.unimplemented program);
   9.140 +    val cs = Code_Thingol.unimplemented program;
   9.141      val names = map_filter (Code_Thingol.lookup_const naming) cs;
   9.142    in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
   9.143  
   9.144 @@ -699,14 +694,6 @@
   9.145      target name some_content thy;
   9.146  
   9.147  
   9.148 -(* abortable constants *)
   9.149 -
   9.150 -fun gen_allow_abort prep_const raw_c thy =
   9.151 -  let
   9.152 -    val c = prep_const thy raw_c;
   9.153 -  in thy |> (Targets.map o apfst o apsnd) (insert (op =) c) end;
   9.154 -
   9.155 -
   9.156  (* concrete syntax *)
   9.157  
   9.158  local
   9.159 @@ -732,14 +719,12 @@
   9.160  val add_class_syntax = gen_add_class_syntax cert_class;
   9.161  val add_instance_syntax = gen_add_instance_syntax cert_inst;
   9.162  val add_include = gen_add_include (K I);
   9.163 -val allow_abort = gen_allow_abort (K I);
   9.164  
   9.165  val add_const_syntax_cmd = gen_add_const_syntax Code.read_const;
   9.166  val add_tyco_syntax_cmd = gen_add_tyco_syntax read_tyco;
   9.167  val add_class_syntax_cmd = gen_add_class_syntax read_class;
   9.168  val add_instance_syntax_cmd = gen_add_instance_syntax read_inst;
   9.169  val add_include_cmd = gen_add_include Code.read_const;
   9.170 -val allow_abort_cmd = gen_allow_abort Code.read_const;
   9.171  
   9.172  fun parse_args f args =
   9.173    case Scan.read Token.stopper f args
   9.174 @@ -842,11 +827,6 @@
   9.175            (Toplevel.theory o add_include_cmd target) (name, content_consts)));
   9.176  
   9.177  val _ =
   9.178 -  Outer_Syntax.command @{command_spec "code_abort"}
   9.179 -    "permit constant to be implemented as program abort"
   9.180 -    (Scan.repeat1 Parse.term >> (Toplevel.theory o fold allow_abort_cmd));
   9.181 -
   9.182 -val _ =
   9.183    Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
   9.184      (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
   9.185  
    10.1 --- a/src/Tools/Code_Generator.thy	Wed Jan 01 01:05:46 2014 +0100
    10.2 +++ b/src/Tools/Code_Generator.thy	Wed Jan 01 01:05:48 2014 +0100
    10.3 @@ -10,7 +10,7 @@
    10.4    "value" "print_codeproc" "code_thms" "code_deps" :: diag and
    10.5    "export_code" "code_identifier" "code_printing" "code_class" "code_instance" "code_type"
    10.6      "code_const" "code_reserved" "code_include" "code_modulename"
    10.7 -    "code_abort" "code_monad" "code_reflect" :: thy_decl and
    10.8 +    "code_monad" "code_reflect" :: thy_decl and
    10.9    "datatypes" "functions" "module_name" "file" "checking"
   10.10    "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
   10.11  begin