formatting and cmd tool

bin/main.ml

@@ -7,39 +7,27 @@ let p_term term reduction scc_paths =
 let tree_of_string s = Grammar.input Lexer.token (Lexing.from_string s)
 
 let () =
-  if Array.length Sys.argv < 4 then
-    failwith "Usage: dune exec bin/main.exe max_depth simultaneous dot term_str"
+  if Array.length Sys.argv < 3 then
+    failwith "Usage: dune exec bin/main.exe max_depth term_str"
   else
     let term =
-      try tree_of_string (Sys.argv.(4) ^ "\n")
+      try tree_of_string (Sys.argv.(2) ^ "\n")
       with _ -> failwith "Syntax error"
     in
     let max_depth = int_of_string Sys.argv.(1) in
-    let simultaneous = bool_of_string Sys.argv.(2) in
-    let generate_dot = bool_of_string Sys.argv.(3) in
+    let generate_dot =
+      try bool_of_string Sys.argv.(3)
+      with _ -> true
+    in
+    let simultaneous = false in
     let scc_analysis = Core.scc term max_depth simultaneous in
     let scc_paths = snd scc_analysis in
     let vc_terminated = fst (fst scc_analysis) in
-    let closed_term =
-      Core.a_term_to_string (Core.make_closed term)
-    in
-    let normalizing = false in
-     (* typable = "Typable." in *)
-    (* snd (fst scc_analysis) in *)
+    let closed_term = Core.a_term_to_string (Core.make_closed term) in
     let reduction =
-      if normalizing then Core.sn_reduce_to_nf Core.casubst term
+      if vc_terminated then Core.sn_reduce_to_nf Core.casubst term
       else Core.reduce_to_nf term max_depth
     in
-    (* let reduction =
-         if normalizing then
-           Core.sn_reduce_with_paths_to_nf term max_depth simultaneous
-         else Core.reduce_with_paths term max_depth simultaneous
-       in
-       let reduction =
-         if List.length reduction <= 1 && normalizing then
-           Core.sn_reduce_to_nf Core.casubst term
-         else reduction
-       in *)
     let reduction_str = List.map Core.a_term_to_string reduction in
     let ord_con = Util.b_to_str (Core.order_consistent term) in
     let is_safe = Util.b_to_str (Core.issafe term) in
@@ -57,7 +45,7 @@ let () =
     in
     let dot = p_term term reduction_str scc_paths in
     Printf.printf
-       "- vc: %s\n\
+      "- vc: %s\n\
        - closed_term: %s\n\
        - max_depth: %d\n\
        - order_consistent: %s\n\

exp/naive.ml

@@ -33,7 +33,10 @@ let () =
     let c2 = !Core.counter in
     let bc2 = !Core.beta_counter in
     let diff = Unix.gettimeofday () -. t in
-    Printf.printf "Execution time (%d): %f seconds\nAlpha conversions: %d\nBeta conversions: %d"
+    Printf.printf
+      "Execution time (%d): %f seconds\n\
+       Alpha conversions: %d\n\
+       Beta conversions: %d"
       (String.length (Core.a_term_to_string s))
       diff (c2 - c1) (bc2 - bc1)
 

lib/core.ml

@@ -253,9 +253,7 @@ type wbp = Empty | Node of string * symbol * simple_type | Comp of wbp list
 
 let posymtyp_to_node = function p, s, t -> Node (p, s, t)
 
-let wbp_isempty = function
-  | Empty -> true
-  | _ -> false
+let wbp_isempty = function Empty -> true | _ -> false
 
 let append_wbp p n =
   match p with
@@ -601,33 +599,46 @@ let legal_paths term =
   (* let wbp = L.filter is_legal wbp in *)
   (fst wbp, L.map wbp_tolist (snd wbp))
 
-let prepos pos = String.sub pos 0 ((String.length pos) - 1)
+let prepos pos = String.sub pos 0 (String.length pos - 1)
 
 let rec _lazy_well_balanced_paths newpaths acc nodes bedges n =
   if n <= 0 then (false, acc)
   else
-
     let apps =
-      L.filter (fun x -> match x with pa, AS _, _ -> pa != "e" | _ -> false) nodes
+      L.filter
+        (fun x -> match x with pa, AS _, _ -> pa != "e" | _ -> false)
+        nodes
     in
