mlw_expr.ml 5.16 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 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
(*

  1. A "proper type" of a vty [v] is [v] with all effects and specs
     (pre/post/xpost) removed. Basically, it is formed from the ity's
     of pvsymbols in the arguments and the result of [v].

  2. Given a vty [v], [vty_freevars v] and [vty_topregions v] return 
     the sets of type variables and regions, respectively, that occur 
     in the proper type of [v]. We will call them "proper" type variables
     and regions of [v].

  3. The specs (pre/post/xpost) and the effects in a vty [v] may contain
     type variables and regions that do not occur in the proper type of [v].
     We will call them "extra" type variables and regions of [v].

  4. A substitution given to [vty_full_inst] MUST instantiate every extra
     type variable and region to itself. We do not verify this invariant,
     but it is going to be ensured by the following.

  5. An expression [e] provides the maps [e.e_tvs] and [e.e_regs] from
     idents (vsymbols, pvsymbols, psymbols, ppsymbols) occurring in [e]
     to sets of type variables and regions, respectively, that are 
     "related" to these idents. For example, every type variable and
     region that occurs in a pv_ity of a pvsymbol [x] is related to [x].
     For psymbols and ppsymbols, the meaning of "related" is explained below.

  6. It is possible that [e.e_vty] contains a proper type variable or 
     a proper region that does not appear in the range of [e.e_tvs] or 
     [e.e_regs]. However, every extra type variable and region of
     [e.e_vty] MUST occur in the range of [e.e_tvs] and [e.e_regs].

  7. A psymbol (monomorphic program symbol) [p] provides the sets [p.p_tvs]
     and [p.p_regs] of its related type variables and regions, respectively, 
     that cover both proper and extra type variables and regions of [p.p_vty].

     One way to ensure this is to put into [p.p_tvs] the union of the proper
     type variables of [p.p_vty] and all the type variables in the range of
     [e.e_tvs], where [e] is the defining expression of [p] (similarly for
     regions). However, this will relate to [p] more that just proper and
     extra variables of [p.p_vty]. It is unclear whether this is a problem,
     but my guess is it's not.

  8. A ppsymbol  
*)






76 77 78 79 80
type variant = {
  v_term : term;           (* : tau *)
  v_rel  : lsymbol option; (* tau tau : prop *)
}

81 82
(* program symbols *)
type psymbol = {
83 84 85 86
  p_name : ident;
  p_tvs  : Stv.t;
  p_reg  : Sreg.t;
  p_vty  : vty;
87 88
}

89 90 91 92 93 94 95 96 97
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; }
98

99 100 101 102 103 104
let ps_equal : psymbol -> psymbol -> bool = (==)

type expr = private {
  e_node  : expr_node;
  e_vty   : vty;
  e_eff   : effect;
105
  e_ghost : bool;
106 107 108 109
  e_label : Slab.t;
  e_loc   : Loc.position option;
}

110 111 112
and expr_node =
  | Elogic  of term
  | Esym    of psymbol (* function *)
113
  | Eapp    of psymbol * expr
114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
  | 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*)