Kakadu

➜  gt-ppx git:(dune) ✗ mkcamlp5 -custom str.cmi str.cma -cclib -lstr -o camlp5str
don't know what to do with 
Usage: ocamlc <options> <files>
Options are:
  -a  Build a library
  -alert <list>  Enable or disable alerts according to <list>:
        +<alertname>  enable alert <alertname>
        -<alertname>  disable alert <alertname>
        ++<alertname> treat <alertname> as fatal error
        --<alertname> treat <alertname> as non-fatal

Kakadu

➜  dune-ocaml-ppx-bug git:(master) dune runtest 
     patdiff (internal) (exit 1)
(cd _build/default && /home/kakadu/.opam/4.09.0+fp+flambda/bin/patdiff -keep-whitespace -location-style omake -unrefined test_inline_test.ml test_inline_test.ml.corrected)
------ test_inline_test.ml
++++++ test_inline_test.ml.corrected
File "test_inline_test.ml", line 6, characters 0-1:
 |
 |let rec fact n = if n = 1 then 1 else n * fact (n - 1)
 |
 |let%expect_test _ =

Kakadu

#use "topfind";;
#rectypes;;
#require "GT";;
#require "GT.ppx";;

type lambda =
    | Lambda of string * lambda
    | Var of string
    | Apply of lambda * lambda
    [@@deriving gt]

Kakadu

➜  pat-match git:(master) ✗ make unn
dune exec unn/main_unnested.exe 
test1 eval_m, 1 answer {
         0ms
q=("pair" [aab; bbb], ["pair"]);
}
test1 eval_m, 1 answer {
         0ms
q=(aab, ["aab"]);
}

Kakadu

    let rec list_mem x xs (q178 as ans) =
      let open Std in
      conde
        [ ((xs === (nil ())) &&& (q178 === (!! false)))
        ; fresh (h tl q181)
           (xs === (h % tl))
           (conde
             [ (x === h) &&& (q178 === (!! true))
             ; (x =/= h) &&& (list_mem x tl q178)
             ])

Kakadu

# 8.46 lsp - debug (local)
recv: {
  "id": "{3591cc33-d1d0-44f9-8fce-ffb493f36b1c}",
  "jsonrpc": "2.0",
  "method": "textDocument/documentHighlight",
  "params": {
    "position": { "character": 0, "line": 3 },
    "textDocument": {
      "uri": "file:///home/kakadu/prog/ocaml/lablqml/ppx/testdemo2.ml"
    }

Kakadu

module Reader = struct
  type ('r, 'a) t = { reader : 'r -> 'a }

  let run_reader { reader } = reader
  let reader f = { reader = f }
  let return x = { reader = (fun _ -> x) }
  let (>>=) x f = reader @@ fun r -> run_reader (f @@ run_reader x r) r
  let ask = reader (fun x -> x)
  let asks = reader

Kakadu

➜  lablqml git:(master) mkae
dune build lib/lablqml.a lib/dlllablqml_stubs.so
make: dune: Command not found
make: *** [Makefile:9: lib] Error 127
➜  lablqml git:(master) la
.  ..  CHANGELOG  configure  CONTRIBUTING.md  demos  dune  dune-project  dune_test  .git  .gitignore  lablqml.opam  lib  Makefile  ppx  README.md  .travis.yml
➜  lablqml git:(master) git pull
Already up to date.
➜  lablqml git:(master) opam switch create . 4.08.1 --verbose

Kakadu

(set-logic UF)
(set-option :produce-models true) 

(declare-sort T 0)
(declare-fun appendo (T T T) Bool)
(declare-fun cons (T T) T)
(declare-fun nil () T)

(assert (forall ((y T)) (appendo nil y y )))
(assert (forall ((x T) (y T) (z T) (w T)) (=> (appendo x y z) (appendo (cons w x) y (cons w z)))))

Kakadu

(declare-sort T 0)
(declare-fun appendo (T T T) Bool)
(declare-fun cons (T T) T)
(declare-fun nil () T)

(assert (forall ((y T)) (appendo nil y y )))
(assert (forall ((x T) (y T) (z T) (w T)) (=> (appendo x y z) (appendo (cons w x) y (cons w z)))))
(assert (forall ((w T) (y T)) (=> (appendo (cons w nil) y y) false)))
(check-sat)
(get-model)