1 theory FistStep

     2 imports Main

     3 begin

     4 

     5 ML {*

     6 val pretty_term = Syntax.pretty_term

     7 val pwriteln = Pretty.writeln

     8 fun pretty_terms ctxt trms =

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

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

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

    12 fun pretty_cterm ctxt ctrm =

    13   pretty_term ctxt (term_of ctrm)

    14 fun pretty_thm ctxt thm =

    15   pretty_term ctxt (prop_of thm)

    16 fun pretty_thm_no_vars ctxt thm =

    17 let

    18   val ctxt' = Config.put show_question_marks false ctxt

    19 in

    20   pretty_term ctxt' (prop_of thm)

    21 end

    22 fun pretty_thms ctxt thms =

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

    24 fun pretty_thms_no_vars ctxt thms =

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

    26 fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty

    27 fun pretty_typs ctxt tys =

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

    29 fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)

    30 fun pretty_ctyps ctxt ctys =

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

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

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

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

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

    36 *}

    37 

    38 ML {*

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

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

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

    42   *}

    43 

    44 ML {*

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

    46 *}

    47 

    48 ML {*

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

    50 *}

    51 

    52 ML {*

    53   fun apply_fresh_args f ctxt =

    54       f |> fastype_of

    55         |> binder_types

    56         |> map (pair "z")

    57         |> Variable.variant_frees ctxt [f]

    58         |> map Free

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

    60         |> curry list_comb f

    61 *}

    62 

    63 ML {*

    64 let

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

    66    val ctxt = ML_Context.the_local_context ()

    67 in

    68    apply_fresh_args trm ctxt

    69     |> pretty_term ctxt

    70     |> pwriteln

    71 end

    72 *}

    73 

    74 ML {*

    75   fun inc_by_three x =

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

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

    78         |> (fn x => x + 2)

    79 *}

    80 

    81 ML {*

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

    83 *}

    84 

    85 ML {*

    86   fun inc_as_pair x =

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

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

    89 *}

    90 

    91 ML {*

    92   3 |> inc_as_pair

    93 *}

    94 

    95 ML {*

    96   fun acc_incs x =

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

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

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

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

   101 *}

   102 

   103 ML {*

   104   2 |> acc_incs

   105 *}

   106 

   107 ML {*

   108 let

   109   val ((names1, names2), _) =

   110     @{context}

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

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

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

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

   115 in

   116   (names1, names2)

   117 end

   118 *}

   119 

   120 ML {*

   121   @{context}

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

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

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

   125 *}

   126 

   127 ML {*

   128 let

   129    val ctxt = @{context}

   130 in

   131    Syntax.parse_term ctxt "m + n"

   132    |> singleton (Syntax.check_terms ctxt)

   133    |> pretty_term ctxt

   134    |> pwriteln

   135 end

   136 *}

   137 

   138 ML {*

   139   val term_pat_setup =

   140   let

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

   142       fun term_pat (ctxt, str) =

   143          str |> Proof_Context.read_term_pattern ctxt

   144              |> ML_Syntax.print_term

   145              |> ML_Syntax.atomic

   146    in

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

   148    end

   149 *}

   150 

   151 setup {* term_pat_setup *}

   152 

   153 

   154 ML {*

   155 val type_pat_setup =

   156 let

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

   158    fun typ_pat (ctxt, str) =

   159      let

   160        val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt

   161      in

   162        str |> Syntax.read_typ ctxt'

   163            |> ML_Syntax.print_typ

   164            |> ML_Syntax.atomic

   165        end

   166 in

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

   168 end

   169 *}

   170 

   171 setup {* type_pat_setup *}

   172 

   173 end