(* 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 Impossible of int;;
exception NotRefinable of string;;
exception Uncertain of string;;
exception WrongUriToConstant of string;;
exception WrongUriToVariable of string;;
exception WrongUriToMutualInductiveDefinitions of string;;
exception RelToHiddenHypothesis;;
exception MetasenvInconsistency;;
exception MutCaseFixAndCofixRefineNotImplemented;;
exception FreeMetaFound of int;;

let fdebug = ref 0;;
let debug t context =
 let rec debug_aux t i =
  let module C = Cic in
  let module U = UriManager in
   CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
 in
  if !fdebug = 0 then
   raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
   (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
;;

let rec type_of_constant uri =
 let module C = Cic in
 let module R = CicReduction in
 let module U = UriManager in
  match CicEnvironment.get_cooked_obj uri with
     C.Constant (_,_,ty,_) -> ty
   | C.CurrentProof (_,_,_,ty,_) -> ty
   | _ -> raise (WrongUriToConstant (U.string_of_uri uri))

and type_of_variable uri =
 let module C = Cic in
 let module R = CicReduction in
 let module U = UriManager in
  match CicEnvironment.get_cooked_obj uri with
     C.Variable (_,_,ty,_) -> ty
   |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))

and type_of_mutual_inductive_defs uri i =
 let module C = Cic in
 let module R = CicReduction in
 let module U = UriManager in
  match CicEnvironment.get_cooked_obj uri with
     C.InductiveDefinition (dl,_,_) ->
      let (_,_,arity,_) = List.nth dl i in
       arity
   | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))

and type_of_mutual_inductive_constr uri i j =
 let module C = Cic in
 let module R = CicReduction in
 let module U = UriManager in
  match CicEnvironment.get_cooked_obj uri with
      C.InductiveDefinition (dl,_,_) ->
       let (_,_,_,cl) = List.nth dl i in
        let (_,ty) = List.nth cl (j-1) in
         ty
   | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))

