let nip str = String.sub str 1 ((String.length str) - 1);;

type expr = Var of string | Not of expr | And of (expr * expr) | Or of (expr * expr) | Conj of (expr * expr);;

let rec print_expr expr = match expr with
    | Var a       -> a
    | Not a       -> "(!" ^ (print_expr a) ^ ")"
    | And  (a, b) -> "(&," ^ (print_expr a) ^ "," ^ (print_expr b) ^ ")"
    | Or   (a, b) -> "(|," ^ (print_expr a) ^ "," ^ (print_expr b) ^ ")"
    | Conj (a, b) -> "(->," ^ (print_expr a) ^ "," ^ (print_expr b) ^ ")";;

let strange = "'";;

let rec make_var str have = if String.length str == 0
    then (Var have, str)
    else if String.length str >= String.length strange && String.sub str 0 (String.length strange) = strange
    then make_var (String.sub str (String.length strange) (String.length str - String.length strange)) (have ^ strange)
    else match str.[0] with
    | 'A'..'Z' | '0'..'9' -> make_var (nip str) (have ^ Char.escaped str.[0])
    | _                   -> (Var have, (String.trim str))

and make_nnot str = match str.[0] with
    | '!'      -> let (item, str) = make_nnot (String.trim (nip str)) in (Not item, str)
    | 'A'..'Z' -> let (item, str) = make_var  (nip str) (Char.escaped str.[0]) in (item, str)
    | _        -> let (item, str) = make_expr (String.trim (nip str)) in (item, (String.trim (nip str)))

and make_aand str = let (item, str) = make_nnot str in
    let rec make_aand_internal str have =
        if String.length str == 0 then (have, str)
        else
        match str.[0] with
        | '&' -> let (item, str) = make_nnot (String.trim (nip str)) in make_aand_internal str (And (have, item))
        | ')' | '|' | '-' -> (have, str)
        | _   -> failwith "Error1"
    in make_aand_internal str item

and make_oor str = let (item, str) = make_aand str in
    let rec make_oor_internal str have =
        if String.length str == 0 then (have, str)
        else
        match str.[0] with
        | '|' -> let (item, str) = make_aand (String.trim (nip str)) in make_oor_internal str (Or (have, item))
        | ')' | '-' -> (have, str)
        | _   -> failwith "Error2"
    in make_oor_internal str item

and make_expr str = let (item, str) = make_oor str in
    if String.length str == 0
    then (item, str)
    else match str.[0] with
        | '-' -> let (item2, str) = make_expr (String.trim (nip (nip str))) in (Conj (item, item2), str)
        | ')' -> (item, str)
        | _   -> failwith "Error3";;

let parse_expr str = let (a, _) = make_expr (String.trim str) in a;;

let rec make_context str =
    let (first, str) = make_expr (String.trim str) in
    let str = String.trim str in
    match str.[0] with
        | ',' -> let (lst, str) = make_context str in (first :: lst, str)
        | _   -> ([first], str);;

type need = Need of expr list * expr;;

let make_first_expr str =
    let (context, str) = make_context str in
    let str = String.trim (nip (nip (String.trim str))) in
    let (expr, _) = make_expr str in Need (context, expr);;

let (>>=) x f = match x with
    | Some a -> f a
    | None   -> None;;

let takeMon x y = match x with
    | Some a -> a
    | None   -> y;;

let rNone x y = None;;
let rNone2 a b y = None;;

let checkExpr f1 f2 f3 f4 f5 expr = match expr with
    | Var a       -> f1 a
    | Not a       -> f2 a
    | And  (a, b) -> f3 a b
    | Or   (a, b) -> f4 a b
    | Conj (a, b) -> f5 a b;;
let checkVar (proj, setter) expr took = match proj took with
    | None   -> Some (setter took (Some expr))
    | Some a -> if a = expr then Some took else None;;
let checkNot  f = checkExpr rNone f rNone2 rNone2 rNone2;;
let checkAnd  f = checkExpr rNone rNone f rNone2 rNone2;;
let checkOr   f = checkExpr rNone rNone rNone2 f rNone2;;
let checkConj f = checkExpr rNone rNone rNone2 rNone2 f;;

let l1 = (fun (a, _, _) -> a), fun (_, b, c) a -> (a, b, c);;
let l2 = (fun (_, a, _) -> a), fun (a, _, c) b -> (a, b, c);;
let l3 = (fun (_, _, a) -> a), fun (a, b, _) c -> (a, b, c);;

let rec print_expr_ expr = match expr with
    | Var a -> let linz = match a with
        | "A" -> l1
        | "B" -> l2
        | _   -> l3 in checkVar linz
    | Not a       -> checkNot  (print_expr_ a)
    | And  (a, b) -> checkAnd  (fun left right x -> print_expr_ a left x >>= (print_expr_ b right))
    | Or   (a, b) -> checkOr   (fun left right x -> print_expr_ a left x >>= (print_expr_ b right))
    | Conj (a, b) -> checkConj (fun left right x -> print_expr_ a left x >>= (print_expr_ b right))

let axioms = List.map (fun x -> print_expr_ (parse_expr x))
(       "A -> B -> A" ::
        "(A -> B) -> (A -> B -> C) -> (A -> C)" ::
        "A -> B -> A & B" ::
        "A & B -> A" ::
        "A & B -> B" ::
        "A -> A | B" ::
        "B -> A | B" ::
        "(A -> B) -> (A -> !B) -> !!A" ::
        "(A -> B) -> (C -> B) -> (A | C -> B)" ::
        "!!A -> A":: []);;

let checkAxioms to_check = List.concat (List.mapi (fun ind chain -> let result = chain to_check (None, None, None) in
    match result with
        | Some _ -> [ind]
        | None   -> []) axioms);;

print_string (String.concat ", " (List.map string_of_int (checkAxioms (parse_expr "((!U & W) -> (A -> B)) -> ((!U & W) -> (A -> B) -> (G -> R -> T)) -> ((!U & W) -> (G -> R -> T))"))));;

type node = Axiom of int | MP of (node * node);;

let checkEverything context need evidence =
    let contextSet = Set.empty in
    let rec checkStepByStep haveMap evidenceMap now =
        if Map.mem haveMap now
        then let to_add = takeMon (Map.find_opt evidenceMap now) []
             and smth_to_add = match now with
                | Conj (a, b) -> if Map.mem haveMap a then [b] else []
                | _ -> []
             and new_list = now ++ to_add ++ (takeMon (Map.find_opt haveMap b) [])

        else None

let make_evidence lines = match lines with
    | []                        -> failwith "Error blyat!"
    | first_line :: other_lines ->
        let Need (context, expr) = make_first_expr first_line in
        let other_expr = List.map make_expr other_lines in
        ();;


print_string "\n";;