Email Gateway (Aug 18 2022 at 16:14): Email Gateway (Aug 18 2022 at 16:14):From: Michael Chan <mchan@inf.ed.ac.uk>
Hello all,
I'm having a problem with looking up the instantiation to a variable in
a matcher with Envir.lookup. The particular matcher is:
ML{* fun rtac' rl i j st = (snd o Seq.chop j) (rtac rl i st) *}
schematic_lemma
fixes g :: "nat => nat"
shows "((?f :: (?'a => ?'b) => ?'c) ?s = ?v) = (g a = x) & Q ?f ?s ?v"
apply rule
apply(tactic {* rtac' refl 1 1712 *})
goal (1 subgoal):
1. Q (%a::?'a => nat. a (?f9 a)) (%b::?'a. g a) x
variables:
a, x :: nat
g :: nat => nat
?f9 :: (?'a => nat) => ?'a
Q ::
((?'a => nat) => nat) => (?'a => nat) => nat => bool
type variables:
?'a :: type
If I lookup the instantiation to the variable ?s in this particular
matcher, which here has the type ?'a => nat, I run into an infinite
recursion. The infinite recursion seems to be caused by an infinite
chasing of type variable assignment at Type.devar:
(*chase variable assignments; if devar returns a type var then it must
be unassigned*)
fun devar tye (T as TVar v) =
(case lookup tye v of
SOME U => devar tye U
| NONE => T)
| devar _ T = T;
Put simply, there's no variable assignment for it to be chased.
In the implementation, Envir.lookup indirectly invokes Type.equal_type,
which checks over each type variable -- in this case, that's ?'a and
?'b. ?'b is fine, and only ?'a is problematic. Now let's look at the tye:
val tye =
Branch2
(Branch2
(Empty, (("'a", 0), (["HOL.type"], "?'a")),
Empty),
(("'b", 0), (["HOL.type"], "RealDef.real")),
Branch2
(Empty,
(("'a", 1), (["HOL.type"], "RealDef.real")),
Empty))
: Type.tyenv
If we call devar tye on (?'a, 0), we'll run into an infinite recursion
because lookup tye (TVar ("'a", 0), ["HOL.type"])) also gives (TVar
("'a", 0), ["HOL.type"])).
Why isn't the variable chasing procedure given a maximum depth?
Any help will be appreciated.
Michael
Email Gateway (Aug 18 2022 at 16:14):From: Alexander Krauss <krauss@in.tum.de>
Hi Michael,
I'm having a problem with looking up the instantiation to a variable in
a matcher with Envir.lookup.
I just looked at the code in envir.ML again, and there is a function
lookup', preceded by the following comment:
(* When dealing with environments produced by matching instead *)
(* of unification, there is no need to chase assigned TVars. *)
(* In this case, we can simply ignore the type substitution *)
(* and use = instead of eq_type. *)
Could this be the source of your problem? Since your problematic
substitution is generated by Unify.matchers (which wasn't clear from you
question), have you tried lookup' instead of lookup?
Larry can maybe explain the details behind this...
Alex
Email Gateway (Aug 18 2022 at 16:14):From: Michael Chan <mchan@inf.ed.ac.uk>
Could this be the source of your problem? Since your problematic
substitution is generated by Unify.matchers (which wasn't clear from you
question), have you tried lookup' instead of lookup?
I shall share my finding here as well:
An exception TYPE will be raised: Variable "?stuff" has two distinct
types. I think the problem there is that lookup' checks the type
variables using op = instead, which would match ?'a => ?'b with the
resulting type. I suspect lookup' can't handle schematic types. It'd
fail in cases in which Envir.lookup succeeds, e.g.:
consts
g :: "'a => 'b"
a :: real
v :: real
ML {*
val trm1 = @{term_pat "(?f'::(?'a=>?'b)=>?'c) ?stuff = ?v"};
val (_ $ (_ $ var) $ _) = trm1;
val mtch_seq = let
val init = Envir.empty 0
val trm2 = @{term "g a = v"}
in
Unify.matchers @{theory} [(trm1,trm2)]
end;
val SOME (mtch,_) = nthseq 1711 mtch_seq;
val tenv = Envir.term_env mtch;
val p = Term.dest_Var var;
val inst = Envir.lookup' (tenv, p);
*}
Larry can maybe explain the details behind this...
That'd be great!
Thanks
Michael
Alex
Last updated: Apr 19 2024 at 20:15 UTC