(* 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 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
      save (html ^ out_result result)
    else ""
    
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
                             )
                       )
             )

let locate s =
 (*CSC: the code should be: Mqint.execute (locate_query s)                  *)
 (*CSC: what follows is the patch to map mutual inductive definition blocks *)
 (*CSC: URIs (i.e. no fragment identifier at all) to the URIs of the first  *)
 (*CSC: mutual inductive type of their block.                               *)
 let MQRefs uris = Mqint.execute (locate_query s) in
  MQRefs
   (List.map
    (function uri ->
      if String.sub uri (String.length uri - 4) 4 = ".con" then uri else
       uri ^ "#1/1"
    ) uris)
;;

let locate_html s = build_result (locate_query s);;

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 backward e c t level =
   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 
   par () ^ il_out il ^ build_result query''