configuration flag "partials"
authorkrauss
Sat Oct 24 20:47:10 2009 +0200 (2009-10-24)
changeset 331018846318b52d0
parent 33100 acc2bd3934ba
child 33102 e3463e6db704
configuration flag "partials"
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_common.ML
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Fri Oct 23 16:37:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Sat Oct 24 20:47:10 2009 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4  
     1.5  
     1.6  val fun_config = FunctionConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), 
     1.7 -                                domintros=false, tailrec=false }
     1.8 +  domintros=false, partials=false, tailrec=false }
     1.9  
    1.10  fun gen_fun add config fixes statements int lthy =
    1.11    let val group = serial_string () in
     2.1 --- a/src/HOL/Tools/Function/function.ML	Fri Oct 23 16:37:56 2009 +0200
     2.2 +++ b/src/HOL/Tools/Function/function.ML	Sat Oct 24 20:47:10 2009 +0200
     2.3 @@ -77,6 +77,7 @@
     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, ...} = config
     2.8  
     2.9        val ((goalstate, cont), lthy) =
    2.10            Function_Mutual.prepare_function_mutual config defname fixes eqs lthy
     3.1 --- a/src/HOL/Tools/Function/function_common.ML	Fri Oct 23 16:37:56 2009 +0200
     3.2 +++ b/src/HOL/Tools/Function/function_common.ML	Sat Oct 24 20:47:10 2009 +0200
     3.3 @@ -170,6 +170,7 @@
     3.4    = Sequential
     3.5    | Default of string
     3.6    | DomIntros
     3.7 +  | No_Partials
     3.8    | Tailrec
     3.9  
    3.10  datatype function_config
    3.11 @@ -178,21 +179,24 @@
    3.12      sequential: bool,
    3.13      default: string,
    3.14      domintros: bool,
    3.15 +    partials: bool,
    3.16      tailrec: bool
    3.17     }
    3.18  
    3.19 -fun apply_opt Sequential (FunctionConfig {sequential, default, domintros,tailrec}) = 
    3.20 -    FunctionConfig {sequential=true, default=default, domintros=domintros, tailrec=tailrec}
    3.21 -  | apply_opt (Default d) (FunctionConfig {sequential, default, domintros,tailrec}) = 
    3.22 -    FunctionConfig {sequential=sequential, default=d, domintros=domintros, tailrec=tailrec}
    3.23 -  | apply_opt DomIntros (FunctionConfig {sequential, default, domintros,tailrec}) =
    3.24 -    FunctionConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec}
    3.25 -  | apply_opt Tailrec (FunctionConfig {sequential, default, domintros,tailrec}) =
    3.26 -    FunctionConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
    3.27 +fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
    3.28 +    FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials, tailrec=tailrec}
    3.29 +  | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
    3.30 +    FunctionConfig {sequential=sequential, default=d, domintros=domintros, partials=partials, tailrec=tailrec}
    3.31 +  | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
    3.32 +    FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials, tailrec=tailrec}
    3.33 +  | apply_opt Tailrec (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
    3.34 +    FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=partials, tailrec=true}
    3.35 +  | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials, tailrec}) =
    3.36 +    FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false, tailrec=true}
    3.37  
    3.38  val default_config =
    3.39    FunctionConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), 
    3.40 -                 domintros=false, tailrec=false }
    3.41 +    domintros=false, partials=true, tailrec=false }
    3.42  
    3.43  
    3.44  (* Analyzing function equations *)
    3.45 @@ -327,6 +331,7 @@
    3.46        P.group "option" ((P.reserved "sequential" >> K Sequential)
    3.47                      || ((P.reserved "default" |-- P.term) >> Default)
    3.48                      || (P.reserved "domintros" >> K DomIntros)
    3.49 +                    || (P.reserved "no_partials" >> K No_Partials)
    3.50                      || (P.reserved "tailrec" >> K Tailrec))
    3.51  
    3.52    fun config_parser default =