Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Isabelle/HOL translation: the isabelle-ignore pragma #2955

Merged
merged 3 commits into from
Aug 19, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 13 additions & 6 deletions src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,9 @@ goModule onlyTypes infoTable Internal.Module {..} =
Theory
{ _theoryName = over nameText toIsabelleName $ over namePretty toIsabelleName _moduleName,
_theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports),
_theoryStatements = concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
_theoryStatements = case _modulePragmas ^. pragmasIsabelleIgnore of
Just (PragmaIsabelleIgnore True) -> []
_ -> concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
}
where
toIsabelleName :: Text -> Text
Expand All @@ -75,13 +77,18 @@ goModule onlyTypes infoTable Internal.Module {..} =
goMutualBlock :: Internal.MutualBlock -> [Statement]
goMutualBlock Internal.MutualBlock {..} =
filter (\stmt -> not onlyTypes || isTypeDef stmt) $
map goMutualStatement (toList _mutualStatements)
mapMaybe goMutualStatement (toList _mutualStatements)

goMutualStatement :: Internal.MutualStatement -> Statement
checkNotIgnored :: Pragmas -> a -> Maybe a
checkNotIgnored pragmas x = case pragmas ^. pragmasIsabelleIgnore of
Just (PragmaIsabelleIgnore True) -> Nothing
_ -> Just x

goMutualStatement :: Internal.MutualStatement -> Maybe Statement
goMutualStatement = \case
Internal.StatementInductive x -> goInductiveDef x
Internal.StatementFunction x -> goFunctionDef x
Internal.StatementAxiom x -> goAxiomDef x
Internal.StatementInductive x -> checkNotIgnored (x ^. Internal.inductivePragmas) $ goInductiveDef x
Internal.StatementFunction x -> checkNotIgnored (x ^. Internal.funDefPragmas) $ goFunctionDef x
Internal.StatementAxiom x -> checkNotIgnored (x ^. Internal.axiomPragmas) $ goAxiomDef x

goInductiveDef :: Internal.InductiveDef -> Statement
goInductiveDef Internal.InductiveDef {..}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1650,14 +1650,27 @@ checkSections sec = topBindings helper
_projectionKind = kind,
_projectionFieldBuiltin = field ^. fieldBuiltin,
_projectionDoc = field ^. fieldDoc,
_projectionPragmas = field ^. fieldPragmas
_projectionPragmas = combinePragmas (i ^. inductivePragmas) (field ^. fieldPragmas)
}
where
kind :: ProjectionKind
kind = case field ^. fieldIsImplicit of
ExplicitField -> ProjectionExplicit
ImplicitInstanceField -> ProjectionCoercion

