load path

parent b752c15d
......@@ -76,12 +76,15 @@ let rec report fmt = function
fprintf fmt "anomaly: %s" (Printexc.to_string e)
let type_file env file =
let c = open_in file in
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let f = Lexer.parse_logic_file lb in
close_in c;
if !parse_only then env else Typing.add_theories env f
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_file env file
let extract_goals ctxt =
Transform.apply Transform.extract_goals ctxt
......@@ -91,7 +94,7 @@ let driver_rules = ref Driver.empty_rules
let transform env l =
let l = List.map
(fun t -> t, Context.use_export Context.create_context t)
(Typing.list_theory l) in
(Typing.local_theories l) in
let l = transformation l in
if !print_stdout then
List.iter
......
......@@ -21,18 +21,7 @@
open Format
open Lexing
open Driver_parser
type error =
| IllegalCharacter of char
| UnterminatedComment
| UnterminatedString
exception Error of error
let report fmt = function
| IllegalCharacter c -> fprintf fmt "illegal character %c" c
| UnterminatedComment -> fprintf fmt "unterminated comment"
| UnterminatedString -> fprintf fmt "unterminated string"
open Lexer
let keywords = Hashtbl.create 97
let () =
......@@ -46,18 +35,6 @@
"cloned", CLONED;
]
let newline lexbuf =
let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_p <-
{ pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
let string_buf = Buffer.create 1024
let char_for_backslash = function
| 'n' -> '\n'
| 't' -> '\t'
| c -> c
}
let space = [' ' '\t' '\r']
......@@ -88,36 +65,12 @@ rule token = parse
| "."
{ DOT }
| "\""
{ Buffer.clear string_buf; string lexbuf }
{ STRING (string lexbuf) }
| eof
{ EOF }
| _ as c
{ raise (Error (IllegalCharacter c)) }
and comment = parse
| "*)"
{ () }
| "(*"
{ comment lexbuf; comment lexbuf }
| '\n'
{ newline lexbuf; comment lexbuf }
| eof
{ raise (Error UnterminatedComment) }
| _
{ comment lexbuf }
and string = parse
| "\""
{ STRING (Buffer.contents string_buf) }
| "\\" (_ as c)
{ Buffer.add_char string_buf (char_for_backslash c); string lexbuf }
| '\n'
{ newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
| eof
{ raise (Error UnterminatedString) }
| _ as c
{ Buffer.add_char string_buf c; string lexbuf }
{
let loc lb = (lexeme_start_p lb, lexeme_end_p lb)
......
......@@ -17,10 +17,19 @@
(* *)
(**************************************************************************)
type error
type error =
| IllegalCharacter of char
| UnterminatedComment
| UnterminatedString
exception Error of error
val newline : Lexing.lexbuf -> unit
val comment : Lexing.lexbuf -> unit
val string : Lexing.lexbuf -> string
val report : Format.formatter -> error -> unit
val parse_logic_file : Lexing.lexbuf -> Ptree.logic_file
......@@ -227,7 +227,7 @@ rule token = parse
| "=>"
{ BIGARROW }
| "\""
{ Buffer.clear string_buf; string lexbuf }
{ STRING (string lexbuf) }
| eof
{ EOF }
| _ as c
......@@ -247,7 +247,9 @@ and comment = parse
and string = parse
| "\""
{ STRING (Buffer.contents string_buf) }
{ let s = Buffer.contents string_buf in
Buffer.clear string_buf;
s }
| "\\" (_ as c)
{ Buffer.add_char string_buf (char_for_backslash c); string lexbuf }
| newline
......
......@@ -21,31 +21,36 @@ open Ty
open Term
open Theory
let qualid_of_lstring = function
| [] -> invalid_arg "Transfrom_utils.qualid_of_lstring : empty list"
| a :: l ->
let id = Ptree.Qident {Ptree.id = a;id_loc = Loc.dummy_position} in
List.fold_left (fun acc x ->
Ptree.Qdot (acc,{Ptree.id = x;id_loc = Loc.dummy_position})) id l
let qualid_of_lstring s =
assert false (*TODO*)
(* let qualid_of_lstring = function *)
(* | [] -> invalid_arg "Transfrom_utils.qualid_of_lstring : empty list" *)
(* | a :: l -> *)
(* let id = Ptree.Qident {Ptree.id = a;id_loc = Loc.dummy_position} in *)
(* List.fold_left (fun acc x -> *)
(* Ptree.Qdot (acc,{Ptree.id = x;id_loc = Loc.dummy_position})) id l *)
let cloned_from_ts env ctxt l s ls1 =
try
let th = Typing.find_theory env (qualid_of_lstring 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
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 =
try
let th = Typing.find_theory env (qualid_of_lstring 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
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 =
try
let th = Typing.find_theory env (qualid_of_lstring 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
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 *)
......@@ -43,7 +43,7 @@ type error =
| BadNumberOfArguments of Ident.ident * int * int
| ClashTheory of string
| ClashNamespace of string
| UnboundTheory of string
| UnboundTheory of qualid
| AlreadyTheory of string
| UnboundNamespace of string
| UnboundFile of string
......@@ -102,8 +102,8 @@ let report fmt = function
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
| UnboundTheory q ->
fprintf fmt "unbound theory %a" print_qualid q
| AlreadyTheory s ->
fprintf fmt "already using a theory with name %s" s
| UnboundNamespace s ->
......@@ -130,11 +130,13 @@ 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;
}
......@@ -334,6 +336,14 @@ let rec qloc = function
| Qident x -> x.id_loc
| Qdot (m, x) -> Loc.join (qloc m) x.id_loc
let rec string_list_of_qualid acc = function
| Qident id -> id.id :: acc
| Qdot (p, id) -> string_list_of_qualid (id.id :: acc) p
let split_qualid = function
| Qident id -> [], id.id
| Qdot (p, id) -> string_list_of_qualid [] p, id.id
(* parsed types -> intermediate types *)
let rec type_inst s ty = match ty.ty_node with
......@@ -1023,43 +1033,13 @@ let add_inductives dl th =
let dl = List.map type_decl dl in
add_decl th (create_ind_decl dl)
let find_in_loadpath env f =
let rec find c lp = match lp, c with
| [], None ->
error ~loc:f.id_loc (NotInLoadpath f.id)
| [], Some file ->
file
| dir :: lp, _ ->
let file = Filename.concat dir f.id in
if Sys.file_exists file then begin match c with
| None -> find (Some file) lp
| Some file' -> error ~loc:f.id_loc (AmbiguousPath (file, file'))
end else
find c lp
in
find None env.loadpath
let locate_file env q =
let rec locate_dir = function
| Qident d ->
find_in_loadpath env d
| Qdot (q, d) ->
let dir = locate_dir q in
let dir = Filename.concat dir d.id in
if not (Sys.file_exists dir) then error ~loc:d.id_loc (UnboundDir dir);
dir
in
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 -> string -> Theory.t *)
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_file file =
......@@ -1075,35 +1055,27 @@ let prop_kind = function
| Kgoal -> Pgoal
| Klemma -> Plemma
let rec find_theory env q = match q with
| Qident id ->
let rec find_theory env q id = match q with
| [] ->
(* local theory *)
begin
try M.find id.id env.theories
with Not_found -> error ~loc:id.id_loc (UnboundTheory id.id)
end
| Qdot (f, id) ->
M.find id env.theories
| _ :: _ ->
(* theory in file f *)
let file = locate_file env f in
if not (Hashtbl.mem loaded_theories file) then begin
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 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);
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 loaded_theories file in
try Hashtbl.find h id.id
with Not_found -> error ~loc:id.id_loc (UnboundTheory id.id)
let h = Hashtbl.find env.loaded_theories q in
M.find id h
and type_theory env id pt =
(* TODO: use long name *)
let n = id_user id.id id.id_loc in
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
close_theory th
......@@ -1120,7 +1092,14 @@ and add_decl env th = function
| PropDecl (loc, k, s, f) ->
add_prop (prop_kind k) loc s f th
| UseClone (loc, use, subst) ->
let t = find_theory env use.use_theory in
let q, id = split_qualid use.use_theory in
let t =
try
find_theory env q id
with
| Not_found -> error ~loc (UnboundTheory use.use_theory)
| Error (AmbiguousPath _ as e) -> error ~loc e
in
let use_or_clone th = match subst with
| None ->
use_export th t
......@@ -1186,17 +1165,25 @@ and add_decl env th = function
let th = add_decls env th dl in
close_namespace th import id
and add_theory env pt =
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 =
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
t, { env with theories = M.add id.id t env.theories }
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
let add_theories =
List.fold_left
(fun env pt -> let _, env = add_theory env pt in env)
and add_file env file =
let tl = load_file file in
List.fold_left (type_and_add_theory "") env tl
let list_theory env =
let local_theories env =
List.rev (M.fold (fun _ v acc -> v::acc) env.theories [])
(*
......
......@@ -24,15 +24,16 @@ type env
val create : string list -> env
(** creates a new typing environment for a given loadpath *)
val add_theory : env -> Ptree.theory -> Theory.theory * env
(** adds a local theory into the environment *)
val add_theory : env -> Theory.theory -> env
(** add a local theory *)
val add_theories : env -> Ptree.theory list -> env
val add_file : env -> string -> env
(** add local theories from a given file *)
val find_theory : env -> Ptree.qualid -> Theory.theory
val find_theory : env -> string list -> string -> Theory.theory
(** searches for a theory using the environment's loadpath *)
val list_theory : env -> Theory.theory list
val local_theories : env -> Theory.theory list
(** error reporting *)
......
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