Isabelle/HOL translation: fix creation of polymorphic records (#3051)

* Creation of polymorphic records was not translated correctly, with the
types appearing as arguments instead of the values.
* Depends on #3050

Author: lukaszcz

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

@@ -471,7 +471,11 @@ goModule onlyTypes infoTable Internal.Module {..} =
 
     goRecordFields :: [Internal.FunctionParameter] -> [a] -> [(Name, a)]
     goRecordFields argtys args = case (argtys, args) of
-      (ty : argtys', arg' : args') -> (fromMaybe (defaultName (getLoc ty) "_") (ty ^. Internal.paramName), arg') : goRecordFields argtys' args'
+      (param : argtys', arg' : args')
+        | param ^. Internal.paramImplicit == Internal.Explicit ->
+            (fromMaybe (defaultName (getLoc param) "_") (param ^. Internal.paramName), arg') : goRecordFields argtys' args'
+        | otherwise ->
+            goRecordFields argtys' args'
       _ -> []
 
     goExpression' :: Internal.Expression -> Expression
@@ -567,6 +571,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
               fn' <- goExpression fn
               args' <- mapM goExpression args
               return $ mkApp fn' args'
+          | _appImplicit /= Internal.Explicit =
+              goExpression _appLeft
           | otherwise = do
               l <- goExpression _appLeft
               r <- goExpression _appRight
@@ -729,7 +735,7 @@ goModule onlyTypes infoTable Internal.Module {..} =
               _ -> Nothing
           _ -> Nothing
           where
-            (fn, args) = Internal.unfoldApplication app
+            (fn, args) = Internal.unfoldExplicitApplication app
 
         getRecordUpdate :: Internal.Application -> Maybe (Name, [Name], Internal.Expression, [(Name, Internal.Expression)])
         getRecordUpdate Internal.Application {..} = case _appLeft of
@@ -752,7 +758,7 @@ goModule onlyTypes infoTable Internal.Module {..} =
                                 _ -> Nothing
                         _ -> Nothing
                         where
-                          (fn, args) = Internal.unfoldApplication app
+                          (fn, args) = Internal.unfoldExplicitApplication app
                       _ -> Nothing
               _ -> Nothing
             _ -> Nothing
@@ -799,7 +805,11 @@ goModule onlyTypes infoTable Internal.Module {..} =
 
         goLet :: Internal.Let -> Sem r Expression
         goLet Internal.Let {..} = do
-          let fdefs = concatMap toFunDefs (toList _letClauses)
+          let fdefs =
+                filter (not . Internal.isTypeConstructor . (^. Internal.funDefType))
+                  . concatMap toFunDefs
+                  . toList
+                  $ _letClauses
           cls <- mapM goFunDef fdefs
           let ns = zipExact (map (^. Internal.funDefName) fdefs) (map (^. letClauseName) cls)
           expr <- localNames ns $ goExpression _letExpression

src/Juvix/Compiler/Internal/Extra/Base.hs

@@ -460,6 +460,15 @@ unfoldExpressionApp = swap . run . runAccumListReverse . go
 unfoldApplication :: Application -> (Expression, NonEmpty Expression)
 unfoldApplication = fmap (fmap (^. appArg)) . unfoldApplication'
 
+unfoldExplicitApplication :: Application -> (Expression, [Expression])
+unfoldExplicitApplication =
+  fmap
+    ( fmap (^. appArg)
+        . filter (\x -> x ^. appArgIsImplicit == Explicit)
+        . toList
+    )
+    . unfoldApplication'
+
 -- | A fold over all transitive children, including self
 patternCosmos :: SimpleFold Pattern Pattern
 patternCosmos f p = case p of

tests/positive/Isabelle/Program.juvix

@@ -204,50 +204,45 @@ nf (n1 n2 : Int) : Bool := n1 - n2 >= n1 || n2 <= n1 + n2;
 
 -- Nested record patterns
 
-type MessagePacket (MessageType : Type) : Type := mkMessagePacket {
-  target : Nat;
-  mailbox : Maybe Nat;
-  message : MessageType;
-};
+type MessagePacket (MessageType : Type) : Type :=
+  mkMessagePacket {
+    target : Nat;
+    mailbox : Maybe Nat;
+    message : MessageType
+  };
 
 open MessagePacket;
 
 type EnvelopedMessage (MessageType : Type) : Type :=
   mkEnvelopedMessage {
     sender : Maybe Nat;
-    packet : MessagePacket MessageType;
+    packet : MessagePacket MessageType
   };
 
 open EnvelopedMessage;
 
-type Timer (HandleType : Type): Type := mkTimer {
-  time : Nat;
-  handle : HandleType;
-};
+type Timer (HandleType : Type) : Type :=
+  mkTimer {
+    time : Nat;
+    handle : HandleType
+  };
 
 type Trigger (MessageType : Type) (HandleType : Type) :=
-  | MessageArrived { envelope : EnvelopedMessage MessageType; }
-  | Elapsed { timers : List (Timer HandleType) };
+  | MessageArrived {envelope : EnvelopedMessage MessageType}
+  | Elapsed {timers : List (Timer HandleType)};
 
 open Trigger;
 
 getMessageFromTrigger : {M H : Type} -> Trigger M H -> Maybe M
-      | (MessageArrived@{
-          envelope := (mkEnvelopedMessage@{
-            packet := (mkMessagePacket@{
-              message := m })})})
-              := just m
-      | _ := nothing;
-
+  | MessageArrived@{envelope := mkEnvelopedMessage@{packet := mkMessagePacket@{message := m}}} :=
+    just m
+  | _ := nothing;
 
 getMessageFromTrigger' {M H} (t : Trigger M H) : Maybe M :=
-     case t of
-      | (MessageArrived@{
-          envelope := (mkEnvelopedMessage@{
-            packet := (mkMessagePacket@{
-              message := m })})})
-              := just m
-      | _ := nothing;
+  case t of
+    | MessageArrived@{envelope := mkEnvelopedMessage@{packet := mkMessagePacket@{message := m}}} :=
+      just m
+    | _ := nothing;
 
 -- Syntax aliases
 
@@ -259,6 +254,38 @@ idT (x : T) : T := x;
 
 t : T := 0;
 
-type RR := mkRR {
-  x : T
-};
+type RR := mkRR {x : T};
+
+-- Type constructor identifiers
+
+type GuardOutput (A L X : Type) :=
+  mkGuardOutput {
+    args : List A;
+    label : L;
+    other : X
+  };
+
+open GuardOutput;
+
+type GuardReturnLabel :=
+  | doIncrement
+  | doRespond Nat;
+
+open GuardReturnLabel;
+
+type GuardReturnOther := nuthing;
+
+open GuardReturnOther;
+
+type GuardReturnArgs := ReplyTo Nat;
+
+ifIncrement
+  : Trigger Nat Nat -> Maybe (GuardOutput GuardReturnArgs GuardReturnLabel GuardReturnOther)
+  | MessageArrived@{envelope := m} :=
+    just
+      mkGuardOutput@{
+        args := [];
+        label := doIncrement;
+        other := nuthing
+      }
+  | Elapsed@{timers := ts} := nothing;

tests/positive/Isabelle/isabelle/Program.thy

@@ -316,4 +316,41 @@ record RR =
 fun x :: "RR \<Rightarrow> Name" where
   "x (| RR.x = x' |) = x'"
 
+(* Type constructor identifiers *)
+record ('A, 'L, 'X) GuardOutput =
+  args :: "'A list"
+  label :: 'L
+  other :: 'X
+
+fun args :: "('A, 'L, 'X) GuardOutput \<Rightarrow> 'A list" where
+  "args (| GuardOutput.args = args', GuardOutput.label = label', GuardOutput.other = other' |) =
+    args'"
+
+fun label :: "('A, 'L, 'X) GuardOutput \<Rightarrow> 'L" where
+  "label (| GuardOutput.args = args', GuardOutput.label = label', GuardOutput.other = other' |) =
+    label'"
+
+fun other :: "('A, 'L, 'X) GuardOutput \<Rightarrow> 'X" where
+  "other (| GuardOutput.args = args', GuardOutput.label = label', GuardOutput.other = other' |) =
+    other'"
+
+datatype GuardReturnLabel
+  = doIncrement |
+    doRespond nat
+
+datatype GuardReturnOther
+  = nuthing
+
+datatype GuardReturnArgs
+  = ReplyTo nat
+
+fun ifIncrement :: "(nat, nat) Trigger \<Rightarrow> ((GuardReturnArgs, GuardReturnLabel, GuardReturnOther) GuardOutput) option" where
+  "ifIncrement (MessageArrived m) =
+    (Some (let
+             args' = [];
+             label' = doIncrement;
+             other' = nuthing
+           in (| GuardOutput.args = args', GuardOutput.label = label', GuardOutput.other = other' |)))" |
+  "ifIncrement (Elapsed ts) = None"
+
 end