combinePragmas :: Maybe ParsedPragmas -> Maybe ParsedPragmas -> Maybe ParsedPragmas
combinePragmas p1 p2 = case (p1, p2) of
(Nothing, Nothing) -> Nothing
(Just p, Nothing) -> Just p
(Nothing, Just p) -> Just p
(Just p1', Just p2') ->
Just
( over
(withLocParam . withSourceValue . pragmasIsabelleIgnore)
(\i2 -> i2 <|> (p1' ^. withLocParam . withSourceValue . pragmasIsabelleIgnore))
p2'
)

getFields :: Sem (Fail ': s') [RecordStatement 'Parsed]
getFields = case i ^. inductiveConstructors of
c :| [] -> case c ^. constructorRhs of
Expand Down
26 changes: 23 additions & 3 deletions src/Juvix/Data/Pragmas.hs
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,11 @@ newtype PragmaIsabelleFunction = PragmaIsabelleFunction
}
deriving stock (Show, Eq, Ord, Data, Generic)

newtype PragmaIsabelleIgnore = PragmaIsabelleIgnore
{ _pragmaIsabelleIgnore :: Bool
}
deriving stock (Show, Eq, Ord, Data, Generic)

data Pragmas = Pragmas
{ _pragmasInline :: Maybe PragmaInline,
_pragmasUnroll :: Maybe PragmaUnroll,
Expand All @@ -82,7 +87,8 @@ data Pragmas = Pragmas
_pragmasSpecialiseBy :: Maybe PragmaSpecialiseBy,
_pragmasEval :: Maybe PragmaEval,
_pragmasIsabelleOperator :: Maybe PragmaIsabelleOperator,
_pragmasIsabelleFunction :: Maybe PragmaIsabelleFunction
_pragmasIsabelleFunction :: Maybe PragmaIsabelleFunction,
_pragmasIsabelleIgnore :: Maybe PragmaIsabelleIgnore
}
deriving stock (Show, Eq, Ord, Data, Generic)

Expand Down Expand Up @@ -121,6 +127,8 @@ instance Hashable PragmaIsabelleOperator

instance Hashable PragmaIsabelleFunction

instance Hashable PragmaIsabelleIgnore

instance Hashable Pragmas

instance Serialize PragmaInline
Expand Down Expand Up @@ -171,6 +179,10 @@ instance Serialize PragmaIsabelleFunction

instance NFData PragmaIsabelleFunction

instance Serialize PragmaIsabelleIgnore

instance NFData PragmaIsabelleIgnore

instance Serialize Pragmas

instance NFData Pragmas
Expand Down Expand Up @@ -201,6 +213,7 @@ instance FromJSON Pragmas where
_pragmasEval <- keyMay "eval" parseEval
_pragmasIsabelleOperator <- keyMay "isabelle-operator" parseIsabelleOperator
_pragmasIsabelleFunction <- keyMay "isabelle-function" parseIsabelleFunction
_pragmasIsabelleIgnore <- keyMay "isabelle-ignore" parseIsabelleIgnore
return Pragmas {..}

parseInline :: Parse YamlError PragmaInline
Expand Down Expand Up @@ -273,6 +286,11 @@ instance FromJSON Pragmas where
_pragmaIsabelleFunctionName <- key "name" asText
return PragmaIsabelleFunction {..}

parseIsabelleIgnore :: Parse YamlError PragmaIsabelleIgnore
parseIsabelleIgnore = do
_pragmaIsabelleIgnore <- asBool
return PragmaIsabelleIgnore {..}

parseSpecialiseArg :: Parse YamlError PragmaSpecialiseArg
parseSpecialiseArg =
(SpecialiseArgNum <$> asIntegral)
Expand Down Expand Up @@ -316,7 +334,8 @@ instance Semigroup Pragmas where
_pragmasSpecialiseArgs = p2 ^. pragmasSpecialiseArgs <|> p1 ^. pragmasSpecialiseArgs,
_pragmasSpecialiseBy = p2 ^. pragmasSpecialiseBy <|> p1 ^. pragmasSpecialiseBy,
_pragmasIsabelleOperator = p2 ^. pragmasIsabelleOperator,
_pragmasIsabelleFunction = p2 ^. pragmasIsabelleFunction
_pragmasIsabelleFunction = p2 ^. pragmasIsabelleFunction,
_pragmasIsabelleIgnore = p2 ^. pragmasIsabelleIgnore <|> p1 ^. pragmasIsabelleIgnore
}

instance Monoid Pragmas where
Expand All @@ -332,7 +351,8 @@ instance Monoid Pragmas where
_pragmasSpecialiseBy = Nothing,
_pragmasEval = Nothing,
_pragmasIsabelleOperator = Nothing,
_pragmasIsabelleFunction = Nothing
_pragmasIsabelleFunction = Nothing,
_pragmasIsabelleIgnore = Nothing
}

adjustPragmaInline :: Int -> PragmaInline -> PragmaInline
Expand Down
1 change: 1 addition & 0 deletions tests/positive/Isabelle/Program.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,7 @@ type Either' A B := Left' A | Right' B;

-- Records

{-# isabelle-ignore: true #-}
type R := mkR {
r1 : Nat;
r2 : Nat;
Expand Down
10 changes: 0 additions & 10 deletions tests/positive/Isabelle/isabelle/Program.thy
Original file line number Diff line number Diff line change
Expand Up @@ -99,16 +99,6 @@ datatype ('A, 'B) Either'
= Left' 'A |
Right' 'B

record R =
r1 :: nat
r2 :: nat

fun r1 :: "R \<Rightarrow> nat" where
"r1 (mkR r1' r2') = r1'"

fun r2 :: "R \<Rightarrow> nat" where
"r2 (mkR r1' r2') = r2'"

fun bf :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
"bf b1 b2 = (\<not> (b1 \<and> b2))"

Expand Down
Loading