iRho: An Imperative Rewriting-calculus

Luigi Liquori and Bernard Paul Serpette

INRIA Sophia Antipolis

 
Capsule. We propose an imperative version of the Rewriting-calculus, a calculus based on pattern-matching, pattern-abstraction, and side-effects, which we call iRho. We formulate a static and a big-step "call-by-value" operational semantics of iRho. The operational semantics is deterministic, and immediately suggests how to build an interpreter for the calculus. The static semantics is given via a first-order type system based on a form of product-types, which can be assigned to terms like structures (i.e., records). The calculus is "a la" Church, i.e., pattern-abstractions are decorated with the types of the free variables of the pattern. iRho is a good candidate for a core of a pattern-matching imperative language, where a (monomorphic) typed store can be safely manipulated and where fixed-points are built-in into the language itself. Properties such as determinism of the interpreter and subject-reduction are completely checked by a machine-assisted approach, using the Coq proof assistant. Progress and decidability of type-checking are proved by pen and paper.

GET  the V1.0


Snake: An Ascii-Oriented Script Language

Based on the Original Screenplay

of the Imperative Rewriting-calculus V1.1

Luigi Liquori

INRIA Sophia Antipolis

Capsule. La version de iRho V1.1, actuellement distribuée, a été complètement réécrite. Un nouveau parseur, des nouvelles constructions syntactiques ont été rajouté, comme par exemple, le gardes sur le patterns, les antipatterns (récemment formalisée par Kirchner-Moreau, ESOP-07), les antiexpressions, un mécanisme d exception et la possibilité de paramétrer une évaluation par rapport au type de filtrage (pattern matching) utilisée, etc. Snake est une version sucré de iRho où toutes les mots clés du langage sont complètement non-alpha, c.à.d. sans aucun mot clés en anglais ou francais (que des ascii-icones). iRho et Snake ont été implémentés en Bigloo-scheme ; chaque interprète fait  1K lignes ; ils sont utilisés comme plate-formee expérimentale utilisé par moi-même et par l équipe Protheo de Nancy pour expérimenter des nouvelles formes de filtrage à intégrer dans le compilateur TOM. Pour l absence de mots en anglais ou français et la présence que de simple icônes ascii, Snake pourrait être également utilisé pour apprendre de l algorithmique de base aux enfants.

Screenshot and help

bash-2.05b$ ./snake
 -----------------------------------------------------------
|            /^\/^\                                         |
|          _|__|  O|                                        |
| \/     /~     \_/ \                                       |
|  \____|__________/  \                                     |
|         \_______      \                                   |
|                 `\     \                 \                |
|                   |     |                  \              |
|                  /      /                    \            |
|                 /     /                       \\          |
|               /      /                         \ \        |
|              /     /                            \  \      |
|            /     /             _----_            \   \    |
|           /     /           _-~      ~-_         |   |    |
|          (      (        _-~    _--_    ~-_     _/   |    |
|           \      ~-____-~    _-~    ~-_    ~-_-~    /     |
|             ~-_           _-~          ~-_       _-~      |
|                ~--______-~                ~-___-~         |
|                                                           |
|                  S    N    A    K    E                    |
|                                                           |
|       The First Ascii-Oriented Programming Language       |
|          Based on the Original Screenplay of the          |
|            Imperative Rewriting Calculus v 1.1            |
|                                                           |
|                Kernel Certified by Coq                    |
|                Powered by Bigloo Scheme                   |
|                  Copyright INRIA 2005                     |
|                                                           |
|                NoEffect Theory Loaded                     |
|                   Version 1.1alpha                        |
|                   ? = Learn Snake                         |
 -----------------------------------------------------------
Snake << ?;;
 <Non_Cap_alphadgt>    as Constants                      e.g. a b x y foo2
 <Cap_alphadgt>        as Constants with HOLE inside     e.g. A B X Y FOO2
 \<Expr>               as Antiexpression                 e.g. \a \X \(X->X 3)
 <Cap_alphadgt>\<Expr> as Guarded Costants with HOLE     e.g. X\a X\Y X\(a->a b)
 ;;                    as the Symbol of Top Level        e.g. 3;;
 ,                     as the Symbol of Structures       e.g. (3,X,foo)
 ->                    as the Symbol of Rule             e.g. X->X
 ->|                   as the Symbol of Resultless Rule  e.g. X->|
 <Space>               as the Symbol of Rule Application e.g.(X->X 4)
 ^                     as the Symbol of Pointer          e.g. ^X
 !                     as the Symbol of Access Pointers  e.g. !X
 <Expr1> <- <Expr2>    as Assign <Expr2> to <Expr1>      e.g. X<-0
 [<Expr> | ...| <Expr>] define a Term Rewriting System
 <Expr1> ; <Expr2>                                       Eval first <Expr1>, and then <Expr2>
 <ElseExpr> <-? <CondExpr> ?-> <ThenExpr>                Conditional
 <HandExpr>  -) <ProtExpr>                               Declare Exception + Handler
                           (-  <RaiseExpr>               Raise   Exception
 <Cap_alphadgt> = <Expr> bind <Expr> to <Cap_alphadgt>  e.g. X = 0
 $ to Switch Theory (Noeffect vs Syntactical)
 # to Clean Namespace
 @ to Exit Snake

Some Try-me files in Snake GET-IT! or in iRho1.1 GET-IT!

GET  the Snake and iRhoV1.1