Commit ccdb4088 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: type marks

parent 5ffac0d8
......@@ -394,7 +394,7 @@ install_local: bin/why3
########
MLW_FILES = mlw_ty mlw_expr mlw_decl mlw_module mlw_pretty \
mlw_dtree mlw_dty mlw_typing mlw_main
mlw_wp mlw_dtree mlw_dty mlw_typing mlw_main
MLWMODULES = $(addprefix src/whyml/, $(MLW_FILES))
......
......@@ -93,7 +93,7 @@ and dexpr_desc =
| DEtry of dexpr * (xsymbol * ident * dexpr) list
| DEfor of ident * dexpr * Ptree.for_direction * dexpr * dinvariant * dexpr
| DEassert of Ptree.assertion_kind * Ptree.lexpr
| DEmark of string * dexpr
| DEmark of ident * dexpr
(* | DEany of dutype_c *)
and drecfun = ident * dity * dlambda
......
......@@ -215,8 +215,18 @@ let clone_export_theory uc th i =
let add_meta uc m al =
{ uc with muc_theory = Theory.add_meta uc.muc_theory m al }
let th_unit =
let ts = create_tysymbol (id_fresh "unit") [] (Some ty_unit) in
let uc = create_theory (id_fresh "Unit") in
let uc = Theory.use_export uc (tuple_theory 0) in
let uc = Theory.add_ty_decl uc ts in
close_theory uc
let create_module ?(path=[]) n =
use_export_theory (empty_module n path) bool_theory
let m = empty_module n path in
let m = use_export_theory m bool_theory in
let m = use_export_theory m th_unit in
m
(** Program decls *)
......
......@@ -438,9 +438,12 @@ let create_itysymbol name ?(abst=false) ?(priv=false) args regs def =
its_abst = abst;
its_priv = priv }
let ts_unit = ts_tuple 0
let ty_unit = ty_tuple []
let ity_int = ity_of_ty Ty.ty_int
let ity_bool = ity_of_ty Ty.ty_bool
let ity_unit = ity_of_ty (Ty.ty_tuple [])
let ity_unit = ity_of_ty ty_unit
let vars_freeze s =
let sbs = Stv.fold (fun v -> Mtv.add v (ity_var v)) s.vars_tv Mtv.empty in
......
......@@ -136,6 +136,9 @@ val ity_v_any : (tvsymbol -> bool) -> (region -> bool) -> ity -> bool
val ity_closed : ity -> bool
val ity_pure : ity -> bool
val ts_unit : tysymbol
val ty_unit : ty
val ity_int : ity
val ity_bool : ity
val ity_unit : ity
......
......@@ -34,6 +34,7 @@ open Mlw_expr
open Mlw_decl
open Mlw_pretty
open Mlw_module
open Mlw_wp
open Mlw_dty
(** errors *)
......@@ -128,10 +129,11 @@ let rec dity_of_pty ~user denv = function
(** Typing program expressions *)
let dity_int = ts_app ts_int []
let dity_int = ts_app ts_int []
let dity_real = ts_app ts_real []
let dity_bool = ts_app ts_bool []
let dity_unit = ts_app (ts_tuple 0) []
let dity_unit = ts_app ts_unit []
let dity_mark = ts_app ts_mark []
let expected_type ?(weak=false) e dity =
unify ~weak e.dexpr_type dity
......@@ -307,12 +309,6 @@ and dpat_app denv ({ dexpr_loc = loc } as de) ppl =
Loc.try2 loc unify de.dexpr_type (make_arrow_type tyl res);
pp, res, denv
(* value restriction *)
let rec is_fun e = match e.dexpr_desc with
| DEfun _ -> true
| DEmark (_, e) -> is_fun e
| _ -> false
let dexpr_app e el =
let res = create_type_variable () in
let tyl = List.map (fun a -> a.dexpr_type) el in
......@@ -342,7 +338,9 @@ and dexpr_desc denv loc = function
| Ptree.Elet (id, e1, e2) ->
let e1 = dexpr denv e1 in
let dity = e1.dexpr_type in
let tvars = if is_fun e1 then denv.tvars else add_tvars denv.tvars dity in
let tvars = match e1.dexpr_desc with
| DEfun _ -> denv.tvars
| _ -> add_tvars denv.tvars dity in
let locals = Mstr.add id.id (tvars, dity) denv.locals in
let denv = { denv with locals = locals; tvars = tvars } in
let e2 = dexpr denv e2 in
......@@ -476,12 +474,13 @@ and dexpr_desc denv loc = function
DEabsurd, create_type_variable ()
| Ptree.Eassert (ak, lexpr) ->
DEassert (ak, lexpr), dity_unit
| Ptree.Emark (id, e1) ->
let e1 = dexpr denv e1 in
DEmark (id, e1), e1.dexpr_type
| Ptree.Eloop (_ann, _e1) ->
assert false (*TODO*)
| Ptree.Efor (_id, _e1, _dir, _e2, _lexpr_opt, _e3) ->
assert false (*TODO*)
| Ptree.Emark (_id, _e1) ->
assert false (*TODO*)
| Ptree.Eany (_type_c) ->
assert false (*TODO*)
| Ptree.Eabstract (_e1, _post) ->
......@@ -545,8 +544,10 @@ let create_post lenv x ty f =
let res = create_vsymbol (id_fresh x) ty in
let log_vars = Mstr.add x res lenv.log_vars in
let log_denv = Typing.add_var x (dty_of_ty ty) lenv.log_denv in
let f = Typing.type_fmla (get_theory lenv.mod_uc) log_denv log_vars f in
create_post res f
(* FIXME? We could add th_mark in create_lenv, but then at/old
would be available in preconditions, variants, etc... *)
let th = Theory.use_export (get_theory lenv.mod_uc) Mlw_wp.th_mark in
create_post res (Typing.type_fmla th log_denv log_vars f)
let create_pre lenv f =
Typing.type_fmla (get_theory lenv.mod_uc) lenv.log_denv lenv.log_vars f
......@@ -646,6 +647,10 @@ let rec expr lenv de = match de.dexpr_desc with
let lenv = add_local id.id (LetV pv) lenv in
xs, pv, expr lenv de in
e_try e1 (List.map branch bl)
| DEmark (x, de1) ->
let ld = create_let_defn (Denv.create_user_id x) e_setmark in
let lenv = add_local x.id ld.let_var lenv in
e_let ld (expr lenv de1)
| _ ->
assert false (*TODO*)
......@@ -674,7 +679,7 @@ and expr_lam lenv (bl, var, p, e, q, xq) =
let lenv = List.fold_right add_binder pvl lenv in
let e = expr lenv e in
let ty = match e.e_vty with
| VTarrow _ -> ty_tuple []
| VTarrow _ -> ty_unit
| VTvalue vtv -> ty_of_ity vtv.vtv_ity in
let mk_variant (t,r) = { v_term = create_pre lenv t; v_rel = r } in
let add_exn m (xs,f) =
......
(**************************************************************************)
(* *)
(* 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 Ty
open Term
open Theory
open Mlw_ty
open Mlw_ty.T
open Mlw_expr
(** WP-only builtins *)
let ts_mark = create_tysymbol (id_fresh "'mark") [] None
let ty_mark = ty_app ts_mark []
let fs_at =
let ty = ty_var (create_tvsymbol (id_fresh "a")) in
create_lsymbol (id_fresh "at") [ty; ty_mark] (Some ty)
let fs_old =
let ty = ty_var (create_tvsymbol (id_fresh "a")) in
create_lsymbol (id_fresh "old") [ty] (Some ty)
let th_mark =
let uc = create_theory (id_fresh "WP builtins") in
let uc = add_ty_decl uc ts_mark in
let uc = add_param_decl uc fs_at in
let uc = add_param_decl uc fs_old in
close_theory uc
let fs_setmark =
create_lsymbol (id_fresh "set_mark") [] (Some ty_mark)
let e_setmark = e_lapp fs_setmark [] (ity_pur ts_mark [])
let vs_old = create_vsymbol (id_fresh "'old") ty_mark
let vs_now = create_vsymbol (id_fresh "'now") ty_mark
(**************************************************************************)
(* *)
(* 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
(** WP-only builtins *)
val ts_mark : Ty.tysymbol
val ty_mark : Ty.ty
val fs_old : Term.lsymbol
val fs_at : Term.lsymbol
val th_mark : Theory.theory
val fs_setmark : Term.lsymbol
val e_setmark : Mlw_expr.expr
......@@ -16,8 +16,6 @@ module N
use import M
goal G1: f 41 = 42
type unit = ()
type tree 'a = Node 'a (forest 'a) | Leaf
with forest 'a = Cons (tree 'a) (forest 'a) | Nil
......@@ -32,10 +30,12 @@ module N
let create_dref i = {| dcontents = {| contents = i |} |}
let myfun r = { r = r }
let rec on_tree t = match t with
'L:
let rec on_tree t = { true } match t with
| Node {| contents = v |} f -> v + on_forest f
| Leaf -> raise (Exit Leaf)
end with on_forest f = match f with
end { at r 'L = t }
with on_forest f = match f with
| Cons t f -> let ee = Leaf in on_tree t + on_forest f + on_tree ee
| Nil -> 1
end
......@@ -46,7 +46,7 @@ module N
dr.dcontents <- nr;
assert { r = r };
try on_tree r with Exit -> 0 end
{ result = 0 }
{ old result = 0 }
end
(*
......
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