arbipher

[@@@warning "-32"]
(* https://discuss.ocaml.org/t/continuation-monad-with-polymorphic-return-type/6330 *)


module Cont = struct
  type ('a, 'r) cont = 'a -> 'r
  type 'a t = { cont : 'r. ('a, 'r) cont -> 'r }

  (*  'a                    'a -> 'r   'a *)
  let ret (x : 'a) = { cont = (fun k -> k x) }

arbipher

open Core

module Test_stream = struct
  let two_streams_from_list () =
    let msgs1 = List.init 3 ~f:Fn.id in
    let msgs2 = List.init 3 ~f:Fn.id in
    let s1 = Lwt_stream.of_list msgs1 in
    let s2 = Lwt_stream.of_list msgs2 in
    let s12 = product_stream s1 s2 in
    let ans = Lwt_stream.get_available s12 in

arbipher

let mk_fib fib x = if x = 0 then 0 else if x = 1 then 1 else (fib (x-2)) + (fib (x-1));;

let rec naive_fix compute e = compute (naive_fix compute) e;;
let fib = naive_fix mk_fib;;

fib 5;; (* => 5 *)

let rec naive_fix' compute = compute (naive_fix' compute);;
let fib' = naive_fix' mk_fib;; (* running forever *)

arbipher

[@@@warning "-38"]

module Id = struct
  type t = string

  let pp = Fmt.string
end

type e = ..

arbipher

open Core
open Lwt.Infix

let ( let* ) = Lwt.bind
let ( and* ) = Lwt.both

(* let seq = ref Lwt_seq.empty *)
let producer_stream, producer_pusher = Lwt_stream.create ()

let () =

arbipher

flowchart TD
    classDef alert-red fill:#f55,stroke-width:3px
    subgraph z3-source
        subgraph z3-c++-source[z3 C++ source]
            z3-src[z3 C++ code] -->|make shared-lib| z3-libz3.so[libz3.so]
            z3-src -->|make static-lib| z3-libz3.a[libz3.a]
        end
        subgraph z3-ocaml[z3 OCaml binding source]
            z3-stub[z3.ml <br /> z3native_stub.ml <br /> z3native.ml ] 
        end

arbipher

for commit in $(cat losted.txt | awk '$2 == "commit" { print $3 }'); do git cat-file -p $commit | grep SMTProver; break; done

arbipher

V "4.8.9.0"
R
C 3
= 0x55c429b82298
R
P 0x55c429b82298
C 7
= 0x55c42a5b59d8
R
P 0x55c429b82298

arbipher

open Z3

let ctx : context = mk_context []

let solver : Solver.solver = Solver.mk_solver ctx None

let intSort : Sort.sort = Arithmetic.Integer.mk_sort ctx

let boolSort : Sort.sort = Boolean.mk_sort ctx

arbipher

#require "angstrom";;
open Angstrom

type tid = string
and exp = 
  | Var of tid

  | Neg of exp
  | Int of int
  | Plus of exp * exp