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

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

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