Add simple functions and tests for inductive arithmetic

Author: sColin16

src/structured/termOperations/substituteUnivVar.ml

@@ -74,6 +74,7 @@ and substitute_univ_var_type_rec (variable_num : int)
     =
   (* Get the in_type in the context of the with_type so we can safely substitute
   in the with_type while any recursive type variables in the with_type still reference the same types *)
+  (* TODO: replace this call with a call to get_unified_type_context_pair *)
   let recontextualized_type = get_type_in_context in_type with_type.context in
   (* Substitute the universal type variables in the recontextualized type context *)
   let new_context = substitute_univ_var_context variable_num with_type recontextualized_type.context in

src/structured/termOperations/typing.ml

@@ -55,6 +55,7 @@ and get_type_rec (term : term) (type_context : type_context_map) (level : int)
               match acc with
               | None -> None
               | Some (acc_union_type, acc_recursive_context) ->
+                  (* TODO: investigate replacing this call with a call to get_unified_type_context *)
                   let new_arg_type =
                     get_type_in_context arg_branch_type acc_recursive_context
                   in
@@ -95,6 +96,7 @@ and get_type_rec (term : term) (type_context : type_context_map) (level : int)
       Option.map
         (fun inner_type ->
           let recontextualized_inner =
+            (* TODO: investigate replacing this with a call to get_unified_type_context_pair *)
             get_type_in_context inner_type recursive_context
           in
           build_structured_type

src/structured/typeOperations/context.ml

@@ -11,7 +11,8 @@ and shift_rec_type_vars_base (amount : int) (base_type : base_type) =
   | RecTypeVar n -> RecTypeVar (n + amount)
   | Intersection functions ->
       Intersection (List.map (shift_rec_type_vars_func amount) functions)
-  | UnivQuantification t -> UnivQuantification (shift_rec_type_vars_union amount t)
+  | UnivQuantification t ->
+      UnivQuantification (shift_rec_type_vars_union amount t)
 
 and shift_rec_type_vars_func (amount : int) ((arg, return) : unary_function) =
   (shift_rec_type_vars_union amount arg, shift_rec_type_vars_union amount return)
@@ -20,13 +21,17 @@ and shift_rec_type_vars_context (amount : int) (context : recursive_context) =
   List.map (shift_rec_type_vars_def amount) context
 
 and shift_rec_type_vars_def (amount : int) (recursive_def : recursive_def) =
-  let shifted_union = List.map (fun flat_base ->
-    match flat_base with
-    | FLabel _ | FUnivTypeVar _ -> flat_base
-    | FIntersection functions ->
-        FIntersection (List.map (shift_rec_type_vars_func amount) functions)
-    | FUnivQuantification t -> FUnivQuantification (shift_rec_type_vars_union amount t)
-  ) recursive_def.flat_union in
+  let shifted_union =
+    List.map
+      (fun flat_base ->
+        match flat_base with
+        | FLabel _ | FUnivTypeVar _ -> flat_base
+        | FIntersection functions ->
+            FIntersection (List.map (shift_rec_type_vars_func amount) functions)
+        | FUnivQuantification t ->
+            FUnivQuantification (shift_rec_type_vars_union amount t))
+      recursive_def.flat_union
+  in
   build_recursive_def recursive_def.kind shifted_union
 
 let get_type_in_context (t : structured_type)
@@ -36,4 +41,25 @@ let get_type_in_context (t : structured_type)
   let new_union =
     shift_rec_type_vars_union (List.length recursive_context) t.union
   in
-  build_structured_type new_union (recursive_context @ new_context)
+  build_structured_type new_union (recursive_context @ new_context)
+
+(* Converts a pair of structured types into a pair of union types that share a context *)
+let get_unified_type_context_pair (typea: structured_type) (typeb: structured_type) =
+  let recontextualized_typeb = get_type_in_context typeb typea.context in
+  let new_typeb = recontextualized_typeb.union in
+  ((typea.union, new_typeb), recontextualized_typeb.context)
+
+(* Converts a list of structured types into a list of union types and a common context they all share,
+   shifting recursive type variables in the union as appropriate *)
+let get_unified_type_context (types : structured_type list) =
+  let new_unions_rev, new_context =
+    List.fold_left
+      (fun (acc_union, acc_context) next_type ->
+        let recontextualized_next_union = get_type_in_context next_type acc_context in
+        let new_acc_union = recontextualized_next_union :: acc_union in
+        let new_acc_context = recontextualized_next_union.context in
+        (new_acc_union, new_acc_context))
+      ([], []) types in
+  (* We must reverse the list of unions since we fold left but want to keep the types in the right order *)
+  let new_unions = List.rev new_unions_rev in
+  new_unions, new_context

src/structured/typeOperations/union.ml

@@ -12,6 +12,7 @@ let get_type_union (types : structured_type list) : structured_type =
       (fun (acc_union_type, acc_recursive_context) next_type ->
         (* Get the next type in the accumulated context to obtain the joined context
            and the next type in the context of that new accumulated context *)
+        (* TODO: investigate replacing this with a call to get_unified_type_context *)
         let new_type = get_type_in_context next_type acc_recursive_context in
         (* Append this union to the accumulated union, use the new context from above *)
         (acc_union_type @ new_type.union, new_type.context))

src/structuredArithmetic.ml

@@ -57,8 +57,8 @@ let decrement =
          (seven.stype, six.term);
        ])
 
