(* 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                                 *)
(*                                                                            *)
(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
(*                                 02/12/2002                                 *)
(*                                                                            *)
(*                            Missing description                             *)
(*                                                                            *)
(******************************************************************************)

type classification =
   Backbone of int
 | Branch of int
 | InConclusion
 | InHypothesis
;;

let soften_classification =
 function
    Backbone _ -> InConclusion
  | Branch _ -> InHypothesis
  | k -> k
;;

let (!!) =
 function
    Backbone n ->
     "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion", Some n
  | Branch n ->
     "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis", Some n
  | InConclusion ->
     "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion", None
  | InHypothesis ->
     "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis", None
;;

let (@@) (l1,l2,l3) (l1',l2',l3') =
 let merge l1 l2 =
  List.fold_left (fun i t -> if List.mem t l2 then i else t::i) l2 l1
 in
  merge l1 l1', merge l2 l2', merge l3 l3'
;;

let get_constraints term =
 let module U = UriManager in
 let module C = Cic in
  let rec process_type_aux kind =
   function
      C.Var (uri,expl_named_subst) ->
       let kind',depth = !!kind in
        ([UriManager.string_of_uri uri,kind',depth],[],[]) @@
          (process_type_aux_expl_named_subst kind expl_named_subst)
    | C.Rel _ ->
       let kind',depth = !!kind in
        (match depth with
            None -> [],[],[]
          | Some d -> [],[kind',Some d],[])
    | C.Sort s ->
       (match kind with
           Backbone _
         | Branch _ ->
            let s' =
             match s with
                Cic.Prop ->
                 "http://www.cs.unibo.it/helm/schemas/schema-helm#Prop"
              | Cic.Set ->
                 "http://www.cs.unibo.it/helm/schemas/schema-helm#Set"
              | Cic.Type ->
                 "http://www.cs.unibo.it/helm/schemas/schema-helm#Type"
            in
             let kind',depth = !!kind in
              (match depth with
                  None -> assert false
                | Some d -> [],[],[kind',Some d,s'])
         | _ -> [],[],[])
    | C.Meta _
    | C.Implicit -> assert false
    | C.Cast (te,_) ->
       (* type ignored *)
       process_type_aux kind te
    | C.Prod (_,sou,ta) ->
       let (source_kind,target_kind) =
        match kind with
           Backbone n -> (Branch 0, Backbone (n+1))
         | Branch n -> (InHypothesis, Branch (n+1))
         | k -> (k,k)
       in
        process_type_aux source_kind sou @@
        process_type_aux target_kind ta
    | C.Lambda (_,sou,ta) ->
        let kind' = soften_classification kind in
         process_type_aux kind' sou @@
         process_type_aux kind' ta
    | C.LetIn (_,te,ta)->
       let kind' = soften_classification kind in
        process_type_aux kind' te @@
        process_type_aux kind ta
    | C.Appl (he::tl) ->
       let kind' = soften_classification kind in
        process_type_aux kind he @@
        List.fold_left (fun i t -> i @@ process_type_aux kind' t) ([],[],[]) tl
    | C.Appl _ -> assert false
    | C.Const (uri,_) ->
       let kind',depth = !!kind in
        [UriManager.string_of_uri uri,kind',depth],[],[]
    | C.MutInd (uri,typeno,expl_named_subst) ->
       let kind',depth = !!kind in
       ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^
          ")", kind', depth],[],[]) @@
         (process_type_aux_expl_named_subst kind expl_named_subst)
    | C.MutConstruct (uri,typeno,consno,expl_named_subst) ->
       let kind',depth = !!kind in
        ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^
          "/" ^ string_of_int consno ^ ")",kind',depth],[],[]) @@
          (process_type_aux_expl_named_subst kind expl_named_subst)
    | C.MutCase (_,_,_,term,patterns) ->
       (* outtype ignored *)
       let kind' = soften_classification kind in
        process_type_aux kind' term @@
        List.fold_left (fun i t -> i @@ process_type_aux kind' t)
         ([],[],[]) patterns
    | C.Fix (_,funs) ->
       let kind' = soften_classification kind in
        List.fold_left
         (fun i (_,_,bo,ty) ->
           i @@
            process_type_aux kind' bo @@
            process_type_aux kind' ty
         ) ([],[],[]) funs
    | C.CoFix (_,funs) ->
       let kind' = soften_classification kind in
        List.fold_left
         (fun i (_,bo,ty) ->
           i @@
            process_type_aux kind' bo @@
            process_type_aux kind' ty
         ) ([],[],[]) funs
 and process_type_aux_expl_named_subst kind =
  List.fold_left
   (fun i (_,t) -> i @@ (process_type_aux (soften_classification kind) t))
   ([],[],[])
in
 let obj_constraints,rel_constraints,sort_constraints =
  process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term)
 in
  (obj_constraints,rel_constraints,sort_constraints)
;;

(*CSC: Debugging only *)
let get_constraints term =
 let res = get_constraints term in
 let (objs,rels,sorts) = res in
  prerr_endline "Constraints on objs:" ;
  List.iter
   (function (s1,s2,n) ->
     prerr_endline
      (s1 ^ " " ^ s2 ^ " " ^
        match n with None -> "NULL" | Some n -> string_of_int n)
   ) objs ;
  prerr_endline "Constraints on Rels:" ;
  List.iter
   (function (s,n) ->
     prerr_endline
      (s ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL"))
   ) rels ;
  prerr_endline "Constraints on Sorts:" ;
  List.iter
   (function (s1,n,s2) ->
     prerr_endline
      (s1 ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL") ^
        " " ^ s2)
   ) sorts ;
  res
;;