Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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 checkOnFence str = String.length str > 2 && str.[0] = '|' && str.[1] = '-';;
- 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)))
- | _ -> failwith "Error4"
- and make_aand str = let (item, str) = make_nnot str in
- let rec make_aand_internal str have =
- if String.length str == 0 || checkOnFence str 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 || checkOnFence str 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 || checkOnFence str
- 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 (String.trim (nip str)) in (first :: lst, str)
- | _ -> ([first], str);;
- type need = Need of expr list * expr;;
- let make_first_expr str =
- let (context, str) =
- if str.[0] = '|' then ([], str) else 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) -> (C -> B) -> (A | C -> B)" ::
- "(A -> B) -> (A -> !B) -> !A" ::
- "!!A -> A":: []);;
- module ExprMap = Map.Make(struct type t = expr let compare = compare end);;
- let list_find_opt f l = try Some (List .find f l) with _ -> None;;
- let map_find_opt k m = try Some (ExprMap.find k m) with _ -> None;;
- let checkAxioms to_check = let rec func lst = match lst with
- | None :: rem_ -> func rem_
- | Some a :: _ -> Some a
- | _ -> None in
- func (List.mapi (fun ind chain -> chain to_check (None, None, None) >>= (fun _ -> Some ind)) axioms);;
- type node = Axiom of (expr * int) | MP of (expr * node * node) | Context of (expr * int);;
- let checkEverything context need evidence =
- let contextMap = List.fold_right (fun (x, ind) mp -> ExprMap.add x ind mp) (List.mapi (fun ind x -> (x, ind)) context) ExprMap.empty in
- let rec checkStepByStep alreadyHadMap possibleMap evidenceMap lst =
- match lst with
- | [] -> None
- | now :: rem_list ->
- let the_node = match map_find_opt now possibleMap with
- | Some the_node -> Some the_node
- | None -> match checkAxioms now with
- | Some ind -> Some (Axiom (now, ind))
- | None -> match map_find_opt now contextMap with
- | Some ind -> Some (Context (now, ind))
- | None -> None in
- if now = need
- then the_node
- else
- the_node >>= fun the_node ->
- let to_add = List.map (fun (_expr, _node) -> (_expr, MP (_expr, _node, the_node))) (ExprMap.fold (fun x y have -> (x, y) :: have) (takeMon (map_find_opt now evidenceMap) ExprMap.empty) []) in
- let evidenceMap = ExprMap.remove now evidenceMap in
- let (smth_to_add, new_evidenceMap) = match now with
- | Conj (a, b) -> (match map_find_opt a alreadyHadMap with
- | Some the_node1 -> ([(b, MP (b, the_node, the_node1))], evidenceMap)
- | _ -> ([], ExprMap.add a (ExprMap.add b the_node (takeMon (map_find_opt a evidenceMap) ExprMap.empty)) evidenceMap))
- | _ -> ([], evidenceMap) in
- let new_list = List.concat (smth_to_add :: to_add :: []) in
- let new_possibleMap = List.fold_right (fun (x, y) mp -> ExprMap.add x y mp) new_list possibleMap in
- let new_alreadyHadMap = ExprMap.add now the_node alreadyHadMap in
- checkStepByStep new_alreadyHadMap new_possibleMap new_evidenceMap rem_list in
- checkStepByStep ExprMap.empty ExprMap.empty ExprMap.empty evidence;;
- let rec printNodeImpl node mp nxt = match node with
- | Axiom (expr_, num) -> (match map_find_opt expr_ mp with
- | Some line -> ("", mp, line, nxt)
- | None -> ("[" ^ string_of_int nxt ^ ". Ax. sch. " ^ string_of_int (num + 1) ^ "] " ^ print_expr expr_ ^ "\n", ExprMap.add expr_ nxt mp, nxt, nxt + 1))
- | Context (expr_, num) -> (match map_find_opt expr_ mp with
- | Some line -> ("", mp, line, nxt)
- | None -> ("[" ^ string_of_int nxt ^ ". Hypothesis " ^ string_of_int (num + 1) ^ "] " ^ print_expr expr_ ^ "\n", ExprMap.add expr_ nxt mp, nxt, nxt + 1))
- | MP (expr_, node1, node2) -> (match map_find_opt expr_ mp with
- | Some line -> ("", mp, line, nxt)
- | None ->
- let (result1, mp, line1, nxt) = printNodeImpl node1 mp nxt in
- let (result2, mp, line2, nxt) = printNodeImpl node2 mp nxt in
- (result1 ^ result2 ^ "[" ^ string_of_int(nxt) ^ ". M.P. " ^ (string_of_int line1) ^ ", " ^ (string_of_int line2) ^ "] " ^ print_expr expr_ ^ "\n", ExprMap.add expr_ nxt mp, nxt, nxt + 1));;
- let printNode the_node = let (res, _, _, _) = printNodeImpl the_node ExprMap.empty 1 in res;;
- 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 parse_expr other_lines in
- match checkEverything context expr other_expr with
- | None -> "Proof is incorrect"
- | Some a -> printNode a;;
- let rec mainImpl () =
- try let cur = input_line stdin in cur :: mainImpl () with _ -> [];;
- print_string (make_evidence (mainImpl ()));;
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement