<commit_before>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Created by <NAME>, Aug 2002 as part of the implementation of
   the Coq module system *)

(* This module provides the main entry points for type-checking basic
   declarations *)

open Errors
open Util
open Names
open Univ
open Term
open Context
open Declarations
open Environ
open Entries
open Typeops

let debug = false
let prerr_endline =
  if debug then prerr_endline else fun _ -> ()

let constrain_type env j cst1 = function
  | None ->
      make_polymorphic_if_constant_for_ind env j, cst1
  | Some t ->
      let (tj,cst2) = infer_type env t in
      let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
      assert (eq_constr t tj.utj_val);
      let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
      NonPolymorphicType t, cstrs


let translate_local_assum env t =
  let (j,cst) = infer env t in
  let t = Typeops.assumption_of_judgment env j in
    (t,cst)


(* Insertion of constants and parameters in environment. *)

let handle_side_effects env body side_eff =
  let handle_sideff t (NewConstant (c,cb)) =
    let cname = 
      let name = string_of_con c in
      for i = 0 to String.length name - 1 do
        if name.[i] = '.' || name.[i] = '#' then name.[i] <- '_' done;
      Name (id_of_string name) in
    let rec sub i x = match kind_of_term x with
      | Const c' when eq_constant c c' -> mkRel i
      | _ -> map_constr_with_binders ((+) 1) sub i x in
    match cb.const_body with
    | Undef _ -> assert false
    | Def b ->
        let b = Lazyconstr.force b in
        let b_ty = Typeops.type_of_constant_type env cb.const_type in
        let t = sub 1 (Vars.lift 1 t) in
        mkLetIn (cname, b, b_ty, t)
    | OpaqueDef b -> 
        let b = Lazyconstr.force_opaque (Future.force b) in
        let b_ty = Typeops.type_of_constant_type env cb.const_type in
        let t = sub 1 (Vars.lift 1 t) in
        mkApp (mkLambda (cname, b_ty, t), [|b|])
  in
  (* CAVEAT: we assure a proper order *)
  Declareops.fold_side_effects handle_sideff body
    (Declareops.uniquize_side_effects side_eff)

(* what is used for debugging only *)
let infer_declaration ?(what="UNKNOWN") env dcl =
  match dcl with
  | DefinitionEntry c ->
      let ctx, entry_body = c.const_entry_secctx, c.const_entry_body in
      if c.const_entry_opaque && c.const_entry_type <> None then
        let _ = prerr_endline ("deferring typing of "^what) in
        let body_cst = Future.chain ~id:("infer_declaration " ^ what)
            entry_body (fun entry_body ->
          let _ = prerr_endline ("forcing deferred typing of "^what) in
          let body, side_eff = entry_body in
          let _ = prerr_endline ("... got proof of "^what) in
          let body = if side_eff = Declareops.no_seff then body else
            let _ = prerr_endline ("    Handling the following side eff:") in
            Declareops.iter_side_effects (fun e -> 
              prerr_endline("     " ^ Declareops.string_of_side_effect e)) 
              side_eff;
            handle_side_effects env body side_eff in
          let (j,cst) = infer env body in
          let _ = prerr_endline ("... typed proof of "^what) in
          let j =
            {uj_val = hcons_constr j.uj_val;
             uj_type = hcons_constr j.uj_type} in
          let (_typ,cst) = constrain_type env j cst c.const_entry_type in
          Lazyconstr.opaque_from_val j.uj_val, cst) in
        let body, cst = Future.split2 body_cst in
        let def = OpaqueDef body in
        let typ = match c.const_entry_type with
        | None -> assert false
        | Some typ -> NonPolymorphicType typ in
        (def, typ, cst, c.const_entry_inline_code, ctx)
      else
        let _ = prerr_endline ("typing now "^what) in
        let body, side_eff = Future.force entry_body in
        let body = if side_eff = Declareops.no_seff then body else
          let _ = prerr_endline ("    Handling the following side eff:") in
          Declareops.iter_side_effects (fun e -> 
            prerr_endline("     " ^ Declareops.string_of_side_effect e))
            side_eff;
          handle_side_effects env body side_eff in
        let (j,cst) =
          try infer env body 
          with Not_found as e -> 
            prerr_endline ("infer not found " ^ what);
            raise e in
        let j =
          {uj_val = hcons_constr j.uj_val;
           uj_type = hcons_constr j.uj_type} in
        let (typ,cst) = constrain_type env j cst c.const_entry_type in
        let _ = prerr_endline ("...typed "^what) in
        let def = Def (Lazyconstr.from_val j.uj_val) in
        (def, typ, Future.from_val cst, c.const_entry_inline_code, ctx)
  | ParameterEntry (ctx,t,nl) ->
      let (j,cst) = infer env t in
      let t = hcons_constr (Typeops.assumption_of_judgment env j) in
      Undef nl, NonPolymorphicType t, Future.from_val cst, false, ctx

