src/Pure/logic.ML
changeset 3893 5a1f22e7b359
parent 3408 98a2d517cabe
child 3915 0eb9b9dd4de6
     1.1 --- a/src/Pure/logic.ML	Thu Oct 16 13:43:42 1997 +0200
     1.2 +++ b/src/Pure/logic.ML	Thu Oct 16 13:45:16 1997 +0200
     1.3 @@ -26,6 +26,8 @@
     1.4    val list_implies	: term list * term -> term
     1.5    val list_rename_params: string list * term -> term
     1.6    val is_equals         : term -> bool
     1.7 +  val loops		: Sign.sg -> term list -> term -> term
     1.8 +                          -> string option * bool
     1.9    val mk_equals		: term * term -> term
    1.10    val mk_flexpair	: term * term -> term
    1.11    val mk_implies	: term * term -> term
    1.12 @@ -348,4 +350,42 @@
    1.13  
    1.14  fun termless tu = (termord tu = LESS);
    1.15  
    1.16 +(** Check for looping rewrite rules **)
    1.17 +
    1.18 +fun vperm (Var _, Var _) = true
    1.19 +  | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
    1.20 +  | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
    1.21 +  | vperm (t, u) = (t = u);
    1.22 +
    1.23 +fun var_perm (t, u) =
    1.24 +  vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
    1.25 +
    1.26 +(*simple test for looping rewrite*)
    1.27 +fun looptest sign prems lhs rhs =
    1.28 +   is_Var (head_of lhs)
    1.29 +  orelse
    1.30 +   (exists (apl (lhs,occs)) (rhs :: prems))
    1.31 +  orelse
    1.32 +   (null prems andalso
    1.33 +    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs));
    1.34 +(*the condition "null prems" in the last case is necessary because
    1.35 +  conditional rewrites with extra variables in the conditions may terminate
    1.36 +  although the rhs is an instance of the lhs. Example:
    1.37 +  ?m < ?n ==> f(?n) == f(?m)*)
    1.38 +
    1.39 +fun loops sign prems lhs rhs =
    1.40 +  let
    1.41 +    val elhs = Pattern.eta_contract lhs;
    1.42 +    val erhs = Pattern.eta_contract rhs;
    1.43 +    val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
    1.44 +               andalso not (is_Var elhs)
    1.45 +  in (if not ((term_vars erhs) subset
    1.46 +              (union_term (term_vars elhs, List.concat(map term_vars prems))))
    1.47 +      then Some("extra Var(s) on rhs") else
    1.48 +      if not perm andalso looptest sign prems elhs erhs
    1.49 +      then Some("loops")
    1.50 +      else None
    1.51 +      ,perm)
    1.52 +  end;
    1.53 +
    1.54  end;