Implement and test every (forall) list function

Author: sColin16

src/structuredPoly.ml

@@ -498,9 +498,37 @@ let fold_left =
                       ] );
                 ]))))
 
+let fold_left_poly_bool =
+  typed_term
+    (UnivApplication
+       (UnivApplication (fold_left.term, base_type (UnivTypeVar 0)), bool_type))
+
+let every =
+   typed_term
+     (UnivQuantifier
+        (Abstraction
+           [
+             ( poly_to_bool_op,
+               Abstraction
+                 [
+                   ( polymoprhic_list_type.full,
+                     trinary_apply fold_left_poly_bool.term
+                       (Abstraction
+                          [
+                            ( bool_type,
+                              Abstraction
+                                [
+                                  ( base_type (UnivTypeVar 0),
+                                    binary_apply and_lambda.term (Variable 1)
+                                      (Application (Variable 3, Variable 0)) );
+                                ] );
+                          ])
+                       true_lambda.term (Variable 0) );
+                 ] );
+           ]))
+
 (* List functions we should implement:
- * fold_left/fold_right
- * forall/exists
+ * exists
  * equal
  * find (return element and/or index)
  * flatten

test/structuredLambdaPoly.ml

@@ -202,6 +202,8 @@ let fold_int_int =
   typed_term
     (UnivApplication (UnivApplication (fold_left.term, ind_integer), ind_integer))
 
+let every_int = typed_term (UnivApplication (every.term, ind_integer))
+
 let true_predicate =
   typed_term
     (UnivQuantifier
@@ -218,6 +220,22 @@ let true_predicate_int =
 let false_predicate_int =
   typed_term (UnivApplication (false_predicate.term, ind_integer))
 
+(* Represents `forall X. (X -> Bool) -> X List -> Bool`, the type for every and exists *)
+let list_predicate_type =
+  map_type
+    (fun list ->
+      [
+        UnivQuantification
+          [
+            Intersection
+              [
+                ( [ Intersection [ ([ UnivTypeVar 0 ], bool_type.union) ] ],
+                  [ Intersection [ (list, bool_type.union) ] ] );
+              ];
+          ];
+      ])
+    polymoprhic_list_type.full
+
 let () =
   test "Polymoprhic identity function type"
     (is_equivalent_type polymoprhic_identity.stype expected_poly_identity_type)
@@ -574,3 +592,31 @@ let () =
        (trinary_apply fold_int_int.term add.term zero.term
           incrementing_integer_list.term)
        (num_term 10))
+
+let () =
+  test "Every function has the right type"
+    (is_subtype every.stype list_predicate_type)
+
+let () =
+  test "Every function called on empty list returns true"
+    (evaluates_to
+       (binary_apply every_int.term is_even.term empty_list.term)
+       true_lambda.term)
+
+let () =
+  test "Every is_even on simple list is false"
+    (evaluates_to
+       (binary_apply every_int.term is_even.term simple_integer_list.term)
+       false_lambda.term)
+
+let () =
+  test "Every is_positive on incrementing integer list is true"
+    (evaluates_to
+       (binary_apply every_int.term
+          (Abstraction
+             [
+               (ind_positive_number, true_lambda.term);
+               (ind_non_positive_number, false_lambda.term);
+             ])
+          incrementing_integer_list.term)
+       true_lambda.term)