<commit_before>(* ========================================================================= *)
(* ARTICLES OF PROOFS IN HIGHER ORDER LOGIC                                  *)
(* Copyright (c) 2004 <NAME>, distributed under the GNU GPL version 2      *)
(* ========================================================================= *)

structure Article :> Article =
struct

open Useful;

(* ------------------------------------------------------------------------- *)
(* Constants.                                                                *)
(* ------------------------------------------------------------------------- *)

val fileExtension = "art";

(* ------------------------------------------------------------------------- *)
(* Article filenames.                                                        *)
(* ------------------------------------------------------------------------- *)

fun isFilename {filename} =
    case OS.Path.ext (OS.Path.file filename) of
      SOME ext => ext = fileExtension
    | NONE => false;

fun normalizeFilename {filename} =
    let
      val filename =
          OS.Path.joinBaseExt
            {base = OS.Path.base (OS.Path.file filename),
             ext = SOME fileExtension}
    in
      {filename = filename}
    end;

(* ------------------------------------------------------------------------- *)
(* A type of proof articles.                                                 *)
(* ------------------------------------------------------------------------- *)

datatype article =
    Article of
      {savable : bool,
       thms : ObjectThms.thms};

val empty =
    let
      val savable = true
      and thms = ObjectThms.empty
    in
      Article
        {savable = savable,
         thms = thms}
    end;

fun savable (Article {savable = x, ...}) = x;

fun objects (Article {thms = x, ...}) = x;

fun thms art = ObjectThms.thms (objects art);

(* ------------------------------------------------------------------------- *)
(* Merging articles.                                                         *)
(* ------------------------------------------------------------------------- *)

fun union art1 art2 =
    let
      val Article {savable = sav1, thms = ths1} = art1
      and Article {savable = sav2, thms = ths2} = art2

      val savable = sav1 andalso sav2

      val thms = ObjectThms.union ths1 ths2
    in
      Article
        {savable = savable,
         thms = thms}
    end;

local
  fun add (art2,art1) = union art1 art2;
in
  fun unionList arts =
      case arts of
        [] => empty
      | art :: arts => List.foldl add art arts;
end;

(* ------------------------------------------------------------------------- *)
(* Input/Output.                                                             *)
(* ------------------------------------------------------------------------- *)

fun fromTextFile {savable,import,interpretation,filename} =
    let
      val Article {savable = importSavable, thms = importThms} = import

      val _ = not savable orelse importSavable orelse
              raise Error "savable article cannot use unsavable import"

      val parameters =
          {import = importThms,
           interpretation = interpretation,
           savable = savable}

      val state = ObjectRead.initial parameters

      val state = ObjectRead.executeTextFile {filename = filename} state

      val stack = ObjectRead.stack state
      and dict = ObjectRead.dict state
      and exp = ObjectRead.export state

      val () =
          let
            val n = ObjectStack.size stack
          in
            if n = 0 then ()
            else
              warn (Int.toString n ^ " object" ^
                    (if n = 1 then "" else "s") ^
                    " left on the stack by " ^ filename)
          end

      val () =
          let
            val n = ObjectDict.size dict
          in
            if n = 0 then ()
            else
              warn (Int.toString n ^ " object" ^
                    (if n = 1 then "" else "s") ^
                    " left in the dictionary by " ^ filename)
          end

      val thms = ObjectThms.fromExport exp
    in
      Article
        {savable = savable,
         thms = thms}
    end
(*OpenTheoryDebug
    handle Error err => raise Error ("Article.fromTextFile: " ^ err);
*)

fun toTextFile {article,filename} =
    let
      val Article {savable,thms} = article

      val _ = savable orelse raise Error "unsavable"<commit_msg>Prettiness tweak<commit_after>(* ========================================================================= *)
(* ARTICLES OF PROOFS IN HIGHER ORDER LOGIC                                  *)
(* Copyright (c) 2004 <NAME>, distributed under the GNU GPL version 2      *)
(* ========================================================================= *)

structure Article :> Article =
struct

open Useful;

(* ------------------------------------------------------------------------- *)
(* Constants.                                                                *)
(* ------------------------------------------------------------------------- *)

val fileExtension = "art";

(* ------------------------------------------------------------------------- *)
(* Article filenames.                                                        *)
(* ------------------------------------------------------------------------- *)

fun isFilename {filename} =
    case OS.Path.ext (OS.Path.file filename) of
      SOME ext => ext = fileExtension
    | NONE => false;

fun normalizeFilename {filename} =
    let
      val filename =
          OS.Path.joinBaseExt
            {base = OS.Path.base (OS.Path.file filename),
             ext = SOME fileExtension}
    in
      {filename = filename}
    end;

(* ------------------------------------------------------------------------- *)
(* A type of proof articles.                                                 *)
(* ------------------------------------------------------------------------- *)

datatype article =
    Article of
      {savable : bool,
       thms : ObjectThms.thms};

val empty =
    let
      val savable = true
      and thms = ObjectThms.empty
    in
      Article
        {savable = savable,
         thms = thms}
    end;

fun savable (Article {savable = x, ...}) = x;

fun objects (Article {thms = x, ...}) = x;

fun thms art = ObjectThms.thms (objects art);

(* ------------------------------------------------------------------------- *)
(* Merging articles.                                                         *)
(* ------------------------------------------------------------------------- *)

fun union art1 art2 =
    let
      val Article {savable = sav1, thms = ths1} = art1
      and Article {savable = sav2, thms = ths2} = art2

      val savable = sav1 andalso sav2

      val thms = ObjectThms.union ths1 ths2
    in
      Article
        {savable = savable,
         thms = thms}
    end;

local
  fun add (art2,art1) = union art1 art2;
in
  fun unionList arts =
      case arts of
        [] => empty
      | art :: arts => List.foldl add art arts;
end;

(* ------------------------------------------------------------------------- *)
(* Input/Output.                                                             *)
(* ------------------------------------------------------------------------- *)

fun fromTextFile {savable,import,interpretation,filename} =
    let
      val Article {savable = importSavable, thms = importThms} = import

      val _ = not savable orelse importSavable orelse
              raise Error "savable article cannot use unsavable import"

      val parameters =
          {import = importThms,
           interpretation = interpretation,
           savable = savable}

      val state = ObjectRead.initial parameters

      val state = ObjectRead.executeTextFile {filename = filename} state

      val stack = ObjectRead.stack state
      and dict = ObjectRead.dict state
      and exp = ObjectRead.export state

      val () =
          let
            val n = ObjectStack.size stack
          in
            if n = 0 then ()
            else
              warn (Print.toString Print.ppPrettyInt n ^ " object" ^
                    (if n = 1 then "" else "s") ^
                    " left on the stack by " ^ filename)
          end

      val () =
          let
            val n = ObjectDict.size dict
          in
            if n = 0 then ()
            else
              warn (Print.toString Print.ppPrettyInt n ^ " object" ^
                    (if n = 1 then "" else "s") ^
                    " left in the dictionary by " ^ filename)
          end

      val thms = ObjectThms.fromExport exp
    in
      Article
        {savable = savable,
         thms = thms}
    end
(*OpenTheoryDebug
    handle Error err => raise Error ("Article.fromTextFile: " ^ err);
*)

fun toTextFile {article,filename} =
    let
      val Article {savable,thms} = article

      val _ = savable orelse raise Error "unsavable"
{'fraction_non_alphanumeric': 0.2711977715877437, 'fraction_numerical': 0.005571030640668524, 'mean_word_length': 1.02710027100271, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 17, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 22, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3573757', 'n_tokens_mistral': 2111, 'n_tokens_neox': 2003, 'n_words': 638}