### Hello World in Coq

Source: https://github.com/lysxia/coq-simple-io/blob/master/README.md

A basic example demonstrating the definition of an IO unit action and its execution using the RunIO command.

```coq
From SimpleIO Require Import SimpleIO.
From Coq Require Import String.
#[local] Open Scope string_scope.

Definition main : IO unit :=
  print_endline "Hello, world!".

RunIO main.
```

--------------------------------

### RunIO Configuration and Execution

Source: https://github.com/lysxia/coq-simple-io/blob/master/README.md

Examples of configuring the RunIO command for different build systems and runtime modes.

```coq
RunIO IOMode Forward.
RunIO Builder Dune "dune".
RunIO Package "my-package".
RunIO Smart On.
```

--------------------------------

### Perform System Operations with OSys

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Provides examples for interacting with the host system, including reading environment variables, executing shell commands, measuring CPU time, and parsing command-line arguments.

```Coq
Definition env_example : IO unit :=
  result <- catch_not_found (OSys.getenv "HOME") ;;
  match result with
  | Some home =>
      print_string "HOME: " ;;
      print_endline home
  | None =>
      prerr_endline "HOME not set"
  end.

Definition run_command : IO unit :=
  exit_code <- OSys.command "echo 'Hello from shell'" ;;
  print_string "Exit code: " ;;
  print_int exit_code ;;
  print_newline.

Definition timing_example : IO unit :=
  t <- OSys.time ;;
  print_string "CPU time: " ;;
  print_string (OFloat.to_string t) ;;
  print_endline " seconds".

Definition args_example : IO unit :=
  args <- OSys.argv ;;
  print_endline "Command line arguments:" ;;
  IO.fix_io (fun loop remaining =>
    match remaining with
    | [] => IO.ret tt
    | arg :: rest =>
        print_string "  " ;;
        print_endline arg ;;
        loop rest
    end) args.
```

--------------------------------

### Unix System Operations with OUnix in Coq

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Demonstrates various low-level Unix system operations using the OUnix module. Includes getting the current time, sleeping, creating TCP clients and servers, handling errors with catch_error, and setting socket timeouts. Requires SimpleIO and Coq libraries.

```coq
From SimpleIO Require Import SimpleIO IO_Unix IO_Float.
From Coq Require Import String.
Import IO.Notations.
Local Open Scope io_scope.
#[local] Open Scope string_scope.

(* Get current time *)
Definition time_example : IO unit :=
  t <- OUnix.gettimeofday ;;
  print_string "Unix timestamp: " ;;
  print_string (OFloat.to_string t) ;;
  print_newline.

(* Sleep for specified seconds *)
Definition sleep_example : IO unit :=
  print_endline "Sleeping for 2 seconds..." ;;
  OUnix.sleep 2 ;;
  print_endline "Awake!".

(* Create TCP socket and connect *)
Definition tcp_client (host : ocaml_string) (port : int) : IO unit :=
  (* Resolve hostname *)
  addrs <- OUnix.getaddrinfo host "" [AI_FAMILY PF_INET] ;;
  match addrs with
  | [] => prerr_endline "Could not resolve hostname"
  | info :: _ ->
      (* Create socket *)
      sock <- OUnix.socket PF_INET SOCK_STREAM 0 ;;

      (* Connect to server *)
      OUnix.connect sock (ADDR_INET (inet_addr_loopback) port) ;;

      print_endline "Connected!" ;;

      (* Close socket *)
      OUnix.close sock
  end.

(* Simple TCP server *)
Definition tcp_server (port : int) : IO unit :=
  (* Create server socket *)
  server <- OUnix.socket PF_INET SOCK_STREAM 0 ;;

  (* Allow address reuse *)
  OUnix.setsockopt server SO_REUSEADDR true ;;

  (* Bind to port *)
  OUnix.bind server (ADDR_INET inet_addr_any port) ;;

  (* Listen for connections *)
  OUnix.listen server 5 ;;

  print_endline "Server listening..." ;;

  (* Accept one connection *)
  client_info <- OUnix.accept server ;;
  let (client, _addr) := client_info in

  print_endline "Client connected!" ;;

  (* Clean up *)
  OUnix.close client ;;
  OUnix.close server.

(* Handle Unix errors *)
Definition safe_connect : IO unit :=
  OUnix.catch_error (
    sock <- OUnix.socket PF_INET SOCK_STREAM 0 ;;
    OUnix.connect sock (ADDR_INET inet_addr_loopback 9999) ;;
    IO.ret tt
  ) (fun err fname param ->
    prerr_string "Unix error in " ;;
    prerr_string fname ;;
    prerr_string ": " ;;
    prerr_endline (OUnix.error_message err)
  ).

(* Set socket timeout *)
Definition socket_with_timeout : IO unit :=
  sock <- OUnix.socket PF_INET SOCK_STREAM 0 ;;
  (* Set 5 second receive timeout *)
  OUnix.Time.setsock_timeout sock SO_RCVTIMEO (OUnix.Time.Seconds 5) ;;
  OUnix.close sock.
```

