syntax.ml

   1: (** Abstract syntax. *)
   2: 
   3: (** Constants and atoms are strings starting with lower-case letters. *)
   4: type constant = string
   5:     
   6: (** Variables are strings starting with upper-case letters, followed
   7:     by a number which indicates an instance of the variable. Thus a
   8:     variable instance is a pair [(x,n)] where [x] is a variable and [n] is
   9:     an integer. When the proof search depth is [n] all variables that we
  10:     need to use are renamed from [(x,0)] to [(x,n)]. This is necessary so
  11:     that we do not use the same variable name in two different
  12:     applications of the same assertion. *)
  13: type variable = string * int
  14: 
  15: (** The datatype of terms. *)
  16: type term =
  17:   | Var of variable             (** Variable [X1], [Y0], [Z2], ... *)
  18:   | Const of constant           (** Constant [a], [b], [c], ... *)
  19:   | App of constant * term list (** Compound term [f(t_1,...,t_n)] *)
  20: 
  21: (** Atomic proposition [p(t_1, ..., t_n)] *)
  22: type atom = constant * term list
  23: 
  24: (** A conjunction of atomic propositions [p_1, ..., p_n]. The empty
  25:     list represents [true]. *)
  26: type clause = atom list
  27: 
  28: (** An assertion [(a,b_1,...,b_n)] is a Horn formula [b_1 & ... & b_n => a]. *)
  29: type assertion = atom * clause
  30: 
  31: (** An environment is a list of pairs [(x, e)] where [x] is a variable
  32:     instance and [e] is a term. An environment represents the current
  33:     values of variables. *)
  34: type environment = (variable * term) list
  35: 
  36: (** A database is a list of assertions. It represents the current
  37:     program. *)
  38: type database = assertion list
  39: 
  40: (** Toplevel commands. *)    
  41: type toplevel_cmd =
  42:   | Assert of assertion  (** Assertion [a :- b_1, ..., b_n.] or [a.] *)
  43:   | Goal of clause       (** Query [?- a] *)
  44:   | Quit                 (** The [$quit] command. *)
  45:   | Use of string        (** The [$use "filename"] command. *)
  46:       
  47: (** [lookup env x] returns the value of variable instance [x] in
  48:     environment [env]. It returns [Var x] if the variable does not occur
  49:     in [env]. *)
  50: let rec lookup env x =
  51:   try List.assoc x env with Not_found -> Var x
  52: 
  53: 
  54: (** [subst_term sub t] substitutes in term [t] values for variables,
  55:     as specified by the associative list [s]. It substitutes
  56:     repeatedly until the terms stops changing, so this is not the
  57:     usual kind of substitution. It is what we need during
  58:     unification. *)
  59: let rec subst_term env = function
  60:   | Var x as e ->
  61:       (let e' = lookup env x in
  62:          if e = e' then e' else subst_term env e')
  63:   | Const _ as e -> e
  64:   | App (c, ls) -> App (c, List.map (subst_term env) ls)        
  65: 
  66: 
  67: (** [string_of_term t] converts term [t] to its string represenation. *)
  68: let rec string_of_term = function
  69:   | Var (v, 0) -> v
  70:   | Var (v, n) -> v ^ string_of_int n
  71:   | Const c -> c
  72:   | App (f, ls) -> f ^ "(" ^ (String.concat ", " (List.map string_of_term ls)) ^ ")"
  73: 
  74: (** [string_of_env env] converts environment [env] to its string
  75:     representation. It only keeps instance variables at level 0, i.e.,
  76:     those that appear in the toplevel goal. *)
  77: let string_of_env env =
  78:   match List.filter (fun ((_, n), _) -> n = 0) env with
  79:     | [] -> "Yes"
  80:     | env' -> String.concat "\n"
  81:         (List.map
  82:            (fun ((x,n), e) ->
  83:               x ^ " = " ^ string_of_term (subst_term env e))
  84:            (List.rev env'))
  85: 
  86: (** [occurs x t] returns [true] when variable instance [x] appears in
  87:     term [t]. *)
  88: let rec occurs x = function
  89:     Var y -> x = y
  90:   | Const _ -> false
  91:   | App (_, ts) -> List.exists (occurs x) ts

unify.ml

   1: (** Unification functions. *)
   2: 
   3: open Syntax
   4: 
   5: (** [NoUnify] is raised when terms cannot be unified. *)
   6: exception NoUnify
   7: 
   8: (** [unify_terms env t1 t2] unifies terms [t1] and [t2] in the current
   9:     environment [env]. On success it returns the environment extended with
  10:     the result of unification. On failure it raises [NoUnify]. *)
  11: let rec unify_terms env t1 t2 =
  12:   match subst_term env t1, subst_term env t2 with
  13:     | t1, t2 when t1 = t2 -> env
  14:     | (Var y, t) | (t, Var y) ->
  15:         if occurs y t then
  16:           raise NoUnify
  17:         else
  18:           (y,t) :: env
  19:     | Const _, _ -> raise NoUnify
  20:     | App (c1, ts1), App (c2, ts2) when c1 = c2 -> unify_lists env ts1 ts2
  21:     | App _, _ -> raise NoUnify
  22: 
  23: (** [unify_lists env lst1 lst2] unifies two lists of terms in current
  24:     environment [env] and returns a new environment [env'] on success. It
  25:     raises [NoUnify] on failure or if the lists are not of equal length.
  26: *)
  27: and unify_lists env lst1 lst2 =
  28:   try
  29:     List.fold_left2 (fun env t1 t2 -> unify_terms env t1 t2) env lst1 lst2
  30:   with Invalid_argument _ -> raise NoUnify
  31: 
  32: (** [unify_atoms env a1 a2] unifies atomic propositions [a1] and [a2]
  33:     in current environment [env] and returns a new environment [env'] on
  34:     success. It raises [NoUnify] on failure. *)
  35: let unify_atoms env (c1,ts1) (c2,ts2) =
  36:   if c1 = c2 then unify_lists env ts1 ts2 else raise NoUnify

solve.ml

   1: (** The prolog solver. *)
   2: 
   3: open Syntax
   4: 
   5: (** A value of type [choice] represents a choice point in the proof
   6:     search at which we may continue searching for another solution. It
   7:     is a tuple [(asrl, env, c, n)] where [asrl]
   8:     for other solutions of clause [c] in environment [env], using
   9:     assertion list [asrl], where [n] is the search depth. *)
  10: type choice = database * environment * clause * int
  11: 
  12: (** The global database of assertions. *)
  13: let base = ref ([] : database)
  14: 
  15: (** Add a new assertion at the end of the current database. *)
  16: let assertz a = 
  17:   let rec add = function [] -> [a] | b::bs -> b::(add bs) in
  18:     (base := add !base)
  19: 
  20: (** Exception [NoSolution] is raised when a goal cannot be proved. *)
  21: exception NoSolution
  22: 
  23: (** [renumber_term n t] renumbers all variable instances occurring in
  24:     term [t] so that they have level [n]. *)
  25: let rec renumber_term n = function
  26:   | Var (x,_) -> Var (x,n)
  27:   | Const _ as c -> c
  28:   | App (c, ts) -> App (c, List.map (renumber_term n) ts)
  29: 
  30: (** [renumber_atom n a] renumbers all variable instances occurring in
  31:     atom [a] so that they have level [n]. *)
  32: let rec renumber_atom n (c,ts) = (c, List.map (renumber_term n) ts)
  33: 
  34: (** [display_solution ch env] displays the solution of a goal encoded
  35:     by [env]. It then gives the user the option to search for other
  36:     solutions, as described by the list of choice points [ch], or to abort
  37:     the current proof search. *)
  38: let rec display_solution ch env =
  39:   match string_of_env env, ch with
  40:     | "Yes", _ -> print_endline "Yes"
  41:     | answer, [] -> print_endline answer
  42:     | answer, ch -> begin
  43:         print_string (answer ^ "\nmore? (y/n) [y] ") ;
  44:         flush stdout ;
  45:         match String.lowercase (read_line ()) with
  46:           | "y" | "yes" | "" -> continue_search ch
  47:           | _ -> raise NoSolution
  48:       end
  49: 
  50: (** [continue_search ch] looks for other answers. It accepts a list of
  51:     choices [ch]. It continues the search at the first choice in the
  52:     list. *)
  53: and continue_search = function
  54:   | [] -> raise NoSolution
  55:   | (asrl,env,gs,n)::cs -> solve cs asrl env gs n
  56: 
  57: (** [solve ch asrl env c n] looks for the proof of clause [c]. Other
  58:     arguments are:
  59:     
  60:     [ch] is a list of choices at which we may look for other solutions,
  61: 
  62:     [asrl] is the list of assertions that are used to reduce [c] to subgoals,
  63: 
  64:     [env] is the current environment (values of variables),
  65: 
  66:     [n] is the search depth, which is increased at each level of search.
  67: 
  68:     When a solution is found, it is printed on the screen. The user
  69:     then decides whether other solutions should be searched for.
  70: *)
  71: and solve ch asrl env c n =
  72:   (** [reduce_atom a asrl] reduces atom [a] to subgoals by using the
  73:       first assertion in the assetion list [asrl] whose conclusion matches
  74:       [a]. It returns [None] if the atom cannot be reduced, or the
  75:       remaining assertions, the new environment and the list of subgoals.
  76:   *)
  77:   let rec reduce_atom a = function
  78:     | [] -> None
  79:     | (b,lst)::asrl' ->
  80:         (try
  81:            let env' = Unify.unify_atoms env a (renumber_atom n b) in
  82:              Some (asrl', env', List.map (renumber_atom n) lst)
  83:          with Unify.NoUnify -> reduce_atom a asrl')
  84:   in
  85:     match c with
  86:       | [] ->
  87:           (* All atoms are solved, we found a solution. *)
  88:           display_solution ch env
  89:       | a::c' ->
  90:           (* Reduce the first atom in the clause. *)
  91:           (match reduce_atom a asrl with
  92:              | None -> 
  93:                  (* This clause cannot be solved, look for other solutions. *)
  94:                  continue_search ch
  95:              | Some (asrl', env', d) ->
  96:                  (* The atom was reduced to subgoals [d]. Continue
  97:                     search with the subgoals added to the list of
  98:                     goals. *)
  99:                  let ch' = (asrl', env, c, n)::ch (* Add a new choice. *)
 100:                  in
 101:                    solve ch' !base env' (d @ c') (n+1))
 102: 
 103: (** [solve_toplevel c] searches for the proof of clause [c] using the
 104:     global databased [!base]. This function is called from the main
 105:     program. *)
 106: let solve_toplevel c =
 107:   try
 108:     solve [] !base [] c 1
 109:   with NoSolution -> print_endline "No"

lexer.mll

   1: {
   2:   open Parser
   3:   open Lexing
   4: 
   5:   let incr_linenum lexbuf =
   6:     let pos = lexbuf.lex_curr_p in
   7:     lexbuf.lex_curr_p <- { pos with
   8:       pos_lnum = pos.pos_lnum + 1;
   9:       pos_bol = pos.pos_cnum;
  10:     }
  11: }
  12: 
  13: let const = ['a'-'z'] ['_' 'a'-'z' 'A'-'Z' '0'-'9']*
  14: let var = ['A'-'Z'] ['_' 'a'-'z' 'A'-'Z' '0'-'9']*
  15: 
  16: 
  17: rule token = parse
  18:     '#' [^'\n']* '\n' { incr_linenum lexbuf; token lexbuf }
  19:   | '\n'            { incr_linenum lexbuf; token lexbuf }
  20:   | [' ' '\t']      { token lexbuf }
  21:   | "$use"          { USE }
  22:   | "$quit"         { QUIT }
  23:   | "?-"            { GOAL }
  24:   | ":-"            { FROM }
  25:   | ";;"            { SEMICOLON2 }
  26:   | "true"          { TRUE }
  27:   | '\"' [^'\"']* '\"' { let str = lexeme lexbuf in
  28:                         STRING (String.sub str 1 (String.length str - 2)) }
  29:   | '('             { LPAREN }
  30:   | ')'             { RPAREN }
  31:   | ','             { COMMA }
  32:   | '.'             { PERIOD }
  33:   | const           { CONST (lexeme lexbuf) }
  34:   | var             { VAR (lexeme lexbuf) }
  35:   | eof             { EOF }
  36: 
  37: {
  38: }

parser.mly

   1: %{
   2:   open Syntax
   3: %}
   4: 
   5: %token <string>VAR
   6: %token <string>CONST
   7: %token FROM
   8: %token COMMA
   9: %token TRUE
  10: %token PERIOD
  11: %token LPAREN RPAREN
  12: %token GOAL
  13: %token QUIT
  14: %token SEMICOLON2
  15: %token USE
  16: %token <string>STRING
  17: %token EOF
  18: 
  19: %start toplevel
  20: %type <Syntax.toplevel_cmd list> toplevel
  21: 
  22: %right SEMICOLON2
  23: %nonassoc PERIOD GOAL IMPLIED
  24: %right COMMA
  25: 
  26: %%
  27: 
  28: toplevel:
  29:   | EOF                      { [] }
  30:   | exprtop                  { $1 }
  31:   | cmdtop                   { $1 }
  32: 
  33: exprtop:
  34:   | expr EOF                 { [$1] }
  35:   | expr toplevel            { $1 :: $2 }
  36: 
  37: cmdtop:
  38:   | cmd EOF                  { [$1] }
  39:   | cmd toplevel             { $1 :: $2 }
  40: 
  41: cmd:
  42:   | USE STRING { Use $2 }
  43:   | QUIT       { Quit }
  44: 
  45: expr:
  46:   | goal      { $1 }
  47:   | assertion { $1 }
  48: 
  49: goal:
  50:   | GOAL clause PERIOD        { Goal $2 }
  51: 
  52: assertion:
  53:   | atom PERIOD               { Assert ($1, []) }
  54:   | atom FROM clause PERIOD   { Assert ($1, $3) }
  55: 
  56: atom:
  57:   | CONST                     { ($1, []) }
  58:   | CONST LPAREN args RPAREN  { ($1, $3) }
  59: 
  60: clause:
  61:   | TRUE                      { [] }
  62:   | atom                      { [$1] }
  63:   | atom COMMA clause         { $1 :: $3 }
  64: 
  65: args:
  66:   | literal            { [$1] }
  67:   | literal COMMA args { $1 :: $3 }
  68: 
  69: literal:
  70:   | CONST                    { Const $1 }
  71:   | VAR                      { Var ($1, 0) }
  72:   | CONST LPAREN args RPAREN { App ($1, $3) }
  73: 
  74: 
  75: %%

message.ml

   1: (** Error messages. *)
   2: 
   3: open Lexing
   4: 
   5: (** [lexer_from_channel fn ch] returns a lexer stream which takes
   6:     input from channel [ch]. The filename (for reporting errors) is
   7:     set to [fn].
   8: *)
   9: let lexer_from_channel fn ch =
  10:   let lex = Lexing.from_channel ch in
  11:   let pos = lex.lex_curr_p in
  12:     lex.lex_curr_p <- { pos with pos_fname = fn; pos_lnum = 1; } ;
  13:     lex
  14: 
  15: (** [lexer_from_string str] returns a lexer stream which takes input
  16:     from a string [str]. The filename (for reporting errors) is set to
  17:     [""]. *)
  18: let lexer_from_string str =
  19:   let lex = Lexing.from_string str in
  20:   let pos = lex.lex_curr_p in
  21:     lex.lex_curr_p <- { pos with pos_fname = ""; pos_lnum = 1; } ;
  22:     lex
  23: 
  24: let string_of_position {pos_fname=fn; pos_lnum=ln; pos_bol=bol; pos_cnum=cn} =
  25:   let c = cn - bol in
  26:     if fn = "" then
  27:       "Character " ^ string_of_int c
  28:     else
  29:       "File \"" ^ fn ^ "\", line " ^ string_of_int ln ^ ", character " ^ string_of_int c
  30: 
  31: let string_of msg pos = string_of_position pos ^ ":\n" ^ msg
  32: 
  33: let syntax_error {lex_curr_p=pos} = string_of "Syntax error" pos
  34: 
  35: let report = print_endline

miniprolog.ml

   1: (** Miniprolog toplevel. *)
   2: 
   3: open Message
   4: open Syntax
   5: 
   6: (**
   7:   The toplevel accepts global value definitions [let x = e] and expressions,
   8:   separated by double semicolons [;;] when contained in a file.
   9: 
  10:   Usage:
  11: 
  12:     [miniprolog] runs the interactive loop
  13: 
  14:     [miniprolog dat1 ... datN] evaluates the contents of files
  15:     [dat1], ..., [datN] then runs the interactive loop.
  16: 
  17:     [miniprolog -n dat1 ..., datN] evaluates the contents of files
  18:     [dat1],...,[datN] and exits.
  19: *)
  20: 
  21: exception Fatal_error of string
  22: 
  23: let fatal_error msg = raise (Fatal_error msg)
  24: 
  25: (** [exec_cmd cmd] executes the toplevel command [cmd]. *)
  26: let rec exec_cmd = function
  27:   | Goal g -> Solve.solve_toplevel g
  28:   | Assert a ->  Solve.assertz a
  29:   | Quit -> raise End_of_file
  30:   | Use fn -> exec_file fn
  31: 
  32: (** [exec_file fn] executes the contents of file [fn]. *)
  33: and exec_file fn =
  34:   let fh = open_in fn in
  35:   let lex = Message.lexer_from_channel fn fh in
  36:     try
  37:       let cmds = Parser.toplevel Lexer.token lex in
  38:         close_in fh ;
  39:         exec_cmds cmds
  40:     with
  41:       | Sys.Break -> fatal_error "Interrupted."
  42:       | Parsing.Parse_error | Failure("lexing: empty token") ->
  43:           fatal_error (Message.syntax_error lex)
  44: 
  45: (** [exec_cmds cmds] executes the list of toplevel commands [cmds]. *)
  46: and exec_cmds cmds = List.iter exec_cmd cmds
  47: ;;
  48: 
  49: (** [shell ()] is the interactive shell. *)
  50: let shell () =
  51:   print_string ("Miniprolog. Press ") ;
  52:   print_string (match Sys.os_type with
  53:                     "Unix" | "Cygwin" -> "Ctrl-D"
  54:                   | "Win32" -> "Ctrl-Z"
  55:                   | _ -> "EOF") ;
  56:   print_endline " to exit." ;
  57:   print_endline "Input syntax: " ;
  58:   print_endline "   ?- query.           Make a query." ;
  59:   print_endline "   a(t1, ..., tn).     Assert an atomic proposition." ;
  60:   print_endline "   A :- B1, ..., Bn.   Assert an inference rule." ;
  61:   print_endline "   $quit               Exit interpreter." ;
  62:   print_endline "   $use \"filename\"     Execute commands from a file." ;
  63:   try
  64:     while true do
  65:       try
  66:         print_string "Prolog> ";
  67:         let str = read_line () in
  68:         let lex = Message.lexer_from_string str in
  69:         let cmds =
  70:           try
  71:             Parser.toplevel Lexer.token lex
  72:           with
  73:             | Failure("lexing: empty token")
  74:             | Parsing.Parse_error -> fatal_error (Message.syntax_error lex)
  75:         in
  76:           exec_cmds cmds
  77:       with
  78:         | Fatal_error msg -> Message.report msg
  79:         | Sys.Break -> Message.report ("Interrupted.")
  80:     done 
  81:   with End_of_file -> print_endline "\nGood bye."
  82: 
  83: (** The main program. *)
  84: let main =
  85:   Sys.catch_break true ;
  86:   let noninteractive = ref false in
  87:   let files = ref [] in
  88:     Arg.parse
  89:       [("-n", Arg.Set noninteractive, "do not run the interactive shell")]
  90:       (fun f -> files := f :: !files)
  91:       "Usage: miniprolog [-n] [file] ..." ;
  92:     files := List.rev !files ;
  93:     try
  94:       List.iter exec_file !files ;
  95:       if not !noninteractive then shell ()
  96:     with Fatal_error msg -> Message.report msg