WhyML: typing of expressions (in progress)

Makefile.in

@@ -389,7 +389,7 @@ install_local: bin/why3
 ########
 
 MLW_FILES = mlw_ty mlw_expr mlw_decl mlw_module mlw_pretty \
-	    mlw_typing mlw_main
+	    mlw_dtree mlw_typing mlw_main
 
 MLWMODULES = $(addprefix src/whyml/, $(MLW_FILES))
 

src/parser/denv.ml

@@ -27,16 +27,6 @@ open Ty
 open Term
 open Theory
 
-exception AnyMessage of string
-
-let error ?loc e = match loc with
-  | None -> raise e
-  | Some loc -> raise (Loc.Located (loc,e))
-
-let () = Exn_printer.register (fun fmt e -> match e with
-  | AnyMessage s -> fprintf fmt "%s" s
-  | _ -> raise e)
-
 (** types with destructive type variables *)
 
 type dty_view =
@@ -124,7 +114,7 @@ let rec ty_of_dty = function
   | Tyvar { type_val = Some t } ->
       ty_of_dty t
   | Tyvar { type_val = None; user = false; type_var_loc = loc } ->
-      error ?loc (AnyMessage "undefined type variable")
+      Loc.errorm ?loc "undefined type variable"
   | Tyvar { tvsymbol = tv } ->
       ty_var tv
   | Tyapp (s, tl) ->

