[isabelle-dev] find_theorems raises UnequalLengths exception

[Tobias Nipkow]

The code is mine and I haven't looked at it for some 15 years. I agree
with Larry, there must be some undocumented precondition about the form
of the terms, eg that they are eta expanded or contracted. Presumably
the calling context used to ensure those preconditions (otherwise we
would would have seen the execption before) but does no longer. Larry's
fix seems fine: it replaces a low level exception by the proper
exception of that module but does not modify the unexceptional behaviour.

Tobias

Lawrence Paulson schrieb:
> This is not my code, and I'm not certain that I understand it, but I don't believe that there is a direct connection between my correction of the unification code and the exception. It is raised from the single occurrence of the ~~ operator in the code below.
> 
> fun match thy (po as (pat,obj)) envir =
> let
>   (* Pre: pat and obj have same type *)
>   fun mtch binders (pat,obj) (env as (iTs,itms)) =
>     case pat of
>       Abs(ns,Ts,ts) =>
>         (case obj of
>            Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (ts,tt) env
>          | _ => let val Tt = Envir.subst_type iTs Ts
>                 in mtch((ns,Tt)::binders) (ts,(incr obj)$Bound(0)) env end)
>     | _ => (case obj of
>               Abs(nt,Tt,tt) =>
>                 mtch((nt,Tt)::binders) ((incr pat)$Bound(0),tt) env
>             | _ => cases(binders,env,pat,obj))
> 
>   and cases(binders,env as (iTs,itms),pat,obj) =
>     let val (ph,pargs) = strip_comb pat
>         fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms)
>         fun rigrig2((a:string,Ta),(b,Tb),oargs) =
>               if a <> b then raise MATCH
>               else rigrig1(typ_match thy (Ta,Tb) iTs, oargs)
>     in case ph of
>          Var(ixn,T) =>
>            let val is = ints_of pargs
>            in case Envir.lookup' (itms, (ixn, T)) of
>                 NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj))
>               | SOME u => if obj aeconv (red u is []) then env
>                           else raise MATCH
>            end
>        | _ =>
>            let val (oh,oargs) = strip_comb obj
>            in case (ph,oh) of
>                 (Const c,Const d) => rigrig2(c,d,oargs)
>               | (Free f,Free g)   => rigrig2(f,g,oargs)
>               | (Bound i,Bound j) => if i<>j then raise MATCH
>                                      else rigrig1(iTs,oargs)
>               | (Abs _, _)        => raise Pattern
>               | (_, Abs _)        => raise Pattern
>               | _                 => raise MATCH
>            end
>     end;
> 
> And the use of this operator seems to embody an assumption that the number of arguments in the pattern necessarily equals the number of arguments in the object. Presumably type checking enforces this much of the time, but with eta contraction I could imagine it could fail. It obviously does fail, as the exception proves. I would be tempted to insert the line
> 
> 	handle UnequalLengths => raise MATCH
> 
> (With appropriate parentheses) immediately after the call to rigrig1(iTs,oargs).
> 
> Can anybody comment who is more familiar with this code?
> 
> Larry
> 
> On 18 Nov 2010, at 17:03, Brian Huffman wrote:
> 
>> On Thu, Nov 18, 2010 at 8:25 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>>> That is certainly my change, but I don't understand why preventing self-referential type instantiations should affect the find_theorems function. Can you get a full trace back from the exception?
>> Here's what I get from turning on the debugging flag in Proof General:
>>
>> Exception trace for exception - UnequalLengths
>> Library.~~(2)
>> Pattern.match(3)cases(5)rigrig1(2)
>> Pattern.match(3)cases(5)
>> Pattern.match(3)mtch(4)
>> Pattern.match(3)
>> Pattern.matches_subterm(3)msub(2)
>> Pattern.matches_subterm(3)msub(2)
>> Pattern.matches_subterm(3)
>> Find_Theorems.filter_pattern(2)check(3)
>> Find_Theorems.filter_pattern(2)check(1)
>> o(2)(1)
>> Find_Theorems.app_filters(1)app(3)
>> List.mapPartial(2)
>> List.mapPartial(2)
>> List.mapPartial(2)
>> List.mapPartial(2)
>> List.mapPartial(2)
>> List.mapPartial(2)
>> List.mapPartial(2)
>> List.mapPartial(2)
>> Find_Theorems.sorted_filter(2)
>> Find_Theorems.find_theorems(5)find_all(2)
>> Find_Theorems.find_theorems(5)find_all(1)
>> Find_Theorems.print_theorems(5)
>> Toplevel.apply_tr(3)(1)
>> Runtime.debugging(2)(1)
>> End of trace
>>
>> *** exception UnequalLengths raised
>> *** At command "find_theorems"
>>> Larry
>>>
>>> On 18 Nov 2010, at 16:03, Brian Huffman wrote:
>>>
>>>> Hello everyone,
>>>>
>>>> Recently I noticed that in HOLCF, whenever I do a theorem search for
>>>> theorems containing the constant "UU" (i.e. bottom), the search fails
>>>> with an UnequalLengths exception. I tracked the problem down to this
>>>> specific theorem from Fun_Cpo.thy: Before this point, find_theorems
>>>> "UU" succeeds, and afterward it causes an error.
>>>>
>>>> lemma app_strict: "UU x = UU"
>>>>
>>>> I found that I can also reproduce the problem directly in HOL:
>>>>
>>>> theory Scratch
>>>> imports Orderings
>>>> begin
>>>>
>>>> find_theorems "bot"
>>>>
>>>> lemma bot_apply: "bot x = bot"
>>>> by (simp only: bot_fun_eq)
>>>>
>>>> find_theorems "bot"
>>>>
>>>> *** exception UnequalLengths raised
>>>> *** At command "find_theorems"
>>>>
>>>> After doing "hg bisect", I traced the origin of the problem:
>>>>
>>>> http://isabelle.in.tum.de/repos/isabelle/rev/b654fa27fbc4
>>>>
>>>> Can anyone figure this out?
>>>>
>>>> - Brian
>>>> _______________________________________________
>>>> Isabelle-dev mailing list
>>>> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev