package frama-c

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

Source file TacRewrite.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
(**************************************************************************)
(*                                                                        *)
(*  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).            *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- Tactic to Apply Substitution by Hand                                   *)
(* -------------------------------------------------------------------------- *)
open Tactical
open Repr

let rewrite ~select ~replaced ~value =
  Applicable
    (Tactical.rewrite
       ?at:(Tactical.at select)
       [ "Rewrite" , Lang.F.p_true , replaced , value ])

let hypothesis s =
  let open Conditions in
  match s.condition with
  | When p | Have p | Core p | Init p -> p
  | _ -> raise Not_found

let clause = function
  | Clause(Step s) -> hypothesis s
  | Inside(Step s,e) ->
    begin
      match Repr.pred (hypothesis s) with
      | And es when List.memq e es -> Lang.F.p_bool e
      | _ -> raise Not_found
    end
  | _ -> raise Not_found

class rewrite dir =
  let id = if dir then "Wp.TacRewrite.Left" else "Wp.TacRewrite.Right" in
  let title = if dir then "Rewrite (<-)" else "Rewrite (->)" in
  object
    inherit Tactical.make
        ~id ~title ~descr:"Rewrite from equality." ~params:[]

    method select _feedback select =
      try
        let p = clause select in
        match Repr.pred p with
        | Eq(a,b) ->
          let replaced,value = if dir then a,b else b,a in
          rewrite ~select ~replaced ~value
        | _ -> Not_applicable
      with Not_found -> Not_applicable
  end

let tacl = Tactical.export (new rewrite true :>  Tactical.tactical)
let tacr = Tactical.export (new rewrite false :>  Tactical.tactical)

let mem a b =
  let rec walk m e =
    if a==e then raise Exit ;
    if not (Lang.F.Tset.mem e !m) then
      begin
        m := Lang.F.Tset.add e !m ;
        Lang.F.lc_iter (walk m) e
      end
  in try walk (ref Lang.F.Tset.empty) b ; false with Exit -> true

let direct a goal =
  match Repr.term goal with
  | Eq(u,v) when a == u || a == v -> true
  | _ -> false

let submit push select e goal rw =
  if direct e goal then
    push (Strategy.make ~priority:1.5 rw select)
  else
  if mem e goal then
    push (Strategy.make ~priority:0.5 rw select)

let rec lookup step push goal e =
  match Repr.term e with
  | And ps -> List.iter (lookup step push goal) ps
  | Eq(a,b) ->
    begin
      let select = Inside(Step step,e) in
      submit push select a goal tacl ;
      submit push select b goal tacr ;
    end
  | _ -> ()

class auto_rewrite =
  object
    method id = "wp:replace"
    method title = "Auto Replace"
    method descr = "Lookup for equalities to rewrite with."
    method search (push : Strategy.strategy -> unit) (hyps,goal) =
      Conditions.iter
        (fun s ->
           let open Conditions in
           match s.condition with
           | Have p | When p | Core p | Init p ->
             lookup s push (Lang.F.e_prop goal) (Lang.F.e_prop p)
           | _ -> ())
        hyps
  end

let () = Strategy.register (new auto_rewrite)

type dir = [ `Left | `Right ]
let tactical = function
  | `Left -> tacl
  | `Right -> tacr

let strategy ?priority dir selection =
  Strategy.make ?priority (tactical dir) selection
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