(* Copyright (C) 2000, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
 *)

let _ = MQueryStandard.init
let _ = MQueryHELM.init 

let query_num = ref 1

let interp_file = ref "interp.cic" 

let log_file = ref ""

let show_queries = ref false

let int_options = ref ""

let nl = " <p>\n"

module IO = MQueryIO
module U  = MQueryUtil
module I  = MQueryInterpreter
module C  = MQIConn
module G  = MQueryGenerator
module L  = MQGTopLexer
module P  = MQGTopParser
module TL = CicTextualLexer
module TP = CicTextualParser
module C3 = CGLocateInductive
module C2 = CGSearchPattern
module C1 = CGMatchConclusion
module GU = MQGUtil
module M  = MQueryMisc

let get_handle () = 
   C.init (C.flags_of_string ! int_options)
          (fun s -> print_string s; flush stdout) 
             
let issue handle q =
   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
      let out = output_string och in 
      if ! query_num = 1 then out (time () ^ nl);
      out ("Query: " ^ string_of_int ! query_num ^ nl);
      IO.text_of_query out nl q;
      out ("Result: " ^ nl);
      IO.text_of_result out nl r;
      close_out och
   in
   if ! show_queries then IO.text_of_query (output_string stdout) nl q;
   let r = I.execute handle q in    
   IO.text_of_result (output_string stdout) nl r;
   if ! log_file <> "" then log q r; 
   incr query_num;
   flush stdout

let get_interp () =
   let lexer = function
      | TP.ID s                -> P.ID s
      | TP.CONURI u            -> P.CONURI u
      | TP.VARURI u            -> P.VARURI u
      | TP.INDTYURI (u, p)     -> P.INDTYURI (u, p)
      | TP.INDCONURI (u, p, s) -> P.INDCONURI (u, p, s)
      | TP.LETIN               -> P.ALIAS
      | TP.EOF                 -> P.EOF
      | _                     -> assert false
   in
   let ich = open_in ! interp_file in
   let lexbuf = Lexing.from_channel ich in
   let f = P.interp (fun x -> lexer (TL.token x)) lexbuf in
   close_in ich; f
   
let get_terms interp = 
   let interp = get_interp () in
   let lexbuf = Lexing.from_channel stdin in
   let rec aux () =
      try
         let dom, mk_term =
            CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf
         in
         (snd (mk_term interp)) :: aux ()
      with
      CicTextualParser0.Eof -> []
   in
   aux ()

let rec join f v1 v2 =
   match v1, v2 with
      | [], v                          -> f v
      | v, []                          -> f v 
      | h1 :: t1, h2 :: _ when h1 < h2 -> 
         let g h = f (h1 :: h) in join g t1 v2
      | h1 :: _, h2 :: t2 when h1 > h2 -> 
         let g h = f (h2 :: h) in join g v1 t2
      | h1 :: t1, _ :: t2              -> 
         let g h = f (h1 :: h) in join g t1 t2

let rec diff f v1 v2 =
   match v1, v2 with
      | [], _                          -> f []
      | _, []                          -> f v1 
      | h1 :: t1, h2 :: _ when h1 < h2 -> 
         let g h = f (h1 :: h) in diff g t1 v2
      | h1 :: _, h2 :: t2 when h1 > h2 -> diff f v1 t2
      | _ :: t1, _ :: t2               -> diff f t1 t2

let add f r k l = join f r [M.string_of_uriref (k, l)]   

let rec add_cons f r k i j = function
   | []      -> f r
   | _ :: tl -> 
      let g s = add f s k [i; j] in
      add_cons g r k i (succ j) tl

let rec refobj_l refobj_t map f r = function
   | []        -> f r
   | h :: tail -> 
      let f r = refobj_l refobj_t map f r tail in 
      refobj_t f r (map h) 

