[ocaml] include CmdLiner package example

coq/third-party/coqeal-mat-seq.v

@@ -0,0 +1,72 @@
+(* From mathcomp Require Import ssralg. *)
+(* From mathcomp.algebra Require Import matrix. *)
+From mathcomp Require Import all_ssreflect all_algebra.
+
+(* https://github.com/coq-community/coqeal/tree/1.1.3 *)
+
+
+Local Open Scope ring_scope.
+
+Definition egmat: 'M[bool]_3 := \matrix_(i<3, j<3) (true).
+
+
+From CoqEAL Require Import hrel param refinements trivial_seq.
+From CoqEAL.refinements Require Import seqmx.
+
+Check fun_of_matrix egmat.
+Check mkseqmx_ord.
+(*
+mkseqmx_ord
+     : forall (A : Type) (m n : nat), ('I_m -> 'I_n -> A) -> seqmx
+*)
+Definition egseq := mkseqmx_ord (fun_of_matrix egmat).
+Print egseq.
+
+Require Import Extraction.
+Extraction Language Haskell.         
+Require Import ExtrHaskellBasic.     
+Require Import ExtrHaskellZInteger.
+Require Import ExtrHaskellNatNum.
+Require Import ExtrHaskellString.
+
+Recursive Extraction eqseq.
+Definition eglst: list bool := cons true (cons false (cons true nil)).
+Recursive Extraction eglst.
+(*
+eglst :: ([]) Prelude.Bool
+eglst =
+  (:) Prelude.True ((:) Prelude.False ((:) Prelude.True ([]))) *)
+
+Check (0 : 'M[int]_(2,2)).
+
+Goal ((0 : 'M[int]_(2,2)) == (const_mx 0)).
+  (* by coqeal (1* didn't work *1) *)
+  rewrite /const_mx //.
+Qed.
+
+Search mkseqmx_ord.
+Check nat_Rxx.
+Print nat_R.
+Check refines.
+Check refine_mkseqmx_ord id 3 3.
+Check Refinements.Op.zero_of bool.
+Print Refinements.Op.zero_of.
+
+Goal ((0 : 'M[int]_(2,2)) == 0).
+  by rewrite /const_mx.
+Qed.
+
+Goal (Mp *m 0 == 0 :> 'M[_]_(2,2)).
+Locate "*m".
+  Check mulmx.
+  rewrite /mulmx //.
+  vm_compute.
+  by coqeal.
+Abort.
+
+(* [coqeal] tactic is defined as:
+
+```
+Ltac coqeal := apply: refines_goal; vm_compute.
+```
+ *)

ocaml/cmdlinerEg/bin/dune

@@ -0,0 +1,4 @@
+(executable
+ (public_name cmdlinerEg)
+ (name main)
+ (libraries cmdlinerEg cmdliner))

ocaml/cmdlinerEg/bin/main.ml

@@ -0,0 +1,56 @@
+open Cmdliner
+
+(*
+let cmd =
+  let doc = "An observability tool for OCaml programs" in
+*)
+
+
+(*
+let gc_stats_cmd =
+  let man =
+    [
+      `S Manpage.s_description;
+      `P "Report the GC latency profile.";
+      `Blocks help_secs;
+    ]
+  in
+*)
+
+(*
+  let doc = "Report the GC latency profile and stats." in
+  let man = [
+    `S Manpage.s_description;
+  ] in
+  let info = Cmd.info "gc-stats" ~doc ~sdocs ~man in
+  Cmd.v info Term.(const gc_stats $ json_option $ output_option $ exec_args 0)
+in
+*)
+
+(* let revolt () = print_endline "Revolt!" *)
+(* let revolt_t = Term.(const revolt $ const ()) *)
+
+(* let cmd = Cmd.v (Cmd.info "revol") revolt_t *)
+
+(* let main () = exit (Cmd.eval cmd) *)
+(* let () = main () *)
+
+let revolt () = print_endline "Revolt!"
+let revolt_t = Term.(const revolt $ const ())
+
+let cmd =
+  let doc = "main docstring" in
+  let man = [
+    `S Manpage.s_bugs;
+    `P "bug section descr";
+    `I ("Wall time", "Real execution time of the program");
+    `I ("CPU time", "Total CPU time across all domains");
+    `I ("GC time", "Total time spent by the program performing garbage collection (major and minor)");
+    `I ("GC overhead", "Percentage of time taken up by GC against the total execution time");
+    `I ("GC time per domain", "Time spent by every domain performing garbage collection (major and minor cycles). Domains are reported with their domain ID (e.g. `Domain0`)");
+    `I ("GC latency profile", "Mean, standard deviation and percentile latency profile of GC events.")] in
+  let info = Cmd.info "cmdname-info" ~version:"0.0.1" ~doc ~man in
+  Cmd.v info revolt_t
+
+let main () = exit (Cmd.eval cmd)
+let () = main ()

ocaml/cmdlinerEg/cmdlinerEg.opam

@@ -0,0 +1,22 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+depends: [
+  "ocaml"
+  "cmdliner"
+  "dune" {>= "3.7" & with-test}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]

ocaml/cmdlinerEg/dune-project

@@ -0,0 +1,14 @@
+(lang dune 3.7)
+
+(name cmdlinerEg)
+
+(generate_opam_files true)
+
+(package
+  (name cmdlinerEg)
+  (depends
+    ocaml
+    cmdliner
+    (dune :with-test)))
+
+; See the complete stanza docs at https://dune.readthedocs.io/en/stable/dune-files.html#dune-project

ocaml/cmdlinerEg/lib/dune

@@ -0,0 +1,2 @@
+(library
+ (name cmdlinerEg))

ocaml/cmdlinerEg/test/dune

@@ -0,0 +1,2 @@
+(test
+ (name cmdlinerEg))