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

type uri = string
type position = string
type depth = string
type sort = string 
 
type spec = MustObj  of uri list * position list * depth list
          | MustSort of sort list * position list * depth list
	  | MustRel  of position list * depth list
	  | OnlyObj  of uri list * position list * depth list
          | OnlySort of sort list * position list * depth list
	  | OnlyRel  of position list * depth list
	  | Universe of position list 

type builtin_t = MainHypothesis
               | InHypothesis
	       | MainConclusion
	       | InConclusion
	       | InBody
	       | Set
	       | Prop
	       | Type

let text_of_builtin s =
   let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
   if s = ns ^ "MainHypothesis" then "$MH" else
   if s = ns ^ "InHypothesis" then "$IH" else
   if s = ns ^ "MainConclusion" then "$MC" else
   if s = ns ^ "InConclusion" then "$IC" else
   if s = ns ^ "InBody" then "$IB" else
   if s =      "Set" then "$SET" else
   if s =      "Prop" then "$PROP" else
   if s =      "Type" then "$TYPE" else s

let text_of_spec out l =
   let rec iter = function 
      | []        -> ()
      | [s]       -> out "\""; out (text_of_builtin s); out "\""
      | s :: tail -> out "\""; out (text_of_builtin s); out "\", "; iter tail
   in
   let txt_list l = out "{"; iter l; out "} " in
   let txt_spec = function
      | MustObj  (u, p, d) -> out "mustobj  "; txt_list u; txt_list p; txt_list d; out "\n" 
      | MustSort (s, p, d) -> out "mustsort "; txt_list s; txt_list p; txt_list d; out "\n" 
      | MustRel  (   p, d) -> out "mustrel  "; txt_list p; txt_list d; out "\n" 
      | OnlyObj  (u, p, d) -> out "onlyobj  "; txt_list u; txt_list p; txt_list d; out "\n" 
      | OnlySort (s, p, d) -> out "onlysort "; txt_list s; txt_list p; txt_list d; out "\n" 
      | OnlyRel  (   p, d) -> out "onlyrel  "; txt_list p; txt_list d; out "\n" 
      | Universe (   p   ) -> out "universe "; txt_list p; out "\n" 
   in   
   List.iter txt_spec l  

module M = MathQL

let locate s =
   let query = 
      M.Property true M.RefineExact ["objectName"] [] [] [] []
                 false (M.Const s) 
   in M.StatQuery query

