# HG changeset patch # User wenzelm # Date 1369666401 -7200 # Node ID 55efdc47ebd1ecd19503a6130d69d95c58e5bf7e # Parent 7fd0b5cfbb798dac47c5d48027f69b92c60f96e0# Parent 3b9c31867707eb2750bed056bf3e368181ee86ad merged diff -r 7fd0b5cfbb79 -r 55efdc47ebd1 Admin/components/bundled --- 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 diff -r 7fd0b5cfbb79 -r 55efdc47ebd1 Admin/components/components.sha1 --- 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 diff -r 7fd0b5cfbb79 -r 55efdc47ebd1 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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; diff -r 7fd0b5cfbb79 -r 55efdc47ebd1 src/Pure/Syntax/ast.ML --- 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) diff -r 7fd0b5cfbb79 -r 55efdc47ebd1 src/Pure/Syntax/syntax_phases.ML --- 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 **) diff -r 7fd0b5cfbb79 -r 55efdc47ebd1 src/Pure/Syntax/syntax_trans.ML --- 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 = diff -r 7fd0b5cfbb79 -r 55efdc47ebd1 src/Pure/Syntax/term_position.ML --- 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 diff -r 7fd0b5cfbb79 -r 55efdc47ebd1 src/Pure/pattern.ML --- 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) diff -r 7fd0b5cfbb79 -r 55efdc47ebd1 src/Pure/unify.ML --- 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;