]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Make the code OCaml-4.06.1-friendly
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 31 May 2018 21:45:14 +0000 (23:45 +0200)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 31 May 2018 21:51:57 +0000 (23:51 +0200)
ocaml/Makefile
ocaml/console.ml
ocaml/lambda4.ml
ocaml/num.ml
ocaml/parser.ml
ocaml/pure.ml
ocaml/simple.ml

index 3a94a7ac8174006d075c6cf3b883276c814a6a0c..2557224f0f1397e830dfad21f0c753df47078b8d 100644 (file)
@@ -13,8 +13,8 @@ a.out: $(UTILS) lambda4.cmx
 test4.out: $(UTILS) lambda4.cmx test.ml
        $(OCAMLC) -o test4.out $(LIB) $^
 
-simple.out: $(UTILS) simple.ml
-       $(OCAMLC) -o simple.out $(LIB) $(UTILS) simple.ml
+simple.out: $(UTILS) simple.cmx
+       $(OCAMLC) -o simple.out $(LIB) $^
 
 simple_test.out: $(UTILS) simple.cmx simple_test.ml
        $(OCAMLC) -o simple_test.out $(LIB) $^
index 696a74d9abe151e3c873d7267e317ed6e0a7bb96..f3fbef6d497d5ab74468889e09adb91eda374095 100644 (file)
@@ -40,7 +40,7 @@ let cols =
 ;;
 
 let writeall s =
-  let _ = Unix.send socket s 0 (String.length s) [] in ()
+  let _ = Unix.send socket (Bytes.of_string s) 0 (String.length s) [] in ()
 ;;
 
 let concat ls = (String.concat sepx ls) ^ endx;;
index 90a91e048b26c88a403f5de22103581f8497cb89..83c1b1dab20be45651ca6ead3406f005f173c7b9 100644 (file)
@@ -39,7 +39,7 @@ let label_of_problem {label} = label;;
 let string_of_var l x =
  try
   List.nth l x
- with Failure "nth" -> "`" ^ string_of_int x
+ with Failure _ -> "`" ^ string_of_int x
 ;;
 let string_of_term p t = print ~l:p.var_names (t :> nf);;
 
index 8ecf12491be1d9931dfdc39fbbe4c9403f391008..cc30cb5c4f2ae5d18adacd81d8a00157d44e025c 100644 (file)
@@ -123,7 +123,7 @@ end
 
 (* let rec string_of_term l  = fun _ -> "";; *)
 
-let rec string_of_term =
+let string_of_term =
  let boundvar x = "v" ^ string_of_int x in
  let varname lev l n =
   if n < lev then boundvar (lev-n-1)
@@ -148,7 +148,8 @@ let rec string_of_term =
  and string_of_term_no_pars lev l = function
   | `Lam _ as t -> string_of_term_no_pars_lam lev l t
   | #nf as t -> string_of_term_no_pars_app lev l t
- in string_of_term_no_pars 0
+ and string_of_term t = string_of_term_no_pars 0 t in
+ string_of_term
 ;;
 
 let print ?(l=[]) = string_of_term l;;
index 1dd4b583c8886216ee6910392103965253b1be05..800322677a102f3aa324df8ddb35ca4daa6afcda 100644 (file)
@@ -30,11 +30,11 @@ let explode s =
 ;;\r
 \r
 let implode l =\r
-  let res = String.create (List.length l) in\r
+  let res = Bytes.create (List.length l) in\r
   let rec aux i = function\r
     | [] -> res\r
-    | c :: l -> res.[i] <- c; aux (i + 1) l in\r
-  aux 0 l\r
+    | c :: l -> Bytes.set res i c; aux (i + 1) l in\r
+  Bytes.to_string (aux 0 l)\r
 ;;\r
 \r
 let rec strip_spaces = function\r
index 3bd7ec491a11059bd91c9a90800f58175fb62cf6..e04b4eac7baedccd62054516e58068087178f5fa 100644 (file)
@@ -115,7 +115,7 @@ in
         (try
           let e,t,s' = List.nth e n in
           aux g (e,t,s'@s)
-         with Invalid_argument "List.nth" | Failure _ -> m
+         with Invalid_argument _ | Failure _ -> m
          )
      | (e, B, _) -> (e, B, [])
      | (e, L t, []) ->
index 991779e7ac995f5f980a174b43c292689cac1ce6..8e4f61946e453827b4024dccca02d6ce8ac2f19b 100644 (file)
@@ -288,9 +288,6 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")")
  sanity p\r
 ;;\r
 \r
-;;\r
-\r
-\r
 let rec auto p =\r
  let hd_var, n_args = get_inert p.div in\r
  match get_subterm_with_head_and_args hd_var n_args p.conv with\r