Add type annotations to array introductions

spec/src/lang/core/base.makam

@@ -40,7 +40,7 @@ int_intro : int -> term.
 
 % Arrays
 array_type : term -> term -> term.
-array_intro : list term -> term.
+array_intro : list term -> term -> term.
 array_elim : term -> term -> term.
 
 % Binary format descriptions

spec/src/lang/core/binary.makam

@@ -25,7 +25,7 @@
     interpret format_intro_s32be (int_intro TODO) [ Byte0, Byte1, Byte2, Byte3 ].
     interpret format_intro_s64le (int_intro TODO) [ Byte0, Byte1, Byte2, Byte3, Byte4, Byte5, Byte6, Byte7, Byte8 ].
     interpret format_intro_s64be (int_intro TODO) [ Byte0, Byte1, Byte2, Byte3, Byte4, Byte5, Byte6, Byte7, Byte8 ].
-    interpret (format_intro_array ElemType Len) (array_intro TODO) Bytes.
+    interpret (format_intro_array Type Len) (array_intro TODO Type) Bytes.
     interpret
         (format_intro_record (field_closure Values (( Label, Type ) :: TypeFields)))
         (record_intro (( Label, Elem ) :: ElemFields) TODO)

spec/src/lang/core/semantics.makam

@@ -57,7 +57,7 @@
 
     % Arrays
     array_type : value -> value -> value.
-    array_intro : list value -> value.
+    array_intro : list value -> value -> value.
 
     % Binary format descriptions
     format_type : value.
@@ -140,14 +140,15 @@
     eval Values (enum_elim Clauses) (enum_elim (choice_closure Values Clauses)).
     eval Values int_type int_type.
     eval Values (int_intro Int) (int_intro Int).
-    eval Values (array_type ElemType LenElem) (array_type ElemType' LenValue) :-
-        eval Values ElemType ElemType',
-        eval Values LenElem LenValue.
-    eval Values (array_intro Elems) (array_intro ElemValues) :-
-        map (fun elem value => eval Values elem value) Elems ElemValues.
+    eval Values (array_type Type LenElem) (array_type Type' LenElem') :-
+        eval Values Type Type',
+        eval Values LenElem LenElem'.
+    eval Values (array_intro Elems Type) (array_intro Elems' Type') :-
+        map (pfun Elem Elem' => eval Values Elem Elem') Elems Elems',
+        eval Values Type Type'.
     % FIXME: This breaks for neutral terms! We should use `array_elim` here.
     eval Values (array_elim ArrayElem IndexElem) ElemValue :-
-        eval Values ArrayElem (array_intro ElemValues),
+        eval Values ArrayElem (array_intro ElemValues _),
         eval Values IndexElem (int_intro Index),
         list.nth ElemValues Index ElemValue.
     eval Values format_type format_type.
@@ -167,8 +168,8 @@
     eval Values format_intro_s32be format_intro_s32be.
     eval Values format_intro_s64le format_intro_s64le.
     eval Values format_intro_s64be format_intro_s64be.
-    eval Values (format_intro_array ElemType LenElem) (format_intro_array ElemType' LenElem') :-
-        eval Values ElemType ElemType',
+    eval Values (format_intro_array Type LenElem) (format_intro_array Type' LenElem') :-
+        eval Values Type Type',
         eval Values LenElem LenElem'.
     eval Values (format_intro_record TypeFields) (format_intro_record (field_closure Values TypeFields)).
     eval Values (format_intro_compute Elem Type) (format_intro_compute Elem' Type') :-
@@ -307,11 +308,12 @@
         )) Clauses Clauses'.
     readback Length int_type int_type.
     readback Length (int_intro Int) (int_intro Int).
