open Final let test_final_1_1 ctxt = assert (occurs_check (var "X") (var "X")) let test_final_1_2 ctxt = assert (not (occurs_check (var "X") (var "Y"))) let test_final_1_3 ctxt = assert (occurs_check...

This ia an Ocaml Final Project


open Final let test_final_1_1 ctxt = assert (occurs_check (var "X") (var "X")) let test_final_1_2 ctxt = assert (not (occurs_check (var "X") (var "Y"))) let test_final_1_3 ctxt = assert (occurs_check (var "X") (func "f" [var "X"])) let test_final_1_4 ctxt = assert (occurs_check (var "E") (func "cons" [const "a"; const "b"; var "E"])) let test_final_2_1 ctxt = assert (VarSet.equal (variables_of_term (func "f" [var "X"; var "Y"; const "a"])) (VarSet.of_list [var "X"; var "Y"])) let test_final_2_2 ctxt = assert (VarSet.equal (variables_of_term (func "p" [var "X"; var "Y"; const "a"])) (VarSet.of_list [var "X"; var "Y"])) let test_final_2_3 ctxt = assert (VarSet.equal (variables_of_clause (fact (func "p" [var "X"; var "Y"; const "a"]))) (VarSet.of_list [var "X"; var "Y"])) let test_final_2_4 ctxt = assert (VarSet.equal (variables_of_clause (rule (func "p" [var "X"; var "Y"; const "a"]) [func "q" [const "a"; const "b"; const "a"]])) (VarSet.of_list [var "X"; var "Y"])) let s = Substitution.add (var "Y") (const "0") (Substitution.add (var "X") (var "Y") Substitution.empty) let test_final_3_1 ctxt = assert (substitute_in_term s (func "f" [var "X"; var "Y"; const "a"]) = func "f" [var "Y"; const "0"; const "a"]) let test_final_3_2 ctxt = assert (substitute_in_term s (func "p" [var "X"; var "Y"; const "a"]) = func "p" [var "Y"; const "0"; const "a"]) let test_final_3_3 ctxt = assert (substitute_in_clause s (fact (func "p" [var "X"; var "Y"; const "a"])) = (fact (func "p" [var "Y"; const "0"; const "a"]))) let test_final_3_4 ctxt = assert (substitute_in_clause s (rule (func "p" [var "X"; var "Y"; const "a"]) [func "q" [const "a"; const "b"; const "a"]]) = (rule (func "p" [var "Y"; const "0"; const "a"]) [func "q" [const "a"; const "b"; const "a"]])) let test_final_4_1 ctxt = assert ((unify (var "X") (var "Y")) = Substitution.singleton (var "Y") (var "X") || (unify (var "X") (var "Y")) = Substitution.singleton (var "X") (var "Y")) let test_final_4_2 ctxt = assert ((unify (var "Y") (var "X")) = Substitution.singleton (var "X") (var "Y") || (unify (var "Y") (var "X")) = Substitution.singleton (var "Y") (var "X")) let test_final_4_3 ctxt = assert (unify (var "Y") (var "Y") = Substitution.empty) let test_final_4_4 ctxt = assert (unify (const "0") (const "0") = Substitution.empty) let test_final_4_5 ctxt = assert (unify (const "0") (var "Y") = Substitution.singleton (var "Y") (const "0")) let test_final_4_6 ctxt = assert ( match unify (const "0") (const "1") with | _ -> false | exception Not_unifiable -> true) let test_final_4_7 ctxt = assert ( match unify (func "f" [const "0"]) (func "g" [const "1"]) with | _ -> false | exception Not_unifiable -> true) let test_final_4_8 ctxt = assert (unify (func "f" [var "X"]) (func "f" [var "Y"]) = Substitution.singleton (var "X") (var "Y") || unify (func "f" [var "X"]) (func "f" [var "Y"]) = Substitution.singleton (var "Y") (var "X")) let s9 = Substitution.add (var "Z") (const "a") (Substitution.add (var "Y") (const "a") (Substitution.add (var "X") (const "a") Substitution.empty)) let test_final_4_9 ctxt = let t1 = Function("f", [Variable "X"; Variable "Y"; Variable "Y"]) in let t2 = Function("f", [Variable "Y"; Variable "Z"; Constant "a"]) in let u = unify t1 t2 in assert (Substitution.equal (=) u s9) (* Test on a simple program *) let psimple = [fact @@ func "f" [const "a"; const "b"]] let test_final_5_1 ctxt = let _ = print_endline "Testing the non-deterministic abstract interpreter" in let _ = print_endline ("Program:\n" ^ (string_of_program psimple)) in let g = [func "f" [const "a"; const "b"]] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query psimple g in assert (g' = [func "f" [const "a"; const "b"]]); print_endline ("Solution:\n" ^ (string_of_goal g')) let test_final_5_2 ctxt = let g = [func "f" [var "X"; const "b"]] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query psimple g in assert (g' = [func "f" [const "a"; const "b"]]); print_endline ("Solution:\n" ^ (string_of_goal g')) let test_final_5_3 ctxt = let g = [func "f" [var "X"; var "Y"]] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query psimple g in assert (g' = [func "f" [const "a"; const "b"]]); print_endline ("Solution:\n" ^ (string_of_goal g') ^ "\n") (* Test on the House Stark program *) let ancestor x y = func "ancestor" [x;y] let father x y = func "father" [x;y] let father_consts x y = father (Constant x) (Constant y) let f1 = Fact (father_consts "rickard" "ned") let f2 = Fact (father_consts "ned" "robb") let r1 = Rule (ancestor (var "X") (var "Y"), [father (var "X") (var "Y")]) let r2 = Rule (ancestor (var "X") (var "Y"), [father (var "X") (var "Z"); ancestor (var "Z") (var "Y")]) let pstark = [f1;f2;r1;r2] let test_final_5_4 ctxt = let _ = print_endline ("Program:\n" ^ (string_of_program pstark)) in let g = [ancestor (const "rickard") (const "ned")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query pstark g in print_endline ("Solution:\n" ^ string_of_goal g'); assert (g' = [ancestor (const "rickard") (const "ned")]) let test_final_5_5 ctxt = let g = [ancestor (const "rickard") (const "robb")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query pstark g in print_endline ("Solution:\n" ^ (string_of_goal g')); assert (g' = [ancestor (const "rickard") (const "robb")]) let test_final_5_6 ctxt = let g = [ancestor (var "X") (const "robb")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query pstark g in print_endline ("Solution:\n" ^ (string_of_goal g') ^ "\n"); assert (g' = [ancestor (const "ned") (const "robb")] || g' = [ancestor (const "rickard") (const "robb")]) (* Test on the list append program *) let nil = const "nil" let cons h t = func "cons" [h;t] let append x y z = func "append" [x;y;z] let c1 = fact @@ append nil (var "Q") (var "Q") let c2 = rule (append (cons (var "H") (var "P")) (var "Q") (cons (var "H") (var "R"))) [append (var "P") (var "Q") (var "R")] let pappend = [c1;c2] let test_final_5_7 ctxt = let _ = print_endline ("Program:\n" ^ (string_of_program pappend)) in let g = [append (var "X") (var "Y") (cons (const "1") (cons (const "2") (cons (const "3") nil)))] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = nondet_query pappend g in print_endline ("Solution:\n" ^ (string_of_goal g') ^ "\n"); assert ( g' = [append nil (cons (const "1") (cons (const "2") (cons (const "3") nil))) (cons (const "1") (cons (const "2") (cons (const "3") nil)))] || g' = [append (cons (const "1") nil) (cons (const "2") (cons (const "3") nil)) (cons (const "1") (cons (const "2") (cons (const "3") nil)))] || g' = [append (cons (const "1") (cons (const "2") nil)) (cons (const "3") nil) (cons (const "1") (cons (const "2") (cons (const "3") nil)))] || g' = [append (cons (const "1") (cons (const "2") (cons (const "3") nil))) nil (cons (const "1") (cons (const "2") (cons (const "3") nil)))] ) (* Test on the simple program *) let test_final_bonus_1 ctxt = let _ = print_endline "Testing the deterministic interpreter" in let _ = print_endline ("Program:\n" ^ (string_of_program psimple)) in (* Tests query failure *) let g = [func "f" [const "a"; const "c"]] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in assert (det_query psimple g = []); print_endline ("Solution:\n" ^ "Empty solution\n") (* Test on the Stark House program *) let test_final_bonus_2 ctxt = let _ = print_endline ("Program:\n" ^ (string_of_program pstark)) in (* Tests backtracking *) let g = [ancestor (const "rickard") (const "robb")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = match det_query pstark g with [v] -> v | _ -> failwith "error" in print_endline ("Solution:\n" ^ (string_of_goal g')); assert (g' = g) let test_final_bonus_3 ctxt = (* Tests choice points *) let g = [ancestor (var "X") (const "robb")] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g1,g2 = match det_query pstark g with [v1;v2] -> v1,v2 | _ -> failwith "error" in print_endline ("Solution:\n" ^ (string_of_goal g1)); print_endline ("Solution:\n" ^ (string_of_goal g2) ^ "\n"); assert (g1 = [ancestor (const "ned") (const "robb")]); assert (g2 = [ancestor (const "rickard") (const "robb")]) (* Test on the list append program *) let test_final_bonus_4 ctxt = let _ = print_endline ("Program:\n" ^ (string_of_program pappend)) in (* Tests choice points *) let g = [append (var "X") (var "Y") (cons (const "1") (cons (const "2") (cons (const "3") nil)))] in let _ = print_endline ("Goal:\n" ^ (string_of_goal g)) in let g' = det_query pappend g in assert (List.length g' = 4); List.iter (fun g -> print_endline ("Solution:\n" ^ (string_of_goal g))) g' let _ = test_final_1_1 (); test_final_1_2 (); test_final_1_3 (); test_final_1_4 (); test_final_2_1 (); test_final_2_2 (); test_final_2_3 (); test_final_2_4 (); test_final_3_1 (); test_final_3_2 (); test_final_3_3 (); test_final_3_4 (); test_final_4_1 (); test_final_4_2 (); test_final_4_3 (); test_final_4_4 (); test_final_4_5 (); test_final_4_6 (); test_final_4_7 (); test_final_4_8 (); test_final_4_9 (); test_final_5_1 (); test_final_5_2 (); test_final_5_3 (); test_final_5_4 (); test_final_5_5 (); test_final_5_6 (); test_final_5_7 () (* ; test_final_bonus_1 (); test_final_bonus_2 (); test_final_bonus_3 (); test_final_bonus_4 () *) let _ = Printf.printf "All tests passed.\n" Important notes about grading: 1. Compiler errors:​ All code you submit must compile. Programs that do not compile will receive an automatic zero. If you run out of time, it is better to comment out the parts that do not compile, than hand in a more complete file that does not compile. 2. Late assignments:​ You must submit your code before the deadline. Verify on Sakai that you have submitted the correct version. If you submit the incorrect version before the