Skip to content

why3
why3
Commit 05ec3de7 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

Typing.env -> Theory.env et est dans context

parent 2b415341
Hide whitespace changes
Inline Side-by-side
Showing with 264 additions and 301 deletions
Makefile.in
View file @ 05ec3de7
......@@ -110,7 +110,7 @@ CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
UTIL_CMO := pp.cmo loc.cmo util.cmo hashcons.cmo
UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))
PARSER_CMO := parser.cmo lexer.cmo typing.cmo transform_utils.cmo
PARSER_CMO := parser.cmo lexer.cmo typing.cmo
PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
TRANSFORM_CMO := transform.cmo simplify_recursive_definition.cmo \
......@@ -531,7 +531,7 @@ binary: $(ALLBINARYFILES)
headers:
headache -c misc/headache_config.txt -h misc/header.txt \
Makefile.in configure.in \
*/*.ml */*.ml[ily4] */*/*.ml */*/*.ml[ily4]
*/*.ml */*/*.ml */*/*.ml[ily4]
# myself
########
......
src/core/theory.ml
View file @ 05ec3de7
......@@ -144,6 +144,7 @@ and namespace = {
}
and context = {
ctxt_env : env;
ctxt_decl : decl;
ctxt_prev : context option;
ctxt_known : decl Mid.t;
......@@ -151,6 +152,14 @@ and context = {
ctxt_tag : int;
}
and env = {
env_retrieve : retrieve_theory;
env_memo : (string list, theory Mnm.t) Hashtbl.t;
env_tag : int;
}
and retrieve_theory = env -> string list -> theory Mnm.t
and decl = {
d_node : decl_node;
d_tag : int;
......@@ -294,13 +303,14 @@ let create_logic_decl ldl =
List.iter check_decl ldl;
create_logic_decl ldl
(** Built-in theory *)
module Ctxt = struct
type t = context
let equal a b = a.ctxt_decl == b.ctxt_decl &&
let equal a b =
a.ctxt_env == b.ctxt_env &&
a.ctxt_decl == b.ctxt_decl &&
match a.ctxt_prev, b.ctxt_prev with
| Some na, Some nb -> na == nb
| None, None -> true
......@@ -311,13 +321,14 @@ module Ctxt = struct
| Some ctxt -> 1 + ctxt.ctxt_tag
| None -> 0
in
Hashcons.combine ctxt.ctxt_decl.d_tag prev
Hashcons.combine2 ctxt.ctxt_decl.d_tag prev ctxt.ctxt_env.env_tag
let tag i ctxt = { ctxt with ctxt_tag = i }
end
module Hctxt = Hashcons.Make(Ctxt)
let mk_context decl prev known cloned = Hctxt.hashcons {
let mk_context env decl prev known cloned = Hctxt.hashcons {
ctxt_env = env;
ctxt_decl = decl;
ctxt_prev = prev;
ctxt_known = known;
......@@ -325,7 +336,9 @@ let mk_context decl prev known cloned = Hctxt.hashcons {
ctxt_tag = -1;
}
let builtin_theory =
let builtin_name = "BuiltIn"
let builtin_theory env =
let decl_int = create_ty_decl [ts_int, Tabstract] in
let decl_real = create_ty_decl [ts_real, Tabstract] in
let decl_equ = create_logic_decl [Lpredicate (ps_equ, None)] in
......@@ -336,10 +349,10 @@ let builtin_theory =
let kn_equ = Mid.add ps_equ.ls_name decl_equ kn_real in
let kn_neq = Mid.add ps_neq.ls_name decl_neq kn_equ in
let ctxt_int = mk_context decl_int None kn_int Mid.empty in
let ctxt_real = mk_context decl_real (Some ctxt_int) kn_real Mid.empty in
let ctxt_equ = mk_context decl_equ (Some ctxt_real) kn_equ Mid.empty in
let ctxt_neq = mk_context decl_neq (Some ctxt_equ) kn_neq Mid.empty in
let ctxt_int = mk_context env decl_int None kn_int Mid.empty in
let ctxt_real = mk_context env decl_real (Some ctxt_int) kn_real Mid.empty in
let ctxt_equ = mk_context env decl_equ (Some ctxt_real) kn_equ Mid.empty in
let ctxt_neq = mk_context env decl_neq (Some ctxt_equ) kn_neq Mid.empty in
let ns_int = Mnm.add ts_int.ts_name.id_short ts_int Mnm.empty in
let ns_real = Mnm.add ts_real.ts_name.id_short ts_real ns_int in
......@@ -349,12 +362,42 @@ let builtin_theory =
let export = { ns_ts = ns_real; ns_ls = ns_neq;
ns_pr = Mnm.empty; ns_ns = Mnm.empty } in
{ th_name = id_register (id_fresh "BuiltIn");
{ th_name = id_register (id_fresh builtin_name);
th_ctxt = ctxt_neq;
th_export = export;
th_local = Sid.empty }
let use_builtin = create_use_decl builtin_theory
(** Environments *)
let create_env =
let r = ref 0 in
fun retrieve ->
incr r;
let env =
{ env_retrieve = retrieve;
env_memo = Hashtbl.create 17;
env_tag = !r; }
in
let builtin = builtin_theory env in
let m = Mnm.add builtin.th_name.id_short builtin Mnm.empty in
Hashtbl.add env.env_memo [] m;
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))
(** Context constructors and utilities *)
......@@ -375,10 +418,8 @@ let empty_inst = {
module Context = struct
let init_context =
let known = builtin_theory.th_ctxt.ctxt_known in
let known = Mid.add builtin_theory.th_name use_builtin known in
mk_context use_builtin None known Mid.empty
let init_context env =
(find_theory env [] builtin_name).th_ctxt
let push_decl ctxt kn d =
let get_cl m id = try Mid.find id m with Not_found -> Sid.empty in
......@@ -391,7 +432,7 @@ module Context = struct
List.fold_left (add_cl m) ctxt.ctxt_cloned sl
| _ -> ctxt.ctxt_cloned
in
mk_context d (Some ctxt) kn cloned
mk_context ctxt.ctxt_env d (Some ctxt) kn cloned
(* Manage known symbols *)
......@@ -772,15 +813,15 @@ module TheoryUC = struct
(* Manage theories *)
let create_theory n = {
uc_name = n;
uc_ctxt = Context.init_context;
uc_import = [builtin_theory.th_export];
uc_export = [builtin_theory.th_export];
uc_local = Sid.empty;
}
let create_theory env n =
let builtin = find_theory env [] builtin_name in
{ uc_name = n;
uc_ctxt = builtin.th_ctxt;
uc_import = [builtin.th_export];
uc_export = [builtin.th_export];
uc_local = Sid.empty; }
let create_theory n = create_theory (id_register n)
let create_theory env n = create_theory env (id_register n)
let close_theory uc = match uc.uc_export with
| [e] ->
......
src/core/theory.mli
View file @ 05ec3de7
......@@ -95,6 +95,7 @@ and namespace = private {
}
and context = private {
ctxt_env : env;
ctxt_decl : decl;
ctxt_prev : context option;
ctxt_known : decl Mid.t;
......@@ -102,6 +103,8 @@ and context = private {
ctxt_tag : int;
}
and env
and decl = private {
d_node : decl_node;
d_tag : int;
......@@ -134,6 +137,16 @@ exception IllegalConstructor of lsymbol
exception UnboundVars of Svs.t
exception BadDecl of ident
(** Environements *)
type retrieve_theory = env -> string list -> theory Mnm.t
val create_env : retrieve_theory -> env
exception TheoryNotFound of string list * string
val find_theory : env -> string list -> string -> theory
(** Context constructors and utilities *)
type th_inst = {
......@@ -147,7 +160,7 @@ val empty_inst : th_inst
module Context : sig
val init_context : context
val init_context : env -> context
val add_decl : context -> decl -> context
......@@ -172,13 +185,11 @@ end
(** Theory constructors and utilities *)
val builtin_theory : theory
type theory_uc (* a theory under construction *)
module TheoryUC : sig
val create_theory : preid -> theory_uc
val create_theory : env -> preid -> theory_uc
val close_theory : theory_uc -> theory
val add_decl : theory_uc -> decl -> theory_uc
......@@ -197,6 +208,8 @@ module TheoryUC : sig
end
val builtin_name : string
(** Debugging *)
val print_ident : Format.formatter -> ident -> unit
......
src/main.ml
View file @ 05ec3de7
......@@ -50,9 +50,9 @@ let () =
let in_emacs = Sys.getenv "TERM" = "dumb"
let transformation env l =
let t1 = Simplify_recursive_definition.t env in
let t2 = Inlining.all env in
let transformation l =
let t1 = Simplify_recursive_definition.t in
let t2 = Inlining.all in
List.map (fun (t,c) ->
let c = if !simplify_recursive
then Transform.apply t1 c
......@@ -76,25 +76,16 @@ let rec report fmt = function
Driver.report fmt e
| e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
let type_file env file =
if !parse_only then begin
let c = open_in file in
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let _ = Lexer.parse_logic_file lb in
close_in c;
env
end else
Typing.add_from_file env file
let extract_goals env ctxt =
Transform.apply (Transform.split_goals env) ctxt
let extract_goals ctxt =
Transform.apply Transform.split_goals ctxt
let transform env l =
let l = List.map
(fun t -> t, Context.use_export Context.init_context t)
(Typing.local_theories l) in
let l = transformation env l in
let l =
List.map
(fun t -> t, Context.use_export (Context.init_context env) t)
l
in
let l = transformation l in
if !print_stdout then
List.iter
(fun (t,ctxt) -> Pretty.print_named_context
......@@ -105,7 +96,7 @@ let transform env l =
| Some file ->
let drv = load_driver file env in
begin match l with
| (_,ctxt) :: _ -> begin match extract_goals env ctxt with
| (_,ctxt) :: _ -> begin match extract_goals ctxt with
| g :: _ ->
Driver.print_context drv std_formatter g
| [] ->
......@@ -114,11 +105,23 @@ let transform env l =
| [] -> ()
end
let type_file env file =
if !parse_only then begin
let c = open_in file in
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let _ = Lexer.parse_logic_file lb in
close_in c
end else begin
let m = Typing.read_file env file in
let l = Mnm.fold (fun _ th acc -> th :: acc) m [] in
transform env l
end
let () =
try
let env = Typing.create !loadpath in
let l = List.fold_left type_file env !files in
transform env l
let env = create_env (Typing.retrieve !loadpath) in
List.iter (type_file env) !files
with e when not !debug ->
eprintf "%a@." report e;
exit 1
......
src/output/alt_ergo.ml
View file @ 05ec3de7
......@@ -123,7 +123,6 @@ let print_type_decl fmt = function
assert false
let ac_th = ["algebra";"AC"]
open Transform_utils
let print_logic_decl drv ctxt fmt = function
| Lfunction (ls, None) ->
......
src/output/alt_ergo.mli
View file @ 05ec3de7
......@@ -16,3 +16,4 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
src/output/driver.ml
View file @ 05ec3de7
......@@ -90,7 +90,7 @@ and driver = {
(* the first is the translation only for this ident, the second is also for representant *)
drv_theory : (translation * translation) Hid.t;
drv_with_ctxt : translation Hid.t;
drv_env : Typing.env;
drv_env : env;
}
......@@ -128,7 +128,7 @@ let string_of_qualid thl idl =
let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} =
let id,qfile = qualid_to_slist qualid in
let th = try
Typing.find_theory env qfile id
find_theory env qfile id
with Not_found -> errorm ~loc "theory %s not found"
(String.concat "." qualid) in
let add_htheory cloned id t =
......@@ -207,7 +207,7 @@ let load_driver file env =
in
List.iter add f.f_global;
let driver = { drv_printer = !printer;
drv_context = Context.init_context;
drv_context = Context.init_context env;
drv_call_stdin = !call_stdin;
drv_call_file = !call_file;
drv_regexps = !regexps;
......
src/output/driver.mli
View file @ 05ec3de7
......@@ -25,7 +25,7 @@ open Theory
type driver
val load_driver : string -> Typing.env -> driver
val load_driver : string -> env -> driver
(** querying drivers *)
......
src/output/why3.mli
View file @ 05ec3de7
......@@ -16,3 +16,4 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
src/parser/transform_utils.ml deleted 100644 → 0
View file @ 2b415341
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* 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 Ty
open Term
open Theory
let cloned_from_ts env ctxt l s ls1 =
assert false (*TODO*)
(* try *)
(* let th = Typing.find_theory env l in *)
(* let ls2 = Mnm.find s th.th_export.ns_ts in *)
(* Context_utils.cloned_from ctxt ls1.ts_name ls2.ts_name *)
(* with Loc.Located _ -> assert false *)
let cloned_from_ls env ctxt l s ls1 =
assert false (*TODO*)
(* try *)
(* let th = Typing.find_theory env l in *)
(* let ls2 = Mnm.find s th.th_export.ns_ls in *)
(* Context_utils.cloned_from ctxt ls1.ls_name ls2.ls_name *)
(* with Loc.Located _ -> assert false *)
let cloned_from_pr env ctxt l s pr1 =
assert false (*TODO*)
(* try *)
(* let th = Typing.find_theory env l in *)
(* let pr2 = Mnm.find s th.th_export.ns_pr in *)
(* Context_utils.cloned_from ctxt pr1.pr_name pr2.pr_name *)
(* with Loc.Located _ -> assert false *)
src/parser/transform_utils.mli deleted 100644 → 0
View file @ 2b415341
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* 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. *)
(* *)
(**************************************************************************)
val cloned_from_ts : Typing.env -> Theory.context ->
string list -> string list -> Ty.tysymbol -> bool
val cloned_from_ls : Typing.env -> Theory.context ->
string list -> string list -> Term.lsymbol -> bool
val cloned_from_pr : Typing.env -> Theory.context ->
string list -> string list -> Theory.prop -> bool
src/parser/typing.ml
View file @ 05ec3de7
......@@ -127,18 +127,6 @@ let report fmt = function
module S = Set.Make(String)
module M = Map.Make(String)
type env = {
loadpath : string list;
loaded_theories : (string list, theory M.t) Hashtbl.t;
theories : theory M.t; (* local theories *)
}
let create lp = {
loadpath = lp;
loaded_theories = Hashtbl.create 17;
theories = M.empty;
}
(** typing using destructive type variables
parsed trees intermediate trees typed trees
......@@ -1032,14 +1020,6 @@ let add_inductives dl th =
let dl = List.map type_decl dl in
add_decl th (create_ind_decl dl)
let locate_file env sl =
let f = List.fold_left Filename.concat "" sl ^ ".why" in
let fl = List.map (fun dir -> Filename.concat dir f) env.loadpath in
match List.filter Sys.file_exists fl with
| [] -> raise Not_found
| [file] -> file
| file1 :: file2 :: _ -> error (AmbiguousPath (file1, file2))
(* parse file and store all theories into parsed_theories *)
let load_channel file c =
......@@ -1058,34 +1038,24 @@ let prop_kind = function
| Kgoal -> Pgoal
| Klemma -> Plemma
let rec find_theory env q id = match q with
let find_theory env lenv q id = match q with
| [] ->
(* local theory *)
M.find id env.theories
begin try Mnm.find id lenv
with Not_found -> Theory.find_theory env [] id end
| _ :: _ ->
(* theory in file f *)
if not (Hashtbl.mem env.loaded_theories q) then begin
Hashtbl.add env.loaded_theories q M.empty;
let file = locate_file env q in
let tl = load_file file in
let long = String.concat "." q in
let env' = { env with theories = M.empty } in
let env' = List.fold_left (type_and_add_theory long) env' tl in
Hashtbl.replace env.loaded_theories q env'.theories;
end;
let h = Hashtbl.find env.loaded_theories q in
M.find id h
and type_theory env q id pt =
let long = if q = "" then id.id else q ^ "." ^ id.id in
let n = id_user_long id.id long id.id_loc in
let th = create_theory n in
let th = add_decls env th pt.pt_decl in
Theory.find_theory env q id
let rec type_theory env lenv id pt =
let n = id_user id.id id.id_loc in
let th = create_theory env n in
let th = add_decls env lenv th pt.pt_decl in
close_theory th
and add_decls env th = List.fold_left (add_decl env) th
and add_decls env lenv th = List.fold_left (add_decl env lenv) th
and add_decl env th = function
and add_decl env lenv th = function
| TypeDecl dl ->
add_types dl th
| LogicDecl dl ->
......@@ -1098,9 +1068,9 @@ and add_decl env th = function
let q, id = split_qualid use.use_theory in
let t =
try
find_theory env q id
find_theory env lenv q id
with
| Not_found -> error ~loc (UnboundTheory use.use_theory)
| TheoryNotFound _ -> error ~loc (UnboundTheory use.use_theory)
| Error (AmbiguousPath _ as e) -> error ~loc e
in
let use_or_clone th = match subst with
......@@ -1165,38 +1135,37 @@ and add_decl env th = function
None
in
let th = open_namespace th in
let th = add_decls env th dl in
let th = add_decls env lenv th dl in
close_namespace th import id
and add_theory env th =
let id = th.th_name.id_short in
if M.mem id env.theories then error (ClashTheory id);
{ env with theories = M.add id th env.theories }
and type_and_add_theory q env pt =
and type_and_add_theory env lenv pt =
let id = pt.pt_name in
try
let th = type_theory env q id pt in
add_theory env th
with
| Error (ClashTheory _ as e) -> error ~loc:id.id_loc e
if Mnm.mem id.id lenv || id.id = builtin_name then error (ClashTheory id.id);
let th = type_theory env lenv id pt in
Mnm.add id.id th lenv
let clear_local_theories env =
{ env with theories = M.empty }
let type_theories env tl =
List.fold_left (type_and_add_theory env) Mnm.empty tl
let add_local_theories env tl =
List.fold_left (type_and_add_theory "") env tl
let add_from_file env file =
let read_file env file =
let tl = load_file file in
add_local_theories env tl
type_theories env tl
let add_from_channel env file ic =
let read_channel env file ic =
let tl = load_channel file ic in
add_local_theories env tl
type_theories env tl
let locate_file lp sl =
let f = List.fold_left Filename.concat "" sl ^ ".why" in
let fl = List.map (fun dir -> Filename.concat dir f) lp in
match List.filter Sys.file_exists fl with
| [] -> raise Not_found
| [file] -> file
| file1 :: file2 :: _ -> error (AmbiguousPath (file1, file2))
let local_theories env =
List.rev (M.fold (fun _ v acc -> v::acc) env.theories [])
let retrieve lp env sl =
let file = locate_file lp sl in
read_file env file
(*
Local Variables:
......
src/parser/typing.mli
View file @ 05ec3de7
......@@ -19,29 +19,14 @@
(** Typing environments *)
type env
open Theory
val create : string list -> env
val retrieve : string list -> retrieve_theory
(** creates a new typing environment for a given loadpath *)
val add_theory : env -> Theory.theory -> env
(** adds a local theory *)
val read_file : env -> string -> theory Mnm.t
val clear_local_theories : env -> env
(** clears the local theories *)
val add_from_file : env -> string -> env
(** adds local theories from a given file *)
val add_from_channel : env -> string -> in_channel -> env
(** [add_from_channel env filename ic] adds local theories
from a given input channel [ic]; [filename] is only used for
locations *)
val find_theory : env -> string list -> string -> Theory.theory
(** searches for a theory using the environment's loadpath *)
val local_theories : env -> Theory.theory list
val read_channel : env -> string -> in_channel -> theory Mnm.t
(** error reporting *)
......
src/test.why
View file @ 05ec3de7
......@@ -5,7 +5,7 @@ theory Test
use import prelude.Int
logic id(x: int) : int = x
logic even(x: int) = 2*(x/2) = x
goal G : forall x:int. even(4)
goal G : (0 : BuiltIn.int) = 0
end
(*
......
src/transform/flatten.ml
View file @ 05ec3de7
......@@ -30,5 +30,5 @@ let elt a =
(*Format.printf "flat %a : %a@\n" Pretty.print_decl a Pretty.print_decl_list r;*)
r
let t = Transform.elt elt
let t env = Transform.elt (fun _ -> elt) env
src/transform/flatten.mli
View file @ 05ec3de7
......@@ -19,4 +19,4 @@
(* a list of decl_or_use to a list of decl *)
val t : Typing.env -> Transform.ctxt_t
val t : Transform.ctxt_t
src/transform/inlining.ml
View file @ 05ec3de7
......@@ -118,8 +118,8 @@ let fold isnotinlinedt isnotinlinedf ctxt0 (env, ctxt) =
(create_prop (id_dup pr.pr_name) (replacep env pr.pr_fmla)))
| Duse _ | Dclone _ -> env,add_decl ctxt d
let t ~isnotinlinedt ~isnotinlinedf env =
Transform.fold_map (fun _ -> fold isnotinlinedt isnotinlinedf) empty_env env
let t ~isnotinlinedt ~isnotinlinedf =
Transform.fold_map (fold isnotinlinedt isnotinlinedf) empty_env
let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)
......
src/transform/inlining.mli
View file @ 05ec3de7
......@@ -23,18 +23,17 @@
val t :
isnotinlinedt:(Term.term -> bool) ->
isnotinlinedf:(Term.fmla -> bool) ->
Typing.env ->
Transform.ctxt_t
(* Inline them all *)
val all : Typing.env -> Transform.ctxt_t
val all : Transform.ctxt_t
(* Inline only the trivial definition :
logic c : t = a
logic f(x : t,...., ) : t = g(y : t2,...) *)
val trivial : Typing.env -> Transform.ctxt_t
val trivial : Transform.ctxt_t
(* Function to use in other transformations if inlining is needed *)
......