X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2Ftable_creator%2Ftable_creator.ml;h=423edfb275850908fec3e2d8cff502f50dc99e60;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=7cd3b35f2461eb06c8e5533b3d3581cc6d076712;hpb=c5abd4206112221708a06dbb1bb9df1eb38a451c;p=helm.git diff --git a/helm/ocaml/metadata/table_creator/table_creator.ml b/helm/ocaml/metadata/table_creator/table_creator.ml index 7cd3b35f2..423edfb27 100644 --- a/helm/ocaml/metadata/table_creator/table_creator.ml +++ b/helm/ocaml/metadata/table_creator/table_creator.ml @@ -1,16 +1,24 @@ +open Printf + let map = (MetadataTypes.library_obj_tbl,`RefObj) :: (MetadataTypes.library_sort_tbl,`RefSort) :: (MetadataTypes.library_rel_tbl,`RefRel) :: (MetadataTypes.library_name_tbl,`ObjectName) :: -(* (MetadataTypes.library_???_tbl,`Owners) :: *) + (MetadataTypes.library_hits_tbl,`Hits) :: (MetadataTypes.library_count_tbl,`Count) :: [] let usage argv_o = prerr_string "\nusage:"; - prerr_string ("\t" ^ argv_o ^ " [-index] tablename[=rename]\n\n"); - prerr_string "known tables:"; + prerr_string ("\t" ^ argv_o ^ " what tablename[=rename]\n"); + prerr_string ("\t" ^ argv_o ^ " what all\n\n"); + prerr_endline "what:"; + prerr_endline "\tlist\tlist table names"; + prerr_endline "\ttable\toutput SQL regarding tables"; + prerr_endline "\tindex\toutput SQL regarding indexes"; + prerr_endline "\tfill\toutput SQL filling tables (only \"hits\" supported)\n"; + prerr_string "known tables:\n\t"; List.iter (fun (n,_) -> prerr_string (" " ^ n)) map; prerr_endline "\n" @@ -23,23 +31,53 @@ let parse_args l = assert (len = 1 || len = 2); if len = 1 then (s,s) else (List.nth parts 0, List.nth parts 1)) l + +let destructor_RE = Str.regexp "table_destructor\\(\\|\\.opt\\)$" + +let am_i_destructor () = + try + let _ = Str.search_forward destructor_RE Sys.argv.(0) 0 in true + with Not_found -> false let main () = let len = Array.length Sys.argv in - if len < 2 then + if len < 3 then begin usage Sys.argv.(0); exit 1 end else begin - let from, index = if Sys.argv.(1) = "-index" then 2,true else 1,false in + let tab,idx,fill = + if am_i_destructor () then + (SqlStatements.drop_tables,SqlStatements.drop_indexes, + fun _ t -> [sprintf "DELETE * FROM %s;" t]) + else + (SqlStatements.create_tables,SqlStatements.create_indexes, + SqlStatements.fill_hits) + in + let from = 2 in + let what = + match Sys.argv.(1) with + | "list" -> `List + | "index" -> `Index + | "table" -> `Table + | "fill" -> `Fill + | _ -> failwith "what must be one of \"index\", \"table\", \"fill\"" + in let todo = Array.to_list (Array.sub Sys.argv from (len - from)) in + let todo = match todo with ["all"] -> List.map fst map | todo -> todo in let todo = parse_args todo in let todo = List.map (fun (x,name) -> name, (List.assoc x map)) todo in - print_endline (SqlStatements.create_tables todo); - if index then print_endline (SqlStatements.create_indexes todo) + match what with + | `Index -> print_endline (String.concat "\n" (idx todo)) + | `Table -> print_endline (String.concat "\n" (tab todo)) + | `Fill -> + print_endline (String.concat "\n" + (fill MetadataTypes.library_obj_tbl MetadataTypes.library_hits_tbl)) + | `List -> print_endline (String.concat " " (List.map fst map)) end let _ = main () +