let global_vars_set_constant_type env = function
  | NonPolymorphicType t -> global_vars_set env t
  | PolymorphicArity (ctx,_) -><commit_msg>Cleanup code in term_typing<commit_after>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Created by <NAME>, Aug 2002 as part of the implementation of
   the Coq module system *)

(* This module provides the main entry points for type-checking basic
   declarations *)

open Errors
open Util
open Names
open Univ
open Term
open Context
open Declarations
open Environ
open Entries
open Typeops

let debug = false
let prerr_endline =
  if debug then prerr_endline else fun _ -> ()

let constrain_type env j cst1 = function
  | None ->
      make_polymorphic_if_constant_for_ind env j, cst1
  | Some t ->
      let (tj,cst2) = infer_type env t in
      let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
      assert (eq_constr t tj.utj_val);
      let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
      NonPolymorphicType t, cstrs


let translate_local_assum env t =
  let (j,cst) = infer env t in
  let t = Typeops.assumption_of_judgment env j in
    (t,cst)


(* Insertion of constants and parameters in environment. *)

let handle_side_effects env body side_eff =
  let handle_sideff t (NewConstant (c,cb)) =
    let cname = 
      let name = string_of_con c in
      for i = 0 to String.length name - 1 do
        if name.[i] = '.' || name.[i] = '#' then name.[i] <- '_' done;
      Name (id_of_string name) in
    let rec sub i x = match kind_of_term x with
      | Const c' when eq_constant c c' -> mkRel i
      | _ -> map_constr_with_binders ((+) 1) sub i x in
    match cb.const_body with
    | Undef _ -> assert false
    | Def b ->
        let b = Lazyconstr.force b in
        let b_ty = Typeops.type_of_constant_type env cb.const_type in
        let t = sub 1 (Vars.lift 1 t) in
        mkLetIn (cname, b, b_ty, t)
    | OpaqueDef b -> 
        let b = Lazyconstr.force_opaque (Future.force b) in
        let b_ty = Typeops.type_of_constant_type env cb.const_type in
        let t = sub 1 (Vars.lift 1 t) in
        mkApp (mkLambda (cname, b_ty, t), [|b|])
  in
  (* CAVEAT: we assure a proper order *)
  Declareops.fold_side_effects handle_sideff body
    (Declareops.uniquize_side_effects side_eff)

(* what is used for debugging only *)
let infer_declaration ?(what="UNKNOWN") env dcl =
  match dcl with
  | DefinitionEntry c ->
      let ctx, entry_body = c.const_entry_secctx, c.const_entry_body in
      if c.const_entry_opaque && c.const_entry_type <> None then
        let id = "infer_declaration " ^ what in
        let body_cst =
          Future.chain ~id entry_body (fun (body, side_eff) ->
            let body = handle_side_effects env body side_eff in
            let j, cst = infer env body in
            let j =
              {uj_val = hcons_constr j.uj_val;
               uj_type = hcons_constr j.uj_type} in
            let _typ, cst = constrain_type env j cst c.const_entry_type in
            Lazyconstr.opaque_from_val j.uj_val, cst) in
        let body, cst = Future.split2 body_cst in
        let def = OpaqueDef body in
        let typ = match c.const_entry_type with
        | None -> assert false
        | Some typ -> NonPolymorphicType typ in
        def, typ, cst, c.const_entry_inline_code, ctx
      else
        let body, side_eff = Future.force entry_body in
        let body = handle_side_effects env body side_eff in
        let j, cst =
          try infer env body 
          with Not_found as e -> 
            prerr_endline ("infer not found " ^ what);
            raise e in
        let j =
          {uj_val = hcons_constr j.uj_val;
           uj_type = hcons_constr j.uj_type} in
        let typ, cst = constrain_type env j cst c.const_entry_type in
        let def = Def (Lazyconstr.from_val j.uj_val) in
        def, typ, Future.from_val cst, c.const_entry_inline_code, ctx
  | ParameterEntry (ctx,t,nl) ->
      let j, cst = infer env t in
      let t = hcons_constr (Typeops.assumption_of_judgment env j) in
      Undef nl, NonPolymorphicType t, Future.from_val cst, false, ctx

let global_vars_set_constant_type env = function
  | NonPolymorphicType t -> global_vars_set env t
  | PolymorphicArity (ctx,_) ->
{'fraction_non_alphanumeric': 0.11964285714285715, 'fraction_numerical': 0.005753968253968254, 'mean_word_length': 2.496704821366632, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 41, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7209605', 'n_tokens_mistral': 3363, 'n_tokens_neox': 3219, 'n_words': 1062}