[isabelle-dev] find_theorems raises UnequalLengths exception

[Lawrence Paulson]

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
>> 
>>