###### tags: pf-dabi

# Lista 3

## Zadanie 3

type formula = 
| Var of string
| False
| Implication of formula * formula

## Zadanie 4

let rec string_of_formula f =
  match f with
  | Var(var_name) -> var_name
  | False -> "⊥"
  | Implication(f1, f2) ->
    match f1 with
    | Implication(_, _) -> "(" ^ (string_of_formula f1) ^ ") -> " ^ (string_of_formula f2)
    | Var(_) | False -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2)

## Zadanie 5

type theorem = formula list * formula

let assumptions thm =
  match thm with 
  | (a, _) -> a 

let consequence thm =
  match thm with 
  | (_, c) -> c

## Zadanie 6

type formula =
| Pin
| Var of string
| Implies of formula * formula

let by_assumption f = ([f], f)

let imp_i f thm = 
   (List.filter (fun x -> x <> f) (assumptions thm),
   (Implies(f, (consequence thm))))

let imp_e th1 th2 =
  match (consequence th1) with 
  | Implies(a, b)  -> 
    if a = (consequence th2) then ((assumptions th1) @ (assumptions th2), b)
    else failwith " "
  | _ -> failwith " "
 
let bot_e f thm =
  if (consequence thm) = Pin then 
    (assumptions thm, f)
  else failwith " "

---

# Lista 4

## Zadania 3-6

open Logic

type no_target_proof =
| Empty of (string * formula) list * formula
| ImpI of no_target_proof * (string * formula) list * formula
| ImpE of no_target_proof * no_target_proof * (string * formula) list * formula
| BotE of no_target_proof * (string * formula) list * formula
| Complete of theorem

and context = 
| Root
| Left of context * no_target_proof * (string * formula) list * formula
| Right of no_target_proof * context * (string * formula) list * formula
| DownB of context * (string * formula) list * formula
| DownI of context * (string * formula) list * formula


type proof = context * no_target_proof


let proof g f =
  (Root, Empty(g, f))

let qed (ctx, pf) =
  match pf with
  | Complete(t)   -> t
  | _             -> failwith "Dowód nieukończony"

let goal (ctx, pf) =
  match pf with
  | Empty(g, f) -> Some(g, f)
  | _           -> None

let rec next_up (ctx, pf) = 
  match pf with
  | Complete(t) -> begin match ctx with 
                   | Root -> (ctx, pf)
                   | DownB(ctx, g, f)      -> next_up (ctx, Complete(bot_e f t))
                   | DownI(ctx, g, f)      -> next_up (ctx, Complete(imp_i f t))
                   | Left(ctx, pf2, g, f)  -> begin match pf2 with
                                              | Complete(t2) -> next_up (ctx, Complete(imp_e t t2))
                                              | _ -> next_right (ctx, ImpE(pf, pf2, g, f))
                                              end
                   | Right(pf2, ctx, g, f) -> begin match pf2 with
                                              | Complete(t2) -> next_up (ctx, Complete(imp_e t2 t))
                                              | _ -> next_left (ctx, ImpE(pf2, pf, g, f))
                                              end
                   end
  | _           -> begin match ctx with
                   | Root                  -> next_left (ctx, pf)
                   | DownB(ctx, g, f)      -> next_up (ctx, BotE(pf, g, f))
                   | DownI(ctx, g, f)      -> next_up (ctx, ImpI(pf, g, f))
                   | Left(ctx, pf2, g, f)  -> next_right (ctx, ImpE(pf, pf2, g, f))
                   | Right(pf2, ctx, g, f) -> next_up (ctx, ImpE(pf2, pf, g, f))
                   end


and next_left (ctx, pf) =
  match pf with
  | Empty(_, _) | Complete(_) -> (ctx, pf)
  | ImpI(pf, g, f)            -> next_left (DownI(ctx, g, f), pf)
  | BotE(pf, g, f)            -> next_left (DownB(ctx, g, f), pf)
  | ImpE(pf1, pf2, g, f)      -> begin match pf1 with
                                 | Complete(_) -> next_right (ctx, pf)
                                 | _           -> next_left (Left(ctx, pf2, g, f), pf1)
                                 end 

