Commit 44e05191 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

programs: setting the code structure for WP

parent f20fd8d4
open Why
open Util
open Ident
open Term
open Pgm_ttree
module Reference = struct
type t = reference
module Vsym = OrderedHash(struct
type t = vsymbol
let tag vs = vs.vs_name.id_tag
end)
module Lsym = OrderedHash(struct
type t = lsymbol
let tag ls = ls.ls_name.id_tag
end)
let compare r1 r2 = match r1, r2 with
| Rlocal v1, Rlocal v2 -> Vsym.compare v1 v2
| Rglobal l1, Rglobal l2 -> Lsym.compare l1 l2
| Rlocal _, Rglobal _ -> -1
| Rglobal _, Rlocal _ -> 1
end
module R = Set.Make(Reference)
module E = Term.Sls
type t = {
reads : R.t;
writes : R.t;
raises : E.t;
}
let empty = { reads = R.empty; writes = R.empty; raises = E.empty }
let file dl = dl
open Why
open Term
open Pgm_ttree
module R : Set.S with type elt = reference
type t = private {
reads : R.t;
writes : R.t;
raises : Sls.t;
}
val empty : t
val file : Pgm_ttree.file -> Pgm_itree.file
......@@ -3,4 +3,63 @@ open Why
(* intermediate trees for weakest preconditions *)
type file = Pgm_ttree.file
type loc = Loc.position
type assertion_kind = Pgm_ptree.assertion_kind
type lazy_op = Pgm_ptree.lazy_op
type variant = Pgm_ttree.variant
type reference = Pgm_ttree.reference
type effect = Pgm_ttree.effect
type pre = Pgm_ttree.pre
type post = Pgm_ttree.post
type type_v = Pgm_ttree.type_v
type type_c = Pgm_ttree.type_c
type binder = Pgm_ttree.binder
type loop_annotation = Pgm_ttree.loop_annotation
type expr = {
expr_desc : expr_desc;
expr_type : Ty.ty;
expr_effect: Pgm_effect.t;
expr_loc : loc;
}
and expr_desc =
| Elogic of Term.term
| Efun of binder list * triple
| Elet of Term.vsymbol * expr * expr
| Eletrec of recfun list * expr
| Esequence of expr * expr
| Eif of expr * expr * expr
| Ewhile of expr * loop_annotation * expr
| Elazy of lazy_op * expr * expr
| Ematch of expr list * (Term.pattern list * expr) list
| Eskip
| Eabsurd
| Eraise of Term.lsymbol * expr option
| Etry of expr * (Term.lsymbol * Term.vsymbol option * expr) list
| Eassert of assertion_kind * Term.fmla
| Eghost of expr
| Elabel of string * expr
| Eany of type_c
and recfun = Term.vsymbol * binder list * variant option * triple
and triple = pre * expr * post
type decl =
| Dlet of Term.lsymbol * expr
| Dletrec of (Term.lsymbol * recfun) list
| Dparam of Term.lsymbol * type_v
type file = decl list
......@@ -74,7 +74,6 @@ let type_file file =
let th = Env.find_theory env ["programs"] "Prelude" in
let uc = Theory.use_export uc th in
let uc, dl = Pgm_typing.file env uc p in
let dl = Pgm_effect.file dl in
if !type_only then raise Exit;
let th = Pgm_wp.file uc dl in
printf "%a@." Pretty.print_theory th;
......
......@@ -2,4 +2,4 @@
open Why
open Theory
val file : theory_uc -> Pgm_itree.file -> theory
val file : theory_uc -> Pgm_ttree.file -> theory
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