Commit 6b352161 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Correctly parse transformations arguments that are meta id arguments

parent eb9e7a58
...@@ -414,6 +414,7 @@ type naming_table = { ...@@ -414,6 +414,7 @@ type naming_table = {
coercion : Coercion.t; coercion : Coercion.t;
printer : Ident.ident_printer; printer : Ident.ident_printer;
aprinter : Ident.ident_printer; aprinter : Ident.ident_printer;
meta_id_args : Ident.ident Mstr.t;
} }
exception Bad_name_table of string exception Bad_name_table of string
......
...@@ -220,6 +220,7 @@ type naming_table = { ...@@ -220,6 +220,7 @@ type naming_table = {
coercion : Coercion.t; coercion : Coercion.t;
printer : Ident.ident_printer; printer : Ident.ident_printer;
aprinter : Ident.ident_printer; aprinter : Ident.ident_printer;
meta_id_args : Ident.ident Mstr.t;
} }
(** In order to interpret, that is type, string arguments as symbols or (** In order to interpret, that is type, string arguments as symbols or
terms, a transformation may need a [naming_table]. Typing arguments terms, a transformation may need a [naming_table]. Typing arguments
......
...@@ -37,10 +37,12 @@ val ns_find_prog_symbol : namespace -> string list -> prog_symbol ...@@ -37,10 +37,12 @@ val ns_find_prog_symbol : namespace -> string list -> prog_symbol
val ns_find_its : namespace -> string list -> itysymbol val ns_find_its : namespace -> string list -> itysymbol
val ns_find_pv : namespace -> string list -> pvsymbol val ns_find_pv : namespace -> string list -> pvsymbol
val ns_find_rs : namespace -> string list -> rsymbol
val ns_find_xs : namespace -> string list -> xsymbol val ns_find_xs : namespace -> string list -> xsymbol
val ns_find_ns : namespace -> string list -> namespace val ns_find_ns : namespace -> string list -> namespace
(* use this only on an export namespace, which cannot have overloaded symbols *)
val ns_find_rs : namespace -> string list -> rsymbol
type overload = type overload =
| FixedRes of ity (* t -> t -> ... -> T *) | FixedRes of ity (* t -> t -> ... -> T *)
| SameType (* t -> t -> ... -> t *) | SameType (* t -> t -> ... -> t *)
......
...@@ -53,7 +53,7 @@ let string_list_of_qualid q = ...@@ -53,7 +53,7 @@ let string_list_of_qualid q =
| Qident id -> id.id_str :: acc in | Qident id -> id.id_str :: acc in
sloq [] q sloq [] q
(* Type of sumbol queried *) (* Type of symbol queried *)
type symbol_kind = type symbol_kind =
| Prop | Prop
| Type | Type
...@@ -500,6 +500,7 @@ open Dexpr ...@@ -500,6 +500,7 @@ open Dexpr
let ty_of_pty tuc = ty_of_pty (get_namespace tuc) let ty_of_pty tuc = ty_of_pty (get_namespace tuc)
let get_namespace muc = List.hd muc.Pmodule.muc_import let get_namespace muc = List.hd muc.Pmodule.muc_import
let get_namespace_export muc = List.hd muc.Pmodule.muc_export
let dterm muc = let dterm muc =
let uc = muc.muc_theory in let uc = muc.muc_theory in
...@@ -510,7 +511,8 @@ let find_itysymbol muc q = find_itysymbol_ns (get_namespace muc) q ...@@ -510,7 +511,8 @@ let find_itysymbol muc q = find_itysymbol_ns (get_namespace muc) q
let find_prog_symbol muc q = find_prog_symbol_ns (get_namespace muc) q let find_prog_symbol muc q = find_prog_symbol_ns (get_namespace muc) q
let find_rsymbol muc q = let find_rsymbol muc q =
find_qualid ~ty:Prog (fun rs -> rs.rs_name) ns_find_rs (get_namespace muc) q let ns = get_namespace_export muc in
find_qualid ~ty:Prog (fun rs -> rs.rs_name) ns_find_rs ns q
let find_special muc test nm q = let find_special muc test nm q =
match find_prog_symbol muc q with match find_prog_symbol muc q with
......
...@@ -144,6 +144,17 @@ let add (d: decl) (tables: naming_table): naming_table = ...@@ -144,6 +144,17 @@ let add (d: decl) (tables: naming_table): naming_table =
let s = id_unique tables id in let s = id_unique tables id in
add_unsafe s (Pr pr) tables add_unsafe s (Pr pr) tables
(* Adds meta arguments of type ident to tables *)
let add_meta_id_args (al: meta_arg list) (tables: naming_table): naming_table =
List.fold_left
(fun t a ->
match a with
| MAident id ->
let s = id_unique tables id in
{ tables with meta_id_args = Mstr.add s id tables.meta_id_args }
| _ -> t)
tables al
(* Takes the set of meta defined in the tasks and build the coercions from it. (* Takes the set of meta defined in the tasks and build the coercions from it.
TODO we could have a set of coercions in the task ? Same problem for naming TODO we could have a set of coercions in the task ? Same problem for naming
table ? table ?
...@@ -173,6 +184,7 @@ let build_naming_tables task : naming_table = ...@@ -173,6 +184,7 @@ let build_naming_tables task : naming_table =
coercion = Coercion.empty; coercion = Coercion.empty;
printer = pr; printer = pr;
aprinter = apr; aprinter = apr;
meta_id_args = Mstr.empty;
} in } in
(* We want conflicting names to be named as follows: (* We want conflicting names to be named as follows:
names closer to the goal should be named with lowest names closer to the goal should be named with lowest
...@@ -182,7 +194,10 @@ let build_naming_tables task : naming_table = ...@@ -182,7 +194,10 @@ let build_naming_tables task : naming_table =
(* TODO:imported theories should be added in the namespace too *) (* TODO:imported theories should be added in the namespace too *)
let tables = Task.task_fold let tables = Task.task_fold
(fun t d -> (fun t d ->
match d.td_node with Decl d -> add d t | _ -> t) tables task match d.td_node with
| Decl d -> add d t
| Meta (_,al) -> add_meta_id_args al t
| _ -> t) tables task
in in
let crc_map = build_coercion_map km_meta in let crc_map = build_coercion_map km_meta in
{tables with coercion = crc_map} {tables with coercion = crc_map}
......
...@@ -442,9 +442,6 @@ let rec reify_term renv t rt = ...@@ -442,9 +442,6 @@ let rec reify_term renv t rt =
Pretty.print_ty (Opt.get t.t_ty) Pretty.print_ty (Opt.get t.t_ty)
Pretty.print_ty (Opt.get rt.t_ty); Pretty.print_ty (Opt.get rt.t_ty);
raise NoReification); 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 match t.t_node, rt.t_node with
| _, Tapp(interp, {t_node = Tvar vx}::vyl) | _, Tapp(interp, {t_node = Tvar vx}::vyl)
when List.mem vx renv.lv when List.mem vx renv.lv
...@@ -647,12 +644,14 @@ let reflection_by_function do_trans s env = Trans.store (fun task -> ...@@ -647,12 +644,14 @@ let reflection_by_function do_trans s env = Trans.store (fun task ->
let re_dot = Str.regexp_string "." in let re_dot = Str.regexp_string "." in
let qs = Str.split re_dot s in let qs = Str.split re_dot s in
let fname = List.hd (List.rev qs) in let fname = List.hd (List.rev qs) in
let es = "Symbol "^fname^" not found in reflection metas" in
let fid = Mstr.find_exn (Arg_error es) s nt.Trans.meta_id_args in
Debug.dprintf debug_refl "looking for symbol %s@." fname; Debug.dprintf debug_refl "looking for symbol %s@." fname;
let (pmod, rs) = let (pmod, rs) =
let fn acc = function let fn acc = function
| [ MAident id ] -> | [ MAident id ] ->
Debug.dprintf debug_refl "found symbol %s@." id.id_string; Debug.dprintf debug_refl "found symbol %s@." id.id_string;
if id.id_string = fname if id_equal id fid
then id :: acc then id :: acc
else acc else acc
| _ -> assert false in | _ -> assert false in
......
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