<commit_before>(**********************************************************************)
(* Equations                                                          *)
(* Copyright (c) 2009-2021 <NAME> <<EMAIL>> *)
(**********************************************************************)
(* This file is distributed under the terms of the                    *)
(* GNU Lesser General Public License Version 2.1                      *)
(**********************************************************************)

open Util
open Names
open Nameops
open Constr
open Context
open Termops
open Declarations
open Inductiveops
open Reductionops
open Pp
open Evarutil
open List
open Globnames
open Tactics
open EConstr
open Equations_common

let mkConstructG c u =
  mkConstructU (destConstructRef (Lazy.force c), u)

let mkIndG c u =
  mkIndU (destIndRef (Lazy.force c), u)

let mkAppG evd gr args = 
  let c = e_new_global evd gr in
    mkApp (c, args)

let applistG evd gr args = 
  mkAppG evd gr (Array.of_list args)

let mkSig evd (n, c, t) = 
  let args = [| c; mkLambda (n, c, t) |] in
    mkAppG evd (Lazy.force coq_sigma) args

let constrs_of_coq_sigma env evd t alias = 
  let rec aux env proj c ty =
    match kind !evd c with
    | App (f, args) when is_global !evd (Lazy.force coq_sigmaI) f && 
	                   Array.length args = 4 ->
       let ty = Retyping.get_type_of env !evd args.(1) in
	(match kind !evd ty with
	| Prod (n, b, t) ->
	    let p1 = mkProj (Lazy.force coq_pr1, proj) in
	    let p2 = mkProj (Lazy.force coq_pr2, proj) in
	    (n, args.(2), p1, args.(0)) ::
              aux (push_rel (of_tuple (n, None, b)) env) p2 args.(3) t
	| _ -> raise (Invalid_argument "constrs_of_coq_sigma"))
    | _ -> [(Context.anonR, c, proj, ty)]
  in aux env alias t (Retyping.get_type_of env !evd t)

let decompose_coq_sigma sigma t = 
  let s = Lazy.force coq_sigma in
    match kind sigma t with
    | App (f, args) when is_global sigma s f && Array.length args = 2 ->
       let ind, u = destInd sigma f in
         Some (u, args.(0), args.(1))
    | _ -> None

let decompose_indapp sigma f args =
  match kind sigma f with
  | Construct ((ind,_),_)
  | Ind (ind,_) ->
      let (mib,mip) = Global.lookup_inductive ind in
      let first = mib.Declarations.mind_nparams_rec in
      let pars, args = Array.chop first args in
	mkApp (f, pars), args
  | _ -> f, args


(* let sigT_info = lazy (make_case_info (Global.env ()) (Globnames.destIndRef (Lazy.force sigT).typ) LetStyle) *)

let telescope_intro env sigma len tele =
  let rec aux n ty =
    let ty = Reductionops.whd_all env sigma ty in
    match kind sigma ty with
    | App (sigma_ty, [| a; p |]) ->
      let sigma_ty, u = destInd sigma sigma_ty in
      let p =
        match kind sigma p with
        | Lambda (na, t, b) ->
          mkLambda (na, t, Reductionops.whd_all
                      (push_rel (Context.Rel.Declaration.LocalAssum (na, t)) env) sigma b)
        | _ -> p
      in
      let sigmaI = mkApp (mkRef (Lazy.force coq_sigmaI, u),
                          [| a; p; mkRel n; aux (pred n) (beta_applist sigma (p, [mkRel n])) |]) in
      sigmaI
    | _ -> mkRel n
  in aux len tele

let telescope_of_context env sigma ctx =
  let sigma, teleinterp = new_global sigma (Lazy.force logic_tele_interp) in
  let _, u = destConst sigma teleinterp in
  let rec aux = function
    | [] -> raise (Invalid_argument "Cannot make telescope out of empty context")
    | [decl] ->
      mkApp (mkRef (Lazy.force logic_tele_tip, u), [|get_type decl|])
    | d :: tl ->
      let ty = get_type d in
      mkApp (mkRef (Lazy.force logic_tele_ext, u), [| ty; mkLambda (get_annot d, ty, aux tl) |])
  in
  let tele = aux (List.rev ctx) in
  let tele_interp = mkApp (teleinterp, [| tele |]) in
  (* Infer universe constraints *)
  let sigma, _ = Typing.type_of env sigma tele_interp in
  sigma, tele, tele_interp

