# maude-magic


<!-- WARNING: THIS FILE WAS AUTOGENERATED! DO NOT EDIT! -->

**Refs:** - [pexpect](https://pexpect.readthedocs.io/en/stable/) -
[nbdev](https://nbdev.fast.ai/tutorials/tutorial.html) - [IPython
magics](https://ipython.readthedocs.io/en/stable/config/custommagics.html) -
[Export
examples](https://nbdev1.fast.ai/export.html#Examples-of-export) - See
persistent Shells.ipynb - [Myst
Markdown](https://mystmd.org/guide/tables)

%%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

``` python

def MaudeShell(
    timeout:int=3
):

```

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

------------------------------------------------------------------------

### TimeoutException

``` python

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

``` python

def MaudeSystem(
    timeout:int=3
):

```

*Encapsulates maude commands as object methods.*

### Intantiation:

Firs, instantiate a MaudeSystem instance:

``` python
maude = MaudeSystem()
```

### Load:

``` python
maude.load('SIMPLE-NAT')
```

### Get a result in a tuple:

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

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

### Test red command:

``` python
maude.red('s s zero')
```

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

### Test for type and value:

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

### Test parse command:

``` python
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

``` python
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

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

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

``` python
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

``` python

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

``` python

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

``` python
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

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

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

``` python
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'}

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

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

### Cell input

``` python
fmod RESOURCE is sort Resource . endfm
```

    fmod RESOURCE is sort Resource . endfm

``` python
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

``` python
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

``` python
fmod BLANK-NODE is sort BlankNode . endfm
```

    fmod BLANK-NODE is sort BlankNode . endfm

``` python
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

``` python
fmod PREDICATE is protecting IRI . endfm
```

    > fmod PREDICATE is protecting IRI . endfm