translate records (wip)

src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs

@@ -283,6 +283,9 @@ goModule onlyTypes infoTable Internal.Module {..} =
             _ -> overNameText quote name
         Nothing -> overNameText quote name
 
+    getArgtys :: Internal.ConstructorInfo -> [Internal.FunctionParameter]
+    getArgtys ctrInfo = fst $ Internal.unfoldFunType $ ctrInfo ^. Internal.constructorInfoType
+
     goFunName :: Name -> Name
     goFunName name =
       case HashMap.lookup name (infoTable ^. Internal.infoFunctions) of
@@ -309,6 +312,11 @@ goModule onlyTypes infoTable Internal.Module {..} =
     withLocalNames nset nmap =
       local (const nset) . local (const nmap)
 
+    goRecordFields :: [Internal.FunctionParameter] -> [a] -> [(Name, a)]
+    goRecordFields argtys args = case (argtys, args) of
+      (ty : argtys', arg' : args') -> (fromMaybe (defaultName "_") (ty ^. Internal.paramName), arg') : goRecordFields argtys' args'
+      _ -> []
+
     goExpression' :: Internal.Expression -> Expression
     goExpression' = goExpression'' (NameSet mempty) (NameMap mempty)
 
@@ -381,6 +389,9 @@ goModule onlyTypes infoTable Internal.Module {..} =
               x' <- goExpression x
               y' <- goExpression y
               return $ ExprTuple (Tuple (x' :| [y']))
+          | Just fields <- getRecordCreation app = do
+              fields' <- mapM (secondM goExpression) fields
+              return $ ExprRecord (Record fields')
           | Just (fn, args) <- getIdentApp app = do
               fn' <- goExpression fn
               args' <- mapM goExpression args
@@ -535,6 +546,17 @@ goModule onlyTypes infoTable Internal.Module {..} =
           where
             (fn, args) = Internal.unfoldApplication app
 
+        getRecordCreation :: Internal.Application -> Maybe [(Name, Internal.Expression)]
+        getRecordCreation app = case fn of
+          Internal.ExpressionIden (Internal.IdenConstructor name) ->
+            case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
+              Just ctrInfo
+                | ctrInfo ^. Internal.constructorInfoRecord -> Just (goRecordFields (getArgtys ctrInfo) (toList args))
+              _ -> Nothing
+          _ -> Nothing
+          where
+            (fn, args) = Internal.unfoldApplication app
+
         getIdentApp :: Internal.Application -> Maybe (Internal.Expression, [Internal.Expression])
         getIdentApp app = case mty of
           Just (ty, paramsNum) -> Just (fn, args')
@@ -574,7 +596,6 @@ goModule onlyTypes infoTable Internal.Module {..} =
         goInstanceHole :: Internal.InstanceHole -> Sem r Expression
         goInstanceHole _ = return ExprUndefined
 
-        -- TODO: binders
         goLet :: Internal.Let -> Sem r Expression
         goLet Internal.Let {..} = do
           let fdefs = concatMap toFunDefs (toList _letClauses)
@@ -771,6 +792,9 @@ goModule onlyTypes infoTable Internal.Module {..} =
               x' <- goPatternArg x
               y' <- goPatternArg y
               return $ PatCons (Cons x' y')
+          | Just fields <- getRecordPat _constrAppConstructor _constrAppParameters = do
+              fields' <- mapM (secondM goPatternArg) fields
+              return $ PatRecord (Record fields')
           | Just (x, y) <- getPairPat _constrAppConstructor _constrAppParameters = do
               x' <- goPatternArg x
               y' <- goPatternArg y
@@ -817,6 +841,13 @@ goModule onlyTypes infoTable Internal.Module {..} =
                 _ -> Nothing
             Nothing -> Nothing
 
+        getRecordPat :: Name -> [Internal.PatternArg] -> Maybe [(Name, Internal.PatternArg)]
+        getRecordPat name args =
+          case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
+            Just ctrInfo
+              | ctrInfo ^. Internal.constructorInfoRecord -> Just (goRecordFields (getArgtys ctrInfo) args)
+            _ -> Nothing
+
         getNatPat :: Name -> [Internal.PatternArg] -> Maybe (Either Pattern Internal.PatternArg)
         getNatPat name args =
           case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of

src/Juvix/Compiler/Internal/Data/InfoTable.hs

@@ -265,5 +265,6 @@ mkConstructorEntries d =
       (_constructorInfoBuiltin, c) <- zipExact builtins (d ^. inductiveConstructors),
       let _constructorInfoType = c ^. inductiveConstructorType,
       let _constructorInfoName = c ^. inductiveConstructorName,
-      let _constructorInfoTrait = d ^. inductiveTrait
+      let _constructorInfoTrait = d ^. inductiveTrait,
+      let _constructorInfoRecord = c ^. inductiveConstructorIsRecord
   ]

src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs

@@ -10,7 +10,8 @@ data ConstructorInfo = ConstructorInfo
     _constructorInfoInductive :: InductiveName,
     _constructorInfoName :: ConstructorName,
     _constructorInfoBuiltin :: Maybe BuiltinConstructor,
-    _constructorInfoTrait :: Bool
+    _constructorInfoTrait :: Bool,
+    _constructorInfoRecord :: Bool
   }
   deriving stock (Generic)
 

tests/positive/Isabelle/Program.juvix

@@ -102,6 +102,13 @@ type R := mkR {
   r2 : Nat;
 };
 
+funR (r : R) : R :=
+  case r of
+  | mkR@{r1; r2} := r@R{r1 := r1 + r2};
+
+funR' : R -> R
+  | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr1 + rr2; r2 := rr2};
+
 -- Standard library
 
 bf (b1 b2 : Bool) : Bool := not (b1 && b2);

tests/positive/Isabelle/isabelle/Program.thy

@@ -99,6 +99,18 @@ datatype ('A, 'B) Either'
   = Left' 'A |
     Right' 'B
 
+record R =
+  r1 :: nat
+  r2 :: nat
+
+fun r1 :: "R \<Rightarrow> nat"  where
+  "r1 \<lparr> r1 = r1', r2 = _  \<rparr> = r1'"
+
+fun funR :: "R \<Rightarrow> R" where
+  "funR r =
+    (case r of
+      _ \<Rightarrow> r\<lparr>r1 := R.r1 r + R.r2 r\<rparr>)"
+
 fun bf :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
   "bf b1 b2 = (\<not> (b1 \<and> b2))"