--- a/Admin/components/bundled Mon May 27 15:14:41 2013 +0200
+++ b/Admin/components/bundled Mon May 27 16:53:21 2013 +0200
@@ -1,3 +1,3 @@
#additional components to be bundled for release
-ProofGeneral-4.1
+ProofGeneral-4.2
--- a/Admin/components/components.sha1 Mon May 27 15:14:41 2013 +0200
+++ b/Admin/components/components.sha1 Mon May 27 16:53:21 2013 +0200
@@ -38,6 +38,7 @@
1812e9fa6d163f63edb93e37d1217640a166cf3e polyml-5.5.0.tar.gz
8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz
847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz
+8472221c876a430cde325841ce52893328302712 ProofGeneral-4.2.tar.gz
0885e1f1d8feaca78d2f204b6487e6eec6dfab4b scala-2.10.0.tar.gz
f7dc7a4e1aea46408fd6e44b8cfacb33af61afbc scala-2.10.1.tar.gz
b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon May 27 15:14:41 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon May 27 16:53:21 2013 +0200
@@ -406,10 +406,17 @@
[] => th
| pairs =>
let val thy = theory_of_thm th
- val (_, tenv) =
+ val cert = cterm_of thy
+ val certT = ctyp_of thy
+ val (tyenv, tenv) =
fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
- val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
- val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
+ fun mkT (v, (S, T)) = (certT (TVar (v, S)), certT T)
+ fun mk (v, (T, t)) =
+ let val T' = Envir.subst_type tyenv T
+ in (cert (Var (v, T')), cert t) end
+ val instsT = Vartab.fold (cons o mkT) tyenv []
+ val insts = Vartab.fold (cons o mk) tenv []
+ val th' = Thm.instantiate (instsT, insts) th
in th' end
handle THM _ => th;
--- a/src/Pure/Syntax/ast.ML Mon May 27 15:14:41 2013 +0200
+++ b/src/Pure/Syntax/ast.ML Mon May 27 16:53:21 2013 +0200
@@ -70,7 +70,7 @@
(* strip_positions *)
fun strip_positions (Appl ((t as Constant c) :: u :: (v as Variable x) :: asts)) =
- if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Term_Position.decode x)
+ if member (op =) Term_Position.markers c andalso is_some (Term_Position.decode x)
then mk_appl (strip_positions u) (map strip_positions asts)
else Appl (map strip_positions (t :: u :: v :: asts))
| strip_positions (Appl asts) = Appl (map strip_positions asts)
--- a/src/Pure/Syntax/syntax_phases.ML Mon May 27 15:14:41 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Mon May 27 16:53:21 2013 +0200
@@ -515,6 +515,34 @@
(* term_to_ast *)
+local
+
+fun mark_aprop tm =
+ let
+ fun aprop t = Syntax.const "_aprop" $ t;
+
+ fun is_prop Ts t =
+ fastype_of1 (Ts, t) = propT handle TERM _ => false;
+
+ fun is_term (Const ("Pure.term", _) $ _) = true
+ | is_term _ = false;
+
+ fun mark _ (t as Const _) = t
+ | mark Ts (t as Const ("_bound", _) $ u) = if is_prop Ts u then aprop t else t
+ | mark _ (t as Free (x, T)) = if T = propT then aprop (Syntax.free x) else t
+ | mark _ (t as Var (xi, T)) = if T = propT then aprop (Syntax.var xi) else t
+ | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t
+ | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t)
+ | mark Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
+ if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ mark Ts t1
+ else mark Ts t1 $ mark Ts t2
+ | mark Ts (t as t1 $ t2) =
+ (if is_Const (Term.head_of t) orelse not (is_prop Ts t) then I else aprop)
+ (mark Ts t1 $ mark Ts t2);
+ in mark [] tm end;
+
+in
+
fun term_to_ast idents is_syntax_const ctxt trf tm =
let
val show_types =
@@ -527,6 +555,25 @@
val {structs, fixes} = idents;
+ fun prune_typs (t_seen as (Const _, _)) = t_seen
+ | prune_typs (t as Free (x, ty), seen) =
+ if ty = dummyT then (t, seen)
+ else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
+ else (t, t :: seen)
+ | prune_typs (t as Var (xi, ty), seen) =
+ if ty = dummyT then (t, seen)
+ else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
+ else (t, t :: seen)
+ | prune_typs (t_seen as (Bound _, _)) = t_seen
+ | prune_typs (Abs (x, ty, t), seen) =
+ let val (t', seen') = prune_typs (t, seen);
+ in (Abs (x, ty, t'), seen') end
+ | prune_typs (t1 $ t2, seen) =
+ let
+ val (t1', seen') = prune_typs (t1, seen);
+ val (t2', seen'') = prune_typs (t2, seen');
+ in (t1' $ t2', seen'') end;
+
fun mark_atoms ((t as Const (c, _)) $ u) =
if member (op =) Pure_Thy.token_markers c
then t $ u else mark_atoms t $ mark_atoms u
@@ -548,25 +595,6 @@
else Syntax.const "_var" $ t
| mark_atoms a = a;
- fun prune_typs (t_seen as (Const _, _)) = t_seen
- | prune_typs (t as Free (x, ty), seen) =
- if ty = dummyT then (t, seen)
- else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
- else (t, t :: seen)
- | prune_typs (t as Var (xi, ty), seen) =
- if ty = dummyT then (t, seen)
- else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
- else (t, t :: seen)
- | prune_typs (t_seen as (Bound _, _)) = t_seen
- | prune_typs (Abs (x, ty, t), seen) =
- let val (t', seen') = prune_typs (t, seen);
- in (Abs (x, ty, t'), seen') end
- | prune_typs (t1 $ t2, seen) =
- let
- val (t1', seen') = prune_typs (t1, seen);
- val (t2', seen'') = prune_typs (t2, seen');
- in (t1' $ t2', seen'') end;
-
fun ast_of tm =
(case strip_comb tm of
(t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
@@ -598,12 +626,14 @@
else simple_ast_of ctxt t;
in
tm
- |> Syntax_Trans.prop_tr'
+ |> mark_aprop
|> show_types ? (#1 o prune_typs o rpair [])
|> mark_atoms
|> ast_of
end;
+end;
+
(** unparse **)
--- a/src/Pure/Syntax/syntax_trans.ML Mon May 27 15:14:41 2013 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML Mon May 27 16:53:21 2013 +0200
@@ -39,7 +39,6 @@
val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
- val prop_tr': term -> term
val variant_abs: string * typ * term -> string * term
val variant_abs': string * typ * term -> string * term
val dependent_tr': string * string -> term list -> term
@@ -378,37 +377,6 @@
| idtyp_ast_tr' _ _ = raise Match;
-(* meta propositions *)
-
-fun prop_tr' tm =
- let
- fun aprop t = Syntax.const "_aprop" $ t;
-
- fun is_prop Ts t =
- fastype_of1 (Ts, t) = propT handle TERM _ => false;
-
- fun is_term (Const ("Pure.term", _) $ _) = true
- | is_term _ = false;
-
- fun tr' _ (t as Const _) = t
- | tr' Ts (t as Const ("_bound", _) $ u) =
- if is_prop Ts u then aprop t else t
- | tr' _ (t as Free (x, T)) =
- if T = propT then aprop (Syntax.free x) else t
- | tr' _ (t as Var (xi, T)) =
- if T = propT then aprop (Syntax.var xi) else t
- | tr' Ts (t as Bound _) =
- if is_prop Ts t then aprop t else t
- | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
- | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
- if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
- else tr' Ts t1 $ tr' Ts t2
- | tr' Ts (t as t1 $ t2) =
- (if is_Const (Term.head_of t) orelse not (is_prop Ts t)
- then I else aprop) (tr' Ts t1 $ tr' Ts t2);
- in tr' [] tm end;
-
-
(* meta implication *)
fun impl_ast_tr' asts =
--- a/src/Pure/Syntax/term_position.ML Mon May 27 15:14:41 2013 +0200
+++ b/src/Pure/Syntax/term_position.ML Mon May 27 16:53:21 2013 +0200
@@ -14,6 +14,7 @@
val decode_positionS: sort -> Position.T list * sort
val is_position: term -> bool
val is_positionT: typ -> bool
+ val markers: string list
val strip_positions: term -> term
end;
@@ -58,8 +59,10 @@
val is_position = is_some o decode_position;
val is_positionT = is_some o decode_positionT;
+val markers = ["_constrain", "_constrainAbs", "_ofsort"];
+
fun strip_positions ((t as Const (c, _)) $ u $ v) =
- if (c = "_constrain" orelse c = "_constrainAbs" orelse c = "_ofsort") andalso is_position v
+ if member (op =) markers c andalso is_position v
then strip_positions u
else t $ strip_positions u $ strip_positions v
| strip_positions (t $ u) = strip_positions t $ strip_positions u
--- a/src/Pure/pattern.ML Mon May 27 15:14:41 2013 +0200
+++ b/src/Pure/pattern.ML Mon May 27 16:53:21 2013 +0200
@@ -242,8 +242,15 @@
and cases thy (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
- if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
- else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
+ if F = G then
+ let val env' = unify_types thy (Fty, Gty) env
+ in flexflex1(env',binders,F,Fty,ints_of' env' ss,ints_of' env' ts) end
+ else
+ let val env' =
+ unify_types thy
+ (Envir.body_type env (length ss) Fty,
+ Envir.body_type env (length ts) Gty) env
+ in flexflex2(env',binders,F,Fty,ints_of' env' ss,G,Gty,ints_of' env' ts) end
| ((Var(F,Fty),ss),_) => flexrigid thy (env,binders,F,Fty,ints_of' env ss,t)
| (_,(Var(F,Fty),ts)) => flexrigid thy (env,binders,F,Fty,ints_of' env ts,s)
| ((Const c,ss),(Const d,ts)) => rigidrigid thy (env,binders,c,d,ss,ts)
--- a/src/Pure/unify.ML Mon May 27 15:14:41 2013 +0200
+++ b/src/Pure/unify.ML Mon May 27 16:53:21 2013 +0200
@@ -186,6 +186,9 @@
fun unify_types thy TU env =
Pattern.unify_types thy TU env handle Pattern.Unif => raise CANTUNIFY;
+fun unify_types_of thy (rbinder, t, u) env =
+ unify_types thy (fastype env (rbinder, t), fastype env (rbinder, u)) env;
+
fun test_unify_types thy (T, U) env =
let
val str_of = Syntax.string_of_typ_global thy;
@@ -196,49 +199,44 @@
(*Is the term eta-convertible to a single variable with the given rbinder?
Examples: ?a ?f(B.0) ?g(B.1,B.0)
Result is var a for use in SIMPL. *)
-fun get_eta_var ([], _, Var vT) = vT
- | get_eta_var (_::rbinder, n, f $ Bound i) =
- if n = i then get_eta_var (rbinder, n + 1, f)
+fun get_eta_var [] n (Var vT) = (n, vT)
+ | get_eta_var (_ :: rbinder) n (f $ Bound i) =
+ if n = i then get_eta_var rbinder (n + 1) f
else raise ASSIGN
- | get_eta_var _ = raise ASSIGN;
+ | get_eta_var _ _ _ = raise ASSIGN;
(*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
If v occurs rigidly then nonunifiable.
If v occurs nonrigidly then must use full algorithm. *)
fun assignment thy (rbinder, t, u) env =
- let val vT as (v,T) = get_eta_var (rbinder, 0, t) in
+ let val (n, (v, T)) = get_eta_var rbinder 0 t in
(case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
NoOcc =>
- let val env = unify_types thy (Envir.body_type env ~1 T, fastype env (rbinder, u)) env
- in Envir.update (vT, Logic.rlist_abs (rbinder, u)) env end
+ let val env = unify_types thy (Envir.body_type env n T, fastype env (rbinder, u)) env
+ in Envir.update ((v, T), Logic.rlist_abs (rbinder, u)) env end
| Nonrigid => raise ASSIGN
| Rigid => raise CANTUNIFY)
end;
(*Extends an rbinder with a new disagreement pair, if both are abstractions.
- Tries to unify types of the bound variables!
Checks that binders have same length, since terms should be eta-normal;
if not, raises TERM, probably indicating type mismatch.
Uses variable a (unless the null string) to preserve user's naming.*)
fun new_dpair thy (rbinder, Abs (a, T, body1), Abs (b, U, body2)) env =
- let
- val env' = unify_types thy (T, U) env;
- val c = if a = "" then b else a;
- in new_dpair thy ((c,T) :: rbinder, body1, body2) env' end
+ let val c = if a = "" then b else a
+ in new_dpair thy ((c, T) :: rbinder, body1, body2) env end
| new_dpair _ (_, Abs _, _) _ = raise TERM ("new_dpair", [])
| new_dpair _ (_, _, Abs _) _ = raise TERM ("new_dpair", [])
| new_dpair _ (rbinder, t1, t2) env = ((rbinder, t1, t2), env);
-
fun head_norm_dpair thy (env, (rbinder, t, u)) : dpair * Envir.env =
new_dpair thy (rbinder,
eta_norm env (rbinder, Envir.head_norm env t),
eta_norm env (rbinder, Envir.head_norm env u)) env;
-
(*flexflex: the flex-flex pairs, flexrigid: the flex-rigid pairs
Does not perform assignments for flex-flex pairs:
may create nonrigid paths, which prevent other assignments.
@@ -247,7 +245,8 @@
*)
fun SIMPL0 thy dp0 (env,flexflex,flexrigid) : Envir.env * dpair list * dpair list =
let
- val (dp as (rbinder, t, u), env) = head_norm_dpair thy (env, dp0);
+ val (dp as (rbinder, t, u), env) =
+ head_norm_dpair thy (unify_types_of thy dp0 env, dp0);
fun SIMRANDS (f $ t, g $ u, env) =
SIMPL0 thy (rbinder, t, u) (SIMRANDS (f, g, env))
| SIMRANDS (t as _$_, _, _) =
@@ -257,11 +256,9 @@
| SIMRANDS (_, _, env) = (env, flexflex, flexrigid);
in
(case (head_of t, head_of u) of
- (Var (_, T), Var (_, U)) =>
- let
- val T' = Envir.body_type env ~1 T and U' = Envir.body_type env ~1 U;
- val env = unify_types thy (T', U') env;
- in (env, dp :: flexflex, flexrigid) end
+ (Var (v, T), Var (w, U)) =>
+ let val env' = if v = w then unify_types thy (T, U) env else env
+ in (env', dp :: flexflex, flexrigid) end
| (Var _, _) =>
((assignment thy (rbinder,t,u) env, flexflex, flexrigid)
handle ASSIGN => (env, flexflex, dp :: flexrigid))
@@ -415,11 +412,11 @@
(*At end of unification, do flex-flex assignments like ?a -> ?f(?b)
Attempts to update t with u, raising ASSIGN if impossible*)
fun ff_assign thy (env, rbinder, t, u) : Envir.env =
- let val vT as (v, T) = get_eta_var (rbinder, 0, t) in
+ let val (n, (v, T)) = get_eta_var rbinder 0 t in
if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
else
- let val env = unify_types thy (Envir.body_type env ~1 T, fastype env (rbinder, u)) env
- in Envir.vupdate (vT, Logic.rlist_abs (rbinder, u)) env end
+ let val env = unify_types thy (Envir.body_type env n T, fastype env (rbinder, u)) env
+ in Envir.vupdate ((v, T), Logic.rlist_abs (rbinder, u)) env end
end;