and next_right (ctx, pf) =
  match pf with 
  | ImpE(pf, pf2, g, f) -> begin match pf2 with
                           | Complete(_) -> next_up (ctx, pf)
                           | _           -> next_left (Right(pf, ctx, g, f), pf2)
                           end
  | _                   -> next_left (ctx, pf)


let next (ctx, pf) =
  match pf with
  | Complete(_) -> failwith "Nie ma więcej dziur"
  | _           -> next_up (ctx, pf)

let intro name (ctx, pf) =
  match goal (ctx, pf) with
  | None       -> failwith "Dowód ukończony"
  | Some(g, f) -> match f with
                  | Implication(left, right) -> (DownI(ctx, g, left), Empty((name, left) :: g, right))
                  | _                        -> failwith "Celem musi być implikacja"

                  
let rec far_right f = 
  match f with 
  | Implication(_, right) -> far_right right
  | _                     -> f

let rec apply_aux f (ctx, pf) g phi acc =
  if f = phi then
    ctx, acc
  else 
    let r = far_right f in
    if r <> phi && r <> False then
      failwith "Dowód niepoprawny"
    else
      match f with
      | False                    -> DownB(ctx, g, phi), acc
      | Implication(left, right) -> let (ctx2, _) = apply_aux right (ctx, pf) g phi (ImpE(acc, Empty(g, left), g, right)) in
                                    Left(ctx2, Empty(g, left), g, right), acc
      | _                        -> failwith "Miejsce nieosiągalne" 
                          

let apply f (ctx, pf) =
  match goal (ctx, pf) with
  | None         -> failwith "Nic do udowodnienia"
  | Some(g, phi) -> next_up (apply_aux f (ctx, pf) g phi (Empty(g, f)))
                                           
let apply_thm thm (ctx, pf) =
  match goal (ctx, pf) with
  | None         -> failwith "Nic do udowodnienia"
  | Some(g, phi) -> next_up (apply_aux (consequence thm) (ctx, pf) g phi (Complete(thm)))

let apply_assm name (ctx, pf) =
  match goal (ctx, pf) with
  | None         -> failwith "Nic do udowodnienia"
  | Some(g, phi) -> apply_thm (by_assumption (List.assoc name g)) (ctx, pf)

let pp_print_proof fmtr pf =
  match goal pf with
  | None -> Format.pp_print_string fmtr "No more subgoals"
  | Some(g, f) ->
    Format.pp_open_vbox fmtr (-100);
    g |> List.iter (fun (name, f) ->
      Format.pp_print_cut fmtr ();
      Format.pp_open_hbox fmtr ();
      Format.pp_print_string fmtr name;
      Format.pp_print_string fmtr ":";
      Format.pp_print_space fmtr ();
      pp_print_formula fmtr f;
      Format.pp_close_box fmtr ());
    Format.pp_print_cut fmtr ();
    Format.pp_print_string fmtr (String.make 40 '=');
    Format.pp_print_cut fmtr ();
    pp_print_formula fmtr f;
    Format.pp_close_box fmtr ()

## Zadanie 7

#install_printer Logic.pp_print_formula;;
#install_printer Logic.pp_print_theorem;;
#install_printer Proof.pp_print_proof;;

open(Proof)
open(Logic)

let p = Variable("p");;
let q = Variable("q");;
let r = Variable("r");;
let f = Implication(p, Implication(Implication(p ,q), q));;


let f1 = Implication(
    Implication(
      p, 
      Implication(
        q, 
        r
        )
    ), 
    Implication(
      Implication(
        p, 
        q
        ),
      Implication(
        p, 
        r
        )
    ) 
);;
proof [] f1 |> intro "1" |> intro "2" |> intro "3" |> apply_assm "1" |> apply_assm "3" |> apply_assm "2" |> apply_assm "3" |> qed;;

let f2 = Implication(
  Implication(
    Implication(
      Implication(
        p,
        False
      ),
      p
    ),
    p
  ), 
  Implication(
    Implication(
      Implication(
        p,
        False
      ),
      False
    ),
    p
  )
);;
proof [] f2 |> intro "1" |> intro "2" |> apply_assm "1" |> intro "3" |> apply_assm "1" |> apply_assm "2" |> apply_assm "3" |> qed;;

let f3 = Implication(
  Implication(
    Implication(
      Implication(
        p,
        False
      ),
      False
    ),
    p
  ), 
  Implication(
    Implication(
      Implication(
        p,
        False
      ),
      p
    ),
    p
  )
);;

