#light

// Programming Paradigms Project

//module DistributedExperimentUnification

open System
open System.Threading
open System.Collections.Generic
open System.Windows.Forms          // Note that you'll need references for System.Windows.Forms and
open System.Drawing                // System.Drawing  (See the "solution explorer", on the right in VS...)  ----->>>




//////////////////////////////////////// Types for experiments, rules, etc.

type exp = A | B | Mix of exp * exp | Var of string




/// The value (e, ee) represents that "e suffices instead of ee" or "e suff ee" for short - see the rule type.
type sufficency = exp * exp

/// The value (e, ee), [(e1,ee1) ... (eN,eeN)] represents the rule that: "E suff EE provided that for all i in 1..N, Ei suff EEi".
/// Here the E, EE, Ei, EEi are the same as e, ee, eI, eeI except with each variable (Var Vj) replaced by an experiment EEEj that
/// contains no vars (the same EEEj each time Vj appears in the rule).  The rule holds for every such substitution for the vars.
type rule = Rule of sufficency * (sufficency list)

type ruleGen = unit -> rule      // A rule generator creates new variables for a rule each time it is called, to avoid clashes
                                 // with variable names in other rules, or when the rule is used multiple times.
type labRules = ruleGen list     // Each lab has a list of rules, represented as generators.


// Types for identifying labs and clients
type labID = int
type clientID = int

/// The number of Bases and Mixes in an experiment
let rec expSize = function A|B -> 1
                         | Mix (x, y) -> 1+expSize x + expSize y
                         | Var _ -> raise (Exception "expSize for a Var")       // This shouldn't happen





let contains comp arr = Array.exists (fun x -> (fst x = fst comp && comp <> x)) arr


let rec unify exp1 exp2 =
    match (exp1,exp2) with
            | (exp.Var x, exp.Var y) when x <> y -> [|exp2,exp1|]
            | (exp.Var a,b) | (b, exp.Var a) when Var(a) <> b -> [|Var(a),b|]
            | (exp.Mix(x,xx), exp.Mix(y,yy)) -> let lists = Array.append (unify x y) (unify xx yy) |> Array.toList
                                                let mutable filtered = [||]
                                                for i in 1 .. lists.Length do
                                                    let temp = lists.Item (i-1)
                                                    if (contains temp (lists |> List.toArray) <> true) then
                                                        filtered <- Array.append filtered [|temp|]
                                                filtered |> Map.ofArray |> Map.toArray
            | _ -> [||]






let a = Mix(A,B)
let b = Mix(Var("x"),Var("y"))
let c = Mix(Mix(A,B),B)
let d = Var("x")



// These are some handy functions for creating rule generators with different numbers of variables

let newVar =   let n = ref 0 in   fun v -> n:=!n+1;
                                           Var (v + string !n)

let newVar2 v1 v2 = newVar v1, newVar v2
let newVar3 (v1,v2,v3) = newVar v1, newVar v2, newVar v3
let newVar4 (v1,v2,v3,v4) = newVar v1, newVar v2, newVar v3, newVar v4



let rule1 () = let x = newVar "x"
               Rule ((x, x), [])

let rule3 () = let x, xx, y = newVar3 ("x", "xx", "y")
               Rule ((Mix(x,xx), y),  [(xx,y)])

let getsuff x =
    match x with
        | Rule(a,b) -> (fst a, snd a)

let getprereqs x =
    match x with
        | Rule(a,b) -> b

let rulesA = [rule1]


let getRuleset (rules : (unit->rule) list) =
    let rulesforyou = [for i in 1 .. rules.Length -> rules.Item(i-1)()]
    rulesforyou


let submarine = unify a b



let rec applySubs expr sublist : exp=
    let mutable newexpr = expr;
    for i in 0 .. (Array.length sublist) - 1 do
        let subfrom = fst (Array.get sublist i)
        let subto = snd (Array.get sublist i)
        match expr with
            | Var(a) when Var(a) = subfrom -> newexpr <- subto
            | Mix(a,b) -> newexpr <- Mix(applySubs a sublist,applySubs b sublist)
            | _ -> ()
    newexpr


let pickone = Array.get submarine 0

let h = applySubs d submarine


// Suffices checks whether exp1 suffices instead of exp2 according to rules.
let rec suffices rules (exp1, exp2) =
    let mutable istrue = false;
    let ruleset = getRuleset rules
    // for each rule
    for i in 1 .. ruleset.Length do
        let r = ruleset.Item(i-1)
        let uniL = unify exp1 (fst (getsuff r))
        let uniR = unify exp2 (snd (getsuff r))
        // check if rule is compatiable
        if (uniL <> [||] && uniR <> [||]) then
            let preq = getprereqs r
            let mutable isgood = true
            // check each prereq (sufficient list)
            for i in 0 .. preq.Length - 1 do
                let newexp1 = applySubs (fst (List.nth preq i)) uniL
                let newexp2 = applySubs (snd (List.nth preq i)) uniR
                if suffices rules (newexp1,newexp2) = true then
                    istrue <- true
    istrue



let testingsfasa = suffices rulesA (c,a)



(* so basically unify the input exp tuples with the string vars in the input rule
    if they match, check all suffices in sufficient list
    if they all true, return true, else false

pseudo code *)