export de fonctions de Typing pour les programmes

parent 3a2b06b6
......@@ -167,7 +167,7 @@ test: bin/why.byte
--call --goal Test.G src/test.why --timeout 3
testl: bin/whyl.byte
ocamlrun -bt bin/whyl.byte src/programs/test.mlw
ocamlrun -bt bin/whyl.byte -I lib/prelude/ src/programs/test.mlw
# programs
##########
......
......@@ -47,17 +47,19 @@ let create_env =
exception TheoryNotFound of string list * string
let find_theory env sl s =
let m =
try
Hashtbl.find env.env_memo sl
with Not_found ->
Hashtbl.add env.env_memo sl Mnm.empty;
let m = env.env_retrieve env sl in
Hashtbl.replace env.env_memo sl m;
m
in
try Mnm.find s m
with Not_found -> raise (TheoryNotFound (sl, s))
try
let m =
try
Hashtbl.find env.env_memo sl
with Not_found ->
Hashtbl.add env.env_memo sl Mnm.empty;
let m = env.env_retrieve env sl in
Hashtbl.replace env.env_memo sl m;
m
in
Mnm.find s m
with Not_found ->
raise (TheoryNotFound (sl, s))
let env_tag env = env.env_tag
......@@ -29,6 +29,11 @@ val read_file : env -> string -> theory Mnm.t
val read_channel : env -> string -> in_channel -> theory Mnm.t
(** incremental parsing *)
val add_decl : env -> theory Mnm.t -> theory_uc -> Ptree.decl -> theory_uc
val fmla : theory_uc -> Ptree.lexpr -> Term.fmla
(** error reporting *)
type error
......
......@@ -31,21 +31,32 @@ let rec report fmt = function
fprintf fmt "syntax error"
| Typing.Error e ->
Typing.report fmt e
| e ->
| e ->
fprintf fmt "anomaly: %s" (Printexc.to_string e)
open Pgm_ptree
open Theory
let env = Env.create_env (Typing.retrieve !loadpath)
let type_file file =
let c = open_in file in
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let _ = Pgm_lexer.parse_file lb in
let p = Pgm_lexer.parse_file lb in
close_in c;
if !parse_only then raise Exit;
let uc = Theory.create_theory (Ident.id_fresh "Pgm") in
let _uc =
List.fold_left
(fun uc d -> match d with
| LogicDecl dl -> List.fold_left (Typing.add_decl env Mnm.empty) uc dl)
uc p
in
()
let handle_file file =
try
(* let env = create_env (Typing.retrieve !loadpath) in *)
type_file file
with Exit ->
()
......
(* test file for ML-why *)
{ logic f(int) : int }
{
use import prelude.Int
logic f(int) : int
logic g(x : int) : int = f(x+1)
}
{
axiom A : forall x:int. f(x) = g(x-1)
}
{ }
(*
Local Variables:
......
......@@ -14,7 +14,8 @@ theory Test
logic succ(x:int) : int = id(x+1)
logic even(x: int) = 2*(x/2) = x
clone ThA with type test = int, logic test = (-_)
goal G : forall x:int. 1 = succ(id2(zero))
goal G : (forall x:int. x=x) or
(forall x:int. x=x+1)
goal G2 : forall x:int. 0 = 1
end
......
......@@ -107,7 +107,8 @@ let fold isnotinlinedt isnotinlinedf task0 (env, task) =
env,add_decl task (create_prop_decl k pr (replacep env f))
let t ~isnotinlinedt ~isnotinlinedf =
Register.store (fun () -> Trans.fold_map (fold isnotinlinedt isnotinlinedf) empty_env None)
Register.store
(fun () -> Trans.fold_map (fold isnotinlinedt isnotinlinedf) empty_env None)
let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)
......
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