-    let activatedapps = L.filter (fun x -> not (wbp_isempty x)) (
-      L.map
-        (fun x ->
-          match x with
-          | pa, AS s, typ ->
-              let ppa = prepos pa in
-              let pexists = List.exists (fun x -> x = ppa) (List.map node_pos (List.map last_wbp acc)) in
-              let acc_acl = L.filter (fun p -> islam_node (last_wbp p)) acc in
-              let pexists2 = List.exists (fun x -> x = ppa) (List.map node_pos (List.map first_wbp acc_acl)) in
-              if pexists || pexists2 then
-              Comp
-                [
-                  Node (pa, AS s, typ);
-                  posymtyp_to_node (L.hd (get_node (pa ^ "0") nodes));
-                ]
-              else Empty
-          | _ -> Empty)
-        apps)
+    let activatedapps =
+      L.filter
+        (fun x -> not (wbp_isempty x))
+        (L.map
+           (fun x ->
+             match x with
+             | pa, AS s, typ ->
+                 let ppa = prepos pa in
+                 let pexists =
+                   List.exists
+                     (fun x -> x = ppa)
+                     (List.map node_pos (List.map last_wbp acc))
+                 in
+                 let acc_acl =
+                   L.filter (fun p -> islam_node (last_wbp p)) acc
+                 in
+                 let pexists2 =
+                   List.exists
+                     (fun x -> x = ppa)
+                     (List.map node_pos (List.map first_wbp acc_acl))
+                 in
+                 if pexists || pexists2 then
+                   Comp
+                     [
+                       Node (pa, AS s, typ);
+                       posymtyp_to_node (L.hd (get_node (pa ^ "0") nodes));
+                     ]
+                 else Empty
+             | _ -> Empty)
+           apps)
     in
     let newpaths = newpaths @ activatedapps in
 
@@ -635,9 +646,7 @@ let rec _lazy_well_balanced_paths newpaths acc nodes bedges n =
 
     let newpaths =
       L.filter
-        (fun x ->
-          (not (L.mem x acc))
-          && (not (first_wbp x = last_wbp x)))
+        (fun x -> (not (L.mem x acc)) && not (first_wbp x = last_wbp x))
         paths
     in
     let newacc = acc @ newpaths in
@@ -649,23 +658,28 @@ let lazy_well_balanced_paths term =
   let nodes = term_nodes term in
   let bedges = b_edges term in
   let apps =
-    L.filter (fun x -> match x with pa, AS _, _ -> pa = "e" | _ -> false) nodes
+    L.filter
+      (fun x -> match x with pa, AS _, _ -> pa = "e" | _ -> false)
+      nodes
   in
-  let acc = L.filter (fun x -> not (wbp_isempty x)) (
-    L.map
-      (fun x ->
-        match x with
-        | pa, AS s, typ -> (
-            let fp = posymtyp_to_node (L.hd (get_node (pa ^ "0") nodes)) in
-            match fp with
-              | Node (_, LS _ ,_) -> Comp [Node (pa, AS s, typ);fp]
-              | _ -> Empty
-            )
-        | _ -> Empty)
-      apps)
+  let acc =
+    L.filter
+      (fun x -> not (wbp_isempty x))
+      (L.map
+         (fun x ->
+           match x with
+           | pa, AS s, typ -> (
+               let fp = posymtyp_to_node (L.hd (get_node (pa ^ "0") nodes)) in
+               match fp with
+               | Node (_, LS _, _) -> Comp [ Node (pa, AS s, typ); fp ]
+               | _ -> Empty )
+           | _ -> Empty)
+         apps)
   in
   let max_compositions = 10 in
-  let compose = _lazy_well_balanced_paths acc acc nodes bedges max_compositions in
+  let compose =
+    _lazy_well_balanced_paths acc acc nodes bedges max_compositions
+  in
   (fst compose, snd compose)
 
 let lazy_well_balanced_paths_al term =
@@ -830,8 +844,7 @@ let rec _subterm_at term pos current =
   match term with
   | AVar (s, t) -> term
   | ALam ((xs, e), t) ->
-      if pos = current then term else
-      _subterm_at e pos (current ^ "0")
+      if pos = current then term else _subterm_at e pos (current ^ "0")
   | AApp (e1, e2, t) ->
       if pos = current then term
       else if is_prefix (current ^ "0") pos then
@@ -844,11 +857,11 @@ let beta subst term =
   (* Printf.printf "beta: %s\n" (a_term_to_string term); *)
   beta_counter := !beta_counter + 1;
   match term with
-  | AApp (ALam (((var,_), e1), _), e2, _) ->
-    (* Printf.printf "subst: %s by %s in %s\n" var (a_term_to_string e2) (a_term_to_string e1); *)
-    let res = subst var e2 e1 in
-    (* Printf.printf "res: %s\n" (a_term_to_string res); *)
-    res
+  | AApp (ALam (((var, _), e1), _), e2, _) ->
+      (* Printf.printf "subst: %s by %s in %s\n" var (a_term_to_string e2) (a_term_to_string e1); *)
+      let res = subst var e2 e1 in
+      (* Printf.printf "res: %s\n" (a_term_to_string res); *)
+      res
   | _ -> failwith "beta: Not a redex."
 
 let rec _reduce_at_pos subst term pos current =
@@ -889,7 +902,7 @@ let rec _reduce_lazy subst term =
       | _ ->
           let left = _reduce_lo subst e1 in
           if left = e1 then AApp (e1, e2, t)
