# HG changeset patch # User krauss # Date 1256410030 -7200 # Node ID 8846318b52d08d30a11cfd3198fe1dba7566027d # Parent acc2bd3934baaae8dcd7d2bc76d52417b6689c9f configuration flag "partials" diff -r acc2bd3934ba -r 8846318b52d0 src/HOL/Tools/Function/fun.ML --- a/src/HOL/Tools/Function/fun.ML Fri Oct 23 16:37:56 2009 +0200 +++ b/src/HOL/Tools/Function/fun.ML Sat Oct 24 20:47:10 2009 +0200 @@ -148,7 +148,7 @@ val fun_config = FunctionConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), - domintros=false, tailrec=false } + domintros=false, partials=false, tailrec=false } fun gen_fun add config fixes statements int lthy = let val group = serial_string () in diff -r acc2bd3934ba -r 8846318b52d0 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Fri Oct 23 16:37:56 2009 +0200 +++ b/src/HOL/Tools/Function/function.ML Sat Oct 24 20:47:10 2009 +0200 @@ -77,6 +77,7 @@ val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec val defname = mk_defname fixes + val FunctionConfig {partials, ...} = config val ((goalstate, cont), lthy) = Function_Mutual.prepare_function_mutual config defname fixes eqs lthy diff -r acc2bd3934ba -r 8846318b52d0 src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Fri Oct 23 16:37:56 2009 +0200 +++ b/src/HOL/Tools/Function/function_common.ML Sat Oct 24 20:47:10 2009 +0200 @@ -170,6 +170,7 @@ = Sequential | Default of string | DomIntros + | No_Partials | Tailrec datatype function_config @@ -178,21 +179,24 @@ sequential: bool, default: string, domintros: bool, + partials: bool, tailrec: bool } -fun apply_opt Sequential (FunctionConfig {sequential, default, domintros,tailrec}) = - FunctionConfig {sequential=true, default=default, domintros=domintros, tailrec=tailrec} - | apply_opt (Default d) (FunctionConfig {sequential, default, domintros,tailrec}) = - FunctionConfig {sequential=sequential, default=d, domintros=domintros, tailrec=tailrec} - | apply_opt DomIntros (FunctionConfig {sequential, default, domintros,tailrec}) = - FunctionConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec} - | apply_opt Tailrec (FunctionConfig {sequential, default, domintros,tailrec}) = - FunctionConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true} +fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials, tailrec}) = + FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials, tailrec=tailrec} + | apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials, tailrec}) = + FunctionConfig {sequential=sequential, default=d, domintros=domintros, partials=partials, tailrec=tailrec} + | apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials, tailrec}) = + FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials, tailrec=tailrec} + | apply_opt Tailrec (FunctionConfig {sequential, default, domintros, partials, tailrec}) = + FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=partials, tailrec=true} + | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials, tailrec}) = + FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false, tailrec=true} val default_config = FunctionConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), - domintros=false, tailrec=false } + domintros=false, partials=true, tailrec=false } (* Analyzing function equations *) @@ -327,6 +331,7 @@ P.group "option" ((P.reserved "sequential" >> K Sequential) || ((P.reserved "default" |-- P.term) >> Default) || (P.reserved "domintros" >> K DomIntros) + || (P.reserved "no_partials" >> K No_Partials) || (P.reserved "tailrec" >> K Tailrec)) fun config_parser default =