(* 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 NotWellTyped of string;;
exception WrongUriToConstant of string;;
exception WrongUriToVariable of string;;
exception WrongUriToMutualInductiveDefinitions of string;;
exception ListTooShort;;
exception RelToHiddenHypothesis;;

type types = {synthesized : Cic.term ; expected : Cic.term};;

let rec split l n =
 match (l,n) with
    (l,0) -> ([], l)
  | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  | (_,_) -> raise ListTooShort
;;

let cooked_type_of_constant uri cookingsno =
 let module C = Cic in
 let module R = CicReduction in
 let module U = UriManager in
  let cobj =
   match CicEnvironment.is_type_checked uri cookingsno with
      CicEnvironment.CheckedObj cobj -> cobj
    | CicEnvironment.UncheckedObj uobj ->
       raise (NotWellTyped "Reference to an unchecked constant")
  in
   match cobj with
      C.Definition (_,_,ty,_) -> ty
    | C.Axiom (_,ty,_) -> ty
    | C.CurrentProof (_,_,_,ty) -> ty
    | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
;;

let type_of_variable uri =
 let module C = Cic in
 let module R = CicReduction in
 let module U = UriManager in
  (* 0 because a variable is never cooked => no partial cooking at one level *)
  match CicEnvironment.is_type_checked uri 0 with
     CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
   | CicEnvironment.UncheckedObj (C.Variable _) ->
      raise (NotWellTyped "Reference to an unchecked variable")
   |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
;;

let cooked_type_of_mutual_inductive_defs uri cookingsno i =
 let module C = Cic in
 let module R = CicReduction in
 let module U = UriManager in
  let cobj =
   match CicEnvironment.is_type_checked uri cookingsno with
      CicEnvironment.CheckedObj cobj -> cobj
    | CicEnvironment.UncheckedObj uobj ->
       raise (NotWellTyped "Reference to an unchecked inductive type")
  in
   match cobj with
      C.InductiveDefinition (dl,_,_) ->
       let (_,_,arity,_) = List.nth dl i in
        arity
    | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
;;

let cooked_type_of_mutual_inductive_constr uri cookingsno i j =
 let module C = Cic in
 let module R = CicReduction in
 let module U = UriManager in
  let cobj =
   match CicEnvironment.is_type_checked uri cookingsno with
      CicEnvironment.CheckedObj cobj -> cobj
    | CicEnvironment.UncheckedObj uobj ->
       raise (NotWellTyped "Reference to an unchecked constructor")
  in
   match cobj 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))
;;

module CicHash =
 Hashtbl.Make
  (struct
    type t = Cic.term
    let equal = (==)
    let hash = Hashtbl.hash
   end)
;;

