package frama-c

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

Source file wpTipApi.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2023                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- Server API for WP                                                  --- *)
(* -------------------------------------------------------------------------- *)

open WpApi
module P = Server.Package
module D = Server.Data
module R = Server.Request
module S = Server.States
module Md = Markdown
module AST = Server.Kernel_ast

let package = P.package ~plugin:"wp" ~name:"tip"
    ~title:"WP Interactive Prover" ()

(* -------------------------------------------------------------------------- *)
(* --- Proof Node                                                         --- *)
(* -------------------------------------------------------------------------- *)

let proofStatus = R.signal ~package ~name:"proofStatus"
    ~descr:(Md.plain "Proof Status has changed")

module Node = D.Index(Map.Make(ProofEngine.Node))(struct let name = "node" end)

let () =
  let snode = R.signature ~input:(module Node) () in
  let set_title = R.result snode ~name:"result"
      ~descr:(Md.plain "Proof node title") (module D.Jstring) in
  let set_proved = R.result snode ~name:"proved"
      ~descr:(Md.plain "Proof node complete") (module D.Jbool) in
  let set_pending = R.result snode ~name:"pending"
      ~descr:(Md.plain "Pending children") (module D.Jint) in
  let set_size = R.result snode ~name:"size"
      ~descr:(Md.plain "Proof size") (module D.Jint) in
  let set_stats = R.result snode ~name:"stats"
      ~descr:(Md.plain "Node statistics") (module D.Jstring) in
  R.register_sig ~package ~kind:`GET ~name:"getNodeInfos"
    ~descr:(Md.plain "Proof node information") snode
    ~signals:[proofStatus]
    begin fun rq node ->
      set_title rq (ProofEngine.title node) ;
      set_proved rq (ProofEngine.proved node) ;
      set_pending rq (ProofEngine.pending node) ;
      let s = ProofEngine.stats node in
      set_size rq (Stats.subgoals s) ;
      set_stats rq (Pretty_utils.to_string Stats.pretty s) ;
    end

(* -------------------------------------------------------------------------- *)
(* --- Proof Tree                                                         --- *)
(* -------------------------------------------------------------------------- *)

let () =
  let state = R.signature ~input:(module Goal) () in
  let set_current = R.result state ~name:"current"
      ~descr:(Md.plain "Current proof node") (module Node) in
  let set_parents = R.result state ~name:"parents"
      ~descr:(Md.plain "Proof node parents") (module D.Jlist(Node)) in
  let set_pending = R.result state ~name:"pending"
      ~descr:(Md.plain "Pending proof nodes") (module D.Jint) in
  let set_index = R.result state ~name:"index"
      ~descr:(Md.plain "Current node index among pending nodes (else -1)")
      (module D.Jint) in
  let set_results = R.result state ~name:"results"
      ~descr:(Md.plain "Prover results for current node")
      (module D.Jlist(D.Jpair(Prover)(Result))) in
  let set_tactic = R.result state ~name:"tactic"
      ~descr:(Md.plain "Proof node tactic header (if any)")
      (module D.Jstring) in
  let set_children = R.result state ~name:"children"
      ~descr:(Md.plain "Proof node tactic children (id any)")
      (module D.Jlist(D.Jpair(D.Jstring)(Node))) in
  R.register_sig ~package
    ~kind:`GET ~name:"getProofState"
    ~descr:(Md.plain "Current Proof Status of a Goal") state
    ~signals:[proofStatus]
    begin fun rq wpo ->
      let tree = ProofEngine.proof ~main:wpo in
      let current,index =
        match ProofEngine.current tree with
        | `Main -> ProofEngine.root tree,-1
        | `Internal node -> node,-1
        | `Leaf(idx,node) -> node,idx in
      let rec parents node = match ProofEngine.parent node with
        | None -> []
        | Some p -> p::parents p in
      let tactic = match ProofEngine.tactical current with
        | None -> ""
        | Some { header } -> header in
      set_current rq current ;
      set_parents rq (parents current) ;
      set_index rq index ;
      set_pending rq (ProofEngine.pending current) ;
      set_results rq (Wpo.get_results (ProofEngine.goal current)) ;
      set_tactic rq tactic ;
      set_children rq (ProofEngine.children current) ;
    end

(* -------------------------------------------------------------------------- *)
(* --- Proof Tree Management                                              --- *)
(* -------------------------------------------------------------------------- *)

let () = R.register ~package ~kind:`SET ~name:"goForward"
    ~descr:(Md.plain "Go to to first pending node, or root if none")
    ~input:(module Goal) ~output:(module D.Junit)
    begin fun goal ->
      let tree = ProofEngine.proof ~main:goal in
      ProofEngine.forward tree ;
      R.emit proofStatus ;
    end

