cakeml/candle/standard/ml_kernel/ppKernelScript.sml at master · ericlp/cakeml · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
(*
  Pretty prints the CakeML code of the Candle kernel.
  The output is produced in a file called kernel_ml.txt.
*)
open HolKernel boolLib bossLib
open ml_translatorLib ml_monad_translatorTheory ml_hol_kernelProgTheory astPP

val _ = new_theory"ppKernel"

val pat = ``Dmod "Kernel" _``
val decls = ml_hol_kernelProgTheory.candle_code_def |> concl |> rand
            |> find_term (can (match_term pat)) |> rand

fun equalityprinter _ _ sysp _ gs d t =
  let
    fun sys g d = sysp {gravs=g,depth=d,binderp=false}
    val (_,ls) = dest_comb t
    val ([l,r],_) = listSyntax.dest_list ls
  in
    sys gs d ``App Opapp [App Opapp [Var(Short"=");^l];^r]``
  end
val _ = add_astPP("equalityprinter",``App Equality [x;y]``,equalityprinter)

fun refprinter _ _ sysp _ gs d t =
  let
    fun sys g d = sysp {gravs=g,depth=d,binderp=false}
    val (_,ls) = dest_comb t
    val ([a],_) = listSyntax.dest_list ls
  in
    sys gs d ``App Opapp [Var(Short"ref");^a]``
  end
val _ = add_astPP("refprinter",``App Opref [x]``,refprinter)

fun assignprinter _ _ sysp _ gs d t =
  let
    fun sys g d = sysp {gravs=g,depth=d,binderp=false}
    val (_,ls) = dest_comb t
    val ([l,r],_) = listSyntax.dest_list ls
  in
    sys gs d ``App Opapp [App Opapp [Var(Short":=");^l];^r]``
  end
val _ = add_astPP("assignprinter",``App Opassign [x;y]``,assignprinter)

fun derefprinter _ _ sysp _ gs d t =
  let
    fun sys g d = sysp {gravs=g,depth=d,binderp=false}
    val (_,ls) = dest_comb t
    val ([a],_) = listSyntax.dest_list ls
  in
    sys gs d ``App Opapp [Var(Short"!");^a]``
  end
val _ = add_astPP("derefprinter",``App Opderef [x]``,derefprinter)

fun plusprinter _ _ sysp _ gs d t =
  let
    fun sys g d = sysp {gravs=g,depth=d,binderp=false}
    val (_,ls) = dest_comb t
    val ([l,r],_) = listSyntax.dest_list ls
  in
    sys gs d ``App Opapp [App Opapp [Var(Short"+");^l];^r]``
  end
val _ = add_astPP("plusprinter",``App (Opn Plus) [x;y]``,plusprinter)

fun implodeprinter _ _ sysp _ gs d t =
  let
    fun sys g d = sysp {gravs=g,depth=d,binderp=false}
    val (_,ls) = dest_comb t
    val ([a],_) = listSyntax.dest_list ls
  in
    sys gs d ``App Opapp [Var(Long"String" (Short "implode"));^a]``
  end
val _ = add_astPP("implodeprinter",``App Implode [x]``,implodeprinter)

fun explodeprinter _ _ sysp _ gs d t =
  let
    fun sys g d = sysp {gravs=g,depth=d,binderp=false}
    val (_,ls) = dest_comb t
    val ([a],_) = listSyntax.dest_list ls
  in
    sys gs d ``App Opapp [Var(Long"String" (Short "explode"));^a]``
  end
val _ = add_astPP("explodeprinter",``App Explode [x]``,explodeprinter)

fun chltprinter _ _ sysp _ gs d t =
  let
    fun sys g d = sysp {gravs=g,depth=d,binderp=false}
    val (_,ls) = dest_comb t
    val ([l,r],_) = listSyntax.dest_list ls
  in
    sys gs d ``App Opapp [App Opapp [Var(Short"<");^l];^r]``
  end
val _ = add_astPP("chltprinter",``App (Chopb Lt) [x;y]``,chltprinter)

val _ = enable_astPP()

val _ = set_trace "pp_avoids_symbol_merges" 0

val f = TextIO.openOut("kernel_ml.txt")

fun appthis tm = let
  val () = TextIO.output(f,term_to_string tm)
  val () = TextIO.output(f,"\n")
in () end

val _ = app appthis (fst(listSyntax.dest_list decls))

val _ = TextIO.closeOut f

val _ = disable_astPP()

val _ = export_theory()