Source file entry.ml
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
open Kernel
open Basic
open Term
type is_opaque = bool
type is_assertion = bool
type should_fail = bool
type test = Convert of term * term | HasType of term * term
exception Assert_error of loc
type entry =
| Decl of loc * ident * Signature.scope * Signature.staticity * term
| Def of loc * ident * Signature.scope * is_opaque * term option * term
| Rules of loc * Rule.partially_typed_rule list
| Eval of loc * Reduction.red_cfg * term
| Check of loc * is_assertion * should_fail * test
| Infer of loc * Reduction.red_cfg * term
| Print of loc * string
| DTree of loc * mident option * ident
| Name of loc * mident
| Require of loc * mident
let pp_entry fmt e =
let open Format in
let scope_to_string = function
| Signature.Public -> ""
| Signature.Private -> "private "
in
match e with
| Decl (_, id, scope, Static, ty) ->
fprintf fmt "@[<2>%s%a :@ %a.@]@.@." (scope_to_string scope) pp_ident id
pp_term ty
| Decl (_, id, scope, Definable Free, ty) ->
fprintf fmt "@[<2>%sdef %a :@ %a.@]@.@." (scope_to_string scope) pp_ident
id pp_term ty
| Decl (_, id, scope, Injective, ty) ->
fprintf fmt "@[<2>%sinjective %a :@ %a.@]@.@." (scope_to_string scope)
pp_ident id pp_term ty
| Decl (_, id, scope, Definable AC, ty) ->
fprintf fmt "@[<2>%sdefac %a [@ %a].@]@.@." (scope_to_string scope)
pp_ident id pp_term ty
| Decl (_, id, scope, Definable (ACU neu), ty) ->
fprintf fmt "@[<2>%sdefacu %a [@ %a, %a].@]@.@." (scope_to_string scope)
pp_ident id pp_term ty pp_term neu
| Def (_, id, scope, opaque, ty, te) -> (
let key = if opaque then "thm" else "def" in
match ty with
| None ->
fprintf fmt "@[<hv2>%s%s %a@ :=@ %a.@]@.@." (scope_to_string scope)
key pp_ident id pp_term te
| Some ty ->
fprintf fmt "@[<hv2>%s%s %a :@ %a@ :=@ %a.@]@.@."
(scope_to_string scope) key pp_ident id pp_term ty pp_term te)
| Rules (_, rs) ->
fprintf fmt "@[<v0>%a@].@.@." (pp_list "" Rule.pp_part_typed_rule) rs
| Eval (_, cfg, te) ->
fprintf fmt "#EVAL%a %a.@." Reduction.pp_red_cfg cfg pp_term te
| Infer (_, cfg, te) ->
fprintf fmt "#INFER%a %a.@." Reduction.pp_red_cfg cfg pp_term te
| Check (_, assrt, neg, test) -> (
let cmd = if assrt then "#ASSERT" else "#CHECK" in
let neg = if neg then "NOT" else "" in
match test with
| Convert (t1, t2) ->
fprintf fmt "%s%s %a ==@ %a.@." cmd neg pp_term t1 pp_term t2
| HasType (te, ty) ->
fprintf fmt "%s%s %a ::@ %a.@." cmd neg pp_term te pp_term ty)
| DTree (_, m, v) -> (
match m with
| None -> fprintf fmt "#GDT %a.@." pp_ident v
| Some m -> fprintf fmt "#GDT %a.%a.@." pp_mident m pp_ident v)
| Print (_, str) -> fprintf fmt "#PRINT %S.@." str
| Name (_, _) -> ()
| Require (_, md) -> fprintf fmt "#REQUIRE %a.@." pp_mident md
let loc_of_entry = function
| Decl (lc, _, _, _, _)
| Def (lc, _, _, _, _, _)
| Rules (lc, _)
| Eval (lc, _, _)
| Infer (lc, _, _)
| Check (lc, _, _, _)
| DTree (lc, _, _)
| Print (lc, _)
| Name (lc, _)
| Require (lc, _) ->
lc