compile.ml 5.83 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 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

(*
  - option to extract into a single file

  - no more why3extract.cma
    use driver preludes instead

  - 2 drivers for nums and zarith

  - no delcaration at all for a module -> no file produced
    (e.g. ref.Ref)

  - suggest a command line to compile the extracted code
    (for instance in a comment)

  - drivers for val now may use %1, %2, etc. (though not mandatory)
    Capp f x y
      "..." -> "..." x y
      "...%1..." -> "...x..." y
      "..(*%1*)..." -> "...(*x*)..." y
      "..%1..%3.." -> (fun z -> "..x..z..")  (y ignored)

  - extract file f.mlw into OCaml file f.ml, with sub-modules

  - "use (im|ex)port" -> "open"
    but OCaml's open is not transitive, so requires some extra work
    to figure out all the opens

  - if a WhyML module M is extracted to something that is a signature,
    then extract "module type B_sig = ..." (as well as "module B = ...")

  - use a black list in printer to avoid clash with Pervasives symbols
    (e.g. ref, (!), etc.)

*)

(** Abstract syntax of ML *)

open Ident
open Ity
Mário Pereira's avatar
Mário Pereira committed
51
open Ty
Mário Pereira's avatar
Mário Pereira committed
52
open Term
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

module ML = struct

  type ty =
    | Tvar    of ident
    | Tapp    of ident * ty list
    | Ttuple  of ty list

  type var = ident * ty

  type pat =
    | Pwild
    | Pident  of ident
    | Papp    of ident * pat list
    | Ptuple  of pat list
    | Precord of (ident * pat) list
    | Por     of pat * pat
    | Pas     of pat * ident

  type is_rec = bool

  type binop = Band | Bor | Beq

  type for_direction = To | DownTo

  type exn =
    | Xident  of ident
    | Xsyntax of string
    | Xexit             (* Pervasives.Exit *)

  type expr = {
Mário Pereira's avatar
Mário Pereira committed
84 85 86
    e_node   : expr_node;
    e_ity    : ity;
    e_effect : effect;
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124
  }

  and expr_node =
    | Econst  of Number.integer_constant
    | Ebool   of bool
    | Eident  of ident
    | Eapp    of expr * expr list
    | Efun    of var list * expr
    | Elet    of ident * expr * expr
    | Eletrec of is_rec * (ident * var list * expr) list * expr
    | Eif     of expr * expr * expr
    | Ecast   of expr * ty
    | Etuple  of expr list (* at least 2 expressions *)
    | Econstr of ident * expr list
    | Ematch  of expr * (pat * expr) list
    | Ebinop  of expr * binop * expr
    | Enot    of expr
    | Eblock  of expr list
    | Ewhile  of expr * expr
    | Efor    of ident * ident * for_direction * ident * expr
    | Eraise  of exn * expr option
    | Etry    of expr * (exn * ident option * expr) list
    | Eabsurd

  type is_mutable = bool

  type typedef =
    | Dabstract
    | Ddata     of (ident * ty list) list
    | Drecord   of (is_mutable * ident * ty) list
    | Dalias    of ty

  type decl = (* TODO add support for the extraction of ocaml modules *)
    | Dtype of (ident * ident list * typedef) list
    | Dlet  of is_rec * (ident * var list * expr) list
        (* TODO add return type? *)
    | Dexn  of ident * ty option

Mário Pereira's avatar
Mário Pereira committed
125 126 127
  let create_expr e_node e_ity e_effect =
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

Mário Pereira's avatar
Mário Pereira committed
128 129 130 131 132
  (* TODO add here some smart constructors for ML expressions *)
  let ml_let id e1 e2 =
    Elet (id, e1, e2)

  let tunit = Ttuple []
133 134

end
Mário Pereira's avatar
Mário Pereira committed
135 136 137 138 139 140 141 142 143 144

(** Translation from Mlw to ML *)

module Translate = struct

  open Expr    (* Mlw expressions *)

  open Pmodule (* for the type of modules *)
  open Pdecl   (* for the type of program declarations *)

Mário Pereira's avatar
Mário Pereira committed
145 146 147 148 149 150 151 152 153 154 155 156 157
  (* types *)
  let rec type_ ty =
    match ty.ty_node with
    | Tyvar tvs ->
       ML.Tvar tvs.tv_name
    | Tyapp (ts, tyl) when is_ts_tuple ts ->
       ML.Ttuple (List.map type_ tyl)
    | Tyapp (ts, tyl) ->
       ML.Tapp (ts.ts_name, List.map type_ tyl)

  let vsty vs =
    vs.vs_name, type_ vs.vs_ty

Mário Pereira's avatar
Mário Pereira committed
158 159 160 161
  (** programs *)

  let pv_name pv = pv.pv_vs.vs_name

Mário Pereira's avatar
Mário Pereira committed
162 163 164 165 166 167 168 169
  let pvty pv =
    if pv.pv_ghost then (pv_name pv, ML.tunit)
    else vsty pv.pv_vs

  (* function arguments *)
  let args = (* point-free *)
    List.map pvty

Mário Pereira's avatar
Mário Pereira committed
170 171 172 173 174 175
  (* expressions *)
  let rec expr e =
    match e.e_node with
    | Evar pvs ->
       let pv_id = pv_name pvs in
       ML.create_expr (ML.Eident pv_id) e.e_ity e.e_effect
Mário Pereira's avatar
Mário Pereira committed
176 177 178
    | Elet (LDvar (pvs, e1), e2) ->
       let ml_let = ML.ml_let (pv_name pvs) (expr e1) (expr e2) in
       ML.create_expr ml_let e.e_ity e.e_effect
Mário Pereira's avatar
Mário Pereira committed
179 180 181 182 183 184 185
    | _ -> assert false (* TODO *)

  (* program declarations *)
  let pdecl pd =
    match pd.pd_node with
    | PDlet (LDvar (_, _)) ->
       []
Mário Pereira's avatar
Mário Pereira committed
186 187
    | PDlet (LDsym ({rs_name = rsn; rs_cty = cty}, {c_node = Cfun e})) ->
       [ML.Dlet (false, [rsn, args cty.cty_args, expr e])]
Mário Pereira's avatar
Mário Pereira committed
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
    | PDlet (LDsym ({rs_name = rsn}, {c_node = Capp _})) ->
       Format.printf "LDsym Capp--> %s@." rsn.id_string;
       []
    | PDlet (LDsym ({rs_name = rsn}, {c_node = Cpur _})) ->
       Format.printf "LDsym Cpur--> %s@." rsn.id_string;
       []
    | PDlet (LDsym ({rs_name = rsn}, {c_node = Cany})) ->
       Format.printf "LDsym Cany--> %s@." rsn.id_string;
       []
    | PDlet (LDrec _) ->
       []
    | PDpure ->
       []
    | _ -> (* TODO *) assert false

  (* unit module declarations *)
  let mdecl = function
    | Udecl pd ->
       pdecl pd
    | Uuse _ ->
       []
    | Uscope _ ->
       []
    | _ -> (* TODO *) assert false

  (* modules *)
  let module_ m =
    List.concat (List.map mdecl m.mod_units)

end
Mário Pereira's avatar
Mário Pereira committed
218 219 220 221 222 223

(*
 * Local Variables:
 * compile-command: "make -C ../.."
 * End:
 *)