merged
authorwenzelm
Mon May 27 16:53:21 2013 +0200 (2013-05-27)
changeset 5218055efdc47ebd1
parent 52174 7fd0b5cfbb79
parent 52179 3b9c31867707
child 52181 59e5dd7b8f9a
merged
     1.1 --- a/Admin/components/bundled	Mon May 27 15:14:41 2013 +0200
     1.2 +++ b/Admin/components/bundled	Mon May 27 16:53:21 2013 +0200
     1.3 @@ -1,3 +1,3 @@
     1.4  #additional components to be bundled for release
     1.5 -ProofGeneral-4.1
     1.6 +ProofGeneral-4.2
     1.7  
     2.1 --- a/Admin/components/components.sha1	Mon May 27 15:14:41 2013 +0200
     2.2 +++ b/Admin/components/components.sha1	Mon May 27 16:53:21 2013 +0200
     2.3 @@ -38,6 +38,7 @@
     2.4  1812e9fa6d163f63edb93e37d1217640a166cf3e  polyml-5.5.0.tar.gz
     2.5  8ee375cfc38972f080dbc78f07b68dac03efe968  ProofGeneral-3.7.1.1.tar.gz
     2.6  847b52c0676b5eb0fbf0476f64fc08c2d72afd0c  ProofGeneral-4.1.tar.gz
     2.7 +8472221c876a430cde325841ce52893328302712  ProofGeneral-4.2.tar.gz
     2.8  0885e1f1d8feaca78d2f204b6487e6eec6dfab4b  scala-2.10.0.tar.gz
     2.9  f7dc7a4e1aea46408fd6e44b8cfacb33af61afbc  scala-2.10.1.tar.gz
    2.10  b447017e81600cc5e30dd61b5d4962f6da01aa80  scala-2.8.1.final.tar.gz
     3.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon May 27 15:14:41 2013 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon May 27 16:53:21 2013 +0200
     3.3 @@ -406,10 +406,17 @@
     3.4        [] => th
     3.5      | pairs =>
     3.6          let val thy = theory_of_thm th
     3.7 -            val (_, tenv) =
     3.8 +            val cert = cterm_of thy
     3.9 +            val certT = ctyp_of thy
    3.10 +            val (tyenv, tenv) =
    3.11                fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
    3.12 -            val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
    3.13 -            val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
    3.14 +            fun mkT (v, (S, T)) = (certT (TVar (v, S)), certT T)
    3.15 +            fun mk (v, (T, t)) =
    3.16 +              let val T' = Envir.subst_type tyenv T
    3.17 +              in (cert (Var (v, T')), cert t) end
    3.18 +            val instsT = Vartab.fold (cons o mkT) tyenv []
    3.19 +            val insts = Vartab.fold (cons o mk) tenv []
    3.20 +            val th' = Thm.instantiate (instsT, insts) th
    3.21          in  th'  end
    3.22          handle THM _ => th;
    3.23  
     4.1 --- a/src/Pure/Syntax/ast.ML	Mon May 27 15:14:41 2013 +0200
     4.2 +++ b/src/Pure/Syntax/ast.ML	Mon May 27 16:53:21 2013 +0200
     4.3 @@ -70,7 +70,7 @@
     4.4  (* strip_positions *)
     4.5  
     4.6  fun strip_positions (Appl ((t as Constant c) :: u :: (v as Variable x) :: asts)) =
     4.7 -      if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Term_Position.decode x)
     4.8 +      if member (op =) Term_Position.markers c andalso is_some (Term_Position.decode x)
     4.9        then mk_appl (strip_positions u) (map strip_positions asts)
    4.10        else Appl (map strip_positions (t :: u :: v :: asts))
    4.11    | strip_positions (Appl asts) = Appl (map strip_positions asts)
     5.1 --- a/src/Pure/Syntax/syntax_phases.ML	Mon May 27 15:14:41 2013 +0200
     5.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Mon May 27 16:53:21 2013 +0200
     5.3 @@ -515,6 +515,34 @@
     5.4  
     5.5  (* term_to_ast *)
     5.6  
     5.7 +local
     5.8 +
     5.9 +fun mark_aprop tm =
    5.10 +  let
    5.11 +    fun aprop t = Syntax.const "_aprop" $ t;
    5.12 +
    5.13 +    fun is_prop Ts t =
    5.14 +      fastype_of1 (Ts, t) = propT handle TERM _ => false;
    5.15 +
    5.16 +    fun is_term (Const ("Pure.term", _) $ _) = true
    5.17 +      | is_term _ = false;
    5.18 +
    5.19 +    fun mark _ (t as Const _) = t
    5.20 +      | mark Ts (t as Const ("_bound", _) $ u) = if is_prop Ts u then aprop t else t
    5.21 +      | mark _ (t as Free (x, T)) = if T = propT then aprop (Syntax.free x) else t
    5.22 +      | mark _ (t as Var (xi, T)) = if T = propT then aprop (Syntax.var xi) else t
    5.23 +      | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t
    5.24 +      | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t)
    5.25 +      | mark Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
    5.26 +          if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ mark Ts t1
    5.27 +          else mark Ts t1 $ mark Ts t2
    5.28 +      | mark Ts (t as t1 $ t2) =
    5.29 +          (if is_Const (Term.head_of t) orelse not (is_prop Ts t) then I else aprop)
    5.30 +            (mark Ts t1 $ mark Ts t2);
    5.31 +  in mark [] tm end;
    5.32 +
    5.33 +in
    5.34 +
    5.35  fun term_to_ast idents is_syntax_const ctxt trf tm =
    5.36    let
    5.37      val show_types =
    5.38 @@ -527,6 +555,25 @@
    5.39  
    5.40      val {structs, fixes} = idents;
    5.41  
    5.42 +    fun prune_typs (t_seen as (Const _, _)) = t_seen
    5.43 +      | prune_typs (t as Free (x, ty), seen) =
    5.44 +          if ty = dummyT then (t, seen)
    5.45 +          else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
    5.46 +          else (t, t :: seen)
    5.47 +      | prune_typs (t as Var (xi, ty), seen) =
    5.48 +          if ty = dummyT then (t, seen)
    5.49 +          else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
    5.50 +          else (t, t :: seen)
    5.51 +      | prune_typs (t_seen as (Bound _, _)) = t_seen
    5.52 +      | prune_typs (Abs (x, ty, t), seen) =
    5.53 +          let val (t', seen') = prune_typs (t, seen);
    5.54 +          in (Abs (x, ty, t'), seen') end
    5.55 +      | prune_typs (t1 $ t2, seen) =
    5.56 +          let
    5.57 +            val (t1', seen') = prune_typs (t1, seen);
    5.58 +            val (t2', seen'') = prune_typs (t2, seen');
    5.59 +          in (t1' $ t2', seen'') end;
    5.60 +
    5.61      fun mark_atoms ((t as Const (c, _)) $ u) =
    5.62            if member (op =) Pure_Thy.token_markers c
    5.63            then t $ u else mark_atoms t $ mark_atoms u
    5.64 @@ -548,25 +595,6 @@
    5.65            else Syntax.const "_var" $ t
    5.66        | mark_atoms a = a;
    5.67  
    5.68 -    fun prune_typs (t_seen as (Const _, _)) = t_seen
    5.69 -      | prune_typs (t as Free (x, ty), seen) =
    5.70 -          if ty = dummyT then (t, seen)
    5.71 -          else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
    5.72 -          else (t, t :: seen)
    5.73 -      | prune_typs (t as Var (xi, ty), seen) =
    5.74 -          if ty = dummyT then (t, seen)
    5.75 -          else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
    5.76 -          else (t, t :: seen)
    5.77 -      | prune_typs (t_seen as (Bound _, _)) = t_seen
    5.78 -      | prune_typs (Abs (x, ty, t), seen) =
    5.79 -          let val (t', seen') = prune_typs (t, seen);
    5.80 -          in (Abs (x, ty, t'), seen') end
    5.81 -      | prune_typs (t1 $ t2, seen) =
    5.82 -          let
    5.83 -            val (t1', seen') = prune_typs (t1, seen);
    5.84 -            val (t2', seen'') = prune_typs (t2, seen');
    5.85 -          in (t1' $ t2', seen'') end;
    5.86 -
    5.87      fun ast_of tm =
    5.88        (case strip_comb tm of
    5.89          (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
    5.90 @@ -598,12 +626,14 @@
    5.91        else simple_ast_of ctxt t;
    5.92    in
    5.93      tm
    5.94 -    |> Syntax_Trans.prop_tr'
    5.95 +    |> mark_aprop
    5.96      |> show_types ? (#1 o prune_typs o rpair [])
    5.97      |> mark_atoms
    5.98      |> ast_of
    5.99    end;
   5.100  
   5.101 +end;
   5.102 +
   5.103  
   5.104  
   5.105  (** unparse **)
     6.1 --- a/src/Pure/Syntax/syntax_trans.ML	Mon May 27 15:14:41 2013 +0200
     6.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Mon May 27 16:53:21 2013 +0200
     6.3 @@ -39,7 +39,6 @@
     6.4    val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
     6.5    val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
     6.6    val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
     6.7 -  val prop_tr': term -> term
     6.8    val variant_abs: string * typ * term -> string * term
     6.9    val variant_abs': string * typ * term -> string * term
    6.10    val dependent_tr': string * string -> term list -> term
    6.11 @@ -378,37 +377,6 @@
    6.12    | idtyp_ast_tr' _ _ = raise Match;
    6.13  
    6.14  
    6.15 -(* meta propositions *)
    6.16 -
    6.17 -fun prop_tr' tm =
    6.18 -  let
    6.19 -    fun aprop t = Syntax.const "_aprop" $ t;
    6.20 -
    6.21 -    fun is_prop Ts t =
    6.22 -      fastype_of1 (Ts, t) = propT handle TERM _ => false;
    6.23 -
    6.24 -    fun is_term (Const ("Pure.term", _) $ _) = true
    6.25 -      | is_term _ = false;
    6.26 -
    6.27 -    fun tr' _ (t as Const _) = t
    6.28 -      | tr' Ts (t as Const ("_bound", _) $ u) =
    6.29 -          if is_prop Ts u then aprop t else t
    6.30 -      | tr' _ (t as Free (x, T)) =
    6.31 -          if T = propT then aprop (Syntax.free x) else t
    6.32 -      | tr' _ (t as Var (xi, T)) =
    6.33 -          if T = propT then aprop (Syntax.var xi) else t
    6.34 -      | tr' Ts (t as Bound _) =
    6.35 -          if is_prop Ts t then aprop t else t
    6.36 -      | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
    6.37 -      | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
    6.38 -          if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
    6.39 -          else tr' Ts t1 $ tr' Ts t2
    6.40 -      | tr' Ts (t as t1 $ t2) =
    6.41 -          (if is_Const (Term.head_of t) orelse not (is_prop Ts t)
    6.42 -            then I else aprop) (tr' Ts t1 $ tr' Ts t2);
    6.43 -  in tr' [] tm end;
    6.44 -
    6.45 -
    6.46  (* meta implication *)
    6.47  
    6.48  fun impl_ast_tr' asts =
     7.1 --- a/src/Pure/Syntax/term_position.ML	Mon May 27 15:14:41 2013 +0200
     7.2 +++ b/src/Pure/Syntax/term_position.ML	Mon May 27 16:53:21 2013 +0200
     7.3 @@ -14,6 +14,7 @@
     7.4    val decode_positionS: sort -> Position.T list * sort
     7.5    val is_position: term -> bool
     7.6    val is_positionT: typ -> bool
     7.7 +  val markers: string list
     7.8    val strip_positions: term -> term
     7.9  end;
    7.10  
    7.11 @@ -58,8 +59,10 @@
    7.12  val is_position = is_some o decode_position;
    7.13  val is_positionT = is_some o decode_positionT;
    7.14  
    7.15 +val markers = ["_constrain", "_constrainAbs", "_ofsort"];
    7.16 +
    7.17  fun strip_positions ((t as Const (c, _)) $ u $ v) =
    7.18 -      if (c = "_constrain" orelse c = "_constrainAbs" orelse c = "_ofsort") andalso is_position v
    7.19 +      if member (op =) markers c andalso is_position v
    7.20        then strip_positions u
    7.21        else t $ strip_positions u $ strip_positions v
    7.22    | strip_positions (t $ u) = strip_positions t $ strip_positions u
     8.1 --- a/src/Pure/pattern.ML	Mon May 27 15:14:41 2013 +0200
     8.2 +++ b/src/Pure/pattern.ML	Mon May 27 16:53:21 2013 +0200
     8.3 @@ -242,8 +242,15 @@
     8.4  
     8.5  and cases thy (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
     8.6         ((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
     8.7 -         if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
     8.8 -                  else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
     8.9 +          if F = G then
    8.10 +            let val env' = unify_types thy (Fty, Gty) env
    8.11 +            in flexflex1(env',binders,F,Fty,ints_of' env' ss,ints_of' env' ts) end
    8.12 +          else
    8.13 +            let val env' =
    8.14 +              unify_types thy
    8.15 +               (Envir.body_type env (length ss) Fty,
    8.16 +                Envir.body_type env (length ts) Gty) env
    8.17 +            in flexflex2(env',binders,F,Fty,ints_of' env' ss,G,Gty,ints_of' env' ts) end
    8.18        | ((Var(F,Fty),ss),_)           => flexrigid thy (env,binders,F,Fty,ints_of' env ss,t)
    8.19        | (_,(Var(F,Fty),ts))           => flexrigid thy (env,binders,F,Fty,ints_of' env ts,s)
    8.20        | ((Const c,ss),(Const d,ts))   => rigidrigid thy (env,binders,c,d,ss,ts)
     9.1 --- a/src/Pure/unify.ML	Mon May 27 15:14:41 2013 +0200
     9.2 +++ b/src/Pure/unify.ML	Mon May 27 16:53:21 2013 +0200
     9.3 @@ -186,6 +186,9 @@
     9.4  fun unify_types thy TU env =
     9.5    Pattern.unify_types thy TU env handle Pattern.Unif => raise CANTUNIFY;
     9.6  
     9.7 +fun unify_types_of thy (rbinder, t, u) env =
     9.8 +  unify_types thy (fastype env (rbinder, t), fastype env (rbinder, u)) env;
     9.9 +
    9.10  fun test_unify_types thy (T, U) env =
    9.11    let
    9.12      val str_of = Syntax.string_of_typ_global thy;
    9.13 @@ -196,49 +199,44 @@
    9.14  (*Is the term eta-convertible to a single variable with the given rbinder?
    9.15    Examples: ?a   ?f(B.0)   ?g(B.1,B.0)
    9.16    Result is var a for use in SIMPL. *)
    9.17 -fun get_eta_var ([], _, Var vT) = vT
    9.18 -  | get_eta_var (_::rbinder, n, f $ Bound i) =
    9.19 -      if n = i then get_eta_var (rbinder, n + 1, f)
    9.20 +fun get_eta_var [] n (Var vT) = (n, vT)
    9.21 +  | get_eta_var (_ :: rbinder) n (f $ Bound i) =
    9.22 +      if n = i then get_eta_var rbinder (n + 1) f
    9.23        else raise ASSIGN
    9.24 -  | get_eta_var _ = raise ASSIGN;
    9.25 +  | get_eta_var _ _ _ = raise ASSIGN;
    9.26  
    9.27  
    9.28  (*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
    9.29    If v occurs rigidly then nonunifiable.
    9.30    If v occurs nonrigidly then must use full algorithm. *)
    9.31  fun assignment thy (rbinder, t, u) env =
    9.32 -  let val vT as (v,T) = get_eta_var (rbinder, 0, t) in
    9.33 +  let val (n, (v, T)) = get_eta_var rbinder 0 t in
    9.34      (case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
    9.35        NoOcc =>
    9.36 -        let val env = unify_types thy (Envir.body_type env ~1 T, fastype env (rbinder, u)) env
    9.37 -        in Envir.update (vT, Logic.rlist_abs (rbinder, u)) env end
    9.38 +        let val env = unify_types thy (Envir.body_type env n T, fastype env (rbinder, u)) env
    9.39 +        in Envir.update ((v, T), Logic.rlist_abs (rbinder, u)) env end
    9.40      | Nonrigid => raise ASSIGN
    9.41      | Rigid => raise CANTUNIFY)
    9.42    end;
    9.43  
    9.44  
    9.45  (*Extends an rbinder with a new disagreement pair, if both are abstractions.
    9.46 -  Tries to unify types of the bound variables!
    9.47    Checks that binders have same length, since terms should be eta-normal;
    9.48      if not, raises TERM, probably indicating type mismatch.
    9.49    Uses variable a (unless the null string) to preserve user's naming.*)
    9.50  fun new_dpair thy (rbinder, Abs (a, T, body1), Abs (b, U, body2)) env =
    9.51 -      let
    9.52 -        val env' = unify_types thy (T, U) env;
    9.53 -        val c = if a = "" then b else a;
    9.54 -      in new_dpair thy ((c,T) :: rbinder, body1, body2) env' end
    9.55 +      let val c = if a = "" then b else a
    9.56 +      in new_dpair thy ((c, T) :: rbinder, body1, body2) env end
    9.57    | new_dpair _ (_, Abs _, _) _ = raise TERM ("new_dpair", [])
    9.58    | new_dpair _ (_, _, Abs _) _ = raise TERM ("new_dpair", [])
    9.59    | new_dpair _ (rbinder, t1, t2) env = ((rbinder, t1, t2), env);
    9.60  
    9.61 -
    9.62  fun head_norm_dpair thy (env, (rbinder, t, u)) : dpair * Envir.env =
    9.63    new_dpair thy (rbinder,
    9.64      eta_norm env (rbinder, Envir.head_norm env t),
    9.65      eta_norm env (rbinder, Envir.head_norm env u)) env;
    9.66  
    9.67  
    9.68 -
    9.69  (*flexflex: the flex-flex pairs,  flexrigid: the flex-rigid pairs
    9.70    Does not perform assignments for flex-flex pairs:
    9.71      may create nonrigid paths, which prevent other assignments.
    9.72 @@ -247,7 +245,8 @@
    9.73  *)
    9.74  fun SIMPL0 thy dp0 (env,flexflex,flexrigid) : Envir.env * dpair list * dpair list =
    9.75    let
    9.76 -    val (dp as (rbinder, t, u), env) = head_norm_dpair thy (env, dp0);
    9.77 +    val (dp as (rbinder, t, u), env) =
    9.78 +      head_norm_dpair thy (unify_types_of thy dp0 env, dp0);
    9.79      fun SIMRANDS (f $ t, g $ u, env) =
    9.80            SIMPL0 thy (rbinder, t, u) (SIMRANDS (f, g, env))
    9.81        | SIMRANDS (t as _$_, _, _) =
    9.82 @@ -257,11 +256,9 @@
    9.83        | SIMRANDS (_, _, env) = (env, flexflex, flexrigid);
    9.84    in
    9.85      (case (head_of t, head_of u) of
    9.86 -      (Var (_, T), Var (_, U)) =>
    9.87 -        let
    9.88 -          val T' = Envir.body_type env ~1 T and U' = Envir.body_type env ~1 U;
    9.89 -          val env = unify_types thy (T', U') env;
    9.90 -        in (env, dp :: flexflex, flexrigid) end
    9.91 +      (Var (v, T), Var (w, U)) =>
    9.92 +        let val env' = if v = w then unify_types thy (T, U) env else env
    9.93 +        in (env', dp :: flexflex, flexrigid) end
    9.94      | (Var _, _) =>
    9.95          ((assignment thy (rbinder,t,u) env, flexflex, flexrigid)
    9.96            handle ASSIGN => (env, flexflex, dp :: flexrigid))
    9.97 @@ -415,11 +412,11 @@
    9.98  (*At end of unification, do flex-flex assignments like ?a -> ?f(?b)
    9.99    Attempts to update t with u, raising ASSIGN if impossible*)
   9.100  fun ff_assign thy (env, rbinder, t, u) : Envir.env =
   9.101 -  let val vT as (v, T) = get_eta_var (rbinder, 0, t) in
   9.102 +  let val (n, (v, T)) = get_eta_var rbinder 0 t in
   9.103      if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
   9.104      else
   9.105 -      let val env = unify_types thy (Envir.body_type env ~1 T, fastype env (rbinder, u)) env
   9.106 -      in Envir.vupdate (vT, Logic.rlist_abs (rbinder, u)) env end
   9.107 +      let val env = unify_types thy (Envir.body_type env n T, fastype env (rbinder, u)) env
   9.108 +      in Envir.vupdate ((v, T), Logic.rlist_abs (rbinder, u)) env end
   9.109    end;
   9.110  
   9.111