simplified typing of use/clone declarations

parent 2f34052b
......@@ -390,12 +390,12 @@ $(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
byte: bin/why3ml.byte
opt: bin/why3ml.opt
bin/why3ml.opt: src/why3.cmxa $(PGMCMX) src/main.cmx
bin/why3ml.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) src/main.cmx
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
bin/why3ml.byte: src/why3.cma $(PGMCMO) src/main.cmo
bin/why3ml.byte: src/why3.cma $(PGMCMO) $(MLWCMO) src/main.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
......@@ -573,12 +573,12 @@ bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(IDECMX)
bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) $(IDECMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
bin/why3ide.byte: src/why3.cma $(PGMCMO) $(IDECMO)
bin/why3ide.byte: src/why3.cma $(PGMCMO) $(MLWCMO) $(IDECMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
......
......@@ -179,8 +179,6 @@ let read_lib_theory lib path th =
try Mstr.find th mth with Not_found ->
raise (TheoryNotFound (path,th))
let read_lib_file lib path = fst (read_lib_file lib path)
let register_format name exts read =
if Hashtbl.mem read_format_table name then raise (KnownFormat name);
let getlib = Wenv.memoize 5 (mk_library read exts) in
......
......@@ -114,7 +114,7 @@ val env_of_library : 'a library -> env
val list_formats : unit -> (fformat * extension list) list
(** [list_formats ()] returns the list of registered formats *)
val read_lib_file : 'a library -> pathname -> 'a
val read_lib_file : 'a library -> pathname -> 'a * theory Mstr.t
(** [read_lib_file lib path] retrieves the contents of a library file
@raise LibFileNotFound [path] if the library file was not found *)
......
......@@ -663,7 +663,6 @@ let is_empty_sm sm =
Mls.is_empty sm.sm_ls &&
Mpr.is_empty sm.sm_pr
(** Meta properties *)
let get_meta_arg_type = function
......
......@@ -124,6 +124,7 @@ val close_theory : theory_uc -> theory
val open_namespace : theory_uc -> theory_uc
val close_namespace : theory_uc -> bool -> string option -> theory_uc
(* the Boolean indicates [import]; the string option indicates [as T] *)
val get_namespace : theory_uc -> namespace
val get_known : theory_uc -> known_map
......
......@@ -62,6 +62,7 @@ module Incremental = struct
let new_use_clone d =
let env = ref_get env_ref in let lenv = ref_get lenv_ref in
ref_set uc_ref (Typing.add_use_clone env lenv (ref_get uc_ref) d)
end
open Ptree
......@@ -184,6 +185,9 @@ end
| Term.IConstBinary s -> int_of_string ("0b"^s)
with Failure _ -> raise Parsing.Parse_error
let qualid_last = function
| Qident x | Qdot (_, x) -> x.id
%}
/* Tokens */
......@@ -316,7 +320,7 @@ namespace_import:
;
namespace_name:
| uident { Some $1 }
| uident { Some $1.id }
| UNDERSCORE { None }
;
......@@ -354,17 +358,17 @@ use_clone:
use:
| imp_exp tqualid
{ { use_theory = $2; use_as = None; use_imp_exp = $1 } }
{ { use_theory = $2; use_as = Some (qualid_last $2); use_imp_exp = $1 } }
| imp_exp tqualid AS uident
{ { use_theory = $2; use_as = Some (Some $4); use_imp_exp = $1 } }
{ { use_theory = $2; use_as = Some $4.id; use_imp_exp = $1 } }
| imp_exp tqualid AS UNDERSCORE
{ { use_theory = $2; use_as = Some None; use_imp_exp = $1 } }
{ { use_theory = $2; use_as = None; use_imp_exp = $1 } }
;
imp_exp:
| IMPORT { Import }
| EXPORT { Export }
| /* epsilon */ { Nothing }
| IMPORT { Some true }
| EXPORT { None }
| /* epsilon */ { Some false }
;
clone_subst:
......@@ -378,13 +382,13 @@ list1_comma_subst:
;
subst:
| NAMESPACE ns EQUAL ns { CSns ($2, $4) }
| TYPE qualid EQUAL qualid { CStsym ($2, $4) }
| CONSTANT qualid EQUAL qualid { CSfsym ($2, $4) }
| FUNCTION qualid EQUAL qualid { CSfsym ($2, $4) }
| PREDICATE qualid EQUAL qualid { CSpsym ($2, $4) }
| LEMMA qualid { CSlemma $2 }
| GOAL qualid { CSgoal $2 }
| NAMESPACE ns EQUAL ns { CSns (floc (), $2, $4) }
| TYPE qualid EQUAL qualid { CStsym (floc (), $2, $4) }
| CONSTANT qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| FUNCTION qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| PREDICATE qualid EQUAL qualid { CSpsym (floc (), $2, $4) }
| LEMMA qualid { CSlemma (floc (), $2) }
| GOAL qualid { CSgoal (floc (), $2) }
;
ns:
......@@ -1062,9 +1066,9 @@ opt_semicolon:
use_module:
| imp_exp MODULE tqualid
{ Duse ($3, $1, None) }
{ Duse ($3, $1, Some (qualid_last $3)) }
| imp_exp MODULE tqualid AS uident
{ Duse ($3, $1, Some $5) }
{ Duse ($3, $1, Some $5.id) }
;
list1_recfun_sep_and:
......
......@@ -94,22 +94,21 @@ type plogic_type =
| PPredicate of pty list
| PFunction of pty list * pty
type imp_exp =
| Import | Export | Nothing
type use = {
use_theory : qualid;
use_as : ident option option;
use_imp_exp : imp_exp;
use_as : string option;
(* None = as _, Some id = as id *)
use_imp_exp : bool option;
(* None = export, Some false = default, Some true = import *)
}
type clone_subst =
| CSns of qualid option * qualid option
| CStsym of qualid * qualid
| CSfsym of qualid * qualid
| CSpsym of qualid * qualid
| CSlemma of qualid
| CSgoal of qualid
| CSns of loc * qualid option * qualid option
| CStsym of loc * qualid * qualid
| CSfsym of loc * qualid * qualid
| CSpsym of loc * qualid * qualid
| CSlemma of loc * qualid
| CSgoal of loc * qualid
type is_mutable = bool
......@@ -246,8 +245,8 @@ type program_decl =
| Dparam of ident * type_v
| Dexn of ident * pty option
(* modules *)
| Duse of qualid * imp_exp * (*as:*) ident option
| Dnamespace of loc * ident option * (* import: *) bool * program_decl list
| Duse of qualid * bool option * (*as:*) string option
| Dnamespace of loc * string option * (* import: *) bool * program_decl list
type theory = {
pth_name : ident;
......
......@@ -31,7 +31,6 @@ open Denv
(** errors *)
exception Message of string
exception DuplicateTypeVar of string
exception TypeArity of qualid * int * int
exception Clash of string
......@@ -47,28 +46,15 @@ exception UnboundTypeVar of string
exception UnboundType of string list
exception UnboundSymbol of string list
let error ?loc e = match loc with
| None -> raise e
| Some loc -> raise (Loc.Located (loc,e))
let errorm ?loc f =
let buf = Buffer.create 512 in
let fmt = Format.formatter_of_buffer buf in
Format.kfprintf
(fun _ ->
Format.pp_print_flush fmt ();
let s = Buffer.contents buf in
Buffer.clear buf;
error ?loc (Message s))
fmt f
let error = Loc.error
let errorm = Loc.errorm
let rec print_qualid fmt = function
| Qident s -> fprintf fmt "%s" s.id
| Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
let () = Exn_printer.register (fun fmt e -> match e with
| Message s ->
fprintf fmt "%s" s
| DuplicateTypeVar s ->
fprintf fmt "duplicate type parameter %s" s
| TypeArity (id, a, n) ->
......@@ -1135,6 +1121,44 @@ let add_decl th = function
let add_decl th d =
if Debug.test_flag debug_parse_only then th else add_decl th d
let type_inst th t s =
let add_inst s = function
| CSns (loc,p,q) ->
let find ns x = find_namespace_ns x ns in
let ns1 = option_fold find t.th_export p in
let ns2 = option_fold find (get_namespace th) q in
clone_ns loc t.th_local ns2 ns1 s
| CStsym (loc,p,q) ->
let ts1 = find_tysymbol_ns p t.th_export in
let ts2 = find_tysymbol q th in
if Mts.mem ts1 s.inst_ts
then error ~loc (Clash ts1.ts_name.id_string);
{ s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
| CSfsym (loc,p,q) ->
let ls1 = find_fsymbol_ns p t.th_export in
let ls2 = find_fsymbol q th in
if Mls.mem ls1 s.inst_ls
then error ~loc (Clash ls1.ls_name.id_string);
{ s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
| CSpsym (loc,p,q) ->
let ls1 = find_psymbol_ns p t.th_export in
let ls2 = find_psymbol q th in
if Mls.mem ls1 s.inst_ls
then error ~loc (Clash ls1.ls_name.id_string);
{ s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
| CSlemma (loc,p) ->
let pr = find_prop_ns p t.th_export in
if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
then error ~loc (Clash pr.pr_name.id_string);
{ s with inst_lemma = Spr.add pr s.inst_lemma }
| CSgoal (loc,p) ->
let pr = find_prop_ns p t.th_export in
if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
then error ~loc (Clash pr.pr_name.id_string);
{ s with inst_goal = Spr.add pr s.inst_goal }
in
List.fold_left add_inst empty_inst s
let add_use_clone env lenv th (loc, use, subst) =
if Debug.test_flag debug_parse_only then th else
let q, id = split_qualid use.use_theory in
......@@ -1145,65 +1169,17 @@ let add_use_clone env lenv th (loc, use, subst) =
| TheoryNotFound _ -> error ~loc (UnboundTheory use.use_theory)
in
let use_or_clone th = match subst with
| None ->
use_export th t
| Some s ->
let add_inst s = function
| CSns (p,q) ->
let find ns x = find_namespace_ns x ns in
let ns1 = option_fold find t.th_export p in
let ns2 = option_fold find (get_namespace th) q in
clone_ns loc t.th_local ns2 ns1 s
| CStsym (p,q) ->
let ts1 = find_tysymbol_ns p t.th_export in
let ts2 = find_tysymbol q th in
if Mts.mem ts1 s.inst_ts
then error ~loc (Clash ts1.ts_name.id_string);
{ s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
| CSfsym (p,q) ->
let ls1 = find_fsymbol_ns p t.th_export in
let ls2 = find_fsymbol q th in
if Mls.mem ls1 s.inst_ls
then error ~loc (Clash ls1.ls_name.id_string);
{ s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
| CSpsym (p,q) ->
let ls1 = find_psymbol_ns p t.th_export in
let ls2 = find_psymbol q th in
if Mls.mem ls1 s.inst_ls
then error ~loc (Clash ls1.ls_name.id_string);
{ s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
| CSlemma p ->
let pr = find_prop_ns p t.th_export in
if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
then error ~loc (Clash pr.pr_name.id_string);
{ s with inst_lemma = Spr.add pr s.inst_lemma }
| CSgoal p ->
let pr = find_prop_ns p t.th_export in
if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
then error ~loc (Clash pr.pr_name.id_string);
{ s with inst_goal = Spr.add pr s.inst_goal }
in
let s = List.fold_left add_inst empty_inst s in
clone_export th t s
in
let n = match use.use_as with
| None -> Some t.th_name.id_string
| Some (Some x) -> Some x.id
| Some None -> None
| None -> use_export th t
| Some s -> clone_export th t (type_inst th t s)
in
begin try match use.use_imp_exp with
| Nothing ->
(* use T = namespace T use_export T end *)
let th = open_namespace th in
let th = use_or_clone th in
close_namespace th false n
| Import ->
(* use import T = namespace T use_export T end import T *)
let th = open_namespace th in
let th = use_or_clone th in
close_namespace th true n
| Export ->
use_or_clone th
| Some imp ->
(* use T = namespace T use_export T end *)
let th = open_namespace th in
let th = use_or_clone th in
close_namespace th imp use.use_as
| None ->
use_or_clone th
with ClashSymbol s -> error ~loc (Clash s)
end
......@@ -1214,13 +1190,12 @@ let close_theory loc lenv th =
if Mstr.mem id lenv then error ~loc (ClashTheory id);
Mstr.add id th lenv
let close_namespace loc import name th =
let id = option_map (fun id -> id.id) name in
let close_namespace loc import id th =
try close_namespace th import id
with ClashSymbol s -> error ~loc (Clash s)
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. test"
compile-command: "unset LANG; make -C ../.."
End:
*)
......@@ -35,7 +35,7 @@ val add_use_clone :
unit Env.library -> theory Mstr.t -> theory_uc -> Ptree.use_clone -> theory_uc
val close_namespace :
Loc.position -> bool -> Ptree.ident option -> theory_uc -> theory_uc
Loc.position -> bool -> string option -> theory_uc -> theory_uc
val close_theory : Loc.position -> theory Mstr.t -> theory_uc -> theory Mstr.t
......@@ -95,3 +95,4 @@ val list_fields: theory_uc ->
(** check that the given fields all belong to the same record type
and do not appear several times *)
val type_inst: theory_uc -> theory -> Ptree.clone_subst list -> th_inst
......@@ -2262,7 +2262,7 @@ let find_module penv lmod q id = match q with
Mstr.find id lmod
| _ :: _ ->
(* module in file f *)
Mstr.find id (Env.read_lib_file penv q)
Mstr.find id (fst (Env.read_lib_file penv q))
(* env = to retrieve theories and modules from the loadpath
lmod = local modules *)
......@@ -2346,22 +2346,13 @@ let rec decl ~wp env ltm lmod uc = function
with Not_found ->
errorm ~loc "@[unbound module %a@]" print_qualid qid
in
let n = match use_as with
| None -> Some (m.m_name.id_string)
| Some x -> Some x.id
in
begin try match imp_exp with
| Nothing ->
| Some imp ->
(* use T = namespace T use_export T end *)
let uc = open_namespace uc in
let uc = use_export uc m in
close_namespace uc false n
| Import ->
(* use import T = namespace T use_export T end import T *)
let uc = open_namespace uc in
let uc = use_export uc m in
close_namespace uc true n
| Export ->
close_namespace uc imp use_as
| None ->
use_export uc m
with ClashSymbol s ->
errorm ~loc "clash with previous symbol %s" s
......@@ -2369,7 +2360,6 @@ let rec decl ~wp env ltm lmod uc = function
| Ptree.Dnamespace (loc, id, import, dl) ->
let uc = open_namespace uc in
let uc = List.fold_left (decl ~wp env ltm lmod) uc dl in
let id = option_map (fun id -> id.id) id in
begin try close_namespace uc import id
with ClashSymbol s -> errorm ~loc "clash with previous symbol %s" s end
| Ptree.Dlogic (TypeDecl d) ->
......
......@@ -26,5 +26,5 @@ val register : exn_printer -> unit
(* Register a formatter of exception *)
val exn_printer : exn_printer
(* exn_printer fmt exn : print the exception using all the previously
registered printer and return *)
(* [exn_printer fmt exn] prints exception [exn] using all previously
registered printers and returns *)
......@@ -54,8 +54,6 @@ let user_position fname lnum cnum1 cnum2 = (fname,lnum,cnum1,cnum2)
let get loc = loc
exception Located of position * exn
let dummy_position = ("",0,0,0)
let join (f1,l1,b1,e1) (f2,_,b2,e2) =
......@@ -77,9 +75,44 @@ let gen_report_position fmt (f,l,b,e) =
let report_position fmt = fprintf fmt "%a:@\n" gen_report_position
(* located exceptions *)
exception Located of position * exn
let try1 loc f x =
try f x with Located _ as e -> raise e | e -> raise (Located (loc, e))
let try2 loc f x y =
try f x y with Located _ as e -> raise e | e -> raise (Located (loc, e))
let try3 loc f x y z =
try f x y z with Located _ as e -> raise e | e -> raise (Located (loc, e))
let try4 loc f x y z t =
try f x y z t with Located _ as e -> raise e | e -> raise (Located (loc, e))
let error ?loc e = match loc with
| None -> raise e
| Some loc -> raise (Located (loc, e))
(* located messages *)
exception Message of string
let errorm ?loc f =
let buf = Buffer.create 512 in
let fmt = Format.formatter_of_buffer buf in
Format.kfprintf
(fun _ ->
Format.pp_print_flush fmt ();
let s = Buffer.contents buf in
Buffer.clear buf;
error ?loc (Message s))
fmt f
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Located (loc,e) ->
fprintf fmt "%a%a" report_position loc Exn_printer.exn_printer e
| _ -> raise exn)
| Message s ->
fprintf fmt "%s" s
| _ ->
raise exn)
......@@ -34,8 +34,6 @@ type position
val extract : Lexing.position * Lexing.position -> position
val join : position -> position -> position
exception Located of position * exn
val dummy_position : position
val user_position : string -> int -> int -> int -> position
......@@ -50,3 +48,19 @@ val gen_report_position : formatter -> position -> unit
val report_position : formatter -> position -> unit
(* located exceptions *)
exception Located of position * exn
val try1: position -> ('a -> 'b) -> 'a -> 'b
val try2: position -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'c
val try3: position -> ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
val try4: position -> ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> 'e
val error: ?loc:position -> exn -> 'a
(* messages *)
exception Message of string
val errorm: ?loc:position -> ('a, Format.formatter, unit, 'b) format4 -> 'a
......@@ -19,6 +19,7 @@
open Why3
open Util
open Ident
open Theory
open Env
open Ptree
......@@ -28,23 +29,94 @@ type mlw_contents = modul Mstr.t
type mlw_library = mlw_contents library
type mlw_file = mlw_contents * Theory.theory Mstr.t
(* let type_only = Debug.test_flag Typing.debug_type_only in *)
(* TODO: let type_only = Debug.test_flag Typing.debug_type_only in *)
let add_theory _lib path mt m =
let find_theory loc lib path s =
(* search first in .mlw files (using lib) *)
let thm =
try Some (Env.read_lib_theory lib path s)
with LibFileNotFound _ | TheoryNotFound _ -> None
in
(* search also in .why files *)
let th =
try Some (Env.find_theory (Env.env_of_library lib) path s)
with LibFileNotFound _ | TheoryNotFound _ -> None
in
match thm, th with
| Some _, Some _ ->
Loc.errorm ~loc
"a module/theory %s is defined both in Why and WhyML libraries" s
| None, None -> Loc.error ~loc (Env.TheoryNotFound (path, s))
| None, Some t | Some t, None -> t
let find_theory loc lib mt path s = match path with
| [] -> (* local theory *)
begin try Mstr.find s mt with Not_found -> find_theory loc lib [] s end
| _ :: _ -> (* theory in file path *)
find_theory loc lib path s
type theory_or_module = Theory of Theory.theory | Module of modul
let find_module loc lib path s =
(* search first in .mlw files *)
let m, thm =
try
let mm, mt = Env.read_lib_file lib path in
Mstr.find_option s mm, Mstr.find_option s mt
with
| LibFileNotFound _ -> None, None
in
(* search also in .why files *)
let th =
try Some (Env.find_theory (Env.env_of_library lib) path s)
with LibFileNotFound _ | TheoryNotFound _ -> None
in
match m, thm, th with
| Some _, None, _ -> assert false
| _, Some _, Some _ ->
Loc.errorm ~loc
"a module/theory %s is defined both in Why and WhyML libraries" s
| None, None, None -> Loc.error ~loc (Env.TheoryNotFound (path, s))
| Some m, Some _, None -> Module m
| None, Some t, None | None, None, Some t -> Theory t
let find_module loc lib mt mm path s = match path with
| [] -> (* local module/theory *)
begin try Module (Mstr.find s mm)
with Not_found -> begin try Theory (Mstr.find s mt)
with Not_found -> find_module loc lib [] s end end
| _ :: _ -> (* module/theory in file path *)
find_module loc lib path s
let add_theory lib path mt m =
let id = m.pth_name in
let loc = id.id_loc in
let uc = Theory.create_theory ~path (Denv.create_user_id id) in
let rec add_decl uc = function
| Duseclone (_loc, _use, None) (* use *) ->
assert false (*TODO*)
| Duseclone (_loc, _use, Some _s) (* clone *) ->
assert false (*TODO*)
| Duseclone (loc, use, inst) ->
let path, s = Typing.split_qualid use.use_theory in
let th = find_theory loc lib mt path s in
(* open namespace, if any *)
let uc =
if use.use_imp_exp <> None then Theory.open_namespace uc else uc in
(* use or clone *)
let uc = match inst with
| None -> Theory.use_export uc th
| Some inst ->
let inst = Typing.type_inst uc th inst in
Theory.clone_export uc th inst
in
(* close namespace, if any *)
begin match use.use_imp_exp with
| None -> uc
| Some imp -> Theory.close_namespace uc imp use.use_as
end
| Dlogic d ->
Typing.add_decl uc d
| Dnamespace (loc, name, import, dl) ->
let uc = Theory.open_namespace uc in
let uc = List.fold_left add_decl uc dl in
Typing.close_namespace loc import name uc
Loc.try3 loc Theory.close_namespace uc import name
| Dlet _ | Dletrec _ | Dparam _ | Dexn _ | Duse _ ->
assert false
in
......
theory T
type t = int
goal G : forall x: t. x=0
end
(*
Local Variables:
compile-command: "unset LANG; ../bin/why3ide test-pgm-jcf.mlx"
End:
*)
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