From c30c61acb09a859820d36d3d053163622e86d9f8 Mon Sep 17 00:00:00 2001
From: engboris <eng@lipn.univ-paris13.fr>
Date: Wed, 2 Mar 2022 17:52:33 +0100
Subject: [PATCH] Initial commit

---
 ArithmeticsPL.hs |  39 +++++++
 Main.hs          |   9 ++
 PrettyPrinter.hs |  21 ++++
 Resolution.hs    | 260 +++++++++++++++++++++++++++++++++++++++++++++++
 Unification.hs   |  94 +++++++++++++++++
 5 files changed, 423 insertions(+)
 create mode 100644 ArithmeticsPL.hs
 create mode 100644 Main.hs
 create mode 100644 PrettyPrinter.hs
 create mode 100644 Resolution.hs
 create mode 100644 Unification.hs

diff --git a/ArithmeticsPL.hs b/ArithmeticsPL.hs
new file mode 100644
index 0000000..f1e2bb9
--- /dev/null
+++ b/ArithmeticsPL.hs
@@ -0,0 +1,39 @@
+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")]]
diff --git a/Main.hs b/Main.hs
new file mode 100644
index 0000000..8980973
--- /dev/null
+++ b/Main.hs
@@ -0,0 +1,9 @@
+module Main where
+import Unification
+import Resolution
+import Data.Maybe
+import ArithmeticsPL
+import qualified Data.Set as Set
+
+main = do
+    return ()
diff --git a/PrettyPrinter.hs b/PrettyPrinter.hs
new file mode 100644
index 0000000..3cd5532
--- /dev/null
+++ b/PrettyPrinter.hs
@@ -0,0 +1,21 @@
+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 ' ')
diff --git a/Resolution.hs b/Resolution.hs
new file mode 100644
index 0000000..1352cf0
--- /dev/null
+++ b/Resolution.hs
@@ -0,0 +1,260 @@
+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)
diff --git a/Unification.hs b/Unification.hs
new file mode 100644
index 0000000..b386593
--- /dev/null
+++ b/Unification.hs
@@ -0,0 +1,94 @@
+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]