(* 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 
   | 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

(* 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) =
   let pos = 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) = (tref_uref r, b)

let ie_eq ((u1, f1), b1) ((u2, f2), b2) = 
   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 inspect_uri main l uri t c =
   let fi = 
      match (t, c) with
         | (None, _) -> (None, None)
	 | (Some t0, c0) -> (Some (t0 + 1), c0) 
      in
   ie_insert ((uri, fi), main) l 

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

let inspect t = inspect_term true [] t 

(* query building functions *)

let build_select (r, b) n =
   let rvar = "uri" ^ string_of_int n in
   let svar = "s" ^ 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 locate s = 
   let locate_aux txt =
      let query = 
         MQList (MQSelect ("uri", 
	                   MQPattern ("cic", [MQAstAst], "con", (None, None)), 
			   MQIs (MQFunc (MQName, "uri"),
			         MQCons txt
			        )
			  )
		)
      in
       match Mqint.execute query with
          MQStrUri l ->
           out_query query ^ nl ^ "Result: " ^  nl ^
            String.concat nl l ^ nl
        | MQRefs _ -> assert false (*CSC: ????????????????????????????? *)
   in
   match Str.split (Str.regexp "[ \t]+") s with
      | [] -> ""
      | head :: tail -> par ^ locate_aux head 
;;

let backward t =
   let uil = inspect t in
   let til = List.map tie_uie uil in
   let query = MQList (build_inter 0 til) in
    match Mqint.execute query with
       MQStrUri l ->
        par ^ out_query query ^ nl ^ (* ^ par ^ out_il uil ^ *)
        "Result: " ^  nl ^ String.concat nl l ^ nl
     | MQRefs _ -> assert false (*CSC: ????????????????????????????? *)
;;

let init = Mqint.init;;
let close = Mqint.close;;