Debugging search order

Demo1

  let goal2 exp =
    conde
      [ call_fresh_named "t" (fun _t  ->
          MKStream.inc2 (fun () ->
          ?&  [ exp === !!0
              ; exp === !!1
              ])
        )
      ; call_fresh_named "es" (fun _t ->
            MKStream.inc2 (fun () -> exp === !!2 ))
      ; call_fresh_named "zz" (fun _t ->
            MKStream.inc2 (fun () -> exp === !!3 ))
      ]
  in
  run q goal2 (fun qs -> Stream.take ~n:2 qs
      |> List.map (fun rr -> rr#prj) |> List.iter (printfn "%d"));

(list-display
  (run 2 (exp)
    (conde
      ((fresh (t)
          (=== exp 0)
          (=== exp 1)
          ))
      ((fresh (es)
          (=== exp 2)))
      ((fresh (zzzzzzzzzs)
          (=== exp 3)))
          ))

)

; and expanded to 
(list-display (run 2 (exp)
  (lambdag@ (st)
    (lambda ()
     (let ((st (state-with-scope st (new-scope))))
      (mplus
        ; Bind was here
        (let ((scope (subst-scope (state-S st))))
          (let ( (t (var 't scope)) )
             (inc
               ((=== exp 1 ) st) )))

        (inc
          (begin (printf "herr\n")
          (mplus
            ; Bind was here
            (let ((scope (subst-scope (state-S st))))
              (let ( (es (var 'es scope)) )
                 (inc
                   ((=== exp 2) st) )))
          (inc
            ; Bind was here
            (let ((scope (subst-scope (state-S st))))
              (let ( (zzzzzzzzzzs (var 'zzzzzzzzzs scope)) )
                 (inc
                   ((=== exp 3) st) )))))))
  ))))
))

Demo2

  let goal1 exp =
    conde [ call_fresh_named "t1" (fun t1 ->
              MKStream.inc2 @@ fun () ->
              ?&  [ (exp === !!0)
                  (* ; conde [ (t1 === !!1) (*&&& (t1 === !!2) *) ] *)
                  ]
              )
          ; call_fresh_named "t2" (fun t2 ->
              MKStream.inc2 @@ fun () ->
              ?&  [ (exp === !!3)
                  (* ; conde [ (t2 === !!4) (*&&& (t2 === !!5) *) ] *)
                  ]
              )
          ; call_fresh_named "t3" (fun t3 ->
              MKStream.inc2 @@ fun () ->
              ?&  [ (exp === !!6)
                  (* ; conde [ (t3 === !!7) (*&&& (t3 === !!8) *) ] *)
                  ]
              )
          ]
  in

  run q goal1 (fun qs -> Stream.take ~n:(-1) qs
    |> List.map (fun rr -> rr#prj) |> List.iter (printfn "%d") );

  (run* (exp)
    (conde
      ((fresh (t1)
          (=== exp 0)
          ;(conde
          ;  ((=== t1 1) );(=== t1 2))
          ;)
          ))
      ((fresh (t2)
          (=== exp 3)
          ;(conde
          ;  ((=== t2 4) );(=== t2 5))
          ;)
          ))
      ((fresh (t3)
          (=== exp 6)
          ;(conde
          ;  ((=== t3 7) );(=== t3 8))
          ;)
          ))
    )
  )

Demo3

  let rec evalo m =
    printfn " applying evalo to m";
    call_fresh_named "f2" (fun f2 ->
      let () = printfn "create inc in fresh ==== (f2)" in
      delay2 @@ fun () ->
        printfn "inc in fresh forced: (f2)" ;
        ?&
      [ conde
          [ call_fresh_named "x" (fun _x ->
              printfn "create inc in fresh ==== (x)";
              delay2 @@ fun () ->
                printfn "inc in fresh forced: (x)" ;
                (f2 === !!1)
            )
          ; call_fresh_named "p" (fun _p ->
              printfn "create inc in fresh ==== (p)";
              delay2 @@ fun () ->
                printfn "inc in fresh forced: (p)" ;
                (f2 === !!2)
            )
          ]
      ; (evalo !!4 )
      ]
    )
  in
  run q evalo (fun qs -> Stream.take ~n:1 qs
    |> List.map (fun rr -> rr#prj) |> List.iter (printfn "%d") );

;(define evalo (lambda (m)
;  (begin (printf " applying evalo to m\n")
;  (fresh (f2)
;      (conde
;        ((lambdag@ (st)
;            (let ( (x (var 'x (subst-scope (state-S st)))) )
;             (printf "create inc in fresh ==== ~a\n" (list 'x))
;             (inc (begin
;                   (printf "inc in fresh forced: ~a \n" (list 'x))
;                   ((=== f2 1) st) )))))
;        ((lambdag@ (st)
;            (let ( (p (var 'p (subst-scope (state-S st)))) )
;             (printf "create inc in fresh ==== ~a\n" (list 'p))
;             (inc (begin
;                   (printf "inc in fresh forced: ~a \n" (list 'p))
;                   ((=== f2 2) st) )))))
;      )
;      (evalo 4)
;  )
;)))

; and expanded to 
(define evalo (lambda (m)
  (begin (printf " applying evalo to m\n")
  (lambdag@ (st)
    (let ((scope (subst-scope (state-S st))))
      (let ((f2 (var 'f2 scope)) )
        (printf "create inc in fresh ==== ~a\n" (list 'f2 ) )
        (inc (begin
            (printf "inc in fresh forced: ~a \n" (list 'f2 ))
            (bind*
              (begin (printf " created inc in conde\n")
                (inc
                  (let ((st (state-with-scope st (new-scope))))
                    (printf " force a conde\n")
                    (mplus
                      (let ( (x (var 'x (subst-scope (state-S st)))) )
                               (printf "create inc in fresh ==== ~a\n" (list 'x))
                               (inc (begin
                                     (printf "inc in fresh forced: ~a \n" (list 'x))
                                     ((=== f2 1) st) )))
                      (inc (begin
                        (printf " force inc from mplus*\n")
                        (let ( (p (var 'p (subst-scope (state-S st)))) )
                            (printf "create inc in fresh ==== ~a\n" (list 'p))
                            (inc (begin
                                  (printf "inc in fresh forced: ~a \n" (list 'p))
                                  ((=== f2 2) st) ))))
                      )
                    )
                  )
                )
              )
              (evalo 4) )
            ))
        )))
)))