(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
and type_of_aux' metasenv context t =
 let rec type_of_aux subst metasenv context =
  let module C = Cic in
  let module S = CicSubstitution in
  let module U = UriManager in
  let module Un = CicUnification in
   function
      C.Rel n ->
       (try
         match List.nth context (n - 1) with
            Some (_,C.Decl t) -> S.lift n t,subst,metasenv
          | Some (_,C.Def bo) ->
             type_of_aux subst metasenv context (S.lift n bo)
	  | None -> raise RelToHiddenHypothesis
        with
         _ -> raise (NotRefinable "Not a close term")
       )
    | C.Var (uri,exp_named_subst) ->
      incr fdebug ;
      let subst',metasenv' =
       check_exp_named_subst subst metasenv context exp_named_subst in
      let ty =
       CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
      in
       decr fdebug ;
       ty,subst',metasenv'
    | C.Meta (n,l) -> 
       let (_,canonical_context,ty) =
        try
         List.find (function (m,_,_) -> n = m) metasenv
        with
         Not_found -> raise (FreeMetaFound n)
       in
        let subst',metasenv' =
         check_metasenv_consistency subst metasenv context canonical_context l
        in
         CicSubstitution.lift_meta l ty, subst', metasenv'
    | C.Sort s ->
       C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
        subst,metasenv
    | C.Implicit -> raise (Impossible 21)
    | C.Cast (te,ty) ->
       let _,subst',metasenv' =
        type_of_aux subst metasenv context ty in
       let inferredty,subst'',metasenv'' =
        type_of_aux subst' metasenv' context ty
       in
        (try
          let subst''',metasenv''' =
           Un.fo_unif_subst subst'' context metasenv'' inferredty ty
          in
           ty,subst''',metasenv'''
         with
          _ -> raise (NotRefinable "Cast"))
    | C.Prod (name,s,t) ->
       let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
       let sort2,subst'',metasenv'' =
        type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
       in
        sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
   | C.Lambda (n,s,t) ->
       let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
       let type2,subst'',metasenv'' =
        type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
       in
        let sort2,subst''',metasenv''' =
         type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
        in
         (* only to check if the product is well-typed *)
         let _,subst'''',metasenv'''' =
          sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
         in
          C.Prod (n,s,type2),subst'''',metasenv''''
   | C.LetIn (n,s,t) ->
      (* only to check if s is well-typed *)
      let _,subst',metasenv' = type_of_aux subst metasenv context s in
      let inferredty,subst'',metasenv'' =
       type_of_aux subst' metasenv' ((Some (n,(C.Def s)))::context) t
      in
       (* One-step LetIn reduction. Even faster than the previous solution.
          Moreover the inferred type is closer to the expected one. *)
       CicSubstitution.subst s inferredty,subst',metasenv'
   | C.Appl (he::tl) when List.length tl > 0 ->
      let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
      let tlbody_and_type,subst'',metasenv'' =
       List.fold_right
        (fun x (res,subst,metasenv) ->
          let ty,subst',metasenv' =
           type_of_aux subst metasenv context x
          in
           (x, ty)::res,subst',metasenv'
        ) tl ([],subst',metasenv')
      in
       eat_prods subst'' metasenv'' context hetype tlbody_and_type
   | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
   | C.Const (uri,exp_named_subst) ->
      incr fdebug ;
      let subst',metasenv' =
       check_exp_named_subst subst metasenv context exp_named_subst in
      let cty =
       CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
      in
       decr fdebug ;
       cty,subst',metasenv'
   | C.MutInd (uri,i,exp_named_subst) ->
      incr fdebug ;
      let subst',metasenv' =
       check_exp_named_subst subst metasenv context exp_named_subst in
      let cty =
       CicSubstitution.subst_vars exp_named_subst
        (type_of_mutual_inductive_defs uri i)
      in
       decr fdebug ;
       cty,subst',metasenv'
   | C.MutConstruct (uri,i,j,exp_named_subst) ->
      let subst',metasenv' =
       check_exp_named_subst subst metasenv context exp_named_subst in
      let cty =
       CicSubstitution.subst_vars exp_named_subst
        (type_of_mutual_inductive_constr uri i j)
      in
       cty,subst',metasenv'
   | C.MutCase _
   | C.Fix _
   | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented

 (* check_metasenv_consistency checks that the "canonical" context of a
 metavariable is consitent - up to relocation via the relocation list l -
 with the actual context *)
 and check_metasenv_consistency subst metasenv context canonical_context l =
   let module C = Cic in
   let module R = CicReduction in
   let module S = CicSubstitution in
    let lifted_canonical_context = 
     let rec aux i =
      function
         [] -> []
       | (Some (n,C.Decl t))::tl ->
          (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
       | (Some (n,C.Def t))::tl ->
          (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
       | None::tl -> None::(aux (i+1) tl)
     in
      aux 1 canonical_context
    in
     List.fold_left2 
      (fun (subst,metasenv) t ct -> 
        match (t,ct) with
           _,None -> subst,metasenv
         | Some t,Some (_,C.Def ct) ->
            (try
              CicUnification.fo_unif_subst subst context metasenv t ct
             with _ -> raise MetasenvInconsistency)
         | Some t,Some (_,C.Decl ct) ->
            let inferredty,subst',metasenv' =
             type_of_aux subst metasenv context t
            in
             (try
               CicUnification.fo_unif_subst subst context metasenv inferredty ct
             with _ -> raise MetasenvInconsistency)
         | _, _  -> raise MetasenvInconsistency
      ) (subst,metasenv) l lifted_canonical_context 

 and check_exp_named_subst metasubst metasenv context =
  let rec check_exp_named_subst_aux metasubst metasenv substs =
   function
      [] -> metasubst,metasenv
    | ((uri,t) as subst)::tl ->
       let typeofvar =
        CicSubstitution.subst_vars substs (type_of_variable uri) in
       (match CicEnvironment.get_cooked_obj ~trust:false uri with
           Cic.Variable (_,Some bo,_,_) ->
            raise
             (NotRefinable
               "A variable with a body can not be explicit substituted")
         | Cic.Variable (_,None,_,_) -> ()
         | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
       ) ;
       let typeoft,metasubst',metasenv' =
        type_of_aux metasubst metasenv context t
       in
        try
         let metasubst'',metasenv'' =
          CicUnification.fo_unif_subst
           metasubst' context metasenv' typeoft typeofvar
         in
          check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
        with _ ->
         raise (NotRefinable "Wrong Explicit Named Substitution")
  in
   check_exp_named_subst_aux metasubst metasenv []

 and sort_of_prod subst metasenv context (name,s) (t1, t2) =
  let module C = Cic in
   (* ti could be a metavariable in the domain of the substitution *)
   let subst',metasenv' = CicUnification.unwind_subst metasenv subst in
   let t1' = CicUnification.apply_subst subst' t1 in
   let t2' = CicUnification.apply_subst subst' t2 in
    let t1'' = CicReduction.whd context t1' in
    let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in
    match (t1'', t2'') with
       (C.Sort s1, C.Sort s2)
         when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
          C.Sort s2,subst',metasenv'
     | (C.Sort s1, C.Sort s2) ->
         (*CSC manca la gestione degli universi!!! *)
         C.Sort C.Type,subst',metasenv'
     | (C.Meta _,_)
     | (_,C.Meta _) ->
       raise
        (Uncertain
          ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^
           CicPp.ppterm t2''))
     | (_,_) ->
       raise
        (NotRefinable
         ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2''))

 and eat_prods subst metasenv context hetype =
  function
     [] -> hetype,subst,metasenv
   | (hete, hety)::tl ->
    (match (CicReduction.whd context hetype) with
        Cic.Prod (n,s,t) ->
         let subst',metasenv' =
          try
           CicUnification.fo_unif_subst subst context metasenv s hety
          with _ ->
           raise (NotRefinable "Appl: wrong parameter-type")
         in
          CicReduction.fdebug := -1 ;
          eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
      | Cic.Meta _ as t ->
         raise
          (Uncertain
            ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
      | _ -> raise (NotRefinable "Appl: wrong Prod-type")
    )
 in
  let ty,subst',metasenv' =
   type_of_aux [] metasenv context t
  in
   let subst'',metasenv'' = CicUnification.unwind_subst metasenv' subst' in
   (* we get rid of the metavariables that have been instantiated *)
   let metasenv''' =
    List.filter
     (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst''))
     metasenv''
   in
    CicUnification.apply_subst subst'' t,
     CicUnification.apply_subst subst'' ty,
     subst'', metasenv'''
;;

(* DEBUGGING ONLY *)
let type_of_aux' metasenv context term =
 try
  let (t,ty,s,m) =
   type_of_aux' metasenv context term
  in
   List.iter
    (function (i,t) ->
      prerr_endline ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
   List.iter
    (function (i,_,t) ->
      prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
   prerr_endline
    ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
   (t,ty,s,m)
 with
  e ->
   List.iter
    (function (i,_,t) ->
      prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
    metasenv ;
   prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
   raise e
;;