Rune dune fmt

Author: sColin16

example/boolean.ml

@@ -6,15 +6,9 @@ let true_lambda = typed_term (Const "True")
 let false_lambda = typed_term (Const "False")
 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 =
-  func_type (bool_type.union, unary_bool_op.union)
-
-let ternary_bool_op =
-  func_type (bool_type.union, binary_bool_op.union)
-
-let identity_lambda =
-  typed_term (Abstraction [ (bool_type, Variable 0) ])
+let binary_bool_op = func_type (bool_type.union, unary_bool_op.union)
+let ternary_bool_op = func_type (bool_type.union, binary_bool_op.union)
+let identity_lambda = typed_term (Abstraction [ (bool_type, Variable 0) ])
 
 let not_lambda =
   typed_term

example/exampleHelpers.ml

@@ -96,7 +96,7 @@ let build_fix (arg_type : recursive_type) (return_type : recursive_type) =
   fix
 
 (* Fixes a provided abstraction with the given arg and return type *)
-let fix (arg_type : recursive_type) (return_type : recursive_type)
-    (term : term) =
+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)

src/common/helpers.ml

@@ -34,26 +34,27 @@ let opt_list_to_list_opt (input : 'a option list) : 'a list option =
 
 type 'a tuple = 'a list
 
-let rec multi_list_product (nested_list: 'a list tuple): 'a tuple list =
-  let rec helper (acc: 'a tuple list) (l1: 'a list) (l2: 'a list tuple) =
-    match l1, l2 with
+let rec multi_list_product (nested_list : 'a list tuple) : 'a tuple list =
+  let rec helper (acc : 'a tuple list) (l1 : 'a list) (l2 : 'a list tuple) =
+    match (l1, l2) with
     | [], _ | _, [] -> acc
-    | h1::t1, h2::t2 ->
-      let acc = (h1::h2)::acc in
-      let acc = helper acc t1 l2 in
-      helper acc [ h1 ] t2
-  in match nested_list with
+    | h1 :: t1, h2 :: t2 ->
+        let acc = (h1 :: h2) :: acc in
+        let acc = helper acc t1 l2 in
+        helper acc [ h1 ] t2
+  in
+  match nested_list with
   | [] -> []
-  | [l1] -> List.map (fun x -> [x]) l1
-  | l1::tail ->
-    let tail_product = multi_list_product tail in
-    helper [] l1 tail_product
+  | [ l1 ] -> List.map (fun x -> [ x ]) l1
+  | l1 :: tail ->
+      let tail_product = multi_list_product tail in
+      helper [] l1 tail_product
 
-let short_circuit_and (exp1: unit -> bool) (exp2: unit -> bool) =
+let short_circuit_and (exp1 : unit -> bool) (exp2 : unit -> bool) =
   if exp1 () then exp2 () else false
 
-let short_circuit_or (exp1: unit -> bool) (exp2: unit -> bool) =
-  if exp1() then true else exp2 ()
+let short_circuit_or (exp1 : unit -> bool) (exp2 : unit -> bool) =
+  if exp1 () then true else exp2 ()
 
-let map_pair (func: 'a -> 'b) (first, second: 'a * 'a): 'b * 'b =
-  (func first), (func second)
+let map_pair (func : 'a -> 'b) ((first, second) : 'a * 'a) : 'b * 'b =
+  (func first, func second)

src/dune

@@ -1,3 +1,9 @@
 (library
  (name setTypedLambda)
- (libraries metatypes termTypes typeOperations termOperations common stringUtils))
+ (libraries
+  metatypes
+  termTypes
+  typeOperations
+  termOperations
+  common
+  stringUtils))

src/stringUtils/stringUtils.ml

@@ -63,7 +63,9 @@ let rec term_to_string (term : term) =
   | UnivQuantifier inner_term ->
       Printf.sprintf "\\T.{%s}" (term_to_string inner_term)
   | UnivApplication (inner_term, inner_type) ->
-      Printf.sprintf "(%s) [%s]" (term_to_string inner_term) (type_to_string inner_type)
+      Printf.sprintf "(%s) [%s]"
+        (term_to_string inner_term)
+        (type_to_string inner_type)
 
 and branch_to_string (branch_type, branch_body) =
   Printf.sprintf "%s:%s"

src/termOperations/substituteUnivVar.ml

@@ -7,8 +7,8 @@ open TypeOperations.SubstituteUnivVar
 
 (* Substitutes the [with_type] into the [in_term] for universal type variables referencing
    the universal quantification at this level (0, or higher if nested within another universal quantifications) *)
-let rec substitute_univ_var_term (with_type : recursive_type) (in_term : term)
-    : term =
+let rec substitute_univ_var_term (with_type : recursive_type) (in_term : term) :
+    term =
   (* Shift the universal type indices in the argument by one since it is about to be substituted into a universal quantification,
      where their binding quantification is one further away *)
   let shifted_with_type = shift_univ_var_type with_type 1 in

src/termOperations/valToTerm.ml

@@ -37,17 +37,15 @@ and substitute_in_term (term : term) (env : environment) (depth : int) =
   | Application (left_term, right_term) ->
       Application
         ( substitute_in_term left_term env depth,
-          substitute_in_term right_term env depth)
+          substitute_in_term right_term env depth )
   (* If a variable references a free variable, we pull it from the env, otherwise, leave it
      because it references a bound variable within this abstraction *)
   | Variable num ->
       if num - depth < 0 then Variable num
       else value_to_term (List.nth env (num - depth))
   (* Universal quantifiers are substituted recursively *)
   | UnivQuantifier inner_term ->
-    UnivQuantifier (substitute_in_term inner_term env depth)
+      UnivQuantifier (substitute_in_term inner_term env depth)
   (* Universal application requires a substitution in the term, but leaves the type the same *)
   | UnivApplication (inner_term, inner_type) ->
-    UnivApplication
-    ( substitute_in_term inner_term env depth,
-      inner_type)
+      UnivApplication (substitute_in_term inner_term env depth, inner_type)

src/typeOperations/context.ml

@@ -44,7 +44,8 @@ let get_type_in_context (t : recursive_type)
   build_recursive_type new_union (recursive_context @ new_context)
 
 (* Converts a pair of recursive types into a pair of union types that share a context *)
-let get_unified_type_context_pair (typea: recursive_type) (typeb: recursive_type) =
+let get_unified_type_context_pair (typea : recursive_type)
+    (typeb : recursive_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)
@@ -55,30 +56,47 @@ let get_unified_type_context (types : recursive_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 recontextualized_next_union =
+          get_type_in_context next_type acc_context
+        in
         let new_acc_union = recontextualized_next_union.union :: acc_union in
         let new_acc_context = recontextualized_next_union.context in
         (new_acc_union, new_acc_context))
-      ([], []) types in
+      ([], []) 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
+  (new_unions, new_context)
 
 (* TODO: consider writing more dedicated logic for this rather than the showving intermediate into intersection *)
 (* Takes a list of arg types and their corresponding body types, and joined them into
    a single recursive type for the intersection of the functions *)
-let unify_function_types (arg_types: recursive_type list) (body_types: recursive_type list) =
+let unify_function_types (arg_types : recursive_type list)
+    (body_types : recursive_type list) =
   (* First, build individual unary function types for each arg/body pair *)
-  let unary_types = List.map2 (fun arg_type body_type ->
-    let (new_arg_type, new_body_type), new_context = get_unified_type_context_pair arg_type body_type in
-    build_recursive_type [ Intersection [(new_arg_type, new_body_type )]] new_context
-  ) arg_types body_types in
+  let unary_types =
+    List.map2
+      (fun arg_type body_type ->
+        let (new_arg_type, new_body_type), new_context =
+          get_unified_type_context_pair arg_type body_type
+        in
+        build_recursive_type
+          [ Intersection [ (new_arg_type, new_body_type) ] ]
+          new_context)
+      arg_types body_types
+  in
   (* Then, rectonextualize all of them so we can prepare to join them into a single type *)
   let new_unary_unions, new_context = get_unified_type_context unary_types in
   (* Then destructure all of the unary types to build a single intersection type *)
-  let unary_list = List.fold_left (fun acc_func_types next_union ->
-    match next_union with
-    | [ Intersection [ next_unary ]] -> next_unary::acc_func_types
-    | _ -> raise (Failure "there was a problem destructuring the unary function types")
-  ) [] new_unary_unions in
-  build_recursive_type [ Intersection unary_list ] new_context
+  let unary_list =
+    List.fold_left
+      (fun acc_func_types next_union ->
+        match next_union with
+        | [ Intersection [ next_unary ] ] -> next_unary :: acc_func_types
+        | _ ->
+            raise
+              (Failure
+                 "there was a problem destructuring the unary function types"))
+      [] new_unary_unions
+  in
+  build_recursive_type [ Intersection unary_list ] new_context

src/typeOperations/shiftUnivVar.ml

@@ -91,4 +91,4 @@ and shift_univ_var_base (shift_amount : int) (cutoff : int) (base : base_type) =
 
 and shift_univ_var_func (shift_amount : int) (cutoff : int)
     ((arg, return) : unary_function) =
-  map_pair (shift_univ_var_union shift_amount cutoff) (arg, return)
+  map_pair (shift_univ_var_union shift_amount cutoff) (arg, return)

src/typeOperations/substituteUnivVar.ml

@@ -49,8 +49,7 @@ let rec substitute_univ_var_type (with_type : recursive_type)
     with the with_type, respecting free variables and the complexities of recursive
     types *)
 and substitute_univ_var_type_rec (variable_num : int)
-    (with_type : recursive_type) (in_type : recursive_type) : recursive_type
-    =
+    (with_type : recursive_type) (in_type : recursive_type) : recursive_type =
   (* Perform initial pass over substitution to get information we use to safely perform substitution *)
   let substitution_profile = get_substitution_profile variable_num in_type in
 
@@ -343,4 +342,4 @@ and merge_context_subs_binary (directives_a : context_subs)
       | Some x, Some _ -> Some x
       | None, y -> y
       | x, None -> x)
-    directives_a directives_b
+    directives_a directives_b