Reprogrammation complète

2 years ago · 6908956bc0
32 changed files with 1511 additions and 1054 deletions
--- a/.gitignore
+++ b/.gitignore
@ -1,25 +1,4 @@
-# ---> Haskell
+main
-dist
+*.cmi
-dist-*
+*.cmo
 cabal-dev
 *.o
 *.hi
 *.hie
 *.chi
 *.chs.h
 *.dyn_o
 *.dyn_hi
 .hpc
 .hsenv
 .cabal-sandbox/
 cabal.sandbox.config
 *.prof
 *.aux
 *.hp
 *.eventlog
 .stack-work/
 cabal.project.local
 cabal.project.local~
 .HTF/
 .ghc.environment.*
--- a/26
+++ b/26
@ -0,0 +1,26 @@
 CC = ocamlc
 MAIN = main
 all: $(MAIN)
 $(MAIN): tools.cmo unification.cmo stellar.cmo parser.cmo lexer.cmo main.cmo
 	$(CC) $^ -o $(MAIN)
 parser.ml: parser.mly
 	menhir --infer $^
 	$(CC) -c parser.mli
 lexer.ml: lexer.mll
 	ocamllex $^
 %.cmo: %.ml
 	$(CC) -c $^
 %.cmi: %.mli
 	$(CC) -c $^
 .PHONY: clean
 clean:
 	@echo "Project clean."
 	@rm -rf *.cmi *.cmo *.cmx *.mli *.o parser.ml lexer.ml parser.conflicts main
--- a/README.md
+++ b/README.md
@ -1,18 +1,122 @@
 # Large Star Collider
-Réalisation de la résolution stellaire.
+La résolution stellaire est un modèle de calcul proche de la résolution du premier ordre de Robinson qui est utilisée en programmation logique. Ce programme est une réalisation en OCaml de ce modèle de résolution stellaire.
-## Réalisation en OCaml
+Un **rayon** est un terme du premier ordre 
 ```
 r := X | f(r1, ..., rn) 
 ```
 où `f` est un symbole de fonction qui peut être préfixé ou non d'une polarité `+` ou `-` (par exemple `+f` et `-f`). Dans ce programme, on pourra aussi utiliser le symbole de fonction binaire `.` qui est infixe et associatif à droite (c'est-à-dire qu'on écrit `a . b . c` pour signifier `a . (b . c)`). Ce symbole est très utile pour créer des séquences de caractères (par exemple pour les mots en entrée des automates).
-Il faut dans un premier temps traduire Unification.hs en OCaml et bien commenter le programme pour réaliser l'unification entre termes. Tester le programme sur des exemples divers.
+Deux rayons qui contiennent des symboles polarisés peuvent être connectés lorsqu'ils sont unifiables sachant que les symboles de fonction identiques modulo inversion de polarité sont compatibles (habituellement, seuls les symboles égaux le sont).
-L'objectif est de réaliser un modèle de calcul appelé "résolution stellaire" qui fonctionne avec des agents indépendants appelés "étoiles" qui calculent en entrant mutuellement en interaction (de façon asynchrone et concurrente). Ces étoiles ont des termes polarisés attachés appelés rayons. L'interaction détruit les rayons connectés et propage la solution de l'équation associée aux rayons connectés aux rayons adjacents.
+Une **étoile** est une séquence de rayons qu'on peut considérer comme une clause dans un langage de programmation.
 ```
 [r1, ..., rn]
 ```
 Les étoiles sont capables d'interagir ensemble le long de rayons connectables par la règle de résolution de Robinson. Par exemple : `[X, -f(X)]` et `[+f(a)]` connectés ensemble le long du symbole `f` donne `[a]`.
 Il faudra dans un premier temps comprendre comment le modèle de calcul fonctionne. En particulier, il faudra comprendre la notion de graphe de dépendance, diagramme, de fusion/actualisation et d'exécution de constellation présentée dans l'article de Eng en références.
-L'idée de ce projet est que ce modèle de calcul est plutôt difficile à réaliser tel que décrit par la théorie mais qu'il existe en fait une manière beaucoup plus naturelle et satisfaisante de la programmer. Il faut voir le graphe de dépendance comme une sorte d'automate qu'on peut parcourir avec des jetons (voir document PDF dans le dépôt).
+Une **constellation** est une union disjointe d'étoiles séparées par le symbole `+`. On peut considérer que les constellations sont des sortes de programmes dans ce modèle. Une constellation est délimitée par des accolades.
 ```
 { [r11, ..., r1n] + ... + [rn1, ..., rnm] }
 ```
 Ce que l'on cherche à exécuter n'est pas une constellation mais un **espace d'interaction**. C'est une expression de la forme :
 ```
 <constellation> |- <constellation>
 ```
 La constellation à gauche de `|-` est la *constellation de référence* et la constellation de droite est *l'espace d'interaction*. L'idée de l'exécution est que les étoiles de l'espace d'interaction va se mettre à jour en interagissant avec des copies d'étoiles voisines mais aussi des copies d'étoiles de la constellation de référence.
 En termes de programmation logique, la constellation de référence est la base de connaissance et l'espace d'interaction est un ensemble de requêtes. Contrairement à la programmation logique (par exemple en Prolog), il n'y a aucune vraie distinction entre une requête et une autre clause. Nous avons donc un espace de résolution de contraintes avec une partie statique dont on tire des étoiles et l'autre dynamique où l'ont construit des solutions. 
 ## Compilation
 ```
 make
 ```
 Pour supprimer les fichiers de compilation et nettoyer le projet :
 ```
 make clean
 ```
 ## Usage
 Il faut simplement lancer l'exécutable `main`.
 ```
 ./main
 ```
 Vous pouvez utiliser les commandes suivantes :
 - `exit` pour quitter le programme (ou le mode interactif).
 - `exec -f <filename>` pour exécuter l'espace d'interaction contenu dans le fichier de nom `<filename>`.
 - `exec <intspace>` pour exécuter l'espace d'interaction `<intspace>`.
 - `intmode` lance le mode interactif avec la constellation vide comme constellation initiale (voir section "Mode interactif").
 - `intmode -f <filename>` lance le mode interactif avec la constellation définie dans `<filename>` (voir section "Mode interactif").
 - `intmode <constellation>` lance le mode interactif avec la constellation `<constellation>` (voir section "Mode interactif").
 - `disable-loops` interdit les équations de la forme `X=X` qui peuvent mener à des boucles triviales.
 - `enable-loops` autorise les boucles triviales.
 ## Mode interactif
 Le mode interactif est un mode ludique adapté aux grands et petits (âge minimum conseillé : 8 ans). Vous démarrez à partir de la constellation initiale vide `{}`. Toutes les constellations que vous écrivez vont interagir et mettre à jour votre constellation.
 Petite astuce : si vous écrivez une constellation qui ne peut interagir avec aucune étoile, cela va simplement l'ajouter à la constellation. Cela permet de remplir petit à petit votre constellation.
 ## Exemples
 Certains exemples avec l'extension `.stellar` sont déjà prêts à être exécutés. Ci-dessous, je présente quelques moyens de créer vos propres exemples. Dans mon manuscrit de thèse, vous retrouverez des méthodes pour réaliser de nombreux autres modèles comme des machines de Turing, automates à piles, transducteurs ou automates alternants de façon très simple.
 ### Programmes logiques
 Les faits sont des étoiles `[+p(t)]` et les règles d'inférences sont des étoiles `[-p(t1)]`
 ### Construire des automates finis
 L'encodage d'un automate fini doit nécessairement avoir les deux étoiles suivantes :
 - `[-i(W), +a(W, q0)]` encodant l'état initial (où `q0` peut être remplacé par un autre nom)
 - `[-a(e, qf), accept]` encodant l'état final (où `qf` peut être remplacé par un autre nom et `e` représente le mot vide "epsilon")
 Chaque transition d'un état `q1` vers un état `q2` le long d'une lettre `a` est encodée par une étoile
 ```
 [-a(a . W, q1), +a(W, q2)]
 ```
 Les mots sont encodés par des séquences de caractères séparés par l'opérateur binaire `.` et terminant par `e`. Par exemple `0 . 0 . 1 . e` ou `e` ou encore `1 . b . c . e`.
 Il faudra ensuite placer l'automate comme constellation de référence et l'étoile correspondant au mot comme seule étoile de l'espace d'interaction. Exemple d'espace d'interaction pour un automate :
 ```
 {
 	[-i(W), +a(W, q0)] +
 	[-a(e, q2), accept] +
 	[-a(0 . W, q0), +a(W, q0)] +
 	[-a(1 . W, q0), +a(W, q0)] +
 	[-a(0 . W, q0), +a(W, q1)] +
 	[-a(0 . W, q1), +a(W, q2)]
 }
 |-
 {
 	[+i(0 . 0 . 0 . e)]
 } 
 ```
 ### Construire des preuves de la logique linéaire multiplicatives
 Il est recommandé de suivre la construction proposée dans mon manuscrit de thèse. On traduit chaque axiome par une étoile binaire contenant la traduction des atomes associés.
 La traduction d'un atome `a` accessible par une conclusion `c` est donnée par un rayon `+c(t)` où `t` est une séquence de symboles `l` (left) et `r` (right) séparés par l'opérateur binaire `.` et terminant par la variable `X`. L'idée pour la construction de `t` est qu'il encode le chemin de `c` à `a`.
 Par exemple si à partir d'une conclusion `c`, on a besoin de remonter en allant deux fois à gauche puis une fois à droite pour atteindre `a`, la traduction de `a` sera `+c(l.l.r.X)`.
 Une coupure connectant les conclusions `c1` et `c2` est encodée par l'étoile `[-c1(X), -c2(X)]`.
 Étant donné que les structures de preuves peuvent être parcourues en commençant par n'importe quel atome libre, il suffit de placer une étoile avec un atome libre (non polarisé dans ce cas) dans l'espace d'interaction et utiliser le reste de la structure de preuve comme constellation de référence. Plus tard, je vais sûrement ajouter un mode "auto" pour sélectionner automatiquement une étoile de départ car ce n'est pas toujours nécessaire de le faire.
 ## Références
 - Term Rewriting and All That. Baader, Franz.
