Fixed bug in decompose.
authorberghofe
Thu Oct 04 00:53:27 2001 +0200 (2001-10-04)
changeset 11660780ffc4d4600
parent 11659 a68f930bafb2
child 11661 37cfa9aad9c0
Fixed bug in decompose.
src/Pure/Proof/reconstruct.ML
     1.1 --- a/src/Pure/Proof/reconstruct.ML	Wed Oct 03 21:03:05 2001 +0200
     1.2 +++ b/src/Pure/Proof/reconstruct.ML	Thu Oct 04 00:53:27 2001 +0200
     1.3 @@ -91,17 +91,21 @@
     1.4    let
     1.5      val Envir.Envir {asol, iTs, maxidx} = env;
     1.6      val (iTs', maxidx') = Type.unify (Sign.tsig_of sg) maxidx iTs (T, U)
     1.7 -  in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end;
     1.8 +  in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end
     1.9 +  handle Type.TUNIFY => error ("Non-unifiable types:\n" ^
    1.10 +    Sign.string_of_typ sg T ^ "\n\n" ^ Sign.string_of_typ sg U);
    1.11  
    1.12  fun decompose sg env Ts
    1.13 -    (Const ("all", _) $ Abs (_, T, t)) (Const ("all", _) $ Abs (_, U, u)) =
    1.14 -      decompose sg (unifyT sg env T U) (T::Ts) t u
    1.15 +    (Const ("all", _) $ t) (Const ("all", _) $ u) = decompose sg env Ts t u
    1.16    | decompose sg env Ts
    1.17      (Const ("==>", _) $ t1 $ t2) (Const ("==>", _) $ u1 $ u2) =
    1.18 -      apsnd (cons (mk_abs Ts t1, mk_abs Ts u1)) (decompose sg env Ts t2 u2)
    1.19 +      let val (env', cs) = decompose sg env Ts t1 u1
    1.20 +      in apsnd (curry op @ cs) (decompose sg env' Ts t2 u2) end
    1.21 +  | decompose sg env Ts (Abs (_, T, t)) (Abs (_, U, u)) =
    1.22 +      decompose sg (unifyT sg env T U) (T::Ts) t u
    1.23    | decompose sg env Ts t u = (env, [(mk_abs Ts t, mk_abs Ts u)]);
    1.24  
    1.25 -fun cantunify sg t u = error ("Cannot unify:\n" ^
    1.26 +fun cantunify sg t u = error ("Non-unifiable terms:\n" ^
    1.27    Sign.string_of_term sg t ^ "\n\n" ^ Sign.string_of_term sg u);
    1.28  
    1.29  fun make_constraints_cprf sg env ts cprf =
    1.30 @@ -237,12 +241,13 @@
    1.31    solution of constraints
    1.32  *********************************************************************************)
    1.33  
    1.34 -exception IMPOSS;
    1.35 -
    1.36  fun solve _ [] bigenv = bigenv
    1.37    | solve sg cs bigenv =
    1.38        let
    1.39 -        fun search env [] = raise IMPOSS
    1.40 +        fun search env [] = error ("Unsolvable constraints:\n" ^
    1.41 +              Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
    1.42 +                Sign.pretty_term sg (Logic.mk_flexpair (pairself
    1.43 +                  (Envir.norm_term bigenv) p))) cs)))
    1.44            | search env ((u, p as (t1, t2), vs)::ps) =
    1.45                if u then
    1.46                  let