File ‹hol_term.ML›

val mk_string = HOLogic.mk_string o Class_Graph.mangle
fun mk_name n = @{const Name} $ mk_string n

fun fsetT typ = Type (@{type_name fset}, [typ])
fun fmapT keyT valueT = Type (@{type_name fmap}, [keyT, valueT])

fun mk_fset typ xs =
  let
    fun f x xs = Const (@{const_name finsert}, typ --> fsetT typ --> fsetT typ) $ x $ xs
    val init = Const (@{const_name bot}, fsetT typ)
  in fold f xs init end

fun mk_fmap (keyT, valueT) xs =
  let
    val fmapT = fmapT keyT valueT
    fun f (k, v) xs = Const (@{const_name fmupd}, keyT --> valueT --> fmapT --> fmapT) $ k $ v $ xs
    val init = Const (@{const_name fmempty}, fmapT)
  in fold f xs init end

signature HOL_TERM = sig
  val mk_term: bool -> term -> term
  val mk_eq: term -> term

  val list_comb: term * term list -> term
  val strip_comb: term -> term * term list
end

structure HOL_Term : HOL_TERM = struct

fun list_comb (f, xs) =
  fold (fn x => fn t => @{const App} $ t $ x) xs f

fun strip_comb t =
  let
    fun go (@{const App} $ f $ x) = apsnd (cons f) (go x)
      | go t = (t, [])
  in apsnd rev (go t) end

fun mk_term schematic t =
  let
    fun aux (Const (n, _)) = @{const Const} $ mk_name n
      | aux (Free (n, _)) =
          if schematic then
            error "free variables are not supported"
          else
            @{const Free} $ mk_name n
      | aux (Bound i) = @{const Bound} $ HOLogic.mk_number @{typ nat} i
      | aux (t $ u) = @{const App} $ aux t $ aux u
      | aux (Abs (_, _, t)) = @{const Abs} $ aux t
      | aux (Var ((n, i), _)) =
          if schematic then
            @{const Free} $ mk_name (n ^ "." ^ Value.print_int i)
          else
            error "schematic variables are not supported"
  in aux t end

val mk_eq =
  HOLogic.mk_prod o @{apply 2} (mk_term true) o Logic.dest_equals

end