package frama-c

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

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

type var = Lang.F.var
type tau = Lang.F.tau
type field = Lang.field
type lfun = Lang.lfun
type term = Lang.F.term
type pred = Lang.F.pred

type repr =
  | True
  | False
  | And of term list
  | Or of term list
  | Not of term
  | Imply of term list * term
  | If of term * term * term
  | Var of var
  | Int of Z.t
  | Real of Q.t
  | Add of term list
  | Mul of term list
  | Div of term * term
  | Mod of term * term
  | Eq of term * term
  | Neq of term * term
  | Lt of term * term
  | Leq of term * term
  | Times of Z.t * term
  | Call of lfun * term list
  | Field of term * field
  | Record of (field * term) list
  | Cst of tau * term
  | Get of term * term
  | Set of term * term * term
  | HigherOrder

module L = Qed.Logic

let term e : repr =
  match Lang.F.repr e with
  | L.True -> True
  | L.False -> False
  | L.And ts -> And ts
  | L.Or ts -> Or ts
  | L.Not t -> Not t
  | L.If(a,b,c) -> If(a,b,c)
  | L.Imply(hs,p) -> Imply(hs,p)
  | L.Kint z -> Int z
  | L.Kreal r -> Real r
  | L.Add ts -> Add ts
  | L.Mul ts -> Mul ts
  | L.Div(a,b) -> Div(a,b)
  | L.Mod(a,b) -> Mod(a,b)
  | L.Eq(a,b) -> Eq(a,b)
  | L.Neq(a,b) -> Neq(a,b)
  | L.Lt(a,b) -> Lt(a,b)
  | L.Leq(a,b) -> Leq(a,b)
  | L.Times(k,t) -> Times(k,t)
  | L.Fun(f,ts) -> Call(f,ts)
  | L.Rget(r,f) -> Field(r,f)
  | L.Rdef fvs -> Record fvs
  | L.Acst(t,v) -> Cst(t,v)
  | L.Aget(a,k) -> Get(a,k)
  | L.Aset(a,k,v) -> Set(a,k,v)
  | L.Fvar x -> Var x
  | L.Bvar _ | L.Bind _ | L.Apply _
    -> HigherOrder

let pred p = term (Lang.F.e_prop p)

let lfun = Lang.name_of_lfun
let field = Lang.name_of_field

(* -------------------------------------------------------------------------- *)
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