Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit 70e507e0 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

syntax for modules, program types now in pgm_types

parent 349a0eb4
......@@ -282,7 +282,7 @@ PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
src/programs/pgm_lexer.ml
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_effect \
pgm_env pgm_typing pgm_wp pgm_main
pgm_types pgm_module # pgm_env pgm_typing pgm_wp pgm_main
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
......
......@@ -7,30 +7,6 @@ open Term
open Ty
module E = Pgm_effect
(* types *)
type effect = E.t
type reference = Pgm_effect.reference
type pre = Term.fmla
type post_fmla = Term.vsymbol (* result *) * Term.fmla
type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
type post = post_fmla * (Term.lsymbol * exn_post_fmla) list
type type_v =
| Tpure of Ty.ty
| Tarrow of binder list * type_c
and type_c =
{ c_result_type : type_v;
c_effect : effect;
c_pre : pre;
c_post : post; }
and binder = Term.vsymbol * type_v
(* environments *)
type env = {
......@@ -96,13 +72,6 @@ let ls_Exit = memo_ls
create_lsymbol (id_fresh "%Exit") [] (Some ty_exn))
let v_result ty = create_vsymbol (id_fresh "result") ty
let exn_v_result ls = match ls.ls_args with
| [] -> None
| [ty] -> Some (v_result ty)
| _ -> assert false
let add_type_v_ref uc m =
let ts_ref = find_ts uc ["ref"] in
let a = ty_var (create_tvsymbol (id_fresh "a")) in
......@@ -161,22 +130,6 @@ let empty_env uc = {
ls_add = find_ls uc ["infix +"];
}
let make_arrow_type env tyl ty =
let arrow ty1 ty2 = Ty.ty_app env.ts_arrow [ty1; ty2] in
List.fold_right arrow tyl ty
let rec uncurry_type = function
| Tpure ty ->
[], ty
| Tarrow (bl, c) ->
let tyl1 = List.map (fun (v,_) -> v.vs_ty) bl in
let tyl2, ty = uncurry_type c.c_result_type in
tyl1 @ tyl2, ty (* TODO: improve? *)
let purify env v =
let tyl, ty = uncurry_type v in
make_arrow_type env tyl ty
(* parsing LOGIC strings using functions from src/parser/
requires proper relocation *)
......@@ -211,170 +164,12 @@ let add_exception id ty env =
let s = create_lsymbol id tyl (Some (ty_app env.ts_exn [])) in
s, { env with exceptions = Mstr.add s.ls_name.id_string s env.exceptions }
(* misc. functions *)
let post_map f ((v, q), ql) =
(v, f q), List.map (fun (e,(v,q)) -> e, (v, f q)) ql
let type_c_of_type_v env = function
| Tarrow ([], c) ->
c
| v ->
let ty = purify env v in
{ c_result_type = v;
c_effect = Pgm_effect.empty;
c_pre = f_true;
c_post = (v_result ty, f_true), []; }
let rec subst_var ts s vs =
let ty' = ty_inst ts vs.vs_ty in
if ty_equal ty' vs.vs_ty then
s, vs
else
let vs' = create_vsymbol (id_clone vs.vs_name) ty' in
Mvs.add vs (t_var vs') s, vs'
and subst_post ts s ((v, q), ql) =
let vq = let s, v = subst_var ts s v in v, f_ty_subst ts s q in
let handler (e, (v, q)) = match v with
| None -> e, (v, f_ty_subst ts s q)
| Some v -> let s, v = subst_var ts s v in e, (Some v, f_ty_subst ts s q)
in
vq, List.map handler ql
let rec subst_type_c ef ts s c =
{ c_result_type = subst_type_v ef ts s c.c_result_type;
c_effect = E.subst ef c.c_effect;
c_pre = f_ty_subst ts s c.c_pre;
c_post = subst_post ts s c.c_post; }
and subst_type_v ef ts s = function
| Tpure ty ->
Tpure (ty_inst ts ty)
| Tarrow (bl, c) ->
let s, bl = Util.map_fold_left (binder ef ts) s bl in
Tarrow (bl, subst_type_c ef ts s c)
and binder ef ts s (vs, v) =
let v = subst_type_v ef ts s v in
let s, vs = subst_var ts s vs in
s, (vs, v)
let tpure ty = Tpure ty
let tarrow bl c = match bl with
| [] ->
invalid_arg "tarrow"
| _ ->
let rename (e, s) (vs, v) =
let vs' = create_vsymbol (id_clone vs.vs_name) vs.vs_ty in
let v' = subst_type_v e Mtv.empty s v in
let e' = Mvs.add vs (E.Rlocal vs') e in
let s' = Mvs.add vs (t_var vs') s in
(e', s'), (vs', v')
in
let (e, s), bl' = Util.map_fold_left rename (Mvs.empty, Mvs.empty) bl in
Tarrow (bl', subst_type_c e Mtv.empty s c)
let subst1 vs1 t2 = Mvs.add vs1 t2 Mvs.empty
let apply_type_v env v vs = match v with
| Tarrow ((x, tyx) :: bl, c) ->
let ts = ty_match Mtv.empty (purify env tyx) vs.vs_ty in
let c = type_c_of_type_v env (Tarrow (bl, c)) in
subst_type_c Mvs.empty ts (subst1 x (t_var vs)) c
| Tarrow ([], _) | Tpure _ ->
assert false
let apply_type_v_ref env v r = match r, v with
| E.Rlocal vs as r, Tarrow ((x, tyx) :: bl, c) ->
let ts = ty_match Mtv.empty (purify env tyx) vs.vs_ty in
let c = type_c_of_type_v env (Tarrow (bl, c)) in
let ef = Mvs.add x r Mvs.empty in
subst_type_c ef ts (subst1 x (t_var vs)) c
| E.Rglobal ls as r, Tarrow ((x, tyx) :: bl, c) ->
let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
let ts = ty_match Mtv.empty (purify env tyx) ty in
let c = type_c_of_type_v env (Tarrow (bl, c)) in
let ef = Mvs.add x r Mvs.empty in
subst_type_c ef ts (subst1 x (t_app ls [] ty)) c
| _ ->
assert false
let occur_formula r f = match r with
| E.Rlocal vs -> f_occurs_single vs f
| E.Rglobal ls -> f_s_any (fun _ -> false) (ls_equal ls) f
let rec occur_type_v r = function
| Tpure _ ->
false
| Tarrow (bl, c) ->
occur_arrow r bl c
and occur_arrow r bl c = match bl with
| [] ->
occur_type_c r c
| (vs, v) :: bl ->
occur_type_v r v ||
not (E.ref_equal r (E.Rlocal vs)) && occur_arrow r bl c
and occur_type_c r c =
occur_type_v r c.c_result_type ||
occur_formula r c.c_pre ||
E.occur r c.c_effect ||
occur_post r c.c_post
and occur_post r ((_, q), ql) =
occur_formula r q ||
List.exists (fun (_, (_, qe)) -> occur_formula r qe) ql
let rec eq_type_v v1 v2 = match v1, v2 with
| Tpure ty1, Tpure ty2 ->
ty_equal ty1 ty2
| Tarrow _, Tarrow _ ->
false (* TODO? *)
| _ ->
assert false
let t_True env =
t_app env.ls_True [] (ty_app env.ts_bool [])
let type_v_unit env =
Tpure (ty_app env.ts_unit [])
(* pretty-printers *)
open Pp
open Format
open Pretty
let print_post fmt ((_,q), el) =
let print_exn_post fmt (l,(_,q)) =
fprintf fmt "| %a -> {%a}" print_ls l print_fmla q
in
fprintf fmt "{%a} %a" print_fmla q (print_list space print_exn_post) el
let rec print_type_v fmt = function
| Tpure ty ->
print_ty fmt ty
| Tarrow (bl, c) ->
fprintf fmt "@[<hov 2>%a ->@ %a@]"
(print_list arrow print_binder) bl print_type_c c
and print_type_c fmt c =
fprintf fmt "@[{%a}@ %a%a@ %a@]" print_fmla c.c_pre
print_type_v c.c_result_type Pgm_effect.print c.c_effect
print_post c.c_post
and print_binder fmt (x, v) =
fprintf fmt "(%a:%a)" print_vs x print_type_v v
(* let apply_type_v env v vs = *)
(* eprintf "apply_type_v: v=%a vs=%a@." print_type_v v print_vs vs; *)
(* apply_type_v env v vs *)
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
......
......@@ -7,32 +7,6 @@ open Theory
open Term
open Decl
(* types *)
type effect = Pgm_effect.t
type reference = Pgm_effect.reference
type pre = Term.fmla
type post_fmla = Term.vsymbol (* result *) * Term.fmla
type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
type post = post_fmla * (Term.lsymbol * exn_post_fmla) list
type type_v = private
| Tpure of Ty.ty
| Tarrow of binder list * type_c
and type_c =
{ c_result_type : type_v;
c_effect : effect;
c_pre : pre;
c_post : post; }
and binder = Term.vsymbol * type_v
val tpure : Ty.ty -> type_v
val tarrow : binder list -> type_c -> type_v
(* environments *)
......@@ -79,25 +53,3 @@ val t_True : env -> term
val type_v_unit : env -> type_v
val purify : env -> type_v -> ty
val apply_type_v : env -> type_v -> vsymbol -> type_c
val apply_type_v_ref : env -> type_v -> reference -> type_c
val occur_type_v : reference -> type_v -> bool
val v_result : ty -> vsymbol
val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
val post_map : (fmla -> fmla) -> post -> post
val subst1 : vsymbol -> term -> term Mvs.t
val eq_type_v : type_v -> type_v -> bool
(* pretty-printers *)
val print_type_v : Format.formatter -> type_v -> unit
val print_type_c : Format.formatter -> type_c -> unit
val print_post : Format.formatter -> post -> unit
......@@ -61,6 +61,7 @@
"label", LABEL;
"let", LET;
"match", MATCH;
"module", MODULE;
"not", NOT;
"of", OF;
"parameter", PARAMETER;
......
......@@ -118,7 +118,7 @@
%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 NOT OF PARAMETER
%token FUN GHOST IF IN INVARIANT LABEL LET MATCH MODULE NOT OF PARAMETER
%token RAISE RAISES READS REC
%token THEN TO TRY TYPE VARIANT WHILE WITH WRITES
......@@ -178,7 +178,26 @@
%%
file:
| list0_decl EOF { $1 }
| list0_module_ EOF { $1 }
;
list0_module_:
| /* epsilon */
{ [] }
| list1_module_
{ $1 }
;
list1_module_:
| module_
{ [$1] }
| module_ list1_module_
{ $1 :: $2 }
;
module_:
| MODULE uident list0_decl END
{ { mod_name = $2; mod_decl = $3 } }
;
list0_decl:
......
......@@ -108,5 +108,10 @@ type decl =
| Dparam of ident * type_v
| Dexn of ident * Ptree.pty option
type file = decl list
type module_ = {
mod_name : ident;
mod_decl : decl list;
}
type file = module_ list
......@@ -111,15 +111,15 @@ type rec_variant = Term.vsymbol * Term.term * Term.lsymbol
type reference = Pgm_effect.reference
type pre = Pgm_env.pre
type pre = Pgm_types.pre
type post = Pgm_env.post
type post = Pgm_types.post
type type_v = Pgm_env.type_v
type type_v = Pgm_types.type_v
type type_c = Pgm_env.type_c
type type_c = Pgm_types.type_c
type binder = Pgm_env.binder
type binder = Pgm_types.binder
type loop_annotation = {
loop_invariant : Term.fmla option;
......
Markdown is supported
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