--------------------------------

### Generate Pseudo-Random Numbers with ORandom

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Demonstrates how to initialize a PRNG with a seed or system time and generate random integers or booleans. It includes examples for reproducible sequences and iterative generation using IO.fix_io.

```Coq
Definition seeded_random : IO unit :=
  ORandom.init (int_of_nat 42) ;;
  n <- ORandom.int 100 ;;
  print_string "Random (0-99): " ;;
  print_int n ;;
  print_newline.

Definition system_random : IO unit :=
  ORandom.self_init tt ;;
  n <- ORandom.int 1000 ;;
  print_string "Random (0-999): " ;;
  print_int n ;;
  print_newline.

Definition coin_flip : IO unit :=
  ORandom.self_init tt ;;
  b <- ORandom.bool tt ;;
  print_endline (if b : bool then "Heads" else "Tails").

Definition roll_dice (n : nat) : IO unit :=
  ORandom.self_init tt ;;
  IO.fix_io (fun loop count =>
    match count with
    | O => IO.ret tt
    | S count' =>
        roll <- ORandom.int 6 ;;
        print_string "Roll: " ;;
        print_int (roll + 1)%int ;;
        print_newline ;;
        loop count'
    end) n.
```

--------------------------------

### Execute and configure IO programs with RunIO

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Shows how to use the RunIO command to extract and execute Coq IO actions, including configuration options for build systems and module management.

```coq
From SimpleIO Require Import SimpleIO.
From Coq Require Import String.
#[local] Open Scope string_scope.

Definition main : IO unit := print_endline "Hello, world!".
RunIO main.

Definition cat : IO unit :=
  _ <- catch_eof
    (IO.fix_io (fun f _ =>
      input <- read_line ;;
      print_endline input ;;
      f tt :> IO unit) tt) ;;
  IO.ret tt.

RunIO cat.

RunIO Builder Dune "dune".
RunIO Package "my-package".
RunIO Smart On.
```

--------------------------------

### Manage temporary files and shell safety

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Demonstrates how to generate temporary file paths, retrieve the system temporary directory, and safely quote filenames for shell command execution.

```Coq
Definition temp_file_example : IO unit := 
  temp_path <- OFilename.temp_file "myapp_" ".tmp" ;; 
  print_endline temp_path ;; 
  temp_dir <- OFilename.get_temp_dir_name ;; 
  print_endline temp_dir.
```

--------------------------------

### Define IO actions with the IO monad

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Demonstrates the core IO monad, including return, bind, sequencing, mapping, and control flow structures like fixpoint recursion and loops.

```coq
From SimpleIO Require Import SimpleIO.
Import IO.Notations.
Local Open Scope io_scope.

Definition pure_example : IO nat := IO.ret 42.

Definition bind_example : IO unit :=
  IO.bind (IO.ret "Hello") (fun msg =>
    print_endline msg).

Definition hello_world : IO unit :=
  msg <- IO.ret "Hello, World!" ;;
  print_endline msg.

Definition sequence_example : IO unit :=
  print_endline "First" ;;
  print_endline "Second" ;;
  print_endline "Third".

Definition map_example : IO int :=
  IO.map (fun n => n + 1) (IO.ret 41).

Definition countdown : int -> IO unit :=
  IO.fix_io (fun recurse n =>
    if (n <=? 0)%int then
      print_endline "Done!"
    else
      print_int n ;;
      print_newline ;;
      recurse (n - 1)%int
  ).

Definition read_until_empty : IO unit :=
  IO.while_loop (fun _ =>
    line <- read_line ;;
    if ostring_eqb line "" then
      IO.ret None
    else
      print_endline line ;;
      IO.ret (Some tt)
  ) tt.

Definition forever_print : unit -> IO unit :=
  IO.loop (fun _ =>
    print_endline "Running..." ;;
    IO.ret tt).
```

