src/HOL/Real_Asymp/lazy_eval.ML

tuned document;

signature LAZY_EVAL = sig

datatype pat = AnyPat of indexname | ConsPat of (string * pat list)

type constructor = string * int

type equation = {
    function : term, 
    thm : thm, 
    rhs : term, 
    pats : pat list
  }

type eval_ctxt' = {
    equations : equation list, 
    constructors : constructor list,
    pctxt : Proof.context, 
    facts : thm Net.net,
    verbose : bool
  }

type eval_hook = eval_ctxt' -> term -> (term * conv) option

type eval_ctxt = {
    ctxt : eval_ctxt', 
    hooks : eval_hook list
  }

val is_constructor_name : constructor list -> string -> bool
val constructor_arity : constructor list -> string -> int option

val mk_eval_ctxt : Proof.context -> constructor list -> thm list -> eval_ctxt
val add_facts : thm list -> eval_ctxt -> eval_ctxt
val get_facts : eval_ctxt -> thm list
val get_ctxt : eval_ctxt -> Proof.context
val add_hook : eval_hook -> eval_ctxt -> eval_ctxt
val get_verbose : eval_ctxt -> bool
val set_verbose : bool -> eval_ctxt -> eval_ctxt
val get_constructors : eval_ctxt -> constructor list
val set_constructors : constructor list -> eval_ctxt -> eval_ctxt

val whnf : eval_ctxt -> term -> term * conv
val match : eval_ctxt -> pat -> term -> 
  (indexname * term) list option -> (indexname * term) list option * term * conv
val match_all : eval_ctxt -> pat list -> term list -> 
  (indexname * term) list option -> (indexname * term) list option * term list * conv

end

structure Lazy_Eval : LAZY_EVAL = struct

datatype pat = AnyPat of indexname | ConsPat of (string * pat list)

type constructor = string * int

type equation = {
    function : term, 
    thm : thm, 
    rhs : term, 
    pats : pat list
  }

type eval_ctxt' = {
    equations : equation list, 
    constructors : constructor list,
    pctxt : Proof.context, 
    facts : thm Net.net,
    verbose : bool
  }

type eval_hook = eval_ctxt' -> term -> (term * conv) option

type eval_ctxt = {
    ctxt : eval_ctxt', 
    hooks : eval_hook list
  }

fun add_hook h ({hooks, ctxt} : eval_ctxt) = 
  {hooks = h :: hooks, ctxt = ctxt} : eval_ctxt

fun get_verbose {ctxt = {verbose, ...}, ...} = verbose

fun set_verbose b ({ctxt = {equations, pctxt, facts, constructors, ...}, hooks} : eval_ctxt) =
  {ctxt = {equations = equations, pctxt = pctxt, facts = facts, 
   constructors = constructors, verbose = b}, hooks = hooks}

fun get_constructors ({ctxt = {constructors, ...}, ...} : eval_ctxt) = constructors

fun set_constructors cs ({ctxt = {equations, pctxt, facts, verbose, ...}, hooks} : eval_ctxt) =
  {ctxt = {equations = equations, pctxt = pctxt, facts = facts, 
   verbose = verbose, constructors = cs}, hooks = hooks}

type constructor = string * int

val is_constructor_name = member (op = o apsnd fst)

val constructor_arity = AList.lookup op =

fun stream_pat_of_term _ (Var v) = AnyPat (fst v)
  | stream_pat_of_term constructors t =
      case strip_comb t of
        (Const (c, _), args) =>
          (case constructor_arity constructors c of
             NONE => raise TERM ("Not a valid pattern.", [t])
           | SOME n => 
               if length args = n then
                 ConsPat (c, map (stream_pat_of_term constructors) args)
               else
                 raise TERM ("Not a valid pattern.", [t]))
      | _ => raise TERM ("Not a valid pattern.", [t])

