programs: setting the code structure for WP (yes, at last)

parent 5e9c2251
......@@ -196,7 +196,8 @@ clean::
PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
src/programs/pgm_parser.output src/programs/pgm_lexer.ml
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_typing pgm_main
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_typing \
pgm_itree pgm_effect pgm_wp pgm_main
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
......
open Why
let file dl = dl
open Why
val file : Pgm_ttree.file -> Pgm_itree.file
open Why
(* intermediate trees for weakest preconditions *)
type file = Pgm_ttree.file
......@@ -73,9 +73,10 @@ let type_file file =
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 uc, _dl = Pgm_typing.file env uc p 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 = Theory.close_theory uc in
let th = Pgm_wp.file uc dl in
printf "%a@." Pretty.print_theory th;
()
......
......@@ -177,6 +177,8 @@ type decl =
| Dletrec of (Term.lsymbol * recfun) list
| Dparam of Term.lsymbol * type_v
type file = decl list
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
......
open Why
open Theory
type error
exception Error of error
val report : Format.formatter -> error -> unit
val file : Env.env -> theory_uc -> Pgm_ptree.file -> theory_uc * Pgm_ttree.file
open Why
let file uc _dl =
Theory.close_theory uc
open Why
open Theory
val file : theory_uc -> Pgm_itree.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