1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml	Fri Apr 10 15:02:50 2020 +0200
     1.3 @@ -0,0 +1,58 @@
     1.4 +(* Title:  BaseDefinitions/rewrite-order.sml
     1.5 +   Author: Walther Neuper
     1.6 +   (c) due to copyright terms
     1.7 +
     1.8 +TODO: use "Rewrite_Ord" for renaming identifiers.
     1.9 +*)
    1.10 +signature REWRITE_ORDER =
    1.11 +sig
    1.12 +  type subst
    1.13 +  val e_rew_ord': Rule_Def.rew_ord';
    1.14 +  val dummy_ord: Rule_Def.rew_ord_
    1.15 +  val e_rew_ord: Rule_Def.rew_ord_
    1.16 +
    1.17 +  type rew_ord = Rule_Def.rew_ord
    1.18 +  val e_rew_ordX: rew_ord
    1.19 +
    1.20 +  type rew_ord' = Rule_Def.rew_ord'
    1.21 +  val rew_ord': (rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
    1.22 +  val assoc_rew_ord: string -> subst -> term * term -> bool
    1.23 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.24 +  (*NONE*)
    1.25 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.26 +  (*NONE*)
    1.27 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.28 +end
    1.29 +
    1.30 +(**)
    1.31 +structure Rewrite_Ord(**): REWRITE_ORDER(**) =
    1.32 +struct
    1.33 +(**)
    1.34 +
    1.35 +val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord';
    1.36 +type rew_ord_ = Rule_Def.rew_ord_;
    1.37 +type subst = (term * term) list;
    1.38 +fun dummy_ord (_: subst) (_: term, _: term) = true;
    1.39 +val e_rew_ord_ = dummy_ord;
    1.40 +
    1.41 +type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord
    1.42 +val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
    1.43 +val e_rew_ordX = (e_rew_ord', e_rew_ord_)
    1.44 +
    1.45 +type rew_ord' = Rule_Def.rew_ord'
    1.46 +(* rewrite orders, also stored in 'type met' and type 'and rls'
    1.47 +  The association list is required for 'rewrite.."rew_ord"..' *)
    1.48 +val rew_ord' = Unsynchronized.ref
    1.49 +  ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
    1.50 +	: (rew_ord' *    (* the key for the association list         *)
    1.51 +	    (subst 	    (* the bound variables - they get high order*)
    1.52 +	     -> (term * term) (* (t1, t2) to be compared                  *)
    1.53 +	     -> bool))        (* if t1 <= t2 then true else false         *)
    1.54 +		list);              (* association list                         *)
    1.55 +fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
    1.56 +  | assoc' ((keyi, xi) :: pairs, key) =
    1.57 +    if key = keyi then SOME xi else assoc' (pairs, key);
    1.58 +fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro))
    1.59 +  handle _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
    1.60 +
    1.61 +end
    1.62 \ No newline at end of file