src/whyml/mlw_dtree.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2012                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Guillaume Melquiond                                                 *)
+(*    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 Denv
+open Ty
+open Mlw_ty
+open Mlw_module
+
+type loc = Loc.position
+
+type ident = Ptree.ident
+
+type constant = Term.constant
+
+type assertion_kind = Ptree.assertion_kind
+
+type lazy_op = Ptree.lazy_op
+
+type for_direction = Ptree.for_direction
+
+(*****************************************************************************)
+(* phase 1: introduction of destructive types *)
+
+(* user type_v *)
+
+type dpre = Ptree.pre
+type dpost_fmla = Ptree.lexpr
+type dexn_post_fmla = Ptree.lexpr
+type dpost = dpost_fmla * (Term.lsymbol * dexn_post_fmla) list
+
+type dueffect = {
+  du_reads  : Ptree.lexpr list;
+  du_writes : Ptree.lexpr list;
+  du_raises : xsymbol list;
+}
+
+type dutype_v =
+  | DUTpure  of Denv.dty
+  | DUTarrow of dubinder list * dutype_c
+
+and dutype_c =
+  { duc_result_type : dutype_v;
+    duc_effect      : dueffect;
+    duc_pre         : Ptree.lexpr;
+    duc_post        : Ptree.lexpr * (Term.lsymbol * Ptree.lexpr) list; }
+
+and dubinder = ident * Denv.dty * dutype_v
+
+type dvariant = Ptree.lexpr * Term.lsymbol option
+
+type dloop_annotation = {
+  dloop_invariant : Ptree.lexpr option;
+  dloop_variant   : dvariant option;
+}
+
+type dexpr = {
+  dexpr_desc : dexpr_desc;
+  dexpr_type : Denv.dty;
+  dexpr_lab  : Ident.label list;
+  dexpr_loc  : loc;
+}
+
+and dexpr_desc =
+  | DEconstant of constant
+  | DElocal of string
+  | DEglobal of prgsymbol
+  | DElogic of Term.lsymbol
+  | DEapply of dexpr * dexpr
+  | DEfun of dubinder list * dtriple
+  | DElet of ident * dexpr * dexpr
+  | DEletrec of drecfun list * dexpr
+  | DEassign of dexpr * Term.lsymbol * int * dexpr
+  | DEsequence of dexpr * dexpr
+  | DEif of dexpr * dexpr * dexpr
+  | DEloop of dloop_annotation * dexpr
+  | DElazy of lazy_op * dexpr * dexpr
+  | DEnot of dexpr
+  | DEmatch of dexpr * (Denv.dpattern * dexpr) list
+  | DEabsurd
+  | DEraise of xsymbol * dexpr option
+  | DEtry of dexpr * (xsymbol * string option * dexpr) list
+  | DEfor of ident * dexpr * for_direction * dexpr * Ptree.lexpr option * dexpr
+  | DEassert of assertion_kind * Ptree.lexpr
+  | DEmark of string * dexpr
+  | DEany of dutype_c
+
+and drecfun = (ident * Denv.dty) * dubinder list * dvariant option * dtriple
+
+and dtriple = dpre * dexpr * dpost

src/whyml/mlw_typing.ml

@@ -27,6 +27,7 @@ open Decl
 open Theory
 open Env
 open Ptree
+open Mlw_dtree
 open Mlw_ty
 open Mlw_expr
 open Mlw_decl
@@ -86,6 +87,90 @@ let () = Exn_printer.register (fun fmt e -> match e with
 
 (* TODO: let type_only = Debug.test_flag Typing.debug_type_only in *)
 
+(** Typing type expressions *)
+
+let ts_arrow =
+  let a = create_tvsymbol (Ident.id_fresh "a") in
+  let b = create_tvsymbol (Ident.id_fresh "b") in
+  Ty.create_tysymbol (Ident.id_fresh "arrow") [a; b] None
+
+let ts_region =
+  let a = create_tvsymbol (Ident.id_fresh "a") in
+  let b = create_tvsymbol (Ident.id_fresh "b") in
+  Ty.create_tysymbol (Ident.id_fresh "region") [a; b] None
+
+(* let rec ity_of_dty = function *)
+(*   | Tyvar { type_val = Some t } -> *)
+(*       ty_of_dty t *)
+(*   | Tyvar { type_val = None; user = false; type_var_loc = loc } -> *)
+(*       error ?loc (AnyMessage "undefined type variable") *)
+(*   | Tyvar { tvsymbol = tv } -> *)
+(*       ty_var tv *)
+(*   | Tyapp (s, tl) -> *)
+(*       ty_app s (List.map ty_of_dty tl) *)
+
+(** Typing program expressions *)
+
+let rec extract_labels labs loc e = match e.Ptree.expr_desc with
+  | Ptree.Enamed (Ptree.Lstr s, e) -> extract_labels (s :: labs) loc e
+  | Ptree.Enamed (Ptree.Lpos p, e) -> extract_labels labs (Some p) e
+  | Ptree.Ecast  (e, ty) ->
+      let labs, loc, d = extract_labels labs loc e in
+      labs, loc, Ptree.Ecast ({ e with Ptree.expr_desc = d }, ty)
+  | e -> List.rev labs, loc, e
+
+type denv = {
+  uc     : module_uc;
+  locals : Denv.dty Mstr.t;
+  denv   : Typing.denv; (* for user type variables only *)
+}
+
+let create_denv uc =
+  { uc = uc;
+    locals = Mstr.empty;
+    denv = Typing.create_denv (); }
+
+let rec dexpr ~userloc denv e =
+  let loc = e.Ptree.expr_loc in
+  let labs, userloc, d = extract_labels [] userloc e in
+  let d, ty = dexpr_desc ~userloc denv loc d in
+  let loc = def_option loc userloc in
+  let e = {
+    dexpr_desc = d; dexpr_loc = loc; dexpr_lab = labs; dexpr_type = ty; }
+  in
+  e
+
+and dexpr_desc ~userloc denv _loc = function
+  | Ptree.Eident (Qident {id=x}) when Mstr.mem x denv.locals ->
+      (* local variable *)
+      let tyv = Mstr.find x denv.locals in
+      DElocal x, tyv
+  | _ ->
+      ignore (userloc);
+      assert false (*TODO*)
+
+type local_var =
+  | Lpvsymbol of pvsymbol
+  | Lpasymbol of pasymbol
+  | Lpsymbol  of psymbol * Denv.type_var Mtv.t * Denv.type_var Mreg.t
+
+let region_table : region Htv.t =
+  Htv.create 17 (* FIXME: use Wtv instead *)
+
+let rec expr locals de = match de.dexpr_desc with
+  | DElocal x ->
+      assert (Mstr.mem x locals);
+      begin match Mstr.find x locals with
+      | Lpvsymbol pv -> e_value pv
+      | Lpasymbol pa -> e_arrow pa
+      | Lpsymbol  (_ps, _, _) ->
+          (* let ity = ity_of_dty de.dexpr_dty in *)
+          (* e_inst ps *)
+          assert false (*TODO*)
+      end
+  | _ ->
+      assert false (*TODO*)
+
 (** Type declaration *)
 
 type tys = ProgTS of itysymbol | PureTS of tysymbol
@@ -546,8 +631,14 @@ let add_module lib path mm mt m =
         let uc = open_namespace uc in
         let uc = List.fold_left add_decl uc dl in
         Loc.try3 loc close_namespace uc import name
-    | Dlet _ | Dletrec _ | Dparam _ | Dexn _ | Duse _ ->
-        assert false
+    | Dlet (_id, e) ->
+        let e = dexpr ~userloc:None (create_denv uc) e in
+        ignore (expr Mstr.empty e);
+        uc
+    | Dletrec _ | Dparam _ | Dexn _ ->
+        assert false (* TODO *)
+    | Duse _ ->
+        assert false (*TO BE REMOVED EVENTUALLY *)
   in
   let uc = List.fold_left add_decl uc m.mod_decl in
   let m = close_module uc in