theory FistStep

imports Main

begin

ML {*

val pretty_term = Syntax.pretty_term

val pwriteln = Pretty.writeln

fun pretty_terms ctxt trms =

  Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))

val show_type_ctxt = Config.put show_types true @{context}

val show_all_types_ctxt = Config.put show_all_types true @{context}

fun pretty_cterm ctxt ctrm =

  pretty_term ctxt (term_of ctrm)

fun pretty_thm ctxt thm =

  pretty_term ctxt (prop_of thm)

fun pretty_thm_no_vars ctxt thm =

let

  val ctxt' = Config.put show_question_marks false ctxt

in

  pretty_term ctxt' (prop_of thm)

end

fun pretty_thms ctxt thms =

  Pretty.block (Pretty.commas (map (pretty_thm ctxt) thms))

fun pretty_thms_no_vars ctxt thms =

  Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))

fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty

fun pretty_typs ctxt tys =

  Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))

fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)

fun pretty_ctyps ctxt ctys =

  Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))

fun `f = fn x => (f x, x)

fun (x, y) |>> f = (f x, y)

fun (x, y) ||> f = (x, f y)

fun (x, y) |-> f = f x y

*}

ML {*

  val _ = pretty_term @{context} @{term "x + y + z"} |> pwriteln

  val _ = pretty_terms @{context} [@{term "x + y"}, @{term "x + y + z"}] |> pwriteln

  val show_type_ctxt = Config.put show_types true @{context}

  *}

ML {*

   pwriteln (pretty_term show_type_ctxt @{term "(1::nat, x)"})

*}

ML {*

pwriteln (Pretty.str (cat_lines ["foo", "bar"]))

*}

ML {*

  fun apply_fresh_args f ctxt =

      f |> fastype_of

        |> binder_types

        |> map (pair "z")

        |> Variable.variant_frees ctxt [f]

        |> map Free

        |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))

        |> curry list_comb f

*}

ML {*

let

   val trm = @{term "P::nat => int => unit => bool"}

   val ctxt = ML_Context.the_local_context ()

in

   apply_fresh_args trm ctxt

    |> pretty_term ctxt

    |> pwriteln

end

*}

ML {*

  fun inc_by_three x =

      x |> (fn x => x + 1)

        |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))

        |> (fn x => x + 2)

*}

ML {*

  fun `f = fn x => (f x, x)

*}

ML {*

  fun inc_as_pair x =

        x |> `(fn x => x + 1)

       |> (fn (x, y) => (x, y + 1))

*}

ML {*

  3 |> inc_as_pair

*}

ML {*

  fun acc_incs x =

      x |> (fn x => (0, x))

        ||>> (fn x => (x, x + 1))

        ||>> (fn x => (x, x + 1))

        ||>> (fn x => (x, x + 1))

*}

ML {*

  2 |> acc_incs

*}

ML {*

let

  val ((names1, names2), _) =

    @{context}

    |> Variable.variant_fixes (replicate 4 "x")

    |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))

    ||>> Variable.variant_fixes (replicate 5 "x")

    |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))

in

  (names1, names2)

end

*}

ML {*

  @{context}

  |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"})

  ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})

  ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})

*}

ML {*

let

   val ctxt = @{context}

in

   Syntax.parse_term ctxt "m + n"

   |> singleton (Syntax.check_terms ctxt)

   |> pretty_term ctxt

   |> pwriteln

end

*}

ML {*

  val term_pat_setup =

  let

    val parser = Args.context -- Scan.lift Args.name_source

      fun term_pat (ctxt, str) =

         str |> Proof_Context.read_term_pattern ctxt

             |> ML_Syntax.print_term

             |> ML_Syntax.atomic

   in

      ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat)

   end

*}

setup {* term_pat_setup *}

ML {*

val type_pat_setup =

let

   val parser = Args.context -- Scan.lift Args.name_source

   fun typ_pat (ctxt, str) =

     let

       val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt

     in

       str |> Syntax.read_typ ctxt'

           |> ML_Syntax.print_typ

           |> ML_Syntax.atomic

       end

in

   ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat)

end

*}

setup {* type_pat_setup *}

end