theory Scratch
imports
  Pure
begin


ML \<open>
(*collect and normalise TVars of a term*)
fun collect_norm_types ctxt tyenv t =
  let
    val norm_type = Envir.norm_type tyenv
    fun prep_type_entry x = (x, Thm.ctyp_of ctxt (norm_type (TVar x)))
  in
    fold_types (fold_atyps (fn (TVar v) => TVars.add (prep_type_entry v) | _ => I)) t
    |> TVars.build
  end

(*collect and normalise Vars of a term*)
fun collect_norm_terms ctxt (env as Envir.Envir {tyenv,...}) t =
  let
    val norm_type = Envir.norm_type tyenv
    val norm_term = Envir.norm_term env
    fun prep_term_entry (x as (n, T)) = ((n, norm_type T), Thm.cterm_of ctxt (norm_term (Var x)))
  in
    fold_aterms (fn (Var v) => Vars.add (prep_term_entry v) | _ => I) t
    |> Vars.build
  end

(*normalise types of a theorem*)
fun norm_thm_types ctxt tyenv thm =
  let 
    val prop = Thm.prop_of thm
    val type_inst = collect_norm_types ctxt tyenv prop
    val inst = (type_inst, Vars.empty)
  in Thm.instantiate inst thm end

(*normalise a theorem*)
fun norm_thm ctxt (env as Envir.Envir {tyenv,...}) thm =
  let 
    val prop = Thm.prop_of thm
    val type_inst = collect_norm_types ctxt tyenv prop
    val term_inst = collect_norm_terms ctxt env prop
    val inst = (type_inst, term_inst)
  in Thm.instantiate inst thm end

(*wrong normalisation of a theorem; this does not work, for example with environments in triangular
form or environments where type variables of a term are substituted*)
fun norm_thm_wrong ctxt (Envir.Envir {tyenv, tenv,...}) thm =
  let
    fun add_type_entry (n, (S, T)) = TVars.add ((n, S), Thm.ctyp_of ctxt T)
    fun add_term_entry (n, (T, t)) = Vars.add ((n, T), Thm.cterm_of ctxt t)
    val type_inst = Vartab.fold add_type_entry tyenv |> TVars.build
    val term_inst = Vartab.fold add_term_entry tenv |> Vars.build
    val inst = (type_inst, term_inst)
  in Thm.instantiate inst thm end
\<close>

ML \<open>
  (*just some auxiliary definitions, you can ignore this*)
  (* pretty-printing *)
  local
  val pretty_term = Syntax.pretty_term
  val pretty_type = Syntax.pretty_typ
  
  fun pretty_env_aux show_entry =
    Vartab.dest
    #> map show_entry
    #> Pretty.list "[" "]"
  
  fun pretty_env_entry show (s, t) = Pretty.enum " := " "" "" (map show [s, t])
  in
  
  fun pretty_tyenv ctxt =
    let
      val show_entry = pretty_env_entry (pretty_type ctxt)
      fun get_typs (v, (s, T)) = (TVar (v, s), T)
    in pretty_env_aux (show_entry o get_typs) end
  
  fun pretty_tenv ctxt =
    let
      val show_entry = pretty_env_entry (pretty_term ctxt)
      fun get_trms (v, (T, t)) = (Var (v, T), t)
    in pretty_env_aux (show_entry o get_trms) end
  
  end
  
  fun pretty_env ctxt env = Pretty.enum "," "(" ")" [
      pretty_tyenv ctxt (Envir.type_env env),
      pretty_tenv ctxt (Envir.term_env env)
    ]

  (* schematic variables in antiquotation *)
  val _ = Theory.setup (
    ML_Antiquotation.inline_embedded \<^binding>\<open>term_pat\<close>
    (Args.term_pattern >> (ML_Syntax.atomic o ML_Syntax.print_term)))
\<close>

declare [[show_types]]

ML \<open>
  val s = @{term_pat "\<lambda> (x :: ?'Y). (?z ::  ?'Y \<Rightarrow> ?'R) x"}
  val t = @{term_pat "\<lambda> (x :: ?'X). (c :: ?'X \<Rightarrow> ?'R) x"}
  (*another example that would fail for a diffferent reason*)
  (*val s = @{term_pat "f (\<lambda> (x :: ?'Y). ?z ::  ?'X)"}*)
  (*val t = @{term_pat "f (\<lambda> (x :: ?'X). (c :: ?'V))"}*)
  val ctxt = @{context}
  val env = Pattern.unify (Context.Proof ctxt) (s, t) (Envir.empty 0)
    |> tap (pretty_env ctxt #> Pretty.writeln)
  val thm = norm_thm @{context} env (Thm.reflexive (Thm.cterm_of ctxt s))
  (*this call fails*)
  (*val thm' = norm_thm_wrong @{context} env (Thm.reflexive (Thm.cterm_of ctxt s))*)
\<close>

end