<commit_before>
(* $Id$ *)

open Pp
open Util
open Names
open Term
open Inductive
open Environ
open Reduction
open Instantiate

(************************************************************************)
(* Reduction of constant hiding fixpoints (e.g. for Simpl). The trick   *)
(* is to reuse the name of the function after reduction of the fixpoint *)

exception Elimconst
exception Redelimination

type constant_evaluation = 
  | EliminationFix of int * (constant * int * (int * constr) list * int)
  | EliminationCases of int
  | NotAnElimination

(* We use a cache registered as a global table *)

let eval_table = ref Spmap.empty

type frozen = (int * constant_evaluation) Spmap.t

let init () =
  eval_table := Spmap.empty

let freeze () =
  !eval_table

let unfreeze ct =
  eval_table := ct

let _ = 
  Summary.declare_summary "evaluation"
    { Summary.freeze_function = freeze;
      Summary.unfreeze_function = unfreeze;
      Summary.init_function = init }


(* Check that c is an "elimination constant"
   [xn:An]..[x1:A1](<P>MutCase (Rel i) of f1..fk end g1 ..gp)
   or [xn:An]..[x1:A1](Fix(f|t) (Rel i1) ..(Rel ip)) 
    with i1..ip distinct variables not occuring in t 
   keep relevenant information ([i1,Ai1;..;ip,Aip],n,b)
   with b = true in case of a fixpoint in order to compute 
   an equivalent of Fix(f|t)[xi<-ai] as 
   [yip:Bip]..[yi1:Bi1](F bn..b1) 
   == [yip:Bip]..[yi1:Bi1](Fix(f|t)[xi<-ai] (Rel 1)..(Rel p))
   with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1] *)

let check_fix_reversibility cst labs args ((lv,i),(tys,_,bds)) =
  let n = List.length labs in
  let nargs = List.length args in
  if nargs > n then raise Elimconst;
  let nbfix = Array.length bds in
  let li =
    List.map
      (function d -> match kind_of_term d with
         | IsRel k ->
             if
	       array_for_all (noccurn k) tys
	       && array_for_all (noccurn (k+nbfix)) bds
	     then 
	       (k, List.nth labs (k-1)) 
	     else 
	       raise Elimconst
         | _ -> 
	     raise Elimconst) args
  in 
  if list_distinct (List.map fst li) then 
    EliminationFix (n-nargs+lv.(i)+1,(cst,nbfix,li,n))
  else 
    raise Elimconst

(* [compute_consteval_direct] expand all constant in a whole, but
   [compute_consteval] only one by one, until finding the one which is
   reversible (in case of a unary Fix) or the last one before the Fix
   if the latter is mutually defined *)

let compute_consteval_direct cst c =
  let rec srec n labs c =
    let c',l = whd_betadeltaeta_stack (Global.env()) Evd.empty c in
    match kind_of_term c' with
      | IsLambda (_,t,g) when l=[] -> srec (n+1) (t::labs) g
      | IsFix fix -> check_fix_reversibility cst labs l fix
      | IsMutCase (_,_,d,_) when isRel d -> EliminationCases n
      | _ -> NotAnElimination
  in srec 0 [] c

let rec compute_consteval cst c = 
  let rec srec n labs c =
    let c',l = whd_betaetalet_stack c in
    let nargs = List.length l in
    match kind_of_term c' with
      | IsConst cst2 ->
	  (match descend_consteval cst2 with
	     | NotAnElimination -> NotAnElimination
	     | EliminationFix (minarg,(_,nbfix,_,_ as info)) ->
		 (* We know that the underlying Fix must be fold by oldcst *)
		 (* We now try to fold it as cst only if nbfix=1 and n=0 *)
		 let new_minarg = max (minarg+n-nargs) minarg in
		 if nbfix=1 then
		   try
		     (* We try to name the Fix by cst *)
		     (* Complexit en n^2, bof, peut mieux faire *)
		     compute_consteval_direct cst c
		   with
		       Elimconst -> EliminationFix (new_minarg,info)
		 else
		   EliminationFix (new_minarg,info)
	     | EliminationCases minarg ->
		 let new_minarg = max (minarg+n-nargs) minarg in
		 EliminationCases new_minarg)
      | IsLambda (_,t,g) when l=[] -> srec (n+1) (t::labs) g
      | IsFix fix -> check_fix_reversibility cst labs l fix
      | IsMutCase (_,_,d,_) when isRel d -> EliminationCases n
      | _ -> raise Elimconst
  in
  try srec 0 [] c
  with Elimconst -> NotAnElimination

and descend_consteval cst =
  match constant_opt_value (Global.env ()) cst with
    | None -> NotAnElimination
    | Some c -> compute_consteval cst c

let constant_eval (sp,_ as cst) =
  try
    Spmap.find sp !eval_table
  with Not_found -> begin
    let v = descend_consteval cst in
    eval_table := Spmap.add sp v !eval_table;
    v<commit_msg>Tables des eval_constant devient une Cstmap<commit_after>
(* $Id$ *)

open Pp
open Util
open Names
open Term
open Inductive
open Environ
open Reduction
open Instantiate

