<commit_before>(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    <NAME>                                                      *)
(*    <NAME>                                           *)
(*    <NAME>                                                      *)
(*    <NAME>                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Format
open Theory

let files = ref []
let parse_only = ref false
let type_only = ref false
let debug = ref false
let loadpath = ref []
let print_stdout = ref false
let simplify_recursive = ref false
let inlining = ref false
let transform = ref false
let alt_ergo = ref false

let () = 
  Arg.parse 
    ["--parse-only", Arg.Set parse_only, "stops after parsing";
     "--type-only", Arg.Set type_only, "stops after type-checking";
     "--debug", Arg.Set debug, "sets the debug flag";
     "-I", Arg.String (fun s -> loadpath := s :: !loadpath), 
       "<dir>  adds dir to the loadpath";
     "--print-stdout", Arg.Set print_stdout, "print the results to stdout";
     "--simplify-recursive", Arg.Set simplify_recursive, "simplify recursive definition";
     "--inline", Arg.Set inlining, "inline the definition not recursive";
     "--transform", Arg.Set transform, "transform the goal (--inline,and --simplify-recursive set it) ";
     "--alt-ergo", Arg.Set alt_ergo, "output for Alt-Ergo on stdout";
    ]
    (fun f -> files := f :: !files)
    "usage: why [options] files..."

let in_emacs = Sys.getenv "TERM" = "dumb"
let transform = !transform || !simplify_recursive || !inlining

let rec report fmt = function
  | Lexer.Error e ->
      fprintf fmt "lexical error: %a" Lexer.report e;
  | Loc.Located (loc, e) ->
      fprintf fmt "%a%a" Loc.report_position loc report e
  | Parsing.Parse_error ->
      fprintf fmt "syntax error"
  | Typing.Error e ->
      Typing.report fmt e
  | Context.UnknownIdent i ->
      fprintf fmt "anomaly: unknownident %s" i.Ident.id_short
  | e ->
      if in_emacs then
        let dir = Filename.dirname (Filename.dirname Sys.executable_name) in
        fprintf fmt "Entering directory `%s'@\n" dir; 
        fprintf fmt "anomaly:@\n%s" (Printexc.to_string e)
      else 
        fprintf fmt "anomaly: %s" (Printexc.to_string e)
let type_file env file =
  let c = open_in file in
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
  let f = Lexer.parse_logic_file lb in 
  close_in c;
  if !parse_only then env else Typing.add_theories env f

let extract_goals th =
  let ctx = Context.use_export Context.empty_context th in
  assert false

let transform l =
  let l = Typing.list_theory l in
  if !print_stdout && not transform then 
    List.iter (Pretty.print_theory Format.std_formatter) l
  else if !alt_ergo then match l with
    | th :: _ -> begin match extract_goals th with
	| g :: _ -> Alt_ergo.print_goal std_formatter g
	| [] -> ()
      end	
    | [] -> ()
  else 
    let l = List.map (fun t -> t,Transform.apply Flatten.t t.th_ctxt)
      l in
    let l = if !simplify_recursive 
    then 
      List.map (fun (t,dl) -> t,Transform.apply 
                  Simplify_recursive_definition.t dl) l
    else l in
    let l = if !inlining<commit_msg>ne fait aucune transformation si aucune n'a été demandé<commit_after>(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    <NAME>                                                      *)
(*    <NAME>                                           *)
(*    <NAME>                                                      *)
(*    <NAME>                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Format
open Theory

let files = ref []
let parse_only = ref false
let type_only = ref false
let debug = ref false
let loadpath = ref []
let print_stdout = ref false
let simplify_recursive = ref false
let inlining = ref false
let alt_ergo = ref false

let () = 
  Arg.parse 
    ["--parse-only", Arg.Set parse_only, "stops after parsing";
     "--type-only", Arg.Set type_only, "stops after type-checking";
     "--debug", Arg.Set debug, "sets the debug flag";
     "-I", Arg.String (fun s -> loadpath := s :: !loadpath), 
       "<dir>  adds dir to the loadpath";
     "--print-stdout", Arg.Set print_stdout, "print the results to stdout";
     "--simplify-recursive", Arg.Set simplify_recursive, "simplify recursive definition";
     "--inline", Arg.Set inlining, "inline the definition not recursive";
     "--alt-ergo", Arg.Set alt_ergo, "output for Alt-Ergo on stdout";
    ]
    (fun f -> files := f :: !files)
    "usage: why [options] files..."

let in_emacs = Sys.getenv "TERM" = "dumb"
let transform = !simplify_recursive || !inlining

let rec report fmt = function
  | Lexer.Error e ->
      fprintf fmt "lexical error: %a" Lexer.report e;
  | Loc.Located (loc, e) ->
      fprintf fmt "%a%a" Loc.report_position loc report e
  | Parsing.Parse_error ->
      fprintf fmt "syntax error"
  | Typing.Error e ->
      Typing.report fmt e
  | Context.UnknownIdent i ->
      fprintf fmt "anomaly: unknownident %s" i.Ident.id_short
  | e ->
      if in_emacs then
        let dir = Filename.dirname (Filename.dirname Sys.executable_name) in
        fprintf fmt "Entering directory `%s'@\n" dir; 
        fprintf fmt "anomaly:@\n%s" (Printexc.to_string e)
      else 
        fprintf fmt "anomaly: %s" (Printexc.to_string e)
let type_file env file =
  let c = open_in file in
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
  let f = Lexer.parse_logic_file lb in 
  close_in c;
  if !parse_only then env else Typing.add_theories env f

let extract_goals th =
  let ctx = Context.use_export Context.empty_context th in
  assert false

let transform l =
  let l = Typing.list_theory l in
  if !print_stdout && not transform then 
    List.iter (Pretty.print_theory Format.std_formatter) l
  else if !alt_ergo then match l with
    | th :: _ -> begin match extract_goals th with
	| g :: _ -> Alt_ergo.print_goal std_formatter g
	| [] -> ()
      end	
    | [] -> ()
  else if transform then
    let l = List.map (fun t -> t,Transform.apply Flatten.t t.th_ctxt)
      l in
    let l = if !simplify_recursive 
    then 
      List.map (fun (t,dl) -> t,Transform.apply 
                  Simplify_recursive_definition.t dl) l
    else l in
    let l = if !inlining
{'fraction_non_alphanumeric': 0.13274443368828653, 'fraction_numerical': 0.001452081316553727, 'mean_word_length': 1.7697721179624666, 'pattern_counts': {'":': 0, '<': 13, '<?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': 48, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7075021', 'n_tokens_mistral': 2282, 'n_tokens_neox': 2180, 'n_words': 763}