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

exception WrongUriToConstant;;
exception WrongUriToInductiveDefinition;;
exception CircularDependency of string;;

module OrderedUris =
 struct
  type t = UriManager.uri
  let compare (s1 : t) (s2 : t) =
   (* library function for = *)
   compare s1 s2
   (*if s1 = s2 then 0 else if s1 < s2 then (-1) else 1*)
 end
;;

let filename_of_uri uri =
 let uri' = UriManager.string_of_uri uri in
  let fn = Str.replace_first (Str.regexp "cic:") Configuration.helm_dir uri' in
   fn ^ ".xml"
;;

(* quite inefficient coding of a set of strings: the only operations  *)
(* performed are mem O(log n), and union O(n * log n?)                *)
(* Perhaps a better implementation would be an array of bits or a map *)
(* from uri to booleans                                               *)
module SetOfUris = Set.Make(OrderedUris);;

let (@@) = SetOfUris.union;;

let rec parameters_of te ty pparams=
 let module S = SetOfUris in
 let module C = Cic in
   let rec aux =
    function
       C.Rel _ -> S.empty
     | C.Var uri -> S.singleton uri
     | C.Meta _ -> S.empty
     | C.Sort _ -> S.empty
     | C.Implicit -> S.empty
     | C.Cast (te, ty) -> aux te @@ aux ty
     | C.Prod (_, s, t) -> aux s @@ aux t
     | C.Lambda (_, s, t) -> aux s @@ aux t
     | C.Appl l -> List.fold_right (fun x i -> aux x @@ i) l S.empty
     | C.Const (uri,_) ->
        (* the parameters could be not exact but only possible *)
        fix_params uri (Some (filename_of_uri uri)) ;
        (* now the parameters are surely possible *)
        (match CicCache.get_obj uri with
            C.Definition (_, _, _, params) ->
              List.fold_right
               (fun (_,l) i ->
                 List.fold_right
                  (fun x i -> S.singleton x @@ i) l i
               ) params S.empty
          | C.Axiom (_, _, params) ->
             List.fold_right
              (fun (_,l) i ->
                List.fold_right
                 (fun x i -> S.singleton x @@ i) l i
              ) params S.empty
          | C.CurrentProof _ -> S.empty (*CSC wrong *)
          | _ -> raise WrongUriToConstant
        )
     | C.Abst _ -> S.empty
     | C.MutInd (uri,_,_) ->
        (match CicCache.get_obj uri with
            C.InductiveDefinition (_, params, _) ->
             List.fold_right
              (fun (_,l) i ->
                List.fold_right
                 (fun x i -> S.singleton x @@ i) l i
              ) params S.empty
          | _ -> raise WrongUriToInductiveDefinition
        )
     | C.MutConstruct (uri,_,_,_) ->
        (match CicCache.get_obj uri with
            C.InductiveDefinition (_, params, _) ->
             List.fold_right
              (fun (_,l) i ->
                List.fold_right
                 (fun x i -> S.singleton x @@ i) l i
              ) params S.empty
          | _ -> raise WrongUriToInductiveDefinition
        )
     | C.MutCase (uri,_,_,outtype,term,patterns) ->
        (*CSC cosa basta? Ci vuole anche uri? *)
        (match CicCache.get_obj uri with
            C.InductiveDefinition (_, params, _) ->
            List.fold_right
             (fun (_,l) i ->
               List.fold_right
                (fun x i -> S.singleton x @@ i) l i
             ) params S.empty
          | _ -> raise WrongUriToInductiveDefinition
        ) @@ aux outtype @@ aux term @@
         List.fold_right (fun x i -> aux x @@ i) patterns S.empty
     | C.Fix (_,fl) ->
        List.fold_right
         (fun (_,_,ty,bo) i  -> aux ty @@ aux bo @@ i)
         fl S.empty
     | C.CoFix (_,fl) ->
        List.fold_right
         (fun (_,ty,bo) i -> aux ty @@ aux bo @@ i)
         fl S.empty
 in
  let actual_params = aux te @@ aux ty in
   (* sort_actual_params wants in input the ordered list of possible params *)
   let rec sort_actual_params2 =
    function
       [] -> []
     | he::tl when S.mem he actual_params -> he::(sort_actual_params2 tl)
     | _::tl -> sort_actual_params2 tl
   in
    let rec sort_actual_params =
     function
        [] -> []
      | (n,l)::tl -> (n, sort_actual_params2 l)::(sort_actual_params tl)
    in
     sort_actual_params pparams

and fix_params uri filename =
 let module C = Cic in
  let ann = CicCache.get_annobj uri in
   match ann with
      C.ADefinition (xid, ann, id, te, ty, C.Possible pparams) ->
       let te' = Deannotate.deannotate_term te in
       let ty' = Deannotate.deannotate_term ty in
        let real_params = parameters_of te' ty' pparams in
         let fixed =
          C.ADefinition (xid,ann,id,te,ty,C.Actual real_params)
         in
          Xml.pp (Cic2Xml.pp fixed uri) filename ;
    | _ -> ()
;;