package frama-c

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

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

open Lang
open Tactical
open Conditions

(* -------------------------------------------------------------------------- *)
(* --- Cut Tactical                                                       --- *)
(* -------------------------------------------------------------------------- *)

let fclause,pclause =
  Tactical.composer
    ~id:"clause"
    ~title:"Clause"
    ~descr:"Clause to cut with."
    ~filter:F.is_prop
    ()

type mode = CASES | MODUS

let fmode,pmode =
  Tactical.selector
    ~id:"case"
    ~title:"Mode"
    ~descr:"Select how the clause is used."
    ~default:MODUS
    ~options:Tactical.[
        { title="Case Analysis" ;
          descr="Consider P->Q and !P->Q." ;
          vid="CASES" ; value=CASES } ;
        { title="Modus Ponens" ;
          descr="Consider P and P->Q." ;
          vid="MODUS" ; value=MODUS } ;
      ] ()

class cut =
  object(self)
    inherit Tactical.make ~id:"Wp.cut"
        ~title:"Cut"
        ~descr:"Use intermerdiate hypothesis."
        ~params:[pmode;pclause]

    method select feedback sel =
      let mode =
        match sel with
        | Clause(Goal p) when p != F.p_false ->
          feedback#update_field ~enabled:false fmode ; CASES
        | _ ->
          feedback#update_field ~enabled:true fmode ;
          self#get_field fmode in
      let cut = self#get_field fclause in
      if Tactical.is_empty cut then
        Not_configured
      else
        match mode with
        | MODUS ->
          feedback#set_descr "Prove then insert the clause." ;
          let clause = F.p_bool (Tactical.selected cut) in
          let step = Conditions.step ~descr:"Cut" (Have clause) in
          let at = Tactical.at sel in
          Applicable
            begin fun sequent ->
              let assume = Conditions.insert ?at step sequent in
              [ "Clause" , (fst sequent,clause) ;
                "Assume" , (fst assume,snd sequent) ]
            end
        | CASES ->
          feedback#set_descr "Proof by case in the clause." ;
          let positive = F.p_bool (Tactical.selected cut) in
          let negative = F.p_not positive in
          Applicable
            begin fun (hs,goal) ->
              [ "Positive" , (hs,F.p_imply positive goal) ;
                "Negative" , (hs,F.p_imply negative goal) ]
            end
  end

let tactical = Tactical.export (new cut)

let strategy ?(priority=1.0) ?(modus=true) selection =
  Strategy.{
    priority ;
    tactical ;
    selection ;
    arguments = [ arg fmode (if modus then MODUS else CASES) ] ;
  }
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