function (default) is legacy feature
authorkrauss
Wed Dec 29 21:52:41 2010 +0100 (2010-12-29)
changeset 41417211dbd42f95d
parent 41414 00b2b6716ed8
child 41418 b6dc60638be0
function (default) is legacy feature
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_common.ML
src/HOL/Tools/Function/function_core.ML
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Wed Dec 29 18:18:42 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Wed Dec 29 21:52:41 2010 +0100
     1.3 @@ -136,7 +136,7 @@
     1.4    Context.theory_map (Function_Common.set_preproc sequential_preproc)
     1.5  
     1.6  
     1.7 -val fun_config = FunctionConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), 
     1.8 +val fun_config = FunctionConfig { sequential=true, default=NONE,
     1.9    domintros=false, partials=false, tailrec=false }
    1.10  
    1.11  fun gen_add_fun add fixes statements config lthy =
     2.1 --- a/src/HOL/Tools/Function/function.ML	Wed Dec 29 18:18:42 2010 +0100
     2.2 +++ b/src/HOL/Tools/Function/function.ML	Wed Dec 29 21:52:41 2010 +0100
     2.3 @@ -85,11 +85,15 @@
     2.4      val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
     2.5  
     2.6      val defname = mk_defname fixes
     2.7 -    val FunctionConfig {partials, tailrec, ...} = config
     2.8 +    val FunctionConfig {partials, tailrec, default, ...} = config
     2.9      val _ =
    2.10        if tailrec then Output.legacy_feature
    2.11          "'function (tailrec)' command. Use 'partial_function (tailrec)'."
    2.12        else ()
    2.13 +    val _ =
    2.14 +      if is_some default then Output.legacy_feature
    2.15 +        "'function (default)'. Use 'partial_function'."
    2.16 +      else ()
    2.17  
    2.18      val ((goal_state, cont), lthy') =
    2.19        Function_Mutual.prepare_function_mutual config defname fixes eqs lthy
     3.1 --- a/src/HOL/Tools/Function/function_common.ML	Wed Dec 29 18:18:42 2010 +0100
     3.2 +++ b/src/HOL/Tools/Function/function_common.ML	Wed Dec 29 21:52:41 2010 +0100
     3.3 @@ -191,7 +191,7 @@
     3.4  
     3.5  datatype function_config = FunctionConfig of
     3.6   {sequential: bool,
     3.7 -  default: string,
     3.8 +  default: string option,
     3.9    domintros: bool,
    3.10    partials: bool,
    3.11    tailrec: bool}
    3.12 @@ -199,7 +199,7 @@
    3.13  fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
    3.14      FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials, tailrec=tailrec}
    3.15    | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
    3.16 -    FunctionConfig {sequential=sequential, default=d, domintros=domintros, partials=partials, tailrec=tailrec}
    3.17 +    FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials, tailrec=tailrec}
    3.18    | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
    3.19      FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials, tailrec=tailrec}
    3.20    | apply_opt Tailrec (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
    3.21 @@ -208,7 +208,7 @@
    3.22      FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false, tailrec=true}
    3.23  
    3.24  val default_config =
    3.25 -  FunctionConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), 
    3.26 +  FunctionConfig { sequential=false, default=NONE,
    3.27      domintros=false, partials=true, tailrec=false }
    3.28  
    3.29  
     4.1 --- a/src/HOL/Tools/Function/function_core.ML	Wed Dec 29 18:18:42 2010 +0100
     4.2 +++ b/src/HOL/Tools/Function/function_core.ML	Wed Dec 29 21:52:41 2010 +0100
     4.3 @@ -871,8 +871,9 @@
     4.4  
     4.5  fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
     4.6    let
     4.7 -    val FunctionConfig {domintros, tailrec, default=default_str, ...} = config
     4.8 +    val FunctionConfig {domintros, tailrec, default=default_opt, ...} = config
     4.9  
    4.10 +    val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*)
    4.11      val fvar = Free (fname, fT)
    4.12      val domT = domain_type fT
    4.13      val ranT = range_type fT