proof [] f3 |> intro "1" |> intro "2" |> apply_assm "1" |> intro "3" |> apply_assm "3" |> apply_assm "2" |> apply_assm "3" |> qed;;

---

# Lista 5

## Zadania 1 & 2

let rec fix f x = f (fix f) x

let fib_f fib n =
    if n <= 1 then n
    else fib (n - 1) + fib (n - 2)


let fib = fix fib_f

let rec fix_with_limit limit f x =
    if limit > 0 then f (fix_with_limit (limit - 1) f) x
    else failwith "Max recursion depth reached"

let fix_memo f =
    let memory = Hashtbl.create 100 in
    let rec fix memory f x =
        match (Hashtbl.find_opt memory x) with
        | None -> let result = f (fix memory f) x
        in Hashtbl.add memory x result; result
        | Some v -> v
    in f (fix memory f)
        
type 'a fix = Roll of ('a fix -> 'a);;
let unroll (Roll x) = x;;
let fix2 f = (fun x a -> f (unroll x x) a) (Roll (fun x a -> f (unroll x x) a));;


let fib0 = ref (fun x -> x);;
let fibm n = if n < 2 then n else (!fib0 (n-1)) + (!fib0 (n-2));;
fib0 := fibm;;



let fixx f x=
    let prefix = ref (fun a -> failwith "undefined") in
    (prefix := fun g ->g (!prefix g) );f (!prefix f) x

## Zadanie 4 & 5

type 'a lazy_cycle = 'a data lazy_t
and 'a data = {
    prev : 'a lazy_cycle;
    elem : 'a;
    next : 'a lazy_cycle;
}

let prev x = (Lazy.force x).prev
let elem x = (Lazy.force x).elem
let next x = (Lazy.force x).next

let of_list xs = 
    let len = List.length xs in
    let add n = (n + 1) mod len in
    let sub n = (n - 1 + len) mod len in
    let rec next n x = 
        let rec cur = lazy({
            prev = x;
            elem = List.nth xs n;
            next = next (add n) cur;
        }) in
        cur in
    let rec prev n x = 
        let rec cur = lazy ({
            prev = prev (sub n) cur;
            elem = List.nth xs n;
            next = x;
        }) in
        cur in
    let rec head = lazy({
        prev = prev (sub 0) head;
        elem = List.nth xs 0;
        next = next (add 0) head;
    }) in
    head
    
let integers = 
    let rec next n x = 
        let rec cur = lazy({
            prev = x;
            elem = n;
            next = next (n + 1) cur;
        }) in
        cur in
    let rec prev n x = 
        let rec cur = lazy ({
            prev = prev (n - 1) cur;
            elem = n;
            next = x;
        }) in
        cur in
    let rec zero = lazy({
        prev = prev (-1) zero;
        elem = 0;
        next = next 1 zero;
    }) in
    zero

## Zadanie 6

type 'a my_lazy = 'a lazy_node ref and
 'a lazy_node =
