src/HOL/Tools/function_package/fundef_common.ML

local open FundefLib;

(*  Title:      HOL/Tools/function_package/fundef_common.ML
    ID:         $Id$
    Author:     Alexander Krauss, TU Muenchen

A package for general recursive function definitions. 
Common definitions and other infrastructure.
*)

structure FundefCommon =
struct

local open FundefLib in

(* Profiling *)
val profile = ref false;

fun PROFILE msg = if !profile then timeap_msg msg else I


val acc_const_name = "Accessible_Part.acc"
fun mk_acc domT R =
    Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 

val function_name = suffix "C"
val graph_name = suffix "_graph"
val rel_name = suffix "_rel"
val dom_name = suffix "_dom"

type depgraph = int IntGraph.T

datatype ctx_tree 
  = Leaf of term
  | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
  | RCall of (term * ctx_tree)



datatype fundef_result =
  FundefResult of
     {
      fs: term list,
      G: term,
      R: term,

      psimps : thm list, 
      trsimps : thm list option, 

      subset_pinducts : thm list, 
      simple_pinducts : thm list, 
      cases : thm,
      termination : thm,
      domintros : thm list option
     }


datatype fundef_context_data =
  FundefCtxData of
     {
      defname : string,

      add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory,

      fs : term list,
      R : term,
      
      psimps: thm list,
      pinducts: thm list,
      termination: thm
     }

fun morph_fundef_data phi (FundefCtxData {add_simps, fs, R, psimps, pinducts, termination, defname}) =
    let
      val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
      val name = Morphism.name phi
    in
      FundefCtxData { add_simps = add_simps (* contains no logical entities *), 
                      fs = map term fs, R = term R, psimps = fact psimps, 
                      pinducts = fact pinducts, termination = thm termination,
                      defname = name defname }
    end

structure FundefData = GenericDataFun
(
  type T = (term * fundef_context_data) NetRules.T;
  val empty = NetRules.init
    (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool)
    fst;
  val copy = I;
  val extend = I;
  fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
);


structure FundefCongs = GenericDataFun
(
  type T = thm list
  val empty = []
  val extend = I
  fun merge _ = Drule.merge_rules
);


(* Generally useful?? *)
fun lift_morphism thy f = 
    let 
      val term = Drule.term_rule thy f
    in
      Morphism.thm_morphism f $> Morphism.term_morphism term $> Morphism.typ_morphism (Logic.type_map term)
    end

fun import_fundef_data t ctxt =
    let
      val thy = Context.theory_of ctxt
      val ct = cterm_of thy t
      val inst_morph = lift_morphism thy o Thm.instantiate 

      fun match data = 
          SOME (morph_fundef_data (inst_morph (Thm.match (cterm_of thy (fst data), ct))) (snd data))
          handle Pattern.MATCH => NONE
    in 
      get_first match (NetRules.retrieve (FundefData.get ctxt) t)
    end

fun import_last_fundef ctxt =
    case NetRules.rules (FundefData.get ctxt) of
      [] => NONE
    | (t, data) :: _ =>
      let 
        val ([t'], ctxt') = Variable.import_terms true [t] (Context.proof_of ctxt)
      in
        import_fundef_data t' (Context.Proof ctxt')
      end

val all_fundef_data = NetRules.rules o FundefData.get

val map_fundef_congs = FundefCongs.map 
val get_fundef_congs = FundefCongs.get



structure TerminationRule = GenericDataFun
(
  type T = thm list
  val empty = []
  val extend = I
  fun merge _ = Drule.merge_rules
);

val get_termination_rules = TerminationRule.get
val store_termination_rule = TerminationRule.map o cons
val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof

fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) =
    FundefData.map (fold (fn f => NetRules.insert (f, data)) fs)
    #> store_termination_rule termination


(* Configuration management *)
datatype fundef_opt 
  = Sequential
  | Default of string
  | Target of xstring
  | DomIntros
  | Tailrec

datatype fundef_config
  = FundefConfig of
   {
    sequential: bool,
    default: string,
    target: xstring option,
    domintros: bool,
    tailrec: bool
   }

fun apply_opt Sequential (FundefConfig {sequential, default, target, domintros,tailrec}) = 
    FundefConfig {sequential=true, default=default, target=target, domintros=domintros, tailrec=tailrec}
  | apply_opt (Default d) (FundefConfig {sequential, default, target, domintros,tailrec}) = 
    FundefConfig {sequential=sequential, default=d, target=target, domintros=domintros, tailrec=tailrec}
  | apply_opt (Target t) (FundefConfig {sequential, default, target, domintros,tailrec}) =
    FundefConfig {sequential=sequential, default=default, target=SOME t, domintros=domintros, tailrec=tailrec}
  | apply_opt DomIntros (FundefConfig {sequential, default, target, domintros,tailrec}) =
    FundefConfig {sequential=sequential, default=default, target=target, domintros=true,tailrec=tailrec}
  | apply_opt Tailrec (FundefConfig {sequential, default, target, domintros,tailrec}) =
    FundefConfig {sequential=sequential, default=default, target=target, domintros=domintros,tailrec=true}

