Commit 6a633482 authored by Gaspard FEREY's avatar Gaspard FEREY

Working on making cicup_v22.maude confluent.

parent 7a7e9585
......@@ -5,8 +5,8 @@ fmod LPM is
op 0 : -> Nat [ctor] .
op 1 : -> Nat [ctor] .
op _+_ : Nat Nat -> Nat [comm assoc] .
op max : Nat Nat -> Nat .
op _+_ : Nat Nat -> Nat [comm assoc ctor] .
op max : Nat Nat -> Nat [comm assoc] .
op rule : Nat Nat -> Nat .
op U : Nat -> Type .
......@@ -19,16 +19,12 @@ fmod LPM is
op Pi : Type Type -> Type .
vars i j k l m x : Nat .
vars j k l m x : Nat .
vars i : Nat .
vars a b : Term .
eq i + 0 = i .
eq max(i, i + j) = i + j .
eq max(i + j, j) = i + j .
eq max(i, i) = i .
eq max(i, 0) = i .
eq max(0, i) = i .
eq rule(i, 0) = 0 .
eq rule(i, j + 1) = max(i, j + 1) .
......@@ -36,7 +32,12 @@ fmod LPM is
eq rule(i, i + j) = i + j .
eq rule(0, j) = j .
eq rule(i, i) = i .
eq rule(max(i,j), k) = max(rule(i,k), rule(j, k)) .
eq rule(i, max(j,k)) = max(rule(i,j), rule(i, k)) .
eq max(i, i + j) = i + j .
eq max(i, i) = i .
eq max(i, 0) = i .
eq liftn(0, a) = a .
eq liftn(i + 1, a) = lift(i, liftn(i, a)) .
......@@ -90,6 +91,4 @@ fmod LPM is
eq prod(i + 1, 0, lift(i, a), b) = prod(i, 0, a, b) .
eq prod( 1, 0, lift(0, a), b) = prod(0, 0, a, b) .
eq i + max(j, k) = max(i + j, i + k) .
endfm
load cicup_v22.maude
load cicup_v2.maude
load /home/gaspi/maude/MFE/src/mfe.maude
(select tool CRC .)
(ccr LPM .)
(show cps .)
(show all cps .)
Set Printing Universes.
Definition id {A : Type} (a : A) := a.
About id.
Definition id {A : Type} (a : A) := a.
Polymorphic Definition pid {A : Type} (a : A) := a.
About pid.
Definition aux := @pid (forall A:Type,A->A) (@id).
Print aux.
Polymorphic Definition paux := @pid (forall A:Type,A->A) (@id).
Definition pid_id := pid (@id).
Definition pid_id_expl := @pid (forall A:Type,A->A) (@id).
Print paux.
Definition pid_pid := pid (@pid).
Definition pid_pid_expl := @pid (forall A:Type,A->A) (@pid). (* identical *)
Polymorphic Definition paux2 := pid (@id).
Polymorphic Definition p_pid_id := pid (@id).
Polymorphic Definition p_pid_id_expl := @pid (forall A:Type,A->A) (@id).
Print paux2.
Polymorphic Definition p_pid_pid := pid (@pid).
Polymorphic Definition p_pid_pid_expl := @pid (forall A:Type,A->A) (@pid).
Print Universes.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment