--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/progtut/FirstStep.thy~	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,173 @@
+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
\ No newline at end of file