Merge

src/Core/Binary.idr

@@ -30,7 +30,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 40
+ttcVersion = 41
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/TTImp/Elab/Record.idr

@@ -261,7 +261,7 @@ elabInstance env fc n fs
          (Just allfields) <- findFieldsExplicit defs fullname
                | _ => throw (NotRecordType fc n)
          fs' <- sequence $ map (sequenceCore . bimap getName getExp . dup) fs
-         seqexp <- sequence $ map (\x => [| pure (lookup x fs') `orElse` throw (NotCoveredField fc x) |]) allfields
+         seqexp <- sequence $ map (\x => lookupOrElse x fs' (throw (NotCoveredField fc x))) allfields
          pure $ (foldl (IApp fc) (IVar fc fullname) seqexp)
   where
     sequenceCore : (Core a, Core b) -> Core (a, b) --specialize
@@ -279,9 +279,12 @@ elabInstance env fc n fs
     bimap : forall a, b, a', b'. (a -> a') -> (b -> b') -> (a, b) -> (a', b')
     bimap f g (x, y) = (f x, g y)
 
-    orElse : forall a. Maybe a -> Lazy a -> a
-    orElse (Just x) _ = x
-    orElse Nothing x = x
+    lookupOrElse : forall a. Eq a => a -> List (a, b) -> Core b -> Core b
+    lookupOrElse x xs def 
+        = case lookup x xs of
+               Nothing => def
+               (Just x) => pure x
+
 
     subsetOf : forall a. Eq a => List a -> List a -> Bool
     subsetOf subset set = length (intersect subset set) == length subset

tests/Main.idr

@@ -95,7 +95,7 @@ idrisTests
        "real001", "real002",
        -- Records, access and dependent update
        "record001", "record002", "record003", "record004", "record005",
-       "record007",
+       "record007", "record006",
        -- Quotation and reflection
        "reflection001", "reflection002", "reflection003", "reflection004",
        "reflection005", "reflection006", "reflection007", "reflection008",

tests/idris2/record006/Fld.idr

@@ -0,0 +1,48 @@
+module Fld
+
+namespace SuperDog
+   public export
+   record SuperDog where
+      constructor MkDog
+      supername : String
+      age : Int
+      weight : Int
+
+namespace OrdinaryDog
+   public export
+   record OrdinaryDog where
+      constructor MkDog
+      name : String
+      age : Int
+      weight : Int
+
+record Other a where
+   constructor MkOther
+   {imp : String}
+   fieldA : a
+   fieldB : b
+
+
+myDog_notWorking : record MkDog {name = "Sam"} -- Not all fields are covered
+
+myDog_notWorking2 : record MkDog 
+                     { age = 4
+                     , age = 2
+                     , weight = 12
+                     , name = "Sam" } -- Duplicate names
+ 
+myDog : ?
+myDog = record MkDog { age = 4
+                     , weight = 12
+                     , name = "Sam" } --Disambiguation by unique fields
+
+mySuperDog : ?
+mySuperDog = record MkDog { age = 3
+                          , weight = 10
+                          , supername = "Super-Sam" } --Disambiguation by unique fields
+
+other : ? -- Elaborates as (MkOther (fromString "hi") (the Int 1) {imp = fromString "Secret string"})
+other = record MkOther {fieldB = the Int 1, fieldA = "hi"} {imp = "Secret string"}
+
+same : record MkDog {name = "Rex", age = 2, weight = 10} = MkDog "Rex" 2 10
+same = Refl

tests/idris2/record006/expected

@@ -0,0 +1,18 @@
+1/1: Building Fld (Fld.idr)
+Error: While processing type of myDog_notWorking. Field not covered age.
+
+Fld.idr:26:20--26:47
+    |
+ 26 | myDog_notWorking : record MkDog {name = "Sam"} -- Not all fields are covered
+    |                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Error: While processing type of myDog_notWorking2. Duplicate fields.
+
+Fld.idr:28:21--32:38
+ 28 | myDog_notWorking2 : record MkDog 
+ 29 |                      { age = 4
+ 30 |                      , age = 2
+ 31 |                      , weight = 12
+ 32 |                      , name = "Sam" } -- Duplicate names
+
+Fld> Bye for now!

tests/idris2/record006/input

@@ -0,0 +1 @@
+:q

tests/idris2/record006/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner Fld.idr < input
+
+rm -rf build