theory FirstStep
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