1635 (case Type.lookup (Envir.type_env env) v of |
1635 (case Type.lookup (Envir.type_env env) v of |
1636 NONE => T |
1636 NONE => T |
1637 | SOME T' => chaseT env T') |
1637 | SOME T' => chaseT env T') |
1638 | chaseT _ T = T; |
1638 | chaseT _ T = T; |
1639 |
1639 |
1640 fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) _ vTs |
1640 fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) _ vTs (t as Const (s, T)) = |
1641 (t as Const (s, T)) = if T = dummyT then |
1641 if T = dummyT then |
1642 (case Sign.const_type thy s of |
1642 (case Sign.const_type thy s of |
1643 NONE => error ("reconstruct_proof: No such constant: " ^ quote s) |
1643 NONE => error ("reconstruct_proof: No such constant: " ^ quote s) |
1644 | SOME T => |
1644 | SOME T => |
1645 let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T) |
1645 let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T) in |
1646 in (Const (s, T'), T', vTs, |
1646 (Const (s, T'), T', vTs, |
1647 Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}) |
1647 Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}) |
1648 end) |
1648 end) |
1649 else (t, T, vTs, env) |
1649 else (t, T, vTs, env) |
1650 | infer_type _ env _ vTs (t as Free (s, T)) = |
1650 | infer_type _ env _ vTs (t as Free (s, T)) = |
1651 if T = dummyT then (case Symtab.lookup vTs s of |
1651 if T = dummyT then |
|
1652 (case Symtab.lookup vTs s of |
1652 NONE => |
1653 NONE => |
1653 let val (T, env') = mk_tvar [] env |
1654 let val (T, env') = mk_tvar [] env |
1654 in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end |
1655 in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end |
1655 | SOME T => (Free (s, T), T, vTs, env)) |
1656 | SOME T => (Free (s, T), T, vTs, env)) |
1656 else (t, T, vTs, env) |
1657 else (t, T, vTs, env) |
1662 in (Abs (s, T', t'), T' --> U, vTs', env'') end |
1663 in (Abs (s, T', t'), T' --> U, vTs', env'') end |
1663 | infer_type thy env Ts vTs (t $ u) = |
1664 | infer_type thy env Ts vTs (t $ u) = |
1664 let |
1665 let |
1665 val (t', T, vTs1, env1) = infer_type thy env Ts vTs t; |
1666 val (t', T, vTs1, env1) = infer_type thy env Ts vTs t; |
1666 val (u', U, vTs2, env2) = infer_type thy env1 Ts vTs1 u; |
1667 val (u', U, vTs2, env2) = infer_type thy env1 Ts vTs1 u; |
1667 in (case chaseT env2 T of |
1668 in |
|
1669 (case chaseT env2 T of |
1668 Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U') |
1670 Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U') |
1669 | _ => |
1671 | _ => |
1670 let val (V, env3) = mk_tvar [] env2 |
1672 let val (V, env3) = mk_tvar [] env2 |
1671 in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end) |
1673 in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end) |
1672 end |
1674 end |