-let fix_binary_num_op = fix three_bit_type.union unary_num_op.union
-let fix_unary_num_op = fix three_bit_type.union three_bit_type.union
+let fix_binary_num_op = fix three_bit_type unary_num_op
+let fix_unary_num_op = fix three_bit_type three_bit_type
 
 let add =
   get_typed_term_unsafe

src/structuredHelpers.ml

@@ -3,6 +3,7 @@ open Structured.TermTypes
 open Structured.TypeOperations.Create
 open Structured.TermOperations.Typing
 open Structured.TypeOperations.Union
+open TypeOperations.Context
 
 type typed_term = { term : term; stype : structured_type }
 
@@ -46,39 +47,56 @@ let get_flat_union_type (union_types : structured_type list) : flat_union_type =
 
 (* Constructs the Z-combinator for a function of a given type, a fixed-point
     combinator for call-by-value semantics *)
-let build_fix (arg_type : union_type) (return_type : union_type) =
-  let func_type = (func_to_structured_type (arg_type, return_type)).union in
-  let fix_context =
-    build_recursive_context
-      [ (Coinductive, [ FIntersection [ ([ RecTypeVar 0 ], func_type) ] ]) ]
+let build_fix (arg_type : structured_type) (return_type : structured_type) =
+  (* First, construct a function type from the arg type to the return type, taking
+     care to properly join the contexts of the two types *)
+  let (new_arg_type, new_return_type), shared_context =
+    get_unified_type_context_pair arg_type return_type
   in