let rec refobj_t f r = function
   | Cic.Implicit _
   | Cic.Meta _
   | Cic.Sort _      
   | Cic.Rel _                      -> f r 
   | Cic.Cast (t, u) 
   | Cic.Prod (_, t, u) 
   | Cic.Lambda (_, t, u) 
   | Cic.LetIn (_, t, u)            -> 
      let f r = refobj_t f r u in refobj_t f r t 
   | Cic.Appl tl                    -> 
      refobj_l refobj_t (fun x -> x) f r tl 
   | Cic.Fix (_, tl)                ->  
      let f r = refobj_l refobj_t (fun (_, _, _, u) -> u) f r tl in
      refobj_l refobj_t (fun (_, _, t, _) -> t) f r tl
   | Cic.CoFix (_, tl)              -> 
      let f r = refobj_l refobj_t (fun (_, _, u) -> u) f r tl in
      refobj_l refobj_t (fun (_, t, _) -> t) f r tl
   | Cic.Var (k, tl)                -> 
      let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
      add f r k [] 
   | Cic.Const (k, tl)              -> 
      let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
      add f r k [] 
   | Cic.MutInd (k, i, tl)          -> 
      let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
      add f r k [i] 
   | Cic.MutConstruct (k, i, j, tl) -> 
      let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
      add f r k [i; j] 
   | Cic.MutCase (k, i, t, u, tl)   -> 
      let f r = refobj_l refobj_t (fun u -> u) f r tl in
      let f r = refobj_t f r u in
      let f r = refobj_t f r t in
      let f r = add f r k [i] in
      add_cons f r k i 1 tl

let get_refobj f r uri =
   let body, ty = M.get_object (M.uriref_of_string uri) in
   let f r = diff f r [uri] in
   let f r = refobj_t f r body in 
   refobj_t f r ty

let rec get_refobj_l f r = function
   | []       -> f r
   | uri :: l -> 
      let f r = get_refobj_l f r l in
      get_refobj f r uri

let show_refobj uri = 
   let f = List.iter print_endline in 
   get_refobj f [] uri

let compute_shells uri =
   let rec aux r d n = 
      let f p r = 
         let l = List.length r in
	 Printf.printf "found %i objects\n" l; flush stdout;
	 let f d = if l > 0 then aux r d (succ n) in
	 join f d p
      in
      Printf.printf "shells: computing level %i ... " n; flush stdout;
      let f r = get_refobj_l (f r) [] r in
      diff f r d
   in
   aux [uri] [] 0
   
let pp_term_of b uri = 
   let s = try 
      let body, ty = M.get_object (M.uriref_of_string uri) in
      if b then CicPp.ppterm body else CicPp.ppterm ty 
   with
      | M.CurrentProof        -> "proof in progress"
      | M.InductiveDefinition -> "inductive definition"
      | M.IllFormedFragment   -> "ill formed fragment identifier"
   in print_endline s; flush stdout

let rec display = function
   | []           -> ()
   | term :: tail -> 
      display tail;
      print_string ("? " ^ CicPp.ppterm term ^ nl);
      flush stdout

let execute ich =
   let lexbuf = Lexing.from_channel ich in
   let handle = get_handle () in
   let rec execute_aux () =
      try 
         let q = IO.query_of_text lexbuf in
         issue handle q; execute_aux ()
      with End_of_file -> ()
   in
   execute_aux ();
   C.close handle

let compose () =
   let handle = get_handle () in  
   let cl = P.specs L.spec_token (Lexing.from_channel stdin) in
   issue handle (G.compose cl);
   C.close handle

let locate name =
   let handle = get_handle () in  
   issue handle (G.locate name); 
   C.close handle

let unreferred target source =
   let handle = get_handle () in  
   issue handle (G.unreferred target source); 
   C.close handle

