mlw_expr.ml 2.97 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
(**************************************************************************)
(*                                                                        *)
(*  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
23
open Term
24 25
open Mlw_ty

26 27 28 29 30
type variant = {
  v_term : term;           (* : tau *)
  v_rel  : lsymbol option; (* tau tau : prop *)
}

31 32
(* program symbols *)
type psymbol = {
33 34 35 36
  p_name : ident;
  p_tvs  : Stv.t;
  p_reg  : Sreg.t;
  p_vty  : vty;
37 38
}

39 40 41 42 43 44 45 46 47
let create_psymbol id tvars regs = function
  | VTvalue pv ->
      let pv =
        create_pvsymbol id ?mut:pv.pv_mutable ~ghost:pv.pv_ghost pv.pv_ity in
      { p_name = pv.pv_vs.vs_name;
        p_tvs = tvars; p_reg = regs; p_vty = vty_value pv; }
  | VTarrow _ as vty ->
      (* TODO? check that tvars/regs are in vty *)
      { p_name = id_register id; p_tvs = tvars; p_reg = regs; p_vty = vty; }
48

49 50 51 52 53 54
let ps_equal : psymbol -> psymbol -> bool = (==)

type expr = private {
  e_node  : expr_node;
  e_vty   : vty;
  e_eff   : effect;
55
  e_ghost : bool;
56 57 58 59
  e_label : Slab.t;
  e_loc   : Loc.position option;
}

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
and expr_node =
  | Elogic  of term
  | Esym    of psymbol (* function *)
  | Eapp    of psymbol * expr * cty
  | Elet    of psymbol * expr * expr
  | Eletrec of recfun list * expr
  | Efun    of lambda
  | Eif     of expr * expr * expr
  | Eassign of pvsymbol * psymbol * region * expr (* e1.f<rho> <- e2 *)

and recfun = psymbol * lambda

and lambda = {
  l_args    : pvsymbol list;
  l_variant : variant list; (* lexicographic order *)
  l_pre     : term;
  l_body    : expr;
  l_post    : term;
  l_xpost   : xpost;
}

let lapp _ = assert false (*TODO*)
let papp _ = assert false (*TODO*)
let app _ = assert false (*TODO*)
let plet _ = assert false (*TODO*)
let pletrec _ = assert false (*TODO*)
let pfun _ = assert false (*TODO*)
let assign _ = assert false (*TODO*)