+  let func_type =
+    build_structured_type
+      [ Intersection [ (new_arg_type, new_return_type) ] ]
+      shared_context
+  in
+  (* Next, build the recursive definition that we'll add to the end of the joined context *)
+  let rec_var_num = List.length shared_context in
+  let fix_rec_def =
+    build_recursive_def Coinductive
+      [ FIntersection [ ([ RecTypeVar rec_var_num ], func_type.union) ] ]
+  in
+  (* Then add that definition to the end of the context so it has the number we assigned it *)
+  let new_shared_context = List.append shared_context [ fix_rec_def ] in
   let fix =
     get_typed_term_unsafe
       (Abstraction
          [
-           ( func_to_structured_type (func_type, func_type),
+           ( build_structured_type
+               [ Intersection [ (func_type.union, func_type.union) ] ]
+               new_shared_context,
              Application
                ( Abstraction
                    [
-                     ( build_structured_type [ RecTypeVar 0 ] fix_context,
+                     ( build_structured_type [ RecTypeVar rec_var_num ]
+                         new_shared_context,
                        Application
                          ( Variable 1,
                            Abstraction
                              [
-                               ( union_to_structured_type arg_type,
+                               ( build_structured_type new_arg_type new_shared_context,
                                  Application
                                    ( Application (Variable 1, Variable 1),
                                      Variable 0 ) );
                              ] ) );
                    ],
                  Abstraction
                    [
-                     ( build_structured_type [ RecTypeVar 0 ] fix_context,
+                     ( build_structured_type [ RecTypeVar rec_var_num ]
+                         new_shared_context,
                        Application
                          ( Variable 1,
                            Abstraction
                              [
-                               ( union_to_structured_type arg_type,
+                               ( build_structured_type new_arg_type new_shared_context,
                                  Application
                                    ( Application (Variable 1, Variable 1),
                                      Variable 0 ) );
@@ -89,6 +107,7 @@ let build_fix (arg_type : union_type) (return_type : union_type) =
   fix
 
 (* Fixes a provided abstraction with the given arg and return type *)
-let fix (arg_type : union_type) (return_type : union_type) (term : term) =
+let fix (arg_type : structured_type) (return_type : structured_type)
+    (term : term) =
   let fix_term = build_fix arg_type return_type in
   Application (fix_term.term, term)

src/structuredMixed.ml

@@ -30,7 +30,7 @@ let is_zero =
            false_lambda.term );
        ])
 
-let fix_even_odd = fix is_even_odd_label.union num_to_bool.union
+let fix_even_odd = fix is_even_odd_label num_to_bool
 
 let is_even_odd =
   get_typed_term_unsafe

src/structuredPoly.ml

@@ -181,3 +181,18 @@ let tail =
               Application (Variable 0, next_label.term) );
             (empty_list.stype, none_label.term)
           ]))
+
+(* List functions we should implement:
+ * Length
+ * nth
+ * reverse
+ * concat
+ * append (add a single element to the end)
+ * flatten
+ * equal
+ * map
+ * filter
+ * fold_left/fold_right
+ * find (return element and/or index)
+ * forall/exists
+*)

src/structuredRecursive.ml

@@ -3,6 +3,7 @@ open Structured.TermTypes
 open Structured.TypeOperations.Create
 open TypeOperations.Union
 open StructuredHelpers
+open StructuredBool
 
 let name = get_typed_term_unsafe (Const "Name")
 let val_lambda = get_typed_term_unsafe (Const "Val")
@@ -192,3 +193,151 @@ let neg_infinity =
        [ (Coinductive, get_flat_union_type [ generate_pred_rec_step 1 ]) ])
 
 let infinity = get_type_union [ pos_infinity; neg_infinity ]
+
+let unary_numerical_op =
+  build_structured_type
+    [ Intersection [ (ind_integer.union, ind_integer.union) ] ]
+    ind_integer.context
+
+let binary_numerical_op =
+  build_structured_type
+    [
+      Intersection
+        [
+          ( ind_integer.union,
+            [ Intersection [ (ind_integer.union, ind_integer.union) ] ] );
+        ];
+    ]
+    ind_integer.context
+
+let num_to_bool_op =
+  build_structured_type
+    [ Intersection [ (ind_integer.union, bool_type.union) ] ]
+    ind_integer.context
+
+let binary_num_to_bool_op =
+  build_structured_type
+    [
+      Intersection
+        [
+          ( ind_integer.union,
+            [ Intersection [ (ind_integer.union, bool_type.union) ] ] );
+        ];
+    ]
+    ind_integer.context
+
+(* Increments an inductive number by one *)
+let increment =
+  get_typed_term_unsafe
+    (Abstraction
+       [
+         (ind_negative_number, Application (Variable 0, val_lambda.term));
+         ( get_type_union [ zero.stype; ind_positive_number ],
+           Abstraction
+             [ (name.stype, succ.term); (val_lambda.stype, Variable 1) ] );
+       ])
+
+(* Decrements an inductive number by one *)
+let decrement =
+  get_typed_term_unsafe
+    (Abstraction
+       [
+         ( get_type_union [ zero.stype; ind_negative_number ],
+           Abstraction
+             [ (name.stype, pred.term); (val_lambda.stype, Variable 1) ] );
+         (ind_positive_number, Application (Variable 0, val_lambda.term));
+       ])
+
+(* Determines if a value is even or odd, leveraging the subtyping system *)
+let is_even =
+  get_typed_term_unsafe
+    (Abstraction
+       [
+         (ind_even_integer, true_lambda.term);
+         (ind_odd_integer, false_lambda.term);
+       ])
+
+let fix_binary_num_to_bool = fix ind_integer num_to_bool_op
+let fix_binary_num_op = fix ind_integer unary_numerical_op
+
+let is_equal =
+  get_typed_term_unsafe
+    (fix_binary_num_to_bool
+       (Abstraction
+          [
+            ( binary_num_to_bool_op,
+              Abstraction
+                [
+                  ( zero.stype,
+                    Abstraction
+                      [
+                        ( get_type_union
+                            [ ind_positive_number; ind_negative_number ],
+                          false_lambda.term );
+                        (zero.stype, true_lambda.term);
+                      ] );
+                  ( ind_positive_number,
+                    Abstraction
+                      [
+                        ( get_type_union [ zero.stype; ind_negative_number ],
+                          false_lambda.term );
+                        ( ind_positive_number,
+                          Application
+                            ( Application
+                                ( Variable 2,
+                                  Application (decrement.term, Variable 1) ),
+                              Application (decrement.term, Variable 0) ) );
+                      ] );
+                  ( ind_negative_number,
+                    Abstraction
+                      [
+                        ( get_type_union [ zero.stype; ind_positive_number ],
+                          false_lambda.term );
+                        ( ind_negative_number,
+                          Application
+                            ( Application
+                                ( Variable 2,
+                                  Application (increment.term, Variable 1) ),
+                              Application (increment.term, Variable 0) ) );
+                      ] );
+                ] );
+          ]))
+
+let add =
+  get_typed_term_unsafe
+    (fix_binary_num_op
+       (Abstraction
+          [
+            ( binary_numerical_op,
+              Abstraction
+                [
+                  (zero.stype, Abstraction [ (ind_integer, Variable 0) ]);
+                  ( ind_negative_number,
+                    Abstraction
+                      [
+                        ( ind_integer,
+                          Application
+                            ( Application
+                                ( Variable 2,
+                                  Application (increment.term, Variable 1) ),
+                              Application (decrement.term, Variable 0) ) );
+                      ] );
+                  ( ind_positive_number,
+                    Abstraction
+                      [
+                        ( ind_integer,
+                          Application
+                            ( Application
+                                ( Variable 2,
+                                  Application (decrement.term, Variable 1) ),
+                              Application (increment.term, Variable 0) ) );
+                      ] );
+                ] );
+          ]))
+
+(* Later, consider also implementing these functions *)
+(* subtract *)
+(* fibonnaci *)
+(* negate *)
+(* multiply *)
+(* divide *)

src/structuredUnions.ml

@@ -122,7 +122,7 @@ let decrement_three_bit =
          (zero.stype, seven.term);
        ])
 
-let fix_binary_num_op = fix three_bit_num.union unary_num_type.union
+let fix_binary_num_op = fix three_bit_num unary_num_type
 
 let add_three_bit =
   get_typed_term_unsafe