src/Pure/logic.ML
changeset 4116 42606637f87f
parent 3963 29c5ec9ecbaa
child 4318 9b672ea2dfe7
     1.1 --- a/src/Pure/logic.ML	Tue Nov 04 12:46:50 1997 +0100
     1.2 +++ b/src/Pure/logic.ML	Tue Nov 04 12:58:10 1997 +0100
     1.3 @@ -26,7 +26,8 @@
     1.4    val list_flexpairs	: (term*term)list * term -> term
     1.5    val list_implies	: term list * term -> term
     1.6    val list_rename_params: string list * term -> term
     1.7 -  val loops		: Sign.sg -> term list -> term -> term
     1.8 +  val rewrite_rule_extra_vars: term list -> term -> term -> string option
     1.9 +  val rewrite_rule_ok   : Sign.sg -> term list -> term -> term
    1.10                            -> string option * bool
    1.11    val mk_equals		: term * term -> term
    1.12    val mk_flexpair	: term * term -> term
    1.13 @@ -350,7 +351,7 @@
    1.14  
    1.15  fun termless tu = (termord tu = LESS);
    1.16  
    1.17 -(** Check for looping rewrite rules **)
    1.18 +(** Test wellformedness of rewrite rules **)
    1.19  
    1.20  fun vperm (Var _, Var _) = true
    1.21    | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
    1.22 @@ -373,18 +374,26 @@
    1.23    although the rhs is an instance of the lhs. Example:
    1.24    ?m < ?n ==> f(?n) == f(?m)*)
    1.25  
    1.26 -fun loops sign prems lhs rhs =
    1.27 +fun rewrite_rule_extra_vars prems elhs erhs =
    1.28 +  if not ((term_vars erhs) subset
    1.29 +          (union_term (term_vars elhs, List.concat(map term_vars prems))))
    1.30 +  then Some("extra Var(s) on rhs") else
    1.31 +  if not ((term_tvars erhs) subset
    1.32 +          (term_tvars elhs  union  List.concat(map term_tvars prems)))
    1.33 +  then Some("extra TVar(s) on rhs")
    1.34 +  else None;
    1.35 +
    1.36 +fun rewrite_rule_ok sign prems lhs rhs =
    1.37    let
    1.38      val elhs = Pattern.eta_contract lhs;
    1.39      val erhs = Pattern.eta_contract rhs;
    1.40      val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
    1.41                 andalso not (is_Var elhs)
    1.42 -  in (if not ((term_vars erhs) subset
    1.43 -              (union_term (term_vars elhs, List.concat(map term_vars prems))))
    1.44 -      then Some("extra Var(s) on rhs") else
    1.45 -      if not perm andalso looptest sign prems elhs erhs
    1.46 -      then Some("loops")
    1.47 -      else None
    1.48 +  in (case rewrite_rule_extra_vars prems elhs erhs of
    1.49 +        None => if not perm andalso looptest sign prems elhs erhs
    1.50 +                then Some("loops")
    1.51 +                else None
    1.52 +      | some => some
    1.53        ,perm)
    1.54    end;
    1.55