package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file pretty.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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- Pretty Printer with sharing                                        --- *)
(* -------------------------------------------------------------------------- *)

open Logic
open Format
open Plib

module Make(T : Term) =
struct

  open T

  (* -------------------------------------------------------------------------- *)
  (* ---  Types                                                             --- *)
  (* -------------------------------------------------------------------------- *)

  let pp_tvarn fmt n = fprintf fmt "?%d" n
  let pp_alpha fmt = function
    | 0 -> pp_print_string fmt "'a"
    | 1 -> pp_print_string fmt "'b"
    | 2 -> pp_print_string fmt "'c"
    | 3 -> pp_print_string fmt "'d"
    | 4 -> pp_print_string fmt "'e"
    | n -> fprintf fmt "?%d" (n-4)

  let pp_tau fmt t =
    let n = Kind.degree_of_tau t in
    if 0<=n && n<5
    then Kind.pp_tau pp_alpha Field.pretty ADT.pretty fmt t
    else Kind.pp_tau pp_tvarn Field.pretty ADT.pretty fmt t

  (* -------------------------------------------------------------------------- *)
  (* --- Shareable                                                          --- *)
  (* -------------------------------------------------------------------------- *)

  let shareable e = match T.repr e with
    | And _ | Or _ | Not _ | Imply _ | Eq _ | Neq _ | Leq _ | Lt _ -> false
    | Fun(f,_) -> (Fun.sort f <> Sprop && Fun.sort f <> Sbool)
    | _ -> true

  let subterms f e =
    match T.repr e with
    | Rdef fts ->
      begin
        match T.record_with fts with
        | None -> T.lc_iter f e
        | Some(a,fts) -> f a ; List.iter (fun (_,e) -> f e) fts
      end
    | _ -> T.lc_iter f e

  (* -------------------------------------------------------------------------- *)
  (* --- Variables                                                          --- *)
  (* -------------------------------------------------------------------------- *)

  module Idx = Map.Make(String)
  module Ids = Set.Make(String)

  type env = {
    mutable bound : string Intmap.t ; (* bound var *)
    mutable named : string Tmap.t ; (* named terms *)
    mutable index : int Idx.t ;     (* index names *)
    mutable known : Ids.t ;         (* known names *)
  }

  (* -------------------------------------------------------------------------- *)
  (* --- Environment                                                        --- *)
  (* -------------------------------------------------------------------------- *)

  let empty = {
    bound = Intmap.empty ;
    named = Tmap.empty ;
    index = Idx.empty ;
    known = Ids.empty ;
  }

  let copy env = {
    bound = env.bound ;
    named = env.named ;
    index = env.index ;
    known = env.known ;
  }

  (* -------------------------------------------------------------------------- *)
  (* --- Fresh                                                              --- *)
  (* -------------------------------------------------------------------------- *)

  let freshname env base =
    let rec scan env base k =
      let a = Printf.sprintf "%s_%d" base k in
      if Ids.mem a env.known
      then scan env base (succ k)
      else (env.index <- Idx.add base (succ k) env.index ; a) in
    scan env base
      (try Idx.find base env.index with Not_found -> 0)

  let known env xs =
    let env = copy env in
    Vars.iter
      (fun x ->
         let x = Plib.to_string Var.pretty x in
         env.known <- Ids.add x env.known
      ) xs ; env

  let marks env =
    T.marks ~shareable ~subterms
      ~shared:(fun t -> Tmap.mem t env.named) ()

  let bind x t env =
    let env = copy env in
    env.named <- Tmap.add t x env.named ;
    env.known <- Ids.add x env.known ;
    env

  let fresh env t =
    let env = copy env in
    let x = freshname env (T.basename t) in
    env.named <- Tmap.add t x env.named ;
    env.known <- Ids.add x env.known ;
    x , env

  let bind_var env k t =
    let x = freshname env (Tau.basename t) in
    env.known <- Ids.add x env.known ;
    env.bound <- Intmap.add k x env.bound ; x

  let find_var env k =
    try Intmap.find k env.bound
    with Not_found -> Printf.sprintf "#%d" k

  (* -------------------------------------------------------------------------- *)
  (* --- Groups of Quantifiers                                              --- *)
  (* -------------------------------------------------------------------------- *)

  module TauMap = Map.Make(T.Tau)

  let group_var t k = TauMap.add t [k] TauMap.empty

  let group_add t k tks =
    let ks = k :: try TauMap.find t tks with Not_found -> [] in
    TauMap.add t ks tks

  let rec group_binders k = function
    | [] -> []
    | (q,t)::qts -> group_collect q (succ k) (group_var t k) qts

  and group_collect q k kts = function
    | [] -> [q,kts]
    | (q0,t) :: qts ->
      if q = q0 && q0 <> Lambda then
        group_collect q (succ k) (group_add t k kts) qts
      else
        (q,kts) :: group_collect q0 (succ k) (group_var t k) qts

  (* -------------------------------------------------------------------------- *)
  (* --- Output Form                                                        --- *)
  (* -------------------------------------------------------------------------- *)

  type out =
    | Sum of term list
    | Atom of string
    | Hbox of string * term list
    | Vbox of string * term list
    | Unop of string * term
    | Binop of ( term * string * term )
    | Cond of ( term * term * term )
    | Call of Fun.t * term list
    | Closure of term * term list
    | Const of term
    | Access of term * term
    | Update of term * term * term
    | Record of field list
    | GetField of term * Field.t
    | Abstraction of (binder * tau) list * term
    | Bind of int

  and field =
    | With  of term
    | Field of Field.t * term
    | Last  of Field.t * term

  let rec fields = function
    | [] -> []
    | [f,v] -> [Last(f,v)]
    | (f,v)::fvs -> Field(f,v)::fields fvs

  let rec abstraction qxs e =
    match T.repr e with
    | Logic.Bind(q,x,t) -> abstraction ((q,x)::qxs) (lc_repr t)
    | _ -> Abstraction( List.rev qxs , e )

  let out e =
    match T.repr e with
    | Bvar(k,_) -> Bind k
    | Fvar x -> Atom( Plib.to_string Var.pretty x )
    | True -> Atom "true"
    | False -> Atom "false"
    | Kint z -> Atom (Z.to_string z)
    | Kreal r -> Atom (Q.to_string r)
    | Times(z,e) when Z.equal z Z.minus_one -> Unop("-",e)
    | Times(z,e) -> Hbox("*",[e_zint z;e])
    | Add es -> Sum es
    | Mul es -> Hbox("*",es)
    | Div(a,b) -> Binop(a,"div",b)
    | Mod(a,b) -> Binop(a,"mod",b)
    | And es -> Vbox("/\\",es)
    | Or  es -> Vbox("\\/",es)
    | Not e -> Unop("not ",e)
    | Imply(hs,p) ->Vbox("->",hs@[p])
    | Eq(a,b) ->
      if T.sort e = Sprop
      then Vbox("<->",[a;b])
      else Hbox("=",[a;b])
    | Lt(a,b) -> Hbox("<",[a;b])
    | Neq(a,b) -> Hbox("!=",[a;b])
    | Leq(a,b) -> Hbox("<=",[a;b])
    | Fun(a,es) -> Call(a,es)
    | Apply(e,es) -> Closure(e,es)
    | If(c,a,b) -> Cond(c,a,b)
    | Acst(_,v) -> Const(v)
    | Aget(a,b) -> Access(a,b)
    | Aset(a,b,c) -> Update(a,b,c)
    | Logic.Bind(q,x,e) -> abstraction [q,x] (lc_repr e)
    | Rget(e,f) -> GetField(e,f)
    | Rdef fvs -> Record
                    begin
                      match T.record_with fvs with
                      | None -> fields fvs
                      | Some(base,fothers) -> With base :: fields fothers
                    end

  let named_out env e =
    try Atom(Tmap.find e env.named)
    with Not_found -> out e

  (* -------------------------------------------------------------------------- *)
  (* --- Atom printer                                                       --- *)
  (* -------------------------------------------------------------------------- *)

  let rec pp_atom (env:env) (fmt:formatter) e =
    pp_atom_out env fmt (named_out env e)

  and pp_atom_out env fmt = function
    | Bind k -> pp_print_string fmt (find_var env k)
    | Atom x -> pp_print_string fmt x
    | Call(f,es) -> pp_call env fmt f es
    | Sum es -> fprintf fmt "@[<hov 1>(%a)@]" (pp_sum false env) es
    | Hbox(op,es) -> fprintf fmt "@[<hov 1>(%a)@]" (pp_hbox env op) es
    | Vbox(op,es) -> fprintf fmt "@[<hov 1>(%a)@]" (pp_vbox env op) es
    | Unop(op,e) -> fprintf fmt "@[<hov 3>(%s%a)@]" op (pp_atom env) e
    | Binop op -> fprintf fmt "@[<hov 3>(%a)@]" (pp_binop env) op
    | Cond c -> fprintf fmt "@[<hv 1>(%a)@]" (pp_cond env) c
    | Closure(e,es) -> pp_closure env fmt e es
    | Abstraction(qts,abs) -> fprintf fmt "@[<v 1>(%t)@]" (pp_abstraction env qts abs)
    | Const(v) -> fprintf fmt "@[<hov 2>[%a..]@]" (pp_free env) v
    | Access(a,b) -> fprintf fmt "@[<hov 2>%a@,[%a]@]"
                       (pp_atom env) a (pp_free env) b
    | Update(a,b,c) -> fprintf fmt "@[<hov 2>%a@,[%a@,->%a]@]"
                         (pp_atom env) a (pp_atom env) b (pp_free env) c
    | GetField(e,f) -> fprintf fmt "%a.%a" (pp_atom env) e Field.pretty f
    | Record fs -> pp_fields env fmt fs

  and pp_free_out env fmt = function
    | Bind k -> pp_print_string fmt (find_var env k)
    | Atom x -> pp_print_string fmt x
    | Call(f,es) -> pp_call env fmt f es
    | Sum es -> fprintf fmt "@[<hov 1>%a@]" (pp_sum true env) es
    | Hbox(op,es) -> fprintf fmt "@[<hov 0>%a@]" (pp_hbox env op) es
    | Vbox(op,es) -> fprintf fmt "@[<hov 0>%a@]" (pp_vbox env op) es
    | Unop(op,e) -> fprintf fmt "@[<hov 2>%s%a@]" op (pp_atom env) e
    | Binop op -> fprintf fmt "@[<hov 2>%a@]" (pp_binop env) op
    | Cond c -> fprintf fmt "@[<hv 0>%a@]" (pp_cond env) c
    | Closure(e,es) -> pp_closure env fmt e es
    | Abstraction(qts,abs) -> fprintf fmt "@[<hv 0>%t@]" (pp_abstraction env qts abs)
    | (Const _ | Access _ | Update _ | Record _ | GetField _) as a -> pp_atom_out env fmt a

  and pp_fields (env:env) (fmt:formatter) fs =
    fprintf fmt "@[<hv 0>{@[<hv 2>" ;
    List.iter
      (function
        | With r ->
          fprintf fmt "@ %a with" (pp_atom env) r
        | Field (f,v) ->
          fprintf fmt "@ @[<hov 2>%a =@ %a ;@]" Field.pretty f (pp_free env) v
        | Last (f,v) ->
          fprintf fmt "@ @[<hov 2>%a =@ %a@]" Field.pretty f (pp_free env) v
      ) fs ;
    fprintf fmt "@]@ }@]"

  (* -------------------------------------------------------------------------- *)
  (* --- Free printer                                                       --- *)
  (* -------------------------------------------------------------------------- *)

  and pp_free (env:env) (fmt:formatter) e = pp_free_out env fmt (named_out env e)
  and pp_freedef (env:env) (fmt:formatter) e = pp_free_out env fmt (out e)

  (* -------------------------------------------------------------------------- *)
  (* --- Call printer                                                       --- *)
  (* -------------------------------------------------------------------------- *)

  and pp_call (env:env) (fmt:formatter) f = function
    | [] -> Fun.pretty fmt f
    | es ->
      fprintf fmt "@[<hov 2>(%a" Fun.pretty f ;
      List.iter (fun e -> fprintf fmt "@ %a" (pp_atom env) e) es ;
      fprintf fmt ")@]"

  (* -------------------------------------------------------------------------- *)
  (* --- Sum printer                                                        --- *)
  (* -------------------------------------------------------------------------- *)

  and pp_sum free (env:env) (fmt:formatter) es =
    let ps,ns = List.fold_right
        (fun e (ps,ns) -> match T.repr e with
           | Times(k,n) when Z.equal k Z.minus_one -> (ps,n::ns)
           | Kint k when Z.lt k Z.zero -> (ps,e_zint (Z.neg k) :: ns)
           | Kreal r when Q.lt r Q.zero -> (ps,e_real (Q.neg r) :: ns)
           | _ -> e::ps , ns)
        es ([],[])
    in match ps , ns with
    | [] , [] -> pp_print_string fmt "0"
    | [] , _ ->
      if free
      then fprintf fmt "(%a)" (pp_factor env "-") ns
      else pp_factor env "-" fmt ns
    | p::ps , ns -> fprintf fmt "%a%a%a"
                      (pp_atom env) p
                      (pp_factor env "+") ps
                      (pp_factor env "-") ns

  and pp_factor env op fmt es =
    List.iter (fun e -> fprintf fmt "%s@,%a" op (pp_atom env) e) es

  (* -------------------------------------------------------------------------- *)
  (* --- Horizontal Boxes                                                   --- *)
  (* -------------------------------------------------------------------------- *)

  and pp_hbox (env:env) (sep:string) (fmt:formatter) = function
    | [] -> pp_print_string fmt "()"
    | e::es -> fprintf fmt "%a%a" (pp_atom env) e (pp_factor env sep) es

  (* -------------------------------------------------------------------------- *)
  (* --- Vertical Boxes                                                     --- *)
  (* -------------------------------------------------------------------------- *)

  and pp_vbox (env:env) (sep:string) (fmt:formatter) = function
    | [] -> ()
    | e::es ->
      pp_atom env fmt e ;
      List.iter (fun e -> fprintf fmt "@ %s %a" sep (pp_atom env) e) es

  (* -------------------------------------------------------------------------- *)
  (* --- Specific Operators                                                 --- *)
  (* -------------------------------------------------------------------------- *)

  and pp_binop (env:env) (fmt:formatter) (a,op,b) =
    fprintf fmt "%a@ %s %a" (pp_atom env) a op (pp_atom env) b

  and pp_cond (env:env) (fmt:formatter) (c,a,b) =
    fprintf fmt "if %a@ then %a@ else %a"
      (pp_atom env) c
      (pp_atom env) a
      (pp_atom env) b

  and pp_closure (env:env) (fmt:formatter) e es =
    fprintf fmt "@[<hov 3>(%a" (pp_atom env) e ;
    List.iter (fun e -> fprintf fmt "@ %a" (pp_atom env) e) es ;
    fprintf fmt ")@]"

  (* -------------------------------------------------------------------------- *)
  (* --- Abstraction                                                        --- *)
  (* -------------------------------------------------------------------------- *)

  and pp_abstraction (env:env) qts abs (fmt:formatter) =
    let env = copy env in
    let groups = group_binders 0 qts in
    let size = List.length qts in
    let last = Bvars.order (lc_vars abs) + size - 1 in
    List.iter
      (fun (q,m) ->
         match q with
         | Forall -> fprintf fmt "@[<hov 4>forall %a.@]@ " (pp_group env last) m
         | Exists -> fprintf fmt "@[<hov 4>exists %a.@]@ " (pp_group env last) m
         | Lambda -> fprintf fmt "@[<hov 4>fun %a ->@]@ " (pp_group env last) m
      ) groups ;
    pp_share env fmt abs

  and pp_group (env:env) (last:int) (fmt:formatter) m =
    let sep = ref false in
    TauMap.iter
      (fun t ks ->
         if !sep then fprintf fmt ",@," ;
         Plib.iteri
           (fun idx k ->
              let x = bind_var env (last - k) t in
              match idx with
              | Isingle | Ifirst -> pp_print_string fmt x
              | Imiddle | Ilast -> fprintf fmt ",@,%s" x
           ) (List.rev ks) ;
         fprintf fmt ":%a" pp_tau t ;
         sep := true ;
      ) m

  (* -------------------------------------------------------------------------- *)
  (* --- Sharing                                                            --- *)
  (* -------------------------------------------------------------------------- *)

  and pp_share (env:env) (fmt:formatter) t =
    begin
      fprintf fmt "@[<hv 0>" ;
      let shared t = Tmap.mem t env.named in
      let ts = T.shared ~shareable ~shared ~subterms [t] in
      let env =
        List.fold_left
          (fun env t ->
             let x,env_x = fresh env t in
             fprintf fmt "@[<hov 4>let %s =@ %a in@]@ " x (pp_atom env) t ;
             env_x)
          env ts in
      pp_free env fmt t ;
      fprintf fmt "@]" ;
    end

  (* -------------------------------------------------------------------------- *)
  (* --- Entry Point                                                        --- *)
  (* -------------------------------------------------------------------------- *)


  let pp_term_env (env:env) (fmt:formatter) t = pp_share env fmt t
  let pp_def_env (env:env) (fmt:formatter) t = pp_freedef env fmt t

  let pp_term (env:env) (fmt:formatter) t = pp_term_env (copy env) fmt t
  let pp_def (env:env) (fmt:formatter) t = pp_def_env (copy env) fmt t

end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct