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
module W = Ortac_core.Warnings
type W.kind +=
| Ghost_value of string
| Ghost_type of string
| Function_without_definition of string
| Predicate_without_definition of string
| Missing_projection of string
let level = function
| Ghost_value _ | Ghost_type _ | Function_without_definition _
| Predicate_without_definition _ ->
W.Warning
| Missing_projection _ -> W.Error
| kind -> W.level kind
open Fmt
let pp_kind ppf = function
| Ghost_value name ->
pf ppf "%s is a ghost value. It was not translated." name
| Ghost_type name -> pf ppf "%s is a ghost type. It was not translated." name
| Function_without_definition name ->
pf ppf "The function %s has no definition. It was not translated." name
| Predicate_without_definition name ->
pf ppf "The predicate %s has no definition. It was not translated." name
| Missing_projection name ->
pf ppf "The model %s has no projection function. It was not translated."
name
| kind -> W.pp_kind ppf kind
let pp = W.pp_param pp_kind level
open Ir
let term ppf (t : term) = Result.iter_error (W.pp ppf) t.translation
let terms ppf = List.iter (term ppf)
let invariants ppf =
List.iter (fun (i : invariant) -> Result.iter_error (W.pp ppf) i.translation)
let missing_proj ppf = List.iter (pp ppf)
let xpost ppf (xp : xpost) =
Result.iter_error (List.iter (W.pp ppf)) xp.translation
let xposts ppf = List.iter (xpost ppf)
let projection _ppf (_p : projection) = ()
let value ppf (v : value) =
match v.ghost with
| Gospel.Tast.Ghost -> W.pp ppf (Ghost_value v.name, v.loc)
| Nonghost ->
terms ppf v.preconditions;
terms ppf v.postconditions;
xposts ppf v.xpostconditions
let mem_projection context gospel_model =
let aux = function
| Projection p -> p.model_name = gospel_model
| _ -> false
in
List.exists aux context
let type_ context ppf (t : type_) =
let missing_projections =
t.models
|> List.filter (fun (gospel_model, _, _) ->
not (mem_projection context.structure gospel_model))
|> List.map (fun (gospel_model, _, _) ->
(Missing_projection gospel_model, t.loc))
in
missing_proj ppf missing_projections;
match t.ghost with
| Gospel.Tast.Ghost -> pp ppf (Ghost_type t.name, t.loc)
| Nonghost ->
invariants ppf t.invariants
let constant ppf (c : constant) =
match c.ghost with
| Gospel.Tast.Ghost -> pp ppf (Ghost_value c.name, c.loc)
| Nonghost -> terms ppf c.checks
let definition ppf w loc = function
| None -> pp ppf (w, loc)
| Some def -> term ppf def
let function_ ppf (f : function_) =
let w = Function_without_definition f.name in
definition ppf w f.loc f.definition
let predicate ppf (p : function_) =
let w = Predicate_without_definition p.name in
definition ppf w p.loc p.definition
let axiom ppf (a : axiom) = term ppf a.definition
let emit_warnings ppf context =
Ir.iter_translation context ~f:(function
| Type t -> type_ context ppf t
| Projection p -> projection ppf p
| Value v -> value ppf v
| Constant c -> constant ppf c
| Function f -> function_ ppf f
| Predicate p -> predicate ppf p
| Axiom a -> axiom ppf a)