Skip to content
GitLab
Commit 479ade45 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

use module

parent 22d9a525
Hide whitespace changes
Inline Side-by-side
src/parser/typing.mli
View file @ 479ade45
......@@ -71,6 +71,7 @@ val dfmla : ?localize:bool -> denv -> Ptree.lexpr -> Denv.dfmla
val dpat : denv -> Ptree.pattern -> denv * Denv.dpattern
val dpat_list : denv -> Denv.dty -> Ptree.pattern -> denv * Denv.dpattern
val split_qualid : Ptree.qualid -> string list * string
val string_list_of_qualid : string list -> Ptree.qualid -> string list
val qloc : Ptree.qualid -> Loc.position
......
src/programs/pgm_lexer.mll
View file @ 479ade45
......@@ -50,12 +50,14 @@
"done", DONE;
"downto", DOWNTO;
"else", ELSE;
"export", EXPORT;
"end", END;
"exception", EXCEPTION;
"for", FOR;
"fun", FUN;
"ghost", GHOST;
"if", IF;
"import", IMPORT;
"in", IN;
"invariant", INVARIANT;
"label", LABEL;
......@@ -73,6 +75,7 @@
"to", TO;
"try", TRY;
"type", TYPE;
"use", USE;
"variant", VARIANT;
"while", WHILE;
"with", WITH;
......
src/programs/pgm_main.ml
View file @ 479ade45
......@@ -21,16 +21,18 @@
open Format
open Why
open Util
open Ptree
open Pgm_ptree
open Pgm_module
let add_module ?(type_only=false) env tm m =
let add_module ?(type_only=false) env lmod m =
ignore (type_only);
let id = m.mod_name in
let uc = create_module (Ident.id_user id.id id.id_loc) in
let _uc = List.fold_left (Pgm_typing.decl env) uc m.mod_decl in
tm
let uc = List.fold_left (Pgm_typing.decl env lmod) uc m.mod_decl in
let m = close_module uc in
Mstr.add id.id m lmod
let read_channel env file c =
let lb = Lexing.from_channel c in
......@@ -40,18 +42,8 @@ let read_channel env file c =
Theory.Mnm.empty
else begin
let type_only = Debug.test_flag Typing.debug_type_only in
List.fold_left (add_module ~type_only env) Theory.Mnm.empty ml
(* let uc = Theory.create_theory (Ident.id_fresh "Pgm") in *)
(* let th = Env.find_theory env ["programs"] "Prelude" in *)
(* let uc = Theory.use_export uc th in *)
(* let gl = empty_env uc in *)
(* let gl = type_and_wp ~type_only env gl dl in *)
(* if type_only then *)
(* Theory.Mnm.empty *)
(* else begin *)
(* let th = Theory.close_theory gl.uc in *)
(* Theory.Mnm.add "Pgm" th Theory.Mnm.empty *)
(* end *)
let _mm = List.fold_left (add_module ~type_only env) Mstr.empty ml in
Theory.Mnm.empty
end
let () = Env.register_format "whyml" ["mlw"] read_channel
......
src/programs/pgm_module.ml
View file @ 479ade45
......@@ -86,9 +86,7 @@ let add_pervasives uc =
let create_module n =
let uc = Theory.create_theory n in
(* let th = Env.find_theory env ["programs"] "Prelude" in *)
(* let uc = Theory.use_export uc th in *)
let uc = add_pervasives uc in
(* let uc = add_pervasives uc in *)
{ uc_name = id_register n;
uc_th = uc;
uc_decls = [];
......@@ -157,6 +155,15 @@ let close_module uc = match uc.uc_export with
| _ ->
raise CloseModule
(** Use *)
let use_export uc m =
match uc.uc_import, uc.uc_export with
| i0 :: sti, e0 :: ste -> { uc with
uc_import = merge_ns false m.m_export i0 :: sti;
uc_export = merge_ns true m.m_export e0 :: ste }
| _ -> assert false
(* parsing LOGIC strings using functions from src/parser/
requires proper relocation *)
......
src/programs/pgm_module.mli
View file @ 479ade45
......@@ -23,7 +23,12 @@ val namespace : uc -> namespace
val theory_uc : uc -> Theory.theory_uc
(** a module *)
type t
type t = private {
m_name : ident;
m_th : Theory.theory;
m_decls : Pgm_ttree.decl list;
m_export : namespace;
}
val create_module : preid -> uc
val close_module : uc -> t
......@@ -31,6 +36,8 @@ val close_module : uc -> t
val open_namespace : uc -> uc
val close_namespace : uc -> bool -> string option -> uc
val use_export : uc -> t -> uc
(** insertion *)
exception ClashSymbol of string
......
src/programs/pgm_parser.mly
View file @ 479ade45
......@@ -82,7 +82,7 @@
let id_unit () = { id = "unit"; id_lab = []; id_loc = loc () }
let id_result () = { id = "result"; id_lab = []; id_loc = loc () }
let id_anonymous () = { id = "_"; id_lab = []; id_loc = loc () }
let exit_exn () = { id = "%Exit"; id_lab = []; id_loc = loc () }
let exit_exn () = Qident { id = "%Exit"; id_lab = []; id_loc = loc () }
let id_lt_nat () = Qident { id = "lt_nat"; id_lab = []; id_loc = loc () }
......@@ -117,10 +117,10 @@
/* keywords */
%token ABSURD AND ANY AS ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO ELSE END
%token EXCEPTION FOR
%token FUN GHOST IF IN INVARIANT LABEL LET MATCH MODULE NOT OF PARAMETER
%token EXCEPTION EXPORT FOR
%token FUN GHOST IF IMPORT IN INVARIANT LABEL LET MATCH MODULE NOT OF PARAMETER
%token RAISE RAISES READS REC
%token THEN TO TRY TYPE VARIANT WHILE WITH WRITES
%token THEN TO TRY TYPE USE VARIANT WHILE WITH WRITES
/* symbols */
......@@ -229,6 +229,21 @@ decl:
{ Dexn (add_lab $2 $3, None) }
| EXCEPTION uident labels OF pure_type
{ Dexn (add_lab $2 $3, Some $5) }
| USE MODULE use
{ $3 }
;
use:
| imp_exp tqualid
{ Duse ($2, $1, None) }
| imp_exp tqualid AS uident
{ Duse ($2, $1, Some $4) }
;
imp_exp:
| IMPORT { Import }
| EXPORT { Export }
| /* epsilon */ { Nothing }
;
list1_recfun_sep_and:
......@@ -276,6 +291,16 @@ uqualid:
| uqualid DOT uident { Qdot ($1, $3) }
;
any_qualid:
| ident { Qident $1 }
| any_qualid DOT ident { Qdot ($1, $3) }
;
tqualid:
| uident { Qident $1 }
| any_qualid DOT uident { Qdot ($1, $3) }
;
expr:
| simple_expr %prec prec_simple
{ $1 }
......@@ -342,9 +367,9 @@ expr:
{ mk_expr Eabsurd }
| expr COLON pure_type
{ mk_expr (Ecast ($1, $3)) }
| RAISE uident
| RAISE uqualid
{ mk_expr (Eraise ($2, None)) }
| RAISE LEFTPAR uident expr RIGHTPAR
| RAISE LEFTPAR uqualid expr RIGHTPAR
{ mk_expr (Eraise ($3, Some $4)) }
| TRY expr WITH option_bar list1_handler_sep_bar END
{ mk_expr (Etry ($2, $5)) }
......@@ -399,9 +424,9 @@ list1_handler_sep_bar:
;
handler:
| ident ARROW expr { ($1, None, $3) }
| ident ident ARROW expr { ($1, Some $2, $4) }
| ident UNDERSCORE ARROW expr { ($1, Some (id_anonymous ()), $4) }
| uqualid ARROW expr { ($1, None, $3) }
| uqualid ident ARROW expr { ($1, Some $2, $4) }
| uqualid UNDERSCORE ARROW expr { ($1, Some (id_anonymous ()), $4) }
;
match_cases:
......@@ -582,7 +607,7 @@ list1_post_exn:
;
post_exn:
| BAR uident ARROW LOGIC { $2, $4 }
| BAR uqualid ARROW LOGIC { $2, $4 }
;
effects:
......@@ -592,17 +617,17 @@ effects:
opt_reads:
| /* epsilon */ { [] }
| READS list0_lident_sep_comma { $2 }
| READS list0_lqualid_sep_comma { $2 }
;
opt_writes:
| /* epsilon */ { [] }
| WRITES list0_lident_sep_comma { $2 }
| WRITES list0_lqualid_sep_comma { $2 }
;
opt_raises:
| /* epsilon */ { [] }
| RAISES list0_uident_sep_comma { $2 }
| RAISES list0_uqualid_sep_comma { $2 }
;
opt_variant:
......@@ -616,24 +641,24 @@ opt_cast:
| COLON pure_type { Some $2 }
;
list0_lident_sep_comma:
| /* epsilon */ { [] }
| list1_lident_sep_comma { $1 }
list0_lqualid_sep_comma:
| /* epsilon */ { [] }
| list1_lqualid_sep_comma { $1 }
;
list1_lident_sep_comma:
| lident { [$1] }
| lident COMMA list1_lident_sep_comma { $1 :: $3 }
list1_lqualid_sep_comma:
| lqualid { [$1] }
| lqualid COMMA list1_lqualid_sep_comma { $1 :: $3 }
;
list0_uident_sep_comma:
| /* epsilon */ { [] }
| list1_uident_sep_comma { $1 }
list0_uqualid_sep_comma:
| /* epsilon */ { [] }
| list1_uqualid_sep_comma { $1 }
;
list1_uident_sep_comma:
| uident { [$1] }
| uident COMMA list1_uident_sep_comma { $1 :: $3 }
list1_uqualid_sep_comma:
| uqualid { [$1] }
| uqualid COMMA list1_uqualid_sep_comma { $1 :: $3 }
;
label:
......
src/programs/pgm_ptree.ml
View file @ 479ade45
......@@ -45,14 +45,14 @@ type loop_annotation = {
type for_direction = To | Downto
type effect = {
pe_reads : ident list;
pe_writes : ident list;
pe_raises : ident list;
pe_reads : qualid list;
pe_writes : qualid list;
pe_raises : qualid list;
}
type pre = lexpr
type post = lexpr * (ident * lexpr) list
type post = lexpr * (qualid * lexpr) list
type type_v =
| Tpure of Ptree.pty
......@@ -88,8 +88,8 @@ and expr_desc =
| Ematch of expr * (Ptree.pattern * expr) list
| Eskip
| Eabsurd
| Eraise of ident * expr option
| Etry of expr * (ident * ident option * expr) list
| Eraise of qualid * expr option
| Etry of expr * (qualid * ident option * expr) list
| Efor of ident * expr * for_direction * expr * lexpr option * expr
(* annotations *)
| Eassert of assertion_kind * lexpr
......@@ -107,6 +107,8 @@ type decl =
| Dlogic of logic
| Dparam of ident * type_v
| Dexn of ident * Ptree.pty option
(* modules *)
| Duse of qualid * Ptree.imp_exp * (*as*) ident option
type module_ = {
mod_name : ident;
......
src/programs/pgm_typing.ml
View file @ 479ade45
......@@ -133,12 +133,14 @@ let specialize_global loc x uc =
let p = ns_find_pr (namespace uc) x in
p.p_ls, specialize_type_v ~loc (Htv.create 17) p.p_tv
let print_qualid = print_list dot pp_print_string
let print_qualids = print_list dot pp_print_string
let print_qualid fmt q =
print_list dot pp_print_string fmt (Typing.string_list_of_qualid [] q)
let specialize_exception loc x uc =
let s =
try ns_find_ex (namespace uc) x
with Not_found -> errorm ~loc "unbound exception %a" print_qualid x
with Not_found -> errorm ~loc "unbound exception %a" print_qualids x
in
match Denv.specialize_lsymbol ~loc s with
| tyl, Some ty -> s, tyl, ty
......@@ -186,23 +188,25 @@ let check_reference_type uc loc ty =
errorm ~loc "this expression has type %a, but is expected to be a reference"
print_dty ty
let dreference env id =
if Typing.mem_var id.id env.denv then
(* local variable *)
let ty = Typing.find_var id.id env.denv in
check_reference_type env.uc id.id_loc ty;
DRlocal id.id
else
let p = Qident id in
let s, _, ty = Typing.specialize_fsymbol p (theory_uc env.uc) in
check_reference_type env.uc id.id_loc ty;
DRglobal s
let dexception env id =
let _, _, ty as r = specialize_exception id.id_loc [id.id] env.uc in
let dreference env = function
| Qident id when Typing.mem_var id.id env.denv ->
(* local variable *)
let ty = Typing.find_var id.id env.denv in
check_reference_type env.uc id.id_loc ty;
DRlocal id.id
| p ->
let loc = Typing.qloc p in
let s, _, ty = Typing.specialize_fsymbol p (theory_uc env.uc) in
check_reference_type env.uc loc ty;
DRglobal s
let dexception env qid =
let sl = Typing.string_list_of_qualid [] qid in
let loc = Typing.qloc qid in
let _, _, ty as r = specialize_exception loc sl env.uc in
let ty_exn = dty_app (find_ts env.uc "exn", []) in
if not (Denv.unify ty ty_exn) then
errorm ~loc:id.id_loc
errorm ~loc
"this expression has type %a, but is expected to be an exception"
print_dty ty;
r
......@@ -400,16 +404,16 @@ and dexpr_desc env loc = function
DElogic (fs_tuple 0), dty_unit env.uc
| Pgm_ptree.Eabsurd ->
DEabsurd, create_type_var loc
| Pgm_ptree.Eraise (id, e) ->
let ls, tyl, _ = dexception env id in
| Pgm_ptree.Eraise (qid, e) ->
let ls, tyl, _ = dexception env qid in
let e = match e, tyl with
| None, [] ->
None
| Some _, [] ->
errorm ~loc "expection %s has no argument" id.id
errorm ~loc "expection %a has no argument" print_qualid qid
| None, [ty] ->
errorm ~loc "exception %s is expecting an argument of type %a"
id.id print_dty ty;
errorm ~loc "exception %a is expecting an argument of type %a"
print_qualid qid print_dty ty;
| Some e, [ty] ->
let e = dexpr env e in
expected_type e ty;
......@@ -424,12 +428,12 @@ and dexpr_desc env loc = function
let ls, tyl, _ = dexception env id in
let x, env = match x, tyl with
| Some _, [] ->
errorm ~loc "expection %s has no argument" id.id
errorm ~loc "expection %a has no argument" print_qualid id
| None, [] ->
None, env
| None, [ty] ->
errorm ~loc "exception %s is expecting an argument of type %a"
id.id print_dty ty;
errorm ~loc "exception %a is expecting an argument of type %a"
print_qualid id print_dty ty;
| Some x, [ty] ->
Some x.id, add_local env x.id (DTpure ty)
| _ ->
......@@ -1300,7 +1304,18 @@ let cannot_be_generalized gl = function
| Tpure _ | Tarrow _ ->
false
let decl env uc = function
let find_module lmod q id = match q with
| [] ->
(* local module *)
Mstr.find id lmod
(* TODO? with Not_found -> find_theory env [] id end *)
| _ :: _ ->
(* theory in file f *)
assert false (*TODO*)
(* env = to retrieve theories from the loadpath
lmod = local modules *)
let decl env lmod uc = function
| Pgm_ptree.Dlogic dl ->
Pgm_module.parse_logic_decls env dl uc
| Pgm_ptree.Dlet (id, e) ->
......@@ -1338,6 +1353,35 @@ let decl env uc = function
| Pgm_ptree.Dexn (id, ty) ->
let ty = option_map (type_type uc) ty in
add_exception id.id_loc id.id ty uc
(* modules *)
| Pgm_ptree.Duse (qid, imp_exp, use_as) ->
let loc = Typing.qloc qid in
let q, id = Typing.split_qualid qid in
let m =
try
find_module lmod q id
with Not_found ->
errorm ~loc "unbound module %a" print_qualid qid
in
let n = match use_as with
| None -> Some (m.m_name.id_string)
| Some x -> Some x.id
in
begin try match imp_exp with
| Nothing ->
(* use T = namespace T use_export T end *)
let uc = open_namespace uc in
let uc = use_export uc m in
close_namespace uc false n
| Import ->
(* use import T = namespace T use_export T end import T *)
let uc = open_namespace uc in
let uc = use_export uc m in
close_namespace uc true n
| Export ->
use_export uc m
with ClashSymbol s -> errorm ~loc "clash with previous symbol %s" s
end
(*
Local Variables:
......
src/programs/pgm_typing.mli
View file @ 479ade45
......@@ -18,10 +18,13 @@
(**************************************************************************)
open Why
open Util
val debug : Debug.flag
val decl : Env.env -> Pgm_module.uc -> Pgm_ptree.decl -> Pgm_module.uc
val decl :
Env.env -> Pgm_module.t Mstr.t ->
Pgm_module.uc -> Pgm_ptree.decl -> Pgm_module.uc
val print_post : Format.formatter -> Pgm_ttree.post -> unit
tests/test-pgm-jcf.mlw
View file @ 479ade45
module A
{ use import programs.Prelude }
parameter x : int
exception E
exception F of int
parameter f : int -> int
end
module P
{ use import list.List }
{ use import programs.Prelude
use import list.List }
use module import A as B
{ logic n : int }
parameter x : list int
let f x = x + B.f 2
let f (x : unit) = ()
let g x = { x >= 0 } f (x+2) { result >= 0 }
end
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment