Rename structured_type -> recursive_type

Author: sColin16

example/boolean.ml

@@ -4,7 +4,7 @@ open TypeOperations.Create
 
 let true_lambda = typed_term (Const "True")
 let false_lambda = typed_term (Const "False")
-let bool_type = type_union [ true_lambda.stype; false_lambda.stype ]
+let bool_type = type_union [ true_lambda.rtype; false_lambda.rtype ]
 let unary_bool_op = func_type (bool_type.union, bool_type.union)
 
 let binary_bool_op =
@@ -20,34 +20,34 @@ let not_lambda =
   typed_term
     (Abstraction
        [
-         (true_lambda.stype, false_lambda.term);
-         (false_lambda.stype, true_lambda.term);
+         (true_lambda.rtype, false_lambda.term);
+         (false_lambda.rtype, true_lambda.term);
        ])
 
 let and_lambda =
   typed_term
     (Abstraction
        [
-         (true_lambda.stype, identity_lambda.term);
-         (false_lambda.stype, Abstraction [ (bool_type, false_lambda.term) ]);
+         (true_lambda.rtype, identity_lambda.term);
+         (false_lambda.rtype, Abstraction [ (bool_type, false_lambda.term) ]);
        ])
 
 let or_lambda =
   typed_term
     (Abstraction
        [
-         (true_lambda.stype, Abstraction [ (bool_type, true_lambda.term) ]);
-         (false_lambda.stype, identity_lambda.term);
+         (true_lambda.rtype, Abstraction [ (bool_type, true_lambda.term) ]);
+         (false_lambda.rtype, identity_lambda.term);
        ])
 
 let if_lambda =
   typed_term
     (Abstraction
        [
-         ( true_lambda.stype,
+         ( true_lambda.rtype,
            Abstraction [ (bool_type, Abstraction [ (bool_type, Variable 1) ]) ]
          );
-         ( false_lambda.stype,
+         ( false_lambda.rtype,
            Abstraction [ (bool_type, Abstraction [ (bool_type, Variable 0) ]) ]
          );
        ])

example/exampleHelpers.ml

@@ -6,13 +6,13 @@ open TypeOperations.Union
 open TypeOperations.Context
 open TermOperations.Helpers
 
-type typed_term = { term : term; stype : structured_type }
+type typed_term = { term : term; rtype : recursive_type }
 
-let build_typed_term (term : term) (stype : structured_type) = { term; stype }
+let build_typed_term (term : term) (rtype : recursive_type) = { term; rtype }
 let get_type_unsafe term = Option.get (get_type term)
 let typed_term term = build_typed_term term (get_type_unsafe term)
 
-let type_intersection (types : structured_type list) : structured_type =
+let type_intersection (types : recursive_type list) : recursive_type =
   let intersection =
     List.fold_left
       (fun acc_intersection next_type ->
@@ -23,7 +23,7 @@ let type_intersection (types : structured_type list) : structured_type =
   in
   base_type (Intersection intersection)
 
-let get_flat_union_type (union_types : structured_type list) : flat_union_type =
+let get_flat_union_type (union_types : recursive_type list) : flat_union_type =
   let union_type = type_union union_types in
   List.map
     (function
@@ -36,14 +36,14 @@ 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 : structured_type) (return_type : structured_type) =
+let build_fix (arg_type : recursive_type) (return_type : recursive_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
+    build_recursive_type
       [ Intersection [ (new_arg_type, new_return_type) ] ]
       shared_context
   in
@@ -59,33 +59,33 @@ let build_fix (arg_type : structured_type) (return_type : structured_type) =
     typed_term
       (Abstraction
          [
-           ( build_structured_type
+           ( build_recursive_type
                [ Intersection [ (func_type.union, func_type.union) ] ]
                new_shared_context,
              Application
                ( Abstraction
                    [
-                     ( build_structured_type [ RecTypeVar rec_var_num ]
+                     ( build_recursive_type [ RecTypeVar rec_var_num ]
                          new_shared_context,
                        Application
                          ( Variable 1,
                            Abstraction
                              [
-                               ( build_structured_type new_arg_type
+                               ( build_recursive_type new_arg_type
                                    new_shared_context,
                                  binary_apply (Variable 1) (Variable 1)
                                    (Variable 0) );
                              ] ) );
                    ],
                  Abstraction
                    [
-                     ( build_structured_type [ RecTypeVar rec_var_num ]
+                     ( build_recursive_type [ RecTypeVar rec_var_num ]
                          new_shared_context,
                        Application
                          ( Variable 1,
                            Abstraction
                              [
-                               ( build_structured_type new_arg_type
+                               ( build_recursive_type new_arg_type
                                    new_shared_context,
                                  binary_apply (Variable 1) (Variable 1)
                                    (Variable 0) );
@@ -96,7 +96,7 @@ let build_fix (arg_type : structured_type) (return_type : structured_type) =
   fix
 
 (* Fixes a provided abstraction with the given arg and return type *)
-let fix (arg_type : structured_type) (return_type : structured_type)
+let fix (arg_type : recursive_type) (return_type : recursive_type)
     (term : term) =
   let fix_term = build_fix arg_type return_type in
   Application (fix_term.term, term)

example/mixed.ml

@@ -7,24 +7,24 @@ open TermOperations.Helpers
 
 let is_even_label = typed_term (Const "isEven")
 let is_odd_label = typed_term (Const "isOdd")
-let is_even_odd_label = type_union [ is_even_label.stype; is_odd_label.stype ]
+let is_even_odd_label = type_union [ is_even_label.rtype; is_odd_label.rtype ]
 let name = typed_term (Const "Name")
 let num_to_bool = func_type (three_bit_type.union, bool_type.union)
 
 let is_zero =
   typed_term
     (Abstraction
        [
-         (zero.stype, true_lambda.term);
+         (zero.rtype, true_lambda.term);
          ( type_union
              [
-               one.stype;
-               two.stype;
-               three.stype;
-               four.stype;
-               five.stype;
-               six.stype;
-               seven.stype;
+               one.rtype;
+               two.rtype;
+               three.rtype;
+               four.rtype;
+               five.rtype;
+               six.rtype;
+               seven.rtype;
              ],
            false_lambda.term );
        ])
@@ -39,36 +39,36 @@ let is_even_odd =
             ( func_type (is_even_odd_label.union, num_to_bool.union),
               Abstraction
                 [
-                  ( is_even_label.stype,
+                  ( is_even_label.rtype,
                     Abstraction
                       [
-                        (zero.stype, true_lambda.term);
+                        (zero.rtype, true_lambda.term);
                         ( type_union
                             [
-                              one.stype;
-                              two.stype;
-                              three.stype;
-                              four.stype;
-                              five.stype;
-                              six.stype;
-                              seven.stype;
+                              one.rtype;
+                              two.rtype;
+                              three.rtype;
+                              four.rtype;
+                              five.rtype;
+                              six.rtype;
+                              seven.rtype;
                             ],
                           binary_apply (Variable 2) is_odd_label.term
                             (Application (decrement.term, Variable 0)) );
                       ] );
-                  ( is_odd_label.stype,
+                  ( is_odd_label.rtype,
                     Abstraction
                       [
-                        (zero.stype, false_lambda.term);
+                        (zero.rtype, false_lambda.term);
                         ( type_union
                             [
-                              one.stype;
-                              two.stype;
-                              three.stype;
-                              four.stype;
-                              five.stype;
-                              six.stype;
-                              seven.stype;
+                              one.rtype;
+                              two.rtype;
+                              three.rtype;
+                              four.rtype;
+                              five.rtype;
+                              six.rtype;
+                              seven.rtype;
                             ],
                           binary_apply (Variable 2) is_even_label.term
                             (Application (decrement.term, Variable 0)) );

example/modularArithmetic.ml

@@ -15,14 +15,14 @@ let seven = typed_term (Const "Seven")
 let three_bit_type =
   type_union
     [
-      zero.stype;
-      one.stype;
-      two.stype;
-      three.stype;
-      four.stype;
-      five.stype;
-      six.stype;
-      seven.stype;
+      zero.rtype;
+      one.rtype;
+      two.rtype;
+      three.rtype;
+      four.rtype;
+      five.rtype;
+      six.rtype;
+      seven.rtype;
     ]
 
 let unary_num_op = func_type (three_bit_type.union, three_bit_type.union)
@@ -32,28 +32,28 @@ let increment =
   typed_term
     (Abstraction
        [
-         (zero.stype, one.term);
-         (one.stype, two.term);
-         (two.stype, three.term);
-         (three.stype, four.term);
-         (four.stype, five.term);
-         (five.stype, six.term);
-         (six.stype, seven.term);
-         (seven.stype, zero.term);
+         (zero.rtype, one.term);
+         (one.rtype, two.term);
+         (two.rtype, three.term);
+         (three.rtype, four.term);
+         (four.rtype, five.term);
+         (five.rtype, six.term);
+         (six.rtype, seven.term);
+         (seven.rtype, zero.term);
        ])
 
 let decrement =
   typed_term
     (Abstraction
        [
-         (zero.stype, seven.term);
-         (one.stype, zero.term);
-         (two.stype, one.term);
-         (three.stype, two.term);
-         (four.stype, three.term);
-         (five.stype, four.term);
-         (six.stype, five.term);
-         (seven.stype, six.term);
+         (zero.rtype, seven.term);
+         (one.rtype, zero.term);
+         (two.rtype, one.term);
+         (three.rtype, two.term);
+         (four.rtype, three.term);
+         (five.rtype, four.term);
+         (six.rtype, five.term);
+         (seven.rtype, six.term);
        ])
 
 let fix_binary_num_op = fix three_bit_type unary_num_op
@@ -67,16 +67,16 @@ let add =
             ( binary_num_op,
               Abstraction
                 [
-                  (zero.stype, Abstraction [ (three_bit_type, Variable 0) ]);
+                  (zero.rtype, Abstraction [ (three_bit_type, Variable 0) ]);
                   ( type_union
                       [
-                        one.stype;
-                        two.stype;
-                        three.stype;
-                        four.stype;
-                        five.stype;
-                        six.stype;
-                        seven.stype;
+                        one.rtype;
+                        two.rtype;
+                        three.rtype;
+                        four.rtype;
+                        five.rtype;
+                        six.rtype;
+                        seven.rtype;
                       ],
                     Abstraction
                       [
@@ -96,15 +96,15 @@ let fib =
             ( unary_num_op,
               Abstraction
                 [
-                  (type_union [ zero.stype; one.stype ], one.term);
+                  (type_union [ zero.rtype; one.rtype ], one.term);
                   ( type_union
                       [
-                        two.stype;
-                        three.stype;
-                        four.stype;
-                        five.stype;
-                        six.stype;
-                        seven.stype;
+                        two.rtype;
+                        three.rtype;
+                        four.rtype;
+                        five.rtype;
+                        six.rtype;
+                        seven.rtype;
                       ],
                     binary_apply add.term
                       (Application