-    readback Length (array_type ElemValue LenValue) (array_type ElemType LenElem) :-
-        readback Length ElemValue ElemType,
-        readback Length LenValue LenElem.
-    readback Length (array_intro ElemValues) (array_intro Elems) :-
-        map (fun value term => readback Length value term) ElemValues Elems.
+    readback Length (array_type Type LenElem) (array_type Type' LenElem') :-
+        readback Length Type Type',
+        readback Length LenElem LenElem'.
+    readback Length (array_intro Elems Type) (array_intro Elems' Type') :-
+        map (pfun Elem Elem' => readback Length Elem Elem') Elems Elems',
+        readback Length Type Type'.
     readback Length format_type format_type.
     readback Length format_intro_void format_intro_void.
     readback Length format_intro_unit format_intro_unit.
@@ -443,8 +445,9 @@
     is_equal Length (array_type ElemType1 LenElem1) (array_type ElemType2 LenElem2) :-
         is_equal Length ElemType1 ElemType2,
         is_equal Length LenElem1 LenElem2.
-    is_equal Length (array_intro ElemValues1) (array_intro ElemValues2) :-
-        map (fun value1 value2 => is_equal Length value1 value2) ElemValues1 ElemType2.
+    is_equal Length (array_intro Elems1 ElemType1) (array_intro Elems2 ElemType2) :-
+        map (pfun Elem1 Elem2 => is_equal Length Elem1 Elem2) Elems1 Elems2,
+        is_equal Length ElemType1 ElemType2.
     is_equal Length format_type format_type.
     is_equal Length format_intro_void format_intro_void.
     is_equal Length format_intro_unit format_intro_unit.

spec/src/lang/core/typing/bidirectional.makam

@@ -197,9 +197,11 @@
     synth_type Context (array_type Type LenElem) type_type :-
         check_type Context Type type_type,
         check_type Context LenElem int_type.
