Commit fc2f7b50 authored by Andrei Paskevich's avatar Andrei Paskevich

move find_ts/find_ls/find_pr functions to Theory,

provide ns_find_prop and ns_find_fmla for convenience
parent 685011c9
......@@ -13,8 +13,8 @@ let make_rt_rf h =
let rec rt env t =
let t = t_map (rt env) (rf env) t in
let array = find_theory env prelude array in
let store = (find_ls array.th_export store).ls_name in
let select = (find_ls array.th_export select).ls_name in
let store = (ns_find_ls array.th_export store).ls_name in
let select = (ns_find_ls array.th_export select).ls_name in
match t.t_node with
| Tapp (lselect,[{t_node=Tapp(lstore,[_;a1;b])};a2])
when lselect.ls_name == select &&
......
......@@ -516,6 +516,7 @@ let find_theory env sl s =
let env_tag env = env.env_tag
(** Context constructors and utilities *)
type th_inst = {
......@@ -856,6 +857,21 @@ module Context = struct
end
(** Namespace search tools *)
let rec ns_find get_map ns = function
| [] -> assert false
| [a] -> Mnm.find a (get_map ns)
| a::l -> ns_find get_map (Mnm.find a ns.ns_ns) l
let ns_find_ts = ns_find (fun ns -> ns.ns_ts)
let ns_find_ls = ns_find (fun ns -> ns.ns_ls)
let ns_find_pr = ns_find (fun ns -> ns.ns_pr)
let ns_find_prop ns sl = fst (ns_find_pr ns sl)
let ns_find_fmla ns sl = snd (ns_find_pr ns sl)
(** Theory constructors and utilities *)
type theory_uc = {
......
......@@ -191,6 +191,15 @@ module Context : sig
end
(** Namespace search tools *)
val ns_find_ts : namespace -> string list -> tysymbol
val ns_find_ls : namespace -> string list -> lsymbol
val ns_find_pr : namespace -> string list -> prop_fmla
val ns_find_prop : namespace -> string list -> prop
val ns_find_fmla : namespace -> string list -> fmla
(** Theory constructors and utilities *)
type theory_uc (* a theory under construction *)
......
......@@ -234,14 +234,14 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
begin
try
add_htheory c
(pr_name (fst (Transform.find_pr th.th_export q))) Remove
(pr_name (ns_find_prop th.th_export q)) Remove
with Not_found -> errorm ~loc "Unknown axioms %s"
(string_of_qualid qualid q)
end
| Rsyntaxls ((loc,q),s) ->
begin
try
let ls = (Transform.find_ls th.th_export q) in
let ls = ns_find_ls th.th_export q in
check_syntax loc s (List.length ls.ls_args);
add_htheory false ls.ls_name (Syntax s)
with Not_found -> errorm ~loc "Unknown logic %s"
......@@ -250,7 +250,7 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
| Rsyntaxty ((loc,q),s) ->
begin
try
let ts = Transform.find_ts th.th_export q in
let ts = ns_find_ts th.th_export q in
check_syntax loc s (List.length ts.ts_args);
add_htheory false ts.ts_name (Syntax s)
with Not_found -> errorm ~loc "Unknown type %s"
......@@ -259,7 +259,7 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
| Rtagls (c,(loc,q),s) ->
begin
try
add_htheory c (Transform.find_ls th.th_export q).ls_name
add_htheory c (ns_find_ls th.th_export q).ls_name
(Tag (Snm.singleton s))
with Not_found -> errorm ~loc "Unknown logic %s"
(string_of_qualid qualid q)
......@@ -267,7 +267,7 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
| Rtagty (c,(loc,q),s) ->
begin
try
add_htheory c (Transform.find_ts th.th_export q).ts_name
add_htheory c (ns_find_ts th.th_export q).ts_name
(Tag (Snm.singleton s))
with Not_found -> errorm ~loc "Unknown type %s"
(string_of_qualid qualid q)
......@@ -275,7 +275,7 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
| Rtagpr (c,(loc,q),s) ->
begin
try
add_htheory c (pr_name (fst (Transform.find_pr th.th_export q)))
add_htheory c (pr_name (ns_find_prop th.th_export q))
(Tag (Snm.singleton s))
with Not_found -> errorm ~loc "Unknown proposition %s"
(string_of_qualid qualid q)
......
......@@ -261,22 +261,6 @@ let rewrite_elt rt rf = elt (rewrite_elt rt rf)
let rewrite_env rt rf =
elt_env (rewrite_env rt rf)
let rec find_ls ns = function
| [] -> assert false
| [a] -> Mnm.find a ns.ns_ls
| a::l -> find_ls (Mnm.find a ns.ns_ns) l
let rec find_ts ns = function
| [] -> assert false
| [a] -> Mnm.find a ns.ns_ts
| a::l -> find_ts (Mnm.find a ns.ns_ns) l
let rec find_pr ns = function
| [] -> assert false
| [a] -> Mnm.find a ns.ns_pr
| a::l -> find_pr (Mnm.find a ns.ns_ns) l
let cloned_from ctxt i1 i2 =
try
i1 = i2 || Sid.mem i2 (Mid.find i1 ctxt.ctxt_cloned)
......
......@@ -115,6 +115,3 @@ val rewrite_env :
val cloned_from : context -> ident -> ident -> bool
val find_ts : namespace -> string list -> Ty.tysymbol
val find_ls : namespace -> string list -> Term.lsymbol
val find_pr : namespace -> string list -> prop_fmla
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