let () = R.register ~package ~kind:`SET ~name:"goToRoot"
    ~descr:(Md.plain "Go to root of proof tree")
    ~input:(module Goal) ~output:(module D.Junit)
    begin fun goal ->
      let tree = ProofEngine.proof ~main:goal in
      ProofEngine.goto tree `Main ;
      R.emit proofStatus ;
    end

let () = R.register ~package ~kind:`SET ~name:"goToIndex"
    ~descr:(Md.plain "Go to k-th pending node of proof tree")
    ~input:(module D.Jpair(Goal)(D.Jint)) ~output:(module D.Junit)
    begin fun (goal,index) ->
      let tree = ProofEngine.proof ~main:goal in
      ProofEngine.goto tree (`Leaf index) ;
      R.emit proofStatus ;
    end

let () = R.register ~package ~kind:`SET ~name:"goToNode"
    ~descr:(Md.plain "Set current node of associated proof tree")
    ~input:(module Node) ~output:(module D.Junit)
    begin fun node ->
      let tree = ProofEngine.tree node in
      ProofEngine.goto tree (`Node node) ;
      R.emit proofStatus ;
    end

let () = R.register ~package ~kind:`SET ~name:"removeNode"
    ~descr:(Md.plain "Remove node from tree and go to parent")
    ~input:(module Node) ~output:(module D.Junit)
    begin fun node ->
      let tree = ProofEngine.tree node in
      ProofEngine.remove tree node ;
      R.emit proofStatus ;
    end

(* -------------------------------------------------------------------------- *)
(* --- Sequent Indexers                                                   --- *)
(* -------------------------------------------------------------------------- *)

module Term = D.Tagged
    (struct
      type t = Lang.F.term
      let id t = Printf.sprintf "#e%d" (Lang.F.QED.id t)
    end)
    (struct let name = "term" end)

module Part = D.Tagged
    (struct
      type t = [ `Term | `Goal | `Step of int ]
      let id = function
        | `Term -> "#term"
        | `Goal -> "#goal"
        | `Step k -> Printf.sprintf "#s%d" k
    end)
    (struct let name = "part" end)

let of_part = function
  | Ptip.Term -> "#term"
  | Ptip.Goal -> "#goal"
  | Ptip.Step s -> Printf.sprintf "#s%d" s.id

let to_part sequent = function
  | `Term -> Ptip.Term
  | `Goal -> Ptip.Goal
  | `Step k ->
    try Ptip.Step (Conditions.step_at sequent k) with Not_found -> Ptip.Term

(* -------------------------------------------------------------------------- *)
(* --- Sequent Printer                                                    --- *)
(* -------------------------------------------------------------------------- *)

let wrap tag pp fmt x =
  begin
    Format.pp_open_stag fmt (Format.String_tag tag) ;
    pp fmt x ;
    Format.pp_close_stag fmt () ;
  end

class printer () : Ptip.pseq =
  let terms : Ptip.term_wrapper =
    object
      method wrap pp fmt t = wrap (Term.get t) pp fmt t
    end in
  let focus : Ptip.term_wrapper =
    object
      method wrap pp fmt t = wrap "wp:focus" pp fmt t
    end in
  let target : Ptip.term_wrapper =
    object
      method wrap pp fmt t = wrap "wp:target" pp fmt t
    end in
  let parts : Ptip.part_marker =
    object
      method wrap pp fmt p = wrap (of_part p) pp fmt p
      method mark : 'a. Ptip.part -> 'a Ptip.printer -> 'a Ptip.printer
        = fun p pp fmt x -> wrap (of_part p) pp fmt x
    end in
  let autofocus = new Ptip.autofocus in
  let plang = new Ptip.plang ~terms ~focus ~target ~autofocus in
  let pcond = new Ptip.pcond ~parts ~target:parts ~autofocus ~plang in
  Ptip.pseq ~autofocus ~plang ~pcond

(* -------------------------------------------------------------------------- *)
(* --- Printer Registry                                                   --- *)
(* -------------------------------------------------------------------------- *)

let printStatus = R.signal ~package ~name:"printStatus"
    ~descr:(Md.plain "Updated TIP printer")

module PRINTER = State_builder.Ref
    (Datatype.Make
       (struct
         include Datatype.Undefined
         type t = (string,printer) Hashtbl.t
         let name = "WpTipApi.PRINTER.Datatype"
         let reprs = [ Hashtbl.create 0 ]
         let mem_project = Datatype.never_any_project
       end))
    (struct
      let name = "WpApi.PRINTER"
      let dependencies = [ Ast.self ]
      let default () = Hashtbl.create 0
    end)

let () = Wpo.add_removed_hook
    (fun wpo ->
       let registry = PRINTER.get () in
       Hashtbl.remove registry wpo.po_gid)

