src/HOL/Tools/function_package/fundef_common.ML
changeset 28883 0f5b1accfb94
parent 28524 644b62cf678f
child 28884 7cef91288634
equal deleted inserted replaced
28882:57bfd0fdea09 28883:0f5b1accfb94
   105 (* Generally useful?? *)
   105 (* Generally useful?? *)
   106 fun lift_morphism thy f = 
   106 fun lift_morphism thy f = 
   107     let 
   107     let 
   108       val term = Drule.term_rule thy f
   108       val term = Drule.term_rule thy f
   109     in
   109     in
   110       Morphism.thm_morphism f $> Morphism.term_morphism term $> Morphism.typ_morphism (Logic.type_map term)
   110       Morphism.thm_morphism f $> Morphism.term_morphism term 
       
   111        $> Morphism.typ_morphism (Logic.type_map term)
   111     end
   112     end
   112 
   113 
   113 fun import_fundef_data t ctxt =
   114 fun import_fundef_data t ctxt =
   114     let
   115     let
   115       val thy = Context.theory_of ctxt
   116       val thy = Context.theory_of ctxt
   187     FundefConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec}
   188     FundefConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec}
   188   | apply_opt Tailrec (FundefConfig {sequential, default, domintros,tailrec}) =
   189   | apply_opt Tailrec (FundefConfig {sequential, default, domintros,tailrec}) =
   189     FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
   190     FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
   190 
   191 
   191 val default_config =
   192 val default_config =
   192   FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), domintros=false, tailrec=false }
   193   FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), 
       
   194                  domintros=false, tailrec=false }
   193 
   195 
   194 
   196 
   195 (* Analyzing function equations *)
   197 (* Analyzing function equations *)
   196 
   198 
   197 fun split_def ctxt geq =
   199 fun split_def ctxt geq =
   232     let
   234     let
   233       val fnames = map (fst o fst) fixes
   235       val fnames = map (fst o fst) fixes
   234                                 
   236                                 
   235       fun check geq = 
   237       fun check geq = 
   236           let
   238           let
   237             fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
   239             fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
   238                                   
   240                                   
   239             val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
   241             val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
   240                                  
   242                                  
   241             val _ = fname mem fnames 
   243             val _ = fname mem fnames 
   242                     orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames 
   244                     orelse input_error 
   243                                                ^ commas_quote fnames))
   245                              ("Head symbol of left hand side must be " 
       
   246                               ^ plural "" "one out of " fnames ^ commas_quote fnames)
   244                                             
   247                                             
   245             fun add_bvs t is = add_loose_bnos (t, 0, is)
   248             fun add_bvs t is = add_loose_bnos (t, 0, is)
   246             val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
   249             val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
   247                         |> map (fst o nth (rev qs))
   250                         |> map (fst o nth (rev qs))
   248                       
   251                       
   249             val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
   252             val _ = null rvs orelse input_error 
   250                                                         ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
   253                         ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
       
   254                          ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
   251                                     
   255                                     
   252             val _ = forall (not o Term.exists_subterm (fn Free (n, _) => n mem fnames | _ => false)) gs 
   256             val _ = forall (not o Term.exists_subterm 
   253                     orelse error (input_error "Recursive Calls not allowed in premises")
   257                              (fn Free (n, _) => n mem fnames | _ => false)) gs 
       
   258                     orelse input_error "Recursive Calls not allowed in premises"
   254 
   259 
   255             val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
   260             val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
   256             val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
   261             val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
   257             val _ = null funvars
   262             val _ = null funvars
   258                     orelse (warning (cat_lines ["Bound variable" ^ plural " " "s " funvars ^ commas_quote (map fst funvars) ^  
   263                     orelse (warning (cat_lines 
   259                                                 " occur" ^ plural "s" "" funvars ^ " in function position.",  
   264                     ["Bound variable" ^ plural " " "s " funvars 
   260                                                 "Misspelled constructor???"]); true)
   265                      ^ commas_quote (map fst funvars) ^  
       
   266                      " occur" ^ plural "s" "" funvars ^ " in function position.",  
       
   267                      "Misspelled constructor???"]); true)
   261           in
   268           in
   262             fqgar
   269             fqgar
   263           end
   270           end
   264           
   271           
   265       fun check_sorts ((fname, fT), _) =
   272       fun check_sorts ((fname, fT), _) =
   266           Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
   273           Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
   267           orelse error ("Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ".")
   274           orelse error (cat_lines 
       
   275           ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
       
   276            setmp show_sorts true (Syntax.string_of_typ ctxt) fT])
   268 
   277 
   269       val _ = map check_sorts fixes
   278       val _ = map check_sorts fixes
   270 
   279 
   271       val _ = mk_arities (map check eqs)
   280       val _ = mk_arities (map check eqs)
   272           handle ArgumentCount fname => 
   281           handle ArgumentCount fname => 
   273                  error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
   282                  error ("Function " ^ quote fname ^ 
       
   283                         " has different numbers of arguments in different equations")
   274     in
   284     in
   275       ()
   285       ()
   276     end
   286     end
   277 
   287 
   278 (* Preprocessors *)
   288 (* Preprocessors *)
   280 type fixes = ((string * typ) * mixfix) list
   290 type fixes = ((string * typ) * mixfix) list
   281 type 'a spec = ((bstring * Attrib.src list) * 'a list) list
   291 type 'a spec = ((bstring * Attrib.src list) * 'a list) list
   282 type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec 
   292 type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec 
   283                -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
   293                -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
   284 
   294 
   285 val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
   295 val fname_of = fst o dest_Free o fst o strip_comb o fst 
       
   296  o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
   286 
   297 
   287 fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
   298 fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
   288   | mk_case_names _ n 0 = []
   299   | mk_case_names _ n 0 = []
   289   | mk_case_names _ n 1 = [n]
   300   | mk_case_names _ n 1 = [n]
   290   | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
   301   | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
   295       val ts = flat tss
   306       val ts = flat tss
   296       val _ = check ctxt fixes ts
   307       val _ = check ctxt fixes ts
   297       val fnames = map (fst o fst) fixes
   308       val fnames = map (fst o fst) fixes
   298       val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
   309       val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
   299 
   310 
   300       fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs)
   311       fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
       
   312                                    (indices ~~ xs)
   301                         |> map (map snd)
   313                         |> map (map snd)
   302 
   314 
   303       (* using theorem names for case name currently disabled *)
   315       (* using theorem names for case name currently disabled *)
   304       val cnames = map_index (fn (i, (n,_)) => mk_case_names i "" 1) nas |> flat
   316       val cnames = map_index (fn (i, (n,_)) => mk_case_names i "" 1) nas |> flat
   305     in
   317     in
   320 
   332 
   321 
   333 
   322 local 
   334 local 
   323   structure P = OuterParse and K = OuterKeyword
   335   structure P = OuterParse and K = OuterKeyword
   324 
   336 
   325   val option_parser = (P.reserved "sequential" >> K Sequential)
   337   val option_parser = 
   326                    || ((P.reserved "default" |-- P.term) >> Default)
   338       P.group "option" ((P.reserved "sequential" >> K Sequential)
   327                    || (P.reserved "domintros" >> K DomIntros)
   339                     || ((P.reserved "default" |-- P.term) >> Default)
   328                    || (P.reserved "tailrec" >> K Tailrec)
   340                     || (P.reserved "domintros" >> K DomIntros)
   329 
   341                     || (P.reserved "tailrec" >> K Tailrec))
   330   fun config_parser default = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") [])
   342 
   331                               >> (fn opts => fold apply_opt opts default)
   343   fun config_parser default = 
       
   344       (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
       
   345         >> (fn opts => fold apply_opt opts default)
   332 
   346 
   333   val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
   347   val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
   334 
   348 
   335   fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
   349   fun pipe_error t = 
   336 
   350   P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
   337   val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
   351 
   338                      --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
   352   val statement_ow = 
       
   353    SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
       
   354     --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
   339 
   355 
   340   val statements_ow = P.enum1 "|" statement_ow
   356   val statements_ow = P.enum1 "|" statement_ow
   341 
   357 
   342   val flags_statements = statements_ow
   358   val flags_statements = statements_ow
   343                          >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
   359                          >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
   344 in
   360 in
   345   fun fundef_parser default_cfg = (config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements)
   361   fun fundef_parser default_cfg = 
       
   362       config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements
   346 end
   363 end
   347 
   364 
   348 
   365 
   349 end
   366 end
   350 end
   367 end