Compiler Explorer

Source code

module State = struct
  type s
  type 'a m = s -> 'a * s

let return a s = (a, s)

let bind m k s =
    let a, s = m s in
    k a s

let map f m = bind m (fun a -> return (f a))

module Import = struct
    let ( let* ) = bind
    let ( let+ ) m f = map f m
  end

let read s = (s, s)
  let run s m = m s

let mfold ps a ~f s =
    let f (a, s) p = f p a s in
    List.fold_left f (a, s) ps
end

open State.Import

type t =
  | True
  | Not of t
  | And of t list
  | Or of t list
  | If of {cnd: t; pos: t; neg: t}

let iter_dnf1 ~meet ~top fml ~f =
  let rec add_conjunct fml (cjn, splits) =
    match fml with
    | True | Not _ ->
        let+ cjn = meet fml cjn in
        (cjn, splits)
    | And ps -> State.mfold ~f:add_conjunct ps (cjn, splits)
    | Or ps -> State.return (cjn, ps :: splits)
    | If {cnd; pos; neg} ->
        add_conjunct (Or [And [cnd; pos]; And [Not cnd; neg]]) (cjn, splits)
  in
  let rec add_disjunct (cjn, splits) fml =
    let* cjn, splits = add_conjunct fml (cjn, splits) in
    let+ s = State.read in
    match splits with
    | ps :: splits ->
        List.iter
          (fun fml -> fst (State.run s (add_disjunct (cjn, splits) fml)))
          ps
    | [] -> f (cjn, s)
  in
  add_disjunct (top, []) fml

let dnf1 ~meet ~top fml =
  let+ s = State.read in
  fun f -> fst (State.run s (iter_dnf1 ~meet ~top fml ~f))

let iter_dnf2 ~meet ~top fml ~f s =
  let rec add_conjunct fml (cjn, splits) s =
    match fml with
    | True | Not _ ->
        let cjn, s = meet fml cjn s in
        ((cjn, splits), s)
    | And ps -> State.mfold ~f:add_conjunct ps (cjn, splits) s
    | Or ps -> ((cjn, ps :: splits), s)
    | If {cnd; pos; neg} ->
        add_conjunct
          (Or [And [cnd; pos]; And [Not cnd; neg]])
          (cjn, splits) s
  in
  let rec add_disjunct (cjn, splits) fml s =
    let (cjn, splits), s = add_conjunct fml (cjn, splits) s in
    match splits with
    | ps :: splits ->
        (List.iter (fun fml -> fst (add_disjunct (cjn, splits) fml s)) ps, s)
    | [] -> (f (cjn, s), s)
  in
  add_disjunct (top, []) fml s

let dnf2 ~meet ~top fml s =
  ((fun f -> fst (iter_dnf2 ~meet ~top fml ~f s)), s)