--------------------------------

### Extract and execute IO programs

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Covers multiple methods for running IO programs, including quick testing with RunIO, full extraction to OCaml files for compilation, and unsafe evaluation for interactive testing.

```Coq
Definition main_program : IO unit := 
  print_endline "Starting program..." ;; 
  args <- OSys.argv ;; 
  print_int (OString.length (OString.concat " " args)) ;; 
  print_endline "Done.".

Definition exe : io_unit := IO.unsafe_run main_program.
Separate Extraction exe.
```

--------------------------------

### Floating Point Operations with OFloat in Coq

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Illustrates basic floating-point arithmetic operations using the OFloat module. Includes addition, subtraction, multiplication, division, exponentiation, using infix notation, and parsing floats from strings. Requires SimpleIO and Coq libraries.

```coq
From SimpleIO Require Import SimpleIO IO_Float.
From Coq Require Import String.
Import IO.Notations.
Import FloatNotations.
Local Open Scope io_scope.
#[local] Open Scope string_scope.

(* Basic arithmetic *)
Definition float_arithmetic : IO unit :=
  let a := OFloat.of_int 10 in
  let b := OFloat.of_int 3 in

  (* Addition *)
  let sum := OFloat.add a b in
  print_string "10 + 3 = " ;;
  print_endline (OFloat.to_string sum) ;;

  (* Subtraction *)
  let diff := OFloat.sub a b in
  print_string "10 - 3 = " ;;
  print_endline (OFloat.to_string diff) ;;

  (* Multiplication *)
  let prod := OFloat.mul a b in
  print_string "10 * 3 = " ;;
  print_endline (OFloat.to_string prod) ;;

  (* Division *)
  let quot := OFloat.div a b in
  print_string "10 / 3 = " ;;
  print_endline (OFloat.to_string quot) ;;

  (* Exponentiation *)
  let power := OFloat.pow a b in
  print_string "10 ^ 3 = " ;;
  print_endline (OFloat.to_string power).

(* Using infix notation *)
Definition float_with_notation : IO unit :=
  let x := OFloat.of_int 5 in
  let y := OFloat.of_int 2 in
  let result := (x + y) * (x - y) in  (* (5+2)*(5-2) = 21 *)
  print_endline (OFloat.to_string result).

(* Parse float from string *)
Definition parse_float_example : IO unit :=
  match OFloat.of_string_opt "3.14159" with
  | Some pi ->
      print_string "Parsed: " ;;
      print_endline (OFloat.to_string pi)
  | None ->
      prerr_endline "Failed to parse"
  end.
```

--------------------------------

### Implement robust error handling in IO

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Shows how to use catch_any_exc and catch_sys_error to manage runtime exceptions and system errors during file operations, ensuring graceful exits.

```Coq
Definition robust_app : IO unit := 
  result <- catch_any_exc ( 
    args <- OSys.argv ;; 
    match args with 
    | [] => failwith "No arguments" 
    | _ :: filename :: _ => 
        content <- catch_sys_error (open_in filename >>= really_input_string) ;; 
        match content with 
        | Some c => print_string c 
        | None => exit 2 
        end 
    end 
  ) ;; IO.ret tt.
```

--------------------------------

### Standard Input and Output Operations in Coq

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Demonstrates printing to stdout/stderr, reading from stdin, and converting values to strings. These functions utilize the IO monad to perform side-effecting operations safely.

```coq
Definition print_examples : IO unit :=
  print_string "Hello" ;;
  print_endline " World" ;;
  print_int 42 ;;
  print_newline ;;
  print_char "A"%char ;;
  print_newline.

Definition read_examples : IO unit :=
  _ <- print_string "Enter your name: " ;;
  name <- read_line ;;
  print_string "Hello, " ;;
  print_endline name ;;
  _ <- print_string "Enter a number: " ;;
  num <- read_int ;;
  print_string "You entered: " ;;
  print_int num ;;
  print_newline.
```

--------------------------------

### File I/O Operations in Coq

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Covers reading from and writing to files, including line-by-line processing and full file reads. These operations require managing file handles and ensuring they are closed after use.

