SHARE
TWEET

Untitled

a guest Sep 6th, 2019 79 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. type expr =
  2.         Implication of (expr * expr) |
  3.         Conjunction of (expr * expr) |
  4.         Disjunction of (expr * expr) |
  5.         Negation of expr |
  6.         Forall of (string * expr) |
  7.         Exists of (string * expr) |
  8.         Predicate of (string * term list) |
  9.         Equals of (term * term)
  10. and term =
  11.         Add of (term * term) |
  12.         Multiply of (term * term) |
  13.         Var of string |
  14.         Increment of term |
  15.         Zero |
  16.         Function of (string * term list)
  17. and document = Document of (expr list * expr * expr list);;
  18.  
  19. let take s ind = if String.length s <= ind || ind < 0 then None else Some (String.get s ind);;
  20.  
  21. let rec trim s =
  22.         match take s 0 with
  23.         | Some ' ' -> trim (String.sub s 1 (String.length s - 1))
  24.         | _ -> s;;
  25.  
  26. let rec trim_end s =
  27.         match take s (String.length s - 1) with
  28.         | Some ' ' | Some '\n' | Some '\t' -> trim_end (String.sub s 0 (String.length s - 1))
  29.         | _ -> s;;
  30.  
  31. let rec printTerm term =
  32.         match term with
  33.         | Add (a, b) -> "(" ^ (printTerm a) ^ "+" ^ (printTerm b) ^ ")"
  34.         | Multiply (a, b) -> "(" ^ (printTerm a) ^ "*" ^ (printTerm b) ^ ")"
  35.         | Var name -> name
  36.         | Increment a -> (printTerm a) ^ "'"
  37.         | Zero -> "0"
  38.         | Function (name, terms) -> name ^ "(" ^ (String.concat "," (List.map printTerm terms)) ^ ")";;
  39.  
  40. let rec printExpr expr =
  41.         match expr with
  42.         | Implication (a, b) -> "(" ^ (printExpr a) ^ "->" ^ (printExpr b) ^ ")"
  43.         | Conjunction (a, b) -> "(" ^ (printExpr a) ^ "&" ^ (printExpr b) ^ ")"
  44.         | Disjunction (a, b) -> "(" ^ (printExpr a) ^ "|" ^ (printExpr b) ^ ")"
  45.         | Negation a -> "!" ^ (printExpr a)
  46.         | Forall (name, e) -> "(@" ^ name ^ "." ^ (printExpr e) ^ ")"
  47.         | Exists (name, e) -> "(?" ^ name ^ "." ^ (printExpr e) ^ ")"
  48.         | Predicate (name, es) -> name ^ "(" ^ (String.concat "," (List.map printTerm es)) ^ ")"
  49.         | Equals (a, b) -> (printTerm a) ^ "=" ^ (printTerm b);;
  50.  
  51. let rec parseImplication s =
  52.         match parseDisjunction s with
  53.         | Some (dis, s) ->
  54.                 let s = trim s in
  55.                 (match (take s 0, take s 1) with
  56.                 | (Some '-', Some '>') ->
  57.                         let s = String.sub s 2 (String.length s - 2) in
  58.                         (match parseImplication s with
  59.                         | Some (impl, s) -> Some (Implication (dis, impl), s)
  60.                         | None -> None)
  61.                 | _ -> Some (dis, s))
  62.         | None -> None
  63. and parseDisjunction s =
  64.         match parseConjunction s with
  65.         | Some (conj, s) ->
  66.                 let rec func prev s =
  67.                         let s = trim s in
  68.                         match take s 0 with
  69.                         | Some '|' ->
  70.                                 let s = String.sub s 1 (String.length s - 1) in
  71.                                 (match parseConjunction s with
  72.                                 | Some (conj, s) -> func (Disjunction (prev, conj)) s
  73.                                 | None -> None)
  74.                         | _ -> Some (prev, s) in
  75.                 func conj s
  76.         | None -> None
  77. and parseConjunction s =
  78.         match parseUnary s with
  79.         | Some (unary, s) ->
  80.                 let rec func prev s =
  81.                         let s = trim s in
  82.                         match take s 0 with
  83.                         | Some '&' ->
  84.                                 let s = String.sub s 1 (String.length s - 1) in
  85.                                 (match parseUnary s with
  86.                                 | Some (unary, s) -> func (Conjunction (prev, unary)) s
  87.                                 | None -> None)
  88.                         | _ -> Some (prev, s) in
  89.                 func unary s
  90.         | None -> None
  91. and parseUnary s =
  92.         let s = trim s in
  93.         match take s 0 with
  94.         | Some '(' ->
  95.                 (match parseImplication (String.sub s 1 (String.length s - 1)) with
  96.                 | Some (impl, s) ->
  97.                         let s = trim s in
  98.                         (match take s 0 with
  99.                         | Some ')' -> Some (impl, String.sub s 1 (String.length s - 1))
  100.                         | _ -> None)
  101.                 | None -> parsePredicate s)
  102.         | Some '!' -> (match parseUnary (String.sub s 1 (String.length s - 1)) with
  103.                 | Some (unary, s) -> Some (Negation unary, s)
  104.                 | None -> None)
  105.         | Some '@' | Some '?' ->
  106.                 let construct var expr = if take s 0 = Some '@' then Forall (var, expr) else Exists (var, expr) in
  107.                 (match parseVar (String.sub s 1 (String.length s - 1)) with
  108.                 | Some (Var var, s) ->
  109.                         let s = trim s in
  110.                         (match take s 0 with
  111.                         | Some '.' ->
  112.                                 (match parseImplication (String.sub s 1 (String.length s - 1)) with
  113.                                 | Some (impl, s) -> Some (construct var impl, s)
  114.                                 | None -> None)
  115.                         | _ -> None)
  116.                 | _ -> None)
  117.  
  118.         | _ ->
  119.                 parsePredicate s
  120. and parseVar s =
  121.         let s = trim s in
  122.         match take s 0 with
  123.         | Some a ->
  124.                 (match a with
  125.                 | 'a'..'z' ->
  126.                         let rec func have s =
  127.                                 match take s 0 with
  128.                                 | Some a ->
  129.                                         (match a with
  130.                                         | '0'..'9' ->
  131.                                                 func (have ^ (Char.escaped a)) (String.sub s 1 (String.length s - 1))
  132.                                         | _ -> (have, s))
  133.                                 | None -> (have, s) in
  134.                         let (name, s) = func (Char.escaped a) (String.sub s 1 (String.length s - 1)) in
  135.                         Some (Var name, s)
  136.                 | _ -> None)
  137.         | None -> None
  138. and parsePredicate s =
  139.         let s = trim s in
  140.         match take s 0 with
  141.         | Some a ->
  142.                 (match a with
  143.                 | 'A'..'Z' ->
  144.                         let rec func have s =
  145.                                 match take s 0 with
  146.                                 | Some a ->
  147.                                         (match a with
  148.                                         | '0'..'9' -> func (have ^ Char.escaped a) (String.sub s 1 (String.length s - 1))
  149.                                         | _ -> (have, s))
  150.                                 | None -> (have, s) in
  151.                         let (name, s) = func (Char.escaped a) (String.sub s 1 (String.length s - 1)) in
  152.                         (match take s 0 with
  153.                         | Some '(' ->
  154.                                 let s = String.sub s 1 (String.length s - 1) in
  155.                                 (match parseTerm s with
  156.                                 | Some (term, s) ->
  157.                                         let rec func s =
  158.                                                 let s = trim s in
  159.                                                 match take s 0 with
  160.                                                 | Some ',' ->
  161.                                                         (match parseTerm (String.sub s 1 (String.length s - 1)) with
  162.                                                         | Some (term, s) ->
  163.                                                                 (match func s with
  164.                                                                 | Some (terms, s) ->
  165.                                                                         Some (term :: terms, s)
  166.                                                                 | None -> None)
  167.                                                         | None -> None)
  168.                                                 | _ -> Some ([], s) in
  169.                                         (match func s with
  170.                                         | Some (terms, s) ->
  171.                                                 let s = trim s in
  172.                                                 (match take s 0 with
  173.                                                 | Some ')' ->
  174.                                                         Some (Predicate (name, term :: terms), String.sub s 1 (String.length s - 1))
  175.                                                 | _ -> None)
  176.                                         | None -> None)
  177.                                 | None -> None)
  178.                         | _ -> None)
  179.                 | _ ->
  180.                         (match parseTerm s with
  181.                         | Some (term, s) ->
  182.                                 let s = trim s in
  183.                                 (match take s 0 with
  184.                                 | Some '=' ->
  185.                                         (match parseTerm (String.sub s 1 (String.length s - 1)) with
  186.                                         | Some (term1, s) ->
  187.                                                 Some (Equals (term, term1), s)
  188.                                         | None -> None)
  189.                                 | _ -> None)
  190.                         | None -> None))
  191.         | None -> None
  192. and parseTerm s =
  193.         match parseSummand s with
  194.         | Some (summand, s) ->
  195.                 let rec func have s =
  196.                         let s = trim s in
  197.                         match take s 0 with
  198.                         | Some '+' ->
  199.                                 let s = String.sub s 1 (String.length s - 1) in
  200.                                 (match parseSummand s with
  201.                                 | Some (summand, s) ->
  202.                                         func (Add (have, summand)) s
  203.                                 | None -> None)
  204.                         | _ -> Some (have, s) in
  205.                 func summand s
  206.         | None -> None
  207. and parseSummand s =
  208.         match parseInc s with
  209.         | Some (mul, s) ->
  210.                 let rec func have s =
  211.                         let s = trim s in
  212.                         match take s 0 with
  213.                         | Some '*' ->
  214.                                 let s = String.sub s 1 (String.length s - 1) in
  215.                                 (match parseInc s with
  216.                                 | Some (mul, s) ->
  217.                                         func (Multiply (have, mul)) s
  218.                                 | None -> None)
  219.                         | _ -> Some (have, s) in
  220.                 func mul s
  221.         | None -> None
  222. and parseInc s =
  223.         match parseMultiplying s with
  224.         | Some (now, s) ->
  225.                 let rec func have s =
  226.                         let s = trim s in
  227.                         match take s 0 with
  228.                         | Some '\'' ->
  229.                                 func (Increment have) (String.sub s 1 (String.length s - 1))
  230.                         | _ -> (have, s) in
  231.                 let (now, s) = func now s in
  232.                 Some (now, s)
  233.         | None -> None
  234. and parseMultiplying s =
  235.         let s = trim s in
  236.         match take s 0 with
  237.         | Some a ->
  238.                 (match a with
  239.                 | '0' -> Some (Zero, String.sub s 1 (String.length s - 1))
  240.                 | '(' ->
  241.                         let s = String.sub s 1 (String.length s - 1) in
  242.                         (match parseTerm s with
  243.                         | Some (term, s) ->
  244.                                 let s = trim s in
  245.                                 (match take s 0 with
  246.                                 | Some ')' ->
  247.                                         Some (term, String.sub s 1 (String.length s - 1))
  248.                                 | _ -> None)
  249.                         | None -> None)
  250.                 | _ ->
  251.                         (match parseVar s with
  252.                         | Some (Var name, s) ->
  253.                                 (match take s 0 with
  254.                                 | Some '(' ->
  255.                                         let s = String.sub s 1 (String.length s - 1) in
  256.                                         (match parseTerm s with
  257.                                         | Some (term, s) ->
  258.                                                 let rec func s =
  259.                                                         let s = trim s in
  260.                                                         match take s 0 with
  261.                                                         | Some ',' ->
  262.                                                                 (match parseTerm (String.sub s 1 (String.length s - 1)) with
  263.                                                                 | Some (term, s) ->
  264.                                                                         (match func s with
  265.                                                                         | Some (terms, s) ->
  266.                                                                                 Some (term :: terms, s)
  267.                                                                         | None -> None)
  268.                                                                 | None -> None)
  269.                                                         | _ -> Some ([], s) in
  270.                                                 (match func s with
  271.                                                 | Some (terms, s) ->
  272.                                                         let s = trim s in
  273.                                                         (match take s 0 with
  274.                                                         | Some ')' ->
  275.                                                                 Some (Function (name, term :: terms), String.sub s 1 (String.length s - 1))
  276.                                                         | _ -> None)
  277.                                                 | None -> None)
  278.                                         | None -> None)
  279.                                 | _ -> Some (Var name, s))
  280.                         | _ -> None))
  281.         | None -> None;;
  282.  
  283. let parse s =
  284.         match parseImplication s with
  285.         | Some (expr, s) ->
  286.                 let s = trim s in
  287.                 if String.length s = 0 then Some expr else None
  288.         | None -> None;;
  289.  
  290. let find_barrier s =
  291.         let rec find_barrier_int s ind =
  292.                 match take s 0 with
  293.                 | Some '|' ->
  294.                         (match take s 1 with
  295.                         | Some '-' ->
  296.                                 Some ind
  297.                         | _ ->
  298.                                 find_barrier_int (String.sub s 1 (String.length s - 1)) (ind + 1))
  299.                 | Some a ->
  300.                         find_barrier_int (String.sub s 1 (String.length s - 1)) (ind + 1)
  301.                 | None -> None in
  302.         find_barrier_int s 0;;
  303.  
  304. let parseDocument s =
  305.         let rec func c s =
  306.                 match parseImplication s with
  307.                 | Some (impl, s) ->
  308.                         let s = trim s in
  309.                         if take s 0 = Some c then
  310.                                 (match func c (String.sub s 1 (String.length s - 1)) with
  311.                                 | Some (last, s) ->
  312.                                         Some (impl :: last, s)
  313.                                 | None -> None)
  314.                         else if take s 0 = None then
  315.                                 Some (impl :: [], s)
  316.                         else None
  317.                 | None -> None in
  318.         match find_barrier s with
  319.         | Some ind ->
  320.                 let s1 = trim (String.sub s 0 ind) in
  321.                 let s = trim_end (trim (String.sub s (ind + 2) (String.length s - ind - 2))) in
  322.                 (match ((if String.length s1 = 0 then Some ([], "") else func ',' s1), func '\n' s) with
  323.                 | (Some (d1, _) , Some (d2 :: d3, _)) ->
  324.                         Some (Document (d1, d2, d3))
  325.                 | _ -> None)
  326.         | None -> None;;
  327.  
  328. let printDocument (Document (d1, d2, d3)) = (String.concat "," (List.map printExpr d1)) ^ "|-" ^ (printExpr d2) ^ "\n" ^ (String.concat "\n" (List.map printExpr d3));;
  329.  
  330. let parse_bad s =
  331.         match parse s with
  332.         | Some x -> x
  333.         | None -> failwith "Bad expression"
  334. and parseDocument_bad s =
  335.         match parseDocument s with
  336.         | Some x -> x
  337.         | None -> failwith "Bad document";;
  338.  
  339. let rawSchemes =
  340.         ["A(0) -> B(0) -> A(0)";
  341.         "(A(0) -> B(0)) -> (A(0) -> B(0) -> C(0)) -> (A(0) -> C(0))";
  342.         "A(0) -> B(0) -> A(0) & B(0)";
  343.         "A(0) & B(0) -> A(0)";
  344.         "A(0) & B(0) -> B(0)";
  345.         "A(0) -> A(0) | B(0)";
  346.         "B(0) -> A(0) | B(0)";
  347.         "(A(0) -> C(0)) -> (B(0) -> C(0)) -> (A(0) | B(0) -> C(0))";
  348.         "(A(0) -> B(0)) -> (A(0) -> !B(0)) -> !A(0)";
  349.         "!!A(0) -> A(0)"];;
  350.  
  351. let schemes = List.map parse_bad rawSchemes;;
  352.  
  353. let rawAxioms =
  354.         ["a = b -> a' = b'";
  355.         "a = b -> a = c -> b = c";
  356.         "a' = b' -> a = b";
  357.         "!a' = 0";
  358.         "a + b' = (a + b)'";
  359.         "a + 0 = a";
  360.         "a * 0 = 0";
  361.         "a * b' = a * b + a"];;
  362.  
  363. let axioms = List.map parse_bad rawAxioms;;
  364.  
  365. module StringMap = Map.Make(String);;
  366. module ExprMap = Map.Make(struct type t = expr let compare = compare end);;
  367. module ExprSet = Set.Make(struct type t = expr let compare = compare end);;
  368. module StringSet = Set.Make(String);;
  369.  
  370. let rec freeVars e =
  371.         match e with
  372.         | Implication (a, b) | Conjunction (a, b) | Disjunction (a, b) ->
  373.                 StringSet.union (freeVars a) (freeVars b)
  374.         | Negation a ->
  375.                 freeVars a
  376.         | Exists (name, a) | Forall (name, a) ->
  377.                 StringSet.remove name (freeVars a)
  378.         | Predicate (_, l) ->
  379.                 List.fold_left (fun m a -> StringSet.union m (freeVarsTerm a)) StringSet.empty l
  380.         | Equals (a, b) ->
  381.                 StringSet.union (freeVarsTerm a) (freeVarsTerm b)
  382. and freeVarsTerm t =
  383.         match t with
  384.         | Add (a, b) | Multiply (a, b) ->
  385.                 StringSet.union (freeVarsTerm a) (freeVarsTerm b)
  386.         | Var name ->
  387.                 StringSet.singleton name
  388.         | Increment a ->
  389.                 freeVarsTerm a
  390.         | Zero ->
  391.                 StringSet.empty
  392.         | Function (_, l) ->
  393.                 List.fold_left (fun m a -> StringSet.union m (freeVarsTerm a)) StringSet.empty l;;
  394.  
  395. let upperPred e name =
  396.         let rec upperPredExpr e name =
  397.                 match e with
  398.                 | Implication (a, b) | Conjunction (a, b) | Disjunction (a, b) ->
  399.                         (match (upperPredExpr a name, upperPredExpr b name) with
  400.                         | (None, None) -> None
  401.                         | (a, b) -> Some (StringSet.union (takeOr a) (takeOr b)))
  402.                 | Negation a ->
  403.                         upperPredExpr a name
  404.                 | Exists (var, a) | Forall (var, a) ->
  405.                         (match upperPredExpr a name with
  406.                         | None -> None
  407.                         | Some b -> Some (StringSet.add var b))
  408.                 | Predicate (_, l) ->
  409.                         List.fold_left (fun m a ->
  410.                                 match m with
  411.                                 | None -> upperPredTerm a name
  412.                                 | Some b ->
  413.                                         Some (StringSet.union b (takeOr (upperPredTerm a name)))) None l
  414.                 | Equals (a, b) ->
  415.                         (match (upperPredTerm a name, upperPredTerm b name) with
  416.                         | (None, None) -> None
  417.                         | (a, b) -> Some (StringSet.union (takeOr a) (takeOr b)))
  418.         and upperPredTerm t name =
  419.                 match t with
  420.                 | Add (a, b) | Multiply (a, b) ->
  421.                         (match (upperPredTerm a name, upperPredTerm b name) with
  422.                         | (None, None) -> None
  423.                         | (a, b) -> Some (StringSet.union (takeOr a) (takeOr b)))
  424.                 | Var var ->
  425.                         if var = name then Some StringSet.empty else None
  426.                 | Increment a ->
  427.                         upperPredTerm a name
  428.                 | Zero ->
  429.                         None
  430.                 | Function (_, l) ->
  431.                         List.fold_left (fun m a ->
  432.                                 match m with
  433.                                 | None -> upperPredTerm a name
  434.                                 | Some b ->
  435.                                         Some (StringSet.union b (takeOr (upperPredTerm a name)))) None l
  436.  
  437.         and takeOr a =
  438.                 match a with
  439.                 | Some b -> b
  440.                 | None -> StringSet.empty in
  441.         takeOr (upperPredExpr e name);;
  442.  
  443. let println_string s = print_string (s ^ "\n");;
  444.  
  445. let rec transformTerm e was became =
  446.         let rec transform t =
  447.                 if t = was then became else
  448.                         match t with
  449.                         | Add (a, b) ->
  450.                                 Add (transform a, transform b)
  451.                         | Multiply (a, b) ->
  452.                                 Multiply (transform a, transform b)
  453.                         | Var name ->
  454.                                 Var name
  455.                         | Increment a ->
  456.                                 Increment (transform a)
  457.                         | Zero ->
  458.                                 Zero
  459.                         | Function (name, l) ->
  460.                                 Function (name, List.map transform l) in
  461.         let rec func e =
  462.                 match e with
  463.                 | Implication (a, b) ->
  464.                         Implication (func a, func b)
  465.                 | Conjunction (a, b) ->
  466.                         Conjunction (func a, func b)
  467.                 | Disjunction (a, b) ->
  468.                         Disjunction (func a, func b)
  469.                 | Negation a ->
  470.                         Negation (func a)
  471.                 | Forall (var, a) ->
  472.                         Forall (var, func a)
  473.                 | Exists (var, a) ->
  474.                         Exists (var, func a)
  475.                 | Predicate (name, l) ->
  476.                         Predicate (name, List.map (fun e -> transform e) l)
  477.                 | Equals (a, b) ->
  478.                         Equals (transform a, transform b) in
  479.         func e
  480. and transformExpr e was became =
  481.         let rec func e =
  482.                 if e = was then became else
  483.                         match e with
  484.                         | Implication (a, b) ->
  485.                                 Implication (func a, func b)
  486.                         | Conjunction (a, b) ->
  487.                                 Conjunction (func a, func b)
  488.                         | Disjunction (a, b) ->
  489.                                 Disjunction (func a, func b)
  490.                         | Negation a ->
  491.                                 Negation (func a)
  492.                         | Forall (var, a) ->
  493.                                 Forall (var, func a)
  494.                         | Exists (var, a) ->
  495.                                 Exists (var, func a)
  496.                         | Predicate (name, l) ->
  497.                                 Predicate (name, l)
  498.                         | Equals (a, b) ->
  499.                                 Equals (a, b) in
  500.         func e;;
  501.  
  502. let rec findTerm e1 e2 need =
  503.         let rec find t1 t2 =
  504.                 if t1 = need then Some t2 else
  505.                         match (t1, t2) with
  506.                         | (Add (a1, b1), Add (a2, b2)) | (Multiply (a1, b1), Multiply (a2, b2)) ->
  507.                                 let res = find a1 a2 in
  508.                                 if res = None then find b1 b2 else res
  509.                         | (Increment a1, Increment a2) ->
  510.                                 find a1 a2
  511.                         | (Function (name1, l1), Function (name2, l2)) ->
  512.                                 if name1 = name2 then
  513.                                         if List.length l1 = List.length l2 then
  514.                                                 List.fold_left (fun a (b1, b2) ->
  515.                                                         match a with
  516.                                                         | Some c -> Some c
  517.                                                         | None -> find b1 b2) None (List.combine l1 l2)
  518.                                         else None
  519.                                 else None
  520.                         | (_, _) -> None in
  521.         let rec func e1 e2 =
  522.                 match (e1, e2) with
  523.                 | (Implication (a1, b1), Implication (a2, b2))
  524.                 | (Conjunction (a1, b1), Conjunction (a2, b2))
  525.                 | (Disjunction (a1, b1), Disjunction (a2, b2)) ->
  526.                         let res = func a1 a2 in
  527.                         if res = None then func b1 b2 else res
  528.                 | (Negation a1, Negation a2) ->
  529.                         func a1 a2
  530.                 | (Forall (var1, a1), Forall (var2, a2))
  531.                 | (Exists (var1, a1), Exists (var2, a2)) ->
  532.                         if var1 = var2 then func a1 a2 else None
  533.                 | (Predicate (name1, l1), Predicate (name2, l2)) ->
  534.                         if name1 = name2 then
  535.                                 if List.length l1 = List.length l2 then
  536.                                         List.fold_left (fun a (b1, b2) ->
  537.                                                 match a with
  538.                                                 | Some c -> Some c
  539.                                                 | None -> find b1 b2) None (List.combine l1 l2)
  540.                                 else None
  541.                         else None
  542.                 | (Equals (a1, b1), Equals (a2, b2)) ->
  543.                         let res = find a1 a2 in
  544.                         if res = None then find b1 b2 else res
  545.                 | (_, _) -> None in
  546.         func e1 e2
  547. and findExpr e1 e2 need =
  548.         let rec func e1 e2 =
  549.                 if e1 = need then Some e2 else
  550.                         match (e1, e2) with
  551.                         | (Implication (a1, b1), Implication (a2, b2))
  552.                         | (Conjunction (a1, b1), Conjunction (a2, b2))
  553.                         | (Disjunction (a1, b1), Disjunction (a2, b2)) ->
  554.                                 let res = func a1 a2 in
  555.                                 if res = None then func b1 b2 else res
  556.                         | (Negation a1, Negation a2) ->
  557.                                 func a1 a2
  558.                         | (Forall (var1, a1), Forall (var2, a2))
  559.                         | (Exists (var1, a1), Exists (var2, a2)) ->
  560.                                 if var1 = var2 then func a1 a2 else None
  561.                         | (_, _) -> None in
  562.         func e1 e2;;
  563.  
  564. let is_scheme_axiom e ax =
  565.         let func e was became =
  566.                 match became with
  567.                 | None -> e
  568.                 | Some became -> transformExpr e was became in
  569.         let a = findExpr ax e (Predicate ("A", [Zero])) in
  570.         let b = findExpr ax e (Predicate ("B", [Zero])) in
  571.         let c = findExpr ax e (Predicate ("C", [Zero])) in
  572.         let za = func ax (Predicate ("A", [Zero])) a in
  573.         let zb = func za (Predicate ("B", [Zero])) b in
  574.         let zc = func zb (Predicate ("C", [Zero])) c in
  575.         zc = e;;
  576.  
  577. let enumerate l =
  578.         let rec func l a =
  579.                 match l with
  580.                 | [] -> []
  581.                 | x :: xs -> (x, a) :: (func xs (a + 1)) in
  582.         func l 0;;
  583.  
  584. let which_scheme_axiom e =
  585.         let eschemes = enumerate schemes in
  586.         let axs = List.map (fun (a, num) -> if is_scheme_axiom e a then Some num else None) eschemes in
  587.         List.fold_left (fun was now ->
  588.                 match was with
  589.                 | None -> now
  590.                 | Some a -> Some a) None axs;;
  591.  
  592. let print_scheme_number e =
  593.         match which_scheme_axiom e with
  594.         | None -> -1
  595.         | Some a -> a;;
  596.  
  597. let check11 e =
  598.         match e with
  599.         | Implication (Forall (var, c), b) ->
  600.                 (match findTerm c b (Var var) with
  601.                 | Some expr ->
  602.                         if StringSet.is_empty (StringSet.inter (freeVarsTerm expr) (upperPred c var)) then
  603.                                 transformTerm c (Var var) expr = b
  604.                         else false
  605.                 | None -> false)
  606.         | _ -> false;;
  607.  
  608. let check12 e =
  609.         match e with
  610.         | Implication (b, Exists (var, c)) ->
  611.                 (match findTerm c b (Var var) with
  612.                 | Some expr ->
  613.                         if StringSet.is_empty (StringSet.inter (freeVarsTerm expr) (upperPred c var)) then
  614.                                 transformTerm c (Var var) expr = b
  615.                         else false
  616.                 | None -> false)
  617.         | _ -> false;;
  618.  
  619. let checkInduction e =
  620.         match e with
  621.         | Implication (Conjunction (s, Forall (var, bb)), res) ->
  622.                 s = (transformTerm res (Var var) Zero) && bb = (Implication (res, transformTerm res (Var var) (Increment (Var var))))
  623.         | _ -> false;;
  624.  
  625. let checkAllAxioms e =
  626.         match which_scheme_axiom e with
  627.         | Some a -> Some ("Scheme " ^ (string_of_int (a + 1)))
  628.         | None ->
  629.                 if check11 e then Some "Scheme 11" else
  630.                 if check12 e then Some "Scheme 12" else
  631.                 if checkInduction e then Some "Induction" else
  632.                 let eaxioms = enumerate axioms in
  633.                 match List.find_opt (fun (now, _) -> now = e) eaxioms with
  634.                 | Some (_, num) -> Some ("Axiom " ^ (string_of_int (num + 1)))
  635.                 | None -> None;;
  636.  
  637. let printAllAxioms e =
  638.         match checkAllAxioms e with
  639.         | None -> "Nothing"
  640.         | Some a -> a;;
  641.  
  642. let rec checkProof (Document (was, need, proof)) =
  643.         let wasExprs = List.fold_left (fun set x -> ExprSet.add x set) ExprSet.empty was in
  644.         let func was needLeft needRight e =
  645.                 if match checkAllAxioms e with
  646.                 | Some _ -> true
  647.                 | None ->
  648.                         match e with
  649.                         | Implication (a, Forall (x, b)) ->
  650.                                 if (List.exists (fun v -> v = x) (StringSet.elements (freeVars a)) = false) && (ExprSet.mem (Implication (a, b)) was) then true
  651.                                 else (ExprSet.mem e wasExprs) || (ExprSet.mem e needRight)
  652.                         | Implication (Exists (x, b), a) ->
  653.                                 if (List.exists (fun v -> v = x) (StringSet.elements (freeVars a)) = false) && (ExprSet.mem (Implication (b, a)) was) then true
  654.                                 else (ExprSet.mem e wasExprs) || (ExprSet.mem e needRight)
  655.                         | _ ->
  656.                                 (ExprSet.mem e wasExprs) || (ExprSet.mem e needRight) then
  657.                         let was = ExprSet.add e was in
  658.                         let (needLeft, needRight) =
  659.                                 match ExprMap.find_opt e needLeft with
  660.                                 | Some l ->
  661.                                         (ExprMap.remove e needLeft, List.fold_left (fun need x -> ExprSet.add x need) needRight l)
  662.                                 | None ->
  663.                                         (needLeft, needRight) in
  664.                         let (needLeft, needRight) =
  665.                                 match e with
  666.                                 | Implication (a, b) ->
  667.                                         if ExprSet.mem a was then (needLeft, ExprSet.add b needRight)
  668.                                         else (ExprMap.add a (b :: (match ExprMap.find_opt a needLeft with
  669.                                         | Some a -> a
  670.                                         | None -> [])) needLeft, needRight)
  671.                                 | _ ->
  672.                                         (needLeft, needRight) in
  673.                         Some (was, needLeft, needRight)
  674.                 else None in
  675.         let rec repeat eproof was needLeft needRight =
  676.                 match eproof with
  677.                 | (x, num) :: xs ->
  678.                         (match func was needLeft needRight x with
  679.                         | Some (was, needLeft, needRight) ->
  680.                                 repeat xs was needLeft needRight
  681.                         | None -> Some num)
  682.                 | [] -> None in
  683.         match repeat (enumerate proof) ExprSet.empty ExprMap.empty ExprSet.empty with
  684.         | Some num -> "Line " ^ (string_of_int (num + 1)) ^ " can't be obtained"
  685.         | None -> if List.exists (fun v -> v = need) proof then "Proof is correct" else "Required hasn't been proven";;
  686.  
  687. let rec readDocument () =
  688.     try let x = input_line stdin in x :: readDocument () with _ -> [];;
  689.  
  690. let rec parseL l =
  691.         match l with
  692.         | x :: xs ->
  693.                 (match parse x with
  694.                 | Some _ -> parseL xs
  695.                 | None -> "Error on " ^ x)
  696.         | [] -> "No errors";;
  697.  
  698. (*print_string (parseL (List.tl (readDocument ())));;*)
  699.  
  700. print_string (checkProof (parseDocument_bad (String.concat "\n" (readDocument ()))));;
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top