Improving prl preprocessing; Improving auto tactic computation

filter/base/filter_cache_fun.ml

@@ -126,9 +126,7 @@ let string_of_op_shape shape =
          Buffer.add_char buf ']'
    in
    let string_of_arity i =
-      Buffer.add_char buf '<';
-      Buffer.add_string buf (string_of_int i);
-      Buffer.add_char buf '>'
+      Printf.bprintf buf "<%i>" i
    in
    let { sh_name = name;
          sh_kind = kind;

filter/base/filter_grammar.ml

@@ -108,26 +108,6 @@ module Lexer = MakeLexer (Lm_channel.LexerInput) (Action);;
 (*
  * Boolean lexer is for parsing comments and quotations.
  *)
-(* unused
-module BoolCompare =
-struct
-   type t = bool
-
-   let compare b1 b2 =
-      if b1 then
-         if b2 then
-            0
-         else
-            1
-      else if b2 then
-         -1
-      else
-         0
-end
-
-module BoolSet = Lm_set.LmMake (BoolCompare);;
-*)
-
 module BoolAction =
 struct
    type action = bool
@@ -140,13 +120,7 @@ struct
       else
          0x5ffa1124
 
-   let compare a b =
-      if a = b then
-         0
-      else if a then
-         1
-      else
-         -1
+   let compare = Bool.compare
 
    let choose = max
 end;;

filter/base/filter_magic.ml

@@ -39,7 +39,7 @@ open File_type_base
  ************************************************************************
  *
  * Current MD5 hash of the summary-related types (as computed by OMake):
- * FILTER_MD5: b2463ac8f553284fb92799f0d93fc130
+ * FILTER_MD5: 2cba8f8a16c795b59ef3e5d3b94bfb79
  *
  * The arguments for pack_version are:
  *    major version number, minor sub-version number, revision number
@@ -125,7 +125,6 @@ let term_versions = List.map (pack_version 1 0) [34;33;32;31;30;29;28;27;25;24]
  * Rev 27: changed the stging encoding of option_info
  * Rev 28: added "opaque" qualifier to the "define" statements
  *
- * Filter_summary has another HACK needed to read some rev 0-15 files.
  * Filter_summary has another HACK needed to read some rev 0-17 files.
  * Filter_summary has another HACK needed to read some rev 0-18 files.
  * Filter_summary has another HACK needed to read some rev 0-20 files.

filter/base/filter_ocaml.ml

@@ -375,7 +375,12 @@ struct
       let loc = MLast.loc_of_expr e in
          mk_loc_term (Ploc.file_name loc) (Lm_num.num_of_int (Ploc.line_nb loc))
 
-   let value_names =
+   let type_name tdl =
+      match tdl.MLast.tdNam with
+         (<:vala< _, <:vala< name >> >>) -> mk_ident_term name
+       | _ -> invalid_arg "Filter_ocaml.type_name"
+
+   let value_name =
       let patt_tuple_op = mk_caml_op "tuple"
       and str_def_op = mk_caml_op "str_def" in
       let rec name_term = function
@@ -387,7 +392,7 @@ struct
             name_term p
        | (<:patt< ($list:lp$) >>) ->
             mk_simple_term patt_tuple_op [mk_olist_term name_term lp]
-       | _ -> invalid_arg "Filter_ocaml.value_names"
+       | _ -> invalid_arg "Filter_ocaml.value_name"
       in fun (p,e,_) -> mk_simple_term str_def_op [name_term p; loc_of_expr e]
 
    let mk_me_item me =
@@ -403,16 +408,16 @@ struct
 
    let mk_str_item =
       let str_external_op = mk_caml_op "str_ext"
-   (* and str_type_op = mk_caml_op "str_type" *)
+      and str_type_op = mk_caml_op "str_type"
       and str_fix_op = mk_caml_op "str_fix"
       and str_open_op = mk_caml_op "str_open"
       in fun vars -> function
          (<:str_item< external $s$ : $t$ = $list:ls$ $itemattrs:_$ >>) ->
             mk_simple_named_term str_external_op s (mk_type t :: List.map mk_simple_string ls)
-   (*  | (<:str_item< type $flag:b$ $list:tdl$ >>) ->
-            mk_simple_term str_type_op [mk_olist_term mk_tdl tdl] *)
+       | (<:str_item< type $flag:b$ $list:tdl$ >>) ->
+            mk_simple_term str_type_op [mk_bool b; mk_olist_term type_name tdl]
        | (<:str_item< value $flag:b$ $list:lpex$ >>) ->
-            mk_simple_term str_fix_op [mk_bool b; mk_olist_term value_names lpex]
+            mk_simple_term str_fix_op [mk_bool b; mk_olist_term value_name lpex]
        | (<:str_item< open $!:b$ $me$ $itemattrs:_$ >>) ->
             mk_simple_term str_open_op [mk_me_item me]
        | _ -> mk_stub_term str_opname

filter/base/filter_summary.ml

@@ -1016,15 +1016,9 @@ struct
 
    (*
     * Get the parameter list.
-    * XXX HACK: the try wrapper is only there for backwards compativility with
-    * old files (ASCII formats <= 1.0.15)
     *)
    let dest_rule_params convert t =
-      try
-         List.map (dest_rule_param convert) (dest_xlist t)
-      with
-         Failure _ ->
-            []
+      List.map (dest_rule_param convert) (dest_xlist t)
 
    (*
     * Get the list of resource updates

filter/filter/filter_convert.ml

@@ -43,7 +43,7 @@ open Filter_cache
  * Show the file loading.
  *)
 let _ =
-   show_loading "Loading Convert%t"
+   show_loading "Loading Convert"
 
 (*
  * Include directories.

filter/filter/filter_prog.ml

@@ -59,7 +59,7 @@ open Proof_convert
  * Show the file loading.
  *)
 let _ =
-   show_loading "Loading Filter_prog%t"
+   show_loading "Loading Filter_prog"
 
 let debug_filter_prog =
    create_debug (**)
@@ -412,7 +412,7 @@ let expr_of_label loc = function
 
 (*
  * Print a message on loading, and catch errors.
- *    Lm_debug.show_loading "Loading name%t";
+ *    Lm_debug.show_loading "Loading name";
  *    try e with
  *       exn ->
  *          Refine_exn.stderr_exn name exn
@@ -422,7 +422,7 @@ let wrap_exn proc loc name e =
    <:expr<
       do {
          (* Print a message before the execution *)
-         Lm_debug.show_loading $str: "Loading " ^ name ^ "%t"$;
+         Lm_debug.show_loading $str: "Loading " ^ name$;
          (* Wrap the body to catch exceptions *)
          try $e$ with
          $lid: exn_id$ ->
@@ -1404,7 +1404,7 @@ let define_resource proc loc name res =
       [<:str_item< type $inp_name$ = $res.res_input$ >>;
        <:str_item< type $outp_name$ = $res.res_output$ >>;
        <:str_item< value $lid:get_resource_name name$ =
-         Mp_resource.create_resource $str:fqn$ (**)
+         Mp_resource.create_resource $str:fqn$
             ( $res.res_body$ : Mp_resource.resource_info $lid:inp_name$ '$intermediate$ $lid:outp_name$ ) >>]
 
 let rec is_list_expr = function
@@ -1531,8 +1531,10 @@ let define_magic_block proc loc { magic_name = name; magic_code = stmts } =
    let index = List.fold_left Filter_hash.hash_str_item 0 stmts in
       <:str_item< value $lid:name$ = $int:string_of_int index$ >> :: stmts
 
+(*
 let define_prefix loc s =
    [<:str_item< value _ = $lid:Infix.prefix_name s$ >>]
+*)
 
 (*
  * Prolog declares the refiner and dformer.
@@ -1559,7 +1561,7 @@ let implem_prolog proc loc name =
                                 $lid:global_num_var$) =
                             Ml_term.term_arrays_of_string $str:String.escaped marshalled_terms$>>]
    in
-      <:str_item< Lm_debug.show_loading $str: "Loading theory " ^ String.capitalize_ascii name ^ "%t"$ >>
+      <:str_item< Lm_debug.show_loading $str: "Loading theory " ^ String.capitalize_ascii name$ >>
       :: <:str_item< value $lid:local_refiner_id$ = $refiner_expr loc$ . null_refiner $str: name$ >>
       :: term_let
 
@@ -1580,7 +1582,7 @@ let implem_postlog proc loc =
                   Theory.thy_groupdesc = $str:proc.imp_groupdesc$;
                   Theory.thy_refiner = $lid:refiner_id$
                }>>;
-            <:str_item< Lm_debug.show_loading $str: ("Finished loading " ^ String.capitalize_ascii proc.imp_name ^ "%t") $ >>]
+            <:str_item< Lm_debug.show_loading $str:"Finished loading " ^ String.capitalize_ascii proc.imp_name$ >>]
 
 (*
  * Now extract the program.
@@ -1688,9 +1690,6 @@ let extract_str_item proc (item, loc) =
          if !debug_filter_prog then
             eprintf "Filter_prog.extract_str_item: magic block%t" eflush;
          define_magic_block proc loc block
-    | MLGramUpd (Infix s)
-    | MLGramUpd (Suffix s) ->
-         define_prefix loc s
     | DefineTerm (shapeclass, class_term, def)
       when is_shape_normal shapeclass ->
          define_term proc loc class_term def
@@ -1699,6 +1698,7 @@ let extract_str_item proc (item, loc) =
     | DeclareType _
     | DeclareTerm _
     | DeclareTypeRewrite _
+    | MLGramUpd _
     | Id _
     | Comment _
     | PRLGrammar _ ->

mllib/http_simple.ml

@@ -550,48 +550,49 @@ type uri_state =
 
 let colon = ':'
 
+let split_at i str =
+   let len = String.length str in
+   let si = succ i in
+      String.sub str 0 i, String.sub str si (len - si)
+
 let parse_uri s =
-   let len = String.length s in
-   let proto = Buffer.create 7 in
-   let host = Buffer.create 64 in
-   let port = Buffer.create 6 in
-   let file = Buffer.create 128 in
-   let rec search state j =
-      if j <> len then
-         let c = s.[j] in
-         let j' = succ j in
-            match state with
-               StateProto ->
-                  if c = colon then
-                     search StateHost j'
-                  else
-                     (Buffer.add_char proto c; search StateProto j')
-             | StateHost ->
-                  if c = colon then
-                     search StatePort j'
-                  else if c = '/' then
-                     search StateFile j'
-                  else
-                     (Buffer.add_char host c; search StateHost j')
-             | StatePort ->
-                  if c = '/' then
-                     search StateFile j'
-                  else
-                     (Buffer.add_char port c; search StatePort j')
-             | StateFile ->
-                  Buffer.add_char file c;
-                  search StateFile j'
+   let proto = ref "" in
+   let host = ref "" in
+   let port = ref "" in
+   let file = ref "" in
+   let rec search state s =
+      match state with
+         StateProto ->
+            (match String.index_opt s colon with
+                Some i -> let p, h = split_at i s in
+                             proto := p; search StateHost h
+              | None -> proto := s)
+       | StateHost ->
+            (match String.index_opt s colon with
+                Some i -> let h, p = split_at i s in
+                             host := h; search StatePort p
+              | None -> (match String.index_opt s '/' with
+                            Some i -> let h, f = split_at i s in
+                                         host := h; search StateFile f
+                          | None -> host := s))
+       | StatePort ->
+            (match String.index_opt s '/' with
+                Some i -> let p, f = split_at i s in
+                             port := p; search StateFile f
+              | None -> port := s)
+       | StateFile ->
+            file := s
    in
-   let _ = search StateProto 0 in
-      { uri_proto = Buffer.contents proto;
-        uri_host = Buffer.contents host;
+   let () = search StateProto s in
+      { uri_proto = !proto;
+        uri_host = !host;
         uri_port =
-           (let i = parse_int (Buffer.contents port) in
+           (let i = parse_int !port in
                if i = 0 then
                   None
                else
                   Some i);
-        uri_path = Buffer.contents file
+        uri_path = !file
       }
 
 let split_eq_val arg =

refiner/reflib/match_seq.ml

@@ -39,7 +39,7 @@ open Term
 open TermType
 open TermSubst
 
-let _ = show_loading "Loading Term_subst_ds%t"
+let () = show_loading "Loading Term_subst_ds"
 
 let cant_match_hyp = RefineError ("Match_seq.match_hyp", StringError "sequents do not match")
 let fail_match _ = raise cant_match_hyp

refiner/reflib/ml_term.ml

@@ -37,7 +37,7 @@ open Term_io
 (*
  * Header.
  *)
-let magic = "MP-OCaml terms:"
+let magic = "MP-ML_terms:"
 let magic_len = String.length magic
 
 let check_magic s =
@@ -49,10 +49,10 @@ let check_magic s =
  *)
 let string_of_term_lists ts mts opnames nums =
    let terms =
-      List.map denormalize_term ts,
-      List.map denormalize_meta_term mts,
-      opnames,
-      nums
+      Lm_array_util.of_list_map denormalize_term ts,
+      Lm_array_util.of_list_map denormalize_meta_term mts,
+      Array.of_list opnames,
+      Array.of_list nums
    in
       magic ^ Marshal.to_string terms []
 
@@ -62,11 +62,11 @@ let string_of_term_lists ts mts opnames nums =
 let term_arrays_of_string s =
    check_magic s;
    let ts, mts, opnames, nums =
-      (Marshal.from_string s magic_len : Refiner_io.TermType.term list * Refiner_io.TermType.meta_term list * opname list * Lm_num.num list) in
-      Array.of_list (List.map normalize_term ts),
-      Array.of_list (List.map normalize_meta_term mts),
-      Array.of_list (List.map normalize_opname opnames),
-      Array.of_list nums
+      (Marshal.from_string s magic_len : Refiner_io.TermType.term array * Refiner_io.TermType.meta_term array * opname array * Lm_num.num array) in
+      Array.map normalize_term ts,
+      Array.map normalize_meta_term mts,
+      Array.map normalize_opname opnames,
+      nums
 
 (*
  * -*-

refiner/reflib/unify_mm.ml

@@ -596,19 +596,19 @@ let rec terms2temp_multieq t0 t1 consts u var_hashtbl b_asslist0 b_asslist1 =
          let op_n0 =List.length tbvs_list0
          and op_n1 =List.length tbvs_list1 in
          if not (op_n0=op_n1) then raise(Clash(ClashTerms("terms2temp_multieq:7",t0,t1)));
-         let op_a0 = Array.of_list (List.map List.length tbvs_list0)
-         and op_a1 = Array.of_list (List.map List.length tbvs_list1) in
+         let op_a0 = Lm_array_util.of_list_map List.length tbvs_list0
+         and op_a1 = Lm_array_util.of_list_map List.length tbvs_list1 in
          if not (op_a0=op_a1) then raise(Clash(ClashTerms("terms2temp_multieq:8",t0,t1)));
          let fs = { opsymb = op0;
                     oparity_n = op_n0;
                     oparity_a = op_a0 ;
                     b_length = 2;
                     opbinding = (Array.init op_n0
-                                 (function i -> (Array.make op_a0.(i) [] )
+                                 (fun i -> (Array.make op_a0.(i) [] )
                                  )
                                 );
                     renamings = (Array.init op_n0
-                                 (function i -> (Array.make op_a0.(i) (V null_var) )
+                                 (fun i -> (Array.make op_a0.(i) (V null_var) )
                                  )
                                 );
                     timestamp = (-1)

refiner/rewrite/rewrite_compile_contractum.ml

@@ -55,8 +55,8 @@ open Rewrite_types
 (*
  * Show the file loading.
  *)
-let _ =
-   show_loading "Loading Rewrite_compile_contractum%t"
+let () =
+   show_loading "Loading Rewrite_compile_contractum"
 
 let debug_rewrite = load_debug "rewrite"