let mpattern n m l =
   let queries = ref [] in
   let univ = Some C2.universe in 
   let handle = get_handle () in
   let rec pattern level = function
      | []           -> ()
      | term :: tail -> 
         pattern level tail;
	 print_string ("? " ^ CicPp.ppterm term ^ nl);
	 let t = U.start_time () in
         let om,rm,sm = C2.get_constraints term in
	 let oml,rml,sml = List.length om, List.length rm, List.length sm in 
	 let oo, ool = if level land 1 = 0 then None, 0 else Some om, oml in
	 let ro, rol = if level land 2 = 0 then None, 0 else Some rm, rml in
         let so, sol = if level land 4 = 0 then None, 0 else Some sm, sml in
	 let q = G.query_of_constraints univ (om,rm,sm) (oo,ro,so) in 
	 if not (List.mem q ! queries) then
	 begin
	    issue handle q;
	    Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
	    Printf.printf "%i GEN = %i: %s"
	       (pred ! query_num) (oml + rml + sml + ool + rol + sol) 
	       (U.stop_time t ^ nl);
	    flush stdout; queries := q :: ! queries
	 end
   in 
   for level = max m n downto min m n do
      Printf.eprintf "\nmqgtop: pattern: trying level %i\n" level; 
      flush stderr; pattern level l
   done;
   Printf.eprintf "\nmqgtop: pattern: %i queries issued\n" 
      (List.length ! queries);
   flush stderr;
   C.close handle

let mbackward n m l =
   let queries = ref [] in
   let univ = Some C1.universe in
   let handle = get_handle () in
   let rec backward level = function
      | []           -> ()
      | term :: tail -> 
         backward level tail;
	 print_string ("? " ^ CicPp.ppterm term ^ nl);
	 let t = U.start_time () in
	 let list_of_must, only = C1.get_constraints [] [] term in
         let max_level = pred (List.length list_of_must) in 
	 let must = List.nth list_of_must (min level max_level) in 
	 let q = G.query_of_constraints univ (must, [], []) (Some only , None, None) in 
	 if not (List.mem q ! queries) then
	 begin
	    issue handle q;
	    Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
	    Printf.printf "%i GEN = %i: %s"
	       (pred ! query_num) (List.length must) 
	       (U.stop_time t ^ nl);
	    flush stdout; queries := q :: ! queries
	 end
   in 
   for level = max m n downto min m n do
      Printf.eprintf "\nmqgtop: backward: trying level %i\n" level; 
      flush stderr; backward level l
   done;
   Printf.eprintf "\nmqgtop: backward: %i queries issued\n" 
      (List.length ! queries);
   flush stderr;
   C.close handle

let inductive l = 
   let queries = ref [] in
   let univ = None in 
   let handle = get_handle () in
   let rec aux = function
      | []           -> ()
      | term :: tail -> 
         aux tail;
	 print_string ("? " ^ CicPp.ppterm term ^ nl);
	 let t = U.start_time () in
         let m = C3.get_constraints term in
	 let q = G.query_of_constraints univ m (None, None, None) in 
	 if not (List.mem q ! queries) then
	 begin
	    issue handle q;
	    Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
	    Printf.printf "%i GEN: %s"
	       (pred ! query_num) (U.stop_time t ^ nl);
	    flush stdout; queries := q :: ! queries
	 end
   in 
   aux l;
   Printf.eprintf "\nmqgtop: inductive: %i queries issued\n" 
      (List.length ! queries);
   flush stderr;
   C.close handle

let check () =
   let handle = get_handle () in
   Printf.eprintf 
      "mqgtop: current options: %s, connection: %s\n"  
      ! int_options (if C.connected handle then "on" else "off");
   C.close handle