let compose cl = 
   let letin = ref [] in
   let must = ref [] in
   let onlyobj = ref [] in
   let onlysort = ref [] in
   let onlyrel = ref [] in
   let only = ref true in
   let univ = ref [] in
   let set_val = function
      | [s] -> M.Const s
      | l   -> 
	 let msval = M.Set (List.map (fun s -> M.Const s) l) in
	 if ! only then begin
	   let vvar = "val" ^ string_of_int (List.length ! letin) in
	   letin := (vvar, msval) :: ! letin;
	   M.VVar vvar
	 end else msval
   in
   let cons o (r, s, p, d) =      
      let con p = function
         | [] -> []
         | l  -> [(false, [p], set_val l)]
      in
      only := o;
      con "h:occurrence" r @ con "h:sort" s @ 
      con "h:position" p @ con "h:depth" d
   in
   let property_must n c =
      M.Property true M.RefineExact [n] []
	         (cons false c) [] [] false (M.Const "") 
   in   
   let property_only n cl =
      let cll = List.map (cons true) cl in
      M.Property false M.RefineExact [n] []
	         ! univ cll [] false (M.Proj None (M.AVar "obj"))
   in
   let rec aux = function 
      | [] -> ()
      | Universe l :: tail    -> 
         only := true; univ := [(false, ["h:position"], set_val l)]; aux tail 
      | MustObj r p d :: tail ->
         must := property_must "refObj" (r, [], p, d) :: ! must; aux tail  
      | MustSort s p d :: tail ->
	 must := property_must "refSort" ([], s, p, d) :: ! must; aux tail 
      | MustRel p d :: tail ->
	 must := property_must "refRel" ([], [], p, d) :: ! must; aux tail
      | OnlyObj r p d :: tail ->
	 onlyobj := (r, [], p, d) :: ! onlyobj; aux tail
      | OnlySort s p d :: tail ->
         onlysort := ([], s, p, d) :: ! onlysort; aux tail
      | OnlyRel p d :: tail ->
         onlyrel := ([], [], p, d) :: ! onlyrel; aux tail
   in
   let rec iter f g = function
      | []           -> raise (Failure "MQueryGenerator.iter")
      | [head]       -> (f head) 
      | head :: tail -> let t = (iter f g tail) in g (f head) t
   in
   text_of_spec prerr_string cl;
   aux cl;
   let must_query =
      if ! must = [] then  
         M.Property false M.RefineExact [] [] [] [] [] true (M.Const ".*")
      else 
         iter (fun x -> x) (fun x y -> M.Bin M.BinFMeet x y) ! must   
   in 
   let onlyobj_val = M.Not (M.Proj None (property_only "refObj" ! onlyobj)) in
   let onlysort_val = M.Not (M.Proj None (property_only "refSort" ! onlysort)) in
   let onlyrel_val = M.Not (M.Proj None (property_only "refRel" ! onlyrel)) in
   let select_query x =
      match ! onlyobj, ! onlysort, ! onlyrel with
         | [], [], [] -> x
	 | _, [], []  -> M.Select "obj" x onlyobj_val
	 | [], _, []  -> M.Select "obj" x onlysort_val
         | [], [], _  -> M.Select "obj" x onlyrel_val
         | _, _, []   -> M.Select "obj" x (M.Test M.And onlyobj_val onlysort_val)
         | _, [], _   -> M.Select "obj" x (M.Test M.And onlyobj_val onlyrel_val)
         | [], _, _   -> M.Select "obj" x (M.Test M.And onlysort_val onlyrel_val)
	 | _, _, _    -> M.Select "obj" x (M.Test M.And (M.Test M.And onlyobj_val onlysort_val) onlyrel_val)
   in	 
   let letin_query = 
      if ! letin = [] then fun x -> x
      else 
        let f (vvar, msval) x = M.LetVVar vvar msval x in 
        iter f (fun x y z -> x (y z)) ! letin
   in 
   M.StatQuery (letin_query (select_query must_query))

let builtin s = 
   let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
   match s with
      | MainHypothesis -> ns ^ "MainHypothesis"
      | InHypothesis   -> ns ^ "InHypothesis"
      | MainConclusion -> ns ^ "MainConclusion"
      | InConclusion   -> ns ^ "InConclusion"
      | InBody         -> ns ^ "InBody"
      | Set            ->      "Set"
      | Prop           ->      "Prop"
      | Type           ->      "Type"

(* conversion functions from the old constraints  ***************************)

type old_depth = int option
 
type r_obj = uri * position * old_depth 
type r_rel = position * old_depth
type r_sort = position * old_depth * sort 

type universe = position list option

type must_restrictions = r_obj list * r_rel list * r_sort list
type only_restrictions =
   r_obj list option * r_rel list option * r_sort list option

let query_of_constraints u (musts_obj, musts_rel, musts_sort)
                           (onlys_obj, onlys_rel, onlys_sort) =
   let conv = function
      | None   -> []
      | Some i -> [string_of_int i]
   in
   let must_obj (r, p, d) = MustObj ([r], [p], conv d) in
   let must_sort (p, d, s) = MustSort ([s], [p], conv d) in
   let must_rel (p, d) = MustRel ([p], conv d) in
   let only_obj (r, p, d) = OnlyObj ([r], [p], conv d) in
   let only_sort (p, d, s) = OnlySort ([s], [p], conv d) in
   let only_rel (p, d) = OnlyRel ([p], conv d) in
   let must = List.map must_obj musts_obj @
              List.map must_rel musts_rel @
	      List.map must_sort musts_sort
   in
   let only = 
      (match onlys_obj with 
         | None    -> []
         | Some [] -> [OnlyObj ([], [], [])]
	 | Some l  -> List.map only_obj l
      ) @
      (match onlys_rel with 
         | None    -> []
         | Some [] -> [OnlyRel ([], [])]
	 | Some l  -> List.map only_rel l
      ) @
      (match onlys_sort with 
         | None    -> []
         | Some [] -> [OnlySort ([], [], [])]
	 | Some l  -> List.map only_sort l
      )
   in
   let univ = match u with None -> [] | Some l -> [Universe l] in
   compose (must @ only @ univ)