Commit d7f70bf2 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Reflection: find qualified program symbols even in own module

parent cf331208
......@@ -565,7 +565,7 @@ let print_meta_arg fmt = function
| MApr pr -> fprintf fmt "prop %a" print_pr pr
| MAstr s -> fprintf fmt "\"%s\"" s
| MAint i -> fprintf fmt "%d" i
| MAident i -> Ident.print_decoded fmt (id_unique sprinter i)
| MAident i -> fprintf fmt "%a" Ident.print_decoded (id_unique sprinter i)
let print_qt fmt th =
if th.th_path = [] then print_th fmt th else
......
......@@ -430,7 +430,6 @@ let store_path, store_theory, restore_path, restore_theory =
Wid.set id_to_th id th;
end
in
let restore_path id = Wid.find id_to_path id in
let restore_theory id = Wid.find id_to_th id in
store_path, store_theory, restore_path, restore_theory
......
......@@ -287,19 +287,27 @@ let add_meta uc m al = { uc with
muc_theory = Theory.add_meta uc.muc_theory m al;
muc_units = Umeta (m,al) :: uc.muc_units; }
let store_path, store_module, restore_path =
let store_path, store_module, restore_path, restore_module_id =
let id_to_path = Wid.create 17 in
let id_to_pmod = Wid.create 17 in
let store_path {muc_theory = uc} path id =
(* this symbol already belongs to some theory *)
if Wid.mem id_to_path id then () else
let prefix = List.rev (id.id_string :: path @ uc.uc_prefix) in
Wid.set id_to_path id (uc.uc_path, uc.uc_name.id_string, prefix) in
let store_module {mod_theory = {th_name = id} as th} =
let store_module pmod =
let th = pmod.mod_theory in
let id = th.th_name in
(* this symbol is already a module *)
if Wid.mem id_to_path id then () else
Wid.set id_to_path id (th.th_path, id.id_string, []) in
if Wid.mem id_to_path id then () else begin
Wid.set id_to_path id (th.th_path, id.id_string, []);
Sid.iter (fun id -> Wid.set id_to_pmod id pmod) pmod.mod_local;
Wid.set id_to_pmod id pmod;
end
in
let restore_path id = Wid.find id_to_path id in
store_path, store_module, restore_path
let restore_module_id id = Wid.find id_to_pmod id in
store_path, store_module, restore_path, restore_module_id
let close_module uc =
let m = close_module uc in
......
......@@ -113,6 +113,10 @@ val restore_path : ident -> string list * string * string list
If [id] is a module name, the third component is an empty list.
Raises Not_found if the ident was never declared in/as a module. *)
val restore_module_id : ident -> pmodule
(** retrieves a module from a program symbol defined in it
Raises Not_found if the ident was never declared in/as a module. *)
val restore_module : theory -> pmodule
(** retrieves a module from its underlying theory
raises [Not_found] if no such module exists *)
......
......@@ -28,6 +28,12 @@ let debug_refl = Debug.register_info_flag
let expl_reification_check = Ident.create_attribute "expl:reification check"
let meta_decision_procedure =
Theory.register_meta
~desc:"decision procedure, used for reflection"
"reflection"
[ Theory.MTident ]
type reify_env = { kn: known_map;
store: (vsymbol * int) Mterm.t;
fr: int;
......@@ -312,7 +318,7 @@ let rec reify_term renv t rt =
end
and invert_interp renv ls (t:term) =
let ld = try Opt.get (find_logic_definition renv.kn ls)
with Invalid_argument _ ->
with Invalid_argument _ | Not_found ->
Debug.dprintf debug_reification
"did not find def of %a@."
Pretty.print_ls ls;
......@@ -349,10 +355,11 @@ let rec reify_term renv t rt =
raise NoReification
and invert_ctx_interp renv ls t l g =
let ld = try Opt.get (find_logic_definition renv.kn ls)
with Invalid_argument _ ->
with | Not_found ->
Debug.dprintf debug_reification "did not find def of %a@."
Pretty.print_ls ls;
raise NoReification
| Invalid_argument _ -> assert false
in
let vl, f = open_ls_defn ld in
Debug.dprintf debug_reification "invert_ctx_interp ls %a @."
......@@ -435,6 +442,9 @@ let rec reify_term renv t rt =
Pretty.print_ty (Opt.get t.t_ty)
Pretty.print_ty (Opt.get rt.t_ty);
raise NoReification);
Debug.dprintf debug_reification "known map: %a@."
(Pp.print_list Pp.newline (fun fmt id -> Format.fprintf fmt "%s" id.id_string))
(Mid.keys renv.kn);
match t.t_node, rt.t_node with
| _, Tapp(interp, {t_node = Tvar vx}::vyl)
when List.mem vx renv.lv
......@@ -621,6 +631,8 @@ open Expr
open Ity
open Wstdlib
open Mlinterp
open Theory
open Pmodule
exception ReductionFail of reify_env
......@@ -632,21 +644,30 @@ let reflection_by_function do_trans s env = Trans.store (fun task ->
let g, prev = Task.task_separate_goal task in
let g = Apply.term_decl g in
let ths = Task.used_theories task in
let o =
Mid.fold
(fun _ th o ->
try
let pmod = Pmodule.restore_module th in
let rs = Pmodule.ns_find_rs pmod.Pmodule.mod_export [s] in
if o = None then Some (pmod, rs)
else (let es = Format.sprintf "module or function %s found twice" s in
raise (Arg_error es))
with Not_found -> o)
ths None in
let (_pmod, rs) = if o = None
then (let es = Format.sprintf "Symbol %s not found@." s in
raise (Arg_error es))
else Opt.get o in
let re_dot = Str.regexp_string "." in
let qs = Str.split re_dot s in
let fname = List.hd (List.rev qs) in
Debug.dprintf debug_refl "looking for symbol %s@." fname;
let (pmod, rs) =
let fn acc = function
| [ MAident id ] ->
Debug.dprintf debug_refl "found symbol %s@." id.id_string;
if id.id_string = fname
then id :: acc
else acc
| _ -> assert false in
begin match on_meta meta_decision_procedure fn [] task with
| [] ->
Debug.dprintf debug_refl "symbol not found in current goal@.";
let es = Format.sprintf "Symbol %s not found@." s in
raise (Arg_error es)
| [id] ->
let pm = restore_module_id id in
Debug.dprintf debug_refl "symbol in module %s@." pm.mod_theory.th_name.id_string;
(pm, ns_find_rs pm.mod_export qs)
| _ -> raise (Arg_error "symbol found twice")
end
in
let lpost = List.map open_post rs.rs_cty.cty_post in
if List.exists (fun pv -> pv.pv_ghost) rs.rs_cty.cty_args
then (Debug.dprintf debug_refl "ghost parameter@.";
......@@ -658,7 +679,7 @@ let reflection_by_function do_trans s env = Trans.store (fun task ->
let pm = Pmodule.restore_module th in
Mstr.add id.id_string pm acc
with Not_found -> acc)
ths Mstr.empty in
ths (Mstr.singleton pmod.mod_theory.th_name.id_string pmod) in
Debug.dprintf debug_refl "module map built@.";
let args = List.map (fun pv -> pv.pv_vs) rs.rs_cty.cty_args in
let rec reify_post = function
......
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