compile.ml 5.04 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 Term
52 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

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
83 84 85
    e_node   : expr_node;
    e_ity    : ity;
    e_effect : effect;
86 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
  }

  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
124 125 126
  let create_expr e_node e_ity e_effect =
    { e_node = e_node; e_ity = e_ity; e_effect = e_effect }

127 128 129
(* TODO add here some smart constructors for ML expressions *)

end
Mário Pereira's avatar
Mário Pereira committed
130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188

(** 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 *)

  (** programs *)

  let pv_name pv = pv.pv_vs.vs_name

  (* 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
    | _ -> assert false (* TODO *)

  (* program declarations *)
  let pdecl pd =
    match pd.pd_node with
    | PDlet (LDvar (_, _)) ->
       []
    | PDlet (LDsym ({rs_name = rsn}, {c_node = Cfun e})) ->
       [ML.Dlet (false, [rsn, [], expr e])]
    | 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