Commit 721efb49 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add support for programs in why3doc by reusing the namespace lookup from Typing in Mlw_typing.

parent 3804bb49
......@@ -82,6 +82,9 @@ val print_qualid: Format.formatter -> Ptree.qualid -> unit
val split_qualid : Ptree.qualid -> string list * string
val string_list_of_qualid : string list -> Ptree.qualid -> string list
val qloc : Ptree.qualid -> Loc.position
val find_ns : ('a -> Ident.ident) ->
('b -> string list -> 'a) -> Ptree.qualid -> 'b -> 'a
val find_lsymbol : Ptree.qualid -> theory_uc -> lsymbol
(*
val is_projection : theory_uc -> lsymbol -> (tysymbol * lsymbol * int) option
......
......@@ -138,19 +138,22 @@ let add_decl_with_tuples uc d = add_decl (flush_tuples uc) d
(** Namespace lookup *)
let uc_find_ls uc p =
let x = Typing.string_list_of_qualid [] p in
try ns_find_ls (Theory.get_namespace (get_theory uc)) x
with Not_found -> error ~loc:(qloc p) (UnboundSymbol p)
Typing.find_lsymbol p (get_theory uc)
let get_id_ts = function
| PT pt -> pt.its_pure.ts_name
| TS ts -> ts.ts_name
let uc_find_ts uc p =
let x = Typing.string_list_of_qualid [] p in
try ns_find_ts (get_namespace uc) x
with Not_found -> error ~loc:(qloc p) (UnboundSymbol p)
Typing.find_ns get_id_ts ns_find_ts p (get_namespace uc)
let get_id_ps = function
| PV pv -> pv.pv_vs.vs_name
| PS ps -> ps.ps_name
| PL pl -> pl.pl_ls.ls_name
| XS xs -> xs.xs_name
| LS ls -> ls.ls_name
let uc_find_ps uc p =
let x = Typing.string_list_of_qualid [] p in
try ns_find_ps (get_namespace uc) x
with Not_found -> error ~loc:(qloc p) (UnboundSymbol p)
Typing.find_ns get_id_ps ns_find_ps p (get_namespace uc)
(** Typing type expressions *)
......
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