mlw_expr.ml 1.87 KB
Newer Older
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
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2011                                               *)
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software 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.                  *)
(*                                                                        *)
(**************************************************************************)

open Why3
open Ident
open Ty
open Mlw_ty

(* program symbols *)
type psymbol = {
27 28 29 30
  p_name : ident;
  p_tvs  : Stv.t;
  p_reg  : Sreg.t;
  p_vty  : vty;
31 32
}

33
let create_psymbol id tvars regs vty = {
34
  (* TODO? check that tvars/regs are in vty *)
35 36 37 38 39
  p_name = id_register id;
  p_tvs  = tvars;
  p_reg  = regs;
  p_vty  = vty;
}
40

41 42 43 44 45 46 47 48 49 50 51
let ps_equal : psymbol -> psymbol -> bool = (==)

type expr = private {
  e_node  : expr_node;
  e_vty   : vty;
  e_eff   : effect;
  e_label : Slab.t;
  e_loc   : Loc.position option;
}

and expr_node