-          (* if left = e1 then AApp (e1, _reduce_lo subst e2, t) *)
+            (* if left = e1 then AApp (e1, _reduce_lo subst e2, t) *)
           else AApp (left, e2, t) )
 
 let reduce_lazy subst term = _reduce_lazy subst term
@@ -903,8 +916,8 @@ let rec _reduce_ne subst term =
       match e1 with
       | ALam _ -> beta subst (AApp (e1, right, t))
       | _ ->
-        let left = _reduce_ne subst e1 in
-        AApp (left, right, t))
+          let left = _reduce_ne subst e1 in
+          AApp (left, right, t) )
 
 let reduce_ne subst term = _reduce_ne subst term
 
@@ -983,10 +996,9 @@ let rec nf subst term =
 let rec _nf_arr acc subst term =
   (* Printf.printf "%d %s\n" (size term) (a_term_to_string term); *)
   let new_term = reduce_lo subst term in
-  if new_term = term then acc else _nf_arr (acc @ [new_term]) subst new_term
+  if new_term = term then acc else _nf_arr (acc @ [ new_term ]) subst new_term
 
-let rec nf_arr subst term =
-  _nf_arr [] subst term
+let rec nf_arr subst term = _nf_arr [] subst term
 
 let rec whnf subst term =
   (* Printf.printf "%d %s\n" (size term) (a_term_to_string term); *)
@@ -1010,30 +1022,28 @@ let rec _reduce_lo_memo subst term cache =
               let left = _reduce_lo_memo subst e1 cache in
               Hashtbl.add cache e1 left;
               (* Printf.printf "Cache add %s.\n" (a_term_to_string e1); *)
-              if left = e1 then
+              if left = e1 then (
                 let arg = _reduce_lo_memo subst e2 cache in
                 (* Printf.printf "Cache add %s.\n" (a_term_to_string e2); *)
                 Hashtbl.add cache e2 arg;
-                AApp (e1, arg, t)
-              else AApp (left, e2, t) ))
+                AApp (e1, arg, t) )
+              else AApp (left, e2, t) ) )
 
 let reduce_lo_memo subst term =
   let h = Hashtbl.create 100 in
   _reduce_lo_memo subst term h
 
 let rec _nf_memo subst term cache =
-(
   match Hashtbl.mem cache term with
-  | true -> (
+  | true ->
       let tc = Hashtbl.find cache term in
       Printf.printf "Cache hit.\n";
-      if tc = term then tc else _nf_memo subst tc cache)
-  | false -> (
+      if tc = term then tc else _nf_memo subst tc cache
+  | false ->
       Printf.printf "NO Cache hit %s.\n\n" (a_term_to_string term);
       let result = reduce_lo_memo subst term in
       Hashtbl.add cache term result;
-      if result = term then result else _nf_memo subst result cache)
-)
+      if result = term then result else _nf_memo subst result cache
 
 let nf_memo subst term =
   let cache = Hashtbl.create 1000 in

lib/dot.ml

@@ -92,12 +92,14 @@ let rec b_edges_to_dot pre = function
 
 let rec c_edges_to_dot pre = function
   | [ p1; p2 ] :: xs ->
-      edge_to_dot (pre ^ p1) (pre ^ p2) "[color=orange1];" ^ c_edges_to_dot pre xs
+      edge_to_dot (pre ^ p1) (pre ^ p2) "[color=orange1];"
+      ^ c_edges_to_dot pre xs
   | _ -> ""
 
 let rec a_edges_to_dot pre = function
   | [ p1; p2 ] :: xs ->
-      edge_to_dot (pre ^ p1) (pre ^ p2) "[color=chartreuse3];" ^ a_edges_to_dot pre xs
+      edge_to_dot (pre ^ p1) (pre ^ p2) "[color=chartreuse3];"
+      ^ a_edges_to_dot pre xs
   | _ -> ""
 
 let r_path_to_dot pre xs =
@@ -234,5 +236,6 @@ let export_term_ctx_dot ctx tterm dir name =
   let oc = open_out fname in
   (* Printf.printf "Generating file %s..." fname; *)
   fprintf oc "%s\n" (term_ctx_to_dot ctx tterm reduction (snd scc_paths) name);
-  close_out oc;
-  (* Printf.printf "done!\t\n" *)
+  close_out oc
+
+(* Printf.printf "done!\t\n" *)

lib/dune

@@ -8,4 +8,5 @@
 (menhir
  (modules grammar))
 
-(documentation (package alpha))
+(documentation
+ (package alpha))

test/test_uterms.ml

@@ -4,7 +4,7 @@ open List
 let test_uterm term =
   let tt = Underlined.u_term_to_a_term term in
   let tpaths = Core.scc tt 10 false in
-  (List.length (snd tpaths)) > 0
+  List.length (snd tpaths) > 0
 
 (* test for variable capture *)
 let%test "slctest_ut1" = test_uterm (List.nth Terms.u_terms 0) = false