program API (in progress)

Makefile.in

@@ -447,7 +447,7 @@ install_local: bin/why3ml
 # Whyml (new API)
 ########
 
-MLW_FILES = mlw_ty mlw_expr
+MLW_FILES = mlw_ty mlw_expr mlw_decl mlw_module
 
 MLWMODULES = $(addprefix src/whyml/, $(MLW_FILES))
 

src/whyml/mlw_decl.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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
+open Mlw_ty
+
+type pdecl
+
+type known_map = pdecl Mid.t

src/whyml/mlw_decl.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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
+open Mlw_ty
+
+type pdecl
+
+type known_map = pdecl Mid.t

src/whyml/mlw_expr.ml

@@ -38,3 +38,14 @@ let create_psymbol id tvars regs vty =
     p_reg   = regs;
     p_vty   = vty; }
 
+let ps_equal : psymbol -> psymbol -> bool = (==)
+
+type expr = private {
+  e_node  : expr_node;
+  e_vty   : vty;
+  e_eff   : effect;
+  e_label : Slab.t;
+  e_loc   : Loc.position option;
+}
+
+and expr_node

src/whyml/mlw_expr.mli

@@ -33,7 +33,19 @@ type psymbol = private {
 
 val create_psymbol: preid -> Stv.t -> Sreg.t -> vty -> psymbol
 
+val ps_equal: psymbol -> psymbol -> bool
+
 (* program expressions *)
+
+type expr = private {
+  e_node  : expr_node;
+  e_vty   : vty;
+  e_eff   : effect;
+  e_label : Slab.t;
+  e_loc   : Loc.position option;
+}
+
+and expr_node
 (*
   | Letrec of (psymbol * lambda) list * expr
   | Let of pvsymbol * expr * expr

src/whyml/mlw_module.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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 Util
+open Ident
+open Ty
+open Theory
+open Mlw_ty
+open Mlw_expr
+open Mlw_decl
+
+(*
+  module = 
+    theory +
+    namespace +
+    program decls (no logic decl here)
+
+  extraction to OCaml
+    1. all types
+         follow order given by theory, and retrieve program types when necessary
+    2. logic decls (no types)
+    3. program decls
+*)
+type namespace = {
+  ns_it : itysymbol Mstr.t;  (* type symbols *)
+  ns_ps : psymbol Mstr.t;    (* program symbols *)
+  ns_ns : namespace Mstr.t;  (* inner namespaces *)
+}
+
+let empty_ns = {
+  ns_it = Mstr.empty;
+  ns_ps = Mstr.empty;
+  ns_ns = Mstr.empty;
+}
+
+exception ClashSymbol of string
+
+let ns_replace eq chk x vo vn =
+  if not chk then vn else
+  if eq vo vn then vo else
+  raise (ClashSymbol x)
+
+let ns_union eq chk =
+  Mstr.union (fun x vn vo -> Some (ns_replace eq chk x vo vn))
+
+let rec merge_ns chk ns1 ns2 =
+  let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
+  { ns_it = ns_union its_equal chk ns1.ns_it ns2.ns_it;
+    ns_ps = ns_union ps_equal chk ns1.ns_ps ns2.ns_ps;
+    ns_ns = Mstr.union fusion     ns1.ns_ns ns2.ns_ns; }
+
+let nm_add chk x ns m = Mstr.change x (function
+  | None -> Some ns
+  | Some os -> Some (merge_ns chk ns os)) m
+
+let ns_add eq chk x v m = Mstr.change x (function
+  | None -> Some v
+  | Some vo -> Some (ns_replace eq chk x vo v)) m
+
+let it_add = ns_add its_equal
+let ps_add = ns_add ps_equal
+
+let add_it chk x ts ns = { ns with ns_it = it_add chk x ts ns.ns_it }
+let add_ps chk x pf ns = { ns with ns_ps = ps_add chk x pf ns.ns_ps }
+let add_ns chk x nn ns = { ns with ns_ns = nm_add chk x nn ns.ns_ns }
+
+let rec ns_find get_map ns = function
+  | []   -> assert false
+  | [a]  -> Mstr.find a (get_map ns)
+  | a::l -> ns_find get_map (Mstr.find a ns.ns_ns) l
+
+let ns_find_it = ns_find (fun ns -> ns.ns_it)
+let ns_find_ps = ns_find (fun ns -> ns.ns_ps)
+let ns_find_ns = ns_find (fun ns -> ns.ns_ns)
+
+(** Module *)
+
+type modul = {
+  mod_theory: theory;			(* pure theory *)
+  mod_decls : pdecl list;		(* module declarations *)
+  mod_export: namespace;		(* exported namespace *)
+  mod_known : known_map;		(* known identifiers *)
+  mod_local : Sid.t;			(* locally declared idents *)
+}
+
+(** Module under construction *)
+
+type module_uc = {
+  muc_theory : theory_uc;
+  muc_decls  : pdecl list;
+  muc_import : namespace list;
+  muc_export : namespace list;
+  muc_known  : known_map;
+  muc_local  : Sid.t;
+}
+
+let empty_module n p = {
+  muc_theory = create_theory ~path:p n;
+  muc_decls  = [];
+  muc_import = [empty_ns];
+  muc_export = [empty_ns];
+  muc_known  = Mid.empty;
+  muc_local  = Sid.empty;
+}
+
+let create_module ?(path=[]) n =
+  empty_module n path
+
+let close_module uc =
+  let th = close_theory uc.muc_theory in (* catches errors *)
+  { mod_theory = th;
+    mod_decls  = List.rev uc.muc_decls;
+    mod_export = List.hd uc.muc_export;
+    mod_known  = uc.muc_known;
+    mod_local  = uc.muc_local; }
+
+let get_namespace uc = List.hd uc.muc_import
+let get_known uc = uc.muc_known
+
+let open_namespace uc = match uc.muc_import with
+  | ns :: _ -> { uc with
+      muc_theory = Theory.open_namespace uc.muc_theory;
+      muc_import =       ns :: uc.muc_import;
+      muc_export = empty_ns :: uc.muc_export; }
+  | [] -> assert false
+
+let close_namespace uc import s =
+  let th = Theory.close_namespace uc.muc_theory import s in (* catches errors *)
+  match uc.muc_import, uc.muc_export with
+  | _ :: i1 :: sti, e0 :: e1 :: ste ->
+      let i1 = if import then merge_ns false e0 i1 else i1 in
+      let _  = if import then merge_ns true  e0 e1 else e1 in
+      let i1 = match s with Some s -> add_ns false s e0 i1 | _ -> i1 in
+      let e1 = match s with Some s -> add_ns true  s e0 e1 | _ -> e1 in
+      { uc with
+	  muc_theory = th;
+	  muc_import = i1 :: sti;
+	  muc_export = e1 :: ste; }
+  | _ ->
+      assert false
+
+
+(** Use *)
+
+(***
+let use_export uc m =
+  match uc.muc_import, uc.muc_export with
+  | i0 :: sti, e0 :: ste -> { uc with
+      muc_import = merge_ns false m.mod_export i0 :: sti;
+      muc_export = merge_ns true  m.mod_export e0 :: ste }
+  | _ -> assert false
+***)

src/whyml/mlw_module.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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 Util
+open Ident
+open Ty
+open Theory
+open Mlw_ty
+open Mlw_expr
+open Mlw_decl
+
+type namespace = private {
+  ns_it : itysymbol Mstr.t;  (* type symbols *)
+  ns_ps : psymbol Mstr.t;    (* program symbols *)
+  ns_ns : namespace Mstr.t;  (* inner namespaces *)
+}
+
+val ns_find_it : namespace -> string list -> itysymbol
+val ns_find_ps : namespace -> string list -> psymbol
+val ns_find_ns : namespace -> string list -> namespace
+
+(** Module *)
+
+type modul = private {
+  mod_theory: theory;			(* pure theory *)
+  mod_decls : pdecl list;		(* module declarations *)
+  mod_export: namespace;		(* exported namespace *)
+  mod_known : known_map;		(* known identifiers *)
+  mod_local : Sid.t;			(* locally declared idents *)
+}
+
+(** Module under construction *)
+
+type module_uc (* a module under construction *)
+
+val create_module : ?path:string list -> preid -> module_uc
+val close_module  : module_uc -> modul
+
+val open_namespace  : module_uc -> module_uc
+val close_namespace : module_uc -> bool -> string option -> module_uc
+
+val get_namespace : module_uc -> namespace
+val get_known : module_uc -> known_map
+
+(** Use *)
+
+(* val use_export : module_uc -> modul -> module_uc *)
+
+(** Clone: not yet implemented *)

src/whyml/mlw_ty.ml

@@ -45,6 +45,7 @@ and ity_node =
 
 and region = {
   reg_ity : ity;
+  reg_ghost: bool;
   reg_tag : Hashweak.tag;
 }
 
@@ -65,9 +66,9 @@ let reg_hash r = Hashweak.tag_hash r.reg_tag
 
 let create_region =
   let r = ref 0 in
-  fun ty ->
+  fun ?(ghost=false) ty ->
     incr r;
-    { reg_ity = ty; reg_tag = Hashweak.create_tag !r }
+    { reg_ity = ty; reg_ghost = ghost; reg_tag = Hashweak.create_tag !r }
 
 (* value type symbols *)
 
@@ -397,9 +398,10 @@ let create_pvsymbol id ?mut ?(ghost=false) ity =
   let ty = ty_of_ity ity in
   let vs = create_vsymbol id ty in
   begin match mut with
-    | Some r when not (ity_equal r.reg_ity ity) ->
+    | Some r when not (ity_equal r.reg_ity ity) || ghost <> r.reg_ghost ->
         raise (InvalidPVsymbol vs.vs_name)
-    | _ -> ()
+    | _ ->
+        ()
   end;
   { pv_vs = vs;
     pv_ity = ity;

src/whyml/mlw_ty.mli

@@ -26,10 +26,10 @@ open Term
 (** individual types (first-order types w/o effects) *)
 
 type itysymbol = private {
-  its_pure  : tysymbol;
-  its_args  : tvsymbol list;
-  its_regs  : region   list;
-  its_def   : ity option;
+  its_pure : tysymbol;
+  its_args : tvsymbol list;
+  its_regs : region   list;
+  its_def  : ity option;
 }
 
 and ity = private {
@@ -44,8 +44,9 @@ and ity_node = private
   (* | Itymod of tysymbol * ity *)
 
 and region = private {
-  reg_ity : ity;
-  reg_tag : Hashweak.tag;
+  reg_ity   : ity;
+  reg_ghost : bool;
+  reg_tag   : Hashweak.tag;
 }
 
 module Mits : Map.S with type key = itysymbol
@@ -78,7 +79,7 @@ exception DuplicateRegion of region
 exception UnboundRegion of region
 exception InvalidRegion of region
 
-val create_region : ity -> region
+val create_region : ?ghost:bool -> ity -> region
 
 val create_itysymbol :
   preid -> tvsymbol list -> region list -> ity option -> itysymbol