let prerr_help () =
   prerr_endline "\nUSAGE: mqgtop.opt OPTIONS < INPUTFILE\n"; 
   prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for";
   prerr_endline "testing purposes. mqgtop 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 "-l  -log-file FILE      sets the log file";
   prerr_endline "-o  -options STRING     sets the interpreter options";
   prerr_endline "-c  -check              checks the database connection";
   prerr_endline "-t  -typeof URI         outputs the CIC type of the given HELM object";
   prerr_endline "-b  -bodyof URI         outputs the CIC body of the given HELM object";
   prerr_endline "-r  -refobj URI         outputs the references in the given HELM object";
   prerr_endline "-s  -shells URI         computes the reference shells of the given HELM object";
   prerr_endline "-x  -execute            issues a query given in the input file";
   prerr_endline "-i  -interp FILE        sets the CIC short names interpretation file";
   prerr_endline "-d  -disply             outputs the CIC terms given in the input file";
   prerr_endline "-L  -locate ALIAS       issues the \"Locate\" query for the given alias";
   prerr_endline "-U  T_PATTERN S_PATTERN issues the \"Unreferred\" query for the given patterns";
   prerr_endline "-C  -compose            issues the \"Compose\" query reading its specifications";
   prerr_endline "                        from the input file"; 
   prerr_endline "-B  -backward LEVEL     issues the \"Backward\" query for the given level on all";
   prerr_endline "                        CIC terms in the input file";
   prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0";
   prerr_endline "                        on all CIC terms in the input file";
   prerr_endline "-P  -pattern LEVEL      issues the \"Pattern\" query for the given level on all";
   prerr_endline "                        CIC terms in the input file";
   prerr_endline "-MP -multi-pattern      issues the \"Pattern\" query for each level from 7 to 0";
   prerr_endline "                        on all CIC terms in the input file";
   prerr_endline "-I                      issues the \"Inductive\" query on all CIC terms in the";
   prerr_endline "                        input file\n";
   prerr_endline "NOTES: * current interpreter options are:";
   prerr_endline "         P (postgres), G (Galax), S (show statistics), Q (quiet)";
   prerr_endline "       * CIC terms are read with the HELM CIC Textual Parser";
   prerr_endline "       * -typeof / -bodyof do not work with proofs in progress\n"

let rec parse = function
   | [] -> ()
   | ("-h"|"-help") :: rem -> prerr_help (); parse rem
   | ("-i"|"-interp") :: arg :: rem -> interp_file := arg; parse rem
   | ("-d"|"-display") :: rem -> display (get_terms ()); parse rem
   | ("-t"|"-typeof") :: arg :: rem -> pp_term_of false arg; parse rem
   | ("-b"|"-bodyof") :: arg :: rem -> pp_term_of true arg; parse rem
   | ("-r"|"-refobj") :: arg :: rem -> show_refobj arg; parse rem
   | ("-s"|"-shells") :: arg :: rem -> compute_shells arg; parse rem
   | ("-x"|"-execute") :: rem -> execute stdin; parse rem
   | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
   | ("-o"|"-options") :: arg :: rem -> int_options := arg; parse rem
   | ("-c"|"-check") :: rem -> check (); parse rem
   | ("-l"|"-log-file") :: arg :: rem -> log_file := arg; parse rem
   | ("-L"|"-Locate") :: arg :: rem -> locate arg; parse rem
   | ("-C"|"-compose") :: rem -> compose (); parse rem   
   | ("-B"|"-backward") :: arg :: rem ->
      let m = (int_of_string arg) in mbackward m m (get_terms ()); parse rem
   | ("-MB"|"-multi-backward") :: arg :: rem ->
      let m = (int_of_string arg) in mbackward m 0 (get_terms ()); parse rem
   | ("-P"|"-pattern") :: arg :: rem ->
      let m = (int_of_string arg) in mpattern m m (get_terms ()); parse rem
   | ("-MP"|"-multi-pattern") :: rem -> mpattern 7 0 (get_terms ()); parse rem
   | ("-U"|"-unreferred") :: arg1 :: arg2 :: rem ->
      unreferred arg1 arg2; parse rem
   | ("-I"|"-inductive") :: rem -> inductive (get_terms ()); parse rem
   | _ :: rem -> parse rem

let _ =
   Helm_registry.load_from "/home/fguidi/miohelm/gTopLevel.conf.xml";
   let t = U.start_time () in
(*   Logger.log_callback :=
      (Logger.log_to_html 
       ~print_and_flush:(fun s -> print_string s; flush stdout)) ; 
*)   parse (List.tl (Array.to_list Sys.argv)); 
   prerr_endline ("mqgtop: done in " ^ (U.stop_time t));
   exit 0