+(*
+ ||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 rec_arg = mk_id (fresh_name ()) in
+ let args = List.rev_map (function name,_ -> mk_id name) args 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
+ name,NCic.Def _ -> assert false
+ | name,NCic.Decl (NCic.Const nref)
+ | name,NCic.Decl (NCic.Appl (NCic.Const nref::_))
+ when
+ let NReference.Ref (uri',_) = nref in
+ NUri.eq uri uri'
+ ->
+ let name = mk_id name in
+ name, Some (
+ CicNotationPt.Appl
+ (rec_name ::
+ params @
+ [p_name] @
+ k_names @
+ List.map (fun _ -> CicNotationPt.Implicit) (List.tl args) @
+ [name]))
+ | name,_ -> 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)));
+
+ []
+ | _ -> []
+;;