(* 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/.
 *)

(******************************************************************************)
(*                                                                            *)
(*                               PROJECT HELM                                 *)
(*                                                                            *)
(*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
(*                                 30/04/2002                                 *)
(*                                                                            *)
(*                                                                            *)
(******************************************************************************)

open Mathql
open Cic

(* string linearization of a reference *)

let str_uptoken = function
   | MQString s -> s
   | MQSlash    -> "/"
   | MQAnyChr   -> "?"
   | MQAst      -> "*"
   | MQAstAst   -> "**"

let rec str_up = function
   | [] -> ""
   | head :: tail -> str_uptoken head ^ str_up tail 

let str_fi = function 
   | (None, _)        -> ""
   | (Some t, None)   -> "#1/" ^ string_of_int t
   | (Some t, Some c) -> "#1/" ^ string_of_int t ^ "/" ^ string_of_int c

let str_tref (p, u, x, i) = 
   p ^ ":/" ^ str_up u ^ "." ^ x ^ str_fi i

let str_uref (u, i) = 
   UriManager.string_of_uri u ^ str_fi i

(* raw HTML representation *)

let key s = "<font color=\"blue\">" ^ s ^ " </font>"

let sym s = s ^ " "

let sep s = s

let con s = "<font color=\"red\">\"" ^ s ^ "\" </font>"

let res s = "<font color=\"brown\">\"" ^ s ^ "\" </font>"

let nl () = "<br>"

let par () = "<p>"

(* HTML representation of a query *)

let out_rvar s = sym s

let out_svar s = sep "$" ^ sym s

let out_tref r = con (str_tref r) 

let out_pat p = out_tref p

let out_func = function
   | MQName -> key "name"

let out_str = function
   | MQCons s      -> con s
   | MQRVar s      -> out_rvar s
   | MQSVar s      -> out_svar s
   | MQFunc (f, r) -> out_func f ^ out_rvar r
   | MQMConclusion -> key "mainconclusion" 
   | MQConclusion  -> key "conclusion" 

let rec out_bool = function
   | MQTrue -> key "true"
   | MQFalse -> key "false"
   | MQIs (s, t) -> out_str s ^ key "is" ^ out_str t
   | MQNot b -> key "not" ^ out_bool b 
   | MQAnd (b1, b2) -> sep "(" ^ out_bool b1 ^ key "and" ^ out_bool b2 ^ sep ")"
   | MQOr (b1, b2) -> sep "(" ^ out_bool b1 ^ key "or" ^ out_bool b2 ^ sep ")"
   
let rec out_list = function
   | MQSelect (r, l, b) -> 
      key "select" ^ out_rvar r ^ key "in" ^ out_list l ^ key "where" ^ out_bool b
   | MQUse (l, v) -> key "use" ^ out_list l ^ key "position" ^ out_svar v
   | MQUsedBy (l, v) -> key "usedby" ^ out_list l ^ key "position" ^ out_svar v
   | MQPattern p -> key "pattern" ^ out_pat p
   | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")"
   | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")"

let out_query = function
   | MQList l -> out_list l

(* HTML representation of a query result *)

let rec out_list = function 
   | []     -> ""
   | u :: l -> res u ^ nl () ^ out_list l 

let out_result qr =
   par () ^ "Result:" ^ nl () ^
   match qr with
      | MQRefs l -> out_list l

(* Converting functions *)

let split s =
   try 
      let i = Str.search_forward (Str.regexp_string ":/") s 0 in
      let p = Str.string_before s i in
      let q = Str.string_after s (i + 2) in
      try
         let j = String.rindex q '.' in
         (p, Str.string_before q j, Str.string_after q (j + 1))
      with 
         Not_found -> (p, q, "")
   with 
      Not_found -> (s, "", "")

let encode = function
   | Str.Text s  -> MQString s
   | Str.Delim s ->  
      if s = "?"  then MQAnyChr else
      if s = "*"  then MQAst    else
      if s = "**" then MQAstAst else
      if s = "/"  then MQSlash  else MQString s

let tref_uref (u, i) =
   let s = UriManager.string_of_uri u in
   match split s with
      | (p, q, r) -> 
         let rx = Str.regexp "\?\|\*\*\|\*\|/" in
         let l = Str.full_split rx q in
         (p, List.map encode l, r, i) 

(* CIC term inspecting functions *)

let out_ie (r, b, v) =
   let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
   res (pos ^ str_uref r) ^ nl () ^
   con (pos ^ str_tref (tref_uref r)) ^ nl ()

let rec out_il = function
   | []           -> ""
   | head :: tail -> out_ie head ^ out_il tail

let tie_uie (r, b, v) = (tref_uref r, b, v)

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 level = ref 0

let inspect_uri main l uri t c v =
   if v > !level then l else
   let fi =
      match (t, c) with
         | (None, _) -> (None, None)
	 | (Some t0, c0) -> (Some (t0 + 1), c0) 
   in
   ie_insert ((uri, fi), main, v) l 

let rec inspect_term main l v = function
   | Rel i                        -> l 
   | Meta (i, _)                  -> l 
   | Sort s                       -> l 
   | Implicit                     -> l 
   | Abst u                       -> l 
   | Var u                        -> inspect_uri main l u None None v
   | Const (u, i)                 -> inspect_uri main l u None None v
   | MutInd (u, i, t)             -> inspect_uri main l u (Some t) None v
   | MutConstruct (u, i, t, c)    -> inspect_uri main l u (Some t) (Some c) v
   | Cast (uu, tt)                -> 
      let luu = inspect_term main l (v + 1) uu in
      inspect_term false luu (v + 1) tt 
   | Prod (n, uu, tt)             ->
      let luu = inspect_term false l (v + 1) uu in
      inspect_term false luu (v + 1) tt
   | Lambda (n, uu, tt)           ->
      let luu = inspect_term false l (v + 1) uu in
      inspect_term false luu (v + 1) tt 
   | LetIn (n, 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 (v + 1) m 
   | MutCase (u, i, t, tt, uu, m) -> 
      let lu = inspect_uri main l u (Some t) None (v + 1) 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 (v + 1) m
   | Fix (i, m)                   -> inspect_ind l (v + 1) m 
   | CoFix (i, m)                 -> inspect_coind l (v + 1) m 
and inspect_list main l v = function
   | []      -> l
   | tt :: m -> 
      let ltt = inspect_term main l v tt in
      inspect_list false ltt v m
and inspect_ind l v = function
   | []                  -> l
   | (n, i, 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
   | (n, 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 inspect t = inspect_term true [] 0 t  

(* query building functions *)

let save s = 
   let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
                          (64 * 6 + 8 * 6 + 4) "mquery.htm" in
   output_string och s; flush och; s

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 (MQPattern r, svar),
	     MQIs (MQSVar svar, mqs)
	    )

let rec build_inter n = function
   | []       -> MQPattern ("cic", [MQAstAst], "con", (None, None))
   | [ie]     -> build_select ie n
   | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)

let build_result query =
   let html = par () ^ out_query query ^ nl () in
   let result = Mqint.execute query in
   save (html ^ out_result result)

let init = Mqint.init

let close = Mqint.close

let locate s = 
   let query = 
      MQList (MQSelect ("ref", 
                        MQPattern ("cic", [MQAstAst], "con", (None, None)),
                        MQIs (MQFunc (MQName, "ref"),
                              MQCons s
                             )
                       )
             )
   in
   build_result query

let backward t n =
   level := n;
   let uil = inspect t in
   let til = List.map tie_uie uil in
   let query = MQList (build_inter 0 til) in 
   par () ^ out_il uil ^ build_result query