Translate function bodies to Isabelle/HOL (#2868)

* Closes #2813 

Implements a translation from Juvix functions to Isabelle/HOL functions.
This extends the previous Juvix -> Isabelle translation which could
handle only type signatures.

Checklist
---------

- [x] Basic translation
- [x] Polymorphism
- [x] Arithmetic operators
- [x] Numeric literals
- [x] List literals
- [x] Comparison operators
- [x] Boolean operators
- [x] `if` translated to Isabelle `if`
- [x] `true` and `false` translated to Isabelle `True` and `False`
- [x] `zero` and `suc` translated to Isabelle `0` and `Suc`
- [x] `Maybe` translated to Isabelle `option`
- [x] Pairs translated to Isabelle tuples
- [x] Quote Isabelle identifier names (e.g. cannot begin with `_`)
- [x] Rename variables to avoid clashes (in Isabelle/HOL pattern
variables don't shadow function identifiers)
- [x] Common stdlib functions (`map`, `filter`, etc) translated to
corresponding Isabelle functions
- [x] Multiple assignments in a single `let`
- [x] CLI
- [x] Test
- The test is very fragile, similar to the markdown test. It just
compares the result of translation to Isabelle against a predefined
expected output file.

Limitations
-----------

The translation is not designed to be completely correct under all
circumstances. There are aspects of the Juvix language that cannot be
straightforwardly translated to Isabelle/HOL, and these are not planned
to ever be properly handled. There are other aspects that are difficult
but not impossible to translate, and these are left for future work.
Occasionally, the generated code may need manual adjustments to
type-check in Isabelle/HOL.

In particular:
* Higher-rank polymorphism or functions on types cannot be translated as
these features are not supported by Isabelle/HOL. Juvix programs using
these features will not be correctly translated (the generated output
may need manual adjustment).
* In cases where Juvix termination checking diverges from Isabelle/HOL
termination checking, providing a termination proof manually may be
necessary. Non-terminating Juvix functions cannot be automatically
translated and need to be manually modelled in Isabelle/HOL in a
different way (e.g. as relations).
* Comments (including judoc) are ignored. This is left for future work.
* Traits are not translated to Isabelle/HOL type classes / locales. This
is left for future work.
* Mutually recursive functions are not correctly translated. This is
left for future work.
* Record creation, update, field access and pattern matching are not
correctly translated. This is left for future work.
* Named patterns are not correctly translated. This is left for future
work.
* Side conditions in patterns are not supported. This is left for future
work.
* If a Juvix function in the translated module has the same name as some
function from the Isabelle/HOL standard library, there will be a name
clash in the generated code.

---------

Co-authored-by: Paul Cadman <[email protected]>

app/Commands/Isabelle/Options.hs

@@ -19,18 +19,18 @@ parseIsabelle = do
     parseGenericOutputDir
       ( value "isabelle"
           <> showDefault
-          <> help "Isabelle/HOL output directory."
+          <> help "Isabelle/HOL output directory"
           <> action "directory"
       )
   _isabelleStdout <-
     switch
       ( long "stdout"
-          <> help "Write the output to stdout instead of a file."
+          <> help "Write the output to stdout instead of a file"
       )
   _isabelleOnlyTypes <-
     switch
       ( long "only-types"
-          <> help "Translate types only. Omit function signatures."
+          <> help "Translate types only"
       )
   _isabelleInputFile <- optional (parseInputFile FileExtJuvix)
   pure IsabelleOptions {..}

app/TopCommand/Options.hs

@@ -201,14 +201,14 @@ commandIsabelle =
   command "isabelle" $
     info
       (Isabelle <$> parseIsabelle)
-      (progDesc "Generate Isabelle/HOL types for a Juvix file")
+      (progDesc "Translate a Juvix file to Isabelle/HOL")
 
 commandDev :: Mod CommandFields TopCommand
 commandDev =
   command "dev" $
     info
       (Dev <$> Dev.parseDevCommand)
-      (progDesc "Commands for the developers")
+      (progDesc "Commands for the Juvix compiler developers")
 
 parseCompilerCommand :: Parser TopCommand
 parseCompilerCommand =

include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix

@@ -7,8 +7,10 @@ trait
 type Natural A :=
   mkNatural {
     syntax operator + additive;
+    {-# isabelle-operator: {name: "+", prec: 65, assoc: left} #-}
     + : A -> A -> A;
     syntax operator * multiplicative;
+    {-# isabelle-operator: {name: "*", prec: 70, assoc: left} #-}
     * : A -> A -> A;
     builtin from-nat
     fromNat : Nat -> A

src/Juvix/Compiler/Backend/Isabelle/Extra.hs

@@ -0,0 +1,8 @@
+module Juvix.Compiler.Backend.Isabelle.Extra where
+
+import Juvix.Compiler.Backend.Isabelle.Language
+
+mkApp :: Expression -> [Expression] -> Expression
+mkApp fn = \case
+  [] -> fn
+  arg : args -> mkApp (ExprApp (Application fn arg)) args

src/Juvix/Compiler/Backend/Isabelle/Language.hs

@@ -5,17 +5,17 @@ module Juvix.Compiler.Backend.Isabelle.Language
   )
 where
 
-import Juvix.Compiler.Internal.Data.Name
-import Juvix.Prelude
+import Juvix.Compiler.Internal.Data.Name hiding (letFixity)
+import Juvix.Prelude hiding (Cons, letFixity)
 
 data Type
-  = TyVar Var
+  = TyVar TypeVar
   | TyFun FunType
   | TyInd IndApp
   deriving stock (Eq)
 
-data Var = Var
-  { _varName :: Name
+data TypeVar = TypeVar
+  { _typeVarName :: Name
   }
   deriving stock (Eq)
 
@@ -31,6 +31,8 @@ data Inductive
   | IndInt
   | IndList
   | IndString
+  | IndOption
+  | IndTuple
   | IndUser Name
   deriving stock (Eq)
 
@@ -40,10 +42,108 @@ data IndApp = IndApp
   }
   deriving stock (Eq)
 
-makeLenses ''Var
+makeLenses ''TypeVar
 makeLenses ''FunType
 makeLenses ''IndApp
 
+data Expression
+  = ExprIden Name
+  | ExprUndefined
+  | ExprLiteral Literal
+  | ExprApp Application
+  | ExprBinop Binop
+  | ExprTuple (Tuple Expression)
+  | ExprList (List Expression)
+  | ExprCons (Cons Expression)
+  | ExprLet Let
+  | ExprIf If
+  | ExprCase Case
+  | ExprLambda Lambda
+
+data Literal
+  = LitNumeric Integer
+  | LitString Text
+
+data Application = Application
+  { _appLeft :: Expression,
+    _appRight :: Expression
+  }
+
+data Binop = Binop
+  { _binopOperator :: Name,
+    _binopLeft :: Expression,
+    _binopRight :: Expression,
+    _binopFixity :: Fixity
+  }
+
+data Let = Let
+  { _letClauses :: NonEmpty LetClause,
+    _letBody :: Expression
+  }
+
+data LetClause = LetClause
+  { _letClauseName :: Name,
+    _letClauseValue :: Expression
+  }
+
+data If = If
+  { _ifValue :: Expression,
+    _ifBranchTrue :: Expression,
+    _ifBranchFalse :: Expression
+  }
+
+data Case = Case
+  { _caseValue :: Expression,
+    _caseBranches :: NonEmpty CaseBranch
+  }
+
+data CaseBranch = CaseBranch
+  { _caseBranchPattern :: Pattern,
+    _caseBranchBody :: Expression
+  }
+
+data Lambda = Lambda
+  { _lambdaVar :: Name,
+    _lambdaType :: Maybe Type,
+    _lambdaBody :: Expression
+  }
+
+data Pattern
+  = PatVar Name
+  | PatZero
+  | PatConstrApp ConstrApp
+  | PatTuple (Tuple Pattern)
+  | PatList (List Pattern)
+  | PatCons (Cons Pattern)
+
+newtype Tuple a = Tuple
+  { _tupleComponents :: NonEmpty a
+  }
+
+newtype List a = List
+  { _listElements :: [a]
+  }
+
+data Cons a = Cons
+  { _consHead :: a,
+    _consTail :: a
+  }
+
+data ConstrApp = ConstrApp
+  { _constrAppConstructor :: Name,
+    _constrAppArgs :: [Pattern]
+  }
+
+makeLenses ''Application
+makeLenses ''Let
+makeLenses ''LetClause
+makeLenses ''If
+makeLenses ''Case
+makeLenses ''CaseBranch
+makeLenses ''Lambda
+makeLenses ''ConstrApp
+makeLenses ''Expression
+
 data Statement
   = StmtDefinition Definition
   | StmtFunction Function
@@ -53,12 +153,19 @@ data Statement
 
 data Definition = Definition
   { _definitionName :: Name,
-    _definitionType :: Type
+    _definitionType :: Type,
+    _definitionBody :: Expression
   }
 
 data Function = Function
   { _functionName :: Name,
-    _functionType :: Type
+    _functionType :: Type,
+    _functionClauses :: NonEmpty Clause
+  }
+
+data Clause = Clause
+  { _clausePatterns :: NonEmpty Pattern,
+    _clauseBody :: Expression
   }
 
 data Synonym = Synonym
@@ -68,7 +175,7 @@ data Synonym = Synonym
 
 data Datatype = Datatype
   { _datatypeName :: Name,
-    _datatypeParams :: [Var],
+    _datatypeParams :: [TypeVar],
     _datatypeConstructors :: [Constructor]
   }
 
@@ -79,7 +186,7 @@ data Constructor = Constructor
 
 data Record = Record
   { _recordName :: Name,
-    _recordParams :: [Var],
+    _recordParams :: [TypeVar],
     _recordFields :: [RecordField]
   }
 
@@ -95,6 +202,7 @@ makeLenses ''Datatype
 makeLenses ''Constructor
 makeLenses ''Record
 makeLenses ''RecordField
+makeLenses ''Tuple
 
 data Theory = Theory
   { _theoryName :: Name,
@@ -104,7 +212,63 @@ data Theory = Theory
 
 makeLenses ''Theory
 
-instance HasAtomicity Var where
+caseFixity :: Fixity
+caseFixity =
+  Fixity
+    { _fixityPrecedence = PrecNat 0,
+      _fixityArity = OpBinary AssocLeft,
+      _fixityId = Nothing
+    }
+
+lambdaFixity :: Fixity
+lambdaFixity =
+  Fixity
+    { _fixityPrecedence = PrecNat 0,
+      _fixityArity = OpUnary AssocPostfix,
+      _fixityId = Nothing
+    }
+
+ifFixity :: Fixity
+ifFixity =
+  Fixity
+    { _fixityPrecedence = PrecNat 1,
+      _fixityArity = OpBinary AssocRight,
+      _fixityId = Nothing
+    }
+
+letFixity :: Fixity
+letFixity =
+  Fixity
+    { _fixityPrecedence = PrecNat 2,
+      _fixityArity = OpBinary AssocRight,
+      _fixityId = Nothing
+    }
+
+consFixity :: Fixity
+consFixity =
+  Fixity
+    { _fixityPrecedence = PrecNat 80,
+      _fixityArity = OpBinary AssocRight,
+      _fixityId = Nothing
+    }
+
+andFixity :: Fixity
+andFixity =
+  Fixity
+    { _fixityPrecedence = PrecNat 35,
+      _fixityArity = OpBinary AssocRight,
+      _fixityId = Nothing
+    }
+
+orFixity :: Fixity
+orFixity =
+  Fixity
+    { _fixityPrecedence = PrecNat 30,
+      _fixityArity = OpBinary AssocRight,
+      _fixityId = Nothing
+    }
+
+instance HasAtomicity TypeVar where
   atomicity _ = Atom
 
 instance HasAtomicity Type where
@@ -114,3 +278,29 @@ instance HasAtomicity Type where
     TyInd IndApp {..}
       | null _indAppParams -> Atom
       | otherwise -> Aggregate appFixity
+
+instance HasAtomicity Expression where
+  atomicity = \case
+    ExprIden {} -> Atom
+    ExprUndefined -> Atom
+    ExprLiteral {} -> Atom
+    ExprApp {} -> Aggregate appFixity
+    ExprBinop Binop {..} -> Aggregate _binopFixity
+    ExprTuple {} -> Atom
+    ExprList {} -> Atom
+    ExprCons {} -> Aggregate consFixity
+    ExprLet {} -> Aggregate letFixity
+    ExprIf {} -> Aggregate ifFixity
+    ExprCase {} -> Aggregate caseFixity
+    ExprLambda {} -> Aggregate lambdaFixity
+
+instance HasAtomicity Pattern where
+  atomicity = \case
+    PatVar {} -> Atom
+    PatZero -> Atom
+    PatConstrApp ConstrApp {..}
+      | null _constrAppArgs -> Atom
+      | otherwise -> Aggregate appFixity
+    PatTuple {} -> Atom
+    PatList {} -> Atom
+    PatCons {} -> Aggregate consFixity