Commit 61af0420 authored by Andrei Paskevich's avatar Andrei Paskevich

Merge branch 'find_program_symbols' into 'master'

Finding program symbols

See merge request !131
parents 4e212696 f01936d9
......@@ -35,6 +35,8 @@ Transformations
* `destruct` now destruct `not p` into `p -> false`. `destruct_rec` is
allowed to further destruct afterwards.
`destruct` can also destruct `true` and `false`.
* decision procedures used for reflection now must be declared explicitly using
`meta reflection val <function_name>` :x:
IDE
* display of counterexamples in the Task view has been improved
......
......@@ -654,6 +654,8 @@ let predicate eq0_int (x:int) = x = 0
clone export ringdecision.AssocAlgebraDecision with type r = int, type a = mat, val rzero = Int.zero, val rone = Int.one, val rplus = (+), val ropp = (-_), val rtimes = (*), val azero = mzero, val aone = id, val aplus = add, val aopp = opp, val atimes = mul, val asub = sub, val ($) = extp, goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc, goal A.Mul_distr_l, goal A.Mul_distr_r, goal asub_def, goal A.Inv_def_l, goal A.Inv_def_r,
axiom . (* FIXME: replace with "goal" and prove *)
meta reflection val norm_f
end
module MatrixTests
......
......@@ -328,7 +328,7 @@
<goal name="VC wmpn_add_n.12.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC wmpn_add_n.12.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.22"/></proof>
<proof prover="0"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="VC wmpn_add_n.12.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.17"/></proof>
......@@ -428,7 +428,7 @@
<goal name="VC wmpn_add.12.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC wmpn_add.12.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.23"/></proof>
<proof prover="0"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="VC wmpn_add.12.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.16"/></proof>
......
This diff is collapsed.
......@@ -988,6 +988,8 @@ use real.FromInt
clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.( * ) = ( *. ), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=int -> real, function C.interp=rinterp, exception C.Unknown = QError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=rzero, val C.cone=rone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=radd, val C.mul=rmul, val C.opp=ropp, val C.eq=req, val C.inv=rinv, goal .
meta reflection val decision
end
module LinearDecisionInt
......@@ -1110,6 +1112,8 @@ let int_decision (l: context') (g: equality') : bool
= let l',g' = m_ctx l g in
R.decision l' g'
meta reflection val int_decision
end
......@@ -1555,6 +1559,8 @@ let mp_decision (l: context') (g: equality') : bool
=
R.decision (m_ctx l) (m_eq g)
meta reflection val mp_decision
end
module EqPropMP
......@@ -1968,6 +1974,8 @@ let prop_ctx (l:context') (g:equality') : (context', equality')
= let l', g' = prop_ctx l g in
mp_decision l' g'
meta reflection val prop_mp_decision
end
module TestMP
......@@ -2048,6 +2056,9 @@ function interp (f:fmla) (b: int -> value) : bool =
let f (f:fmla) : bool
ensures { result -> forall b. interp f b }
= false
meta reflection val f
end
(*
module TestFmla
......
This diff is collapsed.
......@@ -496,7 +496,7 @@
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.44" steps="59"/></proof>
</goal>
<goal name="VC wmpn_sub.36" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="VC wmpn_sub.37" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
......@@ -505,7 +505,7 @@
<proof prover="5"><result status="valid" time="0.47" steps="82"/></proof>
</goal>
<goal name="VC wmpn_sub.39" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.12"/></proof>
<proof prover="2"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="VC wmpn_sub.40" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
......@@ -520,7 +520,7 @@
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.30" steps="78"/></proof>
</goal>
<goal name="VC wmpn_sub.44" expl="integer overflow" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.52" steps="96"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.34" steps="96"/></proof>
</goal>
<goal name="VC wmpn_sub.45" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
......@@ -544,7 +544,7 @@
<proof prover="2"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="VC wmpn_sub.52" expl="postcondition" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.48" steps="67"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.27" steps="67"/></proof>
</goal>
<goal name="VC wmpn_sub.53" expl="assertion" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.19" steps="54"/></proof>
......@@ -782,7 +782,7 @@
<goal name="VC wmpn_sub_in_place.15.0.0" expl="assertion" proved="true">
<transf name="reflection_f" proved="true" arg1="mp_decision">
<goal name="VC wmpn_sub_in_place.15.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="4.32"/></proof>
<proof prover="0"><result status="valid" time="3.70"/></proof>
</goal>
<goal name="VC wmpn_sub_in_place.15.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.30"/></proof>
......@@ -861,7 +861,7 @@
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="0.05" steps="52"/></proof>
</goal>
<goal name="VC wmpn_sub_in_place.35" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.61"/></proof>
<proof prover="0"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="VC wmpn_sub_in_place.36" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
......@@ -1083,10 +1083,10 @@
<proof prover="3"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC wmpn_decr.20" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
<proof prover="2"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="VC wmpn_decr.21" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="0.53" steps="55"/></proof>
<proof prover="5"><result status="valid" time="0.86" steps="55"/></proof>
</goal>
<goal name="VC wmpn_decr.22" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.07"/></proof>
......@@ -1163,7 +1163,7 @@
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_decr.36" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.60"/></proof>
<proof prover="0"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="VC wmpn_decr.37" expl="loop invariant preservation" proved="true">
<proof prover="2" timelimit="5"><result status="valid" time="0.06"/></proof>
......@@ -1463,7 +1463,7 @@
<proof prover="2"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC wmpn_sub_1_in_place.15" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.76"/></proof>
<proof prover="2"><result status="valid" time="0.99"/></proof>
</goal>
<goal name="VC wmpn_sub_1_in_place.16" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
......@@ -1475,10 +1475,10 @@
<proof prover="2"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="VC wmpn_sub_1_in_place.19" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.41"/></proof>
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="VC wmpn_sub_1_in_place.20" expl="assertion" proved="true">
<proof prover="5"><result status="valid" time="1.10" steps="52"/></proof>
<proof prover="5"><result status="valid" time="0.73" steps="52"/></proof>
</goal>
<goal name="VC wmpn_sub_1_in_place.21" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
......@@ -1505,7 +1505,7 @@
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC wmpn_sub_1_in_place.29" expl="assertion" proved="true">
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="1.22" steps="66"/></proof>
<proof prover="5" timelimit="5" memlimit="2000"><result status="valid" time="1.49" steps="66"/></proof>
</goal>
<goal name="VC wmpn_sub_1_in_place.30" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.10"/></proof>
......
......@@ -33,7 +33,7 @@ module type Printer = sig
val tprinter : ident_printer (* type symbols *)
val aprinter : ident_printer (* type variables *)
val sprinter : ident_printer (* variables and functions *)
val pprinter : ident_printer (* propoition names *)
val pprinter : ident_printer (* proposition names *)
val forget_all : unit -> unit (* flush id_unique *)
val forget_tvs : unit -> unit (* flush id_unique for type vars *)
......@@ -556,6 +556,7 @@ let print_meta_arg_type fmt = function
| MTprsymbol -> fprintf fmt "[proposition]"
| MTstring -> fprintf fmt "[string]"
| MTint -> fprintf fmt "[integer]"
| MTid -> fprintf fmt "[identifier]"
let print_meta_arg fmt = function
| MAty ty -> fprintf fmt "type %a" print_ty ty; forget_tvs ()
......@@ -564,6 +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
| MAid 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
......
......@@ -83,6 +83,7 @@ type meta_arg_type =
| MTprsymbol
| MTstring
| MTint
| MTid
type meta_arg =
| MAty of ty
......@@ -91,6 +92,7 @@ type meta_arg =
| MApr of prsymbol
| MAstr of string
| MAint of int
| MAid of ident
type meta = {
meta_name : string;
......@@ -235,6 +237,7 @@ module Hstdecl = Hashcons.Make (struct
| MApr pr -> pr_hash pr
| MAstr s -> Hashtbl.hash s
| MAint i -> Hashtbl.hash i
| MAid i -> Ident.id_hash i
let hs_smap sm h =
Mts.fold hs_cl_ty sm.sm_ty
......@@ -409,8 +412,9 @@ let add_tdecl uc td = match td.td_node with
(** Declarations *)
let store_path, store_theory, restore_path =
let store_path, store_theory, restore_path, restore_theory =
let id_to_path = Wid.create 17 in
let id_to_th = Wid.create 17 in
let store_path uc path id =
(* this symbol already belongs to some theory *)
if Wid.mem id_to_path id then () else
......@@ -420,10 +424,15 @@ let store_path, store_theory, restore_path =
let store_theory th =
let id = th.th_name in
(* this symbol is already a theory *)
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_th id th) th.th_local;
Wid.set id_to_th id th;
end
in
let restore_path id = Wid.find id_to_path id in
store_path, store_theory, restore_path
let restore_theory id = Wid.find id_to_th id in
store_path, store_theory, restore_path, restore_theory
let close_theory uc =
let th = close_theory uc in
......@@ -862,6 +871,7 @@ let get_meta_arg_type = function
| MApr _ -> MTprsymbol
| MAstr _ -> MTstring
| MAint _ -> MTint
| MAid _ -> MTid
let create_meta m al =
let get_meta_arg at a =
......@@ -960,6 +970,7 @@ let print_meta_arg_type fmt = function
| MTprsymbol -> fprintf fmt "proposition"
| MTstring -> fprintf fmt "string"
| MTint -> fprintf fmt "int"
| MTid -> fprintf fmt "identifier"
let () = Exn_printer.register
begin fun fmt exn -> match exn with
......
......@@ -43,6 +43,7 @@ type meta_arg_type =
| MTprsymbol
| MTstring
| MTint
| MTid
type meta_arg =
| MAty of ty
......@@ -51,6 +52,7 @@ type meta_arg =
| MApr of prsymbol
| MAstr of string
| MAint of int
| MAid of ident
type meta = private {
meta_name : string;
......@@ -160,6 +162,8 @@ val restore_path : ident -> string list * string * string list
If [id] is a theory name, the third component is an empty list.
Raises [Not_found] if the ident was never declared in/as a theory. *)
val restore_theory : ident -> theory
(** {2 Declaration constructors} *)
val create_decl : decl -> tdecl
......
......@@ -414,6 +414,7 @@ type naming_table = {
coercion : Coercion.t;
printer : Ident.ident_printer;
aprinter : Ident.ident_printer;
meta_id_args : Ident.ident Mstr.t;
}
exception Bad_name_table of string
......
......@@ -220,6 +220,7 @@ type naming_table = {
coercion : Coercion.t;
printer : 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
terms, a transformation may need a [naming_table]. Typing arguments
......
......@@ -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
......
......@@ -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_pv : namespace -> string list -> pvsymbol
val ns_find_rs : namespace -> string list -> rsymbol
val ns_find_xs : namespace -> string list -> xsymbol
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 =
| FixedRes of ity (* t -> t -> ... -> T *)
| SameType (* t -> t -> ... -> t *)
......@@ -113,6 +115,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 *)
......
......@@ -388,6 +388,7 @@ meta_arg:
| AXIOM qualid { Max $2 }
| LEMMA qualid { Mlm $2 }
| GOAL qualid { Mgl $2 }
| VAL qualid { Mval $2 }
| STRING { Mstr $1 }
| INTEGER { Mint (Number.to_small_integer $1) }
......
......@@ -223,6 +223,7 @@ type metarg =
| Max of qualid
| Mlm of qualid
| Mgl of qualid
| Mval of qualid
| Mstr of string
| Mint of int
......
......@@ -53,7 +53,7 @@ let string_list_of_qualid q =
| Qident id -> id.id_str :: acc in
sloq [] q
(* Type of sumbol queried *)
(* Type of symbol queried *)
type symbol_kind =
| Prop
| Type
......@@ -500,6 +500,7 @@ open Dexpr
let ty_of_pty tuc = ty_of_pty (get_namespace tuc)
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 uc = muc.muc_theory in
......@@ -509,6 +510,10 @@ let find_xsymbol muc q = find_xsymbol_ns (get_namespace muc) q
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_rsymbol 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 =
match find_prog_symbol muc q with
| RS s when test s -> s
......@@ -1478,6 +1483,7 @@ let add_decl muc env file d =
| Ptree.Max q -> MApr (find_prop_of_kind Paxiom tuc q)
| Ptree.Mlm q -> MApr (find_prop_of_kind Plemma tuc q)
| Ptree.Mgl q -> MApr (find_prop_of_kind Pgoal tuc q)
| Ptree.Mval q -> MAid (find_rsymbol muc q).rs_name
| Ptree.Mstr s -> MAstr s
| Ptree.Mint i -> MAint i in
add_meta muc (lookup_meta id.id_str) (List.map convert al)
......
......@@ -370,6 +370,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
| MAid id -> fprintf fmt "%s" (id_unique iprinter id)
let print_qt fmt th =
if th.th_path = [] then print_th fmt th else
......
......@@ -629,6 +629,7 @@ module Checksum = struct
| Theory.MTprsymbol -> char b 'p'
| Theory.MTstring -> char b 's'
| Theory.MTint -> char b 'i'
| Theory.MTid -> char b 'd'
let meta b m =
string b m.Theory.meta_name;
......@@ -642,6 +643,7 @@ module Checksum = struct
| Theory.MApr pr -> char b 'p'; ident b pr.Decl.pr_name
| Theory.MAstr s -> char b 's'; string b s
| Theory.MAint i -> char b 'i'; int b i
| Theory.MAid i -> char b 'd'; ident b i
let tdecl b d = match d.Theory.td_node with
| Theory.Decl d -> decl b d
......
......@@ -144,6 +144,17 @@ let add (d: decl) (tables: naming_table): naming_table =
let s = id_unique tables id in
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
| MAid 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.
TODO we could have a set of coercions in the task ? Same problem for naming
table ?
......@@ -173,6 +184,7 @@ let build_naming_tables task : naming_table =
coercion = Coercion.empty;
printer = pr;
aprinter = apr;
meta_id_args = Mstr.empty;
} in
(* We want conflicting names to be named as follows:
names closer to the goal should be named with lowest
......@@ -182,7 +194,10 @@ let build_naming_tables task : naming_table =
(* TODO:imported theories should be added in the namespace too *)
let tables = Task.task_fold
(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
let crc_map = build_coercion_map km_meta in
{tables with coercion = crc_map}
......
......@@ -158,7 +158,9 @@ let fold tenv taskpre task =
| MAls ls -> MAls (conv_ls tenv ud ls)
| MApr _ -> raise Exit
| MAstr _ as s -> s
| MAint _ as i -> i in
| MAint _ as i -> i
| MAid _ as i -> i
in
let arg = List.map map ml in
add_meta (decl_ud ud task) meta arg
with
......
......@@ -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.MTid ]
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 @."
......@@ -621,6 +628,8 @@ open Expr
open Ity
open Wstdlib
open Mlinterp
open Theory
open Pmodule
exception ReductionFail of reify_env
......@@ -632,21 +641,32 @@ 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
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;
let (pmod, rs) =
let fn acc = function
| [ MAid id ] ->
Debug.dprintf debug_refl "found symbol %s@." id.id_string;
if id_equal id fid
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 +678,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