Melvar

To write an XCompose file, it is normally necessary to enumerate all the desired
sequences individually. However, there are many sets of related sequences with
common prefixes, as well as ones that differ only in a prefix, but have the same
result. Grouping such sets of sequences together, writing the prefix only once,
could ease both the initial writing and later changes (note that I do not assert
that it actually does).

This document is meant for suggestions on and discussion of both this concept
and possibilities of execution as a text-based notation that can be transformed
back into XCompose sequences.

Melvar

VARIABLE Ticks \ seconds
VARIABLE Tocks \ minutes
VARIABLE TickInterval \ TICKs *between* seconds
	19 TickInterval !

CREATE Digits \ bit patterns for digits 0-9 on the seven-segment displays
	63 , 6 , 219 , 207 , 230 , 237 , 253 , 7 , 255 , 239 ,
\ these I have a bit of trouble understanding: bits 0 to 5 appear to be as
\ expected, but for the center bar *both* bits 6 and 7 are set.

Melvar

┯(2)━(Mo Jul 08)━(20:17:45)━(melvar)@(ebony-tower)━(0)━(~/devel/idris/Idris-dev)━╸
└(2741)─($)→ make
cabal install 
Resolving dependencies...
[1 of 1] Compiling Main             ( /tmp/llvm-general-3.3.3.0-7494/llvm-general-3.3.3.0/Setup.hs, /tmp/llvm-general-3.3.3.0-7494/llvm-general-3.3.3.0/dist/setup/Main.o )
Linking /tmp/llvm-general-3.3.3.0-7494/llvm-general-3.3.3.0/dist/setup/setup ...
Configuring llvm-general-3.3.3.0...
Building llvm-general-3.3.3.0...
Preprocessing library llvm-general-3.3.3.0...
[ 1 of 93] Compiling LLVM.General.Internal.FFI.Transforms ( src/LLVM/General/Internal/FFI/Transforms.hs, dist/build/LLVM/General/Internal/FFI/Transforms.o )

Melvar

→ idris -p effects --codegen llvm TestMatrix.idr -o TestMatrix
LLVM ERROR: Cannot select: 0x57d50d0: f64 = sub 0x5739200, 0x57e4780 [ORD=12294] [ID=34]
  0x5739200: f64,ch = load 0x5600110:1, 0x56b84a0, 0x5606f80<LD8[%965]> [ORD=12290] [ID=31]
    0x56b84a0: i64 = add 0x57dd440, 0x57d46c0 [ORD=12289] [ID=24]
      0x57dd440: i64,ch,glue = CopyFromReg 0x57e4570, 0x56634a0, 0x57e4570:1 [ORD=12284] [ID=23]
        0x56634a0: i64 = Register %RAX [ORD=12284] [ID=8]
        0x57e4570: ch,glue = callseq_end 0x57d9500, 0x55d5280, 0x55d5280, 0x57d9500:1 [ORD=12284] [ID=22]
          0x55d5280: i64 = TargetConstant<0> [ORD=12284] [ID=4]
          0x55d5280: i64 = TargetConstant<0> [ORD=12284] [ID=4]
          0x57d9500: ch,glue = X86ISD::CALL 0x55d5480, 0x5602130, 0x56b8cb0, 0x57d3ec0, 0x55d5480:1 [ORD=12284] [ID=21]

Melvar

%unqualified

data JMEq : {A : Type} -> {B : Type} -> (x : A) -> (y : B) -> Type where
  Reflexivity : {A : Type} -> {x : A} -> JMEq x x