fun target_of (FundefConfig {target, ...}) = target

(* Common operations on equations *)

fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
  | open_all_all t = ([], t)

exception MalformedEquation of term

fun split_def geq =
    let
      val (qs, imp) = open_all_all geq

      val gs = Logic.strip_imp_prems imp
      val eq = Logic.strip_imp_concl imp

      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
          handle TERM _ => raise MalformedEquation geq

      val (head, args) = strip_comb f_args

      val fname = fst (dest_Free head)
          handle TERM _ => raise MalformedEquation geq
    in
      (fname, qs, gs, args, rhs)
    end

exception ArgumentCount of string

fun mk_arities fqgars =
    let fun f (fname, _, _, args, _) arities =
            let val k = length args
            in
              case Symtab.lookup arities fname of
                NONE => Symtab.update (fname, k) arities
              | SOME i => (if i = k then arities else raise ArgumentCount fname)
            end
    in
      fold f fqgars Symtab.empty
    end


(* Check for all sorts of errors in the input *)
fun check_defs ctxt fixes eqs =
    let
      val fnames = map (fst o fst) fixes
                                
      fun check geq = 
          let
            fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
                                  
            val fqgar as (fname, qs, gs, args, rhs) = split_def geq
                                 
            val _ = fname mem fnames 
                    orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames 
                                               ^ commas_quote fnames))
                                            
            fun add_bvs t is = add_loose_bnos (t, 0, is)
            val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
                        |> map (fst o nth (rev qs))
                      
            val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
                                                        ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
                                    
            val _ = forall (FundefLib.forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs 
                    orelse error (input_error "Recursive Calls not allowed in premises")
          in
            fqgar
          end

      val _ = mk_arities (map check eqs)
          handle ArgumentCount fname => 
                 error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
    in
      ()
    end

(* Preprocessors *)

type fixes = ((string * typ) * mixfix) list
type 'a spec = ((bstring * Attrib.src list) * 'a list) list
type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec -> (term list * (thm list -> thm spec))

fun empty_preproc check _ _ ctxt fixes spec =
    let 
      val (nas,tss) = split_list spec
      val _ = check ctxt fixes (flat tss)
    in
      (flat tss, curry op ~~ nas o Library.unflat tss)
    end

structure Preprocessor = GenericDataFun
(
  type T = preproc
  val empty : T = empty_preproc check_defs
  val extend = I
  fun merge _ (a, _) = a
);

val get_preproc = Preprocessor.get o Context.Proof
val set_preproc = Preprocessor.map o K



local 
  structure P = OuterParse and K = OuterKeyword 

  val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
                       
  val option_parser = (P.$$$ "sequential" >> K Sequential)
                   || ((P.reserved "default" |-- P.term) >> Default)
                   || (P.reserved "domintros" >> K DomIntros)
                   || (P.reserved "tailrec" >> K Tailrec)
                   || ((P.$$$ "in" |-- P.xname) >> Target)

  fun config_parser default = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") [])
                              >> (fn opts => fold apply_opt opts default)

  val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"

  fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))

  val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
                     --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))

  val statements_ow = P.enum1 "|" statement_ow

  val flags_statements = statements_ow
                         >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))

  fun basic_apply_flags ((config, fixes), (flags, statements)) = ((config, fixes), statements)
in
  fun fundef_parser default_cfg = (config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements)
                                  
end





val default_config = FundefConfig { sequential=false, default="%x. arbitrary", 
                                    target=NONE, domintros=false, tailrec=false }


end
end

(* Common Abbreviations *)

structure FundefAbbrev =
struct

fun implies_elim_swp x y = implies_elim y x

(* HOL abbreviations *)
val boolT = HOLogic.boolT
val mk_prod = HOLogic.mk_prod
val mk_eq = HOLogic.mk_eq
val eq_const = HOLogic.eq_const
val Trueprop = HOLogic.mk_Trueprop
val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT

fun free_to_var (Free (v,T)) = Var ((v,0),T)
  | free_to_var _ = raise Match

fun var_to_free (Var ((v,_),T)) = Free (v,T)
  | var_to_free _ = raise Match


end