```coq
Definition write_file : IO unit :=
  handle <- open_out "output.txt" ;;
  output_string handle "Hello, File!" ;;
  output_char handle "010"%char ;;
  output_string handle "Second line" ;;
  flush handle ;;
  close_out handle.

Definition read_entire_file (filename : ocaml_string) : IO ocaml_string :=
  handle <- open_in filename ;;
  len <- in_channel_length handle ;;
  content <- really_input_string handle len ;;
  close_in handle ;;
  IO.ret content.
```

--------------------------------

### Exception Handling in Coq

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Provides wrappers to catch common OCaml exceptions like End_of_file, Sys_error, and Failure, converting them into Coq option types for safer control flow.

```coq
Definition safe_read_line : IO (option ocaml_string) :=
  catch_eof read_line.

Definition safe_open_file (path : ocaml_string) : IO (option in_channel) :=
  catch_sys_error (open_in path).

Definition safe_parse : IO unit :=
  result <- catch_failure (failwith "oops") ;;
  match result with
  | Some _ => print_endline "Success"
  | None => prerr_endline "Operation failed"
  end.
```

--------------------------------

### Manipulate file paths and names with OFilename

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Provides utilities for joining paths, extracting directory and base names, handling file extensions, and checking path properties. These functions are designed to be platform-independent within the SimpleIO framework.

```Coq
Definition path_examples : IO unit := 
  let path := OFilename.concat "/home/user" "documents" in
  print_endline path ;; 
  let dir := OFilename.dirname "/home/user/file.txt" in
  let base := OFilename.basename "/home/user/file.txt" in
  print_string "Directory: " ;; print_endline dir ;; 
  print_string "Basename: " ;; print_endline base.
```

--------------------------------

### Extracting OCaml Functions to Coq IO

Source: https://github.com/lysxia/coq-simple-io/blob/master/README.md

Demonstrates how to wrap an OCaml effectful function into a Coq IO action using the Extract Constant directive.

```coq
Parameter f : t -> u -> IO v.
Extract Constant f => "fun a b k -> k (f a b)".
```

--------------------------------

### Mutable References in Coq IO

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Demonstrates creating, reading, writing, incrementing, decrementing, and accumulating values using mutable references within the Coq IO monad. These operations allow for imperative-style state management.

```coq
From SimpleIO Require Import SimpleIO.
From Coq Require Import String.
Import IO.Notations.
Local Open Scope io_scope.
#[local] Open Scope string_scope.

(* Create, read, and write references *)
Definition ref_example : IO unit :=
  counter <- new_ref 0 ;;

  (* Read current value *)
  val <- read_ref counter ;;
  print_string "Initial: " ;;
  print_int val ;;
  print_newline ;;

  (* Write new value *)
  write_ref counter 10 ;;

  val2 <- read_ref counter ;;
  print_string "After write: " ;;
  print_int val2 ;;
  print_newline.

(* Increment and decrement integer refs *)
Definition incr_decr_example : IO unit :=
  counter <- new_ref 5 ;;

  incr_ref counter ;;
  val1 <- read_ref counter ;;
  print_int val1 ;;  (* prints 6 *)
  print_newline ;;

  decr_ref counter ;;
  decr_ref counter ;;
  val2 <- read_ref counter ;;
  print_int val2 ;;  (* prints 4 *)
  print_newline.

(* Using refs for accumulation *)
Definition sum_inputs : IO unit :=
  total <- new_ref 0 ;;
  _ <- IO.while_loop (fun _ ->
    result <- catch_eof read_line ;;
    match result with
    | None => IO.ret None
    | Some line ->
        match int_of_ostring_opt line with
        | Some n ->
            current <- read_ref total ;;
            write_ref total (current + n)%int ;;
            IO.ret (Some tt)
        | None => IO.ret (Some tt)
        end
    end) tt ;;
  final <- read_ref total ;;
  print_string "Total: " ;;
  print_int final ;;
  print_newline.
```

--------------------------------

### Bytes Operations (OBytes) in Coq

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Facilitates manipulation of mutable byte sequences (OBytes) for efficient binary data processing in Coq. Covers creation from strings, length retrieval, byte access and modification, conversion to strings, and buffer handling.

