compile.ml 7.77 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

125
  let mk_expr e_node e_ity e_effect =
Mário Pereira's avatar
Mário Pereira committed
126 127
    { 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

158 159 160
  let type_args = (* point-free *)
    List.map (fun x -> x.tv_name)

Mário Pereira's avatar
Mário Pereira committed
161 162
  (** programs *)

163 164 165 166 167 168 169 170 171
  (* individual types *)
  let rec ity t =
    match t.ity_node with
    | Ityvar ({tv_name = tv}, _) ->
       ML.Tvar tv
    | Ityapp ({its_ts = ts}, itl, _) ->
       ML.Tapp (ts.ts_name, List.map ity itl)
    | _ -> (* TODO *) assert false

Mário Pereira's avatar
Mário Pereira committed
172 173
  let pv_name pv = pv.pv_vs.vs_name

Mário Pereira's avatar
Mário Pereira committed
174 175 176 177 178 179 180 181
  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
182 183 184 185 186
  (* expressions *)
  let rec expr e =
    match e.e_node with
    | Evar pvs ->
       let pv_id = pv_name pvs in
187
       ML.mk_expr (ML.Eident pv_id) e.e_ity e.e_effect
Mário Pereira's avatar
Mário Pereira committed
188 189
    | Elet (LDvar (pvs, e1), e2) ->
       let ml_let = ML.ml_let (pv_name pvs) (expr e1) (expr e2) in
190 191 192 193 194 195
       ML.mk_expr ml_let e.e_ity e.e_effect
    | _ -> (* TODO *) assert false

  let its_args ts = ts.its_ts.ts_args
  let itd_name td = td.itd_its.its_ts.ts_name

196 197 198 199 200 201
  let drecord_fields {itd_its = its; itd_fields = fl} =
    List.map (fun ({rs_cty = rsc} as rs) ->
      (List.exists (pv_equal (Opt.get rs.rs_field)) its.its_mfields),
      rs.rs_name,
      if rs_ghost rs then ML.tunit else ity rsc.cty_result) fl

202 203
  let ddata_constructs = (* point-free *)
    List.map (fun ({rs_cty = rsc} as rs) ->
204
      rs.rs_name, List.map (fun {pv_vs = pv} -> type_ pv.vs_ty) rsc.cty_args)
205 206

  (** Question pour Jean-Christophe et Andreï :
207 208 209 210 211 212 213 214
       est-ce que vous pouriez m'expliquer le champ [itd_fields],
       utilisé dans une définition de type ([its_defn]) ?
       MIS-À-JOUR : je viens de coder l'extraction d'une définition
         d'un type enregistrement et je comprends maintenant que che
         champ est utilisé pour stocker les champs d'une définition de
         type enregistrement. Je veux toujours savoir s'il y a des
         cas particulaires d'utilisation, en particulier vis-à-vis du
         champ [itd_constructors] *)
215 216 217 218 219 220

  (* type declarations/definitions *)
  let tdef itd =
    let s = itd.itd_its in
    let id = itd_name itd in
    let args = its_args s in
221 222
    begin match s.its_def, itd.itd_constructors, itd.itd_fields with
      | None, [], [] ->
223
         ML.Dtype [id, type_args args, ML.Dabstract]
224
      | None, cl, [] ->
225
         ML.Dtype [id, type_args args, ML.Ddata (ddata_constructs cl)]
226 227 228
      | None, _, _ ->
         ML.Dtype [id, type_args args, ML.Drecord (drecord_fields itd)]
      | Some t, _, _ ->
229 230
         ML.Dtype [id, type_args args, ML.Dalias (ity t)]
    end
Mário Pereira's avatar
Mário Pereira committed
231 232 233 234 235 236

  (* program declarations *)
  let pdecl pd =
    match pd.pd_node with
    | PDlet (LDvar (_, _)) ->
       []
Mário Pereira's avatar
Mário Pereira committed
237 238
    | 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
239 240 241 242 243 244 245 246 247 248 249 250 251
    | 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 ->
       []
252 253
    | PDtype itl ->
       List.map tdef itl
Mário Pereira's avatar
Mário Pereira committed
254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270
    | _ -> (* 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
271 272 273

(*
 * Local Variables:
274
 * compile-command: "make -C ../.. -j3"
Mário Pereira's avatar
Mário Pereira committed
275 276
 * End:
 *)