let telescope env evd = function
  | [] -> assert false
  | [d] -> let (n, _, t) = to_tuple d in t, [of_tuple (n, Some (mkRel 1), Vars.lift 1 t)],
                                        mkRel 1
  | d :: tl ->
      let (n, _, t) = to_tuple d in
      let len = succ (List.length tl) in
      let ts = Retyping.get_sort_of (push_rel_context tl env) !evd t in
      let ty, tys =
        let rec aux (ty, tyuniv, tys) ds =
          match ds with
          | [] -> (ty, tys)
          | d :: ds ->
            let (n, b, t) = to_tuple d in
            let pred = mkLambda (n, t, ty) in
            let sigty = mkAppG evd (Lazy.force coq_sigma) [|t; pred|] in
            let _, u = destInd !evd (fst (destApp !evd sigty)) in
            let ua = Univ.Instance.to_array (EInstance.kind !evd u) in
            let l = Sorts.sort_of_univ @@ Univ.Universe.make ua.(0) in
            let env = push_rel_context ds env in
            (* Ensure that the universe of the sigma is only >= those of t and pred *)
            let enforce_leq env sigma t cstr =
              let ts = Retyping.get_sort_of env sigma t in
              UGraph.enforce_leq_sort ts l cstr
            in
            let cstrs = enforce_leq env !evd t (UGraph.enforce_leq_sort tyuniv l Univ.Constraints.empty) in
            let () = evd := Evd.add_constraints !evd cstrs in
            aux (sigty, l, (u, pred) :: tys) ds
        in aux (t, ts, []) tl
      in
      let constr, _ = 
	List.fold_right (fun (u, pred) (intro, k) ->
	  let pred = Vars.lift k pred in
	  let (n, dom, codom) = destLambda !evd pred in
	  let intro =
            mkApp (constr_of_global_univ !evd (Lazy.force coq_sigmaI, u),
                   [| dom; pred; mkRel k; intro|]) in
	    (intro, succ k))
	  tys (mkRel 1, 2)<commit_msg>Adapt w.r.t. coq/coq#15890.<commit_after>(**********************************************************************)
(* Equations                                                          *)
(* Copyright (c) 2009-2021 <NAME> <<EMAIL>> *)
(**********************************************************************)
(* This file is distributed under the terms of the                    *)
(* GNU Lesser General Public License Version 2.1                      *)
(**********************************************************************)

open Util
open Names
open Nameops
open Constr
open Context
open Termops
open Declarations
open Inductiveops
open Reductionops
open Pp
open Evarutil
open List
open Globnames
open Tactics
open EConstr
open Equations_common

let mkConstructG c u =
  mkConstructU (destConstructRef (Lazy.force c), u)

let mkIndG c u =
  mkIndU (destIndRef (Lazy.force c), u)

let mkAppG evd gr args = 
  let c = e_new_global evd gr in
    mkApp (c, args)

let applistG evd gr args = 
  mkAppG evd gr (Array.of_list args)

let mkSig evd (n, c, t) = 
  let args = [| c; mkLambda (n, c, t) |] in
    mkAppG evd (Lazy.force coq_sigma) args

let constrs_of_coq_sigma env evd t alias = 
  let rec aux env proj c ty =
    match kind !evd c with
    | App (f, args) when is_global !evd (Lazy.force coq_sigmaI) f && 
	                   Array.length args = 4 ->
       let ty = Retyping.get_type_of env !evd args.(1) in
	(match kind !evd ty with
	| Prod (n, b, t) ->
	    let p1 = mkProj (Lazy.force coq_pr1, proj) in
	    let p2 = mkProj (Lazy.force coq_pr2, proj) in
	    (n, args.(2), p1, args.(0)) ::
              aux (push_rel (of_tuple (n, None, b)) env) p2 args.(3) t
	| _ -> raise (Invalid_argument "constrs_of_coq_sigma"))
    | _ -> [(Context.anonR, c, proj, ty)]
  in aux env alias t (Retyping.get_type_of env !evd t)

let decompose_coq_sigma sigma t = 
  let s = Lazy.force coq_sigma in
    match kind sigma t with
    | App (f, args) when is_global sigma s f && Array.length args = 2 ->
       let ind, u = destInd sigma f in
         Some (u, args.(0), args.(1))
    | _ -> None

