wneuper/isa: src/Tools/isac/BaseDefinitions/rewrite-order.sml@b125dcf14489

     1 (* Title:  BaseDefinitions/rewrite-order.sml

     2    Author: Walther Neuper

     3    (c) due to copyright terms

     4 *)

     5 signature REWRITE_ORDER =

     6 sig

     7   val e_rew_ord': Rule_Def.rew_ord';

     8   val dummy_ord: Rule_Def.rew_ord_

     9   val e_rew_ord: Rule_Def.rew_ord_

    11   type rew_ord = Rule_Def.rew_ord

    12   val e_rew_ordX: rew_ord

    13   val to_string: rew_ord -> string

    15   type rew_ord' = Rule_Def.rew_ord'

    16   val equal: rew_ord * rew_ord -> bool

    17 end

    19 (**)

    20 structure Rewrite_Ord(**): REWRITE_ORDER(**) =

    21 struct

    22 (**)

    24 val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord';

    25 type rew_ord_ = Rule_Def.rew_ord_;

    26 fun dummy_ord (_: subst) (_: term, _: term) = true;

    27 val e_rew_ord_ = dummy_ord;

    29 type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord

    30 val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)

    31 val e_rew_ordX = (e_rew_ord', e_rew_ord_)

    32 fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)"

    34 type rew_ord' = Rule_Def.rew_ord'

    35 fun equal ((id1, _), (id2, _)) = id1 = id2

    37 end

author	wneuper <Walther.Neuper@jku.at>
	Wed, 03 Aug 2022 18:06:02 +0200
changeset 60507	b125dcf14489
parent 60506	145e45cd7a0f
child 60509	2e0b7ca391dc
permissions	-rw-r--r--