wip

Author: janmasrovira

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

@@ -352,6 +352,7 @@ goModule onlyTypes infoTable Internal.Module {..} =
       Internal.ExpressionSimpleLambda {} -> unsupportedType ty
       Internal.ExpressionLambda {} -> unsupportedType ty
       Internal.ExpressionCase {} -> unsupportedType ty
+      Internal.ExpressionNatural {} -> unsupportedType ty
       where
         unsupportedType :: Internal.Expression -> a
         unsupportedType e = error ("unsupported type: " <> Internal.ppTrace e)
@@ -476,6 +477,7 @@ goModule onlyTypes infoTable Internal.Module {..} =
       Internal.ExpressionSimpleLambda x -> goSimpleLambda x
       Internal.ExpressionLambda x -> goLambda x
       Internal.ExpressionCase x -> goCase x
+      Internal.ExpressionNatural {} -> error "TODO"
       where
         goIden :: Internal.Iden -> Sem r Expression
         goIden iden = case iden of

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

@@ -712,6 +712,23 @@ freshHole l = mkHole l <$> freshNameId
 mkFreshHole :: (Members '[NameIdGen] r) => Interval -> Sem r Expression
 mkFreshHole l = ExpressionHole <$> freshHole l
 
+squashBuiltinNatural :: BuiltinNatural -> Either BuiltinNatural Expression
+squashBuiltinNatural n
+  | n ^. builtinNaturalSuc == 0 = case n ^. builtinNaturalArg of
+      ExpressionNatural n' -> squashBuiltinNatural n'
+      m -> Right m
+  | otherwise = case n ^. builtinNaturalArg of
+      ExpressionNatural n' -> case squashBuiltinNatural n' of
+        Right s -> Left (set builtinNaturalArg s n)
+        Left s ->
+          Left
+            BuiltinNatural
+              { _builtinNaturalSuc = n ^. builtinNaturalSuc + s ^. builtinNaturalSuc,
+                _builtinNaturalArg = s ^. builtinNaturalArg,
+                _builtinNaturalLoc = n ^. builtinNaturalLoc <> s ^. builtinNaturalLoc
+              }
+      m -> Right m
+
 matchExpressions ::
   forall r.
   (Members '[State (HashMap Name Name), Reader (HashSet VarName), Error Text] r) =>

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

@@ -47,15 +47,25 @@ makeRigidParam p = case p of
   InstanceParamHole {} -> p
   InstanceParamMeta v -> InstanceParamVar v
 
-paramToExpression :: (Member NameIdGen r) => InstanceParam -> Sem r Expression
+paramToExpression :: forall r. (Member NameIdGen r) => InstanceParam -> Sem r Expression
 paramToExpression = \case
   InstanceParamVar v -> return $ ExpressionIden (IdenVar v)
-  -- TODO use builtin nat in Internal
-  InstanceParamNatural InstanceNat {..} -> return _instanceNatExpression
+  InstanceParamNatural n -> goNat n
   InstanceParamApp InstanceApp {..} -> return _instanceAppExpression
   InstanceParamFun InstanceFun {..} -> return _instanceFunExpression
   InstanceParamHole h -> return $ ExpressionHole h
   InstanceParamMeta v -> ExpressionHole . mkHole (getLoc v) <$> freshNameId
+  where
+    goNat :: InstanceNat -> Sem r Expression
+    goNat InstanceNat {..} = do
+      arg <- paramToExpression _instanceNatArg
+      return $
+        ExpressionNatural
+          BuiltinNatural
+            { _builtinNaturalSuc = _instanceNatSuc,
+              _builtinNaturalArg = arg,
+              _builtinNaturalLoc = _instanceNatLoc
+            }
 
 paramFromExpression :: forall r. (Members '[Reader BuiltinsTable] r) => HashSet VarName -> Expression -> Sem (Fail ': r) InstanceParam
 paramFromExpression metaVars e = case e of

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs

@@ -26,6 +26,7 @@ goArg ty = case ty of
   ExpressionSimpleLambda {} -> invalid
   ExpressionLambda {} -> invalid
   ExpressionCase {} -> invalid
+  ExpressionNatural {} -> invalid
   where
     invalid :: forall a. Sem r a
     invalid =

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs

@@ -1053,6 +1053,7 @@ inferLeftAppExpression mhint e = case e of
   ExpressionApplication {} -> impossible
   ExpressionIden i -> goIden i
   ExpressionLiteral l -> goLiteral l
+  ExpressionNatural n -> goNatural n
   ExpressionFunction f -> goFunction f
   ExpressionHole h -> goHole h
   ExpressionInstanceHole h -> goInstanceHole h
@@ -1062,6 +1063,9 @@ inferLeftAppExpression mhint e = case e of
   ExpressionLet l -> goLet l
   ExpressionCase l -> goCase l
   where
+    goNatural :: BuiltinNatural -> Sem r TypedExpression
+    goNatural = error "TODO"
+
     goLet :: Let -> Sem r TypedExpression
     goLet l = do
       _letClauses <- mapM goLetClause (l ^. letClauses)
@@ -1653,6 +1657,7 @@ typeArity = weakNormalize >=> go
       ExpressionFunction f -> ArityFunction <$> goFun f
       ExpressionHole h -> return (ArityBlocking (BlockingHole h))
       ExpressionInstanceHole {} -> return ArityUnit
+      ExpressionNatural {} -> return ArityUnit
       ExpressionLambda {} -> return ArityError
       ExpressionCase {} -> return ArityNotKnown -- TODO Do better here
       ExpressionUniverse {} -> return ArityUnit
@@ -1716,6 +1721,7 @@ guessArity = \case
   ExpressionHole {} -> return ArityNotKnown
   ExpressionInstanceHole {} -> return ArityUnit
   ExpressionFunction {} -> return ArityUnit
+  ExpressionNatural {} -> return ArityUnit
   ExpressionLiteral {} -> return arityLiteral
   ExpressionApplication a -> appHelper a
   ExpressionIden i -> idenHelper i

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs

@@ -158,6 +158,7 @@ strongNormalize' original = do
       ExpressionApplication app -> goApp app
       ExpressionLiteral {} -> return e
       ExpressionHole h -> goHole h
+      ExpressionNatural n -> goNatural n
       ExpressionInstanceHole h -> goInstanceHole h
       ExpressionUniverse {} -> return e
       ExpressionFunction f -> ExpressionFunction <$> goFunction f
@@ -169,6 +170,11 @@ strongNormalize' original = do
       -- TODO it should normalize like an applied lambda
       ExpressionCase c -> return (ExpressionCase c)
 
+    goNatural :: BuiltinNatural -> Sem r Expression
+    goNatural n = case squashBuiltinNatural n of
+      Left m -> ExpressionNatural <$> traverseOf builtinNaturalArg go m
+      Right e -> go e
+
     goLet :: Let -> Sem r Let
     goLet Let {..} = do
       clauses' <- mapM goLetClause _letClauses
@@ -268,6 +274,7 @@ weakNormalize' = go
       ExpressionIden i -> goIden i
       ExpressionHole h -> goHole h
       ExpressionInstanceHole h -> goInstanceHole h
+      ExpressionNatural h -> goNatural h
       ExpressionApplication a -> goApp a
       ExpressionLiteral {} -> return e
       ExpressionUniverse {} -> return e
@@ -276,6 +283,12 @@ weakNormalize' = go
       ExpressionLambda {} -> return e
       ExpressionLet {} -> return e
       ExpressionCase {} -> return e
+
+    goNatural :: BuiltinNatural -> Sem r Expression
+    goNatural n = return $ case squashBuiltinNatural n of
+      Left m -> ExpressionNatural m
+      Right e -> e
+
     goIden :: Iden -> Sem r Expression
     goIden i = case i of
       IdenFunction f -> do
@@ -383,13 +396,16 @@ runInferenceState inis = reinterpret (runState inis) $ \case
                 (ExpressionUniverse u, ExpressionUniverse u') -> check (u == u')
                 (ExpressionSimpleLambda a, ExpressionSimpleLambda b) -> goSimpleLambda a b
                 (ExpressionLambda a, ExpressionLambda b) -> goLambda a b
+                (ExpressionNatural a, ExpressionNatural b) -> goNatural a b
                 (ExpressionHole h, a) -> goHole h a
                 (a, ExpressionHole h) -> goHole h a
                 (_, ExpressionLet r) -> go normA (r ^. letExpression)
                 (ExpressionLiteral l, ExpressionLiteral l') -> check (l == l')
                 (ExpressionLiteral l, ExpressionApplication a) -> goUnaryNatLiteral l a
                 (ExpressionApplication a, ExpressionLiteral l) -> goUnaryNatLiteral l a
                 (ExpressionLet l, _) -> go (l ^. letExpression) normB
+                (ExpressionNatural {}, _) -> err
+                (_, ExpressionNatural {}) -> err
                 (ExpressionInstanceHole {}, _) -> err
                 (_, ExpressionInstanceHole {}) -> err
                 (ExpressionSimpleLambda {}, _) -> err
@@ -447,6 +463,11 @@ runInferenceState inis = reinterpret (runState inis) $ \case
                   failWhen (num1 /= num2)
                   inject ok
 
+                goNatural :: BuiltinNatural -> BuiltinNatural -> Sem r (Maybe MatchError)
+                goNatural a b
+                  | a ^. builtinNaturalSuc == b ^. builtinNaturalSuc = go (a ^. builtinNaturalArg) (b ^. builtinNaturalArg)
+                  | otherwise = err
+
                 goHole :: Hole -> Expression -> Sem r (Maybe MatchError)
                 goHole h t = do
                   r <- queryMetavar' h

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs

@@ -278,22 +278,23 @@ lookupInstance' visited ctab tab name params
           modify (HashMap.insert v t)
           return True
 
-squashInstanceNat :: InstanceNat -> Either InstanceNat InstanceParam
-squashInstanceNat n
-  | n ^. instanceNatSuc == 0 = case n ^. instanceNatArg of
-      InstanceParamNatural n' -> squashInstanceNat n'
-      m -> Right m
-  | otherwise = case n ^. instanceNatArg of
-      InstanceParamNatural n' -> case squashInstanceNat n' of
-        Right s -> Left (set instanceNatArg s n)
-        Left s ->
-          Left
-            InstanceNat
-              { _instanceNatSuc = n ^. instanceNatSuc + s ^. instanceNatSuc,
-                _instanceNatArg = s ^. instanceNatArg,
-                _instanceNatLoc = n ^. instanceNatLoc <> s ^. instanceNatLoc
-              }
-      m -> Right m
+-- TODO where to use this?
+-- squashInstanceNat :: InstanceNat -> Either InstanceNat InstanceParam
+-- squashInstanceNat n
+--   | n ^. instanceNatSuc == 0 = case n ^. instanceNatArg of
+--       InstanceParamNatural n' -> squashInstanceNat n'
+--       m -> Right m
+--   | otherwise = case n ^. instanceNatArg of
+--       InstanceParamNatural n' -> case squashInstanceNat n' of
+--         Right s -> Left (set instanceNatArg s n)
+--         Left s ->
+--           Left
+--             InstanceNat
+--               { _instanceNatSuc = n ^. instanceNatSuc + s ^. instanceNatSuc,
+--                 _instanceNatArg = s ^. instanceNatArg,
+--                 _instanceNatLoc = n ^. instanceNatLoc <> s ^. instanceNatLoc
+--               }
+--       m -> Right m
 
 lookupInstance ::
   forall r.