Skip to content

GitLab

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

Typing utilise maintenant Theory

parent 022bf4ec
Hide whitespace changes
Inline Side-by-side
Showing with 274 additions and 184 deletions
bench/typing/bad/already_theory2.why
View file @ 5e19909d
theory A end
theory B end
theory C use A use B as A end
theory C use A use A:B end
bench/typing/bad/clash_type1.why 0 → 100644
View file @ 5e19909d
theory A
type t
type t
end
bench/typing/bad/clash_type2.why 0 → 100644
View file @ 5e19909d
theory A
type t
namespace S
type t
end
end
lib/emacs/why.el
View file @ 5e19909d
......@@ -28,7 +28,7 @@
(list
'("(\\*\\([^*]\\|\\*[^)]\\)*\\*)" . font-lock-comment-face)
'("{\\([^}]*\\)}" . font-lock-type-face)
`(,(why-regexp-opt '("use" "open" "include" "inductive" "external" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type")) . font-lock-builtin-face)
`(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type")) . font-lock-builtin-face)
`(,(why-regexp-opt '("let" "rec" "in" "if" "then" "else" "begin" "end" "while" "do" "done" "label" "assert" "try" "with" "theory" "uses")) . font-lock-keyword-face)
; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
)
......
src/main.ml
View file @ 5e19909d
......@@ -53,7 +53,7 @@ let type_file env file =
let () =
try
let env = Env.create [] in
let env = Typing.create [] in
ignore (List.fold_left type_file env !files)
with e ->
eprintf "%a@." report e;
......
src/test.why
View file @ 5e19909d
......@@ -3,20 +3,15 @@
theory A
type t
logic c:t
logic c : t
end
theory B
use import A
logic d : t
logic p : t -> prop
end
theory C
use B
use T : B.A
logic e : T.t
axiom test : B.p(T.c)
namespace S type t end
logic d : S.t
logic f : S.t -> S.t
logic p : S.t -> prop
axiom Ax : forall x:S.t. p(x) or p(f(x))
end
theory Int
......@@ -33,7 +28,7 @@ theory List
logic is_nil : 'a list -> prop
use import Int
type int (* use import Int *)
logic length : 'a list -> int
......@@ -59,10 +54,12 @@ theory Eq
end
(*
theory Test
use Eq
use import L : List
axiom a : forall x : 'a. not Eq.eq(nil, cons(nil, nil))
end
\ No newline at end of file
end
*)
src/theory.ml
View file @ 5e19909d
......@@ -25,7 +25,6 @@ open Term
(** Error reporting *)
type error =
| UnboundNamespace of string
| OpenTheory
| CloseTheory
| NoOpenedTheory
......@@ -39,25 +38,47 @@ let error e = raise (Error e)
module M = Map.Make(String)
type namespace = {
type ty_def =
| Ty_abstract
| Ty_algebraic of fsymbol list
type ty_decl = tysymbol * ty_def
type logic_decl =
| Lfunction of fsymbol * (vsymbol list * term) option (* FIXME: binders *)
| Lpredicate of psymbol * (vsymbol list * fmla) option (* FIXME: binders *)
| Linductive of psymbol * (Name.t * fmla) list
type prop_kind =
| Axiom | Lemma | Goal
type decl =
| Dtype of ty_decl list
| Dlogic of logic_decl list
| Dprop of prop_kind * Name.t * fmla
type decl_or_use =
| Decl of decl
| Use of t
and t = {
t_name : Name.t;
t_namespace : namespace;
t_decls : decl_or_use list;
}
and namespace = {
tysymbols : tysymbol M.t; (* type symbols *)
fsymbols : fsymbol M.t; (* function symbols *)
psymbols : psymbol M.t; (* predicate symbols *)
fmlas : fmla M.t; (* formula *)
namespace : namespace M.t;
}
type decl =
unit (* TODO *)
type theory = {
th_ns : namespace;
th_decl : decl list;
}
type t = {
loadpath : string list;
theories : theory M.t;
ns_stack : (namespace * namespace) list; (* stack of imports/exports *)
type th = {
th_name : Name.t;
th_stack : (namespace * namespace) list; (* stack of imports/exports *)
th_decls : decl_or_use list;
}
(** Creating environments *)
......@@ -66,98 +87,106 @@ let empty_ns = {
tysymbols = M.empty;
fsymbols = M.empty;
psymbols = M.empty;
fmlas = M.empty;
namespace = M.empty;
}
let is_empty_ns ns =
M.is_empty ns.tysymbols &&
M.is_empty ns.fsymbols &&
M.is_empty ns.psymbols &&
M.is_empty ns.namespace
let create lp = {
loadpath = lp;
theories = M.empty;
ns_stack = [];
let create_theory n = {
th_name = n;
th_stack = [empty_ns, empty_ns];
th_decls = [];
}
let open_theory t = match t.ns_stack with
| [] -> { t with ns_stack = [empty_ns, empty_ns] }
| _ -> error OpenTheory
let close_theory t s = match t.ns_stack with
let close_theory th = match th.th_stack with
| [_, e] ->
let th = { th_ns = e; th_decl = [] (* TODO *) } in
{ t with theories = M.add s th t.theories }
{ t_name = th.th_name;
t_namespace = e;
t_decls = th.th_decls; }
| _ ->
error CloseTheory
let open_namespace t = match t.ns_stack with
(*
use export T = use_export T
use T = namespace T use_export T end
use import T = namespace T use_export T end import T
*)
let open_namespace th = match th.th_stack with
| (i, _) :: _ as st ->
{ t with ns_stack = (i, empty_ns) :: st }
{ th with th_stack = (i, empty_ns) :: st }
| [] ->
error NoOpenedTheory
assert false
let close_namespace t s = match t.ns_stack with
let close_namespace th n ~import = match th.th_stack with
| (_, e0) :: (i, e) :: st ->
let s = Name.to_string n in
let add ns = { ns with namespace = M.add s e0 ns.namespace } in
{ t with ns_stack = (add i, add e) :: st }
{ th with th_stack = (add i, add e) :: st }
| [_] ->
error NoOpenedNamespace
| [] ->
error NoOpenedTheory
let add_tysymbol x ty env = { env with tysymbols = M.add x ty env.tysymbols }
let add_fsymbol x ty env = { env with fsymbols = M.add x ty env.fsymbols }
let add_psymbol x ty env = { env with psymbols = M.add x ty env.psymbols }
assert false
(* let self_id = "(\*self*\)" *)
(* let self env = M.find self_id env.theories *)
(* let empty = { empty_env with theories = M.add self_id empty_env M.empty } *)
let use_export th t =
assert false (* TODO *)
(* let add_self f x v env = *)
(* f x v { env with theories = *)
(* M.add self_id (f x v (self env)) env.theories } *)
type th_inst = {
inst_ts : tysymbol Mts.t;
inst_fs : fsymbol Mfs.t;
inst_ps : psymbol Mps.t;
}
(* let add_tysymbol = add_self add_tysymbol *)
(* let add_fsymbol = add_self add_fsymbol *)
(* let add_psymbol = add_self add_psymbol *)
(* let add_theory = add_self add_theory *)
let clone_export th t i =
assert false (* TODO *)
let add_tysymbol x ty ns = { ns with tysymbols = M.add x ty ns.tysymbols }
let add_fsymbol x ty ns = { ns with fsymbols = M.add x ty ns.fsymbols }
let add_psymbol x ty ns = { ns with psymbols = M.add x ty ns.psymbols }
let add_ns add x v th = match th.th_stack with
| (i, e) :: st ->
let x = Name.unsafe_to_string x in (add x v i, add x v e) :: st
| [] -> assert false
let add_decl th d =
let st = match d with
| Dtype [ty, Ty_abstract] ->
add_ns add_tysymbol ty.ts_name ty th
| Dlogic [Lfunction (fs, None)] ->
add_ns add_fsymbol fs.fs_name fs th
| Dlogic [Lpredicate (ps, None)] ->
add_ns add_psymbol ps.ps_name ps th
| _ ->
assert false (* TODO *)
in
{ th with
th_stack = st;
th_decls = (Decl d) :: th.th_decls }
(** Querying environments *)
let ns env = match env.ns_stack with
let get_namespace th = match th.th_stack with
| (ns, _) :: _ -> ns
| [] -> error NoOpenedTheory
| [] -> assert false
let find_tysymbol s env = M.find s env.tysymbols
let find_fsymbol s env = M.find s env.fsymbols
let find_psymbol s env = M.find s env.psymbols
type path =
| Pident of string
| Pdot of path * string
let find_local_namespace s env =
try M.find s env.namespace
with Not_found -> error (UnboundNamespace s)
let rec find_namespace q env = match q with
| Pident t -> find_local_namespace t env
| Pdot (q, t) -> let env = find_namespace q env in find_local_namespace t env
let rec find f q env = match q with
| Pident x -> f x env
| Pdot (m, x) -> let env = find_namespace m env in f x env
let find_tysymbol p env = find find_tysymbol p (ns env)
let find_tysymbol ns s = M.find s ns.tysymbols
let find_fsymbol ns s = M.find s ns.fsymbols
let find_psymbol ns s = M.find s ns.psymbols
let find_namespace ns s = M.find s ns.namespace
let find_fmla ns s = M.find s ns.fmlas
let mem_tysymbol ns s = M.mem s ns.tysymbols
let mem_fsymbol ns s = M.mem s ns.fsymbols
let mem_psymbol ns s = M.mem s ns.psymbols
let mem_namespace ns s = M.mem s ns.namespace
let mem_fmla ns s = M.mem s ns.fmlas
(** Error reporting *)
let report fmt = function
| UnboundNamespace s ->
fprintf fmt "unbound namespace %s" s
| OpenTheory ->
fprintf fmt "cannot open a new theory in a non-empty context"
| CloseTheory ->
......@@ -169,23 +198,26 @@ let report fmt = function
(** Debugging *)
let rec print_env fmt env =
let rec print_namespace fmt ns =
fprintf fmt "@[<hov 2>types: ";
M.iter (fun x ty -> fprintf fmt "%s -> %a;@ " x Name.print ty.Ty.ts_name)
env.tysymbols;
ns.tysymbols;
fprintf fmt "@]@\n@[<hov 2>function symbols: ";
M.iter (fun x s -> fprintf fmt "%s -> %a;@ " x Name.print s.fs_name)
env.fsymbols;
ns.fsymbols;
fprintf fmt "@]@\n@[<hov 2>predicate symbols: ";
M.iter (fun x s -> fprintf fmt "%s -> %a;@ " x Name.print s.ps_name)
env.psymbols;
ns.psymbols;
fprintf fmt "@]@\n@[<hov 2>namespace: ";
M.iter (fun x th -> fprintf fmt "%s -> [@[%a@]];@ " x print_env th)
env.namespace;
M.iter (fun x th -> fprintf fmt "%s -> [@[%a@]];@ " x print_namespace th)
ns.namespace;
fprintf fmt "@]"
let print fmt t =
print_env fmt (ns t)
let print_th fmt th =
print_namespace fmt (get_namespace th)
let print_t fmt t =
fprintf fmt "<theory (TODO>"
(*
Local Variables:
......
src/theory.mli
View file @ 5e19909d
......@@ -44,9 +44,9 @@ type decl_or_use =
| Use of t
and t = private {
th_name : Name.t;
th_namespace : namespace;
th_decls : decl_or_use list;
t_name : Name.t;
t_namespace : namespace;
t_decls : decl_or_use list;
}
and namespace
......@@ -56,12 +56,12 @@ and namespace
type th
(** a theory under construction *)
val create_theory : Name.t -> th
val create_theory : Name.t -> th
val open_namespace : th -> Name.t -> import:bool -> th
val close_namespace : th -> th
val open_namespace : th -> th
val close_namespace : th -> Name.t -> import:bool -> th
val use_export : th -> string -> th
val use_export : th -> t -> th
type th_inst = {
inst_ts : tysymbol Mts.t;
......@@ -69,7 +69,7 @@ type th_inst = {
inst_ps : psymbol Mps.t;
}
val clone_export : th -> string -> th_inst -> th
val clone_export : th -> t -> th_inst -> th
val add_decl : th -> decl -> th
......@@ -85,6 +85,12 @@ val find_psymbol : namespace -> string -> psymbol
val find_namespace: namespace -> string -> namespace
val find_fmla : namespace -> string -> fmla
val mem_tysymbol : namespace -> string -> bool
val mem_fsymbol : namespace -> string -> bool
val mem_psymbol : namespace -> string -> bool
val mem_namespace: namespace -> string -> bool
val mem_fmla : namespace -> string -> bool
(** Error reporting *)
type error
......@@ -96,4 +102,5 @@ val report : Format.formatter -> error -> unit
(** Debugging *)
val print : Format.formatter -> t -> unit
val print_th : Format.formatter -> th -> unit
val print_t : Format.formatter -> t -> unit
src/typing.ml
View file @ 5e19909d
......@@ -20,8 +20,10 @@
open Util
open Format
open Pp
open Ty
open Term
open Ptree
open Theory
(** errors *)
......@@ -29,18 +31,20 @@ type error =
| Message of string
| ClashType of string
| BadTypeArity of string
| UnboundType of qualid
| UnboundType of string
| TypeArity of qualid * int * int
| Clash of string
| PredicateExpected
| TermExpected
| UnboundSymbol of qualid
| UnboundSymbol of string
| TermExpectedType of (formatter -> unit) * (formatter -> unit)
(* actual / expected *)
| BadNumberOfArguments of Name.t * int * int
| ClashTheory of string
| ClashNamespace of string
| UnboundTheory of string
| AlreadyTheory of string
| UnboundNamespace of string
exception Error of error
......@@ -60,7 +64,7 @@ let report fmt = function
| BadTypeArity s ->
fprintf fmt "duplicate type parameter %s" s
| UnboundType s ->
fprintf fmt "Unbound type '%a'" print_qualid s
fprintf fmt "Unbound type '%s'" s
| TypeArity (id, a, n) ->
fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a;
fprintf fmt "but is applied to %d argument(s)@]" n
......@@ -71,7 +75,7 @@ let report fmt = function
| TermExpected ->
fprintf fmt "syntax error: term expected"
| UnboundSymbol s ->
fprintf fmt "Unbound symbol '%a'" print_qualid s
fprintf fmt "Unbound symbol '%s'" s
| BadNumberOfArguments (s, n, m) ->
fprintf fmt "@[Symbol `%a' is aplied to %d terms,@ " Name.print s n;
fprintf fmt "but is expecting %d arguments@]" m
......@@ -80,10 +84,28 @@ let report fmt = function
fprintf fmt "@ but is expected to have type@ "; ty2 fmt; fprintf fmt "@]"
| ClashTheory s ->
fprintf fmt "clash with previous theory %s" s
| ClashNamespace s ->
fprintf fmt "clash with previous namespace %s" s
| UnboundTheory s ->
fprintf fmt "unbound theory %s" s
| AlreadyTheory s ->
fprintf fmt "already using a theory with name %s" s
| UnboundNamespace s ->
fprintf fmt "unbound namespace %s" s
(** Environments *)
module M = Map.Make(String)
type env = {
loadpath : string list;
theories : Theory.t M.t; (* local theories *)
}
let create lp = {
loadpath = lp;
theories = M.empty;
}
(** typing using destructive type variables
......@@ -159,16 +181,14 @@ let rec unify t1 t2 = match t1, t2 with
environment + local variables.
It is only local to this module and created with [create_denv] below. *)
module M = Map.Make(String)
type denv = {
env : Env.t;
th : Theory.th; (* the theory under construction *)
utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
dvars : dty M.t; (* local variables, to be bound later *)
}
let create_denv env = {
env = env;
let create_denv th = {
th = th;
utyvars = Hashtbl.create 17;
dvars = M.empty;
}
......@@ -199,19 +219,56 @@ let rec specialize env t = match t.Ty.ty_node with
| Ty.Tyapp (s, tl) ->
Tyapp (s, List.map (specialize env) tl)
(** generic find function using a path *)
let find_local_namespace {id=x; id_loc=loc} ns =
try find_namespace ns x
with Not_found -> error ~loc (UnboundNamespace x)
let rec find_namespace q ns = match q with
| Qident t -> find_local_namespace t ns
| Qdot (q, t) -> let ns = find_namespace q ns in find_local_namespace t ns
let rec find f q ns = match q with
| Qident x -> f x ns
| Qdot (m, x) -> let ns = find_namespace m ns in f x ns
(** specific find functions using a path *)
let find_tysymbol {id=x; id_loc=loc} ns =
try find_tysymbol ns x
with Not_found -> error ~loc (UnboundType x)
let find_tysymbol p th =
find find_tysymbol p (get_namespace th)
let specialize_tysymbol x env =
let s = Env.find_tysymbol x env.env in
let s = find_tysymbol x env.th in
let env = Htv.create 17 in
s, List.map (find_type_var env) s.Ty.ts_args
let find_fsymbol {id=x; id_loc=loc} ns =
try find_fsymbol ns x
with Not_found -> error ~loc (UnboundSymbol x)
let find_fsymbol p th =
find find_fsymbol p (get_namespace th)
let specialize_fsymbol x env =
let s = (* Env.find_fsymbol x env *) assert false (*TODO*) in
let s = find_fsymbol x env.th in
let tl, t = s.fs_scheme in
let env = Htv.create 17 in
s, List.map (specialize env) tl, specialize env t
let find_psymbol {id=x; id_loc=loc} ns =
try find_psymbol ns x
with Not_found -> error ~loc (UnboundSymbol x)
let find_psymbol p th =
find find_psymbol p (get_namespace th)
let specialize_psymbol x env =
let s = (* find_psymbol x env.env *) assert false (*TODO*) in
let s = find_psymbol x env.th in
let env = Htv.create 17 in
s, List.map (specialize env) s.ps_scheme
......@@ -221,20 +278,13 @@ let rec qloc = function
| Qident x -> x.id_loc
| Qdot (m, x) -> Loc.join (qloc m) x.id_loc
let rec path = function
| Qident x -> Env.Pident x.id
| Qdot (p, x) -> Env.Pdot (path p, x.id)
(* parsed types -> intermediate types *)
let rec dty env = function
| PPTtyvar {id=x} ->
Tyvar (find_user_type_var x env)
| PPTtyapp (p, x) ->
let loc = qloc x in
let s, tv =
try specialize_tysymbol (path x) env
with Not_found -> error ~loc:loc (UnboundType x)
in
let s, tv = specialize_tysymbol x env in
let np = List.length p in
let a = List.length tv in
if np <> a then error ~loc (TypeArity (x, a, np));
......@@ -289,22 +339,14 @@ and dterm_node loc env = function
Tvar x, ty
| PPvar x ->
(* 0-arity symbol (constant) *)
begin try
let s, tyl, ty = specialize_fsymbol x env in
let n = List.length tyl in
if n > 0 then error ~loc (BadNumberOfArguments (s.fs_name, 0, n));
Tapp (s, []), ty
with Not_found ->
error ~loc (UnboundSymbol x)
end
let s, tyl, ty = specialize_fsymbol x env in
let n = List.length tyl in
if n > 0 then error ~loc (BadNumberOfArguments (s.fs_name, 0, n));
Tapp (s, []), ty
| PPapp (x, tl) ->
begin try
let s, tyl, ty = specialize_fsymbol x env in
let tl = dtype_args s.fs_name loc env tyl tl in
Tapp (s, tl), ty
with Not_found ->
error ~loc (UnboundSymbol x)
end
let s, tyl, ty = specialize_fsymbol x env in
let tl = dtype_args s.fs_name loc env tyl tl in
Tapp (s, tl), ty
| _ ->
assert false (*TODO*)
......@@ -330,12 +372,7 @@ and dfmla env e = match e.pp_desc with
let env = { env with dvars = M.add x ty env.dvars } in
Fquant (Fexists, x, ty, dfmla env a)
| PPapp (x, tl) ->
let s, tyl =
try
specialize_psymbol x env
with Not_found ->
error ~loc:e.pp_loc (UnboundSymbol x)
in
let s, tyl = specialize_psymbol x env in
let tl = dtype_args s.ps_name e.pp_loc env tyl tl in
Fapp (s, tl)
| _ ->
......@@ -391,9 +428,9 @@ and fmla env = function
open Ptree
(***
let add_type loc sl s env =
if M.mem s.id env.tysymbols then error ~loc (ClashType s.id);