Theory : use

parent c47b1f02
theory A
type t
namespace S
type t
type t
end
end
(* test file *)
theory A
type t
end
theory B
use export A
type t
end
(* test file *)
theory A
type t
end
theory B
type t
use export A
end
(* test file *)
theory A
type t
end
theory B
type t
use import A
end
(* test file *)
theory A
type t
end
theory B
use import A
type t
end
(* test file *)
theory A
type t
end
theory B
use export A
logic c : A.t
end
(* test file *)
theory A
logic c : t
end
......@@ -61,7 +61,7 @@ let id_user sh ln loc = create_ident sh ln (User loc)
type printer = (string, int) Hashtbl.t * (int, string) Hashtbl.t
let create_printer _ = Hashtbl.create 1997, Hashtbl.create 1997
let create_printer () = Hashtbl.create 1997, Hashtbl.create 1997
let rec find_index indices name ind =
if Hashtbl.mem indices (name ^ string_of_int ind)
......@@ -71,16 +71,17 @@ let find_unique indices name =
try
let ind = Hashtbl.find indices name + 1 in
let ind = find_index indices name ind in
let _ = Hashtbl.add indices name ind in
Hashtbl.add indices name ind;
name ^ string_of_int ind
with Not_found ->
name
let id_unique (indices,values) id =
try Hashtbl.find values id.id_tag
try
Hashtbl.find values id.id_tag
with Not_found ->
let name = find_unique indices id.id_long in
let _ = Hashtbl.add values id.id_tag name in
let _ = Hashtbl.add indices name 0 in
Hashtbl.add values id.id_tag name;
Hashtbl.add indices name 0;
name
......@@ -25,17 +25,11 @@ open Term
(** Error reporting *)
type error =
| OpenTheory
| CloseTheory
| NoOpenedTheory
| NoOpenedNamespace
| RedeclaredIdent
| CannotInstantiate
exception Error of error
let error e = raise (Error e)
exception CloseTheory
exception NoOpenedNamespace
exception RedeclaredIdent of ident
exception CannotInstantiate
exception ClashSymbol of string
(** The environment type *)
......@@ -62,14 +56,14 @@ type decl =
type decl_or_use =
| Decl of decl
| Use of t
and t = {
t_name : ident;
t_local : Sid.t; (* locally declared abstract symbols *)
t_known : Sid.t; (* imported and locally declared symbols *)
t_namespace : namespace;
t_decls : decl_or_use list;
| Use of theory
and theory = {
th_name : ident;
th_param : Sid.t; (* locally declared abstract symbols *)
th_known : ident Mid.t; (* imported and locally declared symbols *)
th_export : namespace;
th_decls : decl_or_use list;
}
and namespace = {
......@@ -80,12 +74,14 @@ and namespace = {
namespace : namespace M.t;
}
type th = {
th_name : ident;
th_local : Sid.t;
th_known : Sid.t;
th_stack : (namespace * namespace) list; (* stack of imports/exports *)
th_decls : decl_or_use list;
type theory_uc = {
uc_name : ident;
uc_param : Sid.t;
uc_known : ident Mid.t;
uc_visible: namespace list; (* stack of visible symbols *)
uc_import : namespace list;
uc_export : namespace list;
uc_decls : decl_or_use list;
}
(** Creating environments *)
......@@ -99,41 +95,92 @@ let empty_ns = {
}
let create_theory n = {
th_name = n;
th_local = Sid.empty;
th_known = Sid.empty;
th_stack = [empty_ns, empty_ns];
th_decls = [];
uc_name = n;
uc_param = Sid.empty;
uc_known = Mid.add n n Mid.empty;
uc_visible = [empty_ns];
uc_import = [empty_ns];
uc_export = [empty_ns];
uc_decls = [];
}
let close_theory th = match th.th_stack with
| [_, e] ->
{ t_name = th.th_name;
t_local = th.th_local;
t_known = th.th_known;
t_namespace = e;
t_decls = List.rev th.th_decls; }
let close_theory th = match th.uc_export with
| [e] ->
{ th_name = th.uc_name;
th_param = th.uc_param;
th_known = th.uc_known;
th_export = e;
th_decls = List.rev th.uc_decls; }
| _ ->
error CloseTheory
let open_namespace th = match th.th_stack with
| (i, _) :: _ as st ->
{ th with th_stack = (i, empty_ns) :: st }
raise CloseTheory
let open_namespace th = match th.uc_visible with
| ns :: _ as st ->
{ th with
uc_visible = ns :: st;
uc_import = empty_ns :: th.uc_import;
uc_export = empty_ns :: th.uc_export; }
| [] ->
assert false
let close_namespace th n ~import = match th.th_stack with
| (_, e0) :: (i, e) :: st ->
let fusion ~check ns1 ns2 =
let merge_ns m1 m2 =
M.fold
(fun k1 v1 m2 ->
if check && M.mem k1 m2 then raise (ClashSymbol k1);
M.add k1 v1 m2)
m1 m2
in
{ tysymbols = merge_ns ns1.tysymbols ns2.tysymbols;
fsymbols = merge_ns ns1.fsymbols ns2.fsymbols;
psymbols = merge_ns ns1.psymbols ns2.psymbols;
props = merge_ns ns1.props ns2.props;
namespace = merge_ns ns1.namespace ns2.namespace; }
let add_known id uc =
if Mid.mem id uc.uc_known then raise (RedeclaredIdent id);
{ uc with uc_known = Mid.add id uc.uc_name uc.uc_known }
let close_namespace uc n ~import =
match uc.uc_visible, uc.uc_import, uc.uc_export with
| v0 :: v1 :: stv, i0 :: i1 :: sti, e0 :: e1 :: ste ->
let s = n.id_short in
let add ns = { ns with namespace = M.add s e0 ns.namespace } in
{ th with th_stack = (add i, add e) :: st }
| [_] ->
error NoOpenedNamespace
| [] ->
let add ns1 ns2 = { ns2 with namespace = M.add s ns1 ns2.namespace } in
let v1 = add v0 v1 and i1 = add i0 i1 and e1 = add e0 e1 in
let v1 = if import then fusion ~check:false v0 v1 else v1 in
let i1 = if import then fusion ~check:true i0 i1 else i1 in
add_known n
{ uc with
uc_visible = v1 :: stv;
uc_import = i1 :: sti;
uc_export = e1 :: ste; }
| [_], [_], [_] ->
raise NoOpenedNamespace
| _ ->
assert false
let use_export th t =
assert false (* TODO *)
let merge_known m1 m2 =
Mid.fold
(fun k1 id1 m ->
try
let id2 = Mid.find k1 m2 in
if id1 != id2 then raise (RedeclaredIdent id1);
m
with Not_found ->
Mid.add k1 id1 m)
m1 m2
let use_export uc th =
match uc.uc_visible, uc.uc_import, uc.uc_export with
| v0 :: stv, i0 :: sti, e0 :: ste ->
{ uc with
uc_visible = fusion ~check:false th.th_export v0 :: stv;
uc_import = fusion ~check:true th.th_export i0 :: sti;
uc_export = fusion ~check:false th.th_export e0 :: ste;
uc_known = merge_known uc.uc_known th.th_known;
}
| _ ->
assert false
type th_inst = {
inst_ts : tysymbol Mts.t;
......@@ -142,58 +189,64 @@ type th_inst = {
}
let check_sym id t =
if Sid.mem id t.t_local then () else error CannotInstantiate
if not (Sid.mem id t.th_param) then raise CannotInstantiate
let clone_export th t i =
let check_ts s _ = check_sym s.ts_name t in
let _ = Mts.iter check_ts i.inst_ts in
Mts.iter check_ts i.inst_ts;
let check_fs s _ = check_sym s.fs_name t in
let _ = Mfs.iter check_fs i.inst_fs in
Mfs.iter check_fs i.inst_fs;
let check_ps s _ = check_sym s.ps_name t in
let _ = Mps.iter check_ps i.inst_ps in
Mps.iter check_ps i.inst_ps;
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 generic_add ~check x v m =
if check && M.mem x m then raise (ClashSymbol x);
M.add x v m
let add_tysymbol ~check x ty ns =
{ ns with tysymbols = generic_add ~check x ty ns.tysymbols }
let add_fsymbol ~check x ty ns =
{ ns with fsymbols = generic_add ~check x ty ns.fsymbols }
let add_psymbol ~check x ty ns =
{ ns with psymbols = generic_add ~check x ty ns.psymbols }
let add_symbol add x v uc =
match uc.uc_visible, uc.uc_import, uc.uc_export with
| v0 :: stv, i0 :: sti, e0 :: ste ->
let x = x.id_short in
{ uc with
uc_visible = add ~check:false x v v0 :: stv;
uc_import = add ~check:true x v i0 :: sti;
uc_export = add ~check:false x v e0 :: ste }
let add_ns add x v th = match th.th_stack with
| (i, e) :: st ->
let x = x.id_short in (add x v i, add x v e) :: st
| [] -> assert false
let add_known id th =
let _ = if Sid.mem id th.th_known
then error RedeclaredIdent else ()
in
{ th with th_known = Sid.add id th.th_known }
| _ ->
assert false
let add_local id th =
let th = add_known id th in
{ th with th_local = Sid.add id th.th_local }
let add_param id uc =
let uc = add_known id uc in
{ uc with uc_param = Sid.add id uc.uc_param }
let add_decl th d =
let st = match d with
let add_decl uc d =
let uc = match d with
| Dtype [ty, Ty_abstract] ->
let th = add_local ty.ts_name th in
add_ns add_tysymbol ty.ts_name ty th
let uc = add_param ty.ts_name uc in
add_symbol add_tysymbol ty.ts_name ty uc
| Dlogic [Lfunction (fs, None)] ->
let th = add_local fs.fs_name th in
add_ns add_fsymbol fs.fs_name fs th
let uc = add_param fs.fs_name uc in
add_symbol add_fsymbol fs.fs_name fs uc
| Dlogic [Lpredicate (ps, None)] ->
let th = add_local ps.ps_name th in
add_ns add_psymbol ps.ps_name ps th
let uc = add_param ps.ps_name uc in
add_symbol add_psymbol ps.ps_name ps uc
| _ ->
assert false (* TODO *)
in
{ th with
th_stack = st;
th_decls = (Decl d) :: th.th_decls }
{ uc with uc_decls = (Decl d) :: uc.uc_decls }
(** Querying environments *)
let get_namespace th = match th.th_stack with
| (ns, _) :: _ -> ns
let get_namespace th = match th.uc_visible with
| ns :: _ -> ns
| [] -> assert false
let find_tysymbol ns s = M.find s ns.tysymbols
......@@ -208,22 +261,6 @@ let mem_psymbol ns s = M.mem s ns.psymbols
let mem_namespace ns s = M.mem s ns.namespace
let mem_prop ns s = M.mem s ns.props
(** Error reporting *)
let report fmt = function
| OpenTheory ->
fprintf fmt "cannot open a new theory in a non-empty context"
| CloseTheory ->
fprintf fmt "cannot close theory: there are still unclosed namespaces"
| NoOpenedTheory ->
fprintf fmt "no opened theory"
| NoOpenedNamespace ->
fprintf fmt "no opened namespace"
| RedeclaredIdent ->
fprintf fmt "cannot redeclare identifiers"
| CannotInstantiate ->
fprintf fmt "cannot instantiate a defined symbol"
(** Debugging *)
let print_ident =
......
......@@ -42,29 +42,29 @@ type decl =
type decl_or_use =
| Decl of decl
| Use of t
and t = private {
t_name : ident;
t_local : Sid.t; (* locally declared abstract symbols *)
t_known : Sid.t; (* imported and locally declared symbols *)
t_namespace : namespace;
t_decls : decl_or_use list;
| Use of theory
and theory = private {
th_name : ident;
th_param : Sid.t; (* locally declared abstract symbols *)
th_known : ident Mid.t; (* imported and locally declared symbols *)
th_export : namespace;
th_decls : decl_or_use list;
}
and namespace
(** Building *)
type th
type theory_uc
(** a theory under construction *)
val create_theory : ident -> th
val create_theory : ident -> theory_uc
val open_namespace : th -> th
val close_namespace : th -> ident -> import:bool -> th
val open_namespace : theory_uc -> theory_uc
val close_namespace : theory_uc -> ident -> import:bool -> theory_uc
val use_export : th -> t -> th
val use_export : theory_uc -> theory -> theory_uc
type th_inst = {
inst_ts : tysymbol Mts.t;
......@@ -72,15 +72,15 @@ type th_inst = {
inst_ps : psymbol Mps.t;
}
val clone_export : th -> t -> th_inst -> th
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
val add_decl : th -> decl -> th
val add_decl : theory_uc -> decl -> theory_uc
val close_theory : th -> t
val close_theory : theory_uc -> theory
(** Querying *)
val get_namespace : th -> namespace
val get_namespace : theory_uc -> namespace
val find_tysymbol : namespace -> string -> tysymbol
val find_fsymbol : namespace -> string -> fsymbol
......@@ -94,16 +94,16 @@ val mem_psymbol : namespace -> string -> bool
val mem_namespace: namespace -> string -> bool
val mem_prop : namespace -> string -> bool
(** Error reporting *)
(** Exceptions *)
type error
exception Error of error
val report : Format.formatter -> error -> unit
exception CloseTheory
exception NoOpenedNamespace
exception RedeclaredIdent of ident
exception CannotInstantiate
exception ClashSymbol of string
(** Debugging *)
val print_th : Format.formatter -> th -> unit
val print_t : Format.formatter -> t -> unit
val print_th : Format.formatter -> theory_uc -> unit
val print_t : Format.formatter -> theory -> unit
......@@ -22,11 +22,13 @@ open Format
let files = ref []
let parse_only = ref false
let type_only = ref false
let debug = ref false
let () =
Arg.parse
["--parse-only", Arg.Set parse_only, "stops after parsing";
"--type-only", Arg.Set type_only, "stops after type-checking";
"--debug", Arg.Set debug, "sets the debug flag";
]
(fun f -> files := f :: !files)
"usage: why [options] files..."
......@@ -49,13 +51,13 @@ let type_file env file =
Loc.set_file file lb;
let f = Lexer.parse_logic_file lb in
close_in c;
if !parse_only then env else List.fold_left Typing.add_theory env f
if !parse_only then env else Typing.add_theories env f
let () =
try
let env = Typing.create ["lib"] in
let env = Typing.create ["lib"; ""] in
ignore (List.fold_left type_file env !files)
with e ->
with e when not !debug ->
eprintf "%a@." report e;
exit 1
......
......@@ -194,19 +194,19 @@ uqualid:
| uqualid DOT uident { Qdot ($1, $3) }
;
tqualid:
| ident { Qident $1 }
| tqualid DOT ident { Qdot ($1, $3) }
any_qualid:
| ident { Qident $1 }
| any_qualid DOT ident { Qdot ($1, $3) }
;
qualid:
| lqualid {$1}
| uqualid {$1}
| ident { Qident $1 }
| uqualid DOT ident { Qdot ($1, $3) }
decl:
| LOGIC list1_lident_sep_comma COLON logic_type
{ Logic (loc_i 3, $2, $4) }
| AXIOM ident COLON lexpr
| AXIOM uident COLON lexpr
{ Axiom (loc (), $2, $4) }
| PREDICATE lident LEFTPAR list0_logic_binder_sep_comma RIGHTPAR EQUAL lexpr
{ Predicate_def (loc (), $2, $4, $7) }
......@@ -215,7 +215,7 @@ decl:
| FUNCTION lident LEFTPAR list0_logic_binder_sep_comma RIGHTPAR COLON
primitive_type EQUAL lexpr
{ Function_def (loc (), $2, $4, $7, $9) }
| GOAL ident COLON lexpr
| GOAL uident COLON lexpr
{ Goal (loc (), $2, $4) }
| TYPE typedecl typedefn
{ let loc, vl, id = $2 in $3 loc vl id }
......@@ -234,7 +234,7 @@ list1_theory:
theory:
| THEORY uident list0_decl END
{ { th_loc = loc (); th_name = $2; th_decl = $3 } }
{ { pt_loc = loc (); pt_name = $2; pt_decl = $3 } }
;
typedecl:
......@@ -266,9 +266,9 @@ typecases:
;
typecase:
| ident
| uident
{ (loc_i 1,$1,[]) }
| ident LEFTPAR list1_primitive_type_sep_comma RIGHTPAR
| uident LEFTPAR list1_primitive_type_sep_comma RIGHTPAR
{ (loc_i 1,$1,$3) }
;
......@@ -283,7 +283,7 @@ indcases:
;
indcase:
| ident COLON lexpr { (loc_i 1,$1,$3) }
| uident COLON lexpr { (loc_i 1,$1,$3) }
;
primitive_type:
......@@ -352,11 +352,6 @@ logic_binder:
***/
;
external_:
| /* epsilon */ { false }
| EXTERNAL { true }
;
lexpr:
| lexpr ARROW lexpr
{ infix_pp $1 PPimplies $3 }
......@@ -435,7 +430,7 @@ match_case:
pattern:
| uqualid { ($1, [], loc ()) }
| uqualid LEFTPAR list1_ident_sep_comma RIGHTPAR { ($1, $3, loc ()) }
| uqualid LEFTPAR list1_lident_sep_comma RIGHTPAR { ($1, $3, loc ()) }
;
triggers:
......@@ -493,21 +488,16 @@ bar_:
| BAR { () }
;
list1_ident_sep_comma:
| ident { [$1] }
| ident COMMA list1_ident_sep_comma { $1 :: $3 }
;
list1_lident_sep_comma:
| lident { [$1] }
| lident COMMA list1_lident_sep_comma { $1 :: $3 }
;
use: