1.1 --- a/src/HOL/Tools/function_package/fundef_common.ML Sat Jun 02 15:26:32 2007 +0200
1.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML Sat Jun 02 15:28:38 2007 +0200
1.3 @@ -3,7 +3,7 @@
1.4 Author: Alexander Krauss, TU Muenchen
1.5
1.6 A package for general recursive function definitions.
1.7 -Common type definitions and other infrastructure.
1.8 +Common definitions and other infrastructure.
1.9 *)
1.10
1.11 structure FundefCommon =
1.12 @@ -153,12 +153,10 @@
1.13 #> store_termination_rule termination
1.14
1.15
1.16 -
1.17 (* Configuration management *)
1.18 datatype fundef_opt
1.19 = Sequential
1.20 | Default of string
1.21 - | Preprocessor of string
1.22 | Target of xstring
1.23 | DomIntros
1.24 | Tailrec
1.25 @@ -168,64 +166,24 @@
1.26 {
1.27 sequential: bool,
1.28 default: string,
1.29 - preprocessor: string option,
1.30 target: xstring option,
1.31 domintros: bool,
1.32 tailrec: bool
1.33 }
1.34
1.35 -
1.36 -val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE,
1.37 - target=NONE, domintros=false, tailrec=false }
1.38 -
1.39 -val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE,
1.40 - target=NONE, domintros=false, tailrec=false }
1.41 -
1.42 -fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) =
1.43 - FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec }
1.44 - | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) =
1.45 - FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec }
1.46 - | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) =
1.47 - FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros, tailrec=tailrec }
1.48 - | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
1.49 - FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros, tailrec=tailrec }
1.50 - | apply_opt DomIntros (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
1.51 - FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true,tailrec=tailrec }
1.52 - | apply_opt Tailrec (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) =
1.53 - FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=domintros,tailrec=true }
1.54 +fun apply_opt Sequential (FundefConfig {sequential, default, target, domintros,tailrec}) =
1.55 + FundefConfig {sequential=true, default=default, target=target, domintros=domintros, tailrec=tailrec}
1.56 + | apply_opt (Default d) (FundefConfig {sequential, default, target, domintros,tailrec}) =
1.57 + FundefConfig {sequential=sequential, default=d, target=target, domintros=domintros, tailrec=tailrec}
1.58 + | apply_opt (Target t) (FundefConfig {sequential, default, target, domintros,tailrec}) =
1.59 + FundefConfig {sequential=sequential, default=default, target=SOME t, domintros=domintros, tailrec=tailrec}
1.60 + | apply_opt DomIntros (FundefConfig {sequential, default, target, domintros,tailrec}) =
1.61 + FundefConfig {sequential=sequential, default=default, target=target, domintros=true,tailrec=tailrec}
1.62 + | apply_opt Tailrec (FundefConfig {sequential, default, target, domintros,tailrec}) =
1.63 + FundefConfig {sequential=sequential, default=default, target=target, domintros=domintros,tailrec=true}
1.64
1.65 fun target_of (FundefConfig {target, ...}) = target
1.66
1.67 -local
1.68 - structure P = OuterParse and K = OuterKeyword
1.69 -
1.70 - val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
1.71 -
1.72 - val option_parser = (P.$$$ "sequential" >> K Sequential)
1.73 - || ((P.reserved "default" |-- P.term) >> Default)
1.74 - || (P.reserved "domintros" >> K DomIntros)
1.75 - || (P.reserved "tailrec" >> K Tailrec)
1.76 - || ((P.$$$ "in" |-- P.xname) >> Target)
1.77 -
1.78 - fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") [])
1.79 - >> (fn opts => fold apply_opt opts def)
1.80 -
1.81 - fun pipe_list1 s = P.enum1 "|" s
1.82 -
1.83 - val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
1.84 -
1.85 - fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
1.86 -
1.87 - val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
1.88 - --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
1.89 -
1.90 - val statements_ow = pipe_list1 statement_ow
1.91 -in
1.92 - fun fundef_parser default_cfg = config_parser default_cfg -- P.fixes --| P.$$$ "where" -- statements_ow
1.93 -end
1.94 -
1.95 -
1.96 -
1.97 (* Common operations on equations *)
1.98
1.99 fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
1.100 @@ -266,6 +224,106 @@
1.101 end
1.102
1.103
1.104 +(* Check for all sorts of errors in the input *)
1.105 +fun check_defs ctxt fixes eqs =
1.106 + let
1.107 + val fnames = map (fst o fst) fixes
1.108 +
1.109 + fun check geq =
1.110 + let
1.111 + fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
1.112 +
1.113 + val fqgar as (fname, qs, gs, args, rhs) = split_def geq
1.114 +
1.115 + val _ = fname mem fnames
1.116 + orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames
1.117 + ^ commas_quote fnames))
1.118 +
1.119 + fun add_bvs t is = add_loose_bnos (t, 0, is)
1.120 + val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
1.121 + |> map (fst o nth (rev qs))
1.122 +
1.123 + val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
1.124 + ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
1.125 +
1.126 + val _ = forall (FundefLib.forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs
1.127 + orelse error (input_error "Recursive Calls not allowed in premises")
1.128 + in
1.129 + fqgar
1.130 + end
1.131 +
1.132 + val _ = mk_arities (map check eqs)
1.133 + handle ArgumentCount fname =>
1.134 + error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
1.135 + in
1.136 + ()
1.137 + end
1.138 +
1.139 +(* Preprocessors *)
1.140 +
1.141 +type fixes = ((string * typ) * mixfix) list
1.142 +type 'a spec = ((bstring * Attrib.src list) * 'a list) list
1.143 +type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec -> (term list * (thm list -> thm spec))
1.144 +
1.145 +fun empty_preproc check _ _ ctxt fixes spec =
1.146 + let
1.147 + val (nas,tss) = split_list spec
1.148 + val _ = check ctxt fixes (flat tss)
1.149 + in
1.150 + (flat tss, curry op ~~ nas o Library.unflat tss)
1.151 + end
1.152 +
1.153 +structure Preprocessor = GenericDataFun
1.154 +(
1.155 + type T = preproc
1.156 + val empty = empty_preproc check_defs
1.157 + val extend = I
1.158 + fun merge _ (a, _) = a
1.159 +);
1.160 +
1.161 +val get_preproc = Preprocessor.get o Context.Proof
1.162 +val set_preproc = Preprocessor.map o K
1.163 +
1.164 +
1.165 +
1.166 +local
1.167 + structure P = OuterParse and K = OuterKeyword
1.168 +
1.169 + val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
1.170 +
1.171 + val option_parser = (P.$$$ "sequential" >> K Sequential)
1.172 + || ((P.reserved "default" |-- P.term) >> Default)
1.173 + || (P.reserved "domintros" >> K DomIntros)
1.174 + || (P.reserved "tailrec" >> K Tailrec)
1.175 + || ((P.$$$ "in" |-- P.xname) >> Target)
1.176 +
1.177 + fun config_parser default = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") [])
1.178 + >> (fn opts => fold apply_opt opts default)
1.179 +
1.180 + val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
1.181 +
1.182 + fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
1.183 +
1.184 + val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
1.185 + --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
1.186 +
1.187 + val statements_ow = P.enum1 "|" statement_ow
1.188 +
1.189 + val flags_statements = statements_ow
1.190 + >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
1.191 +
1.192 + fun basic_apply_flags ((config, fixes), (flags, statements)) = ((config, fixes), statements)
1.193 +in
1.194 + fun fundef_parser default_cfg = (config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements)
1.195 +
1.196 +end
1.197 +
1.198 +
1.199 +
1.200 +
1.201 +
1.202 +val default_config = FundefConfig { sequential=false, default="%x. arbitrary",
1.203 + target=NONE, domintros=false, tailrec=false }
1.204
1.205
1.206