1(* Title: HOL/Tools/Function/function_common.ML 2 Author: Alexander Krauss, TU Muenchen 3 4Common definitions and other infrastructure for the function package. 5*) 6 7signature FUNCTION_COMMON = 8sig 9 type info = 10 {is_partial : bool, 11 defname : binding, 12 (*contains no logical entities: invariant under morphisms:*) 13 add_simps : (binding -> binding) -> string -> (binding -> binding) -> 14 Token.src list -> thm list -> local_theory -> thm list * local_theory, 15 fnames : binding list, 16 case_names : string list, 17 fs : term list, 18 R : term, 19 dom: term, 20 psimps: thm list, 21 pinducts: thm list, 22 simps : thm list option, 23 inducts : thm list option, 24 termination : thm, 25 totality : thm option, 26 cases : thm list, 27 pelims: thm list list, 28 elims: thm list list option} 29 val profile : bool Unsynchronized.ref 30 val PROFILE : string -> ('a -> 'b) -> 'a -> 'b 31 val mk_acc : typ -> term -> term 32 val split_def : Proof.context -> (string -> 'a) -> term -> 33 string * (string * typ) list * term list * term list * term 34 val check_defs : Proof.context -> ((string * typ) * 'a) list -> term list -> unit 35 type fixes = ((string * typ) * mixfix) list 36 type 'a spec = (Attrib.binding * 'a list) list 37 datatype function_config = FunctionConfig of 38 {sequential: bool, 39 default: string option, 40 domintros: bool, 41 partials: bool} 42 type preproc = function_config -> Proof.context -> fixes -> term spec -> 43 term list * (thm list -> thm spec) * (thm list -> thm list list) * string list 44 val fname_of : term -> string 45 val mk_case_names : int -> string -> int -> string list 46 val empty_preproc : (Proof.context -> ((string * typ) * mixfix) list -> term list -> 'c) -> 47 preproc 48 val termination_rule_tac : Proof.context -> int -> tactic 49 val store_termination_rule : thm -> Context.generic -> Context.generic 50 val retrieve_function_data : Proof.context -> term -> (term * info) list 51 val add_function_data : info -> Context.generic -> Context.generic 52 val termination_prover_tac : bool -> Proof.context -> tactic 53 val set_termination_prover : (bool -> Proof.context -> tactic) -> Context.generic -> 54 Context.generic 55 val get_preproc: Proof.context -> preproc 56 val set_preproc: preproc -> Context.generic -> Context.generic 57 datatype function_result = FunctionResult of 58 {fs: term list, 59 G: term, 60 R: term, 61 dom: term, 62 psimps : thm list, 63 simple_pinducts : thm list, 64 cases : thm list, 65 pelims : thm list list, 66 termination : thm, 67 domintros : thm list option} 68 val transform_function_data : morphism -> info -> info 69 val import_function_data : term -> Proof.context -> info option 70 val import_last_function : Proof.context -> info option 71 val default_config : function_config 72 val function_parser : function_config -> 73 (function_config * ((binding * string option * mixfix) list * Specification.multi_specs_cmd)) parser 74end 75 76structure Function_Common : FUNCTION_COMMON = 77struct 78 79local open Function_Lib in 80 81(* info *) 82 83type info = 84 {is_partial : bool, 85 defname : binding, 86 (*contains no logical entities: invariant under morphisms:*) 87 add_simps : (binding -> binding) -> string -> (binding -> binding) -> 88 Token.src list -> thm list -> local_theory -> thm list * local_theory, 89 fnames : binding list, 90 case_names : string list, 91 fs : term list, 92 R : term, 93 dom: term, 94 psimps: thm list, 95 pinducts: thm list, 96 simps : thm list option, 97 inducts : thm list option, 98 termination : thm, 99 totality : thm option, 100 cases : thm list, 101 pelims : thm list list, 102 elims : thm list list option} 103 104fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts, 105 simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims} : info) = 106 let 107 val term = Morphism.term phi 108 val thm = Morphism.thm phi 109 val fact = Morphism.fact phi 110 in 111 { add_simps = add_simps, case_names = case_names, fnames = fnames, 112 fs = map term fs, R = term R, dom = term dom, psimps = fact psimps, 113 pinducts = fact pinducts, simps = Option.map fact simps, 114 inducts = Option.map fact inducts, termination = thm termination, 115 totality = Option.map thm totality, defname = Morphism.binding phi defname, 116 is_partial = is_partial, cases = fact cases, 117 elims = Option.map (map fact) elims, pelims = map fact pelims } 118 end 119 120 121(* profiling *) 122 123val profile = Unsynchronized.ref false 124 125fun PROFILE msg = if !profile then timeap_msg msg else I 126 127val acc_const_name = \<^const_name>\<open>Wellfounded.accp\<close> 128fun mk_acc domT R = 129 Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 130 131 132(* analyzing function equations *) 133 134fun split_def ctxt check_head geq = 135 let 136 fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] 137 val qs = Term.strip_qnt_vars \<^const_name>\<open>Pure.all\<close> geq 138 val imp = Term.strip_qnt_body \<^const_name>\<open>Pure.all\<close> geq 139 val (gs, eq) = Logic.strip_horn imp 140 141 val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) 142 handle TERM _ => error (input_error "Not an equation") 143 144 val (head, args) = strip_comb f_args 145 146 val fname = fst (dest_Free head) handle TERM _ => "" 147 val _ = check_head fname 148 in 149 (fname, qs, gs, args, rhs) 150 end 151 152(*check for various errors in the input*) 153fun check_defs ctxt fixes eqs = 154 let 155 val fnames = map (fst o fst) fixes 156 157 fun check geq = 158 let 159 fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) 160 161 fun check_head fname = 162 member (op =) fnames fname orelse 163 input_error ("Illegal equation head. Expected " ^ commas_quote fnames) 164 165 val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq 166 167 val _ = length args > 0 orelse input_error "Function has no arguments:" 168 169 fun add_bvs t is = add_loose_bnos (t, 0, is) 170 val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs [])) 171 |> map (fst o nth (rev qs)) 172 173 val _ = null rvs orelse input_error 174 ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^ 175 " occur" ^ plural "s" "" rvs ^ " on right hand side only:") 176 177 val _ = forall (not o Term.exists_subterm 178 (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args) 179 orelse input_error "Defined function may not occur in premises or arguments" 180 181 val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args 182 val funvars = 183 filter 184 (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs 185 val _ = null funvars orelse (warning (cat_lines 186 ["Bound variable" ^ plural " " "s " funvars ^ 187 commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^ 188 " in function position.", "Misspelled constructor???"]); true) 189 in 190 (fname, length args) 191 end 192 193 val grouped_args = AList.group (op =) (map check eqs) 194 val _ = grouped_args 195 |> map (fn (fname, ars) => 196 length (distinct (op =) ars) = 1 orelse 197 error ("Function " ^ quote fname ^ 198 " has different numbers of arguments in different equations")) 199 200 val not_defined = subtract (op =) (map fst grouped_args) fnames 201 val _ = null not_defined 202 orelse error ("No defining equations for function" ^ 203 plural " " "s " not_defined ^ commas_quote not_defined) 204 in () end 205 206 207(* preprocessors *) 208 209type fixes = ((string * typ) * mixfix) list 210type 'a spec = (Attrib.binding * 'a list) list 211 212datatype function_config = FunctionConfig of 213 {sequential: bool, 214 default: string option, 215 domintros: bool, 216 partials: bool} 217 218type preproc = function_config -> Proof.context -> fixes -> term spec -> 219 term list * (thm list -> thm spec) * (thm list -> thm list list) * string list 220 221val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o 222 HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all 223 224fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k 225 | mk_case_names _ _ 0 = [] 226 | mk_case_names _ n 1 = [n] 227 | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k) 228 229fun empty_preproc check (_: function_config) (ctxt: Proof.context) (fixes: fixes) spec = 230 let 231 val (bnds, tss) = split_list spec 232 val ts = flat tss 233 val _ = check ctxt fixes ts 234 val fnames = map (fst o fst) fixes 235 val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts 236 237 fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 238 (indices ~~ xs) |> map (map snd) 239 240 (* using theorem names for case name currently disabled *) 241 val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat 242 in 243 (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames) 244 end 245 246 247(* context data *) 248 249structure Data = Generic_Data 250( 251 type T = 252 thm list * 253 (term * info) Item_Net.T * 254 (bool -> Proof.context -> tactic) * 255 preproc 256 val empty: T = 257 ([], 258 Item_Net.init (op aconv o apply2 fst) (single o fst), 259 fn _ => error "Termination prover not configured", 260 empty_preproc check_defs) 261 val extend = I 262 fun merge 263 ((termination_rules1, functions1, termination_prover1, preproc1), 264 (termination_rules2, functions2, _, _)) : T = 265 (Thm.merge_thms (termination_rules1, termination_rules2), 266 Item_Net.merge (functions1, functions2), 267 termination_prover1, 268 preproc1) 269) 270 271fun termination_rule_tac ctxt = resolve_tac ctxt (#1 (Data.get (Context.Proof ctxt))) 272 273val store_termination_rule = Data.map o @{apply 4(1)} o cons o Thm.trim_context 274 275val get_functions = #2 o Data.get o Context.Proof 276 277fun retrieve_function_data ctxt t = 278 Item_Net.retrieve (get_functions ctxt) t 279 |> (map o apsnd) (transform_function_data (Morphism.transfer_morphism' ctxt)); 280 281val add_function_data = 282 transform_function_data Morphism.trim_context_morphism #> 283 (fn info as {fs, termination, ...} => 284 (Data.map o @{apply 4(2)}) (fold (fn f => Item_Net.update (f, info)) fs) 285 #> store_termination_rule termination) 286 287fun termination_prover_tac quiet ctxt = #3 (Data.get (Context.Proof ctxt)) quiet ctxt 288val set_termination_prover = Data.map o @{apply 4(3)} o K 289 290val get_preproc = #4 o Data.get o Context.Proof 291val set_preproc = Data.map o @{apply 4(4)} o K 292 293 294(* function definition result data *) 295 296datatype function_result = FunctionResult of 297 {fs: term list, 298 G: term, 299 R: term, 300 dom: term, 301 psimps : thm list, 302 simple_pinducts : thm list, 303 cases : thm list, 304 pelims : thm list list, 305 termination : thm, 306 domintros : thm list option} 307 308fun import_function_data t ctxt = 309 let 310 val ct = Thm.cterm_of ctxt t 311 fun inst_morph u = 312 Morphism.instantiate_morphism (Thm.match (Thm.cterm_of ctxt u, ct)) 313 fun match (u, data) = 314 SOME (transform_function_data (inst_morph u) data) handle Pattern.MATCH => NONE 315 in 316 get_first match (retrieve_function_data ctxt t) 317 end 318 319fun import_last_function ctxt = 320 (case Item_Net.content (get_functions ctxt) of 321 [] => NONE 322 | (t, _) :: _ => 323 let val ([t'], ctxt') = Variable.import_terms true [t] ctxt 324 in import_function_data t' ctxt' end) 325 326 327(* configuration management *) 328 329datatype function_opt = 330 Sequential 331 | Default of string 332 | DomIntros 333 | No_Partials 334 335fun apply_opt Sequential (FunctionConfig {sequential = _, default, domintros, partials}) = 336 FunctionConfig 337 {sequential = true, default = default, domintros = domintros, partials = partials} 338 | apply_opt (Default d) (FunctionConfig {sequential, default = _, domintros, partials}) = 339 FunctionConfig 340 {sequential = sequential, default = SOME d, domintros = domintros, partials = partials} 341 | apply_opt DomIntros (FunctionConfig {sequential, default, domintros = _, partials}) = 342 FunctionConfig 343 {sequential = sequential, default = default, domintros = true, partials = partials} 344 | apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials = _}) = 345 FunctionConfig 346 {sequential = sequential, default = default, domintros = domintros, partials = false} 347 348val default_config = 349 FunctionConfig { sequential=false, default=NONE, 350 domintros=false, partials=true} 351 352local 353 val option_parser = Parse.group (fn () => "option") 354 ((Parse.reserved "sequential" >> K Sequential) 355 || ((Parse.reserved "default" |-- Parse.term) >> Default) 356 || (Parse.reserved "domintros" >> K DomIntros) 357 || (Parse.reserved "no_partials" >> K No_Partials)) 358 359 fun config_parser default = 360 (Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.list1 option_parser) --| \<^keyword>\<open>)\<close>) []) 361 >> (fn opts => fold apply_opt opts default) 362in 363 fun function_parser default_cfg = 364 config_parser default_cfg -- Parse_Spec.specification 365end 366 367 368end 369end 370