(* Copyright (C) 2004, 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/.
 *)

let debug_print = fun _ -> ()

let rec higher_name arity =
  function 
      Cic.Sort Cic.Prop
    | Cic.Sort Cic.CProp -> 
	if arity = 0 then "A" (* propositions *)
	else if arity = 1 then "P" (* predicates *)
	else "R" (*relations *)
    | Cic.Sort Cic.Set
	-> if arity = 0 then "S" else "F"
    | Cic.Sort (Cic.Type _ ) -> 
	if arity = 0 then "T" else "F"
    | Cic.Prod (_,_,t) -> higher_name (arity+1) t
    | _ -> "f"

let get_initial s = 
   if String.length s = 0 then "_"
   else 
     let head = String.sub s 0 1 in
     String.lowercase head

(* only used when the sort is not Prop or CProp *)
let rec guess_a_name context ty =
  match ty with
    Cic.Rel n ->  
      (match List.nth context (n-1) with
	None -> assert false
      | Some (Cic.Anonymous,_) -> assert false
      | Some (Cic.Name s,_) -> get_initial s)
  | Cic.Var (uri,_) -> get_initial (UriManager.name_of_uri uri)
  | Cic.Sort _ -> higher_name 0 ty
  | Cic.Implicit _ -> assert false
  | Cic.Cast (t1,t2) -> guess_a_name context t1
  | Cic.Prod (na_,_,t) -> higher_name 1 t
  | Cic.Lambda _ -> assert false                   
  | Cic.LetIn (_,s,t) -> guess_a_name context (CicSubstitution.subst s t)
  | Cic.Appl [] -> assert false
  | Cic.Appl (he::_) -> guess_a_name context he 
  | Cic.Const (uri,_)
  | Cic.MutInd (uri,_,_)
  | Cic.MutConstruct (uri,_,_,_) -> get_initial (UriManager.name_of_uri uri)  
  | _ -> "x"

(* mk_fresh_name context name typ                      *)
(* returns an identifier which is fresh in the context *)
(* and that resembles [name] as much as possible.      *)
(* [typ] will be the type of the variable              *)
let mk_fresh_name ~subst metasenv context name ~typ =
 let module C = Cic in
  let basename =
   match name with
      C.Anonymous ->
       (try
        let ty,_ = 
          CicTypeChecker.type_of_aux' ~subst metasenv context typ 
            CicUniv.empty_ugraph in 
         (match ty with
             C.Sort C.Prop
           | C.Sort C.CProp -> "H"
           | _ -> guess_a_name context typ
         )
        with CicTypeChecker.TypeCheckerFailure _ -> "H"
       )
    | C.Name name ->
       Str.global_replace (Str.regexp "[0-9]*$") "" name
  in
   let already_used name =
    List.exists (function Some (n,_) -> n=name | _ -> false) context
   in
    if name <> C.Anonymous && not (already_used name) then
     name
    else if not (already_used (C.Name basename)) then
     C.Name basename
    else
     let rec try_next n =
      let name' = C.Name (basename ^ string_of_int n) in
       if already_used name' then
        try_next (n+1)
       else
        name'
     in
      try_next 1
;;

