<commit_before>(*i camlp4use: "q_MLast.cmo" i*)
open Term
open Environ
open Util
open Nativecode
open Nbegen
open Nbeconv
open Unix

type term = | Rel of int
            | Con of string
	    | Lam1 of (term -> term)
            | Lam2 of (term -> term -> term)
            | Lam3 of (term -> term -> term -> term)
            | Lam4 of (term -> term -> term -> term -> term)
            | Lam5 of (term -> term -> term -> term -> term -> term)
            | Lam6 of (term -> term -> term -> term -> term -> term -> term)
	    | Prod of (term * (term -> term))
	    | App of term list
            | Match of term array
	    | Set
	    | Prop
	    | Type of int
	    | Const of (int * (term array))
            | Var of int
            | Lambda of term
            | Product of term


let compile env c =
  if Sys.file_exists (nbe_name^".ml") then
    anomaly (nbe_name ^".ml already exists");
  if Sys.file_exists (env_name^".ml") then
    anomaly (env_name ^".ml already exists");
  if Sys.file_exists (terms_name^".ml") then
    anomaly (terms_name ^".ml already exists");
  let code = translate env c in
    Pcaml.input_file := "/dev/null";
    print_implem (nbe_name^".ml") nbe_implem; 
    let dump = dump_env [c] env in
    print_implem (env_name^".ml") (compute_loc dump);
    print_implem (terms_name^".ml")
	 [(<:str_item< open $list: [nbe_name]$ >>, loc);
	  (<:str_item< open $list: [env_name]$ >>, loc);
	  (<:str_item< value c = $code$ >>, loc);
	  (<:str_item< value _ = print_nf c >>, loc)]

let rec rebuild_constr n t ty =
  match t with
    | Set -> mkSet
    | Prop -> mkProp
    | Lambda -> mkLambda Anonymous (rebuild)
    | _ -> assert false

let native_norm env c ty =
  let _ = compile (pre_env env) c in
  let file_names = nbe_name^".ml "^env_name^".ml "^terms_name^".ml" in
  let _ = Unix.system ("touch "^env_name^".ml") in
  print_endline "Compilation...";
  let res = Unix.system ("time ocamlopt.opt "^file_names) in
  let _ = Unix.system ("rm "^file_names) in
  match res with
    | Unix.WEXITED 0 ->
      begin
      print_endline "Normalizing...";
      let ch_in = open_process_in "./a.out" in
      let nf = Marshal.from_channel ch_in in
      (*let (fd_in,fd_out) = Unix.pipe() in
      match Unix.fork() with
        | 0 ->
          dup2 fd_out strdout;
          close fd_in;
          execvp "a.out"
        | _ ->
          close fd_out;
          let nf = Narshal.from_channel *)
      match nf with
        | Set ->
           mkSet
        | _ ->
           mkProp
(*      match Unix.system "time ./a.out; rm a.out" with
        | Unix.WEXITED 0 -> cu
        | _ -> (print_endline "Conversion test failure"; raise NotConvertible)*)
      end
    | _ -> anomaly "Compilation failure" 
<commit_msg>First steps towards normalization.<commit_after>(*i camlp4use: "q_MLast.cmo" i*)
open Term
open Environ
open Reduction
open Util
open Nativecode
open Nbegen
open Nbeconv
open Unix

type term = | Rel of int
            | Con of string
	    | Lam1 of (term -> term)
            | Lam2 of (term -> term -> term)
            | Lam3 of (term -> term -> term -> term)
            | Lam4 of (term -> term -> term -> term -> term)
            | Lam5 of (term -> term -> term -> term -> term -> term)
            | Lam6 of (term -> term -> term -> term -> term -> term -> term)
	    | Prod of (term * (term -> term))
	    | App of term list
            | Match of term array
	    | Set
	    | Prop
	    | Type of int
	    | Const of (int * (term array))
            | Var of int
            | Lambda of term
            | Product of term


let compile env c =
  if Sys.file_exists (nbe_name^".ml") then
    anomaly (nbe_name ^".ml already exists");
  if Sys.file_exists (env_name^".ml") then
    anomaly (env_name ^".ml already exists");
  if Sys.file_exists (terms_name^".ml") then
    anomaly (terms_name ^".ml already exists");
  let code = translate env c in
    Pcaml.input_file := "/dev/null";
    print_implem (nbe_name^".ml") nbe_implem; 
    let dump = dump_env [c] env in
    print_implem (env_name^".ml") (compute_loc dump);
    print_implem (terms_name^".ml")
	 [(<:str_item< open $list: [nbe_name]$ >>, loc);
	  (<:str_item< open $list: [env_name]$ >>, loc);
	  (<:str_item< value c = $code$ >>, loc);
	  (<:str_item< value _ = print_nf c >>, loc)]

let rec rebuild_constr n env t ty =
  match t with
    | Set -> mkSet
    | Prop -> mkProp
    | Type u -> mkType u
    | Lambda st ->
        let ty_whd = whd_betadeltaiota env ty in
        let (name,dom,codom as res) = destProd ty_whd in
        mkLambda (name,dom,rebuild_constr (n+1) env st codom)
    | Rel i -> mkRel (i+1)
    | _ -> assert false

let native_norm env c ty =
  let _ = compile (pre_env env) c in
  let file_names = nbe_name^".ml "^env_name^".ml "^terms_name^".ml" in
  let _ = Unix.system ("touch "^env_name^".ml") in
  print_endline "Compilation...";
  let res = Unix.system ("time ocamlopt.opt "^file_names) in
  let _ = Unix.system ("rm "^file_names) in
  match res with
    | Unix.WEXITED 0 ->
      print_endline "Normalizing...";
      let ch_in = open_process_in "./a.out" in
      let nf = Marshal.from_channel ch_in in
        rebuild_constr 0 env nf ty
    | _ -> anomaly "Compilation failure" 

{'fraction_non_alphanumeric': 0.1350316031411607, 'fraction_numerical': 0.004213752154759625, 'mean_word_length': 2.1841463414634146, 'pattern_counts': {'":': 0, '<': 19, '<?xml version=': 0, '>': 83, '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': '4117201', 'n_tokens_mistral': 1873, 'n_tokens_neox': 1777, 'n_words': 572}