coq_printer.ml 4.05 KB
Newer Older
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
1
2
3
4
open Parsetree
open Scoper
open Typer

5
let print_id out_fmter (Id i) = Format.fprintf out_fmter "_%s" i
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
6
7
8
9
10
11
12
13
14
15
let print_cid out_fmter (Cid c) = Format.fprintf out_fmter "%s" c
let print_label out_fmter (Label l) = Format.fprintf out_fmter "\"%s\"" l

let rec print_ty out_fmter = function
  | Stcid (c, _) -> print_cid out_fmter c
  | Stlist [] -> Format.fprintf out_fmter "Empty_type"
  | Stlist ll ->
     Format.fprintf out_fmter "[@[<hov>%a@]]"
       print_ty_elems ll
  | Starr (ty1, ty2) ->
16
17
18
     Format.fprintf out_fmter "@[<hov>%a@ →@ %a@]"
       print_par_ty ty1
       print_par_ty ty2
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
19
  | Stbool ty ->
20
     Format.fprintf out_fmter "@[<hov>BoolT@ %a@]"
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
21
22
23
24
       print_par_ty ty
and print_ty_elem out_fmter (l, ty) =
  Format.fprintf out_fmter "@[<hov>%a :@ %a@]"
    print_label l
25
    print_par_ty ty
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
26
27
28
29
30
31
32
33
34
35
and print_ty_elems out_fmter = function
  | [] -> ()
  | [ el ] -> print_ty_elem out_fmter el
  | el :: els ->
     Format.fprintf out_fmter "%a;@ %a"
       print_ty_elem el
       print_ty_elems els
and print_par_ty out_fmter = function
  | Stcid _ | Stlist _ as ty -> print_ty out_fmter ty
  | ty ->
36
37
     Format.fprintf out_fmter "(%a)"
       print_ty ty
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
38
39
40
41
42

let rec print_term out_fmter : tterm -> unit = function
  | Tvar (id, _)
  | Tconst (id, _, _) -> print_id out_fmter id
  | Tpar t ->
43
44
     Format.fprintf out_fmter "(%a)"
       print_term t
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
45
  | Tapp (t1, t2, _, _) ->
46
47
48
     Format.fprintf out_fmter "@[<hov>%a@ @@@ %a@]"
       print_par_term t1
       print_par_term t2
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
49
  | Tabst (x, ty, body, _) ->
50
51
52
53
     Format.fprintf out_fmter "@[<hov>λ(%a !:@ %a) %a@]"
       print_id x
       print_ty ty
       print_par_term body
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
54
  | Ttrue ty ->
55
     Format.fprintf out_fmter "@[<hov>trueT@ %a@]"
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
56
57
       print_par_ty ty
  | Tfalse ty ->
58
     Format.fprintf out_fmter "@[<hov>falseT@ %a@]"
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
59
60
       print_par_ty ty
  | Tif (b, t, e, _) ->
61
     Format.fprintf out_fmter "@[<hov>ifT@ %a@ then@ %a@ else@ %a@]"
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
62
63
64
       print_term b
       print_term t
       print_par_term e
65
66
67
  | Tobj (ll, ty) ->
     Format.fprintf out_fmter "@[<hov>%a@]"
       (print_obj_elems ty) ll
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
68
  | Tsel (t, l, _) ->
69
70
71
     Format.fprintf out_fmter "@[<hov>%a#%a@]"
       print_par_term t
       print_label l
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
72
  | Tupd (t, l, m, _) ->
73
74
75
76
     Format.fprintf out_fmter "@[<hov>%a##%a@ ⇐ %a@]"
       print_par_term t
       print_label l
       print_meth m
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
77
  | Tcast (t, ty1, ty2) ->
78
     Format.fprintf out_fmter "@[<hov>Ecoerce@ %a@ %a@ %a@ (subtype_dec_correct@ %a@ %a@ Istrue_true)@]"
79
       print_par_ty ty2
80
       print_par_ty ty1
81
       print_par_term t
82
83
       print_par_ty ty1
       print_par_ty ty2
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
84
85
86
and print_par_term out_fmter = function
  | Tvar _ | Tconst _ | Tpar _ | Tobj _ as t -> print_term out_fmter t
  | t ->
87
88
     Format.fprintf out_fmter "(%a)"
       print_term t
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
89
and print_obj_elem out_fmter (l, m) =
90
  Format.fprintf out_fmter "(@[<hov>%a =@ %a@])%%meth"
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
91
92
    print_label l
    print_meth m
93
94
95
96
and print_obj_elems ty out_fmter = function
  | [] ->
     Format.fprintf out_fmter "(init@ %a@ Istrue_true)"
       print_par_ty ty
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
97
  | el :: els ->
98
     Format.fprintf out_fmter "(pocons_3@ %a@ %a)"
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
99
       print_obj_elem el
100
       (print_obj_elems ty) els
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
101
102
103
104
105
106
and print_meth out_fmter (Tmeth (x, ty, body, _)) =
  Format.fprintf out_fmter "@[<h>ς(%a !: %a)%a@]"
    print_id x
    print_ty ty
    print_par_term body

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
107
let rec print_line out_fmter = function
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
108
  | Ttypedef (cid, ty) ->
109
110
111
     Format.fprintf out_fmter "@[<h>Definition %a :=@ %a%%ty.@]@\n"
       print_cid cid
       print_par_ty ty
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
112
  | Tvardef (id, ty, def) ->
113
     Format.fprintf out_fmter "@[<h>Definition %a :@ Expr %a :=@ %a%%obj.@]@\n"
114
115
116
       print_id id
       print_par_ty ty
       print_par_term def
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
117
  | Tcheck (t, ty) ->
118
     Format.fprintf out_fmter "@[<h>Goal Expr %a@].
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
119
120
Proof.
exact %a%%obj.
121
122
Qed.
"
123
124
125
126
127
     print_par_ty ty
     print_par_term t
  | Tconv (t1, t2, ty) ->
     print_line out_fmter (Tcheck (t1, ty));
    print_line out_fmter (Tcheck (t2, ty))
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
128
  | Tnorm t ->
129
130
     Format.fprintf out_fmter "@[<h>Eval Compute %a%%obj.@]@\n"
       print_par_term t
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
131
132
133
134
  | Tprint s ->
     Format.fprintf out_fmter "(* \"%s\" *)@\n" s

let print out_fmter = List.iter (print_line out_fmter)