(* *)
(******************************************************************************)
+
+(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
+let wrong_xpointer_format_from_wrong_xpointer_format' uri =
+ try
+ let index_sharp = String.index uri '#' in
+ let index_rest = index_sharp + 10 in
+ let baseuri = String.sub uri 0 index_sharp in
+ let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in
+ baseuri ^ "#" ^ rest
+ with Not_found -> uri
+;;
+
(* GLOBAL CONSTANTS *)
let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
"</html>"
;;
+(*
let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
+*)
+let prooffile = "/public/sacerdot/currentproof";;
(*CSC: the getter should handle the innertypes, not the FS *)
+(*
let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
+*)
+let innertypesfile = "/public/sacerdot/innertypes";;
(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
String.sub uri 4 (String.length uri - 4)
;;
+(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
+let get_last_query =
+ let query = ref "" in
+ MQueryGenerator.set_confirm_query
+ (function q -> query := MQueryUtil.text_of_query q ; true) ;
+ function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
+;;
+
let locate rendering_window () =
let inputt = (rendering_window#inputt : GEdit.text) in
let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
[] -> ()
| head :: tail ->
inputt#delete_text 0 inputlen ;
- let MathQL.MQRefs uris, html = MQueryGenerator.locate head in
+ let result = MQueryGenerator.locate head in
+ let uris =
+ List.map
+ (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
+ result in
+ let html = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") in
output_html outputhtml html ;
let uri' = user_uri_choice uris in
ignore ((inputt#insert_text uri') ~pos:0)
None -> ()
| Some metano ->
let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
- let MathQL.MQRefs uris, html =
- MQueryGenerator.backward metasenv ey ty level
- in
+ let result = MQueryGenerator.backward metasenv ey ty level in
+ let uris =
+ List.map
+ (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
+ result in
+ let html =
+ " <h1>Backward Query: </h1>" ^
+ " <h2>Levels: </h2> " ^
+ MQueryGenerator.string_of_levels (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
+ " <pre>" ^ get_last_query result ^ "</pre>" in
output_html outputhtml html ;
let uri' = user_uri_choice uris in
inputt#delete_text 0 inputlen ;
CicCooking.init () ;
if !usedb then
begin
- MQueryGenerator.init () ;
+ Mqint.init "host=mowgli.cs.unibo.it dbname=helm user=helm" ;
CicTextualParser0.set_locate_object
(function id ->
- let MathQL.MQRefs uris, html = MQueryGenerator.locate id in
+ let result = MQueryGenerator.locate id in
+ let uris =
+ List.map
+ (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
+ result in
+ let html = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") in
begin
match !rendering_window with
None -> assert false
end ;
ignore (GtkMain.Main.init ()) ;
initialize_everything () ;
- if !usedb then MQueryGenerator.close ();
+ if !usedb then Mqint.close ();
;;
(* *)
(******************************************************************************)
-open Cic
-open MathQL
-open MQueryHTML
-open MQueryUtil
-
-(* CIC term inspecting functions ********************************************)
-
-let env = ref [] (* metasemv *)
-let cont = ref [] (* context *)
-
-let ie_out (r, b, v) =
- let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
- res (pos ^ str_uref r) ^ nl ()
- (* FG: si puo' usare xp_str_uref se si vuole xpointer *)
-
-let rec il_out = function
- | [] -> ""
- | head :: tail -> ie_out head ^ il_out tail
-
-let rec il_max = function
- | [] -> 0
- | (_, _, v) :: tail ->
- let v0 = il_max tail in
- if v > v0 then v else v0
-
-let ie_str_uri (u, b, v) = xp_str_uref u
-
-let rec il_restrict level = function
- | [] -> []
- | (u, b, v) :: tail ->
- if v <= level then (u, b, v) :: il_restrict level tail
- else il_restrict level tail
-
-let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) =
- UriManager.eq u1 u2 && f1 = f2 && b1 = b2
-
-let rec ie_insert ie = function
- | [] -> [ie]
- | head :: tail ->
- head :: if ie_eq head ie then tail else ie_insert ie tail
-
-let degree t =
- let u0 = CicTypeChecker.type_of_aux' !env !cont t in
- let u = CicReduction.whd !cont u0 in
- let rec deg = function
- | Sort _ -> 1
- | Cast (uu, _) -> deg uu
- | Prod (_, _, tt) -> deg tt
- | _ -> 2
- in deg u
-
-let inspect_uri main l uri tc v term =
- let d = degree term in
- let fi = match tc with
- | t0 :: c0 :: _ -> [t0 + 1; c0]
- | t0 :: _ -> [t0 + 1]
- | [] -> []
- in ie_insert ((uri, fi), main, 2 * v + d - 1) l
-
-let rec inspect_term main l v term =
- match term with
- | Rel _ -> l
- | Meta (_, _) -> l
- | Sort _ -> l
- | Implicit -> l
- | Var u -> inspect_uri main l u [] v term
- | Const (u, _) -> inspect_uri main l u [] v term
- | MutInd (u, _, t) -> inspect_uri main l u [t] v term
- | MutConstruct (u, _, t, c) -> inspect_uri main l u [t; c] v term
- | Cast (uu, _) ->
- inspect_term main l v uu
- | Prod (_, uu, tt) ->
- let luu = inspect_term false l (v + 1) uu in
- inspect_term main luu (v + 1) tt
- | Lambda (_, uu, tt) ->
- let luu = inspect_term false l (v + 1) uu in
- inspect_term false luu (v + 1) tt
- | LetIn (_, uu, tt) ->
- let luu = inspect_term false l (v + 1) uu in
- inspect_term false luu (v + 1) tt
- | Appl m -> inspect_list main l true v m
- | MutCase (u, _, t, tt, uu, m) ->
- let lu = inspect_uri main l u [t] (v + 1) term in
- let ltt = inspect_term false lu (v + 1) tt in
- let luu = inspect_term false ltt (v + 1) uu in
- inspect_list main luu false (v + 1) m
- | Fix (_, m) -> inspect_ind l (v + 1) m
- | CoFix (_, m) -> inspect_coind l (v + 1) m
-and inspect_list main l head v = function
- | [] -> l
- | tt :: m ->
- let ltt = inspect_term main l (if head then v else v + 1) tt in
- inspect_list false ltt false v m
-and inspect_ind l v = function
- | [] -> l
- | (_, _, tt, uu) :: m ->
- let ltt = inspect_term false l v tt in
- let luu = inspect_term false ltt v uu in
- inspect_ind luu v m
-and inspect_coind l v = function
- | [] -> l
- | (_, tt, uu) :: m ->
- let ltt = inspect_term false l v tt in
- let luu = inspect_term false ltt v uu in
- inspect_coind luu v m
-
-let rec inspect_backbone = function
- | Cast (uu, _) -> inspect_backbone uu
- | Prod (_, _, tt) -> inspect_backbone tt
- | LetIn (_, uu, tt) -> inspect_backbone tt
- | t -> inspect_term true [] 0 t
-
-let inspect t = inspect_backbone t
-
-(* query building functions *************************************************)
-
-let issue = ref (fun _ -> true)
-
-let save s =
- let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
- (64 * 6 + 8 * 6 + 4) "MQGenLog.htm" in
- output_string och s; flush och; s
-
-let build_result query =
- if ! issue query then
- let html = par () ^ out_query query ^ nl () in
- let result = Mqint.execute query in
- result, save (html ^ out_result result)
- else MQRefs [], ""
-
-let build_select (r, b, v) n =
- let rvar = "ref" ^ string_of_int n in
- let svar = "str" ^ string_of_int n in
- let mqs = if b then MQMConclusion else MQConclusion in
- MQSelect (rvar,
- MQUse (MQReference [xp_str_uref r], svar),
- MQIs (MQStringSVar svar, mqs)
- )
-
-let rec build_inter n = function
- | [] -> MQPattern (None, [MQBSS], [MQFSS])
- | [ie] -> build_select ie n
- | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
-
-let restrict_universe query =
- function
- [] -> query (* no constraints ===> the universe is the library *)
- | l ->
- let universe =
- MQReference (List.map ie_str_uri l)
- in
- MQLetIn (
- "universe", universe,
- MQSelect (
- "uri", query,
- MQSubset (
- MQSelect (
- "uri2",
- MQUsedBy (MQListRVar "uri", "pos"),
- MQOr (
- MQIs (MQStringSVar "pos", MQConclusion),
- MQIs (MQStringSVar "pos", MQMConclusion)
- )
- ),
- MQListLVar "universe"
- )
- )
- )
-
-let init = Mqint.init
-
-let close = Mqint.close
-
-let locate_query s =
-(*CSC: next query to be fixed
- 1) I am exploiting the bug that does not quote '|'
- 2) I am searching only constants and mutual inductive definition blocks
- (i.e. no fragment identifier at all)
-*)
- MQList (MQSelect ("ref",
- MQPattern (Some "cic", [MQBSS ; MQBC ".con|.ind"],[]),
- MQIs (MQFunc (MQName, "ref"),
- MQCons s
- )
- )
- )
+(* level managing functions *************************************************)
+
+type levels_spec = (string * bool * int) list
+
+let levels_of_term metasenv context term =
+ let module TC = CicTypeChecker in
+ let module Red = CicReduction in
+ let module Util = MQueryUtil in
+ let degree t =
+ let rec degree_aux = function
+ | Cic.Sort _ -> 1
+ | Cic.Cast (u, _) -> degree_aux u
+ | Cic.Prod (_, _, t) -> degree_aux t
+ | _ -> 2
+ in
+ let u = TC.type_of_aux' metasenv context t in
+ degree_aux (Red.whd context u)
+ in
+ let entry_eq (s1, b1, v1) (s2, b2, v2) =
+ s1 = s2 && b1 = b2
+ in
+ let rec entry_in e = function
+ | [] -> [e]
+ | head :: tail ->
+ head :: if entry_eq head e then tail else entry_in e tail
+ in
+ let inspect_uri main l uri tc v term =
+ let d = degree term in
+ entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l
+ in
+ let rec inspect_term main l v term = match term with
+ | Cic.Rel _ -> l
+ | Cic.Meta (_, _) -> l
+ | Cic.Sort _ -> l
+ | Cic.Implicit -> l
+ | Cic.Var u -> inspect_uri main l u [] v term
+ | Cic.Const (u, _) -> inspect_uri main l u [] v term
+ | Cic.MutInd (u, _, t) -> inspect_uri main l u [t] v term
+ | Cic.MutConstruct (u, _, t, c) -> inspect_uri main l u [t; c] v term
+ | Cic.Cast (uu, _) ->
+ inspect_term main l v uu
+ | Cic.Prod (_, uu, tt) ->
+ let luu = inspect_term false l (v + 1) uu in
+ inspect_term main luu (v + 1) tt
+ | Cic.Lambda (_, uu, tt) ->
+ let luu = inspect_term false l (v + 1) uu in
+ inspect_term false luu (v + 1) tt
+ | Cic.LetIn (_, uu, tt) ->
+ let luu = inspect_term false l (v + 1) uu in
+ inspect_term false luu (v + 1) tt
+ | Cic.Appl m -> inspect_list main l true v m
+ | Cic.MutCase (u, _, t, tt, uu, m) ->
+ let lu = inspect_uri main l u [t] (v + 1) term in
+ let ltt = inspect_term false lu (v + 1) tt in
+ let luu = inspect_term false ltt (v + 1) uu in
+ inspect_list main luu false (v + 1) m
+ | Cic.Fix (_, m) -> inspect_ind l (v + 1) m
+ | Cic.CoFix (_, m) -> inspect_coind l (v + 1) m
+ and inspect_list main l head v = function
+ | [] -> l
+ | tt :: m ->
+ let ltt = inspect_term main l (if head then v else v + 1) tt in
+ inspect_list false ltt false v m
+ and inspect_ind l v = function
+ | [] -> l
+ | (_, _, tt, uu) :: m ->
+ let ltt = inspect_term false l v tt in
+ let luu = inspect_term false ltt v uu in
+ inspect_ind luu v m
+ and inspect_coind l v = function
+ | [] -> l
+ | (_, tt, uu) :: m ->
+ let ltt = inspect_term false l v tt in
+ let luu = inspect_term false ltt v uu in
+ inspect_coind luu v m
+ in
+ let rec inspect_backbone = function
+ | Cic.Cast (uu, _) -> inspect_backbone uu
+ | Cic.Prod (_, _, tt) -> inspect_backbone tt
+ | Cic.LetIn (_, uu, tt) -> inspect_backbone tt
+ | t -> inspect_term true [] 0 t
+ in
+ inspect_backbone term
+
+let string_of_levels l sep =
+ let entry_out (s, b, v) =
+ let pos = if b then " HEAD: " else " TAIL: " in
+ string_of_int v ^ pos ^ s ^ sep
+ in
+ let rec levels_out = function
+ | [] -> ""
+ | head :: tail -> entry_out head ^ levels_out tail
+ in
+ levels_out l
+
+(* Query issuing functions **************************************************)
+
+exception Discard
+
+let nl = " <p>\n"
+
+let query_num = ref 1
+
+let log_file = ref ""
+
+let confirm_query = ref (fun _ -> true)
+
+let info = ref []
+
+let set_log_file f =
+ log_file := f
+
+let set_confirm_query f =
+ confirm_query := f
+
+let get_query_info () = ! info
+
+let execute_query query =
+ let module Util = MQueryUtil in
+ let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
+ let perm = 64 * 6 + 8 * 6 + 4 in
+ let time () =
+ let lt = Unix.localtime (Unix.time ()) in
+ "NEW LOG: " ^
+ string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
+ string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
+ string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
+ string_of_int (lt.Unix.tm_hour) ^ ":" ^
+ string_of_int (lt.Unix.tm_min) ^ ":" ^
+ string_of_int (lt.Unix.tm_sec)
+ in
+ let log q r =
+ let och = open_out_gen mode perm ! log_file in
+ if ! query_num = 1 then output_string och (time () ^ nl);
+ let str = "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^
+ "Result:" ^ nl ^ Util.text_of_result r nl in
+ output_string och str;
+ flush och
+ in
+ let execute q =
+ let r = Mqint.execute q in
+ if ! log_file <> "" then log q r;
+ info := string_of_int ! query_num :: ! info;
+ incr query_num;
+ r
+ in
+ if ! confirm_query query then execute query else raise Discard
+
+(* Query building functions ************************************************)
let locate s =
- let MQRefs uris, html = build_result (locate_query s) in
-(*CSC: here I am mapping .ind URIs to .ind#1/1, i.e. the first type of *)
-(*CSC: the mutual inductive block. It must be removed once the query *)
-(*CSC: works reasonably. *)
- MQRefs (
- List.map
- (function uri ->
- if String.sub uri (String.length uri - 4) 4 = ".ind" then
- uri ^ "#1/1"
- else
- uri
- ) uris
- ), html
-;;
-
-let levels e c t =
- env := e; cont := c;
- let il = inspect t in
- par () ^ il_out il ^ nl ()
-
-let call_back f =
- issue := f
+ let module M = MathQL in
+ let q = M.Ref (M.Fun "reference" (M.Const [s])) in
+ execute_query q
let backward e c t level =
- let t0 = Sys.time () in
- env := e; cont := c;
- let il = inspect t in
- let query = build_inter 0 (il_restrict level il) in
- let query' = restrict_universe query il in
- let query'' = MQList query' in
- let res = build_result query'' in
- let r,html = res in
- if html <> "" then
- begin
- print_endline ("GEN = " ^ string_of_int (List.length il) ^ ":" ^
- string_of_float (Sys.time () -. t0) ^ "s");
- r, par () ^ il_out il ^ html
- end else res
+ let module M = MathQL in
+ let v_pos = M.Const ["MainConclusion"; "InConclusion"] in
+ let q_where = M.Sub (M.RefOf (
+ M.Select ("uri",
+ M.Relation (M.ExactOp, ["refObj"], M.RVar "uri0", ["pos"]),
+ M.Ex ["uri"] (M.Meet (M.VVar "positions", M.Record ("uri", "pos")))
+ )), M.VVar "universe"
+ )
+ in
+ let uri_of_entry (r, b, v) = r in
+ let rec restrict level = function
+ | [] -> []
+ | (u, b, v) :: tail ->
+ if v <= level then (u, b, v) :: restrict level tail
+ else restrict level tail
+ in
+ let build_select (r, b, v) =
+ let pos = if b then "MainConclusion" else "InConclusion" in
+ M.Select ("uri",
+ M.Relation (M.ExactOp, ["backPointer"], M.Ref (M.Const [r]), ["pos"]),
+ M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", "pos")))
+ )
+ in
+ let rec build_intersect = function
+ | [] -> M.Pattern (M.Const [".*"])
+ | [hd] -> build_select hd
+ | hd :: tl -> M.Intersect (build_select hd, build_intersect tl)
+ in
+ let levels = levels_of_term e c t in
+ let rest = restrict level levels in
+ info := [string_of_int (List.length rest)];
+ let q_in = build_intersect rest in
+ let q_select = M.Select ("uri0", q_in, q_where) in
+ let universe = M.Const (List.map uri_of_entry levels) in
+ let q_let_u = M.LetVVar ("universe", universe, q_select) in
+ let q_let_p = M.LetVVar ("positions", v_pos, q_let_u) in
+ execute_query q_let_p
+let connection_param = "host=mowgli.cs.unibo.it dbname=helm user=helm"
+
+let show_queries = ref false
+
let use_db = ref true
let db_down = ref true
+let nl = " <p>\n"
+
let check_db () =
- if ! db_down then begin
- if ! use_db then begin
- MQueryGenerator.init (); db_down := false
- end else
- raise (Failure "Operation impossible in restricted mode")
- end
-
+ if ! db_down then
+ if ! use_db then begin Mqint.init connection_param; db_down := false; true end
+ else begin print_endline "Not issuing in restricted mode"; false end
+ else true
+
+let default_confirm q =
+ let module Util = MQueryUtil in
+ if ! show_queries then print_string (Util.text_of_query q ^ nl);
+ let b = check_db () in
+ if ! db_down then print_endline "db_down"; b
+
let get_terms () =
let terms = ref [] in
let lexbuf = Lexing.from_channel stdin in
*)
in print_endline s; flush stdout
-let locate name =
- check_db ();
- print_endline (snd (MQueryGenerator.locate name)) ;
- flush stdout
+let dbc () =
+ let on = check_db () in
+ if on then ignore (Mqint.check ())
let rec display = function
| [] -> ()
| term :: tail ->
display tail;
- print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
+ print_string ("? " ^ CicPp.ppterm term ^ nl);
flush stdout
-let rec levels = function
- | [] -> ()
- | term :: tail ->
- levels tail;
- print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
- print_endline (MQueryGenerator.levels [] [] term);
+let levels l =
+ let module Gen = MQueryGenerator in
+ let rec levels_aux = function
+ | [] -> ()
+ | term :: tail ->
+ levels_aux tail;
+ print_string ("? " ^ CicPp.ppterm term ^ nl);
+ print_string (Gen.string_of_levels (Gen.levels_of_term [] [] term) nl);
+ flush stdout
+ in
+ levels_aux l
+
+let execute ich =
+ let module Util = MQueryUtil in
+ let module Gen = MQueryGenerator in
+ Gen.set_confirm_query default_confirm;
+ try
+ let q = Util.query_of_text (Lexing.from_channel ich) in
+ print_endline (Util.text_of_result (Gen.execute_query q) nl);
+ flush stdout
+ with Gen.Discard -> ()
+
+let locate name =
+ let module Util = MQueryUtil in
+ let module Gen = MQueryGenerator in
+ Gen.set_confirm_query default_confirm;
+ try
+ print_endline (Util.text_of_result (Gen.locate name) nl);
flush stdout
-
-let mbackward n m l =
+ with Gen.Discard -> ()
+
+let mbackward n m l =
+ let module Util = MQueryUtil in
+ let module Gen = MQueryGenerator in
let queries = ref [] in
- let issue query =
- if List.mem query ! queries then false
- else begin queries := query :: ! queries; true end
+ let confirm query =
+ if List.mem query ! queries then false
+ else begin queries := query :: ! queries; default_confirm query end
in
let rec backward level = function
| [] -> ()
| term :: tail ->
backward level tail;
- print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
- print_endline (snd (MQueryGenerator.backward [] [] term level)) ;
- flush stdout
+ try
+ if Mqint.get_stat () then
+ print_string ("? " ^ CicPp.ppterm term ^ nl);
+ let t0 = Sys.time () in
+ let r = Gen.backward [] [] term level in
+ let t1 = Sys.time () -. t0 in
+ let info = Gen.get_query_info () in
+ let num = List.nth info 0 in
+ let gen = List.nth info 1 in
+ if Mqint.get_stat () then
+ print_string (num ^ " GEN = " ^ gen ^ ":" ^ string_of_float t1 ^ "s" ^ nl);
+ print_string (Util.text_of_result r nl);
+ flush stdout
+ with Gen.Discard -> ()
in
- check_db ();
- MQueryGenerator.call_back issue;
+ Gen.set_confirm_query confirm;
for level = max m n downto min m n do
prerr_endline ("toplevel: backward: trying level " ^
string_of_int level);
done;
prerr_endline ("toplevel: backward: " ^
string_of_int (List.length ! queries) ^
- " queries issued");
- MQueryGenerator.call_back (fun _ -> true)
-
+ " queries issued")
+
+let prerr_help () =
+ prerr_endline "\nUSAGE: toplevel.opt OPTIONS < INPUTFILE\n";
+ prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for";
+ prerr_endline "testing purposes. Toplevel reads its input from stdin and produces ith output";
+ prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n";
+ prerr_endline "OPTIONS:\n";
+ prerr_endline "-h -help shows this help message";
+ prerr_endline "-q -show-queries outputs generated queries";
+ prerr_endline "-s -stat outputs interpreter statistics";
+ prerr_endline "-c -db-check checks the database connection";
+ prerr_endline "-r -restricted -nodb enables restricted mode: queries are not issued";
+ prerr_endline "-t -typeof URI outputs the CIC type of the given HELM object";
+ prerr_endline "-x -execute issues a query given in the input file";
+ prerr_endline "-d -disply outputs the CIC terms given in the input file";
+ prerr_endline "-l -levels outputs the cut levels of the CIC terms given in the input file";
+ prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias";
+ prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all CIC terms";
+ prerr_endline " in the input file";
+ prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0 on all";
+ prerr_endline " CIC terms in the input file\n";
+ prerr_endline "NOTES: CIC terms are read with the HELM CIC Textual Parser";
+ prerr_endline " -typeof does not work with inductive types and proofs in progress\n"
+
let parse_args () =
let rec parse = function
| [] -> ()
+ | ("-h"|"-help") :: rem -> prerr_help ()
| ("-d"|"-display") :: rem -> display (get_terms ())
| ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
| ("-l"|"-levels") :: rem -> levels (get_terms ())
- | ("-r"|"-restricted") :: rem -> use_db := false; parse rem
+ | ("-x"|"-execute") :: rem -> execute stdin; parse rem
+ | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
+ | ("-s"|"-stat") :: rem -> Mqint.set_stat true; parse rem
+ | ("-r"|"-restricted"|"-nodb") :: rem -> use_db := false; parse rem
+ | ("-c"|"-db-check") :: rem -> dbc (); parse rem
| ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
| ("-B"|"-backward") :: arg :: rem ->
let m = (int_of_string arg) in
mbackward m m (get_terms ())
- | ("-MB"|"-mbackward") :: arg :: rem ->
+ | ("-MB"|"-multi-backward") :: arg :: rem ->
let m = (int_of_string arg) in
mbackward m 0 (get_terms ())
| _ :: rem -> parse rem
parse (List.tl (Array.to_list Sys.argv))
let _ =
+ let module Gen = MQueryGenerator in
CicCooking.init () ;
Logger.log_callback :=
(Logger.log_to_html
~print_and_flush:(function s -> print_string s ; flush stdout)) ;
+ Mqint.set_stat false;
+ Gen.set_log_file "MQGenLog.htm";
parse_args ();
- if not ! db_down then MQueryGenerator.close ();
+ if not ! db_down then Mqint.close ();
+ Gen.set_confirm_query (fun _ -> true);
prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^
" seconds");
exit 0
projects / helm.git / commitdiff