```coq
From SimpleIO Require Import SimpleIO IO_Bytes.
From Coq Require Import String.
Import IO.Notations.
Local Open Scope io_scope.
#[local] Open Scope string_scope.

(* Create and manipulate byte sequences *)
Definition bytes_example : IO unit :=
  (* Create from string *)
  buf <- OBytes.of_string "Hello" ;;

  (* Get length (pure operation) *)
  let len := OBytes.length buf in
  print_string "Length: " ;;
  print_int len ;;
  print_newline ;;

  (* Read a byte *)
  c <- OBytes.get buf 0 ;;
  print_string "First char: " ;;
  print_char c ;;
  print_newline ;;

  (* Modify a byte *)
  OBytes.set buf 0 "h"%char ;;

  (* Convert back to string *)
  result <- OBytes.to_string buf ;;
  print_endline result.  (* prints "hello" *)

(* Create uninitialized buffer *)
Definition buffer_example : IO unit :=
  buf <- OBytes.create 10 ;;
  OBytes.set buf 0 "A"%char ;;
  OBytes.set buf 1 "B"%char ;;
  OBytes.set buf 2 "C"%char ;;

  (* Extract subsequence *)
  sub_buf <- OBytes.sub buf 0 3 ;;
  result <- OBytes.to_string sub_buf ;;
  print_endline result.  (* prints "ABC" *)

(* Binary file reading *)
Definition read_binary_chunk (path : ocaml_string) (size : int) : IO bytes :=
  handle <- open_in path ;;
  buf <- OBytes.create size ;;
  _ <- input handle buf 0 size ;;
  close_in handle ;;
  IO.ret buf.
```

--------------------------------

### String Operations (OString) in Coq

Source: https://context7.com/lysxia/coq-simple-io/llms.txt

Provides operations for manipulating OCaml's native string type (OString) within Coq. Includes safe and unsafe variants for length calculation, character access, concatenation, escaping, and list conversions.

```coq
From SimpleIO Require Import SimpleIO IO_String.
From Coq Require Import String.
Import IO.Notations.
Local Open Scope io_scope.
#[local] Open Scope string_scope.

(* String length *)
Definition length_example : IO unit :=
  let s := "Hello, World!" in
  let len := OString.length s in
  print_string "Length: " ;;
  print_int len ;;
  print_newline.

(* Safe character access with bounds checking *)
Definition safe_get : IO unit :=
  let s := "Hello" in
  match OString.get_opt s 1 with
  | Some c ->
      print_string "Character at index 1: " ;;
      print_char c ;;
      print_newline
  | None ->
      prerr_endline "Index out of bounds"
  end.

(* String concatenation *)
Definition concat_example : IO unit :=
  let parts := ["Hello"; ", "; "World"; "!"] in
  let result := OString.concat "" parts in
  print_endline result.

(* Escape special characters *)
Definition escape_example : IO unit :=
  let s := "Line1
Line2\tTab" in
  print_endline (OString.escaped s).

(* Convert between string and char list *)
Definition list_conversion : IO unit :=
  let s := "ABC" in
  let chars := OString.to_list s in  (* ['A'; 'B'; 'C'] *)
  let s2 := OString.of_list chars in
  print_endline s2.

(* Unsafe operations (may throw exceptions) *)
Module UnsafeExamples.
Import OString.Unsafe.

Definition unsafe_examples : IO unit :=
  (* Direct character access - throws on out of bounds *)
  let c := get "Hello" 0 in
  print_char c ;;
  print_newline ;;

  (* Create string of repeated characters *)
  let stars := make 5 "*"%char in
  print_endline stars ;;  (* prints "*****" *)

  (* Substring extraction *)
  let substr := sub "Hello, World!" 0 5 in
  print_endline substr.  (* prints "Hello" *)

End UnsafeExamples.
```

--------------------------------

### IO Monad Interface and Notations

Source: https://github.com/lysxia/coq-simple-io/blob/master/README.md

Defines the IO type and monadic combinators including bind and notations for sequential composition.

```coq
Parameter IO : Type -> Type.

Module IO.
Parameter ret : forall {a}, a -> IO a.
Parameter bind : forall {a b}, IO a -> (a -> IO b) -> IO b.
Parameter fix_io : forall {a b}, ((a -> IO b) -> (a -> IO b)) -> a -> IO b.

Module Notations.
Notation "c >>= f" := (bind c f)
Notation "f =<< c" := (bind c f)
Notation "x <- c1 ;; c2" := (bind c1 (fun x => c2))
Notation "e1 ;; e2" := (_ <- e1%io ;; e2%io)%io
End Notations.
End IO.
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.