let decompose_indapp sigma f args =
  match kind sigma f with
  | Construct ((ind,_),_)
  | Ind (ind,_) ->
      let (mib,mip) = Global.lookup_inductive ind in
      let first = mib.Declarations.mind_nparams_rec in
      let pars, args = Array.chop first args in
	mkApp (f, pars), args
  | _ -> f, args


(* let sigT_info = lazy (make_case_info (Global.env ()) (Globnames.destIndRef (Lazy.force sigT).typ) LetStyle) *)

let telescope_intro env sigma len tele =
  let rec aux n ty =
    let ty = Reductionops.whd_all env sigma ty in
    match kind sigma ty with
    | App (sigma_ty, [| a; p |]) ->
      let sigma_ty, u = destInd sigma sigma_ty in
      let p =
        match kind sigma p with
        | Lambda (na, t, b) ->
          mkLambda (na, t, Reductionops.whd_all
                      (push_rel (Context.Rel.Declaration.LocalAssum (na, t)) env) sigma b)
        | _ -> p
      in
      let sigmaI = mkApp (mkRef (Lazy.force coq_sigmaI, u),
                          [| a; p; mkRel n; aux (pred n) (beta_applist sigma (p, [mkRel n])) |]) in
      sigmaI
    | _ -> mkRel n
  in aux len tele

let telescope_of_context env sigma ctx =
  let sigma, teleinterp = new_global sigma (Lazy.force logic_tele_interp) in
  let _, u = destConst sigma teleinterp in
  let rec aux = function
    | [] -> raise (Invalid_argument "Cannot make telescope out of empty context")
    | [decl] ->
      mkApp (mkRef (Lazy.force logic_tele_tip, u), [|get_type decl|])
    | d :: tl ->
      let ty = get_type d in
      mkApp (mkRef (Lazy.force logic_tele_ext, u), [| ty; mkLambda (get_annot d, ty, aux tl) |])
  in
  let tele = aux (List.rev ctx) in
  let tele_interp = mkApp (teleinterp, [| tele |]) in
  (* Infer universe constraints *)
  let sigma, _ = Typing.type_of env sigma tele_interp in
  sigma, tele, tele_interp

let telescope env evd = function
  | [] -> assert false
  | [d] -> let (n, _, t) = to_tuple d in t, [of_tuple (n, Some (mkRel 1), Vars.lift 1 t)],
                                        mkRel 1
  | d :: tl ->
      let (n, _, t) = to_tuple d in
      let len = succ (List.length tl) in
      let ts = Retyping.get_sort_of (push_rel_context tl env) !evd t in
      let ty, tys =
        let rec aux (ty, tyuniv, tys) ds =
          match ds with
          | [] -> (ty, tys)
          | d :: ds ->
            let (n, b, t) = to_tuple d in
            let pred = mkLambda (n, t, ty) in
            let sigty = mkAppG evd (Lazy.force coq_sigma) [|t; pred|] in
            let _, u = destInd !evd (fst (destApp !evd sigty)) in
            let ua = Univ.Instance.to_array (EInstance.kind !evd u) in
            let l = Sorts.sort_of_univ @@ Univ.Universe.make ua.(0) in
            let env = push_rel_context ds env in
            (* Ensure that the universe of the sigma is only >= those of t and pred *)
            let open UnivProblem in
            let enforce_leq env sigma t cstr =
              let ts = Retyping.get_sort_of env sigma t in
              UnivProblem.Set.add (ULe (ts, l)) cstr
            in
            let cstrs = enforce_leq env !evd t (UnivProblem.Set.add (ULe (tyuniv, l)) UnivProblem.Set.empty) in
            let () = evd := Evd.add_universe_constraints !evd cstrs in
            aux (sigty, l, (u, pred) :: tys) ds
        in aux (t, ts, []) tl
      in
      let constr, _ = 
	List.fold_right (fun (u, pred) (intro, k) ->
	  let pred = Vars.lift k pred in
	  let (n, dom, codom) = destLambda !evd pred in
	  let intro =
            mkApp (constr_of_global_univ !evd (Lazy.force coq_sigmaI, u),
                   [| dom; pred; mkRel k; intro|]) in
	    (intro, succ k))
	  tys (mkRel 1, 2)
{'fraction_non_alphanumeric': 0.1411744022503516, 'fraction_numerical': 0.0057137834036568216, 'mean_word_length': 2.2748992515831894, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 53, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3580194', 'n_tokens_mistral': 4059, 'n_tokens_neox': 3857, 'n_words': 1367}