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

let hashtbl_add_time = ref 0.0;;

let xxx_add h k v =
 let t1 = Sys.time () in
  Hashtbl.add h k v ;
  let t2 = Sys.time () in
   hashtbl_add_time := !hashtbl_add_time +. t2 -. t1
;;

let number_new_type_of_aux' = ref 0;;
let type_of_aux'_add_time = ref 0.0;;

let xxx_type_of_aux' m c t =
 let t1 = Sys.time () in
 let res = CicTypeChecker.type_of_aux' m c t in
 let t2 = Sys.time () in
 type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
 res
;;

type anntypes =
 {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
;;

let gen_id seed =
 let res = "i" ^ string_of_int !seed in
  incr seed ;
  res
;;

let fresh_id seed ids_to_terms ids_to_father_ids =
 fun father t ->
  let res = gen_id seed in
   xxx_add ids_to_father_ids res father ;
   xxx_add ids_to_terms res t ;
   res
;;

let source_id_of_id id = "#source#" ^ id;;

exception NotEnoughElements;;
exception NameExpected;;

(*CSC: cut&paste da cicPp.ml *)
(* get_nth l n   returns the nth element of the list l if it exists or *)
(* raises NotEnoughElements if l has less than n elements             *)
let rec get_nth l n =
 match (n,l) with
    (1, he::_) -> he
  | (n, he::tail) when n > 1 -> get_nth tail (n-1)
  | (_,_) -> raise NotEnoughElements
;;

let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
     ids_to_inner_types metasenv context idrefs t expectedty
=
 let module D = DoubleTypeInference in
 let module C = Cic in
  let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in
   let time1 = Sys.time () in
   let terms_to_types =
     let time0 = Sys.time () in
     let prova = CicTypeChecker.type_of_aux' metasenv context t in
     let time1 = Sys.time () in
     prerr_endline ("*** Fine type_inference:" ^ (string_of_float (time1 -. time0)));
     let res = D.double_type_of metasenv context t expectedty in
     let time2 = Sys.time () in
   prerr_endline ("*** Fine double_type_inference:" ^ (string_of_float (time2 -. time1)));
     res 
   in
   let time2 = Sys.time () in
   prerr_endline
    ("++++++++++++ Tempi della double_type_of: "^ string_of_float (time2 -. time1)) ;
    let rec aux computeinnertypes father context idrefs tt =
     let fresh_id'' = fresh_id' father tt in
     (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
     let aux' = aux computeinnertypes (Some fresh_id'') in
      (* First of all we compute the inner type and the inner sort *)
      (* of the term. They may be useful in what follows.          *)
      (*CSC: This is a very inefficient way of computing inner types *)
      (*CSC: and inner sorts: very deep terms have their types/sorts *)
      (*CSC: computed again and again.                               *)
      let string_of_sort t =
       match CicReduction.whd context t with 
          C.Sort C.Prop  -> "Prop"
        | C.Sort C.Set   -> "Set"
        | C.Sort C.Type  -> "Type"
	| C.Sort C.CProp -> "CProp"
        | _              -> assert false
      in
       let ainnertypes,innertype,innersort,expected_available =
(*CSC: Here we need the algorithm for Coscoy's double type-inference  *)
(*CSC: (expected type + inferred type). Just for now we use the usual *)
(*CSC: type-inference, but the result is very poor. As a very weak    *)
(*CSC: patch, I apply whd to the computed type. Full beta             *)
(*CSC: reduction would be a much better option.                       *)
(*CSC: solo per testare i tempi *)
(*XXXXXXX *)
        try
(* *)
        let {D.synthesized = synthesized; D.expected = expected} =
         if computeinnertypes then
          D.CicHash.find terms_to_types tt
         else
          (* We are already in an inner-type and Coscoy's double *)
          (* type inference algorithm has not been applied.      *)
          {D.synthesized =
(***CSC: patch per provare i tempi
            CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *)
Cic.Sort Cic.Type ;
          D.expected = None}
        in
         incr number_new_type_of_aux' ;
         let innersort = (*XXXXX *) xxx_type_of_aux' metasenv context synthesized (* Cic.Sort Cic.Prop *) in
          let ainnertypes,expected_available =
           if computeinnertypes then
            let annexpected,expected_available =
               match expected with
                  None -> None,false
                | Some expectedty' ->
                   Some
                    (aux false (Some fresh_id'') context idrefs expectedty'),
                    true
            in
             Some
              {annsynthesized =
                aux false (Some fresh_id'') context idrefs synthesized ;
               annexpected = annexpected
              }, expected_available
           else
            None,false
          in
           ainnertypes,synthesized, string_of_sort innersort, expected_available
(*XXXXXXXX *)
        with
         Not_found ->  (* l'inner-type non e' nella tabella ==> sort <> Prop *)
          (* CSC: Type or Set? I can not tell *)
          None,Cic.Sort Cic.Type,"Type",false
(* *)
       in
        let add_inner_type id =
         match ainnertypes with
            None -> ()
          | Some ainnertypes -> xxx_add ids_to_inner_types id ainnertypes
        in
         match tt with
            C.Rel n ->
             let id =
              match get_nth context n with
                 (Some (C.Name s,_)) -> s
               | _ -> raise NameExpected
             in
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop"  && expected_available then
               add_inner_type fresh_id'' ;
              C.ARel (fresh_id'', List.nth idrefs (n-1), n, id)
          | C.Var (uri,exp_named_subst) ->
             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
             if innersort = "Prop"  && expected_available then
              add_inner_type fresh_id'' ;
             let exp_named_subst' =
              List.map
               (function i,t -> i, (aux' context idrefs t)) exp_named_subst
             in
              C.AVar (fresh_id'', uri,exp_named_subst')
          | C.Meta (n,l) ->
             let (_,canonical_context,_) =
              List.find (function (m,_,_) -> n = m) metasenv
             in
             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
             if innersort = "Prop"  && expected_available then
              add_inner_type fresh_id'' ;
             C.AMeta (fresh_id'', n,
              (List.map2
                (fun ct t ->
                  match (ct, t) with
                  | None, _ -> None
                  | _, Some t -> Some (aux' context idrefs t)
                  | Some _, None -> assert false (* due to typing rules *))
                canonical_context l))
          | C.Sort s -> C.ASort (fresh_id'', s)
          | C.Implicit -> C.AImplicit (fresh_id'')
          | C.Cast (v,t) ->
             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
             if innersort = "Prop" then
              add_inner_type fresh_id'' ;
             C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t)
          | C.Prod (n,s,t) ->
              xxx_add ids_to_inner_sorts fresh_id''
               (string_of_sort innertype) ;
	            let sourcetype = xxx_type_of_aux' metasenv context s in
	             xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
	              (string_of_sort sourcetype) ;
              let n' =
               match n with
                  C.Anonymous -> n
                | C.Name n' ->
                   if DoubleTypeInference.does_not_occur 1 t then
                    C.Anonymous
                   else
                    C.Name n'
              in
               C.AProd
                (fresh_id'', n', aux' context idrefs s,
                 aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
          | C.Lambda (n,s,t) ->
             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
	           let sourcetype = xxx_type_of_aux' metasenv context s in
	            xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
	             (string_of_sort sourcetype) ;
              if innersort = "Prop" then
               begin
                let father_is_lambda =
                 match father with
                    None -> false
                  | Some father' ->
                     match Hashtbl.find ids_to_terms father' with
                        C.Lambda _ -> true
                      | _ -> false
                in
                 if (not father_is_lambda) || expected_available then
                  add_inner_type fresh_id''
               end ;
              C.ALambda
               (fresh_id'',n, aux' context idrefs s,
                aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
          | C.LetIn (n,s,t) ->
             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
             if innersort = "Prop" then
              add_inner_type fresh_id'' ;
             C.ALetIn
              (fresh_id'', n, aux' context idrefs s,
               aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t)
          | C.Appl l ->
             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
             if innersort = "Prop" then
              add_inner_type fresh_id'' ;
             C.AAppl (fresh_id'', List.map (aux' context idrefs) l)
          | C.Const (uri,exp_named_subst) ->
             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
             if innersort = "Prop"  && expected_available then
              add_inner_type fresh_id'' ;
             let exp_named_subst' =
              List.map
               (function i,t -> i, (aux' context idrefs t)) exp_named_subst
             in
              C.AConst (fresh_id'', uri, exp_named_subst')
          | C.MutInd (uri,tyno,exp_named_subst) ->
             let exp_named_subst' =
              List.map
               (function i,t -> i, (aux' context idrefs t)) exp_named_subst
             in
              C.AMutInd (fresh_id'', uri, tyno, exp_named_subst')
          | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
             if innersort = "Prop"  && expected_available then
              add_inner_type fresh_id'' ;
             let exp_named_subst' =
              List.map
               (function i,t -> i, (aux' context idrefs t)) exp_named_subst
             in
              C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst')
          | C.MutCase (uri, tyno, outty, term, patterns) ->
             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
             if innersort = "Prop" then
              add_inner_type fresh_id'' ;
             C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty,
              aux' context idrefs term, List.map (aux' context idrefs) patterns)
          | C.Fix (funno, funs) ->
             let fresh_idrefs =
              List.map (function _ -> gen_id seed) funs in
             let new_idrefs = List.rev fresh_idrefs @ idrefs in
             let tys =
              List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
             in
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop" then
               add_inner_type fresh_id'' ;
              C.AFix (fresh_id'', funno,
               List.map2
                (fun id (name, indidx, ty, bo) ->
                  (id, name, indidx, aux' context idrefs ty,
                    aux' (tys@context) new_idrefs bo)
                ) fresh_idrefs funs
             )
          | C.CoFix (funno, funs) ->
             let fresh_idrefs =
              List.map (function _ -> gen_id seed) funs in
             let new_idrefs = List.rev fresh_idrefs @ idrefs in
             let tys =
              List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs
             in
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop" then
               add_inner_type fresh_id'' ;
              C.ACoFix (fresh_id'', funno,
               List.map2
                (fun id (name, ty, bo) ->
                  (id, name, aux' context idrefs ty,
                    aux' (tys@context) new_idrefs bo)
                ) fresh_idrefs funs
              )
        in
         let timea = Sys.time () in
         let res = aux true None context idrefs t in
         let timeb = Sys.time () in
          prerr_endline
           ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ;
          res
;;

let acic_of_cic_context metasenv context idrefs t =
 let ids_to_terms = Hashtbl.create 503 in
 let ids_to_father_ids = Hashtbl.create 503 in
 let ids_to_inner_sorts = Hashtbl.create 503 in
 let ids_to_inner_types = Hashtbl.create 503 in
 let seed = ref 0 in
   acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
    ids_to_inner_types metasenv context idrefs t,
   ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
;;

let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids 
  ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
  metasenv (metano,context,goal) = 
  let acic_of_cic_context =
    acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
      ids_to_inner_types  metasenv in
  let _, acontext,final_idrefs =
    (List.fold_right
      (fun binding (context, acontext,idrefs) ->
         let hid = "h" ^ string_of_int !hypotheses_seed in
           Hashtbl.add ids_to_hypotheses hid binding ;
           incr hypotheses_seed ;
           match binding with
               Some (n,Cic.Def (t,None)) ->
                 let acic = acic_of_cic_context context idrefs t None in
                 (binding::context),
                   ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
             | Some (n,Cic.Decl t) ->
                 let acic = acic_of_cic_context context idrefs t None in
                 (binding::context),
                   ((hid,Some (n,Cic.ADecl acic))::acontext),(hid::idrefs)
             | None ->
                 (* Invariant: "" is never looked up *)
                  (None::context),((hid,None)::acontext),""::idrefs
             | Some (_,Cic.Def (_,Some _)) -> assert false
         ) context ([],[],[])
       )
  in 
  let agoal = acic_of_cic_context context final_idrefs goal None in
  (metano,acontext,agoal)
;;

let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) = 
    let ids_to_terms = Hashtbl.create 503 in
    let ids_to_father_ids = Hashtbl.create 503 in
    let ids_to_inner_sorts = Hashtbl.create 503 in
    let ids_to_inner_types = Hashtbl.create 503 in
    let ids_to_hypotheses = Hashtbl.create 23 in
    let hypotheses_seed = ref 0 in
    let seed = ref 1 in (* 'i0' is used for the whole sequent *)
    let (metano,acontext,agoal) = 
      aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids 
      ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
      metasenv sequent in
    ("i0",metano,acontext,agoal), 
     ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses
;;

let acic_object_of_cic_object obj =
 let module C = Cic in
 let module E = Eta_fixing in
  let ids_to_terms = Hashtbl.create 503 in
  let ids_to_father_ids = Hashtbl.create 503 in
  let ids_to_inner_sorts = Hashtbl.create 503 in
  let ids_to_inner_types = Hashtbl.create 503 in
  let ids_to_conjectures = Hashtbl.create 11 in
  let ids_to_hypotheses = Hashtbl.create 127 in
  let hypotheses_seed = ref 0 in
  let conjectures_seed = ref 0 in
  let seed = ref 0 in
  let acic_term_of_cic_term_context' =
   acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
    ids_to_inner_types in
  let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] [] in
  let aconjecture_of_conjecture' = aconjecture_of_conjecture seed 
    ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types 
    ids_to_hypotheses hypotheses_seed in 
   let aobj =
    match obj with
      C.Constant (id,Some bo,ty,params) ->
       let bo' = E.eta_fix [] bo in
       let ty' = E.eta_fix [] ty in
       let abo = acic_term_of_cic_term' bo' (Some ty') in
       let aty = acic_term_of_cic_term' ty' None in
        C.AConstant
         ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params)
    | C.Constant (id,None,ty,params) ->
       let ty' = E.eta_fix [] ty in
       let aty = acic_term_of_cic_term' ty' None in
        C.AConstant
         ("mettereaposto",None,id,None,aty,params)
    | C.Variable (id,bo,ty,params) ->
       let ty' = E.eta_fix [] ty in
       let abo =
        match bo with
           None -> None
         | Some bo ->
            let bo' = E.eta_fix [] bo in
             Some (acic_term_of_cic_term' bo' (Some ty'))
       in
       let aty = acic_term_of_cic_term' ty' None in
        C.AVariable
         ("mettereaposto",id,abo,aty, params)
    | C.CurrentProof (id,conjectures,bo,ty,params) ->
       let conjectures' =
        List.map
         (function (i,canonical_context,term) ->
           let canonical_context' =
            List.map
             (function
                 None -> None
               | Some (n, C.Decl t)-> Some (n, C.Decl (E.eta_fix conjectures t))
               | Some (n, C.Def (t,None)) ->
                  Some (n, C.Def ((E.eta_fix conjectures t),None))
               | Some (_,C.Def (_,Some _)) -> assert false
             ) canonical_context
           in
           let term' = E.eta_fix conjectures term in
            (i,canonical_context',term')
         ) conjectures
       in
       let aconjectures = 
        List.map
         (function (i,canonical_context,term) as conjecture ->
           let cid = "c" ^ string_of_int !conjectures_seed in
            xxx_add ids_to_conjectures cid conjecture ;
            incr conjectures_seed ;
           let (i,acanonical_context,aterm) 
             = aconjecture_of_conjecture' conjectures conjecture in
           (cid,i,acanonical_context,aterm))
          conjectures' in 
(*           let idrefs',revacanonical_context =
             let rec aux context idrefs =
              function
                 [] -> idrefs,[]
               | hyp::tl ->
                  let hid = "h" ^ string_of_int !hypotheses_seed in
                  let new_idrefs = hid::idrefs in
                   xxx_add ids_to_hypotheses hid hyp ;
                   incr hypotheses_seed ;
                   match hyp with
                      (Some (n,C.Decl t)) ->
                        let final_idrefs,atl =
                         aux (hyp::context) new_idrefs tl in
                        let at =
                         acic_term_of_cic_term_context'
                          conjectures context idrefs t None
                        in
                         final_idrefs,(hid,Some (n,C.ADecl at))::atl
                    | (Some (n,C.Def (t,_))) ->
                        let final_idrefs,atl =
                         aux (hyp::context) new_idrefs tl in
                        let at =
                         acic_term_of_cic_term_context'
                          conjectures context idrefs t None
                        in
                         final_idrefs,(hid,Some (n,C.ADef at))::atl
                    | None ->
                       let final_idrefs,atl =
                        aux (hyp::context) new_idrefs tl
                       in
                        final_idrefs,(hid,None)::atl
             in
              aux [] [] (List.rev canonical_context) 
            in
             let aterm =
              acic_term_of_cic_term_context' conjectures
               canonical_context idrefs' term None 
             in
              (cid,i,(List.rev revacanonical_context),aterm) 
         ) conjectures' in *)
       let time1 = Sys.time () in
       let bo' = E.eta_fix conjectures' bo in
       let ty' = E.eta_fix conjectures' ty in
       let time2 = Sys.time () in
       prerr_endline
        ("++++++++++ Tempi della eta_fix: "^ string_of_float (time2 -. time1)) ;
       hashtbl_add_time := 0.0 ;
       type_of_aux'_add_time := 0.0 ;
       DoubleTypeInference.syntactic_equality_add_time := 0.0 ;
       let abo =
        acic_term_of_cic_term_context' conjectures' [] [] bo' (Some ty') in
       let aty = acic_term_of_cic_term_context' conjectures' [] [] ty' None in
       let time3 = Sys.time () in
       prerr_endline
        ("++++++++++++ Tempi della hashtbl_add_time: " ^ string_of_float !hashtbl_add_time) ;
       prerr_endline
        ("++++++++++++ Tempi della type_of_aux'_add_time(" ^ string_of_int !number_new_type_of_aux' ^ "): " ^ string_of_float !type_of_aux'_add_time) ;
       prerr_endline
        ("++++++++++++ Tempi della type_of_aux'_add_time nella double_type_inference(" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux'_double_work ^ ";" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux'_prop ^ "/" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux' ^ "): " ^ string_of_float !DoubleTypeInference.type_of_aux'_add_time) ;
       prerr_endline
        ("++++++++++++ Tempi della syntactic_equality_add_time: " ^ string_of_float !DoubleTypeInference.syntactic_equality_add_time) ;
       prerr_endline
        ("++++++++++ Tempi della acic_of_cic: " ^ string_of_float (time3 -. time2)) ;
       prerr_endline
        ("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ;
        C.ACurrentProof
         ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params)
    | C.InductiveDefinition (tys,params,paramsno) ->
       let context =
        List.map
         (fun (name,_,arity,_) -> Some (C.Name name, C.Decl arity)) tys in
       let idrefs = List.map (function _ -> gen_id seed) tys in
       let atys =
        List.map2
         (fun id (name,inductive,ty,cons) ->
           let acons =
            List.map
             (function (name,ty) ->
               (name,
                 acic_term_of_cic_term_context' [] context idrefs ty None)
             ) cons
           in
            (id,name,inductive,acic_term_of_cic_term' ty None,acons)
         ) (List.rev idrefs) tys
       in
        C.AInductiveDefinition ("mettereaposto",atys,params,paramsno)
   in
    aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
     ids_to_conjectures,ids_to_hypotheses
;;