5 Problems. Due asap.
dune-workspace
(lang dune 1.0)
(context default)
(profile release)
_tags
dune-project
(lang dune 1.0)
Makefile
build: main
main: main.byte
%.native: src/*.*
@ocamlbuild $@
%.byte: src/*.*
@ocamlbuild -tag debug $@
clean:
@ocamlbuild -clean
dune
(library
(name cs314)
(modules final))
final.ml
open Stdlib
let _ = Random.self_init ()
type term =
| Constant of string
| Variable of string
| Function of string * term list
type head = term
type body = term list
type clause = Fact of head | Rule of head * body
type program = clause list
type goal = term list
let rec string_of_f_list f tl =
let _, s = List.fold_left (fun (first, s) t ->
let prefix = if first then “” else s ^ “, ” in
false, prefix ^ (f t)) (true,””) tl
in
s
let rec string_of_term t =
match t with
| Constant c -> c
| Variable v -> v
| Function (f,tl) ->
f ^ “(” ^ (string_of_f_list string_of_term tl) ^ “)”
let string_of_term_list fl =
string_of_f_list string_of_term fl
let string_of_goal g =
“?- ” ^ (string_of_term_list g)
let string_of_clause c =
match c with
| Fact f -> string_of_term f ^ “.”
| Rule (h,b) -> string_of_term h ^ ” :- ” ^ (string_of_term_list b) ^ “.”
let string_of_program p =
let rec loop p acc =
match p with
| [] -> acc
| [c] -> acc ^ (string_of_clause c)
| c::t -> loop t (acc ^ (string_of_clause c) ^ “\n”)
in loop p “”
let var v = Variable v
let const c = Constant c
let func f l = Function (f,l)
let fact f = Fact f
let rule h b = Rule (h,b)
(* Problem 1 *)
let rec occurs_check v t =
raise (Failure “Problem 1 Not implemented”)
(* Problem 2 *)
module VarSet = Set.Make(struct type t = term let compare = Stdlib.compare end)
(* API Docs for Set : https://caml.inria.fr/pub/docs/manual-ocaml/libref/Set.S.html *)
let rec variables_of_term t =
raise (Failure “Problem 2 Not implemented”)
let variables_of_clause c =
raise (Failure “Problem 2 Not implemented”)
(* Problem 3 *)
module Substitution = Map.Make(struct type t = term let compare = Stdlib.compare end)
(* See API docs for OCaml Map: https://caml.inria.fr/pub/docs/manual-ocaml/libref/Map.S.html *)
let string_of_substitution s =
“{” ^ (
Substitution.fold (
fun v t s ->
match v with
| Variable v -> s ^ “; ” ^ v ^ ” -> ” ^ (string_of_term t)
| Constant _ -> assert false (* substitution maps a variable to a term *)
| Function _ -> assert false (* substitution maps a variable to a term *)
) s “”
) ^ “}”
let rec substitute_in_term s t =
raise (Failure “Problem 3 Not implemented”)
let substitute_in_clause s c =
raise (Failure “Problem 3 Not implemented”)
(* Problem 4 *)
let counter = ref 0
let fresh () =
let c = !counter in
counter := !counter + 1;
Variable (“_G” ^ string_of_int c)
let freshen c =
let vars = variables_of_clause c in
let s = VarSet.fold (fun v s -> Substitution.add v (fresh()) s) vars Substitution.empty in
substitute_in_clause s c
(*
let c = (rule (func “p” [var “X”; var “Y”; const “a”]) [func “q” [var “X”; const “b”; const “a”]])
let _ = print_endline (string_of_clause c)
let _ = print_endline (string_of_clause (freshen c))
*)
exception Not_unifiable
let unify t1 t2 =
raise (Failure “Problem 4 Not implemented”)
(* Problem 5 *)
let nondet_query program goal =
raise (Failure “Problem 5 Not implemented”)
(* Problem Bonus *)
let det_query program goal =
raise (Failure “Problem Bonus Not implemented”)
main.ml
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”
testUtils.ml
open OUnit2
let assert_true x = assert_equal true x;;
let assert_false x = assert_equal false x;;
dune_1
(tests
(names public)
(libraries cs314 oUnit qcheck))
public.ml
open OUnit2
open Cs314.Final
open TestUtils
let test_final_1_1 ctxt =
assert_equal true @@ (occurs_check (var “X”) (var “X”))
let test_final_1_2 ctxt =
assert_equal true @@ (not (occurs_check (var “X”) (var “Y”)))
let test_final_1_3 ctxt =
assert_equal true @@ (occurs_check (var “X”) (func “f” [var “X”]))
let test_final_1_4 ctxt =
assert_equal true @@ (occurs_check (var “E”) (func “cons” [const “a”; const “b”; var “E”]))
let test_final_2_1 ctxt =
assert_equal true @@ (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_equal true @@ (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_equal true @@ (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_equal true @@ (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_equal true @@ (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_equal true @@ (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_equal true @@ (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_equal true @@ (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_equal true @@ ((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_equal true @@ ((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_equal true @@ (unify (var “Y”) (var “Y”) = Substitution.empty)
let test_final_4_4 ctxt =
assert_equal true @@ (unify (const “0”) (const “0”) = Substitution.empty)
let test_final_4_5 ctxt =
assert_equal true @@ (unify (const “0”) (var “Y”) = Substitution.singleton (var “Y”) (const “0”))
let test_final_4_6 ctxt =
assert_equal true @@ (
match unify (const “0”) (const “1”) with
| _ -> false
| exception Not_unifiable -> true)
let test_final_4_7 ctxt =
assert_equal true @@ (
match unify (func “f” [const “0”]) (func “g” [const “1”]) with
| _ -> false
| exception Not_unifiable -> true)
let test_final_4_8 ctxt =
assert_equal true @@ (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_equal true @@ (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_equal true @@ (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_equal true @@ (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_equal true @@ (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_equal true @@ (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_equal true @@ (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_equal true @@ (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_equal true @@ (
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_equal true @@ (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_equal true @@ (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_equal true @@ (g1 = [ancestor (const “ned”) (const “robb”)]);
assert_equal true @@ (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_equal true @@ (List.length g’ = 4);
List.iter (fun g -> print_endline (“Solution:\n” ^ (string_of_goal g))) g’
let suite =
“public” >::: [
“test_final_1_1″>:: test_final_1_1;
“test_final_1_2″>:: test_final_1_2;
“test_final_1_3″>:: test_final_1_3;
“test_final_1_4″>:: test_final_1_4;
“test_final_2_1″>:: test_final_2_1;
“test_final_2_2″>:: test_final_2_2;
“test_final_2_3″>:: test_final_2_3;
“test_final_2_4″>:: test_final_2_4;
“test_final_3_1″>:: test_final_3_1;
“test_final_3_2″>:: test_final_3_2;
“test_final_3_3″>:: test_final_3_3;
“test_final_3_4″>:: test_final_3_4;
“test_final_4_1″>:: test_final_4_1;
“test_final_4_2″>:: test_final_4_2;
“test_final_4_3″>:: test_final_4_3;
“test_final_4_4″>:: test_final_4_4;
“test_final_4_5″>:: test_final_4_5;
“test_final_4_6″>:: test_final_4_6;
“test_final_4_7″>:: test_final_4_7;
“test_final_4_8″>:: test_final_4_8;
“test_final_4_9″>:: test_final_4_9;
“test_final_5_1″>:: test_final_5_1;
“test_final_5_2″>:: test_final_5_2;
“test_final_5_3″>:: test_final_5_3;
“test_final_5_4″>:: test_final_5_4;
“test_final_5_5″>:: test_final_5_5;
“test_final_5_6″>:: test_final_5_6;
“test_final_5_7″>:: test_final_5_7;
(*”test_final_bonus_1″>:: test_final_bonus_1;
“test_final_bonus_2″>:: test_final_bonus_2;
“test_final_bonus_3″>:: test_final_bonus_3;
“test_final_bonus_4″>:: test_final_bonus_4;*)
]
let _ = run_test_tt_main suite
mportant notes about grading: How to Start (OCaml): let _ = Random.self_init () ancestor(Z, Y), cons (H, T) abbreviated as [H|T] in SWI-Prolog, … The first component of Function is the name of the function, whose parameters are in a term list, the second component of Function.*) type body = term list (* The body of a rule is a list of Prolog Functions *) type clause = Fact of head | Rule of head * body (* A rule is in the shape head :- body *) type program = clause list (* A program consists of a list of clauses in which we have either rules or facts. *) type goal = term list (* A goal is a query that consists of a few functions *) (* This function converts a Prolog term (e.g. a constant, variable or function) to a string *) let rec string_of_term t = (* This function converts a list of Prolog terms, separated by commas, to a string *) let string_of_term_list fl = (* This function converts a Prolog goal (query) to a string *) let string_of_goal g = (* This function converts a Prolog clause (e.g. a rule or a fact) to a string *) let string_of_clause c = (* This function converts a Prolog program (a list of clauses), separated by \n, to a string *) let string_of_program p = let const c = Constant c (* helper function to construct a Prolog Constant *) let func f l = Function (f,l) (* helper function to construct a Prolog Function *) let fact f = Fact f (* helper function to construct a Prolog Fact *) let rule h b = Rule (h,b) (* helper function to construct a Prolog Rule *) Problem 1 https://caml.inria.fr/pub/docs/manual-ocaml/libref/Set.S.html *) let rec variables_of_term t = let variables_of_clause c = assert (VarSet.equal (variables_of_term (func “f” [var “X”; var “Y”; const “a”])) assert (VarSet.equal (variables_of_clause (fact (func “p” [var “X”; var “Y”; const “a”]))) assert (VarSet.equal (variables_of_clause (rule (func “p” [var “X”; var “Y”; const “a”]) https://caml.inria.fr/pub/docs/manual-ocaml/libref/Map.S.html *) (* This funtion converts a substitution to a string (for debugging) *) let string_of_substitution s = let rec substitute_in_term s t = let substitute_in_clause s c = let s = (* Function substitution – f (X, Y, a) [Y/0, X/Y] = f (Y, 0, a) *) assert (substitute_in_term s (func “f” [var “X”; var “Y”; const “a”]) = assert (substitute_in_clause s (fact (func “p” [var “X”; var “Y”; const “a”])) = we have p (Y, 0, a) :- q (a, b, a) *) assert (substitute_in_clause s (rule (func “p” [var “X”; var “Y”; const “a”]) [func “q” [const “a”; const “b”; const “a”]]) = https://caml.inria.fr/pub/docs/manual-ocaml/libref/Map.S.html ) let unify t1 t2 = assert ((unify (var “X”) (var “Y”)) = Substitution.singleton (var “Y”) (var “X”) || assert ((unify (var “Y”) (var “X”)) = Substitution.singleton (var “X”) (var “Y”) || assert (unify (var “Y”) (var “Y”) = Substitution.empty) assert (unify (const “0”) (const “0”) = Substitution.empty) assert (unify (const “0”) (var “Y”) = Substitution.singleton (var “Y”) (const “0”)) assert ( assert ( assert (unify (func “f” [var “X”]) (func “f” [var “Y”]) = Substitution.singleton (var “X”) (var “Y”) || let t1 = Function(“f”, [Variable “X”; Variable “Y”; Variable “Y”]) let freshen c = let _ = print_endline (string_of_clause c) X is replaced by _G0 and Y is replaced by _G1. *) let _ = print_endline (string_of_clause (freshen c)) father(rickard, ned). father(ned, robb). ancestor(X, Y) :- father(X, Y). ancestor(X, Y) :- father(X, Z), ancestor(Z, Y). *) let ancestor x y = func “ancestor” [x;y] let pstark = [f1;f2;r1;r2] (* Define a goal (query): ?- ancestor(rickard, robb) The solution is the query itself. *) let g = [ancestor (const “rickard”) (const “robb”)] (* Define a goal (query): ?- ancestor(X, robb) The solution can be either ancestor(ned, robb) or ancestor(rickard, robb) *) let g = [ancestor (var “X”) (const “robb”)] append(nil, Q, Q). append(cons(H, P), Q, cons(H, R)) :- append(P, Q, R). *) let nil = const “nil” (* Define a goal (query): ?- append(X, Y, cons(1, cons(2, cons(3, nil)))) The solution can be any of the following four: Solution 1: ?- append(nil, cons(1, cons(2, cons(3, nil))), cons(1, cons(2, cons(3, nil)))) Solution 2: ?- append(cons(1, nil), cons(2, cons(3, nil)), cons(1, cons(2, cons(3, nil)))) Solution 3: ?- append(cons(1, cons(2, nil)), cons(3, nil), cons(1, cons(2, cons(3, nil)))) Solution 4: ?- append(cons(1, cons(2, cons(3, nil))), nil, cons(1, cons(2, cons(3, nil)))) *) let g = [append (var “X”) (var “Y”) (cons (const “1”) (cons (const “2”) (cons (const “3”) nil)))] ?- ancestor(X, robb) The solution this time should include both ancestor(ned, robb) and ancestor(rickard, robb) *) let g = [ancestor (var “X”) (const “robb”)] ?- append(X, Y, cons(1, cons(2, cons(3, nil)))) The solution this time should include all of the following four: Solution 1: ?- append(nil, cons(1, cons(2, cons(3, nil))), cons(1, cons(2, cons(3, nil)))) Solution 2: ?- append(cons(1, nil), cons(2, cons(3, nil)), cons(1, cons(2, cons(3, nil)))) Solution 3: ?- append(cons(1, cons(2, nil)), cons(3, nil), cons(1, cons(2, cons(3, nil)))) Solution 4: ?- append(cons(1, cons(2, cons(3, nil))), nil, cons(1, cons(2, cons(3, nil)))) *) let g = [append (var “X”) (var “Y”) (cons (const “1”) (cons (const “2”) (cons (const “3”) nil)))] |