(* let mk_fresh_names ~subst metasenv context t *)
let rec mk_fresh_names ~subst metasenv context t =
  match t with
    Cic.Rel _ -> t
  | Cic.Var (uri,exp_named_subst) ->
      let ens = 
	List.map 
	  (fun (uri,t) ->
	    (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
      Cic.Var (uri,ens)
  | Cic.Meta (i,l) ->
       let l' = 
        List.map 
         (fun t ->
           match t with
             None -> None
           | Some t -> Some (mk_fresh_names ~subst metasenv context t)) l in
       Cic.Meta(i,l')
    | Cic.Sort _ 
    | Cic.Implicit _ -> t
    | Cic.Cast (te,ty) ->
       let te' = mk_fresh_names ~subst metasenv context te in
       let ty' = mk_fresh_names ~subst metasenv context ty in
       Cic.Cast (te', ty')
    | Cic.Prod (n,s,t) ->
	let s' = mk_fresh_names ~subst metasenv context s in
	let n' =
	  match n with
	    Cic.Anonymous -> Cic.Anonymous
	  | Cic.Name "matita_dummy" -> 
	      mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s'
	  | _ -> n in 
	let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in
	Cic.Prod (n',s',t')
    | Cic.Lambda (n,s,t) ->
	let s' = mk_fresh_names ~subst metasenv context s in
	let n' =
	  match n with
	    Cic.Anonymous -> Cic.Anonymous
	  | Cic.Name "matita_dummy" -> 
	      mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s' 
	  | _ -> n in 
	let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Decl s')::context) t in
	Cic.Lambda (n',s',t')
    | Cic.LetIn (n,s,t) ->
	let s' = mk_fresh_names ~subst metasenv context s in
	let n' =
	  match n with
	    Cic.Anonymous -> Cic.Anonymous
	  | Cic.Name "matita_dummy" -> 
	      mk_fresh_name ~subst metasenv context Cic.Anonymous ~typ:s' 
	  | _ -> n in 
	let t' = mk_fresh_names ~subst metasenv (Some(n',Cic.Def (s',None))::context) t in
	Cic.LetIn (n',s',t')	
    | Cic.Appl l ->
	Cic.Appl (List.map (mk_fresh_names ~subst metasenv context) l)
    | Cic.Const (uri,exp_named_subst) ->
        let ens = 
	  List.map 
	    (fun (uri,t) ->
	      (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
	Cic.Const(uri,ens)
    | Cic.MutInd (uri,tyno,exp_named_subst) ->
	let ens = 
	  List.map 
	    (fun (uri,t) ->
	      (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
        Cic.MutInd (uri,tyno,ens)
    | Cic.MutConstruct (uri,tyno,consno,exp_named_subst) ->
        let ens = 
	  List.map 
	    (fun (uri,t) ->
	      (uri,mk_fresh_names ~subst metasenv context t)) exp_named_subst in
        Cic.MutConstruct (uri,tyno,consno, ens)
    | Cic.MutCase (sp,i,outty,t,pl) ->
       let outty' = mk_fresh_names ~subst metasenv context outty in
       let t' = mk_fresh_names ~subst metasenv context t in
       let pl' = List.map (mk_fresh_names ~subst metasenv context) pl in
       Cic.MutCase (sp, i, outty', t', pl')
    | Cic.Fix (i, fl) -> 
        let tys = List.map 
	    (fun (n,_,ty,_) -> 
	      Some (Cic.Name n,(Cic.Decl ty))) fl in
	let fl' = List.map 
	    (fun (n,i,ty,bo) -> 
	      let ty' = mk_fresh_names ~subst metasenv context ty in
	      let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
	      (n,i,ty',bo')) fl in
	Cic.Fix (i, fl') 
    | Cic.CoFix (i, fl) ->
	let tys = List.map 
	    (fun (n,_,ty) -> 
	      Some (Cic.Name n,(Cic.Decl ty))) fl in
	let fl' = List.map 
	    (fun (n,ty,bo) -> 
	      let ty' = mk_fresh_names ~subst metasenv context ty in
	      let bo' = mk_fresh_names ~subst metasenv (tys@context) bo in
	      (n,ty',bo')) fl in
	Cic.CoFix (i, fl') 	
;;

(* clean_dummy_dependent_types term                             *)
(* returns a copy of [term] where every dummy dependent product *)
(* have been replaced with a non-dependent product and where    *)
(* dummy let-ins have been removed.                             *)
let clean_dummy_dependent_types t =
 let module C = Cic in
  let rec aux k =
   function
      C.Rel m as t -> t,[k - m]
    | C.Var (uri,exp_named_subst) ->
       let exp_named_subst',rels = 
        List.fold_right
         (fun (uri,t) (exp_named_subst,rels) ->
           let t',rels' = aux k t in
            (uri,t')::exp_named_subst, rels' @ rels
         ) exp_named_subst ([],[])
       in
        C.Var (uri,exp_named_subst'),rels
    | C.Meta (i,l) ->
       let l',rels =
        List.fold_right
         (fun t (l,rels) ->
           let t',rels' =
            match t with
               None -> None,[]
             | Some t ->
                let t',rels' = aux k t in
                 Some t', rels'
           in
            t'::l, rels' @ rels
         ) l ([],[])
       in
        C.Meta(i,l'),rels
    | C.Sort _ as t -> t,[]
    | C.Implicit _ as t -> t,[]
    | C.Cast (te,ty) ->
       let te',rels1 = aux k te in
       let ty',rels2 = aux k ty in
        C.Cast (te', ty'), rels1@rels2
    | C.Prod (n,s,t) ->
       let s',rels1 = aux k s in
       let t',rels2 = aux (k+1) t in
        let n' =
         match n with
            C.Anonymous ->
             if List.mem k rels2 then
(
              debug_print "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name" ;
              C.Anonymous
)
             else
              C.Anonymous
          | C.Name _ as n ->
             if List.mem k rels2 then n else C.Anonymous
        in
         C.Prod (n', s', t'), rels1@rels2
    | C.Lambda (n,s,t) ->
       let s',rels1 = aux k s in
       let t',rels2 = aux (k+1) t in
        C.Lambda (n, s', t'), rels1@rels2
    | C.LetIn (n,s,t) ->
       let s',rels1 = aux k s in
       let t',rels2 = aux (k+1) t in
       let rels = rels1 @ rels2 in
        if List.mem k rels2 then
         C.LetIn (n, s', t'), rels
        else
         (* (C.Rel 1) is just a dummy term; any term would fit *)
         CicSubstitution.subst (C.Rel 1) t', rels
    | C.Appl l ->
       let l',rels =
        List.fold_right
         (fun t (exp_named_subst,rels) ->
           let t',rels' = aux k t in
            t'::exp_named_subst, rels' @ rels
         ) l ([],[])
       in
        C.Appl l', rels
    | C.Const (uri,exp_named_subst) ->
       let exp_named_subst',rels = 
        List.fold_right
         (fun (uri,t) (exp_named_subst,rels) ->
           let t',rels' = aux k t in
            (uri,t')::exp_named_subst, rels' @ rels
         ) exp_named_subst ([],[])
       in
        C.Const (uri,exp_named_subst'),rels
    | C.MutInd (uri,tyno,exp_named_subst) ->
       let exp_named_subst',rels = 
        List.fold_right
         (fun (uri,t) (exp_named_subst,rels) ->
           let t',rels' = aux k t in
            (uri,t')::exp_named_subst, rels' @ rels
         ) exp_named_subst ([],[])
       in
        C.MutInd (uri,tyno,exp_named_subst'),rels
    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
       let exp_named_subst',rels = 
        List.fold_right
         (fun (uri,t) (exp_named_subst,rels) ->
           let t',rels' = aux k t in
            (uri,t')::exp_named_subst, rels' @ rels
         ) exp_named_subst ([],[])
       in
        C.MutConstruct (uri,tyno,consno,exp_named_subst'),rels
    | C.MutCase (sp,i,outty,t,pl) ->
       let outty',rels1 = aux k outty in
       let t',rels2 = aux k t in
       let pl',rels3 =
        List.fold_right
         (fun t (exp_named_subst,rels) ->
           let t',rels' = aux k t in
            t'::exp_named_subst, rels' @ rels
         ) pl ([],[])
       in
        C.MutCase (sp, i, outty', t', pl'), rels1 @ rels2 @rels3
    | C.Fix (i, fl) ->
       let len = List.length fl in
       let fl',rels =
        List.fold_right
         (fun (name,i,ty,bo) (fl,rels) ->
           let ty',rels1 = aux k ty in
           let bo',rels2 = aux (k + len) bo in
            (name,i,ty',bo')::fl, rels1 @ rels2 @ rels
         ) fl ([],[])
       in
        C.Fix (i, fl'),rels
    | C.CoFix (i, fl) ->
       let len = List.length fl in
       let fl',rels =
        List.fold_right
         (fun (name,ty,bo) (fl,rels) ->
           let ty',rels1 = aux k ty in
           let bo',rels2 = aux (k + len) bo in
            (name,ty',bo')::fl, rels1 @ rels2 @ rels
         ) fl ([],[])
       in
        C.CoFix (i, fl'),rels
  in
   fst (aux 0 t)
;;