fun analyze_eq constructors thm = 
  let
    val ((f, pats), rhs) = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> 
      apfst (strip_comb #> apsnd (map (stream_pat_of_term constructors)))
    handle TERM _ => raise THM ("Not a valid function equation.", 0, [thm])
  in 
    {function = f, thm = thm RS @{thm eq_reflection}, rhs = rhs, pats = pats} : equation
  end

fun mk_eval_ctxt ctxt (constructors : constructor list) thms : eval_ctxt = {
    ctxt = {
        equations = map (analyze_eq constructors) thms, 
        facts = Net.empty, 
        verbose = false,
        pctxt = ctxt,
        constructors = constructors
      }, 
      hooks = []
    }

fun add_facts facts' {ctxt = {equations, pctxt, facts, verbose, constructors}, hooks} =
  let
    val eq = op = o apply2 Thm.prop_of
    val facts' = 
      fold (fn thm => fn net => Net.insert_term eq (Thm.prop_of thm, thm) net
        handle Net.INSERT => net) facts' facts
  in
    {ctxt = {equations = equations, pctxt = pctxt, facts = facts', 
       verbose = verbose, constructors = constructors}, 
     hooks = hooks}
  end

val get_facts = Net.content o #facts o #ctxt

val get_ctxt = (#pctxt o #ctxt : eval_ctxt -> Proof.context)

fun find_eqs (eval_ctxt : eval_ctxt) f = 
  let
    fun eq_const (Const (c, _)) (Const (c', _)) = c = c'
      | eq_const _ _ = false
  in
    map_filter (fn eq => if eq_const f (#function eq) then SOME eq else NONE) 
      (#equations (#ctxt eval_ctxt))
  end

datatype ('a, 'b) either = Inl of 'a | Inr of 'b

fun whnf (ctxt : eval_ctxt) t =
      case whnf_aux1 ctxt (Envir.beta_norm t) of
        (t', conv) => 
          if t aconv t' then 
            (t', conv)
          else
            case whnf ctxt t' of
              (t'', conv') => (t'', conv then_conv conv')
  
and whnf_aux1 (ctxt as {hooks, ctxt = ctxt'}) t =
      case get_first (fn h => h ctxt' t) hooks of
        NONE => whnf_aux2 ctxt t
      | SOME (t', conv) => case whnf ctxt t' of (t'', conv') => 
          (t'', conv then_conv conv')
and whnf_aux2 ctxt t =
  let
    val (f, args) = strip_comb t

    fun instantiate table (Var (x, _)) = the (AList.lookup op = table x)
      | instantiate table (s $ t) = instantiate table s $ instantiate table t
      | instantiate _ t = t
    fun apply_eq {thm, rhs, pats, ...} conv args = 
      let
        val (table, args', conv') = match_all ctxt pats args (SOME [])
      in (
        case table of
          SOME _ => (
            let
              val thy = Proof_Context.theory_of (get_ctxt ctxt)
              val t' = list_comb (f, args')
              val lhs = Thm.term_of (Thm.lhs_of thm)
              val env = Pattern.match thy (lhs, t') (Vartab.empty, Vartab.empty)
              val rhs = Thm.term_of (Thm.rhs_of thm)
              val rhs = Envir.subst_term env rhs |> Envir.beta_norm
            in
              Inr (rhs, conv then_conv conv' then_conv Conv.rewr_conv thm)
            end 
              handle Pattern.MATCH => Inl (args', conv then_conv conv'))
        | NONE => Inl (args', conv then_conv conv'))
       end
    
    fun apply_eqs [] args conv = (list_comb (f, args), conv)
      | apply_eqs (eq :: ctxt) args conv =
          (case apply_eq eq conv args of
             Inr res => res
           | Inl (args', conv) => apply_eqs ctxt args' conv)

  in
    case f of
      Const (f', _) => 
        if is_constructor_name (get_constructors ctxt) f' then
          (t, Conv.all_conv)
        else
          apply_eqs (find_eqs ctxt f) args Conv.all_conv
    | _ => (t, Conv.all_conv)
  end
and match_all ctxt pats args table =
  let
    fun match_all' [] [] acc conv table = (table, rev acc, conv)
      | match_all' (_ :: pats) (arg :: args) acc conv NONE =
        match_all' pats args (arg :: acc) (Conv.fun_conv conv) NONE
      | match_all' (pat :: pats) (arg :: args) acc conv (SOME table) =
          let 
            val (table', arg', conv') = match ctxt pat arg (SOME table)
            val conv = Conv.combination_conv conv conv'
            val acc = arg' :: acc
          in
            match_all' pats args acc conv table'
          end
      | match_all' _ _ _ _ _ = raise Match
  in
    if length pats = length args then
      match_all' pats args [] Conv.all_conv table
    else
      (NONE, args, Conv.all_conv)
  end
and match _ _ t NONE = (NONE, t, Conv.all_conv)
  | match _ (AnyPat v) t (SOME table) = (SOME ((v, t) :: table), t, Conv.all_conv)
  | match ctxt (ConsPat (c, pats)) t (SOME table) =
      let 
        val (t', conv) = whnf ctxt t
        val (f, args) = strip_comb t'
      in
        case f of
          Const (c', _) => 
            if c = c' then
              case match_all ctxt pats args (SOME table) of
                (table, args', conv') => (table, list_comb (f, args'), conv then_conv conv')
            else
              (NONE, t', conv)
          | _ => (NONE, t', conv)
      end

end