Listing¶
Here we provide a listing of our code.
ast.ml¶
This file contains the types for representing our Abstract Syntax Tree.
(* Constants *)
type const =
| IntConst of int (* integers *)
| FloatConst of float (* floats *)
| StringConst of string (* strings *)
(* Expressions *)
type exp =
| VarExp of string (* variables *)
| ConstExp of const (* constants *)
| TermExp of string * exp list (* functor(arg1, arg2, ...) *)
(* Declarations *)
type dec =
| Clause of exp * (exp list) (* Head :- Body. *)
| Query of (exp list) (* ?- Body. *)
common.ml¶
This file contains common functions needed throughout the program.
open Ast
open Parser
(* Takes a string s and returns the abstract syntax tree generated by lexing and parsing s *)
let parse s =
let lexbuf = Lexing.from_string s in
let ast = clause Lexer.token lexbuf in
ast
(* Takes a string s and returns Some of an abstract syntax tree or None *)
let try_parse s =
try Some (parse s) with
| Error -> None
(* String conversion functions *)
let string_of_token t =
match t with
| INT i -> "INT " ^ string_of_int i
| FLOAT f -> "FLOAT " ^ string_of_float f
| STRING s -> "STRING \"" ^ String.escaped s ^ "\""
| ATOM a -> "ATOM \"" ^ String.escaped a ^ "\""
| VAR v -> "VAR \"" ^ v ^ "\""
| RULE -> "RULE"
| QUERY -> "QUERY"
| PERIOD -> "PERIOD"
| LPAREN -> "LPAREN"
| RPAREN -> "RPAREN"
| COMMA -> "COMMA"
| LBRACKET -> "LBRACKET"
| RBRACKET -> "RBRACKET"
| PIPE -> "PIPE"
| EOF -> "EOF"
let string_of_token_list tl =
"[" ^ (String.concat "; " (List.map string_of_token tl)) ^ "]"
let string_of_const c =
match c with
| IntConst i -> "IntConst " ^ string_of_int i
| FloatConst f -> "FloatConst " ^ string_of_float f
| StringConst s -> "StringConst \"" ^ String.escaped s ^ "\""
let rec string_of_exp e =
match e with
| VarExp v -> "VarExp \"" ^ v ^ "\""
| ConstExp c -> "ConstExp (" ^ (string_of_const c) ^ ")"
| TermExp (f, args) ->
let func = String.escaped f in
"TermExp (\"" ^ func ^ "\", [" ^
(String.concat "; " (List.map string_of_exp args)) ^ "])"
let string_of_exp_list g =
"[" ^ (String.concat "; " (List.map string_of_exp g)) ^ "]"
let string_of_dec d =
match d with
| Clause (e1, g) ->
"Clause (" ^ (string_of_exp e1) ^ ", " ^
(string_of_exp_list g) ^ ")"
| Query g -> "Query (" ^ (string_of_exp_list g) ^ ")"
let string_of_db db =
"[" ^ (String.concat "; " (List.map string_of_dec db)) ^ "]"
let string_of_subs s =
"[" ^ (
String.concat "; " (
List.map (
fun (x,y) ->
"(" ^ (string_of_exp x) ^ ", " ^ (string_of_exp y) ^ ")"
)
s
)
) ^ "]"
let string_of_unify_res s =
match s with
| None -> "None"
| Some l -> string_of_subs l
(* Convert ConstExp to a readable string *)
let readable_string_of_const c =
match c with
| IntConst i -> string_of_int i
| FloatConst f -> string_of_float f
| StringConst s -> "\"" ^ String.escaped s ^ "\""
(* Convert exp to a readable string *)
let rec readable_string_of_exp e =
match e with
| VarExp v -> v
| ConstExp c -> readable_string_of_const c
| TermExp (s, l) ->
s ^ (
if List.length l > 0
then "(" ^ (
String.concat ", " (
List.map readable_string_of_exp l
)
) ^ ")"
else ""
)
(* Print a db *)
let print_db db =
print_endline (string_of_db db)
evaluator.ml¶
This file contains the code needed to evaluate our expressions.
open Ast
open Common
(*
fresh:
* takes in:
unit
* returns a string of the increment of the counter
reset:
* takes in:
unit
* returns unit and the counter is reset
*)
let (fresh, reset) =
let nxt = ref 0 in
let f () = (nxt := !nxt + 1; string_of_int (!nxt)) in
let r () = nxt := 0 in
(f, r)
(*
find_vars:
* takes in:
q - a list of exp
* returns a list of all VarExp in the list
*)
let rec find_vars q =
match q with
| [] -> []
| (x :: xs) -> (
match x with
| VarExp v -> x :: (find_vars xs)
| ConstExp c -> (find_vars xs)
| TermExp (s, el) -> (find_vars el) @ (find_vars xs)
)
(*
find_vars_string:
* takes in:
q - a list of exp
* returns a list of all VarExp as strings
*)
let rec find_vars_string q =
match q with
| [] -> []
| (x :: xs) -> (
match x with
| VarExp v -> v :: (find_vars_string xs)
| ConstExp c -> (find_vars_string xs)
| TermExp (s, el) -> (find_vars_string el) @ (find_vars_string xs)
)
(*
uniq:
* takes in:
l - a list
* returns the list reversed with only one copy of each element
adapted from https://rosettacode.org/wiki/Remove_duplicate_elements#OCaml
*)
let uniq l =
let rec tail_uniq a l =
match l with
| [] -> a
| hd :: tl ->
tail_uniq (hd :: a) (List.filter (fun x -> (x <> hd) ) tl) in
tail_uniq [] l
(*
sub_lift_goal:
* takes in:
sub - a list of substitutions for variables
g - a goal of type exp
* returns the goal with the substitutions applied
*)
let rec sub_lift_goal sub g =
match g with
| VarExp v -> (
(* if this variable has a substitution do the substitution *)
try let i = List.assoc g sub in i
with Not_found -> VarExp v
)
| TermExp (s, el) ->
TermExp (s, List.map (fun g1 -> sub_lift_goal sub g1) el)
| _ -> g
(*
sub_lift_goal:
* takes in:
sub - a list of substitutions for variables
gl - a list of goals each of type exp
* returns the list of goals with the substitutions applied to each goal
*)
let sub_lift_goals sub gl =
List.map (fun g1 -> sub_lift_goal sub g1) gl
(*
rename_vars_in_dec:
* takes in:
d - a dec type
* returns a dec with all the variables in d renamed to fresh variable names
*)
let rec rename_vars_in_dec d =
match d with
| Clause (h, b) ->
let head_vars = find_vars [h] in
let body_vars = find_vars b in
(* find uniq vars from both head and body *)
let vars = uniq (head_vars @ body_vars) in
(* get fresh variable mappings *)
let sub = List.map (fun x -> (x, VarExp (fresh()))) vars in
(* substitute new names for variables *)
Clause (sub_lift_goal sub h, sub_lift_goals sub b)
| Query (b) ->
(* find uniq vars in query *)
let body_vars = find_vars b in
(* get fresh variable mappings *)
let vars = uniq (body_vars) in
let sub = List.map (fun x -> (x, VarExp (fresh()))) vars in
(* substitute new names for variables *)
Query (sub_lift_goals sub b)
(*
pairandcat:
* takes in:
sargs - a list of exps
targs - a list of exps
c - a list of constraints where each constraint is of type (exp * exp)
* returns a new list of constraints where c is prepended with each entry
from sargs is paired with a corresponding entry from targs
to make a new constraint
* used for implementing decompose for unification
* sargs and targs must be the same length, otherwise an exception is thrown
*)
let rec pairandcat sargs targs c =
match sargs with
| [] -> (
if (List.length targs = 0)
then c
else raise (Failure "sargs and targs should be the same length")
)
| (s :: ss) -> (
match targs with
| (t :: ts) -> pairandcat ss ts ((s, t) :: c)
| _ -> raise (Failure "sargs and targs should be the same length")
)
(*
replace:
* takes in:
c - a list of constraints where each constraint is of type (exp * exp)
sub - a list of substitutions
* returns a new list of constraints where the substitutions are applied to
both sides of each constraint
*)
let rec replace c sub =
match c with
| [] -> []
| ((s, t) :: xs) ->
(sub_lift_goal sub s, sub_lift_goal sub t) :: (replace xs sub)
(*
occurs:
* takes in:
n - a string
t - an exp
* returns true if n matches any variable names in t and false otherwise
*)
let rec occurs n t =
match t with
| VarExp m -> n = m
| TermExp (st, el) ->
List.fold_left (fun acc v -> acc || (occurs n v)) false el
| _ -> false
(*
unify:
* takes in:
constraints - a list of constraints where each constraint
is of type (exp * exp)
* returns None if the constraints can't be unified,
otherwise returns Some(i) where i is a list of substitutions
that unify the constraints
*)
let rec unify constraints =
match constraints with
| [] -> Some []
| ((s, t) :: c') ->
if s = t
then unify c' (* Delete *)
else (
match s with
| VarExp(n) ->
(* Eliminate *)
if (occurs n t)
then None
else let sub = [(s,t)] in
let c'' = replace c' sub in
let phi = unify c'' in (
match phi with
| None -> None
| Some l -> Some ((s, sub_lift_goal l t) :: l)
)
| TermExp (sname, sargs) -> (
match t with
(* Orient *)
| VarExp k -> unify ((t, s) :: c')
(* Decompose *)
| TermExp (tname, targs) ->
if (tname = sname && List.length targs = List.length sargs)
then unify (pairandcat sargs targs c')
else None
| _ -> None
)
| _ -> (
match t with
(* Orient *)
| VarExp k -> unify ((t, s) :: c')
| _ -> None
)
)
(*
eval_query:
* takes in (all in a triple):
q - a list of exp
db - a list of dec
env - a list of substitutions
where each substitution is of type (exp * exp)
* returns a list of lists of substitutions where each
substitution is of type (exp * exp)
- if the returned list is empty then no solutions were found for the
query for the given db
- otherwise, each element is a list of substitutions for one solution
to the query with the given db
*)
let rec eval_query (q, db, env) orig_vars =
match q with
| [] -> (
(* no more subgoals to prove so finished *)
[env]
)
| (g1 :: gl) -> ( (* have at least one more subgoal (g1) to prove *)
let vars_list_string = (find_vars_string q)@orig_vars |> uniq in
let env =
List.filter (fun (v, _) ->
match v with
| VarExp elt -> List.exists (fun a -> String.equal elt a) vars_list_string
| _ -> false
)
env
in
match g1 with
(* if goal is the true predicate *)
| TermExp("true", []) -> (
eval_query (
gl,
db,
env
)
orig_vars
)
(* if goal is some other predicate *)
| TermExp(_,_) -> (
(* iterate over the db *)
List.fold_right (
fun rule r -> (
match (rename_vars_in_dec rule) with (* rename vars in rule *)
| Clause (h, b) -> (
(* check if this rule can be used for this subgoal *)
match unify [(g1, h)] with
| Some s -> (
match unify (s@env) with
| Some env2 -> (
if (List.length b = 1)
then (
match b with
(* if the rule proved the subgoal (ie. rule was a
fact) then recurse on remaining subgoals *)
| ((TermExp ("true", _)) :: ys) ->
((eval_query (
sub_lift_goals s gl,
db,
env2
) orig_vars
) @ r)
(* if rule wasn't a fact then we have more
subgoals from the body of the rule
to prove *)
| _ -> ((eval_query (
(sub_lift_goals s b) @ (sub_lift_goals s gl),
db,
env2
) orig_vars
) @ r))
else
(* if rule wasn't a fact then we have more
subgoals from the body of the rule
to prove *)
((eval_query (
(sub_lift_goals s b) @ (sub_lift_goals s gl),
db,
env2
) orig_vars
) @ r)
)
(* the substitution from unify the rule head and subgoal
doesn't unify with the environment gathered so far *)
| _ -> r
)
(* this rule's head doesn't unify with the subgoal *)
| _ -> r
)
(* found a dec in the db that isn't a Clause *)
| _ -> r
)) db [] )
(* subgoal isn't a TermExp *)
| _ -> eval_query (gl, db, env) orig_vars
)
(*
string_of_res:
* takes in:
e - a list of lists of substitutions where each
substitution is of type (exp * exp)
orig_query_vars - a list of uniq VarExps that appeared
in the original query
orig_vars_num - number of uniq VarExps that appeared
in the original query
* returns a string consisting of all substitutions of variables
appearing in the original query of all solutions found and the
word true if solution(s) were found and false otherwise
*)
let string_of_res e orig_query_vars orig_vars_num =
(* iterate over e for each solution *)
List.fold_left (
fun r2 env ->
if orig_vars_num > 0
then
"====================\n" ^
(* iterate over original query vars to find their substitution *)
(List.fold_left (
fun r d -> (
match d with
| VarExp v -> (
(* find variable substitution in the solution *)
try let f = List.assoc (VarExp v) env in (
match f with
| VarExp v2 ->
(v ^ " is free\n") ^ r
| _ ->
(v ^ " = " ^ (
readable_string_of_exp f) ^ "\n") ^ r
)
with Not_found -> (v ^ " is free\n") ^ r)
| _ -> r
)
) "" (orig_query_vars) ) ^
"====================\n" ^ r2
else "" ^ r2
) (if List.length e > 0 (* if e is empty then there were no solutions *)
then "true\n"
else "false\n")
e
(*
add_dec_to_db:
* takes in (all in a tuple):
dec - a dec type
db - a list of dec types
* returns db prepended with dec if dec is not
of the pattern TermExp("true",_) as we don't want users to be able
to redefine the "true" atom
otherwise, db is returned
*)
let add_dec_to_db (dec, db) =
match dec with
| Clause (h, b) -> (
match h with
(* don't allow user to add a new definition of true *)
| TermExp ("true", _) ->
print_string "Can't reassign true predicate\n"; db
| _ -> dec :: db
)
| Query (b) -> (
dec :: db
)
(*
eval_dec:
* takes in (all in a tuple):
dec - a dec type
db - a list of dec types
* evaluated the dec with the given db
returns the original db in the case
dec is a Query type
otherwise returns db prepended with dec
*)
let eval_dec (dec, db) =
match dec with
| Clause (h, b) -> add_dec_to_db (dec, db)
| Query b -> (
(* find all uniq VarExps in query *)
let orig_vars = uniq (find_vars b) in
let orig_vars_string = find_vars_string b |> uniq in
(* find num of VarExps in query *)
let orig_vars_num = List.length orig_vars in
(* evaluate query *)
let res = eval_query (b, db, []) orig_vars_string in
(* print the result *)
print_string (string_of_res (res) orig_vars orig_vars_num);
(* reset fresh variable counter *)
reset ();
db
)
lexer.mll¶
This file defines the lexer.
{
open Parser
exception EndInput
}
(* Refer to:
https://www.cs.uni-potsdam.de/wv/lehre/Material/Prolog/Eclipse-Doc/userman/node139.html
http://www.amzi.com/manuals/amzi/pro/ref_terms.htm
for a list of valid tokens *)
(* Character classes *)
let upper_case = ['A' - 'Z']
let underline = '_'
let lower_case = ['a' - 'z']
let digit = ['0' - '9']
let blank_space = [' ' '\t']
let end_of_line = '\n'
let atom_quote = '''
let string_quote = '"'
let line_comment = '%' [^ '\n'] *
let open_comment = "/*"
let close_comment = "*/"
let escape = '\\'
(* Groups of characters *)
let alphanumerical = upper_case | underline | lower_case | digit
let any_character = [' ' - '~']
let non_escape = any_character # ['\\']
let sign = ['+' '-']
(* Atoms *)
let atom = lower_case alphanumerical *
let octal = ['0' - '7']
let octals = octal octal octal
let hex = ['0' - '9' 'A' - 'F' 'a' - 'f']
let hexes = 'x' hex + escape
(* Numbers *)
let digits = digit +
let integers = sign ? digits
let floats =
integers '.' digits (['e' 'E'] sign ? digits) ?
| integers ['e' 'E'] sign ? digits
let inf = '+' ? digits '.' digits "Inf"
let neg_inf = '-' digits '.' digits "Inf"
(* Variables *)
let variable = (upper_case | underline) alphanumerical *
rule token = parse
(* Meta-characters *)
| [' ' '\t' '\n'] { token lexbuf }
| eof { EOF }
(* Comments *)
| line_comment { token lexbuf }
| open_comment { comments 1 lexbuf }
| close_comment { raise (Failure "unmatched closed comment") }
(* Atoms *)
| atom as a { ATOM a }
| atom_quote { atoms "" lexbuf }
(* Numbers *)
| integers as n { INT (int_of_string n) }
| floats as f { FLOAT (float_of_string f) }
| inf { FLOAT infinity }
| neg_inf { FLOAT neg_infinity }
(* Strings *)
| string_quote { strings "" lexbuf }
(* Variables *)
| variable as v { VAR v }
(* Symbols *)
| ":-" { RULE }
| "?-" { QUERY }
| '.' { PERIOD }
| '(' { LPAREN }
| ')' { RPAREN }
| ',' { COMMA }
| '[' { LBRACKET }
| ']' { RBRACKET }
| '|' { PIPE }
and comments count = parse
| open_comment { comments (1 + count) lexbuf }
| close_comment { match count with
| 1 -> token lexbuf
| n -> comments (n - 1) lexbuf
}
| eof { raise (Failure "unmatched open comment") }
| _ { comments count lexbuf }
and strings acc = parse
(* Consecutive strings are concatenated into a single string *)
| string_quote blank_space * string_quote { strings acc lexbuf }
| string_quote { STRING acc }
| non_escape # ['"'] + as s { strings (acc ^ s) lexbuf }
| escape { escaped strings acc lexbuf }
and atoms acc = parse
| atom_quote { ATOM acc }
| non_escape # ['''] + as a { atoms (acc ^ a) lexbuf }
| escape { escaped atoms acc lexbuf }
and escaped callback acc = parse
| 'a' { callback (acc ^ (String.make 1 (char_of_int 7))) lexbuf }
| 'b' { callback (acc ^ (String.make 1 (char_of_int 8))) lexbuf }
| 'f' { callback (acc ^ (String.make 1 (char_of_int 12))) lexbuf }
| 'n' { callback (acc ^ (String.make 1 (char_of_int 10))) lexbuf }
| 'r' { callback (acc ^ (String.make 1 (char_of_int 13))) lexbuf }
| 't' { callback (acc ^ (String.make 1 (char_of_int 9))) lexbuf }
| 'v' { callback (acc ^ (String.make 1 (char_of_int 11))) lexbuf }
| 'e' { callback (acc ^ (String.make 1 (char_of_int 27))) lexbuf }
| 'd' { callback (acc ^ (String.make 1 (char_of_int 127))) lexbuf }
| escape { callback (acc ^ "\\") lexbuf }
| atom_quote { callback (acc ^ "'") lexbuf }
| string_quote { callback (acc ^ "\"") lexbuf }
| end_of_line { callback acc lexbuf }
| 'c' (blank_space | end_of_line) * { callback acc lexbuf }
| octals as o { callback (acc ^ (String.make 1 (char_of_int (
int_of_string ("0o" ^ o))))) lexbuf }
| hexes as h { callback (acc ^ (String.make 1 (char_of_int (
int_of_string ("0" ^ (String.sub h 0 (
(String.length h) - 1))))))) lexbuf }
{
(* Takes a string s and returns a list of tokens generated by lexing s *)
let get_all_tokens s =
let b = Lexing.from_string (s ^ "\n") in
let rec g () =
match token b with
| EOF -> []
| t -> t :: g () in
g ()
(* Takes a string s and returns Some of a list of tokens or None *)
let try_get_all_tokens s =
try Some (get_all_tokens s) with
| Failure _ -> None
}
main.ml¶
This file contains the main interpreter program.
open Ast
open Common
open Lexer
open Parser
open Evaluator
(* Try to detect if something is getting piped in *)
let is_interactive = 0 = (Sys.command "[ -t 0 ]")
let _ =
(if is_interactive
then print_endline "\nWelcome to the Prolog Interpreter\n"
else ()
);
let rec loop db = (
try (
let lexbuf = Lexing.from_channel stdin
in (
if is_interactive
then (print_string "> "; flush stdout)
else ()
);
let dec = clause (
fun lb -> (
match Lexer.token lb with
| EOF -> raise Lexer.EndInput
| r -> r
)
) lexbuf
(* evaluate dec and get a new db *)
in let newdb = eval_dec (dec,db)
in loop newdb (* loop again with new db *)
)
(* exception raised *)
with
| Failure s -> ( (* in case of an error *)
print_newline();
print_endline s;
print_newline();
loop db
)
| Parser.Error -> ( (* failed to parse input *)
print_string "\nDoes not parse\n";
loop db
)
| Lexer.EndInput -> exit 0 (* EOF *)
| _ -> ( (* Any other error *)
print_string "\nUnrecognized error\n";
loop db
)
)
in (loop [])
parser.mly¶
This file defines the parser.
%{
open Ast
(* The fact:
Head.
is equivalent to the rule:
Head :- true.
*)
let fact_sugar p =
Clause (
p,
[TermExp ("true", [])]
)
(* An atom can be regarded as a compound term with arity zero *)
let atom_sugar a =
TermExp (
a,
[]
)
%}
/* Refer to:
https://www.cs.uni-potsdam.de/wv/lehre/Material/Prolog/Eclipse-Doc/userman/node140.html
https://github.com/simonkrenger/ch.bfh.bti7064.w2013.PrologParser/blob/master/doc/prolog-bnf-grammar.txt
for a description of the grammar */
/* Tokens */
/* Constants */
%token <int> INT
%token <float> FLOAT
%token <string> STRING ATOM
/* Variables */
%token <string> VAR
/* Symbols */
%token RULE /* :- */
%token QUERY /* ?- */
%token PERIOD /* . */
%token LPAREN /* ( */
%token RPAREN /* ) */
%token COMMA /* , */
%token LBRACKET /* [ */
%token RBRACKET /* ] */
%token PIPE /* | */
/* Meta-characters */
%token EOF
/* Start symbols */
%start clause
/* Types */
%type <Ast.dec> clause
%type <Ast.exp> predicate term structure
%type <Ast.exp list> term_list predicate_list
%type <Ast.const> constant
%%
clause:
| p = predicate; PERIOD { fact_sugar p }
| p = predicate; RULE; pl = predicate_list; PERIOD { Clause (p, pl) }
| QUERY; pl = predicate_list; PERIOD { Query pl }
predicate_list:
| p = predicate { [p] }
| p = predicate; COMMA; pl = predicate_list { p :: pl }
predicate:
| a = ATOM { atom_sugar a }
| s = structure { s }
structure:
| a = ATOM; LPAREN; RPAREN { atom_sugar a }
| a = ATOM; LPAREN; tl = term_list; RPAREN { TermExp (a, tl) }
list:
| LBRACKET; RBRACKET { TermExp ("empty_list", [])}
| LBRACKET; l = list_body; RBRACKET { l }
list_body:
| t = term { TermExp("list", [t; TermExp("empty_list", [])]) }
| t = term; COMMA; l = list_body { TermExp("list", [t; l]) }
| t = term; PIPE; tl = term { TermExp("list", [t; tl]) }
term_list:
| t = term { [t] }
| t = term; COMMA; tl = term_list { t :: tl }
term:
| c = constant { ConstExp c }
| a = ATOM { atom_sugar a }
| v = VAR { VarExp v }
| s = structure { s }
| l = list { l }
constant:
| i = INT { IntConst i }
| f = FLOAT { FloatConst f }
| s = STRING { StringConst s }