let () = Wpo.add_cleared_hook
    (fun () ->
       let registry = PRINTER.get () in
       Hashtbl.clear registry)

let lookup_printer (node : ProofEngine.node) : printer =
  let tree = ProofEngine.tree node in
  let wpo = ProofEngine.main tree in
  let registry = PRINTER.get () in
  try Hashtbl.find registry wpo.po_gid with Not_found ->
    let pp = new printer () in
    Hashtbl.add registry wpo.po_gid pp ; pp

let selection node =
  let pp = lookup_printer node in
  pp#selection

(* -------------------------------------------------------------------------- *)
(* --- PrintSequent Request                                               --- *)
(* -------------------------------------------------------------------------- *)

let flags (type a) ~name ~descr tags : a R.input =
  (module struct
    type t = a
    let jtype = D.declare ~package ~name ~descr
        (P.Junion (List.map (fun (tg,_) -> P.Jtag tg) tags))
    let of_json js = List.assoc (Json.string js) tags
  end)

let iformat : Plang.iformat R.input =
  flags ~name:"iformat" ~descr:(Md.plain "Integer constants format")
    [ "dec", `Dec ; "hex", `Hex ; "bin", `Bin ]

let rformat : Plang.rformat R.input =
  flags ~name:"rformat" ~descr:(Md.plain "Real constants format")
    [ "ratio", `Ratio ; "float", `Float ; "double", `Double ]

let () =
  let printSequent = R.signature ~output:(module D.Jtext) () in
  let get_node = R.param printSequent ~name:"node"
      ~descr:(Md.plain "Proof Node") (module Node) in
  let get_indent = R.param_opt printSequent ~name:"indent"
      ~descr:(Md.plain "Number of identation spaces") (module D.Jint) in
  let get_margin = R.param_opt printSequent ~name:"margin"
      ~descr:(Md.plain "Maximial text width") (module D.Jint) in
  let get_iformat = R.param_opt printSequent ~name:"iformat"
      ~descr:(Md.plain "Integer constants format") iformat in
  let get_rformat = R.param_opt printSequent ~name:"rformat"
      ~descr:(Md.plain "Real constants format") rformat in
  let get_autofocus = R.param_opt printSequent ~name:"autofocus"
      ~descr:(Md.plain "Auto-focus mode") (module D.Jbool) in
  let get_unmangled = R.param_opt printSequent ~name:"unmangled"
      ~descr:(Md.plain "Unmangled memory model") (module D.Jbool) in
  R.register_sig ~package
    ~kind:`EXEC
    ~name:"printSequent"
    ~descr:(Md.plain "Pretty-print the associated node")
    ~signals:[printStatus] printSequent
    begin fun rq () ->
      let node = get_node rq in
      let pp = lookup_printer node in
      let indent = get_indent rq in
      let margin = get_margin rq in
      Option.iter pp#set_iformat (get_iformat rq) ;
      Option.iter pp#set_rformat (get_rformat rq) ;
      Option.iter pp#set_focus_mode (get_autofocus rq) ;
      Option.iter pp#set_unmangled (get_unmangled rq) ;
      D.jpretty ?indent ?margin pp#pp_goal (ProofEngine.goal node)
    end

(* -------------------------------------------------------------------------- *)
(* --- Selection Requests                                                 --- *)
(* -------------------------------------------------------------------------- *)

let () =
  R.register ~package
    ~kind:`SET
    ~name:"clearSelection"
    ~descr:(Md.plain "Reset node selection")
    ~input:(module Node)
    ~output:(module D.Junit)
    begin fun node ->
      let pp = lookup_printer node in
      pp#reset ; R.emit printStatus
    end

let () =
  let setSelection = R.signature ~output:(module D.Junit) () in
  let get_node = R.param setSelection ~name:"node"
      ~descr:(Md.plain "Proof Node") (module Node) in
  let get_part = R.param setSelection ~name:"part" ~default:`Term
      ~descr:(Md.plain "Selected part") (module Part) in
  let get_term = R.param_opt setSelection ~name:"term"
      ~descr:(Md.plain "Selected term") (module Term) in
  let get_extend = R.param setSelection ~name:"extend"
      ~descr:(Md.plain "Extending selection mode")
      ~default:false (module D.Jbool) in
  R.register_sig ~package
    ~kind:`SET
    ~name:"setSelection"
    ~descr:(Md.plain "Set node selection")
    setSelection
    begin fun rq () ->
      let node = get_node rq in
      let part = get_part rq in
      let term = get_term rq in
      let extend = get_extend rq in
      let pp = lookup_printer node in
      let part = to_part (fst pp#sequent) part in
      pp#restore ~focus:(if extend then `Extend else `Focus) (part,term) ;
      R.emit printStatus
    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