Opened 5 years ago

Last modified 3 years ago

#9601 new feature request

Make the rewrite rule system more powerful

Reported by: spacekitteh Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.8.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Runtime performance bug Test Case:
Blocked By: Blocking:
Related Tickets: #9137, #10804 Differential Rev(s):
Wiki Page:

Description

It would be amazing if the current RULES system could be upgraded to include various predicates, or even into a full-on strategic programming system. This would allow far far more optimisations to be possible, rather than the current conservative system where you have to make sure that the optimisations ALWAYS apply.

Change History (9)

comment:1 Changed 5 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:2 Changed 4 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:3 Changed 4 years ago by thomie

Type of failure: None/UnknownRuntime performance bug

These tickets are related to runtime performance.

comment:5 Changed 4 years ago by bgamari

Milestone: 8.0.18.2.1

comment:6 Changed 4 years ago by nomeata

comment:7 Changed 3 years ago by bgamari

Milestone: 8.2.1

Removing milestone as this is more of a long-term goal.

comment:8 Changed 3 years ago by Iceland_jack

I don't know much about RULES, let me highlight this idea from ticket:9136#comment:1 (that lead to #9137):

forall x y z. (IsLiteral y, IsLiteral z) => (x +# y) -# z = x +# (y -# z)
forall x y z. (IsLiteral y, IsLiteral z) => (x -# y) -# z = x -# (y +# z)
...

This strikes my fancy! It's like a type class (predicate) for syntax

  • Could IsLiteral be given a kind?
  • Which constraint can be made available? (IsEven, IsOdd, ...)
  • Which properties can the compiler make use of?
  • Which properties can the optimizer make use of?

Edit: Maybe

forall op a b c. (Assoc op, IsLiteral b, IsLiteral c) => (a `op` b) `op` c => a `op` (b `op` c)

Edit 2: ..if a# and b# are statically known, so is a# +# b#

instance (IsStatic a#, IsStatic b#) => IsStatic (a# +# b#)
instance (IsStatic a#, IsStatic b#) => IsStatic (a# *# b#)

instance IsStatic (a# *# 0#)
instance IsStatic (0# *# b#)

instance IsStatic 0#
instance IsStatic 1#
...

instance IsStatic i# => IsStatic (I# i#)

hmph

Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:9 Changed 3 years ago by nomeata

The syntax might look like these are types, but morally, they are would simply be boolean predicates:

IsLiteral :: a -> Bool

These predicates could be normal, user defined functions (which the compiler would then try to symbolically evaluate), built-in “magic” predicates like this one, or functions without “normal” implementation, but with further rewrite rules that determine the predicate. Isabelle’s simplifier supports all that, and even more, if you are looking for inspiration.

Note: See TracTickets for help on using tickets.