// Propositional Logic: parsing, evaluating, modeling with truth tables

open System;;
open Microsoft.FSharp.Math;;
open System.Text.RegularExpressions;;
open System.Collections.Generic;;

///////// Lexical Symbol Specification

// use regular expression to represent possible operator symbols:
let mutable operators = "([()\|&\^v!~]|\w|\s|\->|)";;  

// use hash table (Dictionary) to associate each operator with precedence
let prectable = Dictionary<string,int>();;
prectable.["->"] <- 200;
prectable.["v"] <- 300;
prectable.["|"] <- 300;
prectable.["^"] <- 400;
prectable.["&"] <- 400;
prectable.["~"] <- 500;
prectable.["!"] <- 500;
prectable.["("] <- 900;
prectable.[")"] <- 20;

// function to add new operator (as regex string) with precedence (int)
let newoperator (s:string) prec =
  let n = operators.Length
  let prefix = operators.Substring(0,n-1)
  operators <- prefix + "|" + s + ")"
  if s.[0]='\\' then prectable.[s.Substring(1,s.Length-1)] <- prec
  else prectable.[s] <- prec;;

//sample usage of newoperator function:
//newoperator @"&&" 650;;  // use @ before string or use "\^" (explict escape)
//Console.WriteLine(string(prectable.["&&"]));;  // check if success
//newoperator @"^" 600;;

///////// ABSTRACT SYNTAX

// expr folds in both expressions and tokens from the lexer

// proposition types:
type sentence = interface end;; // dummy interface

type proposition = | Atom of string | Binop of string*proposition*proposition | Unary of string*proposition  interface sentence;;

let rec tostring = function
  | Atom(p) -> p
  | Binop(op,a,b) -> "("+tostring(a)+" "+op+" "+tostring(b)+")"
  | Unary(op,p) -> op+tostring(p);;

let rec eval (env:Dictionary<string,bool>) = function
  | Binop("^",a,b) -> (eval env a) && (eval env b)
  | Binop("v",a,b) -> (eval env a) || (eval env b)
  | Binop("->",a,b) -> not(eval env a) || (eval env b)
  | Unary("~",p) -> not(eval env p)
  | Atom(p) -> env.[p] // look up binding in dictionary
  | x -> raise (Exception("malformed proposition "+string(x)));;

// generate binding for list of propositional variables from binary number n
// using right shift operator >>> to extract ith bit from int
let genenv (n:int) (Vs:string list) =
  let env = Dictionary<string,bool>()
  for i in 0..Vs.Length-1 do
    env.[Vs.[i]] <-  (n>>>i)%2 = 1  // binds variable to true/false
  env;;