maude-magic

Execute a maude`s session in Jupyter Lab

Refs: - pexpect - nbdev - IPython magics - Export examples - See persistent Shells.ipynb - Myst Markdown

%%bash for package in pexpect nbdev jupyterlab-quarto do
pip list | grep “^\(package *" > /dev/null && echo "\)package found” || pip install $package done # This must be done in terminal # nbdev_install_quarto

The Maude Shell class

---

MaudeShell

def MaudeShell(
    timeout:int=3
):

Controls maude execution, executing commands and print responses. Preserve sessions between different cell executions.

---

TimeoutException

def TimeoutException(
    
):

Exception raised if time-out.

Creating maude shell:

Stdin-load an incomplete module:

Load a module:

Show module:

Make a reduction:

Warning:

The Maude System class:

---

MaudeSystem

def MaudeSystem(
    timeout:int=3
):

Encapsulates maude commands as object methods.

Intantiation:

Firs, instantiate a MaudeSystem instance:

maude = MaudeSystem()

Load:

maude.load('SIMPLE-NAT')

Get a result in a tuple:

maude._getTupleResult('red','s s zero',MaudeSystem.red_reo)

{'sort': 'Nat', 'value': 's s zero'}

Test red command:

maude.red('s s zero')

{'sort': 'Nat', 'value': 's s zero'}

Test for type and value:

maude.red('s s zero','Nat')
try:
    maude.red('s s zero','NzNat','s s zero')
except:
    pass  
else:
    raise Exception()

Test parse command:

maude.parse('s s zero')

{'sort': 'Nat', 'value': 's s zero'}

Test LOAD

Test READ

%%maude fmod SIMPLE-NAT is sort Nat . op zero : -> Nat . op s_ : Nat -> Nat . op + : Nat Nat -> Nat . vars M N : Nat . eq zero + N = N . eq s N + M = s (N + M) . endfm

Test SHOW

print(maude.show_module())

show module  .
fmod SIMPLE-NAT is
  sort Nat .
  op zero : -> Nat .
  op s_ : Nat -> Nat .
  op _+_ : Nat Nat -> Nat .
  vars M N : Nat .
  eq zero + N = N .
  eq s N + M = s (N + M) .
endfm

Test REDUCE

maude.red('s s zero','Nat','s s zero')

{'sort': 'Nat', 'value': 's s zero'}

maude.red('s s zero','Nat','s s zero',echo=True)

red s s zero .
reduce in SIMPLE-NAT : s s zero .
rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second)
result Nat: s s zero

{'sort': 'Nat', 'value': 's s zero'}

Destroying object closes session:

The maude Magic Class

---

load_ipython_extension

def load_ipython_extension(
    ipython
):

Any module file that define a function named load_ipython_extension can be loaded via %load_ext module.path or be configured to be autoloaded by IPython at startup time.

---

MaudeMagics

def MaudeMagics(
    shell:NoneType=None
):

Adapts Maude Shell to a IPython Magic class.Uses a owned Maude Shell. Cell magics are used to execute maude commands. Line magics are used for command line options.

Usage

Now, MaudeMagic uses an owned MaudeInterpreter to run maude commands:

Test maude Magic

fmod PEANO-NAT is
    sort Nat .
    op zero : -> Nat .
    op s_ : Nat -> Nat .
    op _+_ : Nat Nat -> Nat .
        
    eq zero +  N:Nat = N:Nat .
    eq s N:Nat + N':Nat = N:Nat + s N':Nat .     
endfm

fmod PEANO-NAT is
>     sort Nat .
>     op zero : -> Nat .
>     op s_ : Nat -> Nat .
>     op _+_ : Nat Nat -> Nat .
> 
>     eq zero +  N:Nat = N:Nat .
>     eq s N:Nat + N':Nat = N:Nat + s N':Nat .     
> endfm

maude.red('s zero + s s zero','Nat')

{'sort': 'Nat', 'value': 's s s zero'}

maude.trace=True
maude.red('s zero + s s zero','Nat')

Request:
 'red s zero + s s zero .\n'
Response:
 'red s zero + s s zero .\n\rreduce in PEANO-NAT : s zero + s s zero .\r\nrewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)\r\nresult Nat: s s s zero\r\n\rMaude> '
    Line: 'red s zero + s s zero .'
    Line: 'reduce in PEANO-NAT : s zero + s s zero .'
    Line: 'rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)'
    Line: 'result Nat: s s s zero'

{'sort': 'Nat', 'value': 's s s zero'}

maude.trace=False
maude.parse('s zero + s s zero','Nat')

{'sort': 'Nat', 'value': 's zero + s s zero'}

Cell input

fmod RESOURCE is sort Resource . endfm

fmod RESOURCE is sort Resource . endfm

fmod IRI is 
    pr RESOURCE .
    sort IRI . 
    *** Is a Biyection      
    op denotes  : IRI -> Resource . 
    op referent : IRI -> Resource .
endfm

fmod IRI is 
>     pr RESOURCE .
>     sort IRI . 
>     *** Is a Biyection      
>     op denotes  : IRI -> Resource . 
>     op referent : IRI -> Resource .
> endfm

fmod LITERAL-SORT is 
    ex RESOURCE . 
    sort Literal .
    op denotes : Literal -> Resource .     
endfm

fmod LITERAL-SORT is 
>     ex RESOURCE . 
>     sort Literal .
>     op denotes : Literal -> Resource .     
> endfm

fmod BLANK-NODE is sort BlankNode . endfm

fmod BLANK-NODE is sort BlankNode . endfm

fmod SUBJECT is
    protecting IRI . protecting BLANK-NODE . 
    sort Subject . 
    subsorts IRI BlankNode < Subject .
endfm

fmod SUBJECT is
>     protecting IRI . protecting BLANK-NODE . 
>     sort Subject . 
>     subsorts IRI BlankNode < Subject .
> endfm

fmod PREDICATE is protecting IRI . endfm

> fmod PREDICATE is protecting IRI . endfm