Rename type 'Args' -> 'Tuple'

src/Analysis/TypeInferrer.hs

@@ -63,7 +63,7 @@ class HasSubstitution a where
 instance HasSubstitution Type where
   substitution t i (Variable' j) | i == j = t
   substitution t i (t0 :->:  t1) = substitution t i t0 :->: substitution t i t1
-  substitution t i (Args     ts) = Args $ map (substitution t i) ts
+  substitution t i (Tuple    ts) = Tuple $ map (substitution t i) ts
   substitution _ _ t             = t
 
 instance HasSubstitution Constraint where
@@ -185,7 +185,7 @@ annotatePattern (Variable x _) =
 annotatePattern (List    ps _) =
   do ts  <- mapM annotatePattern ps
      let ps' = map strengthenToPattern ts
-     let tau = Args $ map annotation ps'
+     let tau = Tuple $ map annotation ps'
      return $ Pattern $ List ps' tau
 annotatePattern (PConstructor c ps _) =
   do env <- environment
@@ -217,7 +217,7 @@ solve (constraint : rest) =
     Integer'      :=: Integer'      -> solve rest
     Boolean'      :=: Boolean'      -> solve rest
     (t0 :->: t1)  :=: (t2 :->: t3)  -> solve $ (t0 :=: t2) : (t1 :=: t3) : rest
-    (Args    ts)  :=: (Args    ss)  -> solve $ zipWith (:=:) ts ss ++ rest
+    (Tuple   ts)  :=: (Tuple   ss)  -> solve $ zipWith (:=:) ts ss ++ rest
     (ADT     x1)  :=: (ADT     x2)  ->
       if   x1 /= x2
       then Left $ typeError (ADT x1) (ADT x2)
@@ -247,7 +247,7 @@ refine _              Integer'               = Integer'
 refine _              Boolean'               = Boolean'
 refine s              (tau0 :->: tau1)       = refine s tau0 :->: refine s tau1
 refine _              (ADT name)             = ADT name
-refine s              (Args ts)              = Args $ map (refine s) ts
+refine s              (Tuple ts)             = Tuple $ map (refine s) ts
 
 
 -- Lifting (binding) variables
@@ -268,7 +268,7 @@ liftPattern (PConstructor c ps _, tau) =
 liftPattern (List ps _, tau) =
   do xs <- replicateM (length ps) fresh
      (ps', bs) <- foldrM liftMany ([], id) (zip ps xs)
-     tell [tau :=: Args xs]
+     tell [tau :=: Tuple xs]
      return (List ps' tau, bs)
 
 liftMany :: (Pattern a, Type) -> ([Pattern Type], Bindings -> Bindings)
@@ -294,7 +294,7 @@ alpha i t =
     increment :: Type -> Type
     increment (Variable'    j) = Variable' (i + j)
     increment (tau1 :->: tau2) = increment tau1 :->: increment tau2
-    increment (Args        ts) = Args $ map increment ts
+    increment (Tuple       ts) = Tuple $ map increment ts
     increment t'               = t'
 
 alphaADT :: Index -> [Constructor] -> (Index, [Constructor])
@@ -310,7 +310,7 @@ alphaDef i (Constructor c cs) = second (Constructor c)
 indices :: Type -> [Index]
 indices (Variable' i) = return i
 indices (t0  :->: t1) = indices t0 ++ indices t1
-indices (Args     ts) = concatMap indices ts
+indices (Tuple    ts) = concatMap indices ts
 indices _             = mempty
 
 returnType :: Type -> Type

src/Core/Syntax.hs

@@ -40,7 +40,7 @@ data Type =
   | Variable' Index
   | Type :->: Type
   | ADT  T
-  | Args [Type] -- Only used internally
+  | Tuple [Type] -- Only used internally
 
 data Constructor = Constructor C [Type]
 
@@ -191,7 +191,7 @@ equivalent Integer'     Integer'       = True
 equivalent Boolean'     Boolean'       = True
 equivalent (t0 :->: t1) (t0' :->: t1') = t0 == t0' && t1 == t1'
 equivalent (ADT      t) (ADT        s) = t == s
-equivalent (Args    ts) (Args      ss) = and $ zipWith (==) ts ss 
+equivalent (Tuple   ts) (Tuple     ss) = and $ zipWith (==) ts ss 
 equivalent _            _              = False
 
 instance Eq Constructor where
@@ -350,7 +350,7 @@ instance Show Type where
   show (Variable' i) = "V" ++ show i
   show (t0  :->: t1) = show t0 ++ " -> " ++ show t1
   show (ADT       t) = t
-  show (Args     ts) = "[" ++ intercalate ", " (map show ts) ++ "]"
+  show (Tuple     ts) = "[" ++ intercalate ", " (map show ts) ++ "]"
 
 instance Show Constructor where
   show (Constructor c []) = show c
@@ -391,7 +391,8 @@ instance Show (Value a) where
 
 -- "Direct" AST printing
 -- This is mostly here to ask the parser to write the AST for us,
--- so we can write normal programs instead of ASTs by hand to use in our tests
+-- so that for testing, we can write normal programs instead of
+-- writing ASTs by hand
 programAST :: Program Type -> String
 programAST (Signature x t rest) = "(Signature " ++ show x ++ " " ++ typeAST t
                                   ++ " " ++ programAST rest ++ ")"
@@ -478,4 +479,4 @@ typeAST Boolean'      = "Boolean'"
 typeAST (Variable' i) = "(Variable' " ++ show i ++ ")"
 typeAST (t0 :->:  t1) = "(" ++ typeAST t0 ++ " :->: " ++ typeAST t1 ++ ")"
 typeAST (ADT       t) = "(ADT " ++ t ++ ")"
-typeAST (Args     ts) = "(Args [" ++ intercalate ", " (map typeAST ts) ++ "])"
+typeAST (Tuple    ts) = "(Tuple [" ++ intercalate ", " (map typeAST ts) ++ "])"

src/Validation/Formula.hs

@@ -66,6 +66,7 @@ mergeList sb xs ys
 bind :: X -> SValue -> X `MapsTo` SValue
 bind x tau look y = if x == y then tau else look y
 
+-- TODO: Rename, maybe 'goSymbolic'?
 fresh :: X -> Type -> Formula SValue
 fresh _ Unit'    = return SUnit
 fresh x Integer' =
@@ -77,8 +78,11 @@ fresh x Boolean' =
 fresh x (Variable' _) =
   do sx <- liftSymbolic $ free x
      return $ SNumber sx
-fresh x (Args ts) = undefined
+fresh x (Tuple ts) = undefined
+-- Empty: SymTuple ()
+-- Nested SymTuples
 fresh x (t1 :->: t2) = undefined
+-- You have the name of the function and the program env
 fresh x (ADT t) = undefined
 --   do env <- environment
 -- To generate a fresh ADT variable, you could maybe generate a list of possible constructors + their args