From 761b06a83d0db96d47076344459713596b73b683 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Christophe=20Filli=C3=A2tre?= Date: Fri, 26 Feb 2010 13:50:19 +0000 Subject: [PATCH] Theory : use --- bench/typing/bad/clash_type2.why | 2 +- bench/typing/bad/clash_type3.why | 11 ++ bench/typing/bad/clash_type4.why | 11 ++ bench/typing/bad/clash_type5.why | 11 ++ bench/typing/bad/clash_type6.why | 11 ++ bench/typing/bad/unbound_namespace1.why | 11 ++ bench/typing/bad/unbound_type1.why | 7 + src/core/ident.ml | 11 +- src/core/theory.ml | 237 ++++++++++++++---------- src/core/theory.mli | 50 ++--- src/main.ml | 8 +- src/parser/parser.mly | 40 ++-- src/parser/ptree.mli | 6 +- src/parser/typing.ml | 153 ++++++++------- src/parser/typing.mli | 6 +- src/test.why | 40 +--- 16 files changed, 332 insertions(+), 283 deletions(-) create mode 100644 bench/typing/bad/clash_type3.why create mode 100644 bench/typing/bad/clash_type4.why create mode 100644 bench/typing/bad/clash_type5.why create mode 100644 bench/typing/bad/clash_type6.why create mode 100644 bench/typing/bad/unbound_namespace1.why create mode 100644 bench/typing/bad/unbound_type1.why diff --git a/bench/typing/bad/clash_type2.why b/bench/typing/bad/clash_type2.why index d73e10ec3..c606c14ef 100644 --- a/bench/typing/bad/clash_type2.why +++ b/bench/typing/bad/clash_type2.why @@ -1,6 +1,6 @@ theory A - type t namespace S type t + type t end end diff --git a/bench/typing/bad/clash_type3.why b/bench/typing/bad/clash_type3.why new file mode 100644 index 000000000..a06d6d085 --- /dev/null +++ b/bench/typing/bad/clash_type3.why @@ -0,0 +1,11 @@ + +(* test file *) + +theory A + type t +end + +theory B + use export A + type t +end diff --git a/bench/typing/bad/clash_type4.why b/bench/typing/bad/clash_type4.why new file mode 100644 index 000000000..a18f20c4d --- /dev/null +++ b/bench/typing/bad/clash_type4.why @@ -0,0 +1,11 @@ + +(* test file *) + +theory A + type t +end + +theory B + type t + use export A +end diff --git a/bench/typing/bad/clash_type5.why b/bench/typing/bad/clash_type5.why new file mode 100644 index 000000000..bcc1a135f --- /dev/null +++ b/bench/typing/bad/clash_type5.why @@ -0,0 +1,11 @@ + +(* test file *) + +theory A + type t +end + +theory B + type t + use import A +end diff --git a/bench/typing/bad/clash_type6.why b/bench/typing/bad/clash_type6.why new file mode 100644 index 000000000..2eed9cbfa --- /dev/null +++ b/bench/typing/bad/clash_type6.why @@ -0,0 +1,11 @@ + +(* test file *) + +theory A + type t +end + +theory B + use import A + type t +end diff --git a/bench/typing/bad/unbound_namespace1.why b/bench/typing/bad/unbound_namespace1.why new file mode 100644 index 000000000..f1d4236c3 --- /dev/null +++ b/bench/typing/bad/unbound_namespace1.why @@ -0,0 +1,11 @@ + +(* test file *) + +theory A + type t +end + +theory B + use export A + logic c : A.t +end diff --git a/bench/typing/bad/unbound_type1.why b/bench/typing/bad/unbound_type1.why new file mode 100644 index 000000000..6c4388ba7 --- /dev/null +++ b/bench/typing/bad/unbound_type1.why @@ -0,0 +1,7 @@ + +(* test file *) + +theory A + logic c : t +end + diff --git a/src/core/ident.ml b/src/core/ident.ml index f8551786f..e0a4553d1 100644 --- a/src/core/ident.ml +++ b/src/core/ident.ml @@ -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 diff --git a/src/core/theory.ml b/src/core/theory.ml index e5153218b..54c1079e5 100644 --- a/src/core/theory.ml +++ b/src/core/theory.ml @@ -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 = diff --git a/src/core/theory.mli b/src/core/theory.mli index ae6e2bd94..01bbd83ba 100644 --- a/src/core/theory.mli +++ b/src/core/theory.mli @@ -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 diff --git a/src/main.ml b/src/main.ml index e34c7a3fd..779c0cced 100644 --- a/src/main.ml +++ b/src/main.ml @@ -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 diff --git a/src/parser/parser.mly b/src/parser/parser.mly index 6d74dc1d5..c05f4fa85 100644 --- a/src/parser/parser.mly +++ b/src/parser/parser.mly @@ -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: -| imp_exp tqualid +| imp_exp any_qualid { { use_theory = $2; use_as = None; use_imp_exp = $1 } } -| imp_exp uident COLON tqualid - { { use_theory = $4; use_as = Some $2; use_imp_exp = $1 } } +| imp_exp any_qualid AS uident + { { use_theory = $2; use_as = Some $4; use_imp_exp = $1 } } ; imp_exp: diff --git a/src/parser/ptree.mli b/src/parser/ptree.mli index 77138719e..250d99ce1 100644 --- a/src/parser/ptree.mli +++ b/src/parser/ptree.mli @@ -95,9 +95,9 @@ type logic_decl = | Namespace of loc * ident * logic_decl list type theory = { - th_loc : loc; - th_name : ident; - th_decl : logic_decl list; + pt_loc : loc; + pt_name : ident; + pt_decl : logic_decl list; } type logic_file = theory list diff --git a/src/parser/typing.ml b/src/parser/typing.ml index 4c49175ac..640dbb6cc 100644 --- a/src/parser/typing.ml +++ b/src/parser/typing.ml @@ -74,7 +74,7 @@ let report fmt = function fprintf fmt "@[The type %a expects %d argument(s),@ " print_qualid id a; fprintf fmt "but is applied to %d argument(s)@]" n | Clash id -> - fprintf fmt "Clash with previous constant %s" id + fprintf fmt "Clash with previous symbol %s" id | PredicateExpected -> fprintf fmt "syntax error: predicate expected" | TermExpected -> @@ -82,7 +82,7 @@ let report fmt = function | UnboundSymbol s -> fprintf fmt "Unbound symbol '%s'" s | BadNumberOfArguments (s, n, m) -> - fprintf fmt "@[Symbol `%s' is aplied to %d terms,@ " s.id_short n; + fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_short n; fprintf fmt "but is expecting %d arguments@]" m | TermExpectedType (ty1, ty2) -> fprintf fmt "@[This term has type "; ty1 fmt; @@ -106,13 +106,31 @@ let report fmt = function | NotInLoadpath f -> fprintf fmt "cannot find `%s' in loadpath" f +(**** + + | 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 id -> + fprintf fmt "cannot redeclare identifier %s" id.id_short + | CannotInstantiate -> + fprintf fmt "cannot instantiate a defined symbol" + +****) + + (** Environments *) module M = Map.Make(String) type env = { loadpath : string list; - theories : Theory.t M.t; (* local theories *) + theories : theory M.t; (* local theories *) } let create lp = { @@ -195,7 +213,7 @@ let rec unify t1 t2 = match t1, t2 with It is only local to this module and created with [create_denv] below. *) type denv = { - th : Theory.th; (* the theory under construction *) + th : theory_uc; (* the theory under construction *) utyvars : (string, type_var) Hashtbl.t; (* user type variables *) dvars : dty M.t; (* local variables, to be bound later *) } @@ -444,8 +462,6 @@ and fmla env = function open Ptree let add_type loc sl {id=id} th = - let ns = get_namespace th in - if mem_tysymbol ns id then error ~loc (ClashType id); let tyvars = ref M.empty in let add_ty_var {id=x} = if M.mem x !tyvars then error ~loc (BadTypeArity x); @@ -458,7 +474,11 @@ let add_type loc sl {id=id} th = (* TODO: add the theory name to the long name *) let v = id_user id id loc in let ty = create_tysymbol v vl None in - add_decl th (Dtype [ty, Ty_abstract]) + try + add_decl th (Dtype [ty, Ty_abstract]) + with Theory.ClashSymbol _ -> + error ~loc (ClashType id) + let add_function loc pl t th {id=id} = let ns = get_namespace th in @@ -496,31 +516,6 @@ let axiom loc s f env = ignore (fmla env f); env -(*** -let uses_theory env (as_t, q) = - let loc = qloc q in - let rec find_theory q = match q with - | Qident t -> - t.id, find_local_theory t env - | Qdot (q, t) -> - let _, env = find_theory q in t.id, find_local_theory t env - in - let id, th = find_theory q in - let id = match as_t with None -> id | Some x -> x.id in - if M.mem id (self env).theories then error ~loc (AlreadyTheory id); - add_theory id th env - -let open_theory t env = - let loc = t.id_loc and id = t.id in - if not (M.mem id env.theories) then error ~loc (UnboundTheory id); - let th = M.find id env.theories in - let open_map m1 m2 = M.fold M.add m1 m2 in - { tysymbols = open_map th.tysymbols env.tysymbols; - fsymbols = open_map th.fsymbols env.fsymbols; - psymbols = open_map th.psymbols env.psymbols; - theories = open_map th.theories env.theories } -***) - let find_in_loadpath env f = let rec find c lp = match lp, c with | [], None -> @@ -547,36 +542,26 @@ let locate_file env q = if not (Sys.file_exists dir) then error ~loc:d.id_loc (UnboundDir dir); dir in - let file = match q with - | Qident f -> find_in_loadpath env f - | Qdot (p, f) -> let dir = locate_dir p in Filename.concat dir f.id - in - let file = file ^ ".why" in - if not (Sys.file_exists file) then error ~loc:(qloc q) (UnboundFile file); - file - -type loaded_theory = { - parsed : Ptree.theory; - mutable typed : Theory.t option; -} + match q with + | Qident f -> + find_in_loadpath env { f with id = f.id ^ ".why" } + | Qdot (p, f) -> + let dir = locate_dir p in + let file = Filename.concat dir f.id ^ ".why" in + if not (Sys.file_exists file) then + error ~loc:(qloc q) (UnboundFile file); + file -let loaded_theories = Hashtbl.create 17 (* file -> theory -> loaded_theory *) +let loaded_theories = Hashtbl.create 17 (* file -> string -> Theory.t *) (* parse file and store all theories into parsed_theories *) -let load_theories file = - if not (Hashtbl.mem loaded_theories file) then begin - let c = open_in file in - let lb = Lexing.from_channel c in - Loc.set_file file lb; - let tl = Lexer.parse_logic_file lb in - close_in c; - let h = Hashtbl.create 17 in - Hashtbl.add loaded_theories file h; - List.iter - (fun pt -> - Hashtbl.add h pt.th_name.id { parsed = pt; typed = None }) - tl - end +let load_file file = + let c = open_in file in + let lb = Lexing.from_channel c in + Loc.set_file file lb; + let tl = Lexer.parse_logic_file lb in + close_in c; + tl let rec find_theory env q = match q with | Qident id -> @@ -588,25 +573,27 @@ let rec find_theory env q = match q with | Qdot (f, id) -> (* theory in file f *) let file = locate_file env f in - load_theories file; + if not (Hashtbl.mem loaded_theories file) then begin + let tl = load_file file in + let h = Hashtbl.create 17 in + Hashtbl.add loaded_theories file h; + let env = { env with theories = M.empty } in + let add env pt = + let t, env = add_theory env pt in + Hashtbl.add h t.th_name.id_short t; + env + in + ignore (List.fold_left add env tl); + end; let h = Hashtbl.find loaded_theories file in - try - let t = Hashtbl.find h id.id in - match t.typed with - | Some th -> - th - | None -> - let th = type_theory env id.id t.parsed in - t.typed <- Some th; - th - with Not_found -> - error ~loc:id.id_loc (UnboundTheory id.id); + try Hashtbl.find h id.id + with Not_found -> error ~loc:id.id_loc (UnboundTheory id.id) and type_theory env id pt = - (* TODO: shouldn't we localize this ident? *) - let n = id_fresh id id in + (* TODO: use long name *) + let n = id_user id.id id.id id.id_loc in let th = create_theory n in - let th = add_decls env th pt.th_decl in + let th = add_decls env th pt.pt_decl in close_theory th and add_decls env th = List.fold_left (add_decl env) th @@ -623,10 +610,10 @@ and add_decl env th = function | Use (loc, use) -> let t = find_theory env use.use_theory in let n = match use.use_as with - | None -> t.t_name + | None -> id_clone t.th_name | Some x -> id_user x.id x.id loc in - begin match use.use_imp_exp with + begin try match use.use_imp_exp with | Nothing -> (* use T = namespace T use_export T end *) let th = open_namespace th in @@ -639,6 +626,8 @@ and add_decl env th = function close_namespace th n ~import:true | Export -> use_export th t + with Theory.ClashSymbol s -> + error ~loc (Clash s) end | Namespace (_, {id=id; id_loc=loc}, dl) -> let ns = get_namespace th in @@ -654,11 +643,15 @@ and add_decl env th = function | Inductive_def _ -> assert false (*TODO*) -let add_theory env pt = - let id = pt.th_name.id in - if M.mem id env.theories then error ~loc:pt.th_loc (ClashTheory id); +and add_theory env pt = + let id = pt.pt_name in + if M.mem id.id env.theories then error ~loc:pt.pt_loc (ClashTheory id.id); let t = type_theory env id pt in - { env with theories = M.add id t env.theories } + t, { env with theories = M.add id.id t env.theories } + +let add_theories = + List.fold_left + (fun env pt -> let _, env = add_theory env pt in env) (* Local Variables: diff --git a/src/parser/typing.mli b/src/parser/typing.mli index 2e675c10e..9a4ed7115 100644 --- a/src/parser/typing.mli +++ b/src/parser/typing.mli @@ -24,10 +24,12 @@ type env val create : string list -> env (** creates a new typing environment for a given loadpath *) -val add_theory : env -> Ptree.theory -> env +val add_theory : env -> Ptree.theory -> Theory.theory * env (** adds a local theory into the environment *) -val find_theory : env -> Ptree.qualid -> Theory.t +val add_theories : env -> Ptree.theory list -> env + +val find_theory : env -> Ptree.qualid -> Theory.theory (** searches for a theory using the environment's loadpath *) (** error reporting *) diff --git a/src/test.why b/src/test.why index 472b6e48e..fd1404447 100644 --- a/src/test.why +++ b/src/test.why @@ -3,47 +3,9 @@ theory A type t - logic c : t end theory B - 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 - type int -end - -theory Eq - - logic eq : 'a, 'a -> prop - - (* This part is just a definition of the equality *) - - (* This theory define eq but of course these axioms should not be send - to provers *) - - axiom refl : forall x:'a. eq(x,x) - axiom sym : forall x,y:'a. eq(x,y) -> eq(y,x) - axiom trans : forall x,y,z:'a. eq(x,y) -> eq(y,z) -> eq(x,z) - (* This one can't be written in first order logic. *) type t - type u - logic f : t -> u - axiom congru : forall x,y:t. eq(x,y) -> eq(f(x),f(y)) - -end - -(* -theory Test - - use Eq - use import L : List - axiom a : forall x : 'a. not Eq.eq(nil, cons(nil, nil)) - + use A end -*) -- GitLab