| Value of 'a
| Delayed of (unit -> 'a)
| Calc

let rec force m_lazy = match !m_lazy with
| Calc -> failwith "Calculating"
| Value a -> a
| Delayed f ->
    m_lazy := Calc;
    let calcval = f () in
    m_lazy := Value(calcval);
    calcval

let rec fix f = ref (Delayed(fun () -> f (fix f)))

## Zadanie 7

type 'a info = 
| Cont of (unit -> 'a)
| Data of 'a
| Calculated

type 'a my_lazy =  'a info ref


let force mlz = 
  match mlz.contents with
  | Cont(f)    -> mlz := Calculated; let x = f () in mlz := Data(x); x
  | Data(d)    -> d
  | Calculated -> failwith "ERROR"

let fix f =
  let rec mlz =  
    ref (Cont(fun () -> f mlz))
  in mlz


type 'a llist = 
  'a node my_lazy

and  'a node = 
| Nil
| Cons of 'a * 'a llist

let rec of_list lst = fix (fun _ -> 
  match lst with
  | []     -> Nil
  | h :: t -> Cons(h, of_list t)
  )

let rec to_list llst = 
  match force llst with
  | Nil        -> []
  | Cons(h, t) -> h :: to_list t

let rec filter p llst = fix (fun _ -> 
  match force llst with 
  | Nil                 -> Nil
  | Cons(h, t) when p h -> Cons(h, filter p t)
  | Cons(_, t)          -> force (filter p t)
  )

let rec take_while p llst = fix (fun _ -> 
  match force llst with
  | Nil                 -> Nil
  | Cons(h, t) when p h -> Cons(h, take_while p t)
  | Cons(_, t)          -> Nil
  )

let rec for_all p llst = 
  match force llst with
  | Nil        -> true
  | Cons(h, t) -> p h && for_all p t

let rec nth n llst = 
  match n, force llst with 
  | _, Nil        -> failwith "Error"
  | 0, Cons(h, _) -> h
  | _, Cons(_, t) -> nth (n-1) t

let rec nats_from n = 
  fix (fun _ -> Cons(n, nats_from (n+1)))

let is_prime n = 
  (nats_from 2)
  |> take_while (fun p -> p * p <= n)
  |> for_all (fun p -> n mod p <> 0)

let rec primes = 
  fix (fun _ -> Cons(2, filter is_prime (nats_from 3)))

## Zadania 8 - 10

(* Zadania 8, 10*)
type _ fin_type =
| Unit : unit fin_type
| Bool : bool fin_type
| Pair : 'a fin_type * 'b fin_type -> ('a * 'b) fin_type
| Fun : 'a fin_type * 'b fin_type -> ('a -> 'b) fin_type

let unit_seq = Seq.cons () Seq.empty
let bool_seq = Seq.cons true (Seq.cons false  Seq.empty)


let make_values domain codomain =
  let empty_fun = Seq.cons [] Seq.empty in
  Seq.fold_left (fun acc d -> 
  let pairs = Seq.map (fun cd -> (d, cd)) codomain in (* wszytkie pary true -> 'b *)
    Seq.flat_map (fun f -> Seq.map (fun pair -> pair :: f) pairs) acc
  ) empty_fun domain


let rec all_values:type a. a fin_type -> a Seq.t = function
| Unit -> unit_seq
| Bool -> bool_seq
| Pair(l, r) ->
  let ls, rs = all_values l, all_values r in
  Seq.flat_map (fun l -> Seq.map (fun r -> (l,r)) rs) ls
| Fun(a,b) ->
  let domain = all_values a
  and codomain = all_values b
  and list_to_fun flist = 
    (fun arg1 -> List.find (fun (arg2, v) -> equal_at a arg1 arg2) flist |> snd) in
  let all_functions = make_values domain codomain in
  Seq.map list_to_fun all_functions

and equal_at: type a. a fin_type -> a -> a -> bool  =
  function
  | Unit -> fun x y -> true
  | Bool -> fun x y -> x = y
  | Pair(_,_) -> fun (a,b) (c,d) -> a = c && b = d
  | Fun(a,b) ->
    fun f1 f2 -> 
      Seq.fold_left (fun all arg -> all && equal_at b (f1 arg) (f2 arg))
      true (all_values a)


(* Zadanie 9 *)
type empty = |

type _ fin_type =
| Empty : empty fin_type
| Unit : unit fin_type
| Bool : bool fin_type
| Pair : 'a fin_type * 'b fin_type -> ('a * 'b) fin_type
| Either : 'a fin_type * 'b fin_type -> (('a, 'b) Either.t) fin_type


let unit_seq = Seq.cons () Seq.empty
let bool_seq = Seq.cons true (Seq.cons false  Seq.empty)

let rec all_values:type a. a fin_type -> a Seq.t = function
| Empty -> Seq.empty
| Unit -> unit_seq
| Bool -> bool_seq
| Either(l,r) ->
  let ls = all_values l |> Seq.map Either.left
  and rs = all_values r |> Seq.map Either.right
in Seq.append ls rs
| Pair(l, r) ->
  let ls, rs = all_values l, all_values r in
  Seq.flat_map (fun l -> Seq.map (fun r -> (l,r)) rs) ls

# Lista 5

# Lista 7

## Zadanie 1 & 2

module RS : sig
  type 'a t
  val return : 'a -> 'a t
  val bind : 'a t -> ('a -> 'b t) -> 'b t
  val random : int t
  val run : int -> 'a t -> 'a
end = struct
  type 'a t = int -> 'a * int

  let return x s = (x, s) 

  let bind m f s = 
    let (x, s) = m s in
      f x s

  let hash a = 
    let b = (16807 * (a mod 127773)) - 2836 * (a mod 127773) in
    if b > 0 then b else b + 2147483647

  let random s = (s, hash s) 

  let run s m = let (x, _) = m s in x
end

let (let* ) = RS.bind

let rec rand n acc = 
  if(n = 0) 
    then RS.return acc
    else let* el = RS.random in
      rand (n - 1) (el :: acc)

let arr x = RS.run 0 (rand x [])


let shuffle s xs =
  let rec pick n = function
    | x :: xs ->
      if n = 0 
        then (x, xs) 
        else let (v, xs) = pick (n - 1) xs in
          (v, x :: xs)
    | _ -> failwith "error" 
  in
  let rec iter n acc xs = 
    if n = 0 
      then RS.return acc
      else 
        let* p = RS.random in
        let (v, xs) = pick (p mod n) xs in
        iter (n - 1) (v :: acc) xs
  in RS.run 
    s
    (iter (List.length xs) [] xs)

let shuffled1 = shuffle 1 [1; 2; 3; 4; 5]
let shuffled2 = shuffle 2 [1; 2; 3; 4; 5]
let shuffled3 = shuffle 3 [1; 2; 3; 4; 5]
let shuffled4 = shuffle 4 [1; 2; 3; 4; 5]
let shuffled5 = shuffle 5 [1; 2; 3; 4; 5]

## Zad3

(* identity monad *)
module IM : sig
  type 'a t
  val return : 'a -> 'a t
  val bind : 'a t -> ('a -> 'b t) -> 'b t
  val test : 'a t -> 'a
end = struct

  type 'a t = 'a

  let return x = x

  let bind m f = f m
  
  let test m = m
end

(* testy *)

let x = IM.return 5;;
IM.test x;;

let (let*) = IM.bind;;

let rec test xl =
  match xl with
  | x :: xs ->
    let* a = IM.return x in
    let* b = (test xs) in
    IM.return (a :: b)
  | [] -> IM.return []
;;

let x = test [1;2;3];;
x;;
IM.test x;;


(* lazy monad *)

module LM : sig
  type 'a t
  val return : 'a -> 'a t
  val bind :  'a t -> ('a -> 'b t) -> 'b t
  val test : 'a t -> 'a
end = struct

  type 'a t = unit -> 'a

  let return x = fun () -> x

  let bind m f = f (m ())
  
  let test m = m ();;
end

(* testy *)
let rec r f x = f x;;

let lm = LM.return (r (fun x -> x * 2) 5);;

LM.test lm;;

let x = fun () -> 1;;
let f y = fun () -> y + 1;;
let g z = fun () -> z * 2;;

let (let*) = LM.bind;;

let x = test [1;2;3];;
x;;
IM.test x;;

## Zadanie 4

module type Monad = sig
  type 'a t
  val return : 'a -> 'a t
  val bind : 'a t -> ('a -> 'b t) -> 'b t
end

module Err : sig
  include Monad
  val fail  : 'a t
  val catch : 'a t -> (unit -> 'a t) -> 'a t
  val run : 'a t -> 'a option
end = struct
  type 'r ans = 'r option
  type 'a t = { run : 'r.('a -> 'r ans) -> 'r ans }
  let return x = { run = fun k -> k x }
  let bind m f = { run = fun k -> m.run (fun a -> (f a).run k) }
  let fail = { run = fun _ -> None }
  let catch m f = { run = fun k -> 
    match m.run Option.some with
    | Some a -> (k a)
    | None -> (f ()).run k
  }

  let run x = x.run Option.some
end

module BT : sig
  include Monad
  val fail : 'a t
  val flip : bool t
  val run : 'a t -> 'a Seq.t
end = struct
  type 'r ans = 'r Seq.t
  type 'a t = { run : 'r. ('a -> 'r ans) -> 'r ans }
  let return x = { run = fun k -> k x }
  let bind m f = { run = fun k -> m.run (fun a -> (f a).run k)  }
  let fail = { run = fun _ -> Seq.empty }
  let flip = { run = fun k -> Seq.append (k true) (k false) }
  let run a = a.run Seq.return
end

module St(State : sig type t end) : sig
  include Monad
  val get : State.t t
  val set : State.t -> unit t
  val run : State.t -> 'a t -> 'a
end = struct
  type 'r ans = State.t -> 'r
  type 'a t = { run : 'r. ('a -> 'r ans) -> 'r ans }
  let return x = { run = fun k -> k x }
  let bind m f = { run = fun k -> m.run (fun a -> (f a).run k)  }
  let get = { run = fun k s -> k s s }
  let set s = { run = fun k _ -> k () s }
  let run s m = m.run (fun a -> fun _ -> a) s
end

## Zadanie 5

module BT : sig
  type 'a t

  val return : 'a -> 'a t
  val bind   : 'a t -> ('a -> 'b t) -> 'b t

  (** Brak wyniku *)
  val fail : 'a t
  (** Niedeterministyczny wybór -- zwraca true, a potem false *)
  val flip : bool t

  val run : 'a t -> 'a Seq.t
end = struct
(* Obliczenie typu 'a to leniwa lista wszystkich możliwych wyników *)
type 'a t = 'a Seq.t

  let return x = List.to_seq [ x ]
  let rec bind m f = Seq.flat_map f m

  let fail = Seq.empty
  let flip = List.to_seq [ true; false ]

  let run m = m
end


let (let* ) = BT.bind

type 'a regexp =
| Eps
| Lit of ('a -> bool) 
| Or of 'a regexp * 'a regexp
| Cat of 'a regexp * 'a regexp
| Star of 'a regexp

let ( +% ) r1 r2 = Or(r1, r2)
let ( *% ) r1 r2 = Cat(r1, r2)

let rec match_regexpr : 'a regexp -> 'a list -> 'a list option BT.t =
  fun regexp prefix ->
    match regexp, prefix with
    | Eps, _ -> BT.return None
    | Lit p, c :: xs when p c -> BT.return (Some xs)
    | Or(a,b), _ ->
      let* c = BT.flip in
      if c then match_regexpr a prefix
      else match_regexpr b prefix
    | Cat(a,b), _ ->
      let* res1 = match_regexpr a prefix in
      (match res1 with
      | None -> match_regexpr b prefix
      | Some prefix -> 
        let* res2 = match_regexpr b prefix in 
        match res2 with 
        | None -> BT.return (Some prefix)
        | Some prefix -> BT.return (Some prefix)) 
    | Star a, _ -> 
      let* c = BT.flip in
      if not c then BT.return None
      else let* res1 = match_regexpr a prefix in
      (match res1 with
      | None -> BT.return None
      | Some prefix -> 
        let* res2 = match_regexpr regexp prefix in
        match res2 with
        | None -> BT.return (Some prefix)
        | Some prefix -> BT.return (Some prefix)
      ) 
    | _, _ -> BT.fail

## Zadanie 6

(* module SBT(State : sig type t end) : sig
  type 'a t
  val return : 'a -> 'a t
  val bind : 'a t -> ('a -> 'b t) -> 'b t
  val fail : 'a t
  val flip : bool t
  val get : State.t t
  val put : State.t -> unit t
  val run : State.t -> 'a t -> 'a Seq.t
end  *)



module SBT(State : sig type t end) = struct 
  type 'a t = State.t -> ('a * State.t) Seq.t
  
  let return: 'a -> 'a t = 
    fun x s -> Seq.return (x, s)

  let bind: 'a t -> ('a -> 'b t) -> 'b t =
    fun m f s ->
      let xs = m s in
        Seq.flat_map (fun (x, s) -> f x s) xs
  
  let fail : 'a t =
    fun s -> Seq.empty

  let flip : bool t =
    fun s -> List.to_seq [(true, s); (false, s)]

  let get : State.t t =
    fun s -> Seq.return (s, s)

  let put : State.t -> unit t =
    fun s _ -> Seq.return ((), s)

  let run : State.t -> 'a t -> 'a Seq.t = 
    fun s m -> 
      let xs = (m s) in 
      Seq.map (fst) xs
end
module Match(State : sig type t end) = struct
  module M = SBT(struct type t = State.t list end)
  let ( let* ) = M.bind

type 'a regexp =
| Eps
| Lit of ('a -> bool)
| Or of 'a regexp * 'a regexp
| Cat of 'a regexp * 'a regexp
| Star of 'a regexp

let rec match_regexpr : 'a regexp -> 'a list M.t =
  fun regexp ->
    match regexp with
    | Eps -> M.return []
    | Lit p ->
      let* word = M.get in
      (match word with
      | [] -> M.fail
      | x :: xs when p x ->
        let* () = M.put xs in
        M.return [x]
      | _ -> M.fail)
    | Or(a,b) ->
      let* c = M.flip in
      if c then match_regexpr a
      else match_regexpr b 
    | Cat(a,b) ->
      let* res1 = match_regexpr a in
      let* res2 = match_regexpr b in
      M.return (res1 @ res2)
    | Star a -> 
      let* c = M.flip in
      if not c then M.return []
      else let* res1 = match_regexpr a  in
      (match res1 with
      | [] -> M.return []
      | _ -> 
        let* res2 = match_regexpr regexp in
        M.return (res1 @ res2)
        ) 
    | _ -> M.fail
end

## Zadanie 7

:::warning
Częściowo niegotowe
DaBi: poprawna funkcja bind poniżej
:::

module SBTR(State : sig type t end) : sig

  type 'a t

  val return : 'a -> 'a t
  val bind :'a t -> ('a -> 'b t) -> 'b t

  val fail :'a t
  val flip : bool t

  val get : State.t t
  val set : State.t -> unit t

  val run : State.t -> 'a t -> 'a Seq.t

end = struct
  
  type 'a t = State.t -> 'a sbt_list
  and 'a sbt_list =
  | Nil
  | Cons of 'a * State.t * 'a t

  let return x s = Cons(x, s, fun s -> Nil)

  (* a t -> ('a -> 'b t) -> 'b t *)
  (*  Seq.flat_map (fun (v, s) -> f v s) (m s) *)
  let rec bind :'a t -> ('a -> 'b t) -> 'b t = 
     (*  fun x -> failwith "TODO" *)
    
    fun m f s ->
    let rec concat xs ys =
      match xs with
      | Cons(v, s, xs) -> (fun s -> Cons(v, s, concat (xs s) ys))
      | Nil -> (fun s -> ys)
    in
    let rec map = function
      | Cons(v, s, xs) -> (*concat*) (f v) (* (xs s) *)
      | Nil -> (fun s -> Nil)
    in (map (m s)) s
  
  (* let rec bind m f = Seq.flat_map f m *)
  (* let bind m f s =
    let (x, s) = m s in
    f x s *)

  let fail :'a t = 
    fun s -> Nil
  let flip : bool t = 
    fun s -> Cons(true, s, fun s -> Cons(false, s, fun s -> Nil))

  let get : State.t t =
    fun s -> Cons(s, s, fun s -> Nil)
  let set : State.t -> unit t =
    fun s _ -> Cons((), s, fun s -> Nil)

  let run : State.t -> 'a t -> 'a Seq.t = 
    let rec map = function
    | Nil -> Seq.empty
    | Cons(v, s, tl) ->
      Seq.cons v (map (tl s))
    in
    fun s m -> 
      m s |> map
end

module N = SBTR(Int)

let id x = 
  let h x =
    N.return x
  in N.run 0 (h x)


  let (let* ) = N.bind

let rec select a b =
  if a >= b then N.fail
  else
    let* c = N.flip in
    if c then N.return a
    else select (a+1) b


let rec arrs n acc =
  if n = 0 
  then N.return acc 
  else let* c = N.flip in
    let* v = N.get in
    let* () = N.set (v + 1) in
      if c  then (arrs (n - 1) (v :: acc))
            else (arrs (n - 1) acc)

let force_all m = 
  let rec iter m xs =
    match Seq.uncons m with
    | Some(a, b) -> iter b (a :: xs)
    | None -> xs
  in
  iter m []

  let subs = arrs 3 [] |> N.run 1 |> force_all

:::info
Poprawiona funkcja bind.

Funkcja concat nie łączy list, ale drzewa (obiekty typu 'a t)
:::

 let rec bind m f = 
   let rec concat m1 m2 =
     fun s ->
     match m1 s with
     | Nil -> m2 s
     | Cons(v, s', m2') -> Cons(v, s', concat m2' m2)
   in
   let rec map = function
     | Nil -> Nil
     | Cons(v, s, m') -> concat (f v) (fun s' -> map (m' s')) s
   in fun s -> map (m s)

---
# Lista 8

## Zadanie 3

listTrans :: StreamTrans i o a -> [i] -> ([o], a)
listTrans (Return x) xs =
  ([], x)
listTrans (ReadS f) xs =
  listTrans (f hd) tl
  where
    hd = case xs of
      [] -> Nothing
      (h : _) -> Just h
    tl = case xs of
      [] -> []
      (_ : t) -> t
listTrans (WriteS o st) xs =
  let (rs, x) = listTrans st xs
   in (o : rs, x)

## Zadanie 5

data StreamTrans i o a
  = Return a
  | ReadS (Maybe i -> StreamTrans i o a)
  | WriteS o (StreamTrans i o a)

(|>|) :: StreamTrans i m a -> StreamTrans m o b -> StreamTrans i o b
_ |>| (Return b) = Return b
s1 |>| (WriteS o s2) = WriteS o (s1 |>| s2)
(ReadS c1) |>| s2 = ReadS (\mi -> c1 mi |>| s2)
(WriteS m s1) |>| (ReadS c2) = s1 |>| c2 (Just m)
s1 |>| (ReadS c2) = s1 |>| c2 Nothing

## Zadanie 6

reverseList xs = foldl (\x y -> y:x) [] xs 

catchOutput :: StreamTrans i o a -> StreamTrans i b (a, [o])
catchOutput s = helper s []
  where
    helper (Return a) os = Return (a, (reverseList os))
    helper (ReadS c) os = ReadS (\x -> helper (c x) os)
    helper (WriteS o s) os = helper s (o:os)

--listRun służy do uruchomienia StreamTrans z listą wejściową i zasymulowania wypisywania na output
listRun :: StreamTrans Char Char a -> [Char] -> a
listRun (ReadS f) [] = (listRun (f Nothing) [])
listRun (ReadS f) (x:xs) = listRun (f (Just x)) xs
listRun (WriteS y trans') xs = listRun trans' xs
listRun (Return a) xs = a


main::IO()
main = putStrLn (snd (listRun (catchOutput toLower) "ASbs"))

## Zadanie 8

type Tape = ([Integer], [Integer])
emptyTape = (repeat 0, repeat 0)

runBF :: [BF] -> StreamTrans Char Char () 
runBF code = 
    evalBFBlock emptyTape code >>= (\ tape -> Return ())
    
evalBF :: Tape -> BF -> StreamTrans Char Char Tape
evalBF (prev, h : t) MoveR = 
    Return (h : prev, t)

evalBF (h : t, next) MoveL = 
    Return (t, h : next)

evalBF (prev, h : t) Inc = 
    Return (prev, (h+1) : t)

evalBF (prev, h : t) Dec = 
    Return (prev, (h-1) : t)

evalBF (prev, h : t) Input = 
    ReadS (\ (Just c) -> Return (prev, charToInt c : t))

evalBF tape@(prev, h : t) Output = 
    WriteS (intToChar h) (Return tape)

evalBF tape@(prev, h : t) (While xs) =
    if h > 0 
        then evalBFBlock tape xs >>= (\ t -> evalBF t (While xs))
        else Return tape

-- dwa przypadki, które nie zachodzą, ponieważ listy są nieskończone
evalBF ([], next) MoveL = 
    Return ([], next)

evalBF (prev, []) bf = 
    Return (prev, [])
-- 

evalBFBlock :: Tape -> [BF] -> StreamTrans Char Char Tape
evalBFBlock = 
    foldM evalBF
    
coerceEnum :: (Enum a, Enum b) => a -> b
coerceEnum = toEnum . fromEnum

charToInt :: Char -> Integer
charToInt c = 
    coerceEnum c - 48

intToChar :: Integer -> Char
intToChar n = 
    coerceEnum (n + 48)
    

## Zadanie 9

instance Functor (StreamTrans i o) where
  fmap f m = m >>= return . f

instance Applicative (StreamTrans i o) where
  pure = return
  (<*>) = ap

instance Monad (StreamTrans i o) where
  return a = Return a

  (>>=) (Return a) f =
    f a
  (>>=) (ReadS func) f =
    ReadS (\c -> func c >>= f)
  (>>=) (WriteS o m) f =
    WriteS o m >>= f