- [A gentle introduction to Girard's Transcendental Syntax for the linear logician. Eng.](https://hal.archives-ouvertes.fr/hal-02977750)
+- Le manuscrit de thèse de Boris Eng qui n'est pas encore sorti.
--- a/_build/_log
+++ b/_build/_log
@ -0,0 +1,2 @@
 ### Starting build.
 # Compilation unsuccessful.
--- a/_build/sanitize.sh
+++ b/_build/sanitize.sh
@ -0,0 +1,8 @@
 #!/bin/sh
 # File generated by ocamlbuild
 cd /mnt/e/Multimedia/Documents/Programming/large-star-collider
 rm -f lexer.ml
 # Also clean the script itself
 rm -f /mnt/e/Multimedia/Documents/Programming/large-star-collider/_build/sanitize.sh
--- a/automata.stellar
+++ b/automata.stellar
@ -0,0 +1,12 @@
 {
 	[-i(W), +a(W, q0)] +
 	[-a(e, q2), accept] +
 	[-a(0 . W, q0), +a(W, q0)] +
 	[-a(1 . W, q0), +a(W, q0)] +
 	[-a(0 . W, q0), +a(W, q1)] +
 	[-a(0 . W, q1), +a(W, q2)]
 }
 |-
 {
 	[+i(0 . 0 . 0 . e)]
 } 
--- a/haskell/ArithmeticsPL.hs
+++ b/haskell/ArithmeticsPL.hs
@ -1,39 +0,0 @@
 module ArithmeticsPL where
 import Unification
 import Resolution
 import Data.Semigroup
 import Data.Maybe
 vw = Var "w"
 vx = Var "x"
 vy = Var "y"
 vz = Var "z"
 z = Func "0" []
 s n = Func "s" [n]
 sn 0 b = b
 sn n b = s (sn (n-1) b)
 add x y z = Func "add" [x, y, z]
 mult x y z = Func "mult" [x, y, z]
 s1 = Star [Pos (add z vy vy)]
 s2 = Star [Pos (add (s vx) vy (s vz)), Neg (add vx vy vz)]
 cadd :: Constellation
 cadd = Const [
   Star [Pos (add z vy vy)],
   Star [Pos (add (s vx) vy (s vz)), Neg (add vx vy vz)]]
 qadd :: Int -> Int -> Constellation
 qadd n m = cadd <>
   Const [Star [Neg (add (sn n z) (sn m z) (Var "r")), NC (Var "r")]]
 cmult :: Constellation
 cmult = Const [
  Star [Pos (mult z vx z)],
  Star [Pos (mult (s vx) vy vz), Neg (mult vx vy vw), Neg (add vy vw vz)]]
 qmult :: Int -> Int -> Constellation
 qmult n m = cadd <> cmult <>
   Const [Star [Neg (mult (sn n z) (sn m z) (Var "r")), NC (Var "r")]]
--- a/haskell/Main.hs
+++ b/haskell/Main.hs
@ -1,9 +0,0 @@
 module Main where
 import Unification
 import Resolution
 import Data.Maybe
 import ArithmeticsPL
 import qualified Data.Set as Set
 main = do
    return ()
--- a/haskell/PrettyPrinter.hs
+++ b/haskell/PrettyPrinter.hs
@ -1,21 +0,0 @@
 module PrettyPrinter where
 import Data.Maybe
 import qualified Data.Set as Set
 {- Stars -}
 addsymbol :: Char -> Maybe Char -> [String] -> String
 addsymbol _ after [] =  ""
 addsymbol sym after (w:ws) = w ++ go ws
  where
    go [] = ""
    go (v:vs) =
      case after of
        Nothing -> sym : (v ++ go vs)
        Just after' -> sym : after' : (v ++ go vs)
 addop :: Char -> [String] -> String
 addop op w = addsymbol op Nothing w
 addcomma :: [String] -> String
 addcomma = addsymbol ',' (Just ' ')
--- a/haskell/Resolution.hs
+++ b/haskell/Resolution.hs
@ -1,260 +0,0 @@
 module Resolution where
 import qualified Unification
 import Data.Maybe
 import Data.List
 import Data.Tuple
 import PrettyPrinter as PrettyPrinter
 import Control.Arrow
 import Control.Monad
 import Data.Semigroup
 import qualified Data.Set as Set
 {- ========================================
    Definitions
   ======================================== -}
 data Polarized a = Pos a | Neg a | NC a deriving (Ord, Eq)
 type Ray = Polarized Unification.Term
 newtype Star = Star { get_star :: [Ray] }
 newtype Constellation = Const { get_const :: [Star] }
 newtype Link = Link { get_link :: ((Ray, Ray), Int, Int) }
 newtype StarGraph = StarGraph { get_graph :: ([Star], [Link]) }
 type UGraph = StarGraph
 type Diagram = StarGraph
 instance Functor Polarized where
  fmap f (Pos t) = Pos (f t)
  fmap f (Neg t) = Neg (f t)
  fmap f (NC t) = NC (f t)
 instance Eq Star where
  (Star s1) == (Star s2) = sort s1 == sort s2
 instance Eq Constellation where
  (Const s1) == (Const s2) = sort s1 == sort s2
 instance Eq Link where
  Link (e, i, j) == Link (e', i', j') =
      (i==i' && j==j' && i/=j) || (i==i' && j==j' && i==j && e==swap e')
 instance Ord Star where
  compare (Star s1) (Star s2) = compare s1 s2
 instance Show a => Show (Polarized a) where
  show (Pos t) = "+" ++ show t
  show (Neg t) = "-" ++ show t
  show (NC t) = show t
 instance Show Star where
  show (Star s) = show s
 instance Show Constellation where
  show (Const c) = show $ PrettyPrinter.addop '+' (map show c)
 instance Show Link where
  show (Link x) = show x
 instance Show StarGraph where
  show (StarGraph (v, e)) =
      "------------------------\n" ++
      "Vertices:\n" ++ unlines (mapInd (\x i -> show i ++ ":" ++ show x) v) ++
      "Edges:\n" ++ unlines (map show e)
 instance Semigroup Constellation where
  (Const c1) <> (Const c2) = Const (c1 ++ c2)
 mapInd :: (a -> Int -> b) -> [a] -> [b]
 mapInd f l = zipWith f l [0..]
 change_color :: String -> String -> Ray -> Ray
 change_color s s' r@(Neg (Unification.Func f ts))
  | f==s = Neg (Unification.Func s' ts)
 change_color s s' r@(Pos (Unification.Func f ts))
  | f==s = Neg (Unification.Func s' ts)
 change_color _ _ r = r
 dual :: Ray -> Ray -> Bool
 dual (Pos _) (Neg _) = True
 dual (Neg _) (Pos _) = True
 dual _ _ = False
 get_term :: Ray -> Unification.Term
 get_term (Pos t) = t
 get_term (Neg t) = t
 get_term (NC t) = t
 vars_ray :: Ray -> [Unification.Id]
 vars_ray (Pos t) = Unification.vars t
 vars_ray (Neg t) = Unification.vars t
 vars_ray (NC t)  = Unification.vars t
 vars_star :: Star -> [Unification.Id]
 vars_star (Star s) = concat $ map vars_ray s
 subst_ray :: Unification.Subst -> Ray -> Ray
 subst_ray = fmap . Unification.subst
 subst_rays :: Unification.Subst -> [Ray] -> [Ray]
 subst_rays = map . subst_ray
 extends_ray :: String -> Ray ->  Ray
 extends_ray = fmap . Unification.extends_varname
 extends_star :: String -> Star -> Star
 extends_star s (Star e) = Star (map (extends_ray s) e)
 rays :: Constellation -> [Ray]
 rays (Const cs) = [r | s<-cs, r<-(get_star s)]
 {- ========================================
    Unification graph
   ======================================== -}
 matchable_rays :: Ray -> Ray -> Bool
 matchable_rays r1 r2 = dual r1 r2 &&
  Unification.matchable (get_term r1, get_term r2)
 get_links :: Star -> Star -> [(Ray, Ray)]
 get_links (Star s1) (Star s2) =
  [(r1, r2) | r1<-s1, r2<-s2, matchable_rays r1 r2]
 ugraph :: Constellation -> UGraph
 ugraph (Const cs) =
  let imax = length cs - 1 in
  let pairs = [(i, j) | i<-[0..imax], j<-[0..imax], i<=j] in
  let e = foldl (\acc (i, j) ->
        let links = get_links (cs!!i) (cs!!j) in
        let make_edge e = Link (e, i, j) in
        if links==[] then acc else (map make_edge links) ++ acc) [] pairs in
  StarGraph (cs, nub e)
 {- ========================================
    Actualisation
   ======================================== -}
 make_edge :: [Star] -> (Int, Int) -> (Int, Int) -> Link
 make_edge xs (is1, ir1) (is2, ir2) =
    let (Star s1) = xs !! is1 in
    let (Star s2) = xs !! is2 in
    Link ((s1!!ir1, s2!!ir2), is1, is2)
 equations :: Diagram -> [Unification.Equation]
 equations (StarGraph (v, e)) =
    map (\(Link ((t, u), i, j)) ->
        let new_t = Unification.extends_varname (show i) (get_term t) in
        let new_u = Unification.extends_varname (show j) (get_term u) in
        (new_t, new_u)) e
 appears_in_link :: Ray -> Link -> Bool
 appears_in_link r (Link ((t, u), _, _)) = r==t || r==u
 already_linked :: Link -> [Link] -> Bool
 already_linked (Link ((t, u), i, j)) ls =
    any (\(Link ((t', u'), i', j')) ->
    (t==t' && i==i') || (u==u' && j==j') ||
    (t==u' && i==j') || (u==t' && j==i')) ls
 free_rays :: Diagram -> [Ray]
 free_rays (StarGraph (v, e)) =
    let linked = concat [[(extends_ray (show i) r, i), (extends_ray (show j) r', j)] | (Link ((r, r'), i, j))<-e] in
    let stars = mapInd (curry id) v in
    let rays = concat $ map (\(Star s, i) -> map (\r -> (extends_ray (show i) r, i)) s) stars in
    map fst (rays \\ linked)
 correct :: Diagram -> Bool
 correct d = free_rays d /= [] && (isJust $ Unification.solution (equations d))
 actualise :: Diagram -> Maybe Star
 actualise d = do
  u <- Unification.solution (equations d)
  pure $ Star (subst_rays u (free_rays d))
 fusions :: Star -> Star -> [Star]
 fusions (Star star1) (Star star2) = do
    ray1 <- star1
    ray2 <- star2
    guard (ray1 `matchable_rays` ray2)
    u <- maybeToList $ Unification.solution [(get_term ray1, get_term ray2)]
    [Star (subst_rays u (delete ray1 star1 ++ delete ray2 star2))]
 {- ========================================
    Execution
   ======================================== -}
 connect :: (Star, Int) -> (Star, Int) -> [Link]
 connect (Star s1, i) (Star s2, j) = do
    r1 <- s1
    r2 <- s2
    guard (r1 `matchable_rays` r2)
    [Link ((r1, r2), i, j)]
 saturated :: Constellation -> Diagram -> Bool
 saturated cs d =
    let free = free_rays d in
    let rs = rays cs in
    free_rays d /= [] &&
    [(r1, r2) | r1<-free, r2<-rs, r1 `matchable_rays` r2] == []
 shift_link :: Int -> Link -> Link
 shift_link k (Link (e, i, j)) = Link (e, i+k, j+k)
 singleStep :: Constellation -> Diagram -> [Diagram]
 singleStep (Const cs) d@(StarGraph (stars, links)) =
    let cs' = mapInd (curry id) cs in
    let stars' = mapInd (curry id) stars in
    do
    (s1, i) <- cs'
    (s2, j) <- stars'
    link <- connect (s1, 0) (s2, j+1)
    guard (not $ already_linked link (map (shift_link 1) links))
    pure (StarGraph (s1:stars, link:map (shift_link 1) links))
 allCorrectDiagrams :: Constellation -> [Diagram]
 allCorrectDiagrams (Const []) = []
 allCorrectDiagrams (Const cs) = go [StarGraph ([cs!!0], [])] where
    go (d : ds) = do
        d : go (ds ++ filter correct (singleStep (Const cs) d))
    go [] = []
 allCorrectSaturatedDiagrams :: Constellation -> [Diagram]
 allCorrectSaturatedDiagrams cs = filter (saturated cs) $ allCorrectDiagrams cs
 execution :: Constellation -> Constellation
 execution cs = Const (catMaybes $ map actualise (allCorrectSaturatedDiagrams cs))
 skeleton :: Constellation -> Constellation
 deleteAt :: Int -> [a] -> [a]
 deleteAt idx xs = lft ++ rgt
  where (lft, (_:rgt)) = splitAt idx xs
 fusion :: (Star, Int) -> (Star, Int) -> [Star]
 fusion (Star s1, i) (Star s2, j) =
    let r1 = s1 !! i in
    let r2 = s2 !! j in
    case Unification.solution [(get_term r1, get_term r2)] of
      Just u -> [Star (subst_rays u (deleteAt i s1 ++ deleteAt j s2))]
      Nothing -> []
 step :: Constellation -> [Star] -> [Star]
 step (Const cs) stars = do
    s1' <- cs
    s2' <- stars
    let s1 = get_star s1'
    let s2 = get_star s2'
    guard (s1 /= s2)
    i <- [0..length s1 - 1]
    j <- [0..length s2 - 1]
    guard ((s1 !! i) `matchable_rays` (s2 !! j))
    fusion (s1', i) (s2', j)
 steps :: Int -> Constellation -> [Star] -> [Star]
 steps 0 _ mem = mem
 steps k cs mem =
    let new = step cs mem in
    if new == [] then mem else mem ++ steps (k-1) cs new
 exec :: Constellation -> Constellation
 exec wcs@(Const cs) = Const (steps 0 wcs cs)
--- a/haskell/Unification.hs
+++ b/haskell/Unification.hs
@ -1,94 +0,0 @@
 module Unification where
 import PrettyPrinter
 import Data.List
 import Data.Maybe
 import Control.Arrow
 {- ========================================
    Definitions
   ======================================== -}
 type Id = String
 data Term =
      Var Id
    | Func Id [Term]
    deriving Eq
 type Subst = [(Id, Term)]
 type Equation = (Term, Term)
 instance Show Term where
    show (Var x) = x
    show (Func f []) = f
    show (Func f xs) = f ++ "(" ++ (addcomma (map show xs)) ++ ")"
 instance Ord Term where
    compare (Var x) (Var y) = compare x y
    compare (Var _) (Func _ _) = LT
    compare (Func _ _) (Var _) = GT
    compare (Func f fs) (Func g gs) =
      case compare f g of
        EQ -> compare fs gs
        LT -> LT
        GT -> GT
 {- ========================================
    Predicates
   ======================================== -}
 indom :: Id -> Subst -> Bool
 indom x s = isJust $ lookup x s
 occurs :: Id -> Term -> Bool
 occurs x (Var y) = (x==y)
 occurs x (Func _ ts) = any (occurs x) ts
 {- ========================================
    Renaming
   ======================================== -}
 extends_varname :: String -> Term -> Term
 extends_varname e (Var x) = Var (x++e)
 extends_varname e (Func f ts) = Func f (map (extends_varname e) ts)
 vars :: Term -> [Id]
 vars (Var x) = [x]
 vars (Func _ xs) = concat (map vars xs)
  {- ========================================
      Substitution
     ======================================== -}
 apply :: Subst -> Id -> Term
 apply ((y, t):s) x = if (x==y) then t else apply s x
 subst :: Subst -> Term -> Term
 subst s (Var x) = if indom x s then (apply s x) else (Var x)
 subst s (Func f ts) = Func f (map (subst s) ts)
 {- ========================================
    Unification
   ======================================== -}
 solve' :: [Equation] -> Subst -> Maybe Subst
 solve' [] s = Just s
 solve' ((Var x, t):ps) s = if (Var x == t) then solve' ps s else elim x t ps s
 solve' ((t, Var x):ps) s = elim x t ps s
 solve' ((Func f fs, Func g gs):ps) s =
    if (f == g) then solve' (zip fs gs ++ ps) s else Nothing
 elim :: Id -> Term -> [Equation] -> Subst -> Maybe Subst
 elim x t ps s =
    if occurs x t then Nothing
    else let sigma_xy = subst [(x, t)] in
    solve' (map (\(t1, t2) -> (sigma_xy t1, sigma_xy t2)) ps)
        ((x,t):map (\(y,u) -> (y, sigma_xy u)) s)
 solution :: [Equation] -> Maybe Subst
 solution p = solve' p []
 solvable :: [Equation] -> Bool
 solvable p = isJust (solution p)
 matchable :: Equation -> Bool
 matchable p = isJust $ solution [(extends_varname "0" *** extends_varname "1") p]
--- a/instructions.pdf
+++ b/instructions.pdf
--- a/lexer.ml
+++ b/lexer.ml
@ -0,0 +1,212 @@
 # 1 "lexer.mll"
  open Parser
  exception Eof
 # 7 "lexer.ml"
 let __ocaml_lex_tables = {
  Lexing.lex_base =
   "\000\000\240\255\241\255\001\000\003\000\243\255\002\000\245\255\
    \246\255\247\255\248\255\249\255\250\255\251\255\252\255\253\255\
    \078\000\088\000\244\255";
  Lexing.lex_backtrk =
   "\255\255\255\255\255\255\014\000\013\000\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \001\000\000\000\255\255";
  Lexing.lex_default =
   "\255\255\000\000\000\000\255\255\255\255\000\000\255\255\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \255\255\255\255\000\000";
  Lexing.lex_trans =
   "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\004\000\002\000\002\000\004\000\003\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \004\000\000\000\000\000\004\000\000\000\000\000\000\000\000\000\
    \015\000\014\000\000\000\008\000\013\000\007\000\005\000\018\000\
    \016\000\016\000\016\000\016\000\016\000\016\000\016\000\016\000\
    \016\000\016\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\017\000\017\000\017\000\017\000\017\000\017\000\017\000\
    \017\000\017\000\017\000\017\000\017\000\017\000\017\000\017\000\
    \017\000\017\000\017\000\017\000\017\000\017\000\017\000\017\000\
    \017\000\017\000\017\000\012\000\000\000\011\000\000\000\000\000\
    \000\000\016\000\016\000\016\000\016\000\016\000\016\000\016\000\
    \016\000\016\000\016\000\016\000\016\000\016\000\016\000\016\000\
    \016\000\016\000\016\000\016\000\016\000\016\000\016\000\016\000\
    \016\000\016\000\016\000\010\000\006\000\009\000\016\000\016\000\
    \016\000\016\000\016\000\016\000\016\000\016\000\016\000\016\000\
    \017\000\017\000\017\000\017\000\017\000\017\000\017\000\017\000\
    \017\000\017\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\016\000\
    \016\000\016\000\016\000\016\000\016\000\016\000\016\000\016\000\
    \016\000\016\000\016\000\016\000\016\000\016\000\016\000\016\000\
    \016\000\016\000\016\000\016\000\016\000\016\000\016\000\016\000\
    \016\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \001\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000";
  Lexing.lex_check =
   "\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\000\000\000\000\003\000\004\000\000\000\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \000\000\255\255\255\255\004\000\255\255\255\255\255\255\255\255\
    \000\000\000\000\255\255\000\000\000\000\000\000\000\000\006\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\255\255\000\000\255\255\255\255\
    \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
    \000\000\000\000\000\000\000\000\000\000\000\000\016\000\016\000\
    \016\000\016\000\016\000\016\000\016\000\016\000\016\000\016\000\
    \017\000\017\000\017\000\017\000\017\000\017\000\017\000\017\000\
    \017\000\017\000\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\016\000\
    \016\000\016\000\016\000\016\000\016\000\016\000\016\000\016\000\
    \016\000\016\000\016\000\016\000\016\000\016\000\016\000\016\000\
    \016\000\016\000\016\000\016\000\016\000\016\000\016\000\016\000\
    \016\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \000\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
    \255\255";
  Lexing.lex_base_code =
   "";
  Lexing.lex_backtrk_code =
   "";
  Lexing.lex_default_code =
   "";
  Lexing.lex_trans_code =
   "";
  Lexing.lex_check_code =
   "";
  Lexing.lex_code =
   "";
 }
 let rec read lexbuf =
   __ocaml_lex_read_rec lexbuf 0
 and __ocaml_lex_read_rec lexbuf __ocaml_lex_state =
  match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with
      | 0 ->
 # 12 "lexer.mll"
            ( VAR (Lexing.lexeme lexbuf) )
 # 132 "lexer.ml"
  | 1 ->
 # 13 "lexer.mll"
            ( SYM (Lexing.lexeme lexbuf) )
 # 137 "lexer.ml"
  | 2 ->
 # 14 "lexer.mll"
            ( LEFT_PAR )
 # 142 "lexer.ml"
  | 3 ->
 # 15 "lexer.mll"
            ( RIGHT_PAR )
 # 147 "lexer.ml"
  | 4 ->
 # 16 "lexer.mll"
            ( COMMA )
 # 152 "lexer.ml"
  | 5 ->
 # 17 "lexer.mll"
            ( LEFT_BRACK )
 # 157 "lexer.ml"
  | 6 ->
 # 18 "lexer.mll"
            ( RIGHT_BRACK )
 # 162 "lexer.ml"
  | 7 ->
 # 19 "lexer.mll"
            ( LEFT_BRACE )
 # 167 "lexer.ml"
  | 8 ->
 # 20 "lexer.mll"
            ( RIGHT_BRACE )
 # 172 "lexer.ml"
  | 9 ->
 # 21 "lexer.mll"
            ( PLUS )
 # 177 "lexer.ml"
  | 10 ->
 # 22 "lexer.mll"
            ( MINUS )
 # 182 "lexer.ml"
  | 11 ->
 # 23 "lexer.mll"
            ( VDASH )
 # 187 "lexer.ml"
  | 12 ->
 # 24 "lexer.mll"
            ( DOT )
 # 192 "lexer.ml"
  | 13 ->
 # 25 "lexer.mll"
            ( read lexbuf )
 # 197 "lexer.ml"
  | 14 ->
 # 26 "lexer.mll"
            ( read lexbuf )
 # 202 "lexer.ml"
  | 15 ->
 # 27 "lexer.mll"
            ( exit 0 )
 # 207 "lexer.ml"
  | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf;
      __ocaml_lex_read_rec lexbuf __ocaml_lex_state
 ;;
--- a/lexer.mll
+++ b/lexer.mll
@ -0,0 +1,27 @@
 {
  open Parser
  exception Eof
 }
 let var_id   = ['A'-'Z'] ['0'-'9']*
 let func_id  = ['a'-'z' '0'-'9']+
 let space    = [' ' '\t']+
 let newline  = '\r' | '\n' | "\r\n"
 rule read = parse
 	| var_id   { VAR (Lexing.lexeme lexbuf) }
 	| func_id  { SYM (Lexing.lexeme lexbuf) }
 	| '('      { LEFT_PAR }
 	| ')'      { RIGHT_PAR }
 	| ','      { COMMA }
 	| '['      { LEFT_BRACK }
 	| ']'      { RIGHT_BRACK }
 	| '{'      { LEFT_BRACE }
 	| '}'      { RIGHT_BRACE }
 	| '+'      { PLUS }
 	| '-'      { MINUS }
 	| "|-"     { VDASH }
 	| '.'      { DOT }
 	| space    { read lexbuf }
 	| newline  { read lexbuf }
 	| eof      { exit 0 }
--- a/loop.stellar
+++ b/loop.stellar
@ -0,0 +1 @@
 { [-1(X), -2(X)] } |- { [+1(X), +2(X)] }
--- a/main.ml
+++ b/main.ml
@ -0,0 +1,136 @@
 open Stellar
 open Parser
 open Tools
 (* ---------------------------------------
   Prompt
   --------------------------------------- *)
 let welcome () = print_endline "Use 'help' for the list of commands."
 let tab = repeat_string "\t"
 let line = repeat_string "-"
 let commands_list () =
 	print_endline ("Command" ^ tab 4 ^ "Description (shortcut)");
 	print_endline (line 70);
 	print_endline ("exit" ^ tab 4 ^ "Exits the program");
 	print_endline ("exec -f <filename>" ^ tab 2 ^ "Executes the constellation defined in <filename>");
 	print_endline ("exec <intspace>" ^ tab 3 ^ "Executes the interaction space <intspace>");
 	print_endline (
 		"intmode" ^
 		tab 4 ^
 		"Enables interactive mode with the empty constellation as initial constellation."
 	);
 	print_endline (
 		"intmode <constellation>" ^
 		tab 2 ^
 		"Enables interactive mode with <constellation> as initial constellation"
 	);
 	print_endline (
 		"intmode -f <filename>" ^
 		tab 2 ^
 		"Enables interactive mode with the constellation defined in <filename> as initial constellation"
 	);
 	print_endline (
 		"disable-loops" ^
 		tab 2 ^
 		"Forbid equations X=X which yields trivial loops"
 	);
 	print_endline (
 		"enable-loops" ^
 		tab 2 ^
 		"Allow equations X=X which yields trivial loops (default setting)"
 	)
 	(* print_endline (
 		"load <filename> as <var>" ^
 		tab 1 ^
 		"Stores a constellation defined in <filename> as <var> in the environement"
 	);
 	print_endline (
 		"store <constellation> as <var>" ^
 		tab 1 ^
 		"Stores a constellation defined in <constellation> as <var> in the environement"
 	) *)
 let prompt () = print_string "> "
 let intmode_prompt cs =
 	print_endline ">>>>>>>>>> Interactive mode";
 	print_endline "Type constellations and they will interact your initial constellation ('exit' to exit interactive mode).";
 	print_endline (string_of_constellation cs)
 let rec intmode ?(withloops=true) cs =
 	prompt ();
 	let input = read_line () in
 	if input = "exit" then
 		print_endline "<<<<<<<<<< Exit interactive mode"
 	else
 		(try
 			let cs' = constc Lexer.read (Lexing.from_string input) in
 			let result = intexec ~withloops (cs, cs') in
 			print_endline (string_of_constellation result);
 			intmode result
 		with _ ->
 			print_endline "Syntax error. Please try again.";
 			intmode cs)
 let last_command : string option ref = ref None
 (* ---------------------------------------
   Main function
   --------------------------------------- *)
 let _ =
 	let withloops = ref true in
 	welcome ();
 	while true do
 		prompt ();
 		let input = read_line () in 
 		begin match String.split_on_char ' ' input with
 		| ["exit"] -> exit 0
 		| ["disable-loops"] ->
 			print_endline "Loops disabled."; withloops := false
 		| ["enable-loops"] ->
 			print_endline "Loops enabled."; withloops := true
 		| ["help"] -> commands_list ()
 		| ["exec"; "-f"; filename] ->
 			begin try
 				let lexbuf = Lexing.from_channel (open_in filename) in
 				let cs = spacec Lexer.read lexbuf in
 				let result = intexec ~withloops:!withloops cs in
 				print_endline (string_of_constellation result)
 			with Sys_error f -> print_endline f
 			end
 		| "exec"::intspace ->
 			let lexbuf = Lexing.from_string (String.concat " " intspace) in
 			(try 
 				let cs = spacec Lexer.read lexbuf in
 				let result = intexec ~withloops:!withloops cs in
 				print_endline (string_of_constellation result)
 			with _ -> print_endline "Syntax error. Please try again.")
 		(* | ["load"; filename; "as"; x] ->
 			let fchannel = open_in filename in
 			let lexbuf = Lexing.from_channel fchannel in
 			let cs = constc Lexer.read lexbuf in
 			env := (x, cs) :: (!env) *)
 		| ["intmode"; "-f"; filename] ->
 			(try
 				let lexbuf = Lexing.from_channel (open_in filename) in
 				let cs = constc Lexer.read lexbuf in
 				intmode_prompt cs;
 				intmode cs
 			with Sys_error f -> print_endline f)
 		| ["intmode"] ->
 			intmode_prompt [];
 			intmode []
 		| "intmode"::intspace ->
 			let lexbuf = Lexing.from_string (String.concat " " intspace) in
 			let cs = constc Lexer.read lexbuf in
 			intmode_prompt cs;
 			intmode cs
 		| _ ->
 			print_endline "Invalid command. Please type 'help' for the list of commands."
 		end
 	done
--- a/mllcorrectness.stellar
+++ b/mllcorrectness.stellar
@ -0,0 +1,3 @@
 { [+5(l.X), +6(l.X)] + [+5(r.X), +6(r.X)] + [-5(l.X), -5(r.X), 5(X)] + [-6(l.X)] }
 |-
 { [-6(r.X), 6(X)] }
--- a/mllcutelim.stellar
+++ b/mllcutelim.stellar
@ -0,0 +1,3 @@
 { [+7(l.X), +7(r.X)] + [3(X), +8(l.X)] + [-7(X), -8(X)] }
 |-
 { [+8(r.X), 6(X)] }
--- a/ocaml/Circuits.ml
+++ b/ocaml/Circuits.ml
@ -1,107 +0,0 @@
 (* ============================================
               Boolean circuits
   ============================================ *)
 (* _________ Types _________ *)
 type var = string
 type id = int 
 type op =
  | CIn of int | COut | CShare
  | CAnd | COr | CNeg
 type input = id
 type output = id
 type gate = input list * op * output list
 type circuit = gate list
 (* _________ Getters _________ *)
 let get_node_info circ target =
  let (ins, op, outs) =
    List.hd (List.filter (fun (_, _, outs) -> List.mem target outs) circ)
  in (ins, op, outs)
 let get_inputs circ node =
  let (ins, _, _) = get_node_info circ node in ins
 let get_outputs circ node =
  let (_, _, outs) = get_node_info circ node in outs
 let get_op circ node =
  let (_, op, _) = get_node_info circ node in op
 (* extracts the two first inputs in a list of inputs *)
 let twinhd = function
  | [] -> failwith "Error extract_bin_ins: no input."
  | h1::h2::t -> (h1, h2)
  | _ -> failwith "Error extract_bin_ins: inputs do not match." 
 (* _________ Evaluation _________ *)
 (* provides the boolean value of the node 'concl' in a circuit 'circ' *)
 let rec value circ concl =
  match get_op circ concl with
  | CIn i -> i
  | CShare | COut ->
      let x = List.hd (get_inputs circ concl) in
      value circ x
  | CAnd ->
      let (x, y) = twinhd (get_inputs circ concl) in
      let vx = value circ x in
      let vy = value circ y in
      min vx vy
  | COr ->
      let (x, y) = twinhd (get_inputs circ concl) in
      let vx = value circ x in
      let vy = value circ y in
      max vx vy
  | CNeg ->
      let x = List.hd (get_inputs circ concl) in
      let vx = value circ x in
      1 - vx
 let rec eval (circ : circuit) : int =
  let (_, _, concl) =
    List.hd (List.filter (fun (_, o, _) -> o = COut) circ)
  in value circ (List.hd concl)
 (* _________ Examples _________ *)
 let make_gate ins op outs : gate = (ins, op, outs)
 let make_input value outs : gate = ([], CIn value, outs)
 let make_and_circ x y : circuit = [
  make_input x [0];
  make_input y [1];
  make_gate [0;1] CAnd [2];
  make_gate [2] COut [3]
 ]
 let make_or_circ x y : circuit = [
  make_input x [0];
  make_input y [1];
  make_gate [0;1] COr [2];
  make_gate [2] COut [3]
 ]
 let make_neg_circ x : circuit = [
  make_input x [0];
  make_gate [0] CNeg [1];
  make_gate [1] COut [2]
 ]
 (* corresponds to the excluded middle x v ~x *)
 let make_em_circ x : circuit = [
  make_input x [0];
  make_gate [0] CShare [1;2];
  make_gate [1] CNeg [3];
  make_gate [3;2] COr [4];
  make_gate [4] COut [5]
 ]
 let c1 = List.map eval [make_and_circ 0 0; make_and_circ 0 1; make_and_circ 1 0; make_and_circ 1 1]
 let c2 = List.map eval [make_or_circ 0 0; make_or_circ 0 1; make_or_circ 1 0; make_or_circ 1 1]
 let c3 = List.map eval [make_neg_circ 0; make_neg_circ 1]
 let c4 = List.map eval [make_em_circ 0; make_em_circ 1]
--- a/ocaml/FSA.ml
+++ b/ocaml/FSA.ml
@ -1,32 +0,0 @@
 (* ============================================
              Finite State Automata
   ============================================ *)
 type id = int
 type state = id
 type initial_state = state
 type final_state = state
 type fa_transition = state * char * state
 type fautomata = initial_state * (fa_transition list) * final_state list
 let accepts ((qi, ts, qf) : fautomata) (w : char list) =
  let rec head q (read : char list) =
    match read with
    | [] -> List.mem q qf
    | c::w ->
      let (_, _, qnext) =
        List.hd (List.filter (fun (qs, c', qt) -> qs=q && c=c') ts)
      in head qnext w
  in head qi w
 (* _________ Examples _________ *)
 let even_ones : fautomata = (
  0,
  [
    (0, '1', 1);
    (1, '1', 0)
  ],
  [0]
 )
--- a/ocaml/Resolution.ml
+++ b/ocaml/Resolution.ml
@ -1,250 +0,0 @@
 open Unification
 (* ========================================
     Definitions
   ======================================== *)
 type pol = Pos | Neg | Npol
 type ray = Var of id | Func of (id * pol * ray list)
 (* alternative ray definition using terms *)
 (* type ray = PR of id * pol * ray | NR of term *)
 type star = ray list
 type constellation = star list
 type graph = (int * int) * (ray * ray) list
 (* token is a couple of a family number and a star number in the constellation *)
 type token = int * int
 type process = token list
 (* List monad *)
 let return x = [x] (*plongement dans la monade de liste*)
 let (>>=) xs k = List.flatten (List.map k xs)
 let guard c x = if c then return x else []
 (* ========================================
     Useful functions
   ======================================== *)
 let make_const_pol pol c = Func (c, pol, [])
 let make_const c = make_const_pol Npol c
 (* Takes a list and remove doubles from it *)
 let remove_double list =
  List.fold_left (fun l a -> if not(List.mem a l) then (a::l) else l) [] list
 (* Convert a pol and an id to a string, adding + or - before the id *)
 let pol_to_string pol id =
    if pol = Pos then "+" ^ id 
    else if pol = Neg then "-" ^ id 
    else id
 (* Convert a ray (which is polarized) to a term (which isn't)*)
 let rec ray_to_term r =
  match r with
  | Var id -> (Var(id) : term)
  | Func(id, pol, raylist) -> (Func(pol_to_string pol id, List.map ray_to_term raylist) : term)
 (* Invert polarization of a pol*)
 let inv_pol pol = 
    if pol = Pos then Neg
    else if pol = Neg then Pos 
    else pol
 (* Invert the polarization of a ray to allow an easier Unification writing *)
 let rec inv_pol_ray ray = 
    match ray with
    | Func(id, pol, raylist) -> Func(id, inv_pol pol, List.map inv_pol_ray raylist)
    | _ -> ray
 (* Checks if a ray is polarised *)
 let rec is_polarised r =
    match r with
    | Var id -> false
    | Func(_, p, r) -> (p <> Npol) || (List.fold_left (fun acc b -> (is_polarised b) || acc) false r)
 (* Checks if two rays are dual, meaning that after inverting polarization of one ray, the two rays can be unified *)
 let dual_check r1 r2 =
  if (is_polarised r1 && is_polarised r2) then 
  (solve [(extends_varname (ray_to_term (inv_pol_ray r1)) "0"), (extends_varname ((ray_to_term r2)) "1")] []) 
  else None
 (* Create an index for a constellation *)
 let index_constellation const = 
    List.combine (List.init (List.length const) (fun a -> a)) const
 (* apply_ray applies a substitution to a var of a ray*)
 let apply_ray id sub = 
  let (_,s) = try List.find (fun (a,_) -> a = id ) sub with Not_found -> (id,Var(id)) in (s :ray)
 (* substit_ray applies all possible substition from an environment to a ray *)
 let rec substit_ray ray sub =
  match ray with
  | Var id -> apply_ray id sub  
  | Func(f, p, tl) -> Func(f, p, List.map (fun a -> substit_ray a sub) tl) 
 (* substit_star applies all possible substition from an environment to a star *)
 let substit_star star sub =
  List.map (fun a -> substit_ray a sub) star
 (* substit_const applies all possible substition from an environment to a constellation *)
 let substit_const const sub =
  List.map (fun a -> substit_star a sub) const
 (* extends_varname adds suffix to all var names of a ray *)  
 let rec extends_varname_ray t ext =
  match t with
  | Var id -> Var(id ^ ext)
  | Func(f, p, tl) -> Func(f, p, List.map (fun a -> extends_varname_ray a ext) tl)
 (* extends_varname adds suffix to all var names of a star *)
 let extends_varname_star const ext =
  List.map (fun a -> extends_varname_ray a ext) const
 (* extends_varname adds suffix to all var names of a constellation based on each star number after being indexed *)
 let extends_varname_const const =
  List.map (fun (i,a) -> extends_varname_star a (string_of_int i)) (index_constellation const)
 (* convert a term to a ray *)
 let rec term_to_ray (term : term) =
  match term with
  | Var id -> (Var(id) : ray)
  | Func(f, r) -> Func(f, Npol, List.map (fun a -> term_to_ray a) r)
 (* convert a star to a string*)
 let rec  star_to_string star =
  match star with
  | [] -> ""
  | h::t -> term_to_string (ray_to_term h) ^ "\n" ^ (star_to_string t)
 (*print a star*)
 let print_star star =
    print_string (star_to_string star)
 (*convert a constellation to a string*)
 let rec const_to_string const =
  match const with
  | [] -> ""
  | h::t -> (star_to_string h) ^ "---------- \n" ^ (const_to_string t)
 (*print a constellation*)
 let print_const const =
  print_string (const_to_string const)  
 (* ========================================
     Constellation graph
   ======================================== *)
 (* Makes a dgraph from a constellation *)
 let dgraph const =
  let indexed_const = index_constellation const in 
  indexed_const >>= fun (i, il) ->
  indexed_const >>= fun (j, jl) ->
  il >>= fun r1 ->
  jl >>= fun r2 ->
  guard (j >= i) ( let uni = dual_check r1 r2 in 
                   if Option.is_some uni then [((i,j),(r1,r2))]
                   else [])
 (* Convert a link to a string to be printable *)
 let link_to_string dg = 
  let rec aux dgl =
    match dgl with
    | [] -> ""
    | ((i,j),(r1, r2))::[] -> ("(" ^ string_of_int i ^ ", " ^ string_of_int j ^ ")" ^ "," ^ "(" ^ term_to_string (ray_to_term r1) ^ ", " ^ term_to_string (ray_to_term r2) ^ ")")
    | ((i,j),(r1, r2))::t -> ("(" ^ string_of_int i ^ ", " ^ string_of_int j ^ ")" ^ "," ^ "(" ^ term_to_string (ray_to_term r1) ^ ", " ^ term_to_string (ray_to_term r2) ^ ")") ^ "+" ^ (aux t)
  in aux dg ;;
 (* Convert an equation list (which is a link without the index) to a string *)
 let eq_to_string eq = 
  let rec aux dgl =
    match dgl with
    | [] -> ""
    | ((r1, r2))::[] -> ("(" ^ term_to_string (ray_to_term r1) ^ " = " ^ term_to_string (ray_to_term r2) ^ ")")
    | ((r1, r2))::t -> ("(" ^ term_to_string (ray_to_term r1) ^ " = " ^ term_to_string (ray_to_term r2) ^ ")") ^ "\n" ^ (aux t)
  in aux eq;;
 (* print an equation list*)
 let print_eq eq =
  print_string (eq_to_string eq)
 (* remove empty list from a dgraph *)
 let clean_dgraph g =
  List.filter (fun a -> a <> []) g
 (* Print a dgraph *)
 let print_dgraph dg =
  let rec aux dgl =
    match dgl with
    | [] -> ""
    | h::[] -> (link_to_string h)
    | h::t -> (link_to_string h) ^ "\n" ^ aux t 
  in print_string (aux (clean_dgraph dg));;
  (* get a star using its number in the list from a constellation *)
 let get_star const i =
  List.nth const i
 (* Takes a constellation, a ray and a (ray,ray) list and extracts rays from stars number i (respectively j) that are  not ri (respectively rj) when ri (respectively rj) isn't in the prob list *)
 let star_filter const ((i, j),(ri,rj)) prob =
  let (prob_a, prob_b) = List.split prob in
  (if List.mem ri prob_a then []
  else (List.filter (fun a -> a <> ri) (get_star const i))
  )@( 
  if List.mem rj prob_b then []
  else (List.filter (fun a -> a <> rj) (get_star const j))
  )
 (* convert the (ray,ray) list part of a link to an equation, converting its rays to terms *)
 let link_to_eq prob =
  List.map (fun (ra, rb) -> (ray_to_term (inv_pol_ray ra)), ray_to_term rb) prob
 (* removes rays from prob from the star *)
 let star_postfilter star prob =
  let (prob_a, prob_b) = List.split prob in
  List.filter (fun a -> not(List.mem a prob_a) && not(List.mem a prob_b )) star
 (* takes a token, a graph and a constellation and returns the list of tokens to check next and a list of solvable equation *)
 let divide_token (fam, n_star) toklist graph const prob fstar =
  let links = List.filter (fun ((i, _),(_, _)) -> i = n_star) graph in
    let rec aux l tokl prob_aux star_aux =
      match l with
        [] -> Some (tokl,prob_aux,star_aux,fam)
        | ((i, j),(ri,rj))::tl -> 
        if fam > (List.length prob_aux) || prob_aux = [] then (* We check if the family number is the same as the number of equations lists in prob. If it's superior, we add a new list in prob instead of filling the first equation list because it means we're treating a new family *)
          if Option.is_some (dual_check ri rj) then 
            aux tl ((fam, j)::tokl) ([(ri, rj)]::prob_aux) ( (( star_filter const ((i, j),(ri,rj)) [] ))::star_aux )
          else None
        else 
          if Option.is_some (solve (link_to_eq ((ri, rj)::(List.hd(*nth*) prob_aux (*fam*)))) []) then (* We made sure prob_aux head would not be empty*)
            aux tl ((fam, j)::tokl) (((ri, rj)::(List.hd prob_aux))::(List.tl prob_aux)) ( (( star_filter const ((i, j),(ri,rj)) (List.hd prob_aux) )@(List.hd star_aux))::(List.tl star_aux) ) (*We use List.hd because the current family we're working on should be the current first*)
          else
            None
    in if links = [] then Some (toklist,prob,fstar,fam) 
    else aux links toklist prob fstar
 (* should be deterministic exec, graph shouldn't be empty, takes a constellation and a list of stars that are gonna be beginning points *)
 (* Start_star_list, the second argument, should not be empty*)
 let exec const start_star_list =
  let const_ext = extends_varname_const const in
  let graph = List.flatten (clean_dgraph (dgraph const_ext)) in
  let max_fam = List.length start_star_list in
  let rec aux (toklist,prob,star,current_fam) = (*toklist is a list of tokens (int of family number and the number of a star), prob is the current list of equations, current_fam is the current family number  *)
    begin match toklist with
      | [] -> 
          if current_fam = max_fam-1 then star,prob 
          else aux ([(current_fam+1, List.nth start_star_list (current_fam+1))], prob, star, current_fam+1)
      | h::t -> aux (Option.get (divide_token h t graph const_ext prob star ))
    end              
  in if start_star_list = [] then
    failwith "star_star_list is empty"
  else  
    let i = List.hd start_star_list
  in let (constf, prob_tmp) = aux ([(0,i)],[],[],0) 
  in let probf = List.rev prob_tmp
  in let indexed_final_const = index_constellation constf
  in List.map (fun (fam_star, a) -> 
    let fam_prob = List.nth probf fam_star
    in let substit_list = (List.map (fun (i,b) -> (i,term_to_ray b)) (Option.get (solve (link_to_eq fam_prob) [])))
    in substit_star (remove_double (star_postfilter a fam_prob)) substit_list) indexed_final_const
--- a/ocaml/StellarCircuits.ml
+++ b/ocaml/StellarCircuits.ml
@ -1,55 +0,0 @@
 open Circuits
 open Resolution
 (* ============================================
               Stellar Circuits
   ============================================ *)
 let port pol i v = Func ("c"^(string_of_int i), pol, v)
 let inport i x = port Neg i [Var x]
 let outport i x = port Pos i [Var x]
 let call_cneg pol arg res = Func ("neg", pol, [arg; res])
 let call_cand pol arg1 arg2 res = Func ("and", pol, [arg1; arg2; res])
 let call_cor pol arg1 arg2 res = Func ("or", pol, [arg1; arg2; res])
 let star_of_gate circ (ins, op, outs) =
  match op with
  | CIn i -> [port Pos (List.hd outs) [make_const (string_of_int i)]]
  | COut -> [inport (List.hd ins) "r"; Var "r"]
  | CShare -> 
      let (o1, o2) = twinhd outs in
      [inport (List.hd ins) "x"; outport o1 "x"; outport o2 "x"] 
  | CNeg -> [
      inport (List.hd ins) "x";
      call_cneg Neg (Var "x") (Var "r");
      outport (List.hd outs) "r" 
    ]
  | CAnd ->
      let (i1, i2) = twinhd ins in [
        inport i1 "x";
        inport i2 "y";
        call_cand Neg (Var "x") (Var "y") (Var "r");
        outport (List.hd outs) "r" 
      ]
  | COr ->
      let (i1, i2) = twinhd ins in [
        inport i1 "x";
        inport i2 "y";
        call_cor Neg (Var "x") (Var "y") (Var "r");
        outport (List.hd outs) "r" 
      ]
 let const_of_circuit (circ : circuit) = List.map (star_of_gate circ) circ
 let prop_logic : constellation = [
  [call_cneg Pos (make_const "0") (make_const "1")];
  [call_cneg Pos (make_const "1") (make_const "0")];
  [call_cand Pos (make_const "0") (make_const "0") (make_const "0")];
  [call_cand Pos (make_const "0") (make_const "1") (make_const "0")];
  [call_cand Pos (make_const "1") (make_const "0") (make_const "0")];
  [call_cand Pos (make_const "1") (make_const "1") (make_const "1")];
  [call_cor Pos (make_const "0") (make_const "0") (make_const "0")];
  [call_cor Pos (make_const "0") (make_const "1") (make_const "1")];
  [call_cor Pos (make_const "1") (make_const "0") (make_const "1")];
  [call_cor Pos (make_const "1") (make_const "1") (make_const "1")]
 ]
--- a/ocaml/StellarFSA.ml
+++ b/ocaml/StellarFSA.ml
@ -1,15 +0,0 @@
 open Resolution
 open FSA
 (* ============================================
              Stellar Automata
   ============================================ *)
 let dot x y = Func ("·", Npol, [x; y])
 let const_of_word (w : char list) =
  let rec aux = function
    | [] -> Func ("", Npol, [])
    | c::w ->
        dot (Func (String.make 1 c, Npol, [])) (aux w)
  in [Func ("i", Pos, [aux w])]
--- a/ocaml/Unification.ml
+++ b/ocaml/Unification.ml
@ -1,92 +0,0 @@
 open List
 (* ========================================
     Definitions
   ======================================== *)
 type id = string
 type term = Var of id | Func of (id * term list)
 type subst = id * term list
 type equation = term * term
 (* convert a term to a string *)
 let rec term_to_string t =
   match t with
   | Var id -> id
   | Func(f, []) -> f
   | Func(f, tl) -> f ^ "(" ^
      let rec aux2 vl =
        match vl with
        | [] -> ""
        | h::[] -> term_to_string h
        | h::t -> (term_to_string h) ^ "," ^ (aux2 t) 
      in (aux2 tl) ^ ")"
 let print_term t =
  print_string (term_to_string t)
 (* Compare two terms *)
 let rec compare_term t1 t2 =
   match t1, t2 with
   | Var(id1), Var(id2) -> String.compare id1 id2
   | Var(_), Func(_,_) -> -1
   | Func(_,_), Var(_) -> 1
   | Func(f, fs), Func(g, gs) -> let comp = String.compare f g in if comp > 0 then 1 
   else if comp < 0 then -1 
   else List.compare compare_term fs gs
 (* Look if there's a var to be substituted in the term in the substitution environment *)
 let rec indom t sl = 
  match t with
  | Var id -> List.exists (fun (a,_) -> a = id ) sl
  | Func(_, tl) -> List.exists (fun a -> indom a sl) tl
 (* occurs checks if given var is in term *)
 let rec occurs id t =
  match t with
  | Var i -> i = id 
  | Func(_, tl) -> List.exists (fun a -> occurs id a) tl
 (* extends_varname adds suffix to all var names of a term *)
 let rec extends_varname t ext =
  match t with
  | Var id -> Var(id ^ ext)
  | Func(f, tl) -> Func(f, List.map (fun a -> extends_varname a ext) tl)
 (* vars gives a list of all vars in a term *)
 let rec vars t =
  match t with
  | Var id -> [id]
  | Func(_, tl) -> List.fold_left (fun a b -> (vars b)@a) [] tl
  (* ========================================
      Substitution
     ======================================== *)
 (* apply applies a substitution to a var *)
 let apply id sub = let (_,s) = try List.find (fun (a,_) -> a = id ) sub with Not_found -> (id,Var(id)) in s
 (* subst applies all possible substition from an environment to a term *)
 let rec substit trm sub =
  match trm with
  | Var id -> apply id sub
  | Func(f,tl) -> Func(f,List.map (fun a -> substit a sub) tl)  
  (* ========================================
      Unification
     ======================================== *)
 (* Solves an equation list by returning solution list *)
 let rec solve eq sub = 
  match eq with
  | [] -> Some sub
  | (Var(x), term)::t -> if Var(x) = term then (solve t sub) else (elim x term t sub) (* If x = x it's a useless equation *)
  | (term, Var(x))::t -> (elim x term t sub) (*It's useless to check if term = Var(x) because it would be the same case as above *)
  | (Func(f, fs), Func(g, gs))::t -> if f = g then (solve ((List.combine fs gs)@t) sub) else (*failwith (Printf.sprintf "f=%s g=%s" f g)*) None (* If f and g are not equal, the equation can't be solved *)
 and elim id term eq sub =
  if occurs id term then (*failwith (Printf.sprintf "id=%s is in term" id)*) None (* If that's the case, we would have something like x = f(x) which can't be solved *)
  else let sigma_xy = [(id, term)] in
  solve (List.map (fun (a,b) -> (substit a sigma_xy, substit b sigma_xy)) eq) ((List.map (fun (i, t) -> (i, substit t sigma_xy)) sub)@sigma_xy) (* We apply the sigma_xy substitution to the equations and the solution list and we add it to the solution list *)
--- a/ocaml/main.ml
+++ b/ocaml/main.ml
@ -1,49 +0,0 @@
 open Resolution
 open Circuits
 open StellarCircuits
  (* ========================================
      Tests
     ======================================== *)
 (* _________ Tests on Resolution _________ *)
 let y = Var("y")
 let x = Var("x")
 let z = Var("z")
 let r = Var("r")
 let zero = make_const "0"
 let s x = Func("s", Npol, [x])
 let add p x y z = Func("add", p, [x;y;z])
 (* Convert int to term *)
 let rec enat i = 
  if i = 0 then zero else s (enat (i-1))
 (* makes the constellation corresponding to an addition *)
 let make_const_add n m = 
  [[add Pos zero y y]; [add Neg x y z; add Pos (s x) y (s z)]; [add Neg (enat n) (enat m) r; r]] 
 let constellation = make_const_add 1 3 ;;
 print_dgraph (dgraph constellation) ;;
 (* simple determinist constellation test*)
 let test = [ [Func("e", Neg, [x]); x] ; [Func("e", Pos, [Func("d", Npol, [y])]) ; Func("e", Npol, [x]) ] ] ;;
 print_dgraph (dgraph test);;
 exec test ;;
 (* _________ Tests on exec using Stellar Circuits _________ *)
 (* Constellation of excluded middle without boolean doors *)
 let excl_mid_no_prop = (const_of_circuit (make_em_circ 1));;
 (* Constellation of excluded middle with boolean doors *)
 let excl_mid_prop = ((const_of_circuit (make_em_circ 1))@[[Func("or", Pos, [Func("0", Npol, []); Func("1", Npol, []); Func("1", Npol, [])])];[Func("neg",Pos, [Func("1", Npol, []); Func("0", Npol, [])])]]);;
 let exec_exmid_noprop = exec excl_mid_no_prop [0];;
 (* should return 1*)
 let exec_exmid_prop = exec excl_mid_prop [0];;
 print_const exec_exmid_prop;;
 let test_fam = excl_mid_prop@test
--- a/parser.ml
+++ b/parser.ml
@ -0,0 +1,666 @@
 module MenhirBasics = struct
  exception Error
  let _eRR =
    fun _s ->
      raise Error
  type token = 
    | VDASH
    | VAR of (
 # 5 "parser.mly"
       (string)
 # 16 "parser.ml"
  )
    | SYM of (
 # 6 "parser.mly"
       (string)
 # 21 "parser.ml"
  )
    | RIGHT_PAR
    | RIGHT_BRACK
    | RIGHT_BRACE
    | PLUS
    | MINUS
    | LEFT_PAR
    | LEFT_BRACK
    | LEFT_BRACE
    | DOT
    | COMMA
 end
 include MenhirBasics
 type ('s, 'r) _menhir_state = 
  | MenhirState00 : ('s, _menhir_box_constc) _menhir_state
    (** State 00.
        Stack shape : .
        Start symbol: constc. *)
  | MenhirState01 : (('s, 'r) _menhir_cell1_LEFT_BRACE, 'r) _menhir_state
    (** State 01.
        Stack shape : LEFT_BRACE.
        Start symbol: <undetermined>. *)
  | MenhirState02 : (('s, 'r) _menhir_cell1_LEFT_BRACK, 'r) _menhir_state
    (** State 02.
        Stack shape : LEFT_BRACK.
        Start symbol: <undetermined>. *)
  | MenhirState10 : (('s, 'r) _menhir_cell1_symc, 'r) _menhir_state
    (** State 10.
        Stack shape : symc.
        Start symbol: <undetermined>. *)
  | MenhirState14 : (('s, 'r) _menhir_cell1_rayc, 'r) _menhir_state
    (** State 14.
        Stack shape : rayc.
        Start symbol: <undetermined>. *)
  | MenhirState16 : (('s, 'r) _menhir_cell1_rayc, 'r) _menhir_state
    (** State 16.
        Stack shape : rayc.
        Start symbol: <undetermined>. *)
  | MenhirState22 : (('s, 'r) _menhir_cell1_starc, 'r) _menhir_state
    (** State 22.
        Stack shape : starc.
        Start symbol: <undetermined>. *)
  | MenhirState28 : ('s, _menhir_box_spacec) _menhir_state
    (** State 28.
        Stack shape : .
        Start symbol: spacec. *)
  | MenhirState29 : (('s, _menhir_box_spacec) _menhir_cell1_LEFT_BRACE, _menhir_box_spacec) _menhir_state
    (** State 29.
        Stack shape : LEFT_BRACE.
        Start symbol: spacec. *)
  | MenhirState34 : (('s, _menhir_box_spacec) _menhir_cell1_constc, _menhir_box_spacec) _menhir_state
    (** State 34.
        Stack shape : constc.
        Start symbol: spacec. *)
 and ('s, 'r) _menhir_cell1_constc = 
  | MenhirCell1_constc of 's * ('s, 'r) _menhir_state * (Stellar.constellation)
 and ('s, 'r) _menhir_cell1_rayc = 
  | MenhirCell1_rayc of 's * ('s, 'r) _menhir_state * (Stellar.StellarRays.term)
 and ('s, 'r) _menhir_cell1_starc = 
  | MenhirCell1_starc of 's * ('s, 'r) _menhir_state * (Stellar.star)
 and ('s, 'r) _menhir_cell1_symc = 
  | MenhirCell1_symc of 's * ('s, 'r) _menhir_state * (Stellar.StellarSig.idfunc)
 and ('s, 'r) _menhir_cell1_LEFT_BRACE = 
  | MenhirCell1_LEFT_BRACE of 's * ('s, 'r) _menhir_state
 and ('s, 'r) _menhir_cell1_LEFT_BRACK = 
  | MenhirCell1_LEFT_BRACK of 's * ('s, 'r) _menhir_state
 and _menhir_box_spacec = 
  | MenhirBox_spacec of (Stellar.constellation * Stellar.constellation) [@@unboxed]
 and _menhir_box_constc = 
  | MenhirBox_constc of (Stellar.constellation) [@@unboxed]
 let _menhir_action_02 =
  fun xs ->
    let cs = 
 # 229 "<standard.mly>"
    ( xs )
 # 119 "parser.ml"
     in
    (
 # 22 "parser.mly"
                                                            ( cs )
 # 124 "parser.ml"
     : (Stellar.constellation))
 let _menhir_action_03 =
  fun () ->
    (
 # 139 "<standard.mly>"
    ( [] )
 # 132 "parser.ml"
     : (Stellar.star))
 let _menhir_action_04 =
  fun x ->
    (
 # 141 "<standard.mly>"
    ( x )
 # 140 "parser.ml"
     : (Stellar.star))
 let _menhir_action_05 =
  fun () ->
    (
 # 139 "<standard.mly>"
    ( [] )
 # 148 "parser.ml"
     : (Stellar.constellation))
 let _menhir_action_06 =
  fun x ->
    (
 # 141 "<standard.mly>"
    ( x )
 # 156 "parser.ml"
     : (Stellar.constellation))
 let _menhir_action_07 =
  fun x ->
    (
 # 33 "parser.mly"
          ( Stellar.to_var x )
 # 164 "parser.ml"
     : (Stellar.StellarRays.term))
 let _menhir_action_08 =
  fun r1 r2 ->
    (
 # 34 "parser.mly"
                            ( Stellar.to_func ((Stellar.Null, "."), [r1; r2]) )
 # 172 "parser.ml"
     : (Stellar.StellarRays.term))
 let _menhir_action_09 =
  fun pf ts ->
    (
 # 36 "parser.mly"
 ( Stellar.to_func (pf, ts) )
 # 180 "parser.ml"
     : (Stellar.StellarRays.term))
 let _menhir_action_10 =
  fun pf ->
    (
 # 37 "parser.mly"
            ( Stellar.to_func (pf, []) )
 # 188 "parser.ml"
     : (Stellar.StellarRays.term))
 let _menhir_action_11 =
  fun x ->
    (
 # 238 "<standard.mly>"
    ( [ x ] )
 # 196 "parser.ml"
     : (Stellar.star))
 let _menhir_action_12 =
  fun x xs ->
    (
 # 240 "<standard.mly>"
    ( x :: xs )
 # 204 "parser.ml"
     : (Stellar.star))
 let _menhir_action_13 =
  fun x ->
    (
 # 238 "<standard.mly>"
    ( [ x ] )
 # 212 "parser.ml"
     : (Stellar.constellation))
 let _menhir_action_14 =
  fun x xs ->
    (
 # 240 "<standard.mly>"
    ( x :: xs )
 # 220 "parser.ml"
     : (Stellar.constellation))
 let _menhir_action_15 =
  fun cs space ->
    (
 # 19 "parser.mly"
                                     ( (cs, space) )
 # 228 "parser.ml"
     : (Stellar.constellation * Stellar.constellation))
 let _menhir_action_16 =
  fun xs ->
    let rs = 
 # 229 "<standard.mly>"
    ( xs )
 # 236 "parser.ml"
     in
    (
 # 25 "parser.mly"
                                                            ( rs )
 # 241 "parser.ml"
     : (Stellar.star))
 let _menhir_action_17 =
  fun f p ->
    (
 # 28 "parser.mly"
                    ( (Pos, f) )
 # 249 "parser.ml"
     : (Stellar.StellarSig.idfunc))
 let _menhir_action_18 =
  fun f p ->
    (
 # 29 "parser.mly"
                     ( (Neg, f) )
 # 257 "parser.ml"
     : (Stellar.StellarSig.idfunc))
 let _menhir_action_19 =
  fun f ->
    (
 # 30 "parser.mly"
          ( (Stellar.Null, f) )
 # 265 "parser.ml"
     : (Stellar.StellarSig.idfunc))
 let _menhir_print_token : token -> string =
  fun _tok ->
    match _tok with
    | COMMA ->
        "COMMA"
    | DOT ->
        "DOT"
    | LEFT_BRACE ->
        "LEFT_BRACE"
    | LEFT_BRACK ->
        "LEFT_BRACK"
    | LEFT_PAR ->
        "LEFT_PAR"
    | MINUS ->
        "MINUS"
    | PLUS ->
        "PLUS"
    | RIGHT_BRACE ->
        "RIGHT_BRACE"
    | RIGHT_BRACK ->
        "RIGHT_BRACK"
    | RIGHT_PAR ->
        "RIGHT_PAR"
    | SYM _ ->
        "SYM"
    | VAR _ ->
        "VAR"
    | VDASH ->
        "VDASH"
 let _menhir_fail : unit -> 'a =
  fun () ->
    Printf.eprintf "Internal failure -- please contact the parser generator's developers.\n%!";
    assert false
 include struct
  [@@@ocaml.warning "-4-37-39"]
  let rec _menhir_run_35 : type  ttv_stack. (ttv_stack, _menhir_box_spacec) _menhir_cell1_constc -> _ -> _menhir_box_spacec =
    fun _menhir_stack _v ->
      let MenhirCell1_constc (_menhir_stack, _, cs) = _menhir_stack in
      let space = _v in
      let _v = _menhir_action_15 cs space in
      MenhirBox_spacec _v
  let rec _menhir_run_27 : type  ttv_stack. ttv_stack -> _ -> _menhir_box_constc =
    fun _menhir_stack _v ->
      MenhirBox_constc _v
  let rec _menhir_run_01 : type  ttv_stack ttv_result. ttv_stack -> _ -> _ -> (ttv_stack, ttv_result) _menhir_state -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s ->
      let _menhir_stack = MenhirCell1_LEFT_BRACE (_menhir_stack, _menhir_s) in
      let _tok = _menhir_lexer _menhir_lexbuf in
      match (_tok : MenhirBasics.token) with
      | LEFT_BRACK ->
          _menhir_run_02 _menhir_stack _menhir_lexbuf _menhir_lexer MenhirState01
      | RIGHT_BRACE ->
          let _v = _menhir_action_05 () in
          _menhir_run_25 _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok
      | _ ->
          _eRR ()
  and _menhir_run_02 : type  ttv_stack ttv_result. ttv_stack -> _ -> _ -> (ttv_stack, ttv_result) _menhir_state -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s ->
      let _menhir_stack = MenhirCell1_LEFT_BRACK (_menhir_stack, _menhir_s) in
      let _menhir_s = MenhirState02 in
      let _tok = _menhir_lexer _menhir_lexbuf in
      match (_tok : MenhirBasics.token) with
      | VAR _v ->
          _menhir_run_03 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s
      | SYM _v ->
          _menhir_run_04 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s
      | PLUS ->
          _menhir_run_05 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s
      | MINUS ->
          _menhir_run_07 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s
      | RIGHT_BRACK ->
          let _v = _menhir_action_03 () in
          _menhir_goto_loption_separated_nonempty_list_COMMA_rayc__ _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok
      | _ ->
          _eRR ()
  and _menhir_run_03 : type  ttv_stack ttv_result. ttv_stack -> _ -> _ -> _ -> (ttv_stack, ttv_result) _menhir_state -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s ->
      let _tok = _menhir_lexer _menhir_lexbuf in
      let x = _v in
      let _v = _menhir_action_07 x in
      _menhir_goto_rayc _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
  and _menhir_goto_rayc : type  ttv_stack ttv_result. ttv_stack -> _ -> _ -> _ -> (ttv_stack, ttv_result) _menhir_state -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok ->
      match _menhir_s with
      | MenhirState14 ->
          _menhir_run_15 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
      | MenhirState02 ->
          _menhir_run_13 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
      | MenhirState16 ->
          _menhir_run_13 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
      | MenhirState10 ->
          _menhir_run_13 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
      | _ ->
          _menhir_fail ()
  and _menhir_run_15 : type  ttv_stack ttv_result. ((ttv_stack, ttv_result) _menhir_cell1_rayc as 'stack) -> _ -> _ -> _ -> ('stack, ttv_result) _menhir_state -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok ->
      match (_tok : MenhirBasics.token) with
      | DOT ->
          let _menhir_stack = MenhirCell1_rayc (_menhir_stack, _menhir_s, _v) in
          _menhir_run_14 _menhir_stack _menhir_lexbuf _menhir_lexer
      | COMMA | RIGHT_BRACK | RIGHT_PAR ->
          let MenhirCell1_rayc (_menhir_stack, _menhir_s, r1) = _menhir_stack in
          let r2 = _v in
          let _v = _menhir_action_08 r1 r2 in
          _menhir_goto_rayc _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
      | _ ->
          _eRR ()
  and _menhir_run_14 : type  ttv_stack ttv_result. (ttv_stack, ttv_result) _menhir_cell1_rayc -> _ -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer ->
      let _menhir_s = MenhirState14 in
      let _tok = _menhir_lexer _menhir_lexbuf in
      match (_tok : MenhirBasics.token) with
      | VAR _v ->
          _menhir_run_03 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s
      | SYM _v ->
          _menhir_run_04 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s
      | PLUS ->
          _menhir_run_05 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s
      | MINUS ->
          _menhir_run_07 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s
      | _ ->
          _eRR ()
  and _menhir_run_04 : type  ttv_stack ttv_result. ttv_stack -> _ -> _ -> _ -> (ttv_stack, ttv_result) _menhir_state -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s ->
      let _tok = _menhir_lexer _menhir_lexbuf in
      let f = _v in
      let _v = _menhir_action_19 f in
      _menhir_goto_symc _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
  and _menhir_goto_symc : type  ttv_stack ttv_result. ttv_stack -> _ -> _ -> _ -> (ttv_stack, ttv_result) _menhir_state -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok ->
      match (_tok : MenhirBasics.token) with
      | LEFT_PAR ->
          let _menhir_stack = MenhirCell1_symc (_menhir_stack, _menhir_s, _v) in
          let _menhir_s = MenhirState10 in
          let _tok = _menhir_lexer _menhir_lexbuf in
          (match (_tok : MenhirBasics.token) with
          | VAR _v ->
              _menhir_run_03 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s
          | SYM _v ->
              _menhir_run_04 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s
          | PLUS ->
              _menhir_run_05 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s
          | MINUS ->
              _menhir_run_07 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s
          | _ ->
              _eRR ())
      | COMMA | DOT | RIGHT_BRACK | RIGHT_PAR ->
          let pf = _v in
          let _v = _menhir_action_10 pf in
          _menhir_goto_rayc _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
      | _ ->
          _eRR ()
  and _menhir_run_05 : type  ttv_stack ttv_result. ttv_stack -> _ -> _ -> (ttv_stack, ttv_result) _menhir_state -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s ->
      let _tok = _menhir_lexer _menhir_lexbuf in
      match (_tok : MenhirBasics.token) with
      | SYM _v ->
          let _tok = _menhir_lexer _menhir_lexbuf in
          let (f, p) = (_v, ()) in
          let _v = _menhir_action_17 f p in
          _menhir_goto_symc _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
      | _ ->
          _eRR ()
  and _menhir_run_07 : type  ttv_stack ttv_result. ttv_stack -> _ -> _ -> (ttv_stack, ttv_result) _menhir_state -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s ->
      let _tok = _menhir_lexer _menhir_lexbuf in
      match (_tok : MenhirBasics.token) with
      | SYM _v ->
          let _tok = _menhir_lexer _menhir_lexbuf in
          let (f, p) = (_v, ()) in
          let _v = _menhir_action_18 f p in
          _menhir_goto_symc _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
      | _ ->
          _eRR ()
  and _menhir_run_13 : type  ttv_stack ttv_result. ttv_stack -> _ -> _ -> _ -> (ttv_stack, ttv_result) _menhir_state -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok ->
      match (_tok : MenhirBasics.token) with
      | DOT ->
          let _menhir_stack = MenhirCell1_rayc (_menhir_stack, _menhir_s, _v) in
          _menhir_run_14 _menhir_stack _menhir_lexbuf _menhir_lexer
      | COMMA ->
          let _menhir_stack = MenhirCell1_rayc (_menhir_stack, _menhir_s, _v) in
          let _menhir_s = MenhirState16 in
          let _tok = _menhir_lexer _menhir_lexbuf in
          (match (_tok : MenhirBasics.token) with
          | VAR _v ->
              _menhir_run_03 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s
          | SYM _v ->
              _menhir_run_04 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s
          | PLUS ->
              _menhir_run_05 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s
          | MINUS ->
              _menhir_run_07 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s
          | _ ->
              _eRR ())
      | RIGHT_BRACK | RIGHT_PAR ->
          let x = _v in
          let _v = _menhir_action_11 x in
          _menhir_goto_separated_nonempty_list_COMMA_rayc_ _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
      | _ ->
          _eRR ()
  and _menhir_goto_separated_nonempty_list_COMMA_rayc_ : type  ttv_stack ttv_result. ttv_stack -> _ -> _ -> _ -> (ttv_stack, ttv_result) _menhir_state -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok ->
      match _menhir_s with
      | MenhirState02 ->
          _menhir_run_18 _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok
      | MenhirState16 ->
          _menhir_run_17 _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok
      | MenhirState10 ->
          _menhir_run_11 _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok
      | _ ->
          _menhir_fail ()
  and _menhir_run_18 : type  ttv_stack ttv_result. (ttv_stack, ttv_result) _menhir_cell1_LEFT_BRACK -> _ -> _ -> _ -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok ->
      let x = _v in
      let _v = _menhir_action_04 x in
      _menhir_goto_loption_separated_nonempty_list_COMMA_rayc__ _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok
  and _menhir_goto_loption_separated_nonempty_list_COMMA_rayc__ : type  ttv_stack ttv_result. (ttv_stack, ttv_result) _menhir_cell1_LEFT_BRACK -> _ -> _ -> _ -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok ->
      match (_tok : MenhirBasics.token) with
      | RIGHT_BRACK ->
          let _tok = _menhir_lexer _menhir_lexbuf in
          let MenhirCell1_LEFT_BRACK (_menhir_stack, _menhir_s) = _menhir_stack in
          let xs = _v in
          let _v = _menhir_action_16 xs in
          (match (_tok : MenhirBasics.token) with
          | PLUS ->
              let _menhir_stack = MenhirCell1_starc (_menhir_stack, _menhir_s, _v) in
              let _menhir_s = MenhirState22 in
              let _tok = _menhir_lexer _menhir_lexbuf in
              (match (_tok : MenhirBasics.token) with
              | LEFT_BRACK ->
                  _menhir_run_02 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s
              | _ ->
                  _eRR ())
          | RIGHT_BRACE ->
              let x = _v in
              let _v = _menhir_action_13 x in
              _menhir_goto_separated_nonempty_list_PLUS_starc_ _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
          | _ ->
              _eRR ())
      | _ ->
          _eRR ()
  and _menhir_goto_separated_nonempty_list_PLUS_starc_ : type  ttv_stack ttv_result. ttv_stack -> _ -> _ -> _ -> (ttv_stack, ttv_result) _menhir_state -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok ->
      match _menhir_s with
      | MenhirState29 ->
          _menhir_run_24 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
      | MenhirState01 ->
          _menhir_run_24 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
      | MenhirState22 ->
          _menhir_run_23 _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok
      | _ ->
          _menhir_fail ()
  and _menhir_run_24 : type  ttv_stack ttv_result. ((ttv_stack, ttv_result) _menhir_cell1_LEFT_BRACE as 'stack) -> _ -> _ -> _ -> ('stack, ttv_result) _menhir_state -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok ->
      let x = _v in
      let _v = _menhir_action_06 x in
      _menhir_goto_loption_separated_nonempty_list_PLUS_starc__ _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
  and _menhir_goto_loption_separated_nonempty_list_PLUS_starc__ : type  ttv_stack ttv_result. ((ttv_stack, ttv_result) _menhir_cell1_LEFT_BRACE as 'stack) -> _ -> _ -> _ -> ('stack, ttv_result) _menhir_state -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok ->
      match _menhir_s with
      | MenhirState29 ->
          _menhir_run_30 _menhir_stack _menhir_lexbuf _menhir_lexer _v
      | MenhirState01 ->
          _menhir_run_25 _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok
      | _ ->
          _menhir_fail ()
  and _menhir_run_30 : type  ttv_stack. (ttv_stack, _menhir_box_spacec) _menhir_cell1_LEFT_BRACE -> _ -> _ -> _ -> _menhir_box_spacec =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v ->
      let _tok = _menhir_lexer _menhir_lexbuf in
      let MenhirCell1_LEFT_BRACE (_menhir_stack, _menhir_s) = _menhir_stack in
      let xs = _v in
      let _v = _menhir_action_02 xs in
      _menhir_goto_constc _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
  and _menhir_goto_constc : type  ttv_stack ttv_result. ttv_stack -> _ -> _ -> _ -> (ttv_stack, ttv_result) _menhir_state -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok ->
      match _menhir_s with
      | MenhirState34 ->
          _menhir_run_35 _menhir_stack _v
      | MenhirState28 ->
          _menhir_run_33 _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
      | MenhirState00 ->
          _menhir_run_27 _menhir_stack _v
      | _ ->
          _menhir_fail ()
  and _menhir_run_33 : type  ttv_stack. ttv_stack -> _ -> _ -> _ -> (ttv_stack, _menhir_box_spacec) _menhir_state -> _ -> _menhir_box_spacec =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok ->
      let _menhir_stack = MenhirCell1_constc (_menhir_stack, _menhir_s, _v) in
      match (_tok : MenhirBasics.token) with
      | VDASH ->
          let _menhir_s = MenhirState34 in
          let _tok = _menhir_lexer _menhir_lexbuf in
          (match (_tok : MenhirBasics.token) with
          | LEFT_BRACE ->
              _menhir_run_01 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s
          | _ ->
              _eRR ())
      | _ ->
          _eRR ()
  and _menhir_run_25 : type  ttv_stack ttv_result. (ttv_stack, ttv_result) _menhir_cell1_LEFT_BRACE -> _ -> _ -> _ -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok ->
      let MenhirCell1_LEFT_BRACE (_menhir_stack, _menhir_s) = _menhir_stack in
      let xs = _v in
      let _v = _menhir_action_02 xs in
      _menhir_goto_constc _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
  and _menhir_run_23 : type  ttv_stack ttv_result. (ttv_stack, ttv_result) _menhir_cell1_starc -> _ -> _ -> _ -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok ->
      let MenhirCell1_starc (_menhir_stack, _menhir_s, x) = _menhir_stack in
      let xs = _v in
      let _v = _menhir_action_14 x xs in
      _menhir_goto_separated_nonempty_list_PLUS_starc_ _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
  and _menhir_run_17 : type  ttv_stack ttv_result. (ttv_stack, ttv_result) _menhir_cell1_rayc -> _ -> _ -> _ -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok ->
      let MenhirCell1_rayc (_menhir_stack, _menhir_s, x) = _menhir_stack in
      let xs = _v in
      let _v = _menhir_action_12 x xs in
      _menhir_goto_separated_nonempty_list_COMMA_rayc_ _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
  and _menhir_run_11 : type  ttv_stack ttv_result. (ttv_stack, ttv_result) _menhir_cell1_symc -> _ -> _ -> _ -> _ -> ttv_result =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer _v _tok ->
      match (_tok : MenhirBasics.token) with
      | RIGHT_PAR ->
          let _tok = _menhir_lexer _menhir_lexbuf in
          let MenhirCell1_symc (_menhir_stack, _menhir_s, pf) = _menhir_stack in
          let ts = _v in
          let _v = _menhir_action_09 pf ts in
          _menhir_goto_rayc _menhir_stack _menhir_lexbuf _menhir_lexer _v _menhir_s _tok
      | _ ->
          _eRR ()
  let rec _menhir_run_00 : type  ttv_stack. ttv_stack -> _ -> _ -> _menhir_box_constc =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer ->
      let _menhir_s = MenhirState00 in
      let _tok = _menhir_lexer _menhir_lexbuf in
      match (_tok : MenhirBasics.token) with
      | LEFT_BRACE ->
          _menhir_run_01 _menhir_stack _menhir_lexbuf _menhir_lexer _menhir_s
      | _ ->
          _eRR ()
  let rec _menhir_run_28 : type  ttv_stack. ttv_stack -> _ -> _ -> _menhir_box_spacec =
    fun _menhir_stack _menhir_lexbuf _menhir_lexer ->
      let _tok = _menhir_lexer _menhir_lexbuf in
      match (_tok : MenhirBasics.token) with
      | LEFT_BRACE ->
          let _menhir_stack = MenhirCell1_LEFT_BRACE (_menhir_stack, MenhirState28) in
          let _tok = _menhir_lexer _menhir_lexbuf in
          (match (_tok : MenhirBasics.token) with
          | LEFT_BRACK ->
              _menhir_run_02 _menhir_stack _menhir_lexbuf _menhir_lexer MenhirState29
          | RIGHT_BRACE ->
              let _v = _menhir_action_05 () in
              _menhir_run_30 _menhir_stack _menhir_lexbuf _menhir_lexer _v
          | _ ->
              _eRR ())
      | _ ->
          _eRR ()
 end
 let spacec =
  fun _menhir_lexer _menhir_lexbuf ->
    let _menhir_stack = () in
    let MenhirBox_spacec v = _menhir_run_28 _menhir_stack _menhir_lexbuf _menhir_lexer in
    v
 let constc =
  fun _menhir_lexer _menhir_lexbuf ->
    let _menhir_stack = () in
    let MenhirBox_constc v = _menhir_run_00 _menhir_stack _menhir_lexbuf _menhir_lexer in
    v
--- a/parser.mli
+++ b/parser.mli
@ -0,0 +1,27 @@
 (* The type of tokens. *)
 type token = 
  | VDASH
  | VAR of (string)
  | SYM of (string)
  | RIGHT_PAR
  | RIGHT_BRACK
  | RIGHT_BRACE
  | PLUS
  | MINUS
  | LEFT_PAR
  | LEFT_BRACK
  | LEFT_BRACE
  | DOT
  | COMMA
 (* This exception is raised by the monolithic API functions. *)
 exception Error
 (* The monolithic API. *)
 val spacec: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Stellar.constellation * Stellar.constellation)
 val constc: (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (Stellar.constellation)
--- a/parser.mly
+++ b/parser.mly
@ -0,0 +1,37 @@
 %token COMMA
 %token LEFT_BRACK RIGHT_BRACK
 %token LEFT_PAR RIGHT_PAR
 %token LEFT_BRACE RIGHT_BRACE
 %token <string> VAR
 %token <string> SYM
 %token PLUS MINUS
 %token DOT
 %token VDASH
 %right DOT
 %start <Stellar.constellation * Stellar.constellation> spacec
 %start <Stellar.constellation> constc
 %%
 spacec:
 | cs = constc; VDASH; space = constc { (cs, space) }
 constc:
 | LEFT_BRACE; cs = separated_list(PLUS, starc); RIGHT_BRACE { cs }
 starc:
 | LEFT_BRACK; rs = separated_list(COMMA, rayc); RIGHT_BRACK { rs }
 symc:
 | p = PLUS; f = SYM { (Pos, f) }
 | p = MINUS; f = SYM { (Neg, f) }
 | f = SYM { (Stellar.Null, f) }
 rayc:
 | x = VAR { Stellar.to_var x }
 | r1 = rayc; DOT; r2 = rayc { Stellar.to_func ((Stellar.Null, "."), [r1; r2]) }
 | pf = symc; LEFT_PAR; ts = separated_nonempty_list(COMMA, rayc); RIGHT_PAR
 	{ Stellar.to_func (pf, ts) }
 | pf = symc { Stellar.to_func (pf, []) }
--- a/prolog.stellar
+++ b/prolog.stellar
@ -0,0 +1,8 @@
 {
 	[+add(0, Y, Y)] +
 	[-add(X, Y, Z), +add(s(X), Y, s(Z))]
 }
 |-
 {
 	[-add(s(s(0)), s(s(0)), R), R]
 } 
--- a/stellar.ml
+++ b/stellar.ml
@ -0,0 +1,123 @@
 type polarity = Pos | Neg | Null
 let string_of_polarity = function
 	| Pos -> "+"
 	| Neg -> "-"
 	| Null -> ""
 let string_of_polsym (p, f) = (string_of_polarity p) ^ f
 module StellarSig = struct
 	type idvar = string
 	type idfunc = polarity * string
 	let concat = (^)
 	let compatible f g =
 		match f, g with
 		| (Pos, f), (Neg, g)
 		| (Neg, f), (Pos, g) when f = g -> true
 		| (Null, f), (Null, g) when f = g -> true
 		| _ -> false
 	let string_of_idfunc = string_of_polsym
 end
 module StellarRays = Unification.Make(StellarSig)
 open StellarSig
 open StellarRays
 open Tools
 (* ---------------------------------------
   Stars and Constellations
   --------------------------------------- *)
 type ray = term
 type star = ray list
 type constellation = star list
 let to_var x = Var x
 let to_func (pf, ts) = Func (pf, ts)
 let pos f = (Pos, f)
 let neg f = (Neg, f)
 let null f = (Null, f)
 let pfunc f ts = Func (pos f, ts)
 let nfunc f ts = Func (neg f, ts)
 let func f ts = Func (null f, ts)
 let var x = Var x
 let pconst f = pfunc f []
 let nconst f = nfunc f []
 let const f = func f []
 let rec is_polarised r : bool =
 	let aux = (function
 		| (Pos, _) | (Neg, _) -> true
 		| (Null, _) -> false)
 	in exists_term_func aux r
 (* ---------------------------------------
   Display
   --------------------------------------- *)
 let rec string_of_list printer sep = function
 	| [] -> ""
 	| [x] -> printer x
 	| h::t ->
 		(printer h) ^ sep ^ (string_of_list printer sep t)
 let rec string_of_ray = function
 	| Var x -> x
 	| Func (pf, []) -> string_of_polsym pf
 	| Func ((Null, "."), [r1; r2]) ->
 		(string_of_ray r1) ^ " · " ^ (string_of_ray r2)
 	| Func (pf, ts) -> string_of_polsym pf ^
 		"(" ^ (string_of_list string_of_ray ", " ts) ^ ")"
 let string_of_subst sub =
 	"{" ^ 
 	(List.fold_left (
 		fun acc (x, r) -> x ^ "->" ^ (string_of_ray r)
 	) "" sub) ^
 	"}"
 let string_of_star s = "[" ^ (string_of_list string_of_ray ", " s) ^ "]"
 let string_of_constellation cs =
 	if cs = [] then "{}" else string_of_list string_of_star " + " cs
 let string_of_intspace (cs, space) =
 	(string_of_constellation cs) ^ " |- " ^ (string_of_constellation space)
 (* ---------------------------------------
   Interactive execution
   --------------------------------------- *)
 let raymatcher ?(withloops=true) r r' : substitution option =
 	if is_polarised r && is_polarised r' then
 		solution ~withloops [(r, r')]
 	else
 		None
 let interaction ?(withloops=true) (s : star) i j (cs : constellation) : constellation = 
 	cs >>= fun i' s' ->
 	let s = List.map (extends_vars i) s in
 	let s' = List.map (extends_vars i') s' in
 	s' >>= fun j' r' ->
 	match raymatcher ~withloops (List.nth s j) r' with
 	| None -> []
 	| Some sub ->
 		let s1 = without j s in
 		let s2 = without j' s' in
 		return (List.map (subst sub) (s1@s2))
 let intspace ?(withloops=true) cs space : constellation =
 	List.flatten (
 		space >>= fun i s ->
 		s >>= fun j _ ->
 		return (interaction ~withloops s i j (cs@space))
 	)
 let rec intexec ?(withloops=true) (cs, space) : constellation =
 	let result = intspace ~withloops cs space in
 	if result = [] then space
 	else intexec ~withloops (cs, result)
--- a/tools.ml
+++ b/tools.ml
@ -0,0 +1,21 @@
 (* ---------------------------------------
   Few useful functions
   --------------------------------------- *)
 let lift_pairl f (x, y) = (f x, y)
 let lift_pairr f (x, y) = (x, f y)
 let lift_pair f p = lift_pairr f (lift_pairl f p)
 let rec repeat_string s n = if n=0 then "" else s ^ repeat_string s (n-1)
 let foldi_left f acc l =
 	snd (List.fold_left (fun (i, acc') x -> (i+1, f i acc' x)) (0, acc) l)
 let without i l = foldi_left (fun j acc x -> if i=j then acc else acc@[x]) [] l
 (* ---------------------------------------
   List monad (with index)
   --------------------------------------- *)
 let return x = [x]
 let (>>=) l f = List.flatten (List.mapi f l)
--- a/unification.ml
+++ b/unification.ml
@ -0,0 +1,85 @@
 open Tools
 module type Signature = sig
 	type idvar
 	type idfunc
 	val concat : idvar -> string -> idvar
 	val compatible : idfunc -> idfunc -> bool
 	val string_of_idfunc : idfunc -> string
 end
 (* ---------------------------------------
   Elementary definitions
   --------------------------------------- *)
 module Make (Sig : Signature) = struct
 type term =
 	| Var of Sig.idvar
 	| Func of (Sig.idfunc * term list)
 type substitution = (Sig.idvar * term) list
 type equation = term * term
 type problem = equation list
 let rec fold_term fnode fbase acc = function
 	| Var x -> fbase x acc
 	| Func (f, ts) ->
 		let acc' = fnode f acc in
 		List.fold_left (fold_term fnode fbase) acc' ts
 let rec map_term fnode fbase = function
 	| Var x -> fbase x
 	| Func (g, ts) ->
 		Func (fnode g, List.map (map_term fnode fbase) ts)
 let skip = fun _ acc -> acc
 let exists_term_vars p t = fold_term skip (fun y acc -> p y || acc) false t
 let all_term_vars p t = fold_term skip (fun y acc -> p y && acc) true t
 let exists_term_func p t = fold_term (fun y acc -> p y || acc) skip false t
 let all_term_func p t = fold_term (fun y acc -> p y && acc) skip true t
 let occurs x t = exists_term_vars (fun y -> x=y) t
 let extends_vars (i : int) =
 	map_term (fun x -> x) (fun x -> Var (Sig.concat x (string_of_int i)))
 let vars t = fold_term skip List.cons [] t
 let apply sub x = try List.assoc x sub with Not_found -> Var x  
 let rec subst sub = map_term (fun x -> x) (apply sub) 
 (* ---------------------------------------
   Unification algorithm
   --------------------------------------- *)
 let rec solve ?(withloops=true) sub : problem -> substitution option = function
  | [] -> Some sub
  (* Clear *)
  | (Var x, Var y)::pbs when x = y ->
 	if withloops then solve ~withloops sub pbs else None
  (* Orient + Replace *)
  | (Var x, t)::pbs | (t, Var x)::pbs -> elim ~withloops x t pbs sub
  (* Open *)
  | (Func (f, ts), Func (g, us))::pbs when Sig.compatible f g ->
 	begin try solve ~withloops sub ((List.combine ts us)@pbs)
 	with Invalid_argument _ ->
 		failwith (
 			"Unification error on symbols " ^
 			(Sig.string_of_idfunc f) ^
 			" and " ^
 			(Sig.string_of_idfunc g))
 	end
  | _ -> None
 (* Replace *)
 and elim ?(withloops=true) x t pbs sub : substitution option =
  if occurs x t then None (* Circularity *)
  else
 	let new_prob = List.map (lift_pair (subst [(x, t)])) pbs in
 	let new_sub = (x, t) :: List.map (lift_pairr (subst [(x, t)])) sub in
 	solve ~withloops new_sub new_prob
 let solution ?(withloops=true) : problem -> substitution option = solve ~withloops []
 end
		`@ -0,0 +1,2 @@`
							`### Starting build.`
							`# Compilation unsuccessful.`