(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)

let fresh_name =
 let i = ref 0 in
 function () ->
  incr i;
  "x_" ^ string_of_int !i
;;

let mk_id id =
 let id = if id = "_" then fresh_name () else id in
  CicNotationPt.Ident (id,None)
;;

(*CSC: cut&paste from nCicReduction.split_prods, but does not check that
  the return type is a sort *)
let rec my_split_prods ~subst context n te =
  match (n, NCicReduction.whd ~subst context te) with
   | (0, _) -> context,te
   | (n, NCic.Prod (name,so,ta)) ->
       my_split_prods ~subst ((name,(NCic.Decl so))::context) (n - 1) ta
   | (n, _) when n <= 0 -> context,te
   | (_, _) -> raise (Failure "my_split_prods")
;;

let mk_elims (uri,_,_,_,obj) =
 match obj with
    NCic.Inductive (true,leftno,[it],_) ->
     let _,ind_name,ty,cl = it in
     let rec_name = ind_name ^ "_rect" in
     let rec_name = mk_id rec_name in
     let name_of_k id = mk_id ("H_" ^ id) in
     let p_name = mk_id "Q_" in
     let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
     let params = List.rev_map (function name,_ -> mk_id name) params in
     let args,sort = NCicReduction.split_prods ~subst:[] [] (-1) ty in
     let args = List.rev_map (function name,_ -> mk_id name) args in
     let rec_arg = mk_id (fresh_name ()) in
     let p_ty =
      List.fold_right
       (fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args
       (CicNotationPt.Binder
        (`Forall,
         (rec_arg,Some (CicNotationPt.Appl (mk_id ind_name :: params @ args))),
         CicNotationPt.Sort (`Type (CicUniv.fresh ())))) in
     let args = args @ [rec_arg] in
     let k_names = List.map (function _,name,_ -> name_of_k name) cl in
     let final_params =
      List.map (function name -> name, None) params @
      [p_name,Some p_ty] @
      List.map (function name -> name, None) k_names @
      List.map (function name -> name, None) args in
     let ty = Some (CicNotationPt.Appl (p_name :: args)) in
     let branches =
      List.map
       (function (_,name,ty) ->
         let _,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
         let cargs,ty= my_split_prods ~subst:[] [] (-1) ty in
         let cargs_and_recursive_args =
          List.rev_map
           (function
               _,NCic.Def _ -> assert false
             | name,NCic.Decl ty ->
                let context,ty = my_split_prods ~subst:[] [] (-1) ty in
                 match ty with
                  | NCic.Const nref
                  | NCic.Appl (NCic.Const nref::_)
                     when
                      let NReference.Ref (uri',_) = nref in
                       NUri.eq uri uri'
                     ->
                      let abs = List.rev_map (fun id,_ -> mk_id id) context in
                      let name = mk_id name in
                       name, Some (
                       List.fold_right
                        (fun id res ->
                          CicNotationPt.Binder (`Lambda,(id,None),res))
                        abs
                        (CicNotationPt.Appl
                         (rec_name ::
                          params @
                          [p_name] @
                          k_names @
                          List.map (fun _ -> CicNotationPt.Implicit)
                           (List.tl args) @
                          [CicNotationPt.Appl (name::abs)])))
                  | _ -> mk_id name,None
           ) cargs in
         let cargs,recursive_args = List.split cargs_and_recursive_args in
         let recursive_args = HExtlib.filter_map (fun x -> x) recursive_args in
          CicNotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs),
           CicNotationPt.Appl (name_of_k name :: cargs @ recursive_args)
       ) cl
     in
     let bo = CicNotationPt.Case (rec_arg,None,None,branches) in
     let where = List.length final_params - 1 in
     let res =
      CicNotationPt.LetRec (`Inductive,
       [final_params, (rec_name,ty), bo, where], rec_name)
     in
      prerr_endline (CicNotationPp.pp_term res);
      prerr_endline "#####";
      prerr_endline
       (BoxPp.render_to_string
         ~map_unicode_to_tex:false
         (function x::_ -> x | _ -> assert false)
         80 (CicNotationPres.render (Hashtbl.create 0)
         (TermContentPres.pp_ast res)));
      []
  | _ -> []
;;