-    check_type Context (array_intro Elems) (array_type Type (int_intro Len)) :-
+    synth_type Context (array_intro Elems Type) (array_type Type' (int_intro Len)) :-
         length Elems Len,
-        map (fun elem => check_type Context elem Type) Elems.
+        check_type Context Type type_type,
+        context.eval Context Type Type',
+        map (pfun Elem => check_type Context Elem Type') Elems.
     synth_type Context (array_elim ArrayElem IndexElem) Type :-
         % FIXME: ensure `IndexElem` is in array bounds, possibly with refinement types?
         synth_type Context ArrayElem (array_type Type _),

spec/src/lang/core/typing/declarative.makam

@@ -136,14 +136,14 @@
     is_elem Context (array_type Type LenElem) type_type :-
         is_elem Context Type type_type,
         is_elem Context LenElem int_type.
-    is_elem Context (array_intro Elems) (array_type Type LenElem) :-
+    is_elem Context (array_intro Elems Type) (array_type Type LenElem) :-
         is_equal_elem Context (int_intro Len) LenElem int_type,
         length Elems Len,
-        map (fun elem => is_elem Context elem Type) Elems.
-    is_equal_elem Context (array_elim (array_intro Elems) IndexElem) Elem Type :-
+        map (pfun Elem => is_elem Context Elem Type) Elems.
+    is_equal_elem Context (array_elim (array_intro Elems Type) IndexElem) Elem Type :-
         % FIXME: ensure `IndexElem` is in array bounds, possibly with refinement types?
         is_equal_elem Context (int_intro Index) IndexElem int_type,
-        map (fun elem => is_elem Context elem Type) Elems,
+        map (pfun Elem => is_elem Context Elem Type) Elems,
         list.nth Elems Index Elem.
 
     % Binary format descriptions

spec/src/lang/stratified.makam

@@ -70,7 +70,7 @@
 
     % Arrays
     array_type : term1 -> term0 -> term1.
-    array_intro : list term0 -> term0.
+    array_intro : list term0 -> term1 -> term0.
     array_elim : term0 -> term0 -> term0.
 
     % Singletons
@@ -86,10 +86,10 @@
     singleton_intro_arrow : term1 -> term1 -> term1.        % Arrow singletons
     singleton_intro_forall_2 : term1 -> term1 -> term1.     % Universal quantification over level-2 variables
     singleton_intro_forall_1 : term1 -> term1 -> term1.     % Universal quantification over level-1 variables
-    singleton_intro_record : map string term1 -> term1.     % Record singletons
+    singleton_intro_record : map string term1 -> list (string * term1) -> term1. % Record singletons
     singleton_intro_enum : string -> set string -> term1.   % Enumeration singletons
     singleton_intro_int : int -> term1.                     % Integer singletons
-    singleton_intro_array : list term1 -> term1.            % Array Singletons
+    singleton_intro_array : list term1 -> term1 -> term1.   % Array Singletons
 
     % Binary format descriptions
     %
@@ -140,7 +140,7 @@
     enum_intro : string -> set string ->  expr. % Enumeration introductions
     enum_elim : map string expr -> expr.        % Enumeration eliminations
     int_intro : int -> expr.                    % Integer introductions
-    array_intro : list expr -> expr.            % Array introductiona
+    array_intro : list expr -> term0 -> expr.   % Array introductiona
     array_elim : expr -> expr -> expr.          % Array eliminations
 
 %end.

spec/src/pass/core_to_stratified.makam

@@ -137,7 +137,10 @@
     :-
         from_term_to_term1 Context SourceType TargetType,
         from_term_to_term0 Context SourceLenElem TargetLenElem.
-    from_term Context (core.array_intro SourceElems) (term0 (stratified.array_intro TargetElems)) :-
+    from_term Context (core.array_intro SourceElems SourceType)
+        (term0 (stratified.array_intro TargetElems TargetType))
+    :-
+        from_term_to_term1 Context SourceType TargetType,
         map (pfun SourceElem TargetElem =>
             from_term_to_term0 Context SourceElem TargetElem
         ) SourceElems TargetElems.

spec/test/lang/core/semantics.makam

@@ -68,7 +68,7 @@
 >> normalize [ int_intro 2, int_intro 1, int_type ]
     (record_intro
         [ ( "len", local 0 )
-        , ( "data", array_intro [local 1, int_intro 2] )
+        , ( "data", array_intro [local 1, int_intro 2] (local 2) )
         ]
         [ ( "len", int_type )
         , ( "data", array_type (local 3) (local 0) )
@@ -78,7 +78,7 @@
 >> Term :=
     record_intro
         [ ( "len", int_intro 2 )
-        , ( "data", array_intro [int_intro 1, int_intro 2] )
+        , ( "data", array_intro [int_intro 1, int_intro 2] int_type )
         ]
         [ ( "len", int_type )
         , ( "data", array_type int_type (local 0) )
@@ -88,7 +88,7 @@
     (record_elim
         (record_intro
             [ ( "len", int_intro 2 )
-            , ( "data", array_intro [int_intro 1, int_intro 2] )
+            , ( "data", array_intro [int_intro 1, int_intro 2] int_type )
             ]
             [ ( "len", int_type )
             , ( "data", array_type int_type (local 0) )
@@ -102,15 +102,15 @@
     (record_elim
         (record_intro
             [ ( "len", int_intro 2 )
-            , ( "data", array_intro [int_intro 1, int_intro 2] )
+            , ( "data", array_intro [int_intro 1, int_intro 2] int_type )
             ]
             [ ( "len", int_type )
             , ( "data", array_type int_type (local 0) )
             ])
         "data")
     Term ?
 >> Yes:
->> Term := array_intro [int_intro 1, int_intro 2].
+>> Term := array_intro [int_intro 1, int_intro 2] int_type.
 
 >> normalize [ neutral (local 0) ] (record_elim (local 0) "data") Term ?
 >> Yes:
@@ -206,20 +206,21 @@
 >> Yes:
 >> Term := array_type int_type (int_intro 42).
 
->> normalize (array_intro []) Term ?
+>> normalize (array_intro [] int_type) Term ?
 >> Yes:
->> Term := array_intro [].
+>> Term := array_intro [] int_type.
 
->> normalize [ int_intro 25, int_intro 30 ] (array_intro [ local 0, local 1 ]) Term ?
+>> normalize [ int_intro 25, int_intro 30, int_type ] (array_intro [ local 0, local 1 ] (local 2)) Term ?
 >> Yes:
->> Term := array_intro [int_intro 25, int_intro 30].
+>> Term := array_intro [int_intro 25, int_intro 30] int_type.
 
 >> normalize
     [ int_intro 1
     , int_intro 25
     , int_intro 30
+    , int_type
     ]
-    (array_elim (array_intro [ local 1, local 2 ]) (local 0))
+    (array_elim (array_intro [ local 1, local 2 ] (local 3)) (local 0))
     Term ?
 >> Yes:
 >> Term := int_intro 30.

spec/test/lang/core/typing/bidirectional.makam

@@ -71,7 +71,7 @@
 >> synth_type
     (ann
         (record_intro
-            [ ( "data", array_intro [] )
+            [ ( "data", array_intro [] (enum_type [ "unit" ]) )
             , ( "len", int_intro 0 )
             ]
             [ ( "len", int_type )
@@ -92,7 +92,13 @@
 >> synth_type
     (ann
         (record_intro
-            [ ( "data", array_intro [ enum_intro "unit" [ "unit" ], enum_intro "unit" [ "unit" ] ])
+            [ ( "data"
+              , array_intro
+                [ enum_intro "unit" [ "unit" ]
+                , enum_intro "unit" [ "unit" ]
+                ]
+                (enum_type [ "unit" ])
+              )
             , ( "len", int_intro 2 )
             ]
             [ ( "len", int_type )
@@ -256,7 +262,7 @@
 
 >> synth_type
     (record_intro
-        [ ( "data", array_intro [] )
+        [ ( "data", array_intro [] (enum_type [ "unit" ]) )
         , ( "len", int_intro 0 )
         ]
         [ ( "len", int_type )
@@ -278,6 +284,7 @@
                 [ enum_intro "unit" [ "unit" ]
                 , enum_intro "unit" [ "unit" ]
                 ]
+                (enum_type [ "unit" ])
           )
         , ( "len", int_intro 2 )
         ]
@@ -333,6 +340,7 @@
                     [ enum_intro "unit" [ "unit" ]
                     , enum_intro "unit" [ "unit" ]
                     ]
+                    (enum_type [ "unit" ])
                 )
             , ( "len", int_intro 2 )
             ]
@@ -442,11 +450,13 @@
 
     % Arrays
 
->> check_type (array_intro []) (array_type int_type (int_intro 0)) ?
->> Yes.
+>> synth_type (array_intro [] int_type) Type ?
+>> Yes:
+>> Type := array_type int_type (int_intro 0).
 
->> check_type (array_intro [int_intro 1, int_intro 2, int_intro 3]) (array_type int_type (int_intro 3)) ?
->> Yes.
+>> synth_type (array_intro [int_intro 1, int_intro 2, int_intro 3] int_type) Type ?
+>> Yes:
+>> Type := array_type int_type (int_intro 3).
 
     % Binary format descriptions
 

spec/test/pass/core_to_stratified.makam

@@ -94,7 +94,13 @@
 
 >> from_term
     (core.record_intro
-        [ ( "data", core.array_intro [ core.record_intro [] [], core.record_intro [] [] ] )
+        [ ( "data",
+            core.array_intro
+                [ core.record_intro [] []
+                , core.record_intro [] []
+                ]
+                core.int_type
+          )
         , ( "len", core.int_intro 2 )
         ]
         [ ( "len", core.int_type )
@@ -110,6 +116,7 @@
                 [ stratified.record_intro [] []
                 , stratified.record_intro [] []
                 ]
+                stratified.int_type
           )
         ]
         [ ( "len", stratified.int_type )