path: root/pretyping/indrec.ml

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id: indrec.ml,v 1.20.2.3 2004/07/16 19:30:44 herbelin Exp $ *)

open Pp
open Util
open Names
open Libnames
open Nameops
open Term
open Termops
open Declarations
open Entries
open Inductive
open Inductiveops
open Instantiate
open Environ
open Reductionops
open Typeops
open Type_errors
open Indtypes (* pour les erreurs *)
open Safe_typing
open Nametab

let make_prod_dep dep env = if dep then prod_name env else mkProd
let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)

(*******************************************)
(* Building curryfied elimination          *)
(*******************************************)

(**********************************************************************)
(* Building case analysis schemes *)
(* Nouvelle version, plus concise mais plus coûteuse à cause de
   lift_constructor et lift_inductive_family qui ne se contentent pas de 
   lifter les paramètres globaux *)

let mis_make_case_com depopt env sigma (ind,mib,mip) kind =
  let lnamespar = mip.mind_params_ctxt in
  let dep = match depopt with 
    | None -> mip.mind_sort <> (Prop Null)
    | Some d -> d
  in
  if not (List.exists ((=) kind) mip.mind_kelim) then
    raise
      (InductiveError
	 (NotAllowedCaseAnalysis
	    (dep,(new_sort_in_family kind),ind)));

  let nbargsprod = mip.mind_nrealargs + 1 in

  (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
  (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
  let env' = push_rel_context lnamespar env in

  let indf = make_ind_family(ind, extended_rel_list 0 lnamespar) in
  let constrs = get_constructors env indf in

  let rec add_branch env k = 
    if k = Array.length mip.mind_consnames then
      let nbprod = k+1 in
      let indf = make_ind_family(ind,extended_rel_list nbprod lnamespar) in
      let lnamesar,_ = get_arity env indf in
      let ci = make_default_case_info env RegularStyle ind in
      let depind = build_dependent_inductive env indf in
      let deparsign = (Anonymous,None,depind)::lnamesar in
      let p =
      it_mkLambda_or_LetIn_name env'
          (appvect
            (mkRel ((if dep then nbargsprod else mip.mind_nrealargs) + nbprod),
            if dep then extended_rel_vect 0 deparsign
            else extended_rel_vect 0 lnamesar))
          (if dep then deparsign else lnamesar) in
      it_mkLambda_or_LetIn_name env'
       	(mkCase (ci, lift nbargsprod p,
		     mkRel 1,
		     rel_vect nbargsprod k))
       	deparsign
    else
      let cs = lift_constructor (k+1) constrs.(k) in
      let t = build_branch_type env dep (mkRel (k+1)) cs in
      mkLambda_string "f" t
	(add_branch (push_rel (Anonymous, None, t) env) (k+1))
  in
  let typP = make_arity env' dep indf (new_sort_in_family kind) in
  it_mkLambda_or_LetIn_name env 
    (mkLambda_string "P" typP
       (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
    
(* check if the type depends recursively on one of the inductive scheme *)

(**********************************************************************)
(* Building the recursive elimination *)

(*
 * t is the type of the constructor co and recargs is the information on 
 * the recursive calls. (It is assumed to be in form given by the user).
 * build the type of the corresponding branch of the recurrence principle
 * assuming f has this type, branch_rec gives also the term 
 *   [x1]..[xk](f xi (F xi) ...) to be put in the corresponding branch of 
 * the case operation
 * FPvect gives for each inductive definition if we want an elimination 
 * on it with which predicate and which recursive function. 
 *)

let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = 
  let make_prod = make_prod_dep dep in
  let nparams = List.length vargs in
  let process_pos env depK pk =
    let rec prec env i sign p =
      let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
      match kind_of_term p' with
	| Prod (n,t,c) ->
	    let d = (n,None,t) in
	    make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c)
	| LetIn (n,b,t,c) ->
	    let d = (n,Some b,t) in
	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c)
     	| Ind (_,_) ->
	    let realargs = list_skipn nparams largs in
	    let base = applist (lift i pk,realargs) in
            if depK then 
	      Reduction.beta_appvect
                base [|applist (mkRel (i+1),extended_rel_list 0 sign)|]
            else 
	      base
      	| _ -> assert false 
    in
    prec env 0 []
  in
  let rec process_constr env i c recargs nhyps li =
    if nhyps > 0 then match kind_of_term c with 
      | Prod (n,t,c_0) ->
          let (optionpos,rest) = 
	    match recargs with 
	      | [] -> None,[]
              | ra::rest ->
                  (match dest_recarg ra with 
	            | Mrec j when is_rec -> (depPvect.(j),rest)
	            | Imbr _  -> 
		        Options.if_verbose warning "Ignoring recursive call"; 
		        (None,rest) 
                    | _ -> (None, rest))
	  in 
          (match optionpos with 
	     | None -> 
		 make_prod env
		   (n,t,
		    process_constr (push_rel (n,None,t) env) (i+1) c_0 rest
		      (nhyps-1) (i::li))
             | Some(dep',p) -> 
		 let nP = lift (i+1+decP) p in
                 let env' = push_rel (n,None,t) env in
		 let t_0 = process_pos env' dep' nP (lift 1 t) in 
		 make_prod_dep (dep or dep') env
                   (n,t,
		    mkArrow t_0
		      (process_constr
			(push_rel (Anonymous,None,t_0) env')
			 (i+2) (lift 1 c_0) rest (nhyps-1) (i::li))))
      | LetIn (n,b,t,c_0) ->
	  mkLetIn (n,b,t,
		   process_constr
		     (push_rel (n,Some b,t) env)
		     (i+1) c_0 recargs (nhyps-1) li)
      | _ -> assert false
    else
      if dep then
	let realargs = List.map (fun k -> mkRel (i-k)) (List.rev li) in
        let params = List.map (lift i) vargs in
        let co = applist (mkConstruct cs.cs_cstr,params@realargs) in
	Reduction.beta_appvect c [|co|]
      else c
  in
  let nhyps = List.length cs.cs_args in
  let nP = match depPvect.(tyi) with 
    | Some(_,p) -> lift (nhyps+decP) p
    | _ -> assert false in
  let base = appvect (nP,cs.cs_concl_realargs) in
  let c = it_mkProd_or_LetIn base cs.cs_args in
  process_constr env 0 c recargs nhyps []

let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs = 
  let process_pos env fk  =
    let rec prec env i hyps p =
      let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
      match kind_of_term p' with
	| Prod (n,t,c) ->
	    let d = (n,None,t) in
	    lambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
	| LetIn (n,b,t,c) ->
	    let d = (n,Some b,t) in
	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
     	| Ind _ -> 
            let realargs = list_skipn nparams largs
            and arg = appvect (mkRel (i+1),extended_rel_vect 0 hyps) in 
            applist(lift i fk,realargs@[arg])
     	| _ -> assert false
    in
    prec env 0 []
  in
  (* ici, cstrprods est la liste des produits du constructeur instantié *)
  let rec process_constr env i f = function
    | (n,None,t as d)::cprest, recarg::rest -> 
        let optionpos = 
	  match dest_recarg recarg with 
            | Norec   -> None
            | Imbr _  -> None
            | Mrec i  -> fvect.(i)
	in 
        (match optionpos with 
           | None ->
	       lambda_name env
		 (n,t,process_constr (push_rel d env) (i+1)
		    (whd_beta (applist (lift 1 f, [(mkRel 1)])))
		    (cprest,rest))
           | Some(_,f_0) -> 
	       let nF = lift (i+1+decF) f_0 in
               let env' = push_rel d env in
	       let arg = process_pos env' nF (lift 1 t) in 
               lambda_name env
		 (n,t,process_constr env' (i+1)
		    (whd_beta (applist (lift 1 f, [(mkRel 1); arg])))
		    (cprest,rest)))
    | (n,Some c,t as d)::cprest, rest ->
	mkLetIn
	  (n,c,t,
	   process_constr (push_rel d env) (i+1) (lift 1 f)
	     (cprest,rest))
    | [],[] -> f
    | _,[] | [],_ -> anomaly "process_constr"

  in
  process_constr env 0 f (List.rev cstr.cs_args, recargs)

(* Main function *)
let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
  let nparams = mip.mind_nparams in
  let lnamespar = mip.mind_params_ctxt in
  let nrec = List.length listdepkind in
  let depPvec =
    Array.create mib.mind_ntypes (None : (bool * constr) option) in 
  let _ = 
    let rec 
      assign k = function 
	| [] -> ()
        | (indi,mibi,mipi,dep,_)::rest -> 
            (Array.set depPvec (snd indi) (Some(dep,mkRel k));
             assign (k-1) rest)
    in 
    assign nrec listdepkind in 
  let recargsvec =
    Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
  let make_one_rec p =
    let makefix nbconstruct =
      let rec mrec i ln ltyp ldef = function
	| (indi,mibi,mipi,dep,_)::rest ->
	    let tyi = snd indi in
	    let nctyi =
              Array.length mipi.mind_consnames in (* nb constructeurs du type*)

            (* arity in the context of the fixpoint, i.e.
                P1..P_nrec f1..f_nbconstruct *)
	    let args = extended_rel_list (nrec+nbconstruct) lnamespar in
	    let indf = make_ind_family(indi,args) in
	    let lnames,_ = get_arity env indf in

	    let nar = mipi.mind_nrealargs in
	    let dect = nar+nrec+nbconstruct in

	    let branches = 
              (* constructors in context of the Cases expr, i.e.
                 P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
	      let args' = extended_rel_list (dect+nrec+1) lnamespar in
              let indf' = make_ind_family(indi,args') in
	      let constrs = get_constructors env indf' in
	      let vecfi = rel_vect (dect+1-i-nctyi) nctyi in
	      array_map3
		(make_rec_branch_arg env sigma (nparams,depPvec,nar+1))
                vecfi constrs (dest_subterms recargsvec.(tyi)) in
	    let j = (match depPvec.(tyi) with 
		       | Some (_,c) when isRel c -> destRel c 
		       | _ -> assert false) in
	    let deftyi = 
	      let ci = make_default_case_info env RegularStyle indi in
	      let indf' = lift_inductive_family nrec indf in
	      let depind = build_dependent_inductive env indf' in
	      let lnames' = Termops.lift_rel_context nrec lnames in
	      let p =
		let arsign =
		  if dep then (Anonymous,None,depind)::lnames' else lnames' in
		it_mkLambda_or_LetIn_name env
		  (appvect
		    (mkRel ((if dep then 1 else 0) + dect + j),
		    extended_rel_vect 0 arsign)) arsign
	      in
	      it_mkLambda_or_LetIn_name env
		(lambda_create env
		  (depind,mkCase (ci, lift (nar+1) p, mkRel 1, branches)))
		lnames'
	    in
	    let typtyi = 
	      let ind = build_dependent_inductive env indf in
	      it_mkProd_or_LetIn_name env
		(prod_create env
		   (ind,
		    (if dep then 
		       let ext_lnames = (Anonymous,None,ind)::lnames in
		       let args = extended_rel_list 0 ext_lnames in
		       applist (mkRel (nbconstruct+nar+j+1), args)
		     else
		       let args = extended_rel_list 1 lnames in
		       applist (mkRel (nbconstruct+nar+j+1), args))))
          	lnames
	    in 
	    mrec (i+nctyi) (nar::ln) (typtyi::ltyp) (deftyi::ldef) rest
        | [] -> 
	    let fixn = Array.of_list (List.rev ln) in
            let fixtyi = Array.of_list (List.rev ltyp) in
            let fixdef = Array.of_list (List.rev ldef) in 
            let names = Array.create nrec (Name(id_of_string "F")) in
	    mkFix ((fixn,p),(names,fixtyi,fixdef))
      in 
      mrec 0 [] [] [] 
    in 
    let rec make_branch env i = function 
      | (indi,mibi,mipi,dep,_)::rest ->
          let tyi = snd indi in
	  let nconstr = Array.length mipi.mind_consnames in
	  let rec onerec env j = 
	    if j = nconstr then 
	      make_branch env (i+j) rest 
	    else 
	      let recarg = (dest_subterms recargsvec.(tyi)).(j) in
	      let vargs = extended_rel_list (nrec+i+j) lnamespar in
	      let indf = (indi, vargs) in
	      let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in
	      let p_0 =
		type_rec_branch
                  true dep env sigma (vargs,depPvec,i+j) tyi cs recarg
	      in 
	      mkLambda_string "f" p_0
		(onerec (push_rel (Anonymous,None,p_0) env) (j+1))
	  in onerec env 0
      | [] -> 
	  makefix i listdepkind
    in 
    let rec put_arity env i = function 
      | (indi,_,_,dep,kinds)::rest -> 
	  let indf = make_ind_family (indi,extended_rel_list i lnamespar) in
	  let typP = make_arity env dep indf (new_sort_in_family kinds) in
	  mkLambda_string "P" typP
	    (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
      | [] -> 
	  make_branch env 0 listdepkind 
    in 
    let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in
    let env' = push_rel_context lnamespar env in
    if mis_is_recursive_subset
      (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind)
      mipi.mind_recargs
    then 
      it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) lnamespar
    else 
      mis_make_case_com (Some dep) env sigma (indi,mibi,mipi) kind 
  in 
  list_tabulate make_one_rec nrec

(**********************************************************************)
(* This builds elimination predicate for Case tactic *)

let make_case_com depopt env sigma ity kind =
  let (mib,mip) = lookup_mind_specif env ity in 
  mis_make_case_com depopt env sigma (ity,mib,mip) kind

let make_case_dep env   = make_case_com (Some true) env
let make_case_nodep env = make_case_com (Some false) env 
let make_case_gen env   = make_case_com None env


(**********************************************************************)
(* [instanciate_indrec_scheme s rec] replace the sort of the scheme
   [rec] by [s] *)

let change_sort_arity sort = 
  let rec drec a = match kind_of_term a with
    | Cast (c,t) -> drec c 
    | Prod (n,t,c) -> mkProd (n, t, drec c)
    | Sort _ -> mkSort sort
    | _ -> assert false
  in 
  drec 

(* [npar] is the number of expected arguments (then excluding letin's) *)
let instanciate_indrec_scheme sort =
  let rec drec npar elim =
    match kind_of_term elim with
      | Lambda (n,t,c) -> 
	  if npar = 0 then 
	    mkLambda (n, change_sort_arity sort t, c)
	  else 
	    mkLambda (n, t, drec (npar-1) c)
      | LetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c)
      | _ -> anomaly "instanciate_indrec_scheme: wrong elimination type"
  in
  drec

(* Change the sort in the type of an inductive definition, builds the
   corresponding eta-expanded term *)
let instanciate_type_indrec_scheme sort npars term =
  let rec drec np elim =
    match kind_of_term elim with
      | Prod (n,t,c) -> 
	  if np = 0 then 
            let t' = change_sort_arity sort t in
            mkProd (n, t', c),
            mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1)))
	  else 
            let c',term' = drec (np-1) c in
	    mkProd (n, t, c'), mkLambda (n, t, term')
      | LetIn (n,b,t,c) -> let c',term' = drec np c in
           mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') 
      | _ -> anomaly "instanciate_type_indrec_scheme: wrong elimination type"
  in
  drec npars

(**********************************************************************)
(* Interface to build complex Scheme *)

let check_arities listdepkind = 
  List.iter 
    (function (indi,mibi,mipi,dep,kind) -> 
       let id = mipi.mind_typename  in
       let kelim = mipi.mind_kelim in
       if not (List.exists ((=) kind) kelim) then
	 raise
	   (InductiveError (BadInduction (dep, id, new_sort_in_family kind))))
    listdepkind

let build_mutual_indrec env sigma = function 
  | (mind,mib,mip,dep,s)::lrecspec ->
      let (sp,tyi) = mind in
      let listdepkind = 
    	(mind,mib,mip, dep,s)::
    	(List.map
	   (function (mind',mibi',mipi',dep',s') ->
	      let (sp',_) = mind' in
	      if sp=sp' then 
                let (mibi',mipi') = lookup_mind_specif env mind' in
		(mind',mibi',mipi',dep',s') 
	      else 
		raise (InductiveError NotMutualInScheme))
	   lrecspec)
      in
      let _ = check_arities listdepkind in 
      mis_make_indrec env sigma listdepkind (mind,mib,mip)
  | _ -> anomaly "build_indrec expects a non empty list of inductive types"

let build_indrec env sigma ind =
  let (mib,mip) = lookup_mind_specif env ind in
  let kind = family_of_sort mip.mind_sort in
  let dep = kind <> InProp in
  List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] (ind,mib,mip))

(**********************************************************************)
(* To handle old Case/Match syntax in Pretyping                       *)

(*****************************************)
(* To interpret Case and Match operators *)
(* Expects a dependent predicate *)

let type_rec_branches recursive env sigma indt p c = 
  let IndType (indf,realargs) = indt in
  let (ind,params) = dest_ind_family indf in
  let (mib,mip) = lookup_mind_specif env ind in
  let recargs = mip.mind_recargs in
  let tyi = snd ind in
  let init_depPvec i = if i = tyi then Some(true,p) else None in
  let depPvec = Array.init mib.mind_ntypes init_depPvec in
  let vargs = Array.of_list params in
  let constructors = get_constructors env indf in
  let lft =
    array_map2
      (type_rec_branch recursive true env sigma (params,depPvec,0) tyi)
      constructors (dest_subterms recargs) in
  (lft,Reduction.beta_appvect p (Array.of_list (realargs@[c])))
(* Non recursive case. Pb: does not deal with unification
    let (p,ra,_) = type_case_branches env (ind,params@realargs) pj c in
    (p,ra)
*)

(*s Eliminations. *)

let elimination_suffix = function
  | InProp -> "_ind"
  | InSet  -> "_rec"
  | InType -> "_rect"

let make_elimination_ident id s = add_suffix id (elimination_suffix s)

(* Look up function for the default elimination constant *)

let lookup_eliminator ind_sp s =
  let kn,i = ind_sp in
  let mp,dp,l = repr_kn kn in
  let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
  let id = add_suffix ind_id (elimination_suffix s) in
  (* Try first to get an eliminator defined in the same section as the *)
  (* inductive type *)
  let ref = ConstRef (make_kn mp dp (label_of_id id)) in
  try 
    let _ = sp_of_global ref in
    constr_of_reference ref
  with Not_found ->
  (* Then try to get a user-defined eliminator in some other places *)
  (* using short name (e.g. for "eq_rec") *)
  try constr_of_reference (Nametab.locate (make_short_qualid id))
  with Not_found ->
    errorlabstrm "default_elim"
      (str "Cannot find the elimination combinator " ++
       pr_id id ++ spc () ++
       str "The elimination of the inductive definition " ++
       pr_id id ++ spc () ++ str "on sort " ++ 
       spc () ++ print_sort_family s ++
       str " is probably not allowed")


(*  let env = Global.env() in
  let path = sp_of_global None (IndRef ind_sp) in
  let dir, base = repr_path path in
  let id = add_suffix base (elimination_suffix s) in
  (* Try first to get an eliminator defined in the same section as the *)
  (* inductive type *)
  try construct_absolute_reference (Names.make_path dir id)
  with Not_found ->
  (* Then try to get a user-defined eliminator in some other places *)
  (* using short name (e.g. for "eq_rec") *)
    try constr_of_reference (Nametab.locate (make_short_qualid id))
    with Not_found ->
      errorlabstrm "default_elim"
	(str "Cannot find the elimination combinator " ++
           pr_id id ++ spc () ++
	   str "The elimination of the inductive definition " ++
           pr_id base ++ spc () ++ str "on sort " ++ 
           spc () ++ print_sort_family s ++
	   str " is probably not allowed")
*)