(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
let rec type_of_aux' subterms_to_types metasenv context t =
 (* Coscoy's double type-inference algorithm             *)
 (* It computes the inner-types of every subterm of [t], *)
 (* even when they are not needed to compute the types   *)
 (* of other terms.                                      *)
 let rec type_of_aux context t =
  let module C = Cic in
  let module R = CicReduction in
  let module S = CicSubstitution in
  let module U = UriManager in
   let synthesized =
    match t with
       C.Rel n ->
        (try
          match List.nth context (n - 1) with
             Some (_,C.Decl t) -> S.lift n t
           | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
	   | None -> raise RelToHiddenHypothesis
         with
          _ -> raise (NotWellTyped "Not a close term")
        )
     | C.Var uri -> type_of_variable uri
     | C.Meta (n,l) -> 
        (* Let's visit all the subterms that will not be visited later *)
        let _ =
         List.iter
          (function None -> () | Some t -> ignore (type_of_aux context t)) l
        in
         let (_,canonical_context,ty) =
          List.find (function (m,_,_) -> n = m) metasenv
         in
          (* Checks suppressed *)
          CicSubstitution.lift_meta l ty
     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
     | C.Implicit -> raise (Impossible 21)
     | C.Cast (te,ty) ->
        (* Let's visit all the subterms that will not be visited later *)
        let _ = type_of_aux context te in
        let _ = type_of_aux context ty in
         (* Checks suppressed *)
         ty
     | C.Prod (name,s,t) ->
        let sort1 = type_of_aux context s
        and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
         sort_of_prod context (name,s) (sort1,sort2)
     | C.Lambda (n,s,t) ->
        (* Let's visit all the subterms that will not be visited later *)
        let _ = type_of_aux context s in
         let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
          (* Checks suppressed *)
          C.Prod (n,s,type2)
     | C.LetIn (n,s,t) ->
        (* Let's visit all the subterms that will not be visited later *)
        let _ = type_of_aux context s in
         (* Checks suppressed *)
         C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)
     | C.Appl (he::tl) when List.length tl > 0 ->
        let hetype = type_of_aux context he
        and tlbody_and_type =
         List.map (fun x -> (x, type_of_aux context x)) tl
        in
         eat_prods context hetype tlbody_and_type
     | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
     | C.Const (uri,cookingsno) ->
        cooked_type_of_constant uri cookingsno
     | C.Abst _ -> raise (Impossible 22)
     | C.MutInd (uri,cookingsno,i) ->
        cooked_type_of_mutual_inductive_defs uri cookingsno i
     | C.MutConstruct (uri,cookingsno,i,j) ->
        let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j in
         cty
     | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
        (* Let's visit all the subterms that will not be visited later *)
        let _ = List.map (type_of_aux context) pl in
         let outsort = type_of_aux context outtype in
         let (need_dummy, k) =
          let rec guess_args context t =
           match CicReduction.whd context t with
              C.Sort _ -> (true, 0)
            | C.Prod (name, s, t) ->
               let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
                if n = 0 then
                 (* last prod before sort *)
                 match CicReduction.whd context s with
                    (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
                    C.MutInd (uri',_,i') when U.eq uri' uri && i' = i ->
                     (false, 1)
                  | C.Appl ((C.MutInd (uri',_,i')) :: _)
                     when U.eq uri' uri && i' = i -> (false, 1)
                  | _ -> (true, 1)
                else
                 (b, n + 1)
            | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
          in
           (*CSC whd non serve dopo type_of_aux ? *)
           let (b, k) = guess_args context outsort in
            if not b then (b, k - 1) else (b, k)
         in
         let (_, arguments) =
           match R.whd context (type_of_aux context term) with
              (*CSC manca il caso dei CAST *)
              C.MutInd (uri',_,i') ->
               (* Checks suppressed *)
               [],[]
            | C.Appl (C.MutInd (uri',_,i') :: tl) ->
               split tl (List.length tl - k)
            | _ ->
              raise (NotWellTyped "MutCase: the term is not an inductive one")
         in
          (* Checks suppressed *)
          if not need_dummy then
           C.Appl ((outtype::arguments)@[term])
          else if arguments = [] then
           outtype
          else
           C.Appl (outtype::arguments)
     | C.Fix (i,fl) ->
        (* Let's visit all the subterms that will not be visited later *)
        let context' =
         List.rev
          (List.map
            (fun (n,_,ty,_) ->
              let _ = type_of_aux context ty in
               (Some (C.Name n,(C.Decl ty)))
            ) fl
          ) @
          context
        in
         let _ =
          List.iter
           (fun (_,_,_,bo) -> ignore (type_of_aux context' bo))
         in
          (* Checks suppressed *)
          let (_,_,ty,_) = List.nth fl i in
           ty
     | C.CoFix (i,fl) ->
        (* Let's visit all the subterms that will not be visited later *)
        let context' =
         List.rev
          (List.map
            (fun (n,ty,_) ->
              let _ = type_of_aux context ty in
               (Some (C.Name n,(C.Decl ty)))
            ) fl
          ) @
          context
        in
         let _ =
          List.iter
           (fun (_,_,bo) -> ignore (type_of_aux context' bo))
         in
          (* Checks suppressed *)
          let (_,ty,_) = List.nth fl i in
           ty
   in
    (*CSC: Is whd the right thing to do? Or should full beta *)
    (*CSC: reduction be more appropriate?                    *)
(*CSC: Nota: whd fa troppo (esempio: fa anche iota) e full beta sembra molto *)
(*CSC: costosa quando fatta ogni passo. Fare solo un passo? *)
    let synthesized' = CicReduction.whd context synthesized in
     CicHash.add subterms_to_types t
      {synthesized = synthesized' ; expected = Cic.Implicit} ;
     synthesized'

 and sort_of_prod context (name,s) (t1, t2) =
  let module C = Cic 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
    | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
    | (_,_) ->
      raise
       (NotWellTyped
        ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))

 and eat_prods context hetype =
  (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
  (*CSC: cucinati                                                         *)
  function
     [] -> hetype
   | (hete, hety)::tl ->
    (match (CicReduction.whd context hetype) with
        Cic.Prod (n,s,t) ->
         (* Checks suppressed *)
         eat_prods context (CicSubstitution.subst hete t) tl
      | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
    )

 in
  type_of_aux context t
;;

let double_type_of metasenv context t =
 let subterms_to_types = CicHash.create 503 in
  ignore (type_of_aux' subterms_to_types metasenv context t) ;
  subterms_to_types
;;