(************************************************************************)
(* Reduction of constant hiding fixpoints (e.g. for Simpl). The trick   *)
(* is to reuse the name of the function after reduction of the fixpoint *)

exception Elimconst
exception Redelimination

type constant_evaluation = 
  | EliminationFix of int * (constant * int * (int * constr) list * int)
  | EliminationCases of int
  | NotAnElimination

(* We use a cache registered as a global table *)


module CstOrdered =
  struct
    type t = constant
    let compare = Pervasives.compare
  end
module Cstmap = Map.Make(CstOrdered)

let eval_table = ref Cstmap.empty

type frozen = (int * constant_evaluation) Cstmap.t

let init () =
  eval_table := Cstmap.empty

let freeze () =
  !eval_table

let unfreeze ct =
  eval_table := ct

let _ = 
  Summary.declare_summary "evaluation"
    { Summary.freeze_function = freeze;
      Summary.unfreeze_function = unfreeze;
      Summary.init_function = init }


(* Check that c is an "elimination constant"
   [xn:An]..[x1:A1](<P>MutCase (Rel i) of f1..fk end g1 ..gp)
   or [xn:An]..[x1:A1](Fix(f|t) (Rel i1) ..(Rel ip)) 
    with i1..ip distinct variables not occuring in t 
   keep relevenant information ([i1,Ai1;..;ip,Aip],n,b)
   with b = true in case of a fixpoint in order to compute 
   an equivalent of Fix(f|t)[xi<-ai] as 
   [yip:Bip]..[yi1:Bi1](F bn..b1) 
   == [yip:Bip]..[yi1:Bi1](Fix(f|t)[xi<-ai] (Rel 1)..(Rel p))
   with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1] *)

let check_fix_reversibility cst labs args ((lv,i),(tys,_,bds)) =
  let n = List.length labs in
  let nargs = List.length args in
  if nargs > n then raise Elimconst;
  let nbfix = Array.length bds in
  let li =
    List.map
      (function d -> match kind_of_term d with
         | IsRel k ->
             if
	       array_for_all (noccurn k) tys
	       && array_for_all (noccurn (k+nbfix)) bds
	     then 
	       (k, List.nth labs (k-1)) 
	     else 
	       raise Elimconst
         | _ -> 
	     raise Elimconst) args
  in 
  if list_distinct (List.map fst li) then 
    EliminationFix (n-nargs+lv.(i)+1,(cst,nbfix,li,n))
  else 
    raise Elimconst

(* [compute_consteval_direct] expand all constant in a whole, but
   [compute_consteval] only one by one, until finding the one which is
   reversible (in case of a unary Fix) or the last one before the Fix
   if the latter is mutually defined *)

let compute_consteval_direct cst c =
  let rec srec n labs c =
    let c',l = whd_betadeltaeta_stack (Global.env()) Evd.empty c in
    match kind_of_term c' with
      | IsLambda (_,t,g) when l=[] -> srec (n+1) (t::labs) g
      | IsFix fix -> check_fix_reversibility cst labs l fix
      | IsMutCase (_,_,d,_) when isRel d -> EliminationCases n
      | _ -> NotAnElimination
  in srec 0 [] c

let rec compute_consteval cst c = 
  let rec srec n labs c =
    let c',l = whd_betaetalet_stack c in
    let nargs = List.length l in
    match kind_of_term c' with
      | IsConst cst2 ->
	  (match descend_consteval cst2 with
	     | NotAnElimination -> NotAnElimination
	     | EliminationFix (minarg,(_,nbfix,_,_ as info)) ->
		 (* We know that the underlying Fix must be fold by oldcst *)
		 (* We now try to fold it as cst only if nbfix=1 and n=0 *)
		 let new_minarg = max (minarg+n-nargs) minarg in
		 if nbfix=1 then
		   try
		     (* We try to name the Fix by cst *)
		     (* Complexit en n^2, bof, peut mieux faire *)
		     compute_consteval_direct cst c
		   with
		       Elimconst -> EliminationFix (new_minarg,info)
		 else
		   EliminationFix (new_minarg,info)
	     | EliminationCases minarg ->
		 let new_minarg = max (minarg+n-nargs) minarg in
		 EliminationCases new_minarg)
      | IsLambda (_,t,g) when l=[] -> srec (n+1) (t::labs) g
      | IsFix fix -> check_fix_reversibility cst labs l fix
      | IsMutCase (_,_,d,_) when isRel d -> EliminationCases n
      | _ -> raise Elimconst
  in
  try srec 0 [] c
  with Elimconst -> NotAnElimination

and descend_consteval cst =
  match constant_opt_value (Global.env ()) cst with
    | None -> NotAnElimination
    | Some c -> compute_consteval cst c

let constant_eval (sp,_ as cst) =
  try
    Cstmap.find cst !eval_table
  with Not_found -> begin
    let v = descend_consteval cst in
    eval_table := Cstmap.add cst v !eval_table;
    v
{'fraction_non_alphanumeric': 0.11809954751131221, 'fraction_numerical': 0.006787330316742082, 'mean_word_length': 2.920620842572062, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 49, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7418864', 'n_tokens_mistral': 3300, 'n_tokens_neox': 3128, 'n_words': 1013}