Adding RulesDSD
This commit is contained in:
Neil Dalchau
Родитель
4545f9489f
Коммит
d539d1bbc0
|
|
@ -0,0 +1,43 @@
|
|||
|
||||
Microsoft Visual Studio Solution File, Format Version 12.00
|
||||
# Visual Studio Version 16
|
||||
VisualStudioVersion = 16.0.30907.101
|
||||
MinimumVisualStudioVersion = 10.0.40219.1
|
||||
Project("{6EC3EE1D-3C4E-46DD-8F32-0CC8E7565705}") = "RulesDSD", "RulesDSD\RulesDSD.fsproj", "{BA8017D3-FECC-4675-8529-BF66858E01DC}"
|
||||
EndProject
|
||||
Project("{6EC3EE1D-3C4E-46DD-8F32-0CC8E7565705}") = "SiteGraphReactor", "..\SiteGraphReactor\SiteGraphReactor\SiteGraphReactor.fsproj", "{DD8A92D8-9520-4BF2-B399-08ED9B6E1F95}"
|
||||
EndProject
|
||||
Project("{6EC3EE1D-3C4E-46DD-8F32-0CC8E7565705}") = "ParserCombinators", "..\ParserCombinators\ParserCombinators\ParserCombinators.fsproj", "{DD8FEC26-6D1D-4642-A706-04070B6D5494}"
|
||||
EndProject
|
||||
Project("{6EC3EE1D-3C4E-46DD-8F32-0CC8E7565705}") = "Filzbach.FSharp.Portable", "..\Filzbach.FSharp\Filzbach.FSharp.Portable.fsproj", "{7DE55D27-0DFE-4975-ABD9-AD36B56150C4}"
|
||||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|x64 = Debug|x64
|
||||
Release|x64 = Release|x64
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{BA8017D3-FECC-4675-8529-BF66858E01DC}.Debug|x64.ActiveCfg = Debug|x64
|
||||
{BA8017D3-FECC-4675-8529-BF66858E01DC}.Debug|x64.Build.0 = Debug|x64
|
||||
{BA8017D3-FECC-4675-8529-BF66858E01DC}.Release|x64.ActiveCfg = Release|Any CPU
|
||||
{BA8017D3-FECC-4675-8529-BF66858E01DC}.Release|x64.Build.0 = Release|Any CPU
|
||||
{DD8A92D8-9520-4BF2-B399-08ED9B6E1F95}.Debug|x64.ActiveCfg = Debug|Any CPU
|
||||
{DD8A92D8-9520-4BF2-B399-08ED9B6E1F95}.Debug|x64.Build.0 = Debug|Any CPU
|
||||
{DD8A92D8-9520-4BF2-B399-08ED9B6E1F95}.Release|x64.ActiveCfg = Release|Any CPU
|
||||
{DD8A92D8-9520-4BF2-B399-08ED9B6E1F95}.Release|x64.Build.0 = Release|Any CPU
|
||||
{DD8FEC26-6D1D-4642-A706-04070B6D5494}.Debug|x64.ActiveCfg = Debug|Any CPU
|
||||
{DD8FEC26-6D1D-4642-A706-04070B6D5494}.Debug|x64.Build.0 = Debug|Any CPU
|
||||
{DD8FEC26-6D1D-4642-A706-04070B6D5494}.Release|x64.ActiveCfg = Release|Any CPU
|
||||
{DD8FEC26-6D1D-4642-A706-04070B6D5494}.Release|x64.Build.0 = Release|Any CPU
|
||||
{7DE55D27-0DFE-4975-ABD9-AD36B56150C4}.Debug|x64.ActiveCfg = Debug|x64
|
||||
{7DE55D27-0DFE-4975-ABD9-AD36B56150C4}.Debug|x64.Build.0 = Debug|x64
|
||||
{7DE55D27-0DFE-4975-ABD9-AD36B56150C4}.Release|x64.ActiveCfg = Release|x64
|
||||
{7DE55D27-0DFE-4975-ABD9-AD36B56150C4}.Release|x64.Build.0 = Release|x64
|
||||
EndGlobalSection
|
||||
GlobalSection(SolutionProperties) = preSolution
|
||||
HideSolutionNode = FALSE
|
||||
EndGlobalSection
|
||||
GlobalSection(ExtensibilityGlobals) = postSolution
|
||||
SolutionGuid = {5B9EB4F4-CDA0-4D54-A047-0F1C49805094}
|
||||
EndGlobalSection
|
||||
EndGlobal
|
||||
|
|
@ -0,0 +1,13 @@
|
|||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<configuration>
|
||||
<startup>
|
||||
<supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.7.2" />
|
||||
</startup>
|
||||
|
||||
<runtime><assemblyBinding xmlns="urn:schemas-microsoft-com:asm.v1">
|
||||
<dependentAssembly>
|
||||
<Paket>True</Paket>
|
||||
<assemblyIdentity name="FSharp.Core" publicKeyToken="b03f5f7f11d50a3a" culture="neutral" />
|
||||
<bindingRedirect oldVersion="0.0.0.0-65535.65535.65535.65535" newVersion="4.7.0.0" />
|
||||
</dependentAssembly>
|
||||
</assemblyBinding></runtime></configuration>
|
||||
|
|
@ -0,0 +1,41 @@
|
|||
namespace RulesDSD.AssemblyInfo
|
||||
|
||||
open System.Reflection
|
||||
open System.Runtime.CompilerServices
|
||||
open System.Runtime.InteropServices
|
||||
|
||||
// General Information about an assembly is controlled through the following
|
||||
// set of attributes. Change these attribute values to modify the information
|
||||
// associated with an assembly.
|
||||
[<assembly: AssemblyTitle("RulesDSD")>]
|
||||
[<assembly: AssemblyDescription("")>]
|
||||
[<assembly: AssemblyConfiguration("")>]
|
||||
[<assembly: AssemblyCompany("")>]
|
||||
[<assembly: AssemblyProduct("RulesDSD")>]
|
||||
[<assembly: AssemblyCopyright("Copyright © 2017")>]
|
||||
[<assembly: AssemblyTrademark("")>]
|
||||
[<assembly: AssemblyCulture("")>]
|
||||
|
||||
// Setting ComVisible to false makes the types in this assembly not visible
|
||||
// to COM components. If you need to access a type in this assembly from
|
||||
// COM, set the ComVisible attribute to true on that type.
|
||||
[<assembly: ComVisible(false)>]
|
||||
|
||||
// The following GUID is for the ID of the typelib if this project is exposed to COM
|
||||
[<assembly: Guid("ba8017d3-fecc-4675-8529-bf66858e01dc")>]
|
||||
|
||||
// Version information for an assembly consists of the following four values:
|
||||
//
|
||||
// Major Version
|
||||
// Minor Version
|
||||
// Build Number
|
||||
// Revision
|
||||
//
|
||||
// You can specify all the values or you can default the Build and Revision Numbers
|
||||
// by using the '*' as shown below:
|
||||
// [<assembly: AssemblyVersion("1.0.*")>]
|
||||
[<assembly: AssemblyVersion("1.0.0.0")>]
|
||||
[<assembly: AssemblyFileVersion("1.0.0.0")>]
|
||||
|
||||
do
|
||||
()
|
||||
|
|
@ -0,0 +1,34 @@
|
|||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<Project Sdk="Microsoft.NET.Sdk">
|
||||
<PropertyGroup>
|
||||
<TargetFramework>netstandard2.0</TargetFramework>
|
||||
<AutoGenerateBindingRedirects>true</AutoGenerateBindingRedirects>
|
||||
<Platforms>x64</Platforms>
|
||||
<PlatformTarget>x64</PlatformTarget>
|
||||
</PropertyGroup>
|
||||
<ItemGroup>
|
||||
<Compile Include="AssemblyInfo.fs" />
|
||||
<Compile Include="syntax.fs" />
|
||||
<Compile Include="concreteProcess.fs" />
|
||||
<Compile Include="substitution.fs" />
|
||||
<Compile Include="unification.fs" />
|
||||
<Compile Include="processEquality.fs" />
|
||||
<Compile Include="resolution.fs" />
|
||||
<Compile Include="parser.fs" />
|
||||
<None Include="App.config" />
|
||||
<None Include="paket.references" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<PackageReference Include="QuickGraph" Version="3.6.61119.7" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<ProjectReference Include="..\..\CRNEngine\CRNEngineDotNet\CRNEngineDotNet.fsproj" />
|
||||
<ProjectReference Include="..\..\ParserCombinators\ParserCombinators\ParserCombinators.fsproj" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<Reference Include="Oslo.FSharp">
|
||||
<HintPath>..\..\Lib\Oslo.FSharp\Oslo.FSharp.dll</HintPath>
|
||||
</Reference>
|
||||
</ItemGroup>
|
||||
<Import Project="..\..\.paket\Paket.Restore.targets" />
|
||||
</Project>
|
||||
|
|
@ -0,0 +1,11 @@
|
|||
[<JavaScript>]
|
||||
module RulesDSD.ConcreteProcess
|
||||
|
||||
open RulesDSD.Syntax
|
||||
|
||||
(*
|
||||
The main purpose of this module is to provide an intermediate data structure 'ProcessC' that strips a Syntax.Process
|
||||
of Term-related components, thus providing a simpler data structure to render in the tool.
|
||||
*)
|
||||
|
||||
// the suffix 'C' is for 'concrete', and it helps to separate this module's namespace from Syntax's namespace
|
||||
|
|
@ -0,0 +1,9 @@
|
|||
group NETSTANDARD
|
||||
|
||||
#FsCheck
|
||||
#FsUnit.xUnit
|
||||
#xunit.core
|
||||
#xunit.runner.console
|
||||
#xunit.runner.visualstudio
|
||||
FSharp.Collections.ParallelSeq
|
||||
FSharp.Core
|
||||
|
|
@ -0,0 +1,363 @@
|
|||
[<JavaScript>]
|
||||
module RulesDSD.Parser
|
||||
|
||||
open Parser
|
||||
open RulesDSD.Syntax
|
||||
open RulesDSD.Substitution
|
||||
|
||||
(* Terms syntax:
|
||||
TERM ::=
|
||||
(* standard logic programming terms *)
|
||||
// standard Prolog structures
|
||||
<VARIABLE>
|
||||
| <CONSTANT>
|
||||
| <INT>
|
||||
| <OPERATION>
|
||||
// lists
|
||||
| '[' <TERM>* ']' // finite list of terms
|
||||
| '[' <TERM>+ '|' <VAR> ']' // partial list of terms
|
||||
// | TCONS // appends a term to a TList
|
||||
| <PATTERN>
|
||||
| <CONTEXT>
|
||||
(* Pattern related terms *)
|
||||
| PATTERN
|
||||
| SYSTEM
|
||||
| HOLE
|
||||
| CONTEXT
|
||||
|
||||
// operations, such as "+(1, 2)"
|
||||
OPERATION ::= <OP_NAME> '(' (<TERM> ',')* <TERM>')'
|
||||
OP_NAME ::= '+' | '-' | '*' | '/' | NAME
|
||||
*)
|
||||
let pname = (name .>> spaces) <|> kw "_"
|
||||
let pnick = kw ">" >>. kw "|" >>. kw "<"
|
||||
|
||||
let pnil st = (kw "nil" >>. preturn (Pattern<'s>.Nihil)) st
|
||||
|
||||
// grammar disambiguation types
|
||||
type NextParser = PFunction | PPattern | PArithmetic | PVariable | PContext
|
||||
|
||||
|
||||
let rec plocation idProvider =
|
||||
let f x = if x = "_" then (-1, "_") else idProvider x
|
||||
choice [ kw "@" >>. pname |>> (f >> Location.Var)
|
||||
preturn (Location.Var (-1, "_")) ]
|
||||
|
||||
and ppattern (sp : Parser.t<'s>) idProvider =
|
||||
let ppatternSite : t<'s * Location> = sp .>>. plocation idProvider
|
||||
choice [
|
||||
// naught pattern
|
||||
pnil
|
||||
// <... or <...> patterns
|
||||
kw "<" >>. many1 ppatternSite >>= fun sites ->
|
||||
choice [
|
||||
kw ">" >>. preturn (Pattern.Strand sites)
|
||||
preturn (Pattern.FivePrime sites)
|
||||
]
|
||||
|
||||
// ... or ...> or ...> | <... patterns
|
||||
many1 (sp .>>. plocation idProvider) >>= fun sites ->
|
||||
choice [
|
||||
kw ">" >>. choice [
|
||||
// ...> | <...
|
||||
kw "|" >>. kw "<" >>. many (sp .>>. plocation idProvider) |>> fun moreSites -> Pattern.Nicking (sites, moreSites)
|
||||
// ...>
|
||||
preturn (Pattern.ThreePrime sites)
|
||||
]
|
||||
preturn (Pattern.Inner sites)
|
||||
]
|
||||
]
|
||||
|
||||
and psystem sp =
|
||||
(Parser.sepBy1 (between (kw "<") (kw ">") (many1 sp)) (kw "|")
|
||||
|>> Process.OfList)
|
||||
|
||||
and doPTerm (sp:Parser.t<'s>) cle (isExp:bool) (isComplex:bool) (idProvider : string -> (int*string)) (domainKeywords: string list (* the list of keywords that distinguish a variable from a domain specific element (e.g. in DSD "!" turns A in A!i from a generic variable to a DSD variable) *))
|
||||
st : Parser.Result<Term<'s>> =
|
||||
let pexp = choice [ kw "+" >>. preturn PArithmetic
|
||||
kw "-" >>. preturn PArithmetic
|
||||
kw "*" >>. preturn PArithmetic
|
||||
kw "/" >>. preturn PArithmetic
|
||||
kw "**" >>. preturn PArithmetic
|
||||
kw "%" >>. preturn PArithmetic ]
|
||||
|
||||
let termParser st : Parser.Result<Term<'s>> = doPTerm sp cle isExp isComplex idProvider domainKeywords st
|
||||
// let termParserNoExp st : Parser.Result<Term<'s>> = doPTerm sp cle false idProvider domainKeywords st
|
||||
let termParserNoExp st : Parser.Result<Term<'s>> = doPTerm sp cle true isComplex idProvider domainKeywords st
|
||||
let ptermExpression st = (Microsoft.Research.CRNEngine.Expression.parse termParserNoExp |>> Term<'s>.FromExpression) st
|
||||
|
||||
(choice [
|
||||
|
||||
// Naught pattern (like the empty reactant/product set 0 in CRNs)
|
||||
pnil |>> Term.Pat
|
||||
|
||||
// term in parentheses
|
||||
paren (termParser)
|
||||
|
||||
// NUMBERS
|
||||
plookAheadWith (
|
||||
pfloat >>. spaces >>. choice [ pexp
|
||||
preturn PPattern] )
|
||||
>>= fun disambiguation ->
|
||||
match disambiguation with
|
||||
| PArithmetic -> ptermExpression
|
||||
| PPattern -> pfloat .>> spaces |>> Term.Float
|
||||
| _ -> failwith ""
|
||||
|
||||
plookAheadWith (
|
||||
pint32 >>. spaces >>. choice [ pexp
|
||||
preturn PPattern] )
|
||||
>>= fun disambiguation ->
|
||||
match disambiguation with
|
||||
| PArithmetic -> ptermExpression
|
||||
| PPattern -> pint32 .>> spaces |>> (float >> Term.Float)
|
||||
| _ -> failwith ""
|
||||
|
||||
// CONSTANT
|
||||
kw "\"" >>. (manySatisfy ((<>) '"') .>> kw "\"")
|
||||
|>> System.String.Concat
|
||||
|>> Term.Const
|
||||
|
||||
// TLIST
|
||||
sqBrackets
|
||||
<| choice [
|
||||
sepBy termParser (kw ";") >>=
|
||||
(fun listElements ->
|
||||
choice [
|
||||
kw "#" >>. pname |>> fun restOfList ->
|
||||
let f x = if x = "_" then (-1, "_") else idProvider x
|
||||
List.foldBack (fun x y -> TCons(x, y)) listElements (Term.Var (f restOfList))
|
||||
preturn (TList listElements)
|
||||
]
|
||||
)
|
||||
]
|
||||
|
||||
// PROCESS
|
||||
psystem sp |>> Term.Proc // >> (Term.Canonical CLE.empty))
|
||||
|
||||
// CRNs
|
||||
Parser.braces
|
||||
(Parser.opt (Parser.kw "|")
|
||||
>>. Parser.sepBy1 (
|
||||
// reaction parser with mass action or functional rate, mostly taken from CRNEngine
|
||||
let pmset st = let counted =
|
||||
(Parser.pint32 +>>+ termParserNoExp |>> fun (n,s) -> n, s)
|
||||
<|> (termParserNoExp |>> (fun s -> 1, s))
|
||||
Parser.sepBy counted (Parser.kw "+") |>> Term.TMSet
|
||||
<| st
|
||||
|
||||
|
||||
// parse reactants
|
||||
pmset .>>.
|
||||
Parser.choice [
|
||||
Parser.kw "~" >>. pmset |>> Some
|
||||
Parser.preturn None
|
||||
]
|
||||
>>= fun (mset1, mset2) ->
|
||||
//parse arrows and rate
|
||||
let ptermExpression st = (Microsoft.Research.CRNEngine.Expression.parse termParser |>> Term<'s>.FromExpression) st
|
||||
let ptermSqExpression st = (Microsoft.Research.CRNEngine.Expression.parse (Microsoft.Research.CRNEngine.Key.parse termParser)
|
||||
|>> fun x -> Term<'s>.FromFuncExpression x) st
|
||||
let defaultRate = Term.Float 1.0
|
||||
let parseRate st =
|
||||
choice [
|
||||
Parser.bracket "{" "}" ptermExpression |>> fun x -> Term.Func(Keywords.massActionRate, [x])
|
||||
Parser.bracket "[" "]" ptermSqExpression |>> fun x -> Term.Func (Keywords.functionalRate, [x])
|
||||
] st
|
||||
Parser.choice [
|
||||
Parser.kw "->" >>. (parseRate |>> fun r -> (r,None)
|
||||
<|> Parser.preturn (Term.Func (Keywords.massActionRate, [defaultRate]), None))
|
||||
Parser.kw "<->" >>. (Parser.pTry (parseRate +>>+ parseRate)
|
||||
<|> (Parser.braces (ptermExpression +>> Parser.kw "," +>>+ ptermExpression)
|
||||
<|> Parser.preturn (defaultRate, defaultRate)
|
||||
|>> fun (x,y) -> Term.Func (Keywords.massActionRate, [x]), Term.Func (Keywords.massActionRate, [y])))
|
||||
|>> fun (r,r') -> (r,Some r')
|
||||
]
|
||||
//parse products
|
||||
.>>. pmset >>= fun ((fwRate, bwRateOpt), products) ->
|
||||
let bwRate = match bwRateOpt with | None -> Term.Func("",[]) | Some x -> x
|
||||
//create reaction
|
||||
Parser.preturn (
|
||||
match mset2 with
|
||||
| None -> Term.Func(Keywords.reaction, [Term.TMSet([]); mset1; fwRate; bwRate; products])
|
||||
| Some reactants -> Term.Func(Keywords.reaction, [mset1; reactants; fwRate; bwRate; products]))
|
||||
) (kw "|"))
|
||||
|>> Term<'s>.TCRN
|
||||
|
||||
|
||||
|
||||
// disambiguation step
|
||||
(Parser.plookAheadWith
|
||||
(choice [
|
||||
(pname <|> kw "_") >>= fun str ->
|
||||
let isVar = str = "_" || System.Char.IsUpper (str.Chars 0)
|
||||
if isVar
|
||||
then
|
||||
choice [
|
||||
kw "->" >>. preturn PVariable
|
||||
kw "<->" >>. preturn PVariable
|
||||
|
||||
// <CONTEXT>
|
||||
kw "[[" >>. preturn PContext
|
||||
kw "[" >>. preturn PContext
|
||||
|
||||
// <PATTERN>
|
||||
Parser.choice (domainKeywords |> List.map Parser.kw) >>. preturn PPattern
|
||||
|
||||
// <EXPRESSION>
|
||||
if isExp then preturn PVariable else pexp
|
||||
|
||||
kw "is" >>. preturn PVariable
|
||||
kw ">=" >>. preturn PVariable
|
||||
kw "<=" >>. preturn PVariable
|
||||
kw "<" >>. preturn PVariable
|
||||
kw ">" >>. preturn PVariable
|
||||
kw "=" >>. preturn PVariable
|
||||
kw "->" >>. preturn PVariable
|
||||
kw "<->" >>. preturn PVariable
|
||||
|
||||
// complex
|
||||
kw ":" >>. preturn PVariable
|
||||
|
||||
preturn PVariable
|
||||
]
|
||||
elif List.contains str ["sum"; "prod"; "log"; "ceiling"; "floor"; "round"]
|
||||
then preturn PArithmetic
|
||||
else
|
||||
choice [
|
||||
// <OPERATION>
|
||||
kw "(" >>. preturn PFunction
|
||||
|
||||
// <PATTERN>
|
||||
Parser.choice (domainKeywords |> List.map Parser.kw) >>. preturn PPattern
|
||||
|
||||
kw "is" >>. preturn PPattern
|
||||
kw ">=" >>. preturn PPattern
|
||||
kw "<=" >>. preturn PPattern
|
||||
kw "<" >>. preturn PPattern
|
||||
kw ">" >>. preturn PPattern
|
||||
kw "=" >>. preturn PPattern
|
||||
|
||||
kw "@" >>. preturn PPattern
|
||||
// CRN
|
||||
kw "->" >>. preturn PPattern
|
||||
kw "<->" >>. preturn PPattern
|
||||
|
||||
kw ":" >>. preturn PPattern
|
||||
|
||||
// if there is another name, the first name is a domain and the rest is a pattern
|
||||
pname >>. preturn PPattern
|
||||
preturn PPattern
|
||||
]
|
||||
])
|
||||
>>= fun disambiguationWithoutComplex ->
|
||||
let disambiguation =
|
||||
if not isComplex then disambiguationWithoutComplex
|
||||
else match disambiguationWithoutComplex with
|
||||
| PFunction _ -> PFunction
|
||||
// ":" has higher binding priority than e.g. + from an expression
|
||||
| PPattern _ -> PPattern
|
||||
| PVariable
|
||||
| PArithmetic _ -> PVariable
|
||||
| PContext _ -> disambiguationWithoutComplex
|
||||
let f x = if x = "_" then (-1, "_") else idProvider x
|
||||
match disambiguation with
|
||||
| PFunction -> pname .>>. paren (sepBy termParser (kw ",")) |>> Term.Func
|
||||
| PPattern -> ppattern sp idProvider |>> Term.Pat
|
||||
| PArithmetic -> Microsoft.Research.CRNEngine.Expression.parse (doPTerm sp cle true isComplex idProvider domainKeywords) |>> Term.FromExpression
|
||||
| PVariable -> choice [ pname |>> (f >> Term.Var)
|
||||
kw "_" |>> fun x -> Term.Var (-1, x)]
|
||||
// parses process parallel composition such as P1 | P2
|
||||
>>= fun v ->
|
||||
if isExp
|
||||
then preturn v
|
||||
else choice [ kw "|" >>. sepBy1 termParser (kw "|") |>> fun ts -> TList (v :: ts)
|
||||
preturn v ]
|
||||
| PContext -> (pname <|> kw "_") .>>.
|
||||
choice [
|
||||
kw "[[" >>. name .>> spaces .>> kw "]]" |>> (f >> Term.Var)
|
||||
many1 (sqBrackets (ppattern sp idProvider)) |>> (fun ps -> ps |> List.map Term.Pat |> TList)
|
||||
] |>> fun (ctxName, holes) -> Func (Keywords.context, [Term.Var (f ctxName); holes])
|
||||
>>= fun v -> choice [ kw "|" >>. sepBy1 termParser (kw "|") |>> fun ts -> Func ("|", v :: ts)
|
||||
preturn v ]
|
||||
|
||||
)
|
||||
] >>= fun t ->
|
||||
// COMPLEXES
|
||||
Parser.plookAheadWith (choice [ kw "::" >>. preturn false
|
||||
kw ":" >>. preturn true
|
||||
preturn false ])
|
||||
>>= fun isComplex ->
|
||||
if isComplex
|
||||
then
|
||||
let pterm st = doPTerm sp cle isExp true idProvider domainKeywords st
|
||||
kw ":" >>. Parser.sepBy pterm (kw ":") >>= fun ts ->
|
||||
let ts' = t::ts |> List.map (fun x-> 1, x)
|
||||
preturn (Term.TMSet ts')
|
||||
else preturn t
|
||||
) st
|
||||
|
||||
and pterm (sp:Parser.t<'s>) cle (idProvider : string -> (int*string)) (domainKeywords: string list (* the list of keywords that distinguish a variable from a domain specific element (e.g. in DSD "!" turns A in A!i from a generic variable to a DSD variable) *))
|
||||
st : Parser.Result<Term<'s>> = doPTerm sp cle false false idProvider domainKeywords st
|
||||
|
||||
|
||||
let ppredicate cle sp idProvider domainKeywords st =
|
||||
let z = (pterm sp cle idProvider domainKeywords >>= fun t1 ->
|
||||
choice [
|
||||
kw "is" >>. pterm sp cle idProvider domainKeywords |>> fun t2 -> Pred ("is", [t1; t2])
|
||||
kw ">=" >>. pterm sp cle idProvider domainKeywords |>> fun t2 -> Pred (">=", [t1; t2])
|
||||
kw "<=" >>. pterm sp cle idProvider domainKeywords |>> fun t2 -> Pred ("<=", [t1; t2])
|
||||
kw "<" >>. pterm sp cle idProvider domainKeywords |>> fun t2 -> Pred ("<", [t1; t2])
|
||||
kw ">" >>. pterm sp cle idProvider domainKeywords |>> fun t2 -> Pred (">", [t1; t2])
|
||||
kw "=" >>. pterm sp cle idProvider domainKeywords |>> fun t2 ->
|
||||
match t1 with
|
||||
| Func ("_ctx", [Term.Var (i, ctxName); TList holes]) -> Pred ("is", [t2; Term.Var (i, ctxName); TList holes])
|
||||
| Func ("_ctx", [Term.Var (i, ctxName); Term.Var (j, holes)]) -> Pred ("is", [t2; Term.Var (i, ctxName); Term.Var (j, holes)])
|
||||
| Func ("|", _) -> Pred ("is", [t2; t1])
|
||||
| _ -> match t2 with
|
||||
| Func ("_ctx", [Term.Var (i, ctxName); TList holes]) -> Pred ("is", [t1; Term.Var (i, ctxName); TList holes])
|
||||
| Func ("_ctx", [Term.Var (i, ctxName); Term.Var (j, holes)]) -> Pred ("is", [t1; Term.Var (i, ctxName); Term.Var (j, holes)])
|
||||
| Func ("|", _) -> Pred ("is", [t1; t2])
|
||||
| _ -> Pred ("=", [t1; t2])
|
||||
|
||||
// if the parser caught a function but there is no subsequent operation "is", "=", etc.
|
||||
// then turn the function into a predicate
|
||||
(match t1 with
|
||||
| Term.Func (name, args) -> preturn <| Pred (name, args)
|
||||
| _ -> let msg = sprintf "Unexpected predicate %s" (Term.ToStringWith cle t1)
|
||||
failParser msg)
|
||||
])
|
||||
z st
|
||||
(* Atoms syntax:
|
||||
ATOM ::= <NAME> '(' <TERM>* ')'
|
||||
*)
|
||||
let patom cle x y = ppredicate cle x y
|
||||
|
||||
(* Literals syntax:
|
||||
LITERAL ::= <ATOM>
|
||||
| 'not' <ATOM>
|
||||
*)
|
||||
let pliteral cle sp idProvider domainKeywords =
|
||||
choice [
|
||||
kw "not" >>. choice [ paren (patom cle sp idProvider domainKeywords); (patom cle sp idProvider domainKeywords)] |>> Neg
|
||||
(patom cle sp idProvider domainKeywords) |>> Pos
|
||||
]
|
||||
|
||||
(* clause syntax:
|
||||
CLAUSE ::= <NAME> '(' <TERM>* ')' '.' // a stated fact in the prolog database
|
||||
| <NAME> '(' <TERM>* ')' ':-' <LITERAL>* '.' // a derived fact, assuming its body ( the LITERAL* ) holds
|
||||
*)
|
||||
let pclause (cle:CLE<'s, 'a>) sp idProvider =
|
||||
let cache = idProvider ()
|
||||
let speciesParser = sp cache
|
||||
pname .>>. paren (sepBy (pterm speciesParser cle cache cle.domainKeywords) (kw ",")) >>= fun p ->
|
||||
let predicate = Pred p
|
||||
choice [ kw "." >>. preturn (Clause.Create predicate)
|
||||
kw ":-" >>. Parser.sepBy1 (pliteral cle speciesParser cache cle.domainKeywords) (kw ",") .>> kw "." >>= fun atoms ->
|
||||
preturn (Clause.Create(predicate, atoms)) ]
|
||||
|>> cle.disambiguateVars
|
||||
|
||||
(* program syntax: *)
|
||||
let pprogram (cle:CLE<'s, 'a>) (sp : (string -> int * string) -> Parser.t<'s>) : Parser.t<RulesProgram<'s>> =
|
||||
Parser.many (pclause cle sp idProvider)
|
||||
|>> toProgram
|
||||
|
|
@ -0,0 +1,391 @@
|
|||
[<JavaScript>]
|
||||
module RulesDSD.ProcessEquality
|
||||
|
||||
open RulesDSD.Syntax
|
||||
open RulesDSD.Substitution
|
||||
open RulesDSD.Unification
|
||||
|
||||
// TODO: turn into unifyHole
|
||||
let rec patternMatches cle (strand : Hole<'s>) (pattern : Hole<'s>) sol : Substitution<'s, 'a> list =
|
||||
match strand,pattern with
|
||||
| _, [] -> [sol] // match found
|
||||
| [], _ -> [] // the empty strand never matches any pattern
|
||||
|
||||
| h1::hs1, h2::hs2 ->
|
||||
let h1' = sol.Apply(h1, cle)
|
||||
let h2' = sol.Apply(h2, cle)
|
||||
(h1', h2')
|
||||
|> unifyHoleEntry cle
|
||||
|> List.collect (fun theta ->
|
||||
let sol' = Substitution<'s, 'a>.Compose sol theta cle
|
||||
patternMatches cle hs1 hs2 sol')
|
||||
|
||||
// find all pattern matches in a strand. acc is the set of matches found so far, pos is the pattern's index in the strand currently being matched
|
||||
let rec fam cle (strand : Hole<'s>) (pattern : Hole<'s>) acc pos =
|
||||
match strand, pattern with
|
||||
| [], _ -> acc
|
||||
| _, [] -> acc
|
||||
| _::rest, _ ->
|
||||
if strand.Length < pattern.Length
|
||||
then acc
|
||||
else
|
||||
let acc' =
|
||||
patternMatches cle strand pattern Substitution.id
|
||||
|> List.map (fun x -> x, pos)
|
||||
|> Set.ofList
|
||||
|> Set.union acc
|
||||
|
||||
fam cle rest pattern acc' (pos + 1)
|
||||
|
||||
let findAllMatches cle (strand : Hole<'s>) (sites : Hole<'s>) =
|
||||
fam cle strand sites Set.empty 0
|
||||
|
||||
type ProcessEquality = PE
|
||||
with
|
||||
static member FindContexts(Process.Proc sys, patterns: Pattern<'s> list, cle) =
|
||||
let contexts =
|
||||
patterns |> List.fold
|
||||
(fun acc pattern ->
|
||||
match acc with
|
||||
| None -> None // skip remaining patterns if a previous pattern failed to match
|
||||
| Some (previousContexts: Set<Substitution<'s, 'a> * Pattern<'s> list>) ->
|
||||
let dummyHole = []
|
||||
let matches =
|
||||
Map.fold
|
||||
(fun acc (strandID:StrandID) (_strand:Strand<'s>) ->
|
||||
let strand = _strand
|
||||
|> List.mapi (fun i x -> x, Location.Loc (strandID, i))
|
||||
//let _proc = Term.Proc (Process.ofList [_strand])
|
||||
// TODO: optimization: apply substitutions to filter out bad matches early
|
||||
let addPositions pos (sites:Hole<'s>) : Hole<'s> =
|
||||
sites
|
||||
|> List.mapi (fun i s -> (fst s, Location.Loc (strandID, pos+i)))
|
||||
match pattern with
|
||||
//| Hole h -> Set.add (Substitution.id, h) acc
|
||||
| Nihil -> Set.add (Substitution.id, Pattern.Nihil) acc
|
||||
| Pattern.Inner sites ->
|
||||
let matches = findAllMatches cle strand sites
|
||||
if matches.IsEmpty
|
||||
then acc
|
||||
else
|
||||
let newMatches =
|
||||
matches
|
||||
|> Set.map (fun (sub, pos) ->
|
||||
let hole = Pattern.Inner (addPositions pos sites)
|
||||
(sub, hole))
|
||||
Set.union acc newMatches
|
||||
|
||||
| Pattern.Strand sites ->
|
||||
patternMatches cle strand sites Substitution<'s, 'a>.id
|
||||
|> List.fold (fun acc sub ->
|
||||
if sites.Length = strand.Length
|
||||
then
|
||||
let hole = Pattern.Strand (addPositions 0 sites)
|
||||
Set.add (sub, sub.Apply(hole, cle)) acc
|
||||
else acc) acc
|
||||
|
||||
| FivePrime p ->
|
||||
patternMatches cle strand p Substitution.id
|
||||
|> List.fold (fun acc sub ->
|
||||
let hole = Pattern.FivePrime (addPositions 0 p)
|
||||
Set.add (sub, hole) acc) acc
|
||||
|
||||
| ThreePrime p ->
|
||||
let offset = strand.Length - p.Length
|
||||
if offset < 0
|
||||
then acc
|
||||
else
|
||||
let cutStrand = List.skip offset strand
|
||||
patternMatches cle cutStrand p Substitution.id
|
||||
|> List.fold (fun acc sub ->
|
||||
let hole = Pattern.ThreePrime (addPositions offset p)
|
||||
Set.add (sub, hole) acc
|
||||
) acc
|
||||
|
||||
| Nicking (threePrime, fivePrime) ->
|
||||
let offset = strand.Length - threePrime.Length
|
||||
let threePrimeMatch =
|
||||
if offset < 0
|
||||
then []
|
||||
else
|
||||
let cutStrand = List.skip offset strand
|
||||
patternMatches cle cutStrand threePrime Substitution.id
|
||||
let fivePrimeMatch = patternMatches cle strand fivePrime Substitution.id
|
||||
|
||||
(* create two distinct pattern matches for Nicking, one with the matched 3' end and a dummy range, and one with the dummy range and a 5' matched range. This avoid creating a pattern match on two ends of the same strand (it could create a circular pattern).
|
||||
After finding all such patterns in a system, dummy ranges will be replaced by 3' or 5' ranges from other strands. This second step is performed outside the fold loops.*)
|
||||
let tpHole = addPositions offset threePrime
|
||||
let fpHole = addPositions 0 fivePrime
|
||||
let tpPattern = Pattern.Nicking (tpHole, dummyHole)
|
||||
let fpPattern = Pattern.Nicking (dummyHole, fpHole)
|
||||
match threePrimeMatch, fivePrimeMatch with
|
||||
| [], [] -> acc
|
||||
| tps, [] -> tps |> List.map (fun tp -> tp, tpPattern) |> Set.ofList |> Set.union acc
|
||||
| [], fps -> fps |> List.map (fun fp -> fp, fpPattern) |> Set.ofList |> Set.union acc
|
||||
| tps, fps -> let x = tps |> List.map (fun tp -> tp, tpPattern) |> Set.ofList
|
||||
let y = fps |> List.map (fun fp -> fp, fpPattern) |> Set.ofList
|
||||
Set.union (Set.union acc x) y
|
||||
) Set.empty sys
|
||||
|> Set.map (fun (s, h) -> s, s.Apply(h, cle))
|
||||
|
||||
// find all valid combinations of nicking patterns and remove all dummy ranges
|
||||
let newMatches =
|
||||
match pattern with
|
||||
| Nicking _ ->
|
||||
matches |> Set.fold
|
||||
(fun acc nick1 ->
|
||||
Set.remove nick1 matches
|
||||
|> Set.fold (fun acc nick2 ->
|
||||
match nick1, nick2 with
|
||||
| (s1, Nicking (tp1, fp1)), (s2, Nicking (tp2, fp2)) ->
|
||||
let tp1IsDummy = (tp1 = dummyHole)
|
||||
let tp2IsDummy = (tp2 = dummyHole)
|
||||
// skip if the non dummy ranges are both 3' or 5'
|
||||
if (tp1IsDummy && tp2IsDummy)
|
||||
|| (not tp1IsDummy && not tp2IsDummy)
|
||||
then acc
|
||||
else
|
||||
// skip non-mergeable matches
|
||||
match Substitution.TryMerge s1 s2 cle with
|
||||
| None -> acc
|
||||
| Some sub ->
|
||||
let sid (x:Hole<'s>) = match snd x.[0] with
|
||||
| Location.Loc (i, _) -> i
|
||||
| _ -> failwith "Unexpected error in context finding"
|
||||
let tp, fp = if tp1IsDummy
|
||||
then tp2, fp1
|
||||
else tp1, fp2
|
||||
// skip pattern matches on the same strand
|
||||
if sid tp = sid fp
|
||||
then acc
|
||||
else Set.add (sub, Pattern.Nicking (tp, fp)) acc
|
||||
|
||||
// this should not happen
|
||||
| _,_ -> failwith "Unexpected patterns in nicking pattern matching"
|
||||
) acc
|
||||
) Set.empty
|
||||
| _ -> matches
|
||||
if newMatches.IsEmpty
|
||||
then None
|
||||
else
|
||||
let currentContexts =
|
||||
if previousContexts.IsEmpty
|
||||
then // initialize the context by placing each hole in a different hole list
|
||||
matches |> Set.map (fun (x, y) -> (x, [y]))
|
||||
else
|
||||
(* for each matched contex hole, add it to the previous matches only if they don't overlap *)
|
||||
previousContexts
|
||||
|> Set.fold (fun acc (prevSub, prevHoles) ->
|
||||
newMatches
|
||||
|> Set.fold (fun acc (newSub, newHole) ->
|
||||
if prevHoles |> List.forall (newHole.Overlaps >> not)
|
||||
then
|
||||
match Substitution.TryMerge prevSub newSub cle with
|
||||
| Some mergedSub -> Set.add (mergedSub, prevHoles @ [newHole]) acc
|
||||
| None -> acc
|
||||
else acc
|
||||
) acc
|
||||
) Set.empty
|
||||
if currentContexts.IsEmpty
|
||||
then None
|
||||
else Some currentContexts
|
||||
) (Some Set.empty)
|
||||
|
||||
// create a new goal for each matched context
|
||||
match contexts with
|
||||
| None -> None
|
||||
| Some cs ->
|
||||
cs
|
||||
|> Set.toList
|
||||
|> List.map (fun (theta, holes) ->
|
||||
let holes' = holes |> List.map (fun x -> theta.Apply(x, cle) |> Pat) |> TList
|
||||
let p = Process.Proc sys
|
||||
let context = Func ("_ctx", [Term.Proc p; holes'])
|
||||
(theta, context))
|
||||
|> Some
|
||||
|
||||
static member Flatten (cle:CLE<'s,'a>) (t:Term<'s>) =
|
||||
let rec flatten (t:Term<'s>) : Process<'s> option =
|
||||
match t with
|
||||
| Term.Proc p -> Some p
|
||||
| Term.TList ps
|
||||
| Func("|", ps) -> ps
|
||||
|> List.fold (fun acc p ->
|
||||
match acc, flatten p with
|
||||
| Some p1, Some p2 -> Some (cle.ComposeProcesses p1 p2)
|
||||
| _, _ -> None) (Process.OfList [] |> Some)
|
||||
| Func("_ctx", [Func ("_ctx", [Proc (Process.Proc ctxSys); TList ctxHoles]); TList inputHoles])
|
||||
| Func("_ctx", [Proc (Process.Proc ctxSys); TList ctxHoles; TList inputHoles]) ->
|
||||
let newHoles =
|
||||
inputHoles
|
||||
|> List.map (fun pattern ->
|
||||
match pattern with
|
||||
| Pat p -> p
|
||||
| _ -> failwith "Unexpected term in context patterns.")
|
||||
|
||||
let newSys =
|
||||
newHoles
|
||||
|> List.zip ctxHoles
|
||||
|> List.fold
|
||||
(fun (acc:Map<StrandID,Strand<'s>>) (ctxHole, newHole) ->
|
||||
|
||||
let replaceAt oldStrand (startIdx, endIdx) newSites =
|
||||
let start = List.take startIdx oldStrand
|
||||
let ending = List.skip endIdx oldStrand
|
||||
start @ newSites @ ending
|
||||
|
||||
let freshStrandID (p:Map<StrandID, Strand<'s>>) =
|
||||
let max = Map.toList p
|
||||
|> List.map fst
|
||||
|> List.max
|
||||
max + 1
|
||||
let getStrandID (x:Hole<'s>) = match snd x.Head with
|
||||
| Location.Loc (i, _) -> i
|
||||
| _ -> failwith "Unexpected error in context finding"
|
||||
let getStrandStart (x:Hole<'s>) = match snd x.Head with
|
||||
| Location.Loc (_, i) -> i
|
||||
| _ -> failwith "Unexpected error in context finding"
|
||||
|
||||
match ctxHole with
|
||||
(* whole strand substitutions *)
|
||||
| Term.Var _ -> failwith <| sprintf "Insufficiently instantiated variable \"%s\"" (Term.ToString ctxHole)
|
||||
| Pat Pattern.Nihil ->
|
||||
match newHole with
|
||||
| Pattern.Nihil -> acc
|
||||
| Pattern.Strand sites -> acc.Add(freshStrandID acc, List.map fst sites)
|
||||
| _ -> failwith "Mismatching context hole substitution."
|
||||
|
||||
| Pat (Pattern.Strand sites) ->
|
||||
let strandID = getStrandID sites
|
||||
match newHole with
|
||||
| Pattern.Nihil ->
|
||||
acc.Remove strandID
|
||||
| Pattern.Strand sites ->
|
||||
acc.Add(strandID, List.map fst sites)
|
||||
| _ -> failwith "Mismatching context hole substitution."
|
||||
|
||||
(* nick and inner sequences substitutions *)
|
||||
| Pat (Pattern.Inner sites) ->
|
||||
let strandID = getStrandID sites
|
||||
let threePrimeStart = getStrandStart sites
|
||||
let fivePrimeEnd = threePrimeStart + sites.Length
|
||||
|
||||
match newHole with
|
||||
// replace an inner sequence
|
||||
| Pattern.Inner newSites ->
|
||||
let oldStrand = acc.[strandID]
|
||||
let innerRange = (threePrimeStart, fivePrimeEnd)
|
||||
let newStrand = replaceAt oldStrand innerRange (List.map fst newSites)
|
||||
acc.Add(strandID, newStrand)
|
||||
|
||||
// introduce a new nick
|
||||
| Pattern.Nicking (newThreePrimeEnd, newFivePrimeStart) ->
|
||||
let oldStrand = acc.[strandID]
|
||||
let newStrand1 = List.take threePrimeStart oldStrand
|
||||
@ List.map fst newThreePrimeEnd
|
||||
let newStrand2 = List.map fst newFivePrimeStart
|
||||
@ List.skip fivePrimeEnd oldStrand
|
||||
let acc' = acc.Add(strandID, newStrand1)
|
||||
acc'.Add(freshStrandID acc', newStrand2)
|
||||
|
||||
| _ -> failwith "Mismatching context hole substitution."
|
||||
|
||||
| Pat (Pattern.Nicking (sites1, sites2)) ->
|
||||
let strandID1 = getStrandID sites1
|
||||
let strandID2 = getStrandID sites2
|
||||
let tpStart = getStrandStart sites1
|
||||
let fpEnd = sites2.Length
|
||||
|
||||
match newHole with
|
||||
// replace a nick
|
||||
| Pattern.Nicking (newThreePrimeEnd, newFivePrimeStart) ->
|
||||
let oldStrand1 = acc.[strandID1]
|
||||
let oldStrand2 = acc.[strandID2]
|
||||
let newStrand1 = List.take tpStart oldStrand1
|
||||
@ List.map fst newThreePrimeEnd
|
||||
let newStrand2 = List.map fst newFivePrimeStart
|
||||
@ List.take fpEnd oldStrand2
|
||||
acc.Add(strandID1, newStrand1).Add(strandID2, newStrand2)
|
||||
|
||||
// ligate a nick
|
||||
| Pattern.Inner newSites ->
|
||||
let oldStrand1 = acc.[strandID1]
|
||||
let oldStrand2 = acc.[strandID2]
|
||||
let newStrand = List.take tpStart oldStrand1
|
||||
@ List.map fst newSites
|
||||
@ List.take fpEnd oldStrand2
|
||||
acc.Remove(strandID2).Add(strandID1, newStrand)
|
||||
|
||||
| _ -> failwith "Mismatching context hole substitution."
|
||||
|
||||
(* 3' end substitution *)
|
||||
| Pat (Pattern.ThreePrime sites) ->
|
||||
let strandID = getStrandID sites
|
||||
let tpStart = getStrandStart sites
|
||||
|
||||
match newHole with
|
||||
| Pattern.ThreePrime newSites ->
|
||||
let oldStrand = acc.[strandID]
|
||||
let newStrand = List.take tpStart oldStrand @ List.map fst newSites
|
||||
acc.Add(strandID, newStrand)
|
||||
|
||||
| _ -> failwith "Mismatching context hole substitution."
|
||||
|
||||
(* 5' end substitution *)
|
||||
| Pat (Pattern.FivePrime sites) ->
|
||||
let strandID = getStrandID sites
|
||||
|
||||
match newHole with
|
||||
| Pattern.FivePrime newSites ->
|
||||
let oldStrand = acc.[strandID]
|
||||
let fpEnd = sites.Length
|
||||
let newStrand = List.map fst newSites @ List.skip fpEnd oldStrand
|
||||
acc.Add(strandID, newStrand)
|
||||
|
||||
| _ -> failwith "Mismatching context hole substitution."
|
||||
| _ -> failwith <| sprintf "Unexpected term \"%s\" in process \"%s\"" (Term.ToString ctxHole) (Process.ToString (Process.Proc ctxSys))
|
||||
) ctxSys
|
||||
(* CS: the commented out code below is a well-formedness restriction, that has been lifted up for the time being.
|
||||
By enforcing that dangling bonds are not deleted in a context, and that all other bonds are either
|
||||
deleted or added in pairs, result of applying holes to a context is always well-formed.
|
||||
Unfortunately this doesn't let programmers write code that splits complexes and adds bonds to them
|
||||
separately. For example:
|
||||
reaction([P1 ; P2], ...) :-
|
||||
P1 = C1 [D], P2 = C2 [D'],
|
||||
compl(D, D'),
|
||||
Q1 = C1 [D!i], Q2 = C2[D'!i] <----- two dangling bonds
|
||||
Maybe the safety check can be implemented in a separate type system for the rules.
|
||||
*)
|
||||
//let newBondsMap = getBondsMap Pattern.Fold newHoles
|
||||
//if newBondsMap.[0].Length > 0
|
||||
// then None
|
||||
// else
|
||||
// // Dangling pointers check
|
||||
// let rec termFold (f:(Map<Bond,int> -> (SiteT* _) -> Map<Bond,int>))
|
||||
// (acc:Map<Bond,int>)
|
||||
// (t:Term) : Map<Bond,int> =
|
||||
// let g x y = f x (fst y)
|
||||
// match t with
|
||||
// //| Term.Hole h -> Hole.Fold g acc h
|
||||
// | Term.Pat p -> Pattern.Fold f acc p
|
||||
// | Term.Var _ -> acc
|
||||
// // these should not happen
|
||||
// | Term.TList ts -> List.fold (termFold f) acc ts
|
||||
// | Term.TCons (t,t') -> List.fold (termFold f) acc [t;t']
|
||||
// | Term.Float _ -> acc
|
||||
// | Term.Const _ -> acc
|
||||
// | Term.Func _ -> acc // List.fold (termFold f) acc ts
|
||||
// | Term.Proc _ -> acc
|
||||
//| Term.Ctx _ -> acc
|
||||
|
||||
//let oldBondsMap = getBondsMap termFold ctxHoles
|
||||
//let oldDanglingBonds = oldBondsMap.[1]
|
||||
//let newDanglingBonds = newBondsMap.[1]
|
||||
//if oldDanglingBonds <> newDanglingBonds
|
||||
// then None
|
||||
// else
|
||||
// // TODO: bond variables
|
||||
// Some (Process.Proc newSys) // |> Process.Canonical)
|
||||
Some (Process.Proc newSys)
|
||||
| _ -> None
|
||||
flatten t
|
||||
|
|
@ -0,0 +1,702 @@
|
|||
[<JavaScript>]
|
||||
module RulesDSD.Resolution
|
||||
|
||||
open RulesDSD.Syntax
|
||||
open RulesDSD.Substitution
|
||||
open RulesDSD.Unification
|
||||
open RulesDSD.ProcessEquality
|
||||
|
||||
open System.Diagnostics
|
||||
#if JavaScript
|
||||
#else
|
||||
open QuickGraph
|
||||
#endif
|
||||
|
||||
type Mode = SingleAnswer | AllAnswers
|
||||
|
||||
type TJVertex = {n : int; index : int; lowlink : int; onStack:bool}
|
||||
|
||||
// Tarjan's strongly connected components algorithm, from https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm
|
||||
let tarjan (vertices : TJVertex seq) (edges: (int * int) list) =
|
||||
let index = ref 0
|
||||
let S = ref []
|
||||
let result = ref []
|
||||
let state : TJVertex [] = Array.ofSeq vertices
|
||||
|
||||
let rec strongconnect (v:int) =
|
||||
// Set the depth index for v to the smallest unused index
|
||||
let updatedNode = {n = state.[v].n; index = !index; lowlink = !index; onStack = true}
|
||||
Array.set state v updatedNode
|
||||
|
||||
index := !index + 1
|
||||
S := v :: !S
|
||||
|
||||
// Consider successors of v
|
||||
for (v, w) in edges |> List.filter (fun x -> fst x = v) do
|
||||
if state.[w].index = -1
|
||||
then
|
||||
// Successor w has not yet been visited; recurse on it
|
||||
strongconnect(w)
|
||||
Array.set state v { state.[v] with lowlink = min state.[v].lowlink state.[w].lowlink }
|
||||
elif state.[w].onStack
|
||||
// Successor w is in stack S and hence in the current SCC
|
||||
// If w is not on stack, then (v, w) is an edge pointing to an SCC already found and must be ignored
|
||||
// Note: The next line may look odd - but is correct.
|
||||
// It says w.index not w.lowlink; that is deliberate and from the original paper
|
||||
then Array.set state v { state.[v] with lowlink = min state.[v].lowlink state.[w].index }
|
||||
|
||||
|
||||
// If v is a root node, pop the stack and generate an SCC
|
||||
if state.[v].lowlink = state.[v].index then
|
||||
// start a new strongly connected component
|
||||
let x = ref []
|
||||
let c = ref -1
|
||||
while !c = -1 || state.[!c] <> state.[v] do
|
||||
let sHead, sTail =
|
||||
match !S with
|
||||
| x::y -> x,y
|
||||
| [] -> failwith "Unexpected error in SCC computation."
|
||||
S := sTail
|
||||
Array.set state sHead { state.[sHead] with onStack = false }
|
||||
// add w to current strongly connected component
|
||||
c := sHead
|
||||
x := !c :: !x
|
||||
// output the current strongly connected component
|
||||
result := !x :: !result
|
||||
|
||||
// traverse graph
|
||||
let n = Seq.length vertices
|
||||
for v in [0..n-1] do
|
||||
if (state.[v]).index = -1
|
||||
then strongconnect(v)
|
||||
|
||||
// return result
|
||||
!result
|
||||
|
||||
[<DebuggerDisplay("{this.String()}")>]
|
||||
type Goal<'s, 'a when 's : equality and 'a :equality> =
|
||||
{ goals : Literal<'s> list
|
||||
rule : Clause<'s>
|
||||
solution : Substitution<'s, 'a> }
|
||||
with
|
||||
static member Create (s, g, r) = { goals = g; rule = r; solution = s}
|
||||
static member Create (g, r) = { goals = g; rule = r; solution = Substitution<'s, 'a>.id }
|
||||
static member Create (g, cle) =
|
||||
let sol =
|
||||
g
|
||||
|> List.map (fvl cle)
|
||||
|> Set.unionMany
|
||||
|> Set.fold (fun (acc:Substitution<'s, 'a>) v ->
|
||||
match v with
|
||||
| Variable.TVar x -> acc.Add(v, Term.Var x, cle)
|
||||
| Variable.SVar (x,s) -> acc.Add(x, Choice3Of4 s, cle)
|
||||
| Variable.IVar (x,a) -> acc.Add(x, Choice4Of4 a, cle)
|
||||
| Variable.LVar x -> acc.Add(v, Location.Var x, cle)
|
||||
) Substitution<'s, 'a>.id
|
||||
{ goals = g; rule = Clause.Create(Pred("", [])); solution = sol }
|
||||
static member OK : Literal<'s> list = []
|
||||
static member ToString(this:Goal<'s, 'a>, cle) =
|
||||
sprintf "{%s} {%s}" (this.goals |> List.map (fun x -> x.String) |> String.concat ", " ) (this.solution.String cle)
|
||||
member this.String() = Goal.ToString(this, CLE.empty)
|
||||
|
||||
(************************)
|
||||
(************************)
|
||||
(************************)
|
||||
|
||||
let optionMap2 f x y =
|
||||
match x, y with
|
||||
| (Some x', Some y') -> Some (f x' y')
|
||||
| (None, _) -> None
|
||||
| (_, None) -> None
|
||||
|
||||
let rec eval (cle:CLE<'s,_> ) (t:Term<'s>) =
|
||||
match t with
|
||||
| Term.Var _ -> None
|
||||
| Term.Float i -> Some i
|
||||
| Term.Const c -> None
|
||||
// TODO: print context
|
||||
| Term.Func (op, ts) ->
|
||||
if Term.IsExpression t
|
||||
then
|
||||
let e = Term.ToExpression t
|
||||
let err _ = let msg = e |> Microsoft.Research.CRNEngine.Expression.to_string (Term.ToStringWith cle)
|
||||
failwithf "Cannot evaluate expression %s" msg
|
||||
e |> Microsoft.Research.CRNEngine.Expression.eval err
|
||||
|> Some
|
||||
else
|
||||
match op with
|
||||
| "length" -> match ts with
|
||||
| [TList ts] -> Some (float ts.Length)
|
||||
| _ -> None
|
||||
| _ ->
|
||||
let ts' = ts |> List.map (eval cle)
|
||||
let ts'' = ts' |> List.fold (optionMap2 (fun x y -> x@[y])) (Some [])
|
||||
match ts'' with
|
||||
| None -> None
|
||||
| Some ns ->
|
||||
match op with
|
||||
| "+" -> Some <| List.sum ns
|
||||
| "*" -> Some <| List.fold (*) 1.0 ns
|
||||
| "-" -> match ns with
|
||||
| [a; b] -> Some (a - b)
|
||||
| _ -> None
|
||||
|_ -> None
|
||||
| Term.TList _ -> None
|
||||
| Term.TCons _ -> None
|
||||
| Term.Pat _ -> None
|
||||
| Term.Proc _ -> None
|
||||
| Term.TMSet _ -> None
|
||||
| Term.TCRN _ -> None
|
||||
|
||||
let applyP cle (theta:Substitution<'s, 'a>) (Pred (psym, pargs)) =
|
||||
Pred(psym, pargs |> List.map (fun x -> theta.Apply(x, cle)))
|
||||
|
||||
let applyL cle (theta:Substitution<'s, 'a>) lit =
|
||||
match lit with
|
||||
| Pos p -> Pos (applyP cle theta p)
|
||||
| Neg p -> Neg (applyP cle theta p)
|
||||
|
||||
let applyG cle (theta:Substitution<'s, 'a>) goal =
|
||||
match goal with
|
||||
| Pos p -> Pos (applyP cle theta p)
|
||||
| Neg p -> Neg (applyP cle theta p)
|
||||
|
||||
let freshID counter =
|
||||
let n = !counter
|
||||
counter := n + 1
|
||||
n
|
||||
|
||||
let freshName counter =
|
||||
let n = !counter
|
||||
counter := n + 1
|
||||
n
|
||||
|
||||
(****************************************************)
|
||||
(****************************************************)
|
||||
(* Core LSDNF resolution step: unify a goal
|
||||
predicate with some predicate from the program *)
|
||||
(****************************************************)
|
||||
(****************************************************)
|
||||
let rec resolveGoal (program:RulesProgram<'s>) (theta:Substitution<'s, 'a>) (cle:CLE<'s,'a>) varCounter g (*(debugMap:Map<string,System.TimeSpan> ref)*) : (Substitution<'s, 'a> *Substitution<'s, 'a> * Literal<'s> list * Clause<'s>) list option =
|
||||
let extendSolutions cle (theta:Substitution<'s,'a>) debug solutions =
|
||||
match solutions with
|
||||
| [] -> None
|
||||
| sols -> sols |> List.fold (fun acc sol ->
|
||||
let theta' = Substitution<'s, 'a>.Update theta sol cle
|
||||
(sol, theta', Goal<'s, 'a>.OK, debug) :: acc
|
||||
) []
|
||||
|> Some
|
||||
// let t = System.DateTime.Now // uncomment this line, debugMap and related code below to enable performance profiling
|
||||
let r =
|
||||
match cle.resolveGoal (match g with Pred (a,b) -> a,b) (match theta with Sub t -> t) with
|
||||
| Some sols -> Some (sols |> List.map (fun (a,b) -> Sub a, Sub b, Goal<'s,'a>.OK, Clause.Create(Pred("custom", []))))
|
||||
| None ->
|
||||
match g with
|
||||
(*****************)
|
||||
(* Context setup *)
|
||||
(*****************)
|
||||
| Pred ("is", [Term.Var (x,y); Func("|", procs)])
|
||||
-> let flatProcs = procs
|
||||
|> List.choose (ProcessEquality.Flatten cle (*false*))
|
||||
if flatProcs.Length <> procs.Length
|
||||
then None
|
||||
else let flatProc = flatProcs |> List.fold (cle.ComposeProcesses (*false*)) (Process.OfList [])
|
||||
let sol = Substitution<'s, 'a>.Create ((x,y), Term.Proc flatProc)
|
||||
let theta' = Substitution<'s, 'a>.Update theta sol cle
|
||||
Some [sol, theta', Goal<'s, 'a>.OK, Clause.Create( Pred("is",[]))]
|
||||
// holes must be instantiated in order to find a context
|
||||
| Pred ("is", [p; ctx; TCons (x,y)]) ->
|
||||
match TCons (x, y) |> Term.FlattenList with
|
||||
| Choice1Of2 flattenedHoles -> let g' = Pred ("is", [p; ctx; TList flattenedHoles])
|
||||
resolveGoal program theta cle varCounter g' (*debugMap*)
|
||||
| _ -> None
|
||||
| Pred ("is", [Term.TList ps; ctx; ts]) ->
|
||||
match Term.TList ps |> ProcessEquality.Flatten cle (*false*) with
|
||||
| Some p -> let g' = Pred ("is", [Term.Proc p; ctx; ts])
|
||||
resolveGoal program theta cle varCounter g' (*debugMap*)
|
||||
| None -> None
|
||||
|
||||
(*******************)
|
||||
(* Context finding *)
|
||||
(*******************)
|
||||
| Pred ("is", [Term.Proc p; Term.Var (ctx,y); ts]) ->
|
||||
match ts |> Term.FlattenList with
|
||||
| Choice2Of2 _ -> None
|
||||
| Choice1Of2 patternTerms ->
|
||||
let patterns =
|
||||
patternTerms
|
||||
|> List.choose (fun t -> match t with
|
||||
| Pat p -> Some p
|
||||
| _ -> None)
|
||||
if patterns.Length <> patternTerms.Length
|
||||
then None // i.e. resolution fails because one of the holes is not a pattern but some other term
|
||||
else
|
||||
match ProcessEquality.FindContexts(p, patterns, cle) with
|
||||
| None -> None
|
||||
| Some cs ->
|
||||
cs
|
||||
|> List.distinct
|
||||
|> List.map (fun (sub, context) ->
|
||||
let ctxSub = Substitution<'s, 'a>.Create ((ctx,y), context)
|
||||
let sol = Substitution<'s, 'a>.Compose sub ctxSub cle
|
||||
let theta' = Substitution<'s, 'a>.Update theta sol cle
|
||||
(sol, theta', Goal<'s, 'a>.OK, Clause<'s>.Create( Pred("is ctx",[]))))
|
||||
|> Some
|
||||
|
||||
(************************)
|
||||
(* Context substitution *)
|
||||
(************************)
|
||||
// Replace the holes in a context with the patterns
|
||||
| Pred ("is", [sys; Func("_ctx", [Term.Proc (Process.Proc ctxSys); ctxTerm]); ts]) ->
|
||||
match ts |> Term.FlattenList with
|
||||
| Choice2Of2 _ -> None
|
||||
| Choice1Of2 inputHoles ->
|
||||
match ctxTerm with
|
||||
| Term.Var (-1, "_") ->
|
||||
Some [Substitution<'s, 'a>.id, theta, Goal<'s, 'a>.OK, Clause.Create( Pred("is ctx",[]))]
|
||||
| Term.Var (x,y) -> // generate a variable for each input hole, in order to postpone holes unification
|
||||
let varHoles = inputHoles |> List.map (fun _ -> Var (freshID varCounter, "_X"))
|
||||
let sol = Substitution<'s, 'a>.Create((x,y), TList varHoles)
|
||||
let theta' = theta.Add(TVar (x,y), TList varHoles, cle)
|
||||
Some [sol, theta', Goal<'s, 'a>.OK, Clause.Create( Pred("is ctx",[]))]
|
||||
(* // TODO: double check that this is context holes unification
|
||||
*)
|
||||
| TList ctxHoles ->
|
||||
match ProcessEquality.Flatten cle (Func("_ctx", [Proc (Process.Proc ctxSys); TList ctxHoles; TList inputHoles]) ) with
|
||||
| None -> None
|
||||
| Some p ->
|
||||
match sys with
|
||||
| Term.Var (-1, "_") ->
|
||||
let sol = Substitution<'s, 'a>.id
|
||||
Some [sol, theta, Goal<'s, 'a>.OK, Clause.Create( Pred("is ctx",[]) ) ]
|
||||
| Term.Var (sysVar, y) ->
|
||||
let sol = Substitution<'s, 'a>.Create((sysVar, y), Term.Proc p)
|
||||
let theta' : Substitution<'s, 'a> = theta.Add(TVar (sysVar, y), Term.Proc p, cle)
|
||||
Some [sol, theta', Goal<'s, 'a>.OK, Clause.Create( Pred("is ctx",[]) ) ]
|
||||
| Proc q ->
|
||||
if cle.toCanonicalFormProcess p = cle.toCanonicalFormProcess q
|
||||
then Some [Substitution<'s, 'a>.id, theta, Goal<'s, 'a>.OK, Clause.Create( Pred("is ctx",[]) ) ]
|
||||
else None
|
||||
| _ -> None
|
||||
| _ -> None
|
||||
|
||||
(**********************)
|
||||
(* Strand conversions *)
|
||||
(**********************)
|
||||
| Pred ("length", [t1; t2])
|
||||
-> match Term.FlattenList t1 with
|
||||
| Choice1Of2 ts -> unify cle [TEq (Float (float ts.Length), t2) ]
|
||||
|> extendSolutions cle theta (Clause.Create(Pred("length",[])))
|
||||
| Choice2Of2 _ -> None
|
||||
(**********************)
|
||||
(* Graph operations *)
|
||||
(**********************)
|
||||
| Pred ("tscc", [t1; t2])
|
||||
| Pred ("scc", [t1; t2])
|
||||
-> match Term.FlattenList t1 with
|
||||
| Choice1Of2 ts1 ->
|
||||
// t1 must be a list of pairs (node n, list of neighbours of n)
|
||||
let pairs : ((Process<'s> * Process<'s> list) list) option =
|
||||
ts1 |> List.fold (fun acc x ->
|
||||
match acc with
|
||||
| Some accx ->
|
||||
match x with
|
||||
| TList [Term.Proc source; ts2] ->
|
||||
match ts2 with
|
||||
| TList procs ->
|
||||
procs |> List.fold (fun accy y ->
|
||||
match accy with
|
||||
| None -> None
|
||||
| Some ps -> match y with
|
||||
| Term.Proc py -> Some (py::ps)
|
||||
| _ -> None) (Some [])
|
||||
|> fun tgs -> match tgs with
|
||||
| Some targets -> Some ((source, targets) :: accx)
|
||||
| None -> None
|
||||
| _ -> None
|
||||
| _ -> None
|
||||
| None -> None
|
||||
) (Some [])
|
||||
match pairs with
|
||||
| None -> None
|
||||
| Some edges ->
|
||||
// manual implementation of Tarjan's Strongly Connected Components algorithm, from https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm
|
||||
#if JavaScript
|
||||
let e =
|
||||
edges
|
||||
|> List.map (fun (source, ts) ->
|
||||
ts
|
||||
|> List.map (fun target -> (source, target)))
|
||||
|> List.concat
|
||||
let procs =
|
||||
e
|
||||
|> List.collect (fun (x,y) -> [x;y])
|
||||
|> List.distinct
|
||||
let iProcs = procs |> List.indexed
|
||||
let procToIndex = iProcs |> List.map (fun (x,y) -> y,x) |> Map.ofList
|
||||
let indexToProc = iProcs |> Map.ofList
|
||||
|
||||
let prefs = iProcs |> List.map (fun (x, y) -> x, { n = procToIndex.[y]; index = -1; lowlink = -1; onStack = false})
|
||||
let indexToRef = prefs |> Map.ofList
|
||||
let edgess = e |> List.map (fun (x,y) -> procToIndex.[x], procToIndex.[y])
|
||||
let vertices =
|
||||
edgess
|
||||
|> List.collect (fun (x, y) -> [x; y])
|
||||
|> List.distinct
|
||||
|> List.map (fun i -> indexToRef.[i])
|
||||
|
||||
let sccs = tarjan vertices edgess
|
||||
let sccDict =
|
||||
sccs
|
||||
|> List.indexed
|
||||
|> List.collect (fun (i, procIndexes) -> procIndexes |> List.map (fun x -> indexToProc.[x], i))
|
||||
|> Map.ofList
|
||||
#else
|
||||
// NON-JAVASCRIPT PATH
|
||||
// create QuickGraph digraph g
|
||||
let e = edges |> List.map (fun (source, ts) ->
|
||||
ts |> List.map (fun target ->
|
||||
new SEdge<Process<'s>>(source, target)
|
||||
)
|
||||
)
|
||||
|> List.concat
|
||||
let agraph = e.ToAdjacencyGraph()
|
||||
|
||||
// compute strongly connected components of g
|
||||
let sccAlgo = QuickGraph.Algorithms.ConnectedComponents.StronglyConnectedComponentsAlgorithm agraph
|
||||
sccAlgo.Compute()
|
||||
|
||||
|
||||
// convert sccs into Terms
|
||||
let sccDict = sccAlgo.Components
|
||||
let procs = sccDict.Keys
|
||||
#endif
|
||||
|
||||
let toTerm = Seq.map (fun (_, cc) -> TList (cc |> Seq.map Term.Proc |> Seq.toList))
|
||||
>> Seq.toList
|
||||
>> TList
|
||||
let scc = procs |> Seq.groupBy (fun p -> sccDict.[p])
|
||||
if g.Name = "tscc"
|
||||
then
|
||||
let componentsMap =
|
||||
edges
|
||||
|> List.map (fun (x, ys) -> x, ys |> List.map (fun y -> sccDict.[y]) |> List.distinct)
|
||||
|> Map.ofList
|
||||
let tscc =
|
||||
scc
|
||||
|> Seq.filter ( fun (i, cc) ->
|
||||
let targetCcs =
|
||||
cc
|
||||
|> Seq.map (fun i -> componentsMap.[i])
|
||||
|> Seq.concat
|
||||
|> Seq.distinct
|
||||
let l = targetCcs |> Seq.length
|
||||
if l = 1
|
||||
then targetCcs |> Seq.head = i
|
||||
else l = 0
|
||||
)
|
||||
unify cle [TEq (tscc |> toTerm, t2) ]
|
||||
|> extendSolutions cle theta (Clause.Create(Pred("tscc",[])))
|
||||
else
|
||||
unify cle [TEq (scc |> toTerm, t2) ]
|
||||
|> extendSolutions cle theta (Clause.Create(Pred("scc",[])))
|
||||
| Choice2Of2 _ -> None
|
||||
|
||||
(***************)
|
||||
(* Arithmetics *)
|
||||
(***************)
|
||||
| Pred ("is", [Term.Var (x,y); aExpr])
|
||||
| Pred ("is", [aExpr; Term.Var (x,y)]) ->
|
||||
(* eval evaluates an expression to a number*)
|
||||
match eval cle aExpr with
|
||||
| Some n ->
|
||||
let sol = Substitution<'s, 'a>.Create((x,y), Float n)
|
||||
let theta' : Substitution<'s, 'a> = theta.Add(TVar (x,y), Float n, cle)
|
||||
Some [sol, theta', Goal<'s, 'a>.OK, Clause.Create( Pred("is",[]) ) ]
|
||||
| None -> None
|
||||
|
||||
(**********************)
|
||||
(* Boolean operations *)
|
||||
(**********************)
|
||||
| Pred ("<", [aExpr; bExpr]) ->
|
||||
match eval cle aExpr with
|
||||
| Some n1 ->
|
||||
match eval cle bExpr with
|
||||
| Some n2 ->
|
||||
if n1 < n2
|
||||
then Some [Substitution.id, theta, Goal<'s, 'a>.OK, Clause.Create( Pred("<",[]) ) ]
|
||||
else None
|
||||
| None -> None
|
||||
| None -> None
|
||||
| Pred ("<", _ ) -> failwith <| sprintf "unsupported arithmetic operation \"%s\"" g.String
|
||||
| Pred ("<=", [aExpr; bExpr]) ->
|
||||
match eval cle aExpr with
|
||||
| Some n1 ->
|
||||
match eval cle bExpr with
|
||||
| Some n2 ->
|
||||
if n1 <= n2
|
||||
then Some [Substitution.id, theta, Goal<'s, 'a>.OK, Clause.Create( Pred("<=",[]) ) ]
|
||||
else None
|
||||
| None -> None
|
||||
| None -> None
|
||||
| Pred ("<=", _ ) -> failwith <| sprintf "unsupported arithmetic operation \"%s\"" g.String
|
||||
| Pred (">", [aExpr; bExpr]) ->
|
||||
match eval cle aExpr with
|
||||
| Some n1 ->
|
||||
match eval cle bExpr with
|
||||
| Some n2 ->
|
||||
if n1 > n2
|
||||
then Some [Substitution.id, theta, Goal<'s, 'a>.OK, Clause.Create( Pred(">",[]) )]
|
||||
else None
|
||||
| None -> None
|
||||
| None -> None
|
||||
| Pred (">", _ ) -> failwith <| sprintf "unsupported arithmetic operation \"%s\"" g.String
|
||||
| Pred (">=", [aExpr; bExpr]) ->
|
||||
match eval cle aExpr with
|
||||
| Some n1 ->
|
||||
match eval cle bExpr with
|
||||
| Some n2 ->
|
||||
if n1 >= n2
|
||||
then Some [Substitution.id, theta, Goal<'s, 'a>.OK, Clause.Create( Pred(">=",[]) ) ]
|
||||
else None
|
||||
| None -> None
|
||||
| None -> None
|
||||
| Pred (">=", _ ) -> failwith <| sprintf "unsupported arithmetic operation \"%s\"" g.String
|
||||
// unify two terms
|
||||
| Pred ("=", [t1; t2]) ->
|
||||
unify cle [TEq(t1, t2)]
|
||||
|> extendSolutions cle theta (Clause.Create( Pred("=",[])))
|
||||
|
||||
(*******************)
|
||||
(* List operations *)
|
||||
(*******************)
|
||||
// list membership
|
||||
| Pred ("member", [t; t']) ->
|
||||
match Term.FlattenList t' with
|
||||
| Choice1Of2 ts -> ts
|
||||
|> List.map (fun t' ->
|
||||
Substitution.id, theta, [Pos (Pred ("=", [t;t']))], Clause.Create (Pred("member",[]))
|
||||
)
|
||||
|> Some
|
||||
| _ -> None
|
||||
// list containment check (no unification is called)
|
||||
| Pred ("contains", [t; t']) ->
|
||||
match Term.FlattenList t' with
|
||||
| Choice1Of2 ts -> if ts |> List.contains t
|
||||
then Some [Substitution.id, theta, Goal<'s, 'a>.OK, Clause.Create( Pred("contains",[]) )]
|
||||
else None
|
||||
| _ -> None
|
||||
|
||||
// reverse a list
|
||||
| Pred ("reverse", [ts; x]) ->
|
||||
match Term.FlattenList ts with
|
||||
|Choice1Of2 t ->
|
||||
unify cle [TEq(List.rev t |> TList, x)]
|
||||
|> extendSolutions cle theta (Clause.Create( Pred("reverse",[]) ) )
|
||||
| Choice2Of2 _ -> None
|
||||
|
||||
// append two lists together
|
||||
| Pred ("append", [ts1; ts2; x]) ->
|
||||
match Term.FlattenList ts1, Term.FlattenList ts2 with
|
||||
|Choice1Of2 t1, Choice1Of2 t2 ->
|
||||
let t3 = t1@t2
|
||||
unify cle [TEq (t3 |> TList, x)]
|
||||
|> extendSolutions cle theta (Clause.Create( Pred("append",[]) ) )
|
||||
| _ -> None
|
||||
|
||||
// similar to List.concat
|
||||
| Pred ("concat", [ts; x]) ->
|
||||
let concat x =
|
||||
x
|
||||
|> List.fold (fun acc t -> match t |> Term.FlattenList with
|
||||
| Choice1Of2 ts -> (List.rev ts) @ acc
|
||||
| _ -> failwith <| sprintf "Cannot concat indeterminate list %s " (Term.ToString t)) []
|
||||
|> List.rev
|
||||
match Term.FlattenList ts with
|
||||
| Choice1Of2 tlist ->
|
||||
unify cle [TEq (x, concat tlist |> TList)]
|
||||
|> extendSolutions cle theta (Clause.Create(Pred("concat",[])))
|
||||
| Choice2Of2 (tlist, rest) ->
|
||||
unify cle [TEq (x, TCons(concat tlist |> TList, rest))]
|
||||
|> extendSolutions cle theta (Clause.Create( Pred("concat",[])))
|
||||
// sorts a list; duplicates are maintained
|
||||
| Pred ("sort", [ts; x]) ->
|
||||
match Term.FlattenList ts with
|
||||
|Choice1Of2 t ->
|
||||
unify cle [TEq(List.sort t |> TList, x)]
|
||||
|> extendSolutions cle theta (Clause.Create( Pred("reverse",[]) ) )
|
||||
| Choice2Of2 _ -> None
|
||||
// removes duplicates from a list
|
||||
| Pred ("distinct", [ts; x]) ->
|
||||
match Term.FlattenList ts with
|
||||
|Choice1Of2 t ->
|
||||
unify cle [TEq(t |> List.distinct |> TList, x)]
|
||||
|> extendSolutions cle theta (Clause.Create( Pred("reverse",[]) ) )
|
||||
| Choice2Of2 _ -> None
|
||||
|
||||
| Pred ("difference", [ts1; ts2; x]) ->
|
||||
match Term.FlattenList ts1, Term.FlattenList ts2 with
|
||||
| Choice1Of2 t1, Choice1Of2 t2 ->
|
||||
let d = t1 |> List.filter (fun t -> not (List.contains t t2))
|
||||
unify cle [TEq(TList d, x)]
|
||||
|> extendSolutions cle theta (Clause.Create( Pred("reverse",[]) ) )
|
||||
| _, _ -> None
|
||||
|
||||
| Pred ("intersection", [ts1; ts2; x]) ->
|
||||
match Term.FlattenList ts1, Term.FlattenList ts2 with
|
||||
| Choice1Of2 t1, Choice1Of2 t2 ->
|
||||
let terms, theta' =
|
||||
t1
|
||||
|> List.fold (fun (tAcc, sol:Substitution<'s, 'a>) t ->
|
||||
let sol' = t2
|
||||
|> List.map (fun x -> sol.Apply(x, cle))
|
||||
|> List.collect (fun z -> unify cle [TEq(z, t)])
|
||||
match sol' with
|
||||
| [] -> (tAcc, Substitution.Update sol theta cle)
|
||||
| thetas -> (t::tAcc, Substitution.Update sol theta cle)
|
||||
) ([], Substitution.id)
|
||||
|> fun (ts, sol) -> let ts' = ts |> List.rev |> List.map (fun x-> theta.Apply(x, cle)) |> TList
|
||||
ts', sol
|
||||
match unify cle [TEq (x, terms)] with
|
||||
| [] -> None
|
||||
| thetas ->
|
||||
thetas
|
||||
|> List.map (fun theta'' ->
|
||||
let sol = Substitution.Compose theta' theta'' cle
|
||||
let theta''' = theta
|
||||
|> fun x -> Substitution.Update x theta' cle
|
||||
|> fun x -> Substitution.Update x theta'' cle
|
||||
sol, theta''', Goal<'s, 'a>.OK, Clause.Create( Pred("intersection",[]) ))
|
||||
|> Some
|
||||
| _ -> None
|
||||
|
||||
(*******************)
|
||||
(* meta predicates *)
|
||||
(*******************)
|
||||
// findAll(+X, +p(a1, ..., X, ... aN), -Xs)
|
||||
// returns Xs, the list of all variables X such that satisfy predicate p(a1, ..., X, ... aN)
|
||||
| Pred ("findAll", [t; Term.Func(f, args); Term.Var (xs,ys)]) ->
|
||||
let p = Pred (f, args)
|
||||
let g = Goal<'s, 'a>.Create ([Pos p], cle)
|
||||
match resolveInner [g] cle varCounter program [] AllAnswers (*debugMap*) with
|
||||
| Some gmatches ->
|
||||
let res = gmatches
|
||||
|> List.map (fun (sub:Substitution<'s, 'a>)-> sub.Apply(t, cle))
|
||||
|> List.distinct
|
||||
|> TList
|
||||
unify cle [TEq(res, Term.Var (xs,ys))]
|
||||
|> extendSolutions cle theta (Clause.Create( Pred("reverse",[]) ) )
|
||||
| None -> unify cle [TEq(TList [], Term.Var (xs,ys))]
|
||||
|> extendSolutions cle theta (Clause.Create( Pred("reverse",[]) ) )
|
||||
|
||||
(***********************************)
|
||||
(* Unify query with program clause *)
|
||||
(***********************************)
|
||||
| Pred (gSym, gArgs) ->
|
||||
let key = gSym, gArgs.Length
|
||||
if not <| program.ContainsKey key
|
||||
then None
|
||||
else
|
||||
program.Item key
|
||||
|> Set.toList // TODO: replace with Set.filter
|
||||
|> List.choose (fun rule ->
|
||||
match rule.head with
|
||||
| Pred (pSym, pArgs) ->
|
||||
if pSym = gSym && pArgs.Length = gArgs.Length
|
||||
then // unify goal with a clause in the program
|
||||
let idCache : Map<string, int> ref = emptyIdCache ()
|
||||
let idProvider = cachedIdProvider varCounter idCache >> fst
|
||||
let freshArgs = pArgs |> List.map (Term.refresh cle idProvider)
|
||||
let eqs = List.zip gArgs freshArgs
|
||||
|> List.map TEq
|
||||
match unify cle eqs with
|
||||
| [] -> None
|
||||
| sols -> sols
|
||||
|> List.fold (fun acc sol ->
|
||||
let theta' = Substitution.Update theta sol cle
|
||||
let freshBody = rule.body |> List.map (Literal<'s>.refresh cle idProvider >> applyG cle sol)
|
||||
(sol, theta', freshBody, rule) :: acc) []
|
||||
|> Some
|
||||
else None)
|
||||
|> List.concat
|
||||
|> fun x -> if x.IsEmpty then None else Some x
|
||||
(* // performance profiling
|
||||
let dt = System.DateTime.Now - t
|
||||
match (!debugMap).TryFind g.Name with
|
||||
| None -> debugMap := (!debugMap).Add(g.Name, dt)
|
||||
| Some t' -> debugMap := (!debugMap).Add(g.Name, t' + dt)
|
||||
*)
|
||||
r
|
||||
|
||||
and resolveInner (slds:Goal<'s, 'a> list) cle varCounter program oldSolutions mode (*debugMap*) =
|
||||
match slds with
|
||||
| [] -> None
|
||||
| _ ->
|
||||
let expandGoal (sld:Goal<'s, 'a>) : Goal<'s, 'a> list =
|
||||
match sld.goals with
|
||||
// SLD resolution
|
||||
| Pos atom :: gs ->
|
||||
if mode = AllAnswers && atom |> fvp cle |> Set.isEmpty
|
||||
then
|
||||
let oneQueryOnly = Goal<'s, 'a>.Create([Pos atom], cle)
|
||||
|> List.singleton
|
||||
match resolveInner oneQueryOnly cle varCounter program [] SingleAnswer (*debugMap*) with
|
||||
| Some _ -> (sld.solution, gs, Clause.Create (Pred (sprintf "not(%s)" atom.String,[])))
|
||||
|> Goal<'s, 'a>.Create
|
||||
|> List.singleton
|
||||
| None -> []
|
||||
else
|
||||
match resolveGoal program sld.solution cle varCounter atom (*debugMap*) with
|
||||
// create a new SLD node for each match
|
||||
| Some gmatches ->
|
||||
gmatches
|
||||
|> List.map (fun (tmpSol, sol', newGoals, rule) ->
|
||||
let gs' = newGoals @ (gs |> List.map (applyL cle tmpSol) )
|
||||
Goal<'s, 'a>.Create(sol', gs', rule.head |> applyP cle tmpSol |> Clause.Create))
|
||||
|
||||
// resolution failed; remove the SLD node from the list
|
||||
| None -> []
|
||||
// negation-as-failure (NF)
|
||||
| Neg atom :: gs ->
|
||||
// Floundering check: try to disprove ground atoms only (otherwise SLDNF might be unsound)
|
||||
(* TODO: this check could be relaxed by allowing goals to have variables,
|
||||
and fail NF only if all solutions always contain the empty substitution.
|
||||
Some Prolog implementations do not check for floundering at all.
|
||||
(see pg. 74, "Logic, Programming and Prolog" by U. Nilsson, J. Maluszynski *)
|
||||
if Set.isEmpty (fvp cle atom)
|
||||
then
|
||||
let counterProof = Goal<'s, 'a>.Create([Pos atom], cle)
|
||||
match resolveInner [counterProof] cle varCounter program [] SingleAnswer (*debugMap*) with
|
||||
| None -> [sld.solution, gs, Clause<'s>.Create (Pred (sprintf "not(%s)" atom.String,[]))]
|
||||
|> List.map Goal<'s, 'a>.Create
|
||||
| Some _ -> [] // negation failed
|
||||
else []
|
||||
| [] -> []
|
||||
|
||||
match mode with
|
||||
| SingleAnswer ->
|
||||
let slds' = slds |> List.collect expandGoal
|
||||
match slds' |> List.tryFind (fun s -> s.goals.IsEmpty) with
|
||||
| Some sld -> Some [sld.solution]
|
||||
| None -> if slds' = slds
|
||||
then None
|
||||
else resolveInner slds' cle varCounter program [] mode (*debugMap*)
|
||||
| AllAnswers ->
|
||||
let g, gs = slds.Head, slds.Tail
|
||||
let successfulSlds, newSlds = g |> expandGoal |> List.partition (fun s -> s.goals.IsEmpty)
|
||||
let newSolutions = successfulSlds |> List.map (fun g -> g.solution)
|
||||
let sols = oldSolutions @ newSolutions
|
||||
if newSlds.IsEmpty && gs.IsEmpty
|
||||
then if sols.IsEmpty
|
||||
then None
|
||||
else Some sols
|
||||
else resolveInner (newSlds @ gs) cle varCounter program sols mode (*debugMap*)
|
||||
|
||||
let resolve goal (program:RulesProgram<'s>) (cle:CLE<'s, 'a>) (*debugMap*) =
|
||||
let counter = fvl cle goal |> Set.count |> fun x -> x + 1 |> ref
|
||||
resolveInner [Goal<'s, 'a>.Create([goal], cle)] cle counter program [] SingleAnswer (*debugMap*)
|
||||
|> Option.map List.head
|
||||
|
||||
let resolveAll (goal:Literal<'s>) (program:RulesProgram<'s>) (cle:CLE<'s,'a>) =
|
||||
let counter = fvl cle goal |> Set.count |> fun x -> x + 1 |> ref
|
||||
resolveInner [Goal<'s, 'a>.Create([goal], cle)] cle counter program [] AllAnswers
|
||||
|
|
@ -0,0 +1,229 @@
|
|||
[<JavaScript>]
|
||||
module RulesDSD.Substitution
|
||||
|
||||
open RulesDSD.Syntax
|
||||
|
||||
open System.Diagnostics
|
||||
|
||||
let mapUnion (loses: Map<_,_>) (wins: Map<_,_>) =
|
||||
Seq.fold (fun m (KeyValue(k,v)) -> Map.add k v m) loses wins
|
||||
|
||||
[<DebuggerDisplay("{this.String}")>]
|
||||
type Substitution<'s, 'a when 's :equality and 'a :equality> = Sub of Map<Var, Choice<Term<'s>, Location, 's, 'a>>
|
||||
with
|
||||
static member Apply (Sub sub:Substitution<'s, 'a>, s:'s, cle:CLE<'s, 'a>) : 's = cle.applyAll sub (Choice1Of2 s)
|
||||
static member Apply (Sub sub:Substitution<'s, 'a>, a:'a, cle:CLE<'s, 'a>) : 'a = cle.applySubVar sub a
|
||||
|
||||
(* identity substitution *)
|
||||
static member id : Substitution<'s, 'a> = Sub Map.empty
|
||||
static member Create (x:Var, t:Term<'s>) : Substitution<'s, 'a> = Sub (Map.ofList [x, Choice1Of4 t])
|
||||
static member Create (x:Var, l:Location) : Substitution<'s, 'a> = Sub (Map.ofList [x, Choice2Of4 l])
|
||||
static member Create (x:Var, s:'s) : Substitution<'s, 'a> = Sub (Map.ofList [x, Choice3Of4 s])
|
||||
static member Create (x:Var, s:'a) : Substitution<'s, 'a> = Sub (Map.ofList [x, Choice4Of4 s])
|
||||
|
||||
(* add a binding *)
|
||||
member this.Add(k:Variable<'s, 'a>, t:Term<'s>, cle:CLE<'s, 'a>) =
|
||||
match k with
|
||||
| TVar x ->
|
||||
let sub : Substitution<'s, 'a> = Substitution<'s, 'a>.Create(x, t)
|
||||
Substitution.Compose this sub cle
|
||||
| _ -> failwith <| sprintf "Substitution extension failed: cannot extend %s with %s" (this.String cle) k.String
|
||||
|
||||
member this.Add(k:Variable<'s, 'a>, l:Location, cle:CLE<'s, 'a>) =
|
||||
match k with
|
||||
| LVar x ->
|
||||
let sub : Substitution<'s, 'a> = Substitution<'s, 'a>.Create(x, l)
|
||||
Substitution.Compose this sub cle
|
||||
| _ -> failwith <| sprintf "Substitution extension failed: cannot extend %s with %s" (this.String cle) k.String
|
||||
|
||||
member this.Add(k, x:'a, cle:CLE<'s, 'a>) =
|
||||
let sub = Substitution<'s, 'a>.Create(k, x)
|
||||
Substitution.Compose this sub cle
|
||||
|
||||
member this.Add(k, c:Choice<Term<'s>, Location, 's, 'a>, cle:CLE<'s, 'a>) =
|
||||
let sub = match c with
|
||||
| Choice1Of4(x) -> Substitution<'s, 'a>.Create(k, x)
|
||||
| Choice2Of4(x) -> Substitution<'s, 'a>.Create(k, x)
|
||||
| Choice3Of4(x) -> Substitution<'s, 'a>.Create(k, x)
|
||||
| Choice4Of4(x) -> Substitution<'s, 'a>.Create(k, x)
|
||||
Substitution.Compose this sub cle
|
||||
|
||||
(* map values *)
|
||||
member this.Map (f : Var -> Term<'s> -> Term<'s>) =
|
||||
let wrapper x y = match y with
|
||||
| Choice1Of4 z -> Choice1Of4 (f x z)
|
||||
| _ -> y
|
||||
match this with Sub m -> Sub (Map.map wrapper m)
|
||||
member this.Map (f : Var -> Location -> Location) =
|
||||
let wrapper x y = match y with
|
||||
| Choice2Of4 z -> Choice2Of4 (f x z)
|
||||
| _ -> y
|
||||
match this with Sub m -> Sub (Map.map wrapper m)
|
||||
|
||||
member this.Map (f : Var -> 's -> 's) =
|
||||
let wrapper x y = match y with
|
||||
| Choice3Of4 z -> Choice3Of4 (f x z)
|
||||
| _ -> y
|
||||
match this with Sub m -> Sub (Map.map wrapper m)
|
||||
|
||||
member this.Map (f : Var -> 'a -> 'a) =
|
||||
let wrapper x y = match y with
|
||||
| Choice4Of4 z -> Choice4Of4 (f x z)
|
||||
| _ -> y
|
||||
match this with Sub m -> Sub (Map.map wrapper m)
|
||||
|
||||
static member Apply (Sub sub:Substitution<'s, 'a>, loc:Location) : Location =
|
||||
match loc with
|
||||
| Location.Var (-1, "_") -> Location.Var (-1, "_")
|
||||
| Location.Var v -> match sub.TryFind(v) with
|
||||
| Some (Choice2Of4 l) -> l
|
||||
| Some (Choice1Of4 _)
|
||||
| Some (Choice3Of4 _)
|
||||
| Some (Choice4Of4 _)
|
||||
| None -> loc
|
||||
| Location.Loc _ -> loc
|
||||
|
||||
static member Apply (sub, (s:'s, l:Location), cle:CLE<'s, 'a>) = Substitution<'s, 'a>.Apply(sub, s, cle), Substitution<'s, 'a>.Apply(sub, l)
|
||||
static member Apply (Sub sub, p:Pattern<'s>, cle:CLE<'s, 'a>) = p |> Pattern.Map (fun (s, l) -> (cle.applyAll sub (Choice1Of2 s), Substitution<'s, 'a>.Apply(Sub sub, l)))
|
||||
static member Apply (Sub s : Substitution<'s, 'a>, t:Term<'s>, cle:CLE<'s, 'a>) : Term<'s> =
|
||||
let sub : Substitution<'s, 'a> = Sub s
|
||||
match t with
|
||||
| Term.Var (-1, "_") -> t
|
||||
| Term.Var (x,y) -> match s.TryFind((x,y)) with
|
||||
| Some (Choice1Of4 t') -> t'
|
||||
| Some (Choice2Of4 l) -> Pat <| Pattern.Inner [cle.underscore(), l]
|
||||
| Some (Choice3Of4 sp) -> Pat <| Pattern.Inner [cle.applyAll s (Choice1Of2 sp), Location.Var (-1,"_")]
|
||||
| Some (Choice4Of4 sp) -> Pat <| Pattern.Inner [cle.applySubVar s sp |> cle.cast, Location.Var (-1,"_")]
|
||||
| None -> t
|
||||
|
||||
| Term.Const _ -> t
|
||||
| Term.Float _ -> t
|
||||
| Term.Func (f, ts) -> Term<'s>.Func (f, ts |> List.map (fun t -> sub.Apply(t, cle)))
|
||||
| Term.TList ts -> Term<'s>.TList (ts |> List.map (fun t -> sub.Apply(t, cle)))
|
||||
| Term.TCons (t, t') -> Term<'s>.TCons (sub.Apply(t, cle), sub.Apply(t', cle))
|
||||
| Term.Pat p -> Substitution<'s, 'a>.Apply(sub, p, cle) |> Pat
|
||||
| Term.Proc s -> s |> Process<'s>.Map (fun (x:'s) -> Substitution<'s, 'a>.Apply(sub, x, cle)) |> Proc
|
||||
| Term.TCRN ts -> ts
|
||||
|> List.map (fun t -> sub.Apply(t, cle))
|
||||
|> List.distinct
|
||||
|> TCRN
|
||||
| Term.TMSet ts -> ts
|
||||
|> List.map (fun (n, t) -> n, sub.Apply(t, cle))
|
||||
|> TMSet
|
||||
|
||||
member this.Apply(term:Term<'s>, cle:CLE<'s, 'a>) = Substitution<'s, 'a>.Apply(this, term, cle)
|
||||
member this.Apply(loc:Location) = Substitution<'s, 'a>.Apply(this, loc)
|
||||
member this.Apply(sp:'s, cle:CLE<'s, 'a>) = Substitution<'s, 'a>.Apply(this, sp, cle)
|
||||
member this.Apply(a:'a, cle:CLE<'s, 'a>) = Substitution<'s, 'a>.Apply(this, a, cle)
|
||||
member this.Apply(x:Choice<Term<'s>, Location, 's, 'a>, cle:CLE<'s, 'a>) =
|
||||
match x with
|
||||
| Choice1Of4 t -> this.Apply(t, cle) |> Choice1Of4
|
||||
| Choice2Of4 l -> this.Apply l |> Choice2Of4
|
||||
| Choice3Of4 s -> this.Apply(s, cle) |> Choice3Of4
|
||||
| Choice4Of4 a -> this.Apply(a, cle) |> Choice4Of4
|
||||
member this.Apply(p:Pattern<'s>, cle:CLE<'s,'a>) = Substitution<'s, 'a>.Apply(this, p, cle)
|
||||
member this.Apply((s:'s, l:Location), cle:CLE<'s, 'a>) = Substitution<'s, 'a>.Apply(this, s, cle), Substitution<'s, 'a>.Apply(this, l)
|
||||
member this.Apply(p:RulesDSD.Syntax.Predicate<'s>, cle:CLE<'s, 'a>) =
|
||||
match p with
|
||||
| RulesDSD.Syntax.Predicate.Pred(x,y) -> RulesDSD.Syntax.Predicate<'s>.Pred(x, (y |> List.map (fun x -> this.Apply(x, cle))))
|
||||
|
||||
member this.Apply(l:Literal<'s>, cle) = match l with
|
||||
| Neg p -> Neg (this.Apply(p, cle))
|
||||
| Pos p -> Pos (this.Apply(p, cle))
|
||||
|
||||
member this.Apply(c:Clause<'s>, cle:CLE<'s, 'a>) =
|
||||
let head = this.Apply(c.head, cle)
|
||||
let body = c.body |> List.map (fun x -> this.Apply(x, cle))
|
||||
Clause<'s>.Create(head, body)
|
||||
|
||||
member this.Add(that:Substitution<'s, 'a>) =
|
||||
match this, that with | Sub m1, Sub m2 -> Sub (mapUnion m1 m2)
|
||||
|
||||
member this.Keys () = match this with Sub s -> s |> Map.toList |> List.map fst
|
||||
|
||||
static member Update (Sub x:Substitution<'s, 'a>) (y:Substitution<'s, 'a>) (cle:CLE<'s, 'a>) =
|
||||
x |> Map.map (fun _ i -> y.Apply(i, cle))
|
||||
|> Sub
|
||||
|
||||
(* Substitution composition. NB: this operation is NOT commutative; the left operand has precedence over *)
|
||||
static member Compose (Sub x:Substitution<'s, 'a>) (Sub y:Substitution<'s, 'a>) (cle:CLE<'s, 'a>) =
|
||||
x
|
||||
|> Map.map (fun _ v ->
|
||||
match v with
|
||||
| Choice1Of4 t -> Choice1Of4 ((Sub y).Apply(t, cle))
|
||||
| Choice2Of4 l -> Choice2Of4 ((Sub y).Apply(l))
|
||||
| Choice3Of4 s -> Choice3Of4 (cle.applySub y s)
|
||||
| Choice4Of4 s -> Choice4Of4 (cle.applySubVar y s))
|
||||
|> fun x -> (Sub x).Add(Sub y)
|
||||
|
||||
(* Composes two substitutions only if they have disjoint domains *)
|
||||
static member TryMerge (Sub x:Substitution<'s, 'a>) (Sub y:Substitution<'s, 'a>) (cle:CLE<'s, 'a>) : Substitution<'s, 'a> option =
|
||||
y
|
||||
|> Map.fold (fun acc k v ->
|
||||
match acc with
|
||||
| None -> None
|
||||
| Some (Sub x') ->
|
||||
match x'.TryFind(k) with
|
||||
| Some v' -> if v = v'
|
||||
then Some (Sub x')
|
||||
else None
|
||||
| None -> let sub' = (Sub x').Add(k,v, cle)
|
||||
Some sub'
|
||||
) (Some (Sub x))
|
||||
|
||||
(* display *)
|
||||
member this.String (cle:CLE<'s, 'a>) =
|
||||
let mappings = match this with
|
||||
| Sub s -> s |> Map.toList
|
||||
|> List.map (fun (k,v) -> let txt = match v with
|
||||
| Choice1Of4 t -> Term.ToStringWith cle t
|
||||
| Choice2Of4 l -> Location.ToString l
|
||||
| Choice3Of4 sp -> cle.toString sp
|
||||
| Choice4Of4 sp -> cle.toStringTempVar sp
|
||||
sprintf "%s -> %s" (printVar k) txt)
|
||||
String.concat "; " mappings
|
||||
|
||||
(* free variables *)
|
||||
let unionFold f = List.fold (fun x y -> Set.union x (f y)) Set.empty
|
||||
|
||||
let fvLocation l =
|
||||
match l with
|
||||
| Location.Loc _ -> Set.empty
|
||||
| Location.Var (-1, "_") -> Set.empty
|
||||
| Location.Var x -> Set.singleton (LVar x)
|
||||
|
||||
let rec fvPattern (cle:CLE<'s, 'a>) p =
|
||||
let fv (x, y) = cle.fvs x |> Set.union (fvLocation y)
|
||||
match p with
|
||||
| Pattern.Inner a -> unionFold fv a
|
||||
| Pattern.Nicking (a, b) -> Set.union (unionFold fv a) (unionFold fv b)
|
||||
| Pattern.Strand a -> unionFold fv a
|
||||
| Pattern.ThreePrime a -> unionFold fv a
|
||||
| Pattern.FivePrime a -> unionFold fv a
|
||||
| Pattern.Nihil -> Set.empty
|
||||
|
||||
and fvSystem (cle:CLE<'s, 'a>) (Process.Proc s) =
|
||||
s |> Map.toList
|
||||
|> List.map (snd >> unionFold cle.fvs)
|
||||
|> Set.unionMany
|
||||
|
||||
and fvt (cle:CLE<'s, 'a>) t =
|
||||
match t with
|
||||
| Term.Var (-1, "_") -> Set.empty
|
||||
| Term.Var (x,y) -> Set.singleton (TVar (x,y))
|
||||
| Term.Const _ -> Set.empty
|
||||
| Term.Float _ -> Set.empty
|
||||
| Term.Func (_, ts) -> ts |> unionFold (fvt cle)
|
||||
| Term.TList ts -> ts |> unionFold (fvt cle)
|
||||
| Term.TCons (t,t') -> [t;t'] |> unionFold (fvt cle)
|
||||
| Term.Pat p -> p |> fvPattern cle
|
||||
| Term.Proc s -> s |> fvSystem cle
|
||||
| Term.TCRN ts -> ts |> unionFold (fvt cle)
|
||||
| Term.TMSet ts -> ts |> List.map snd |> unionFold (fvt cle)
|
||||
|
||||
let fvp (cle:CLE<'s, 'a>) (Pred (_, ts)) = ts |> unionFold (fvt cle)
|
||||
|
||||
let rec fvl (cle:CLE<'s, 'a>) lit =
|
||||
match lit with
|
||||
| Pos p -> fvp cle p
|
||||
| Neg p -> fvp cle p
|
||||
|
|
@ -0,0 +1,827 @@
|
|||
[<JavaScript>]
|
||||
module RulesDSD.Syntax
|
||||
|
||||
open System
|
||||
open System.Diagnostics
|
||||
|
||||
// Position is an internal index, that pinpoints a domain within a strand graph.
|
||||
// The first int indexes a strand in a strand graph, the second int indexes a domain within that strand.
|
||||
// This is for internal use only.
|
||||
type StrandID = int
|
||||
type SiteIndex = int
|
||||
type BondID = int
|
||||
type Var = int * string
|
||||
type Pos = StrandID * SiteIndex
|
||||
type Range = StrandID * (SiteIndex * SiteIndex)
|
||||
|
||||
let GT = 1
|
||||
let LT = -1
|
||||
let EQ = 0
|
||||
|
||||
let printVar (x,y) = if x >=0 then sprintf "%s(%i)" y x else y
|
||||
|
||||
(* CRN reaction encoding keywords *)
|
||||
type Keywords = Base of unit
|
||||
with
|
||||
static member context = "_ctx"
|
||||
static member reaction = "_rxn"
|
||||
static member mset = "_mset"
|
||||
static member massActionRate = "_massActionRate"
|
||||
static member functionalRate = "_functionalRate"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(* Variables distinguished by type *)
|
||||
[<DebuggerDisplay("{this.String}"); CustomEquality; CustomComparison>]
|
||||
type Variable<'s, 'a> = TVar of Var // terms
|
||||
| LVar of Var // locations
|
||||
| SVar of Var * 's // species
|
||||
| IVar of Var * 'a // sub-species
|
||||
with
|
||||
member this.String =
|
||||
match this with
|
||||
| TVar x -> printVar x
|
||||
| LVar x -> printVar x
|
||||
| SVar (x, _) -> printVar x
|
||||
| IVar (x, _) -> printVar x
|
||||
static member ToVar (this :Variable<'s, 'a>) =
|
||||
match this with | TVar x | SVar (x, _) | LVar x | IVar (x, _) -> x
|
||||
override this.Equals that =
|
||||
match that with
|
||||
| :? Variable<'s, 'a> as that' -> Variable<_,_>.ToVar this = Variable<_,_>.ToVar that'
|
||||
| _ -> invalidArg "yobj" "cannot compare values of different types"
|
||||
override this.GetHashCode() = Variable<_,_>.ToVar this |> hash
|
||||
interface System.IComparable with
|
||||
member this.CompareTo that =
|
||||
match that with
|
||||
| :? Variable<'s, 'a> as that' -> compare (Variable<_,_>.ToVar this) (Variable<_,_>.ToVar that')
|
||||
| _ -> invalidArg "yobj" "cannot compare values of different types"
|
||||
|
||||
(* variable ID provider *)
|
||||
let emptyIdCache () = ref Map.empty
|
||||
|
||||
let cachedIdProvider counter =
|
||||
fun (cache:Map<'s, int> ref) name ->
|
||||
if (!cache).ContainsKey name
|
||||
then ((!cache).[name], name)
|
||||
else
|
||||
let n = !counter
|
||||
counter := n + 1
|
||||
cache := (!cache).Add(name, n)
|
||||
(n, name)
|
||||
|
||||
let newIdProvider () =
|
||||
cachedIdProvider (ref 0)
|
||||
|
||||
let makeProvider () =
|
||||
newIdProvider () (emptyIdCache ())
|
||||
|
||||
let idProvider () : 's -> int * 's =
|
||||
let cache = ref Map.empty
|
||||
newIdProvider () cache
|
||||
|
||||
|
||||
[<DebuggerDisplay("{ToString(this)}")>]
|
||||
type Location = Loc of StrandID * SiteIndex
|
||||
| Var of Var
|
||||
with
|
||||
static member ToString(l:Location) =
|
||||
match l with
|
||||
| Location.Loc (i, j) -> sprintf "(%i, %i)" i j
|
||||
| Location.Var v -> printVar v
|
||||
static member Compare (l1:Location) (l2:Location) =
|
||||
match l1, l2 with
|
||||
| Location.Var (_,X), Location.Var (_,Y) -> System.String.Compare(X,Y)
|
||||
| Location.Var _, Location.Loc _ -> LT
|
||||
| Location.Loc _, Location.Var _ -> GT
|
||||
| Location.Loc (x1, y1), Location.Loc(x2, y2) ->
|
||||
if x1 = x2
|
||||
then compare y1 y2
|
||||
else compare x1 x2
|
||||
static member refresh idProvider loc =
|
||||
match loc with
|
||||
| Location.Loc _ -> loc
|
||||
| Location.Var (-1, "_") -> loc
|
||||
| Location.Var (x, n) -> Location.Var (idProvider n, n)
|
||||
static member wildcard = Location.Var (-1, "_")
|
||||
|
||||
type Hole<'s> = ('s * Location) list
|
||||
and Sub<'s, 'a when 's : equality> = Map<Var, Choice<Term<'s>, Location, 's, 'a>> // this is the inner type of a Substitution; not ideal
|
||||
|
||||
(*********************
|
||||
Custom Logic Engine
|
||||
|
||||
A Custom Logic Engine (CLE) offers a programmatic interface that to domain specific elements into a general logic programming language with graph grammars.
|
||||
For example, Logic DSD is obtained by implementing a CLE for sites (domains + bonds); predicates, contexts and patterns are then obtained "for free".
|
||||
|
||||
The CLE is polymorphic in two parameters 's and 'a. 's stands for the main domain-specific species captured by the language (e.g. a site).
|
||||
'a stands for the sub-species that 's might contain (e.g. a domain or a bond). Roughly, 's and 'a correspond to the kind of logic variables that
|
||||
are domain-specific (e.g. variable X in d!X is different from the same variable in N is X + 1).
|
||||
**************************)
|
||||
and CLE<'s , 'a when 's : equality> =
|
||||
{ toString : 's -> string // print 's
|
||||
toStringTempVar : 'a -> string // print 'a
|
||||
compare : 's -> 's -> int // compare two 's, used for sorting; the actual ordering is unimportant, as long as it is a partial order
|
||||
cast : 'a -> 's // cast a 'a into a 's (e.g. a bond X can be cast into a site _!X); used in substitutions
|
||||
toCanonicalForm : 's -> 's // find the canonical form of 's
|
||||
toCanonicalFormProcess : Process<'s> -> Process<'s> // find the canonical form of a process. Since species 's might reference each other (e.g. as in bonds), it is necessary to have a Process level canonical form function
|
||||
unify : 's * 's -> Sub<'s, 'a> list // species unification. The core algorithm that find a 's and 'a variable substitution such that two species are equivalent after applying it
|
||||
underscore : unit -> 's // wildcard "_" for 's
|
||||
applyAll : Sub<'s, 'a> -> Choice<'s, 'a> -> 's // apply a substitution to a species or subspecies
|
||||
applySub : Sub<'s, 'a> -> 's -> 's // apply a species substitution
|
||||
applySubVar : Sub<'s, 'a> -> 'a -> 'a // apply a substitution to a subspecies
|
||||
fvs : 's -> Set<Variable<'s, 'a>> // free variables in 's
|
||||
refresh : (string -> int) -> 's -> 's // provide a copy of 's where variables have been renamed by an ID provider. Used in resolution
|
||||
disambiguateVars : Clause<'s> -> Clause<'s> // post-parsing step applied to each parsed clause. In Logic DSD this is used to disambiguate the use of domain variables (e.g. in P = C[D][D!i], D can be cast down to an unbound domain rather than a generic site)
|
||||
ComposeProcesses : Process<'s> -> Process<'s> -> Process<'s> // compose two processes together (possibly forming a complex in Logic DSD)
|
||||
resolveGoal : (string * Term<'s> list) // a predicate // species-specific predicates resolution. The core resolution algorithm that executes custom predicates for species (e.g. "compl(D, E)" is a custom predicate in Logic DSD to find the complement E of a domain D)
|
||||
-> Sub<'s, 'a> // the current unification solution theta
|
||||
-> (Sub<'s, 'a> * Sub<'s, 'a>) list option // a list of expanded solutions theta', together with the solution sigma such that theta' = sigma \circ theta
|
||||
domainKeywords : string list
|
||||
}
|
||||
with
|
||||
static member empty : CLE<'s, 'a> =
|
||||
{ toString = fun x -> x.ToString()
|
||||
toStringTempVar = fun x -> x.ToString()
|
||||
cast = fun _ -> failwith "Internal error (CLE)"
|
||||
compare = fun _ _ -> failwith "Internal error (CLE)"
|
||||
toCanonicalForm = id
|
||||
toCanonicalFormProcess = id
|
||||
unify = fun _ -> failwith "Internal error (CLE)"
|
||||
underscore = fun _ -> failwith "Internal error (CLE)"
|
||||
applyAll = fun _ _ -> failwith "Internal error (CLE)"
|
||||
applySub = fun _ _ -> failwith "Internal error (CLE)"
|
||||
applySubVar = fun _ _ -> failwith "Internal error (CLE)"
|
||||
fvs = fun _ -> failwith "Internal error (CLE)"
|
||||
refresh = fun _ -> failwith "Internal error (CLE)"
|
||||
disambiguateVars = fun _ -> failwith "Internal error (CLE)"
|
||||
ComposeProcesses = fun _ _ -> failwith "Internal error (CLE)"
|
||||
resolveGoal = fun _ _ -> failwith "Internal error (CLE)"
|
||||
domainKeywords = []
|
||||
}
|
||||
and
|
||||
[<DebuggerDisplay("{ToString(this)}")>]
|
||||
Pattern<'s when 's : equality> =
|
||||
| Nicking of Hole<'s> * Hole<'s>
|
||||
| Inner of Hole<'s>
|
||||
| Strand of Hole<'s>
|
||||
| ThreePrime of Hole<'s>
|
||||
| FivePrime of Hole<'s>
|
||||
| Nihil
|
||||
|
||||
with
|
||||
static member ToStringWith (cle:CLE<'s, 'a>) (p:Pattern<'s>) =
|
||||
let printHole (x:Hole<'s>) = x
|
||||
|> List.map (fun (s, l) ->
|
||||
match l with
|
||||
| Location.Var (-1,"_") -> cle.toString s
|
||||
| _ -> sprintf "%s @ %s" (cle.toString s) (Location.ToString l))
|
||||
|> String.concat " "
|
||||
match p with
|
||||
| Nihil -> "0"
|
||||
| Inner s -> printHole s |> sprintf "%s"
|
||||
| Nicking (l, r) -> let left = printHole l
|
||||
let right = printHole r
|
||||
sprintf "%s> | <%s" left right
|
||||
| Strand s -> printHole s |> sprintf "<%s>"
|
||||
| ThreePrime s -> printHole s |> sprintf "%s>"
|
||||
| FivePrime s -> printHole s |> sprintf "<%s"
|
||||
|
||||
static member ToString(p:Pattern<'s>) = Pattern.ToStringWith CLE.empty p
|
||||
|
||||
|
||||
static member Map(f : ('s * Location) -> ('t * Location)) (p:Pattern<'s>) =
|
||||
let g s = s |> List.map f
|
||||
match p with
|
||||
| Nihil -> Nihil
|
||||
| Inner s -> Inner (g s)
|
||||
| Nicking (s1, s2) -> Nicking (g s1, g s2)
|
||||
| Strand s -> Strand (g s)
|
||||
| ThreePrime s -> ThreePrime (g s)
|
||||
| FivePrime s -> FivePrime (g s)
|
||||
|
||||
static member Fold (f:'a -> ('s * Location) -> 'a) (acc : 'a) (h:Pattern<'s>) =
|
||||
match h with
|
||||
| ThreePrime hole -> List.fold f acc hole
|
||||
| FivePrime hole -> List.fold f acc hole
|
||||
| Nicking (h1, h2) -> List.fold f (List.fold f acc h1) h2
|
||||
| Strand hole -> List.fold f acc hole
|
||||
| Inner hole -> List.fold f acc hole
|
||||
| Nihil -> acc
|
||||
|
||||
member this.Overlaps(that:Pattern<'s>) =
|
||||
let holes (p:Pattern<'s>) =
|
||||
match p with
|
||||
| ThreePrime hole -> [hole]
|
||||
| FivePrime hole -> [hole]
|
||||
| Nicking (h1, h2) -> [h1; h2]
|
||||
| Strand hole -> [hole]
|
||||
| Inner hole -> [hole]
|
||||
| Nihil -> []
|
||||
let toRange p (h:Hole<'s>) : Range =
|
||||
match snd h.Head with
|
||||
| Location.Loc (sid, idx) -> (sid, (idx, idx+h.Length-1))
|
||||
| Location.Var _ -> failwith <| sprintf "Unexpected uninstantiated pattern %s" (Pattern.ToString p)
|
||||
let overlaps ((sid1, (x1, y1)) : Range) ((sid2, (x2, y2)) : Range) =
|
||||
sid1 = sid2
|
||||
&& (x1 <= y2 && y1 >= x2)
|
||||
// all ranges are disjoint
|
||||
this
|
||||
|> holes
|
||||
|> List.map (toRange this)
|
||||
|> List.exists (fun r1 ->
|
||||
that
|
||||
|> holes
|
||||
|> List.map (toRange that)
|
||||
|> List.exists (overlaps r1))
|
||||
|
||||
static member Canonical (cle:CLE<'s, 'a>) (p:Pattern<'s>) =
|
||||
p |> Pattern.Map (fun (x,y) -> (x |> cle.toCanonicalForm, y))
|
||||
|
||||
static member refresh (cle:CLE<'s, 'a>) (idProvider : string -> int) (p : Pattern<'s>) =
|
||||
let refreshHole (sp, loc) =
|
||||
let loc' = Location.refresh idProvider loc
|
||||
let sp' = cle.refresh idProvider sp
|
||||
(sp', loc')
|
||||
match p with
|
||||
| Pattern.Nihil -> Pattern.Nihil
|
||||
| Pattern.Inner hs -> Pattern.Inner (hs |> List.map refreshHole)
|
||||
| Pattern.ThreePrime hs -> Pattern.ThreePrime (hs |> List.map refreshHole)
|
||||
| Pattern.FivePrime hs -> Pattern.FivePrime (hs |> List.map refreshHole)
|
||||
| Pattern.Strand hs -> Pattern.Strand (hs |> List.map refreshHole)
|
||||
| Pattern.Nicking(hs1, hs2) -> let hs1' = hs1 |> List.map refreshHole
|
||||
let hs2' = hs2 |> List.map refreshHole
|
||||
Pattern.Nicking(hs1', hs2')
|
||||
|
||||
(* System *)
|
||||
and Strand<'s> = 's list
|
||||
and
|
||||
[<DebuggerDisplay("{ToString(this)}")>]
|
||||
Process<'s when 's : equality> = Proc of Map<StrandID, Strand<'s>>
|
||||
with
|
||||
static member ToStringWith (cle:CLE<'s, 'a>) (Proc s:Process<'s>) =
|
||||
s |> Map.toList
|
||||
|> List.map (snd
|
||||
>> List.map (cle.toString)
|
||||
>> String.concat " "
|
||||
>> sprintf "<%s>")
|
||||
|> String.concat " | "
|
||||
static member ToString(p:Process<'s>) = Process.ToStringWith CLE.empty p
|
||||
static member Map(f:'s -> 't) (Proc s:Process<'s>) =
|
||||
Proc (s |> Map.map (fun _ -> List.map f))
|
||||
static member Fold(f:'State -> 's -> 'State) (acc:'State) (Proc s:Process<'s>)=
|
||||
s |> Map.fold (fun st _ x -> x |> List.fold f st) acc
|
||||
static member ToList(Proc p:Process<'s>) = p |> Map.toList
|
||||
|> List.map snd
|
||||
static member OfList(ss:Strand<'s> list) = ss |> List.mapi (fun i x -> i, x)
|
||||
|> Map.ofList
|
||||
|> Process.Proc
|
||||
static member Compare (cle:CLE<'s, 'a>) (p:Process<'s>) (q:Process<'s>) : int =
|
||||
List.compareWith
|
||||
(List.compareWith cle.compare)
|
||||
(p |> Process<'s>.ToList)
|
||||
(q |> Process<'s>.ToList)
|
||||
|
||||
|
||||
static member Canonical (cle:CLE<'s, 'a>) (p:Process<'s>) : Process<'s> =
|
||||
cle.toCanonicalFormProcess p
|
||||
|
||||
static member refresh (cle : CLE<'s, 'a>) (idProvider : string ->int) (p : Process<'s>) =
|
||||
p |> Process.Map (cle.refresh idProvider)
|
||||
|
||||
(*****************************************************************)
|
||||
(** End of processes canonical form ******************************)
|
||||
(*****************************************************************)
|
||||
|
||||
(* terms *)
|
||||
and Mset<'s when 's : equality> = (int * Term<'s>) list
|
||||
and
|
||||
[<DebuggerDisplay("{ToString(this)}")>]
|
||||
Term<'s when 's : equality> =
|
||||
(* standard logic programming terms *)
|
||||
| Var of int * string // variable ID (int), debug string (the string field can be erased in principle)
|
||||
| Const of string // "some string"
|
||||
| Float of float
|
||||
| Func of string * Term<'s> list // f(t1, ..., tn)
|
||||
| TList of Term<'s> list // [t1; t2; ...; tN]
|
||||
| TCons of Term<'s> * Term<'s> // [t1; ...; tK # Rest] // TODO: change? E.g. to a "partial list" type TListp of (Term list * Var), where Var is the rest of the list
|
||||
| TCRN of Term<'s> list // a CRN with a set { R1, ... Rk } of k reactions. Each reaction is encoded as Prolog terms as Term.Func("_rxn", [ Term.TMSet; Term.Func("_massActionRate", [Term expression]); Term.TMSet])
|
||||
| TMSet of Mset<'s> // a multiset {| n1 t1, ... nk tk |}, where ni is the multiplicity of term ti. An example of a TMSet is 2a + 3b, which is written as {| 2 a, 3 b|} in multiset notation
|
||||
// The multiplicity ni must be a concrete integer number (e.g. 2 in "2 a + 3 b"), it cannot be a generic logic variable X currently
|
||||
(* TODO: possible future extensions:
|
||||
- add undefined CRNs, e.g. {t1, ..., tk # X}, where X is some undefined set; X must be computed through unification
|
||||
- add undefined multisets, e.g. {| n1 t1, ..., nk tk # X |}, where X is the same as above
|
||||
- add undefined multiplicities, e.g. n1 can be either an integer or a variable X *)
|
||||
(* DSD specific terms *)
|
||||
| Proc of Process<'s>
|
||||
| Pat of Pattern<'s>
|
||||
with
|
||||
static member Wildcard : Term<'s>= Term.Var (-1, "_")
|
||||
static member FlattenList t =
|
||||
let rec flatten t =
|
||||
match t with
|
||||
| TCons (x, ts) ->
|
||||
match flatten ts with
|
||||
| Choice1Of2 groundList -> Choice1Of2 (x :: groundList)
|
||||
| Choice2Of2 (leadingItems, listVar) -> Choice2Of2 (x::leadingItems, listVar)
|
||||
| TList x -> Choice1Of2 x
|
||||
| Var(x,y) -> Choice2Of2 ([], Var(x,y)) // unexpanded list that ends in a variable
|
||||
| _ -> failwith <| sprintf "Ill-formed list: %s" (Term<'s>.ToString t)
|
||||
flatten t
|
||||
static member ToStringWith (cle:CLE<'s, 'a>) (x:Term<'s>) =
|
||||
let printer = Term.ToStringWith cle
|
||||
match x with
|
||||
| Var(x,y) -> printVar (x,y)
|
||||
| Const c -> sprintf "\"%s\"" c
|
||||
| Float f -> sprintf "%f" f
|
||||
| Func (f, ts) -> let printRate r = match r with
|
||||
| Term.Func("_functionalRate", [e])
|
||||
| Term.Func("_massActionRate", [e]) ->
|
||||
if e = Term.Float 1.0
|
||||
then ""
|
||||
else match r with
|
||||
| Term.Func("_massActionRate", _) -> sprintf "{%s}" (e |> Term<'s>.ToExpression |> Microsoft.Research.CRNEngine.Expression.to_string (Term.ToStringWith cle))
|
||||
| Term.Func("_functionalRate", _) -> sprintf "[%s]" (e |> Term<'s>.ToFuncExpression |> Microsoft.Research.CRNEngine.Expression.to_string (Microsoft.Research.CRNEngine.Key.to_string (Term.ToStringWith cle)))
|
||||
| _ -> failwith ""
|
||||
| _ -> failwithf "Ill-formed rate %s" (Term.ToStringWith cle r)
|
||||
match f with
|
||||
| "_ctx" -> match ts with
|
||||
| [_; Var (x,y)] -> sprintf "ctx(%s)" (printVar (x,y))
|
||||
| [_; TList hs] -> sprintf "ctx(%s)" (hs |> List.map printer |> String.concat "")
|
||||
| _ -> sprintf "Ill-formed context %s in" (printer x)
|
||||
| "_rxn" -> match ts with
|
||||
| [cata; mset1; r; bwr; mset2] ->
|
||||
let reactants = printer mset1
|
||||
let products = printer mset2
|
||||
let x = r
|
||||
let rate = printRate r
|
||||
|
||||
let hasCata = cata <> Term.TMSet([])
|
||||
let catalysts = if hasCata then printer cata else ""
|
||||
|
||||
let hasBwRate = bwr <> Term.Func("",[])
|
||||
let bwRate = if hasBwRate then printRate bwr else ""
|
||||
|
||||
match hasCata, hasBwRate with
|
||||
| false, false -> sprintf "%s ->%s %s" reactants rate products
|
||||
| true, false -> sprintf "%s ~ %s ->%s %s" catalysts reactants rate products
|
||||
| true, true -> sprintf "%s ~ %s <->%s%s %s" catalysts reactants rate bwRate products
|
||||
| false, true -> sprintf "%s <->%s%s %s" reactants rate bwRate products
|
||||
|
||||
| _ -> sprintf "Ill-formed reaction %s in" (printer x)
|
||||
| _ -> sprintf "%s(%s)" f (ts |> List.map printer |> String.concat ", ")
|
||||
| TList ts -> ts |> List.map printer |> String.concat "; " |> sprintf "[%s]"
|
||||
| TCons _ -> match Term<'s>.FlattenList x with
|
||||
| Choice1Of2 groundList -> TList groundList |> printer
|
||||
| Choice2Of2 (leadingItems, terminator) ->
|
||||
let leads = leadingItems
|
||||
|> List.map printer
|
||||
|> String.concat "; "
|
||||
let trailer = terminator |> printer
|
||||
sprintf "[%s # %s]" leads trailer
|
||||
| TCRN ts -> ts |> List.map printer |> String.concat " | " |> sprintf "{ %s }"
|
||||
| TMSet ts -> ts
|
||||
|> List.map (fun (i, t) -> (if i = 1 then printer t else sprintf "%i %s" i (printer t))) |> String.concat ":" // |> sprintf "_complex(%s)"
|
||||
|
||||
| Pat p -> Pattern.ToStringWith cle p
|
||||
| Proc s -> Process.ToStringWith cle s
|
||||
|
||||
static member ToString(x:Term<'s>) = Term<'s>.ToStringWith CLE.empty x
|
||||
|
||||
static member FromExpression(e:Microsoft.Research.CRNEngine.Expression.t<Term<'s>>) : Term<'s> =
|
||||
match e with
|
||||
| Microsoft.Research.CRNEngine.Expression.Float n -> Term.Float n
|
||||
| Microsoft.Research.CRNEngine.Expression.Key k -> Term.Func("_key", [k])
|
||||
| Microsoft.Research.CRNEngine.Expression.Times xs -> Term.Func("_Times", xs |> List.map Term.FromExpression)
|
||||
| Microsoft.Research.CRNEngine.Expression.Plus xs -> Term.Func("_Plus", xs |> List.map Term.FromExpression)
|
||||
| Microsoft.Research.CRNEngine.Expression.Divide xs -> Term.Func("_Divide", [Term.FromExpression xs.div1; Term.FromExpression xs.div2])
|
||||
| Microsoft.Research.CRNEngine.Expression.Power xs -> Term.Func("_Power", [Term.FromExpression xs.base_; Term.FromExpression xs.exponent])
|
||||
| Microsoft.Research.CRNEngine.Expression.Minus xs -> Term.Func("_Minus", [Term.FromExpression xs.sub1; Term.FromExpression xs.sub2])
|
||||
| Microsoft.Research.CRNEngine.Expression.Absolute x -> Term.Func("_Absolute", [Term.FromExpression x])
|
||||
| Microsoft.Research.CRNEngine.Expression.Log x -> Term.Func("_Log", [Term.FromExpression x])
|
||||
| Microsoft.Research.CRNEngine.Expression.Modulo x -> Term.Func("_Modulo", [Term.FromExpression x.div; Term.FromExpression x.modulo])
|
||||
| Microsoft.Research.CRNEngine.Expression.Ceiling x -> Term.Func("_Ceiling", [Term.FromExpression x])
|
||||
| Microsoft.Research.CRNEngine.Expression.Floor x -> Term.Func("_Floor", [Term.FromExpression x])
|
||||
| Microsoft.Research.CRNEngine.Expression.Round x -> Term.Func("_Round", [Term.FromExpression x])
|
||||
| Microsoft.Research.CRNEngine.Expression.If(x, y, z) -> failwith "Conditional expression are not supported yet."
|
||||
|
||||
static member FromFuncExpression(e:Microsoft.Research.CRNEngine.Expression.t<Microsoft.Research.CRNEngine.Key<Term<'s>>>) : Term<'s> =
|
||||
match e with
|
||||
| Microsoft.Research.CRNEngine.Expression.Float n -> Term.Float n
|
||||
| Microsoft.Research.CRNEngine.Expression.Key k -> match k with
|
||||
| Microsoft.Research.CRNEngine.Key.Species s -> Term.Func("_key_species", [s])
|
||||
| Microsoft.Research.CRNEngine.Key.Parameter p -> Term.Func("_key_param", [Term.Const p])
|
||||
| Microsoft.Research.CRNEngine.Key.Rate r -> Term.Func("_key_rate", [Term.Const r])
|
||||
| Microsoft.Research.CRNEngine.Key.Time -> Term.Const "_time"
|
||||
| Microsoft.Research.CRNEngine.Expression.Times xs -> Term.Func("_Times", xs |> List.map Term.FromFuncExpression)
|
||||
| Microsoft.Research.CRNEngine.Expression.Plus xs -> Term.Func("_Plus", xs |> List.map Term.FromFuncExpression)
|
||||
| Microsoft.Research.CRNEngine.Expression.Divide xs -> Term.Func("_Divide", [Term.FromFuncExpression xs.div1; Term.FromFuncExpression xs.div2])
|
||||
| Microsoft.Research.CRNEngine.Expression.Power xs -> Term.Func("_Power", [Term.FromFuncExpression xs.base_; Term.FromFuncExpression xs.exponent])
|
||||
| Microsoft.Research.CRNEngine.Expression.Minus xs -> Term.Func("_Minus", [Term.FromFuncExpression xs.sub1; Term.FromFuncExpression xs.sub2])
|
||||
| Microsoft.Research.CRNEngine.Expression.Absolute x -> Term.Func("_Absolute", [Term.FromFuncExpression x])
|
||||
| Microsoft.Research.CRNEngine.Expression.Log x -> Term.Func("_Log", [Term.FromFuncExpression x])
|
||||
| Microsoft.Research.CRNEngine.Expression.Modulo x -> Term.Func("_Modulo", [Term.FromFuncExpression x.div; Term.FromFuncExpression x.modulo])
|
||||
| Microsoft.Research.CRNEngine.Expression.Ceiling x -> Term.Func("_Ceiling", [Term.FromFuncExpression x])
|
||||
| Microsoft.Research.CRNEngine.Expression.Floor x -> Term.Func("_Floor", [Term.FromFuncExpression x])
|
||||
| Microsoft.Research.CRNEngine.Expression.Round x -> Term.Func("_Round", [Term.FromFuncExpression x])
|
||||
| Microsoft.Research.CRNEngine.Expression.If(x, y, z) -> failwith "Conditional expression are not supported yet."
|
||||
|
||||
|
||||
static member IsExpression (e:Term<'s>) : bool =
|
||||
match e with
|
||||
| Term.Float _ -> true
|
||||
| Term.Func("_key", [_]) -> true
|
||||
| Term.Func("_key_species", [_]) -> true
|
||||
| Term.Func("_key_param", [_]) -> true
|
||||
| Term.Func("_key_rate", [_]) -> true
|
||||
| Term.Func("_Times", ts) -> (ts |> List.forall Term.IsExpression)
|
||||
| Term.Func("_Plus", ts) -> (ts |> List.forall Term.IsExpression)
|
||||
| Term.Func("_Divide", [div1; div2]) -> Term.IsExpression div1 && Term.IsExpression div2
|
||||
| Term.Func("_Power", [bas; exponent]) -> Term.IsExpression bas && Term.IsExpression exponent
|
||||
| Term.Func("_Minus", [sub1; sub2]) -> Term.IsExpression sub1 && Term.IsExpression sub2
|
||||
| Term.Func("_Absolute", [x]) -> Term.IsExpression x
|
||||
| Term.Func("_Log", [x]) -> Term.IsExpression x
|
||||
| Term.Func("_Modulo", [div; modulo]) -> Term.IsExpression div && Term.IsExpression modulo
|
||||
| Term.Func("_Ceiling", [x]) -> Term.IsExpression x
|
||||
| Term.Func("_Floor", [x]) -> Term.IsExpression x
|
||||
| Term.Func("_Round", [x]) -> Term.IsExpression x
|
||||
| _ -> false
|
||||
|
||||
static member ToExpression (e:Term<'s>) : Microsoft.Research.CRNEngine.Expression.t<Term<'s>> =
|
||||
match e with
|
||||
| Term.Float n -> Microsoft.Research.CRNEngine.Expression.Float n
|
||||
| Term.Func("_key", [Term.Float n]) -> Microsoft.Research.CRNEngine.Expression.Float n
|
||||
| Term.Func("_key", [k]) -> Microsoft.Research.CRNEngine.Expression.Key k
|
||||
| Term.Func("_Times", ts) -> Microsoft.Research.CRNEngine.Expression.Times (ts |> List.map Term.ToExpression)
|
||||
| Term.Func("_Plus", ts) -> Microsoft.Research.CRNEngine.Expression.Plus (ts |> List.map Term.ToExpression)
|
||||
| Term.Func("_Divide", [div1; div2]) -> Microsoft.Research.CRNEngine.Expression.Divide {Microsoft.Research.CRNEngine.Expression.div1 = Term.ToExpression div1; Microsoft.Research.CRNEngine.Expression.div2 = Term.ToExpression div2}
|
||||
| Term.Func("_Power", [bas; exponent]) -> Microsoft.Research.CRNEngine.Expression.Power {Microsoft.Research.CRNEngine.Expression.base_ = Term.ToExpression bas; Microsoft.Research.CRNEngine.Expression.exponent = Term.ToExpression exponent}
|
||||
| Term.Func("_Minus", [sub1; sub2]) -> Microsoft.Research.CRNEngine.Expression.Minus {Microsoft.Research.CRNEngine.Expression.sub1 = Term.ToExpression sub1; Microsoft.Research.CRNEngine.Expression.sub2 = Term.ToExpression sub2}
|
||||
| Term.Func("_Absolute", [x]) -> Microsoft.Research.CRNEngine.Expression.Absolute (Term.ToExpression x)
|
||||
| Term.Func("_Log", [x]) -> Microsoft.Research.CRNEngine.Expression.Log (Term.ToExpression x)
|
||||
| Term.Func("_Modulo", [div; modulo]) -> Microsoft.Research.CRNEngine.Expression.Modulo {Microsoft.Research.CRNEngine.Expression.div = Term.ToExpression div; Microsoft.Research.CRNEngine.Expression.modulo = Term.ToExpression modulo }
|
||||
| Term.Func("_Ceiling", [x]) -> Microsoft.Research.CRNEngine.Expression.Ceiling (Term.ToExpression x)
|
||||
| Term.Func("_Floor", [x]) -> Microsoft.Research.CRNEngine.Expression.Floor (Term.ToExpression x)
|
||||
| Term.Func("_Round", [x]) -> Microsoft.Research.CRNEngine.Expression.Round (Term.ToExpression x)
|
||||
| _ -> failwithf "Conversion of term %s to expression not supported." (Term.ToString e)
|
||||
|
||||
static member ToFuncExpression (e:Term<'s>) : Microsoft.Research.CRNEngine.Expression.t<Microsoft.Research.CRNEngine.Key<Term<'s>>> =
|
||||
match e with
|
||||
| Term.Const "_time" -> Microsoft.Research.CRNEngine.Expression.Key Microsoft.Research.CRNEngine.Key.Time
|
||||
| Term.Const s -> Microsoft.Research.CRNEngine.Expression.Key (Microsoft.Research.CRNEngine.Key.Parameter s)
|
||||
| Term.Float n -> Microsoft.Research.CRNEngine.Expression.Float n
|
||||
| Term.Func("_key", [Term.Float n]) -> Microsoft.Research.CRNEngine.Expression.Float n
|
||||
| Term.Func("_key", [k]) -> Microsoft.Research.CRNEngine.Expression.Key (Microsoft.Research.CRNEngine.Key.Species k)
|
||||
| Term.Func("_key_species",[s]) -> Microsoft.Research.CRNEngine.Expression.Key (Microsoft.Research.CRNEngine.Key.Species s)
|
||||
| Term.Func("_key_param", [Term.Const p]) -> Microsoft.Research.CRNEngine.Expression.Key (Microsoft.Research.CRNEngine.Key.Parameter p)
|
||||
| Term.Func("_key_rate", [Term.Const r]) -> Microsoft.Research.CRNEngine.Expression.Key (Microsoft.Research.CRNEngine.Key.Rate r)
|
||||
| Term.Func("_Times", ts) -> Microsoft.Research.CRNEngine.Expression.Times (ts |> List.map Term.ToFuncExpression)
|
||||
| Term.Func("_Plus", ts) -> Microsoft.Research.CRNEngine.Expression.Plus (ts |> List.map Term.ToFuncExpression)
|
||||
| Term.Func("_Divide", [div1; div2]) -> Microsoft.Research.CRNEngine.Expression.Divide {Microsoft.Research.CRNEngine.Expression.div1 = Term.ToFuncExpression div1; Microsoft.Research.CRNEngine.Expression.div2 = Term.ToFuncExpression div2}
|
||||
| Term.Func("_Power", [bas; exponent]) -> Microsoft.Research.CRNEngine.Expression.Power {Microsoft.Research.CRNEngine.Expression.base_ = Term.ToFuncExpression bas; Microsoft.Research.CRNEngine.Expression.exponent = Term.ToFuncExpression exponent}
|
||||
| Term.Func("_Minus", [sub1; sub2]) -> Microsoft.Research.CRNEngine.Expression.Minus {Microsoft.Research.CRNEngine.Expression.sub1 = Term.ToFuncExpression sub1; Microsoft.Research.CRNEngine.Expression.sub2 = Term.ToFuncExpression sub2}
|
||||
| Term.Func("_Absolute", [x]) -> Microsoft.Research.CRNEngine.Expression.Absolute (Term.ToFuncExpression x)
|
||||
| Term.Func("_Log", [x]) -> Microsoft.Research.CRNEngine.Expression.Log (Term.ToFuncExpression x)
|
||||
| Term.Func("_Modulo", [div; modulo]) -> Microsoft.Research.CRNEngine.Expression.Modulo {Microsoft.Research.CRNEngine.Expression.div = Term.ToFuncExpression div; Microsoft.Research.CRNEngine.Expression.modulo = Term.ToFuncExpression modulo }
|
||||
| Term.Func("_Ceiling", [x]) -> Microsoft.Research.CRNEngine.Expression.Ceiling (Term.ToFuncExpression x)
|
||||
| Term.Func("_Floor", [x]) -> Microsoft.Research.CRNEngine.Expression.Floor (Term.ToFuncExpression x)
|
||||
| Term.Func("_Round", [x]) -> Microsoft.Research.CRNEngine.Expression.Round (Term.ToFuncExpression x)
|
||||
| _ -> failwithf "Conversion of term %s to expression not supported." (Term.ToString e)
|
||||
|
||||
// decode a term into a CRN rate
|
||||
static member ToRate (t:Term<'s>) : Microsoft.Research.CRNEngine.Rate<Microsoft.Research.CRNEngine.Value, Microsoft.Research.CRNEngine.Expression.t<Microsoft.Research.CRNEngine.Key<Term<'s>>>> option =
|
||||
let toMassActionRate (x:Term<'s>) =
|
||||
let exp = x |> Term.ToExpression
|
||||
let isConvertible = Microsoft.Research.CRNEngine.Expression.mentions exp
|
||||
|> List.forall (fun x -> match x with
|
||||
| Term.Const _ -> true
|
||||
| _ -> false)
|
||||
if not isConvertible
|
||||
then None // TODO: throw an exception?
|
||||
else
|
||||
exp |> Microsoft.Research.CRNEngine.Expression.map (fun x -> match x with
|
||||
| Term.Const s -> s
|
||||
| _ -> failwith "")
|
||||
|> Microsoft.Research.CRNEngine.MassAction
|
||||
|> Some
|
||||
|
||||
let toFunctionalRate (x:Term<'s>) =
|
||||
let exp = x |> Term.ToFuncExpression
|
||||
let isConvertible = Microsoft.Research.CRNEngine.Expression.mentions exp
|
||||
|> List.forall (fun x -> match x with
|
||||
| Microsoft.Research.CRNEngine.Key.Species (Term.Const _)
|
||||
| Microsoft.Research.CRNEngine.Key.Species (Term.Pat (Pattern.Inner [_, _]))
|
||||
| Microsoft.Research.CRNEngine.Key.Parameter _
|
||||
| Microsoft.Research.CRNEngine.Key.Rate _
|
||||
| Microsoft.Research.CRNEngine.Key.Time -> true
|
||||
| _ -> false)
|
||||
if not isConvertible
|
||||
then None
|
||||
else
|
||||
exp (*|> Expression.map (fun x -> match x with
|
||||
| Key.Parameter s -> Key.Parameter s
|
||||
| Key.Rate r -> Key.Rate r
|
||||
| Key.Time -> Key.Time
|
||||
| Key.Species (Term.Const)
|
||||
| Term.Const s -> Key.Parameter s
|
||||
| _ -> Key.Species x)*)
|
||||
//| Term.Proc p -> Key.Species p
|
||||
//| Term.Pat (Pattern.Inner [sp, _]) -> Key.Species (Process.OfList [[sp]])
|
||||
//| _ -> failwith "")
|
||||
|> Microsoft.Research.CRNEngine.Function
|
||||
|> Some
|
||||
match t with
|
||||
| Term.Func (fwRateKind, [fr]) ->
|
||||
if not (Term.IsExpression fr)
|
||||
then None
|
||||
else match fwRateKind with
|
||||
| "_massActionRate" -> toMassActionRate fr
|
||||
| "_functionalRate" -> toFunctionalRate fr
|
||||
| _ -> None
|
||||
| _ -> None
|
||||
|
||||
// decode a term into a CRN reaction
|
||||
static member ToReactions (t:Term<'s>) : Microsoft.Research.CRNEngine.Reaction<Term<'s>, Microsoft.Research.CRNEngine.Value, Microsoft.Research.CRNEngine.Expression.t<Microsoft.Research.CRNEngine.Key<Term<'s>>>> list =
|
||||
let toReaction (t:Term<'s>) : Microsoft.Research.CRNEngine.Reaction<Term<'s>, Microsoft.Research.CRNEngine.Value, Microsoft.Research.CRNEngine.Expression.t<Microsoft.Research.CRNEngine.Key<Term<'s>>>> option =
|
||||
match t with
|
||||
| Term.Func ("_rxn", [ Term.TMSet catalysts
|
||||
; Term.TMSet reactants
|
||||
; fwr
|
||||
; bwr
|
||||
; Term.TMSet products]) ->
|
||||
let fwRateOpt = Term.ToRate fwr
|
||||
|
||||
match fwRateOpt with
|
||||
| None -> None
|
||||
| Some fwRate ->
|
||||
let bwRate = Term.ToRate bwr
|
||||
let toCrnMset (x:(int * Term<'s>) list) : Microsoft.Research.CRNEngine.Mset.t<Term<'s>> =
|
||||
x |> List.fold (fun acc (i, t) -> { Microsoft.Research.CRNEngine.Mset.element = t;
|
||||
Microsoft.Research.CRNEngine.Mset.multiplicity = i } :: acc) []
|
||||
(*match accOpt with
|
||||
| None -> None
|
||||
| Some acc -> match t with
|
||||
| Term.Proc p -> Some ({ element = p; multiplicity = i } :: acc)
|
||||
| Term.Pat (Pattern.Inner [sp, _]) -> Some ({ element = Process.OfList [[sp]]; multiplicity = i } :: acc)
|
||||
// | Term.TMSet ts ->
|
||||
| _ -> None) (Some [])*)
|
||||
let cata = toCrnMset catalysts
|
||||
let reac = toCrnMset reactants
|
||||
let prod = toCrnMset products
|
||||
// TODO: the compiler cannot link to Microsoft.Research.CRNEngine.Reaction.create for unknown reasons; substitute mkR with Reaction.create
|
||||
let mkR c r br fr p = { Microsoft.Research.CRNEngine.catalysts = c;
|
||||
Microsoft.Research.CRNEngine.reactants = r;
|
||||
Microsoft.Research.CRNEngine.reverse = br;
|
||||
Microsoft.Research.CRNEngine.rate = fr;
|
||||
Microsoft.Research.CRNEngine.products = p}
|
||||
if cata.IsEmpty
|
||||
then Some <| mkR Microsoft.Research.CRNEngine.Mset.empty reac bwRate fwRate prod
|
||||
else Some <| mkR cata reac bwRate fwRate prod
|
||||
| _ -> None
|
||||
|
||||
match t with
|
||||
| Term.TCRN ts
|
||||
| Term.TList ts -> ts |> List.choose toReaction
|
||||
| _ -> match toReaction t with
|
||||
| Some r -> [r]
|
||||
| None -> []
|
||||
|
||||
/// NB: Compare is only meant to be used in the normal form algorithm
|
||||
static member Compare (cle:CLE<'s, 'a>) (t1:Term<'s>) (t2:Term<'s>) =
|
||||
let termNumber t =
|
||||
match t with
|
||||
| Term.Func _ -> 0
|
||||
| Term.Const _ -> 1
|
||||
| Term.Float _ -> 2
|
||||
| Term.Pat _ -> 3
|
||||
| Term.Proc _ -> 4
|
||||
| Term.TCons _ -> 5
|
||||
| Term.TList _ -> 6
|
||||
| Term.Var _ -> 7
|
||||
| Term.TCRN _ -> 8
|
||||
| Term.TMSet _ -> 9
|
||||
let n1, n2 = termNumber t1, termNumber t2
|
||||
if n1 < n2 then LT
|
||||
elif n1 > n2 then GT
|
||||
else (* same type*)
|
||||
match t1 , t2 with
|
||||
| Term.Func(name1, args1), Term.Func(name2,args2) ->
|
||||
let nameComparison = String.Compare(name1, name2)
|
||||
if nameComparison < 0 then LT
|
||||
elif nameComparison > 0 then GT
|
||||
else List.zip args1 args2
|
||||
|> List.fold (fun acc (a1, a2) -> if acc = GT || acc = LT
|
||||
then acc
|
||||
else Term.Compare cle a1 a2) EQ
|
||||
| Term.Const name1, Term.Const name2 -> String.Compare(name1, name2)
|
||||
| Term.Float f1, Term.Float f2 -> if f1 < f2 then LT
|
||||
elif f1 > f2 then GT
|
||||
else EQ
|
||||
| Term.Var (_,v1), Term.Var (_,v2) -> String.Compare(v1, v2)
|
||||
| Term.Pat p1, Term.Pat p2 ->
|
||||
match p1, p2 with
|
||||
| Pattern.Inner s1, Pattern.Inner s2 ->
|
||||
s2 |> List.compareWith (fun (x1, y1) (x2, y2) ->
|
||||
let cmp = cle.compare x1 x2
|
||||
if cmp = EQ
|
||||
then Location.Compare y1 y2
|
||||
else cmp) s1
|
||||
| _, _ -> failwith "Tagging a domain with a pattern is not supported yet."
|
||||
| Term.TList ts1, Term.TList ts2 -> if ts1.IsEmpty && ts2.IsEmpty then EQ
|
||||
elif ts1.IsEmpty then GT
|
||||
else let t1 = ts1.Head
|
||||
let t2 = ts2.Head
|
||||
let comp = Term<'s>.Compare cle t1 t2
|
||||
if comp = EQ
|
||||
then Term.Compare cle (Term.TList ts1.Tail) (Term.TList ts2.Tail)
|
||||
else comp
|
||||
| Term.TCons(t1, ts1), Term.TList ts2 -> if ts2.IsEmpty then LT
|
||||
else let t2 = ts2.Head
|
||||
let comp = Term.Compare cle t1 t2
|
||||
if comp = EQ
|
||||
then Term.Compare cle ts1 (Term.TList ts2.Tail)
|
||||
else comp
|
||||
| Term.TList ts1, Term.TCons (t2, ts2) -> if ts1.IsEmpty then LT
|
||||
else let t1 = ts1.Head
|
||||
let comp = Term.Compare cle t1 t2
|
||||
if comp = EQ
|
||||
then Term.Compare cle (Term.TList ts1.Tail) ts2
|
||||
else comp
|
||||
| Term.TCons(t1, ts1), Term.TCons (t2, ts2) -> let comp = Term.Compare cle t1 t2
|
||||
if comp = EQ
|
||||
then Term.Compare cle ts1 ts2
|
||||
else comp
|
||||
| Term.TMSet ts1, Term.TMSet ts2 -> match ts1, ts2 with // Assumption: ts1 and ts2 are in canonical form, therefore sorted
|
||||
| [], [] -> EQ
|
||||
| [], _ -> LT
|
||||
| _, [] -> GT
|
||||
| (n1, t1)::tail1, (n2, t2)::tail2 ->
|
||||
if n1 = n2
|
||||
then let x = Term.Compare cle t1 t2
|
||||
if x <> EQ then x else Term.Compare cle (Term.TMSet tail1) (Term.TMSet tail2)
|
||||
else compare n1 n2
|
||||
| Term.TCRN ts1, Term.TCRN ts2 -> Term.Compare cle (Term.TList ts1) (Term.TList ts2) // Assumption: ts1 and ts2 are in canonical form, therefore sorted
|
||||
| Term.Proc p1, Term.Proc p2 -> Process.Compare cle p1 p2
|
||||
| _, _ -> failwith ""
|
||||
|
||||
static member Canonical cle (t:Term<'s>) =
|
||||
match t with
|
||||
| Term.Func(x, ts) -> Term<'s>.Func(x, ts |> List.map (Term<'s>.Canonical cle))
|
||||
| Term.Const _ -> t
|
||||
| Term.Float _ -> t
|
||||
| Term.Pat p -> p |> fun z -> Pattern<'s>.Canonical cle z |> Term<'s>.Pat
|
||||
| Term.Proc p -> p |> Process<'s>.Canonical cle |> Term<'s>.Proc
|
||||
| Term.TCons (t1, t2) -> (Term.Canonical cle t1, Term.Canonical cle t2) |> Term.TCons
|
||||
| Term.TList ts -> ts |> List.map (Term.Canonical cle) |> Term.TList
|
||||
| Term.Var _ -> t
|
||||
| Term.TMSet ts -> ts
|
||||
|> List.map (fun (n, t) -> n, Term.Canonical cle t)
|
||||
|> List.sortWith (fun (n1, t1) (n2, t2) -> let x = compare n1 n2
|
||||
if x <> EQ
|
||||
then x
|
||||
else Term.Compare cle t1 t2)
|
||||
|> Term.TMSet
|
||||
| Term.TCRN ts -> ts
|
||||
|> List.map (Term.Canonical cle)
|
||||
|> List.sortWith (Term.Compare cle)
|
||||
|> List.distinct
|
||||
|> Term.TCRN
|
||||
|
||||
static member refresh (cle:CLE<'s, 'a>) (idProvider : string -> int) (t:Term<'s>) =
|
||||
match t with
|
||||
| Term.Var (-1, "_") -> t
|
||||
| Term.Var (x, y) -> Term.Var (idProvider y, y)
|
||||
| Term.Func(x, ts) -> Term<'s>.Func(x, ts |> List.map (Term.refresh cle idProvider))
|
||||
| Term.Const _ -> t
|
||||
| Term.Float _ -> t
|
||||
| Term.Pat p -> Term.Pat (p |> Pattern.refresh cle idProvider)
|
||||
| Term.Proc p -> Term.Proc (p |> Process.refresh cle idProvider)
|
||||
| Term.TCons (t1, t2) -> let t1' = Term.refresh cle idProvider t1
|
||||
let t2' = Term.refresh cle idProvider t2
|
||||
Term.TCons (t1', t2')
|
||||
| Term.TList ts -> Term<'s>.TList (ts |> List.map (Term.refresh cle idProvider))
|
||||
| Term.TCRN ts -> Term<'s>.TCRN (ts |> List.map (Term.refresh cle idProvider))
|
||||
| Term.TMSet ts -> Term<'s>.TMSet (ts |> List.map (fun (i, t) -> i, t |> Term.refresh cle idProvider))
|
||||
|
||||
static member Map (f:'s -> 't) (t:Term<'s>) : Term<'t> =
|
||||
match t with
|
||||
| Term.Var (-1, "_") -> Term.Var (-1, "_")
|
||||
| Term.Var (x, y) -> Term.Var (x, y)
|
||||
| Term.Func(x, ts) -> Term<'t>.Func(x, ts |> List.map (Term.Map f) )
|
||||
| Term.Const x -> Term.Const x
|
||||
| Term.Float x -> Term.Float x
|
||||
| Term.Pat p -> Term.Pat (p |> Pattern.Map (fun (x,y) -> f x, y))
|
||||
| Term.Proc p -> Term.Proc (p |> Process.Map f)
|
||||
| Term.TCons (t1, t2) -> let t1' = Term.Map f t1
|
||||
let t2' = Term.Map f t2
|
||||
Term.TCons (t1', t2')
|
||||
| Term.TList ts -> Term<'t>.TList (ts |> List.map (Term.Map f))
|
||||
| Term.TCRN ts -> Term<'t>.TCRN (ts |> List.map (Term.Map f))
|
||||
| Term.TMSet ts -> Term<'t>.TMSet (ts |> List.map (fun (i, t) -> i, t |> Term.Map f))
|
||||
|
||||
static member wildcard : Term<'s> = Term.Var (-1, "_")
|
||||
|
||||
static member Species (t:Term<'s>) : 's list =
|
||||
let rec f x =
|
||||
match x with
|
||||
| Term.Var _
|
||||
| Term.Const _
|
||||
| Term.Float _ -> []
|
||||
| Term.TCRN ts
|
||||
| Term.Func (_, ts)
|
||||
| Term.TList ts -> ts |> List.collect f
|
||||
| Term.TCons (t1, t2) -> f t1 @ f t2
|
||||
| Term.TMSet s -> s |> List.collect (snd >> f)
|
||||
| Term.Proc p -> p |> Process.ToList |> List.concat
|
||||
| Term.Pat p -> p |> Pattern.Fold (fun acc (x, _) -> x::acc) []
|
||||
f t |> List.distinct
|
||||
(* predicates *)
|
||||
and
|
||||
[<DebuggerDisplay("{this.String}")>]
|
||||
Predicate<'s when 's : equality> = Pred of string * Term<'s> list
|
||||
with
|
||||
static member ToStringWith cle (Pred (p, ts)) = sprintf "%s(%s)" p (ts |> List.map (Term<'s>.ToStringWith cle)
|
||||
|> String.concat ", ")
|
||||
static member ToString (Pred (p, ts)) = Predicate.ToStringWith CLE.empty (Pred (p, ts))
|
||||
member this.String = Predicate.ToString this
|
||||
member this.Name = match this with Pred (n,_) -> n
|
||||
member this.Args = match this with Pred (_,a) -> a
|
||||
static member refresh cle idProvider (Pred (n, ts)) = Pred (n, ts |> List.map (Term.refresh cle idProvider))
|
||||
static member Map (f:Term<'s> -> Term<'s>) (Pred (p, ts):Predicate<'s>) = Pred (p, ts |> List.map f)
|
||||
static member Species (Pred (_, ts):Predicate<'s>) = ts |> List.collect Term.Species
|
||||
|
||||
(* formulas *)
|
||||
and
|
||||
[<DebuggerDisplay("{this.String}")>]
|
||||
Literal<'s when 's : equality> = Pos of Predicate<'s>
|
||||
| Neg of Predicate<'s>
|
||||
with
|
||||
static member ToStringWith cle (l:Literal<'s>) =
|
||||
match l with
|
||||
| Pos p -> Predicate.ToStringWith cle p
|
||||
| Neg p -> sprintf "not %s" (Predicate.ToStringWith cle p)
|
||||
static member ToString(l:Literal<'s>) = Literal.ToStringWith CLE.empty l
|
||||
member this.String = Literal<'s>.ToString this
|
||||
|
||||
static member Map (f:Term<'s> -> Term<'s>) (l:Literal<'s>) = match l with
|
||||
| Pos p -> Pos (p |> Predicate<'s>.Map f)
|
||||
| Neg p -> Neg (p |> Predicate<'s>.Map f)
|
||||
static member Species (l:Literal<'s>) =
|
||||
match l with
|
||||
| Pos p
|
||||
| Neg p -> Predicate.Species p
|
||||
static member refresh cle idProvider (l:Literal<'s>) =
|
||||
match l with
|
||||
| Pos p -> Pos (Predicate.refresh cle idProvider p)
|
||||
| Neg p -> Neg (Predicate.refresh cle idProvider p)
|
||||
(*
|
||||
type Formula = Atom of Predicate<'s>
|
||||
| Not of Formula
|
||||
| And of Formula * Formula
|
||||
| Or of Formula * Formula
|
||||
| Implies of Formula * Formula
|
||||
| Iff of Formula * Formula
|
||||
| ForAll of Variable * Formula
|
||||
| Exists of Variable * Formula
|
||||
*)
|
||||
|
||||
(* logic programs *)
|
||||
and
|
||||
[<DebuggerDisplay("{this.String}")>]
|
||||
Clause<'s when 's : equality> = { head: Predicate<'s>
|
||||
body: Literal<'s> list } with
|
||||
static member Create(p:Predicate<'s>, bs:Literal<'s> list) = {head=p; body=bs}
|
||||
static member Create(p:Predicate<'s>) = {head=p; body=[]}
|
||||
static member Map (f:Term<'s> -> Term<'s>) (c:Clause<'s>) = { head = c.head |> Predicate<'s>.Map f
|
||||
body = c.body |> List.map (Literal<'s>.Map f)}
|
||||
static member Species (c:Clause<'s>) = Predicate.Species(c.head) @ (c.body |> List.collect Literal.Species) |> List.distinct
|
||||
|
||||
static member ToStringWith cle (c:Clause<'s>) =
|
||||
if c.body.IsEmpty
|
||||
then sprintf "%s." (Predicate.ToStringWith cle c.head)
|
||||
else sprintf "%s :- %s." (Predicate.ToStringWith cle c.head)
|
||||
(c.body |> List.map (Literal.ToStringWith cle) |> String.concat ", ")
|
||||
static member ToString(c:Clause<'s>) = Clause.ToStringWith CLE.empty c
|
||||
member this.String = Clause<'s>.ToString this
|
||||
|
||||
type Signature = string * int // the name and the number of arguments of a predicate (the head of a Horn clause in the program)
|
||||
type RulesProgram<'s when 's : comparison> = System.Collections.Generic.Dictionary<Signature, Set<Clause<'s>>>
|
||||
let toProgram p =
|
||||
p
|
||||
|> (List.fold (fun (acc:Map<Signature, Set<Clause<'s>>>) clause ->
|
||||
let name = clause.head.Name
|
||||
let args = clause.head.Args
|
||||
let key = name, args.Length
|
||||
if acc.ContainsKey(key)
|
||||
then let set = acc.[key]
|
||||
acc.Add(key, Set.add clause set)
|
||||
else acc.Add(key, Set.singleton(clause))
|
||||
) Map.empty
|
||||
>> Map.toSeq
|
||||
>> fun zz -> let x = new System.Collections.Generic.Dictionary<Signature, Set<Clause<'s>>>()
|
||||
for k,v in zz do
|
||||
x.Add(k,v)
|
||||
x)
|
||||
|
|
@ -0,0 +1,248 @@
|
|||
[<JavaScript>]
|
||||
module RulesDSD.Unification
|
||||
|
||||
open RulesDSD.Syntax
|
||||
open RulesDSD.Substitution
|
||||
|
||||
open System
|
||||
open System.Diagnostics
|
||||
|
||||
(**************************************)
|
||||
(**************************************)
|
||||
(******** Unification ***********)
|
||||
(* Unification is the process of finding a substitution \theta such that
|
||||
term_1\theta = term_2\theta for any term t_1 and t_2 [*].
|
||||
|
||||
If t_1 and t_2 are ground terms (i.e. they have no free variables),
|
||||
unification reduces to checking that t_1 is equal to t_2.
|
||||
In this case unification returns the identity substitution, Substitution.id.
|
||||
|
||||
|
||||
*: The notation t\theta means "apply substitution \theta to t".
|
||||
It's a useful notation to express function composition:
|
||||
t\theta_1\theta_2
|
||||
which is parsed (t\theta_1)\theta_2) and means "apply \theta_1 and then \theta_2 to t".
|
||||
*)
|
||||
(**************************************)
|
||||
(**************************************)
|
||||
[<DebuggerDisplay("{this.String}")>]
|
||||
type TermEquation<'s when 's : equality> = TEq of Term<'s> * Term<'s>
|
||||
with member this.String = match this with
|
||||
| TEq (t1, t2) -> sprintf "%s = %s" (Term.ToString t1) (Term.ToString t2)
|
||||
|
||||
|
||||
|
||||
let rec unifyLocation (l1, l2) : Substitution<'s, 'a> option=
|
||||
match l1, l2 with
|
||||
| Location.Loc(x1,y1),
|
||||
Location.Loc(x2,y2) -> if (x1,y1) = (x2,y2)
|
||||
then Some (Substitution<'s, 'a>.id)
|
||||
else None
|
||||
| Location.Var (-1,"_"), _
|
||||
| _, Location.Var (-1,"_") -> Some (Substitution<'s, 'a>.id)
|
||||
| Location.Var v, l
|
||||
| l, Location.Var v -> Some (Substitution<'s, 'a>.Create(v, l))
|
||||
|
||||
and unifyHoleEntry (cle:CLE<'s, 'a>) ((s1:'s, l1), (s2:'s, l2)) =
|
||||
match cle.unify (s1, s2) with
|
||||
| [] -> []
|
||||
| thetas1 ->
|
||||
match unifyLocation (l1, l2) with
|
||||
| Some theta2 -> thetas1 |> List.map (fun theta1 -> Substitution<'s, 'a>.Compose (Sub theta1) theta2 cle)
|
||||
| None -> []
|
||||
|
||||
and unifyInner (theta:Substitution<'s, 'a>) (cle:CLE<'s, 'a>) (sys:TermEquation<'s> list) : Substitution<'s, 'a> list =
|
||||
match sys with
|
||||
| [] -> [theta]
|
||||
| TEq (t1, t2) :: rest ->
|
||||
match t1, t2 with
|
||||
(*** list unification ***)
|
||||
| TCons (t, ts), TList (t' :: ts')
|
||||
| TList (t' :: ts'), TCons (t, ts) -> unifyInner theta cle (TEq (t, t') :: TEq (ts, TList ts') :: rest)
|
||||
|
||||
|
||||
| TCons (t, Term.Var(X,Y)), TCons (t', ts)
|
||||
| TCons (t', ts), TCons (t, Term.Var (X,Y))
|
||||
-> unifyInner theta cle (TEq (t, t') :: TEq (Term.Var (X,Y), ts) :: rest)
|
||||
|
||||
| TCons (t, Term.Var (X,Y)), TList ts
|
||||
| TList ts, TCons (t, Term.Var (X,Y))
|
||||
-> match ts with
|
||||
| [] -> []
|
||||
| t' :: ts' -> unifyInner theta cle (TEq (t, t') :: TEq (Term.Var (X,Y), TList ts') :: rest)
|
||||
|
||||
| TCons (t, ts), TCons (t', ts')
|
||||
| TCons (t', ts'), TCons (t, ts)
|
||||
-> unifyInner theta cle (TEq (t, t') :: TEq (ts, ts') :: rest)
|
||||
|
||||
| TList ts1, TList ts2 ->
|
||||
if ts1.Length = ts2.Length
|
||||
then
|
||||
let newEqs = List.zip ts1 ts2
|
||||
|> List.map TEq
|
||||
unifyInner theta cle (newEqs @ rest)
|
||||
else []
|
||||
|
||||
(*** Sets and Multisets unification ***)
|
||||
// Unification in this section roughly follows the paper:
|
||||
// "Integrating Lists, Multisets, and Sets in a Logic Programming Framework", A. Dovier, A. Policriti, G. Rossi at https://doi.org/10.1007/978-94-009-0349-4_16
|
||||
| TCRN crn1, TCRN crn2 ->
|
||||
// TODO: otimization: check if the CRN is ground?
|
||||
if crn1.Length <> crn2.Length
|
||||
then [] // unification fails
|
||||
else
|
||||
let rec g t1 crn2 acc crn1 sols =
|
||||
match crn2 with
|
||||
| [] -> sols
|
||||
| t2::rest2 -> let crn1' = TCRN crn1
|
||||
let crn2' = TCRN (rest2 @ acc)
|
||||
let sols' = unifyInner theta cle (TEq (t1, t2) :: TEq (crn1', crn2') :: rest)
|
||||
g t1 rest2 (t2::acc) crn1 (sols @ sols')
|
||||
and f crn1 crn2 acc sols =
|
||||
match crn1 with
|
||||
| [] -> match crn2 with
|
||||
| [] -> unifyInner theta cle rest
|
||||
| _::_ -> sols
|
||||
| t1::rest1 -> let crn1' = acc @ rest1
|
||||
let sols' = g t1 crn2 [] crn1' sols
|
||||
f rest1 crn2 (t1::acc) sols'
|
||||
|
||||
f crn1 crn2 [] [] |> List.distinct
|
||||
|
||||
(* set unification algorithm (adapted to the case {t0...tn|X} with X = []):
|
||||
t|s = t'|s' iff t=t' and:
|
||||
s = s'
|
||||
or t|s = s'
|
||||
or s = t'|s'
|
||||
*)
|
||||
| TMSet ts1, TMSet ts2 ->
|
||||
if (ts1.Length = 0 && ts2.Length <> 0)
|
||||
|| (ts2.Length = 0 && ts1.Length <> 0) // TODO: what if two elements in one mset are unified, and the lenghts become different?
|
||||
then []
|
||||
else
|
||||
match ts1 with
|
||||
| [] -> unifyInner theta cle rest
|
||||
| (n1, t1)::tail1 ->
|
||||
let rec f acc heads2 curr =
|
||||
match curr with
|
||||
| (n2, t2) :: tail2 ->
|
||||
match unifyInner theta cle [TEq (t1, t2)] with
|
||||
| [] -> // unify t1 with another element of the multiset
|
||||
f acc ((n2, t2)::heads2) tail2
|
||||
| thetas' ->
|
||||
let sols =
|
||||
thetas'
|
||||
|> List.collect (fun theta' ->
|
||||
let t1' = if n1 = n2
|
||||
then TMSet tail1
|
||||
else TMSet ((abs (n1-n2), t1)::tail1)
|
||||
|> fun x -> theta'.Apply(x, cle)
|
||||
let t2' = TMSet (heads2@tail2)
|
||||
|> fun x -> theta'.Apply(x, cle)
|
||||
let rest' = rest |> List.map (fun (TEq(t1, t2)) -> TEq (theta'.Apply(t1, cle), theta'.Apply(t2, cle)))
|
||||
let newConstraints = TEq (t1', t2') :: rest'
|
||||
unifyInner theta' cle newConstraints)
|
||||
f (sols @ acc) ((n2, t2)::heads2) tail2
|
||||
| [] -> acc
|
||||
|
||||
f [] [] ts2
|
||||
|> List.collect (fun theta' -> unifyInner theta' cle rest)
|
||||
|> List.distinct
|
||||
|
||||
|
||||
|
||||
|
||||
(*** Operations unification ***)
|
||||
| Func (f, xs), Func (g, ys) ->
|
||||
if f <> g
|
||||
then []
|
||||
elif xs.Length <> ys.Length
|
||||
then []
|
||||
else
|
||||
let newEqs = List.zip xs ys |> List.map TEq
|
||||
unifyInner theta cle (newEqs @ rest)
|
||||
(*** Base terms unification ***)
|
||||
| Float n1, Float n2 ->
|
||||
if n1 = n2
|
||||
then unifyInner theta cle rest
|
||||
else []
|
||||
| Const c1, Const c2 ->
|
||||
if c1 = c2
|
||||
then unifyInner theta cle rest
|
||||
else []
|
||||
|
||||
(*** Variables unification ***)
|
||||
| t, Term.Var (-1, "_")
|
||||
| Term.Var (-1, "_"), t -> match t with
|
||||
| Term.Var (-1, "_") -> unifyInner theta cle rest
|
||||
| Term.Var (X, Y) -> let theta' : Substitution<'s, 'a> = theta.Add(TVar (X,Y), Term.Var (-1, "_"), cle)
|
||||
rest |> List.map (fun (TEq(t1, t2)) -> TEq (theta'.Apply(t1, cle), theta'.Apply(t2, cle)))
|
||||
|> fun x -> unifyInner theta' cle x
|
||||
| _ -> unifyInner theta cle rest
|
||||
| Term.Var (X,Y), t -> if Term.Var (X,Y) = t
|
||||
then unifyInner theta cle rest // skips "X = X"
|
||||
elif (fvt cle t |> Set.map Variable<_,_>.ToVar).Contains (X,Y)
|
||||
then [] // occurs-check failed
|
||||
else
|
||||
let theta' = theta.Add(TVar (X,Y), t, cle)
|
||||
rest |> List.map (fun (TEq(t1, t2)) -> TEq (theta'.Apply(t1, cle), theta'.Apply(t2, cle )))
|
||||
|> unifyInner theta' cle
|
||||
|
||||
(*** Patterns unification ***)
|
||||
| (Pat p1, Pat p2) ->
|
||||
match p1, p2 with
|
||||
| Nihil, Nihil -> [Substitution<'s, 'a>.id]
|
||||
| Nicking (a1, b1), Nicking (a2, b2)
|
||||
-> if a1.Length <> a2.Length
|
||||
|| b1.Length <> b2.Length
|
||||
then []
|
||||
else let a3 = List.zip a1 a2
|
||||
let b3 = List.zip b1 b2
|
||||
let unifiedPatterns =
|
||||
(a3 @ b3)
|
||||
|> List.fold (fun subs (s1, s2) ->
|
||||
subs
|
||||
|> List.collect (fun (sub : Substitution<'s, 'a>)-> unifyHoleEntry cle (sub.Apply(s1, cle), sub.Apply(s2, cle)))
|
||||
|> List.allPairs subs
|
||||
|> List.map (fun (sub, sub') -> Substitution.Compose sub sub' cle))
|
||||
[Substitution.id]
|
||||
unifiedPatterns
|
||||
|> List.choose (fun x -> Substitution.TryMerge theta x cle)
|
||||
|> List.collect (fun (theta' : Substitution<'s, 'a>) ->
|
||||
rest
|
||||
|> List.map (fun (TEq (x, y)) -> TEq (theta'.Apply(x, cle), theta'.Apply(y, cle)))
|
||||
|> unifyInner theta' cle)
|
||||
|
||||
| Pattern.Strand s1, Pattern.Strand s2
|
||||
| Pattern.Inner s1, Pattern.Inner s2
|
||||
| Pattern.ThreePrime s1, Pattern.ThreePrime s2
|
||||
| Pattern.FivePrime s1, Pattern.FivePrime s2
|
||||
-> if s1.Length <> s2.Length
|
||||
then []
|
||||
else
|
||||
let unifiedPattern =
|
||||
List.zip s1 s2
|
||||
|> List.fold (fun subs (s1, s2) ->
|
||||
subs
|
||||
|> List.collect (fun (sub : Substitution<'s,'a>) -> unifyHoleEntry cle (sub.Apply(s1, cle), sub.Apply(s2, cle)))
|
||||
|> List.allPairs subs
|
||||
|> List.map (fun (sub, sub') -> Substitution.Compose sub sub' cle))
|
||||
[Substitution.id]
|
||||
unifiedPattern
|
||||
|> List.choose (fun x -> Substitution.TryMerge theta x cle)
|
||||
|> List.collect (fun (theta' : Substitution<'s,'a>) ->
|
||||
rest
|
||||
|> List.map (fun (TEq (x, y)) -> TEq (theta'.Apply(x, cle), theta'.Apply(y, cle)))
|
||||
|> unifyInner theta' cle)
|
||||
| _, _ -> [] // sprintf "Patterns mismatch: \"%s\", \"%s\" " (t1.ToString()) (t2.ToString())
|
||||
|
||||
| (Term.Proc p1, Term.Proc p2) -> // TODO: this assumes processes are in canonical form
|
||||
if Process.Canonical cle p1 = Process.Canonical cle p2
|
||||
then unifyInner theta cle rest
|
||||
else []
|
||||
|
||||
// flip var on rhs
|
||||
| (t1, Var (X,Y)) -> unifyInner theta cle (TEq (Var (X,Y), t1)::rest)
|
||||
| _ -> [] // Choice2Of2 <| sprintf "Failed unification: cannot unify \"%s\" with \"%s\"" (Term.ToString t1) (Term.ToString t2)
|
||||
|
||||
and unify cle : TermEquation<'s> list -> Substitution<'s, 'a> list = unifyInner Substitution<'s,'a>.id cle
|
||||
|
|
@ -0,0 +1,37 @@
|
|||
|
||||
Microsoft Visual Studio Solution File, Format Version 12.00
|
||||
# Visual Studio 15
|
||||
VisualStudioVersion = 15.0.27130.2027
|
||||
MinimumVisualStudioVersion = 10.0.40219.1
|
||||
Project("{6EC3EE1D-3C4E-46DD-8F32-0CC8E756570}") = "ParserCombinatorsJS", "..\ParserCombinators\ParserCombinatorsJS\ParserCombinatorsJS.fsproj", "{2EED2DFA-7D94-4E12-ADC5-455FC9F85BF9}"
|
||||
EndProject
|
||||
Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "SiteGraphReactorJS", "..\SiteGraphReactor\SiteGraphReactorJS\SiteGraphReactorJS.fsproj", "{E7457C45-ABDE-4DF5-B7A2-D396D2825B2C}"
|
||||
EndProject
|
||||
Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "RulesDSDJS", "RulesDSDJS\RulesDSDJS.fsproj", "{0A242719-974A-4831-BECF-D9F29B85F335}"
|
||||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|Any CPU = Debug|Any CPU
|
||||
Release|Any CPU = Release|Any CPU
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{2EED2DFA-7D94-4E12-ADC5-455FC9F85BF9}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
|
||||
{2EED2DFA-7D94-4E12-ADC5-455FC9F85BF9}.Debug|Any CPU.Build.0 = Debug|Any CPU
|
||||
{2EED2DFA-7D94-4E12-ADC5-455FC9F85BF9}.Release|Any CPU.ActiveCfg = Release|Any CPU
|
||||
{2EED2DFA-7D94-4E12-ADC5-455FC9F85BF9}.Release|Any CPU.Build.0 = Release|Any CPU
|
||||
{E7457C45-ABDE-4DF5-B7A2-D396D2825B2C}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
|
||||
{E7457C45-ABDE-4DF5-B7A2-D396D2825B2C}.Debug|Any CPU.Build.0 = Debug|Any CPU
|
||||
{E7457C45-ABDE-4DF5-B7A2-D396D2825B2C}.Release|Any CPU.ActiveCfg = Release|Any CPU
|
||||
{E7457C45-ABDE-4DF5-B7A2-D396D2825B2C}.Release|Any CPU.Build.0 = Release|Any CPU
|
||||
{0A242719-974A-4831-BECF-D9F29B85F335}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
|
||||
{0A242719-974A-4831-BECF-D9F29B85F335}.Debug|Any CPU.Build.0 = Debug|Any CPU
|
||||
{0A242719-974A-4831-BECF-D9F29B85F335}.Release|Any CPU.ActiveCfg = Release|Any CPU
|
||||
{0A242719-974A-4831-BECF-D9F29B85F335}.Release|Any CPU.Build.0 = Release|Any CPU
|
||||
EndGlobalSection
|
||||
GlobalSection(SolutionProperties) = preSolution
|
||||
HideSolutionNode = FALSE
|
||||
EndGlobalSection
|
||||
GlobalSection(ExtensibilityGlobals) = postSolution
|
||||
SolutionGuid = {60093EFF-8C1C-48D5-8F6D-0E3E11201D4D}
|
||||
EndGlobalSection
|
||||
EndGlobal
|
||||
|
|
@ -0,0 +1,13 @@
|
|||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<configuration>
|
||||
<startup>
|
||||
<supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.7.2" />
|
||||
</startup>
|
||||
|
||||
<runtime><assemblyBinding xmlns="urn:schemas-microsoft-com:asm.v1">
|
||||
<dependentAssembly>
|
||||
<Paket>True</Paket>
|
||||
<assemblyIdentity name="FSharp.Core" publicKeyToken="b03f5f7f11d50a3a" culture="neutral" />
|
||||
<bindingRedirect oldVersion="0.0.0.0-65535.65535.65535.65535" newVersion="4.7.0.0" />
|
||||
</dependentAssembly>
|
||||
</assemblyBinding></runtime></configuration>
|
||||
|
|
@ -0,0 +1,51 @@
|
|||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<Project Sdk="Microsoft.NET.Sdk">
|
||||
<PropertyGroup>
|
||||
<TargetFramework>netstandard2.0</TargetFramework>
|
||||
<AutoGenerateBindingRedirects>true</AutoGenerateBindingRedirects>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Release|AnyCPU'">
|
||||
<DefineConstants>TRACE;JavaScript</DefineConstants>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Debug|AnyCPU'">
|
||||
<DefineConstants>TRACE;JavaScript</DefineConstants>
|
||||
</PropertyGroup>
|
||||
<ItemGroup>
|
||||
<Compile Include="..\RulesDSD\AssemblyInfo.fs">
|
||||
<Link>AssemblyInfo.fs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\RulesDSD\syntax.fs">
|
||||
<Link>syntax.fs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\RulesDSD\concreteProcess.fs">
|
||||
<Link>concreteProcess.fs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\RulesDSD\substitution.fs">
|
||||
<Link>substitution.fs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\RulesDSD\unification.fs">
|
||||
<Link>unification.fs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\RulesDSD\processEquality.fs">
|
||||
<Link>processEquality.fs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\RulesDSD\resolution.fs">
|
||||
<Link>resolution.fs</Link>
|
||||
</Compile>
|
||||
<Compile Include="..\RulesDSD\parser.fs">
|
||||
<Link>parser.fs</Link>
|
||||
</Compile>
|
||||
<Content Include="App.config" />
|
||||
<None Include="paket.references" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<ProjectReference Include="..\..\CRNEngine\CRNEngineJS\CRNEngineJS.fsproj" />
|
||||
<ProjectReference Include="..\..\PDESolvers\ReactionDiffusionJS\ReactionDiffusionJS.fsproj" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<Reference Include="Oslo.FSharp.WebSharper">
|
||||
<HintPath>..\..\Lib\Oslo-FSharp.websharper\Oslo.FSharp.WebSharper.dll</HintPath>
|
||||
</Reference>
|
||||
</ItemGroup>
|
||||
<Import Project="..\..\.paket\Paket.Restore.targets" />
|
||||
</Project>
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
group NETSTANDARD
|
||||
|
||||
WebSharper.FSharp
|
||||
FSharp.Core
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
//This comes from the default xUnit template
|
||||
module Program = let [<EntryPoint>] main _ = 0
|
||||
|
|
@ -0,0 +1,21 @@
|
|||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<Project Sdk="Microsoft.NET.Sdk">
|
||||
<PropertyGroup>
|
||||
<TargetFramework>netcoreapp3.1</TargetFramework>
|
||||
<IsPackable>false</IsPackable>
|
||||
<GenerateProgramFile>false</GenerateProgramFile>
|
||||
</PropertyGroup>
|
||||
<ItemGroup>
|
||||
<Compile Include="unification.test.fs" />
|
||||
<Compile Include="resolution.test.fs" />
|
||||
<Compile Include="parser.test.fs" />
|
||||
<Compile Include="integration.test.fs" />
|
||||
<Compile Include="Program.fs" />
|
||||
<None Include="paket.references" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<ProjectReference Include="..\..\ClassicDSD\ClassicDSDDotNet\ClassicDSDDotNet.fsproj" />
|
||||
<ProjectReference Include="..\RulesDSD\RulesDSD.fsproj" />
|
||||
</ItemGroup>
|
||||
<Import Project="..\..\.paket\Paket.Restore.targets" />
|
||||
</Project>
|
||||
|
|
@ -0,0 +1,178 @@
|
|||
module RulesDSD.IntegrationTests
|
||||
|
||||
open FsUnit
|
||||
open Xunit
|
||||
open FsUnit.Xunit
|
||||
|
||||
open RulesDSD.Syntax
|
||||
open RulesDSD.Resolution
|
||||
|
||||
|
||||
let cle = Microsoft.Research.DNA.LogicDSD.engine
|
||||
let psite = Microsoft.Research.DNA.LogicDSD.psite cle
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Resolution - Context finding")>]
|
||||
let testContextFinding () =
|
||||
let provider = RulesDSD.Syntax.makeProvider ()
|
||||
let ps = psite provider true
|
||||
let strands = Parser.from_string (RulesDSD.Parser.psystem ps)
|
||||
"<a b!0> | <d e^!1> | <f c^!2 d!3> | <e^*!1 d*!3 c^*!2 b*!0>"
|
||||
|
||||
let program = Parser.from_string (RulesDSD.Parser.pprogram cle (fun x -> psite x false))
|
||||
"ok(P) :-
|
||||
P = C [E!j D] [D!i] [D'!i F!k].
|
||||
|
||||
ok(P) :-
|
||||
P = C [D E!j] [D!i] [F!k D'!i]."
|
||||
let goal = Pos (Pred("ok", [Term.Proc strands]))
|
||||
match resolveAll goal program cle with
|
||||
| None -> failwith "Test failed."
|
||||
| Some sols -> let xs = sols |> List.map (fun theta -> theta.Apply (Term.Var (provider "C"), cle))
|
||||
Assert.Equal(1, xs.Length)
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Resolution - Context substitution")>]
|
||||
let testContextSubs () =
|
||||
let provider = RulesDSD.Syntax.makeProvider ()
|
||||
let ps = psite provider true
|
||||
let strands = Parser.from_string (RulesDSD.Parser.psystem ps)
|
||||
"<a b!0> | <d e^!1> | <f c^!2 d!3> | <e^*!1 d*!3 c^*!2 b*!0>"
|
||||
|
||||
let program = Parser.from_string (RulesDSD.Parser.pprogram cle (fun x -> psite x false))
|
||||
"ok(P, Q) :-
|
||||
P = C [E!j D] [D!i] [D'!i F!k],
|
||||
Q = C [E!j D!i] [D] [D'!i F!k].
|
||||
|
||||
ok(P, Q) :-
|
||||
P = C [D E!j] [D!i] [F!k D'!i],
|
||||
Q = C [D!i E!j] [D] [F!k D'!i]."
|
||||
let goal = Pos (Pred("ok", [Term.Proc strands; Term.Var (provider "Q")]))
|
||||
match resolveAll goal program cle with
|
||||
| None -> failwith "Test failed."
|
||||
| Some sols -> let xs = sols |> List.map (fun theta -> theta.Apply (Term.Var (provider "Q"), cle))
|
||||
Assert.Equal(1, xs.Length)
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Resolution - Context displacement")>]
|
||||
let testContextDispl () =
|
||||
let provider = RulesDSD.Syntax.makeProvider ()
|
||||
let ps = psite provider true
|
||||
let strands = Parser.from_string (RulesDSD.Parser.psystem ps)
|
||||
"<a b!0> | <d e^!1> | <f c^!2 d!3> | <e^*!1 d*!3 c^*!2 b*!0>"
|
||||
|
||||
let program = Parser.from_string (RulesDSD.Parser.pprogram cle (fun x -> psite x false))
|
||||
"reaction([P], Rate, Q) :-
|
||||
P = C [E!j D] [D!i] [D'!i F!k],
|
||||
Q = C [E!j D!i] [D] [D'!i F!k],
|
||||
Rate is 20,
|
||||
junction(E!j, F!k, Q).
|
||||
// junction(E!j, Q).
|
||||
|
||||
reaction([P], Rate, Q) :-
|
||||
P = C [D E!j] [D!i] [F!k D'!i],
|
||||
Q = C [D!i E!j] [D] [F!k D'!i],
|
||||
Rate is 20,
|
||||
junction(E!j, F!k, Q).
|
||||
|
||||
junction(E!j,F!j,_).
|
||||
junction(E!j,F!k,Q):-
|
||||
Q = C [F!k] [G!l E'!j] [E!j],
|
||||
junction(G!l,F!k,Q)."
|
||||
|
||||
let goal = Pos (Pred("reaction", [TList [Term.Proc strands]; Term.Var (provider "Rate"); Term.Var (provider "Q")]))
|
||||
match resolveAll goal program cle with
|
||||
| None -> failwith "Test failed."
|
||||
| Some sols -> let xs = sols |> List.map (fun theta -> theta.Apply (Term.Var (provider "Q"), cle))
|
||||
Assert.Equal(1, xs.Length)
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Syntax - Canonical form")>]
|
||||
let testCanonical () =
|
||||
let provider = RulesDSD.Syntax.makeProvider ()
|
||||
let ps = psite provider true
|
||||
let canonize x = x |> Parser.from_string (RulesDSD.Parser.psystem ps) |> Process.Canonical cle
|
||||
let a = canonize "<a!0 b!1> | <a!2 b!3> | <b!3 a!2 b!1 a!0>" |> Process.ToStringWith cle
|
||||
let b = canonize "<a!2 b!3> | <a!0 b!1> | <b!3 a!2 b!1 a!0>" |> Process.ToStringWith cle
|
||||
let c = canonize "<a!0 b!1> | <a!2 b!3> | <b!1 a!0 b!3 a!2>" |> Process.ToStringWith cle
|
||||
let d = canonize "<a!2 b!3> | <a!0 b!1> | <b!1 a!0 b!3 a!2>" |> Process.ToStringWith cle
|
||||
Assert.True( (a = b) )
|
||||
Assert.True( (b = c) )
|
||||
Assert.True( (c = d) )
|
||||
|
||||
let e = canonize "<b tx^!0> | <to^*!1 x*!2 tx^*!0 b*!3 tb^*!4> | <x!2 to^!1> | <tb^!4 b!3>" |> Process.ToStringWith cle
|
||||
let f = canonize "<to^*!0 x*!1 tx^*!2 b*!3 tb^*!4> | <x!1 to^!0> | <b tx^!2> | <tb^!4 b!3>" |> Process.ToStringWith cle
|
||||
Assert.True( (e = f) )
|
||||
|
||||
let g = canonize "<a^!0 c^*!1 a^*!2 c^!3 a^*!4 c^*!5 a^*!6 a^*!7 a^*!8 c^!9 c^*!10 a^!11 c^*!12 a^*!13 a^!14 a^!15> | <a^!16 a^*!17 c^*!18 a^!19 c^*!20 a^*!21 c^!22 a^!23 a^*!24 c^*!25 c^!26> | <a^*{\"O\"}!15 a^*!14 a^!13 c^!12 a^*!11 c^!10 c^*!9 a^!8 a^!7 a^!6 c^!5 a^!4 c^*!3 a^!2 c^!1 a^*!0 c^*!26 c^!25 a^!24 a^*!23 c^*!22 a^!21 c^!20 a^*!19 c^!18 a^!17 a^*!16>" |> Process.ToStringWith cle
|
||||
let h = canonize "<a^!0 a^*!1 c^*!2 a^!3 c^*!4 a^*!5 c^!6 a^!7 a^*!8 c^*!9 c^!10> | <a^!11 c^*!12 a^*!13 c^!14 a^*!15 c^*!16 a^*!17 a^*!18 a^*!19 c^!20 c^*!21 a^!22 c^*!23 a^*!24 a^!25 a^!26> | <a^*{\"O\"}!26 a^*!25 a^!24 c^!23 a^*!22 c^!21 c^*!20 a^!19 a^!18 a^!17 c^!16 a^!15 c^*!14 a^!13 c^!12 a^*!11 c^*!10 c^!9 a^!8 a^*!7 c^*!6 a^!5 c^!4 a^*!3 c^!2 a^!1 a^*!0>" |> Process.ToStringWith cle
|
||||
Assert.True( (g = h) )
|
||||
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Resolution - Phosphate nucleotide")>]
|
||||
let testPhopsho () =
|
||||
let provider1 = RulesDSD.Syntax.makeProvider ()
|
||||
let ps1 = psite provider1 true
|
||||
let strands1 = Parser.from_string (RulesDSD.Parser.psystem ps1)
|
||||
"""<a!0 b{"phosphate"}> | <a*!0>"""
|
||||
|
||||
let program = Parser.from_string (RulesDSD.Parser.pprogram cle (fun x -> psite x false))
|
||||
"""polymerase(P,Q,A!i,B!j) :-
|
||||
P = C [<A!i>] [<A'!i B'>], not (B' = _ {"phosphate"}), compl(B, B'),
|
||||
Q = C [<A!i B!j>] [<B'!j A'!i>], freshBond(B!j, P)."""
|
||||
|
||||
let goal = Pos (Pred("polymerase", [Term.Proc strands1; Term.Var (-1, "_"); Term.Var (-1, "_"); Term.Var (-1, "_")]))
|
||||
let result = resolveAll goal program cle
|
||||
Assert.True( Option.isNone result)
|
||||
|
||||
let provider2 = RulesDSD.Syntax.makeProvider ()
|
||||
let ps2 = psite provider2 true
|
||||
let strands2 = Parser.from_string (RulesDSD.Parser.psystem ps2)
|
||||
"""<a!0 b{"phosphat"}> | <a*!0>"""
|
||||
let goal = Pos (Pred("polymerase", [Term.Proc strands2; Term.Var (-1, "_"); Term.Var (-1, "_"); Term.Var (-1, "_")]))
|
||||
let result = resolveAll goal program cle
|
||||
Assert.True( Option.isSome result)
|
||||
|
||||
let provider3 = RulesDSD.Syntax.makeProvider ()
|
||||
let ps3 = psite provider3 true
|
||||
let strands3 = Parser.from_string (RulesDSD.Parser.psystem ps3)
|
||||
"""<a!0 b> | <a*!0>"""
|
||||
let goal = Pos (Pred("polymerase", [Term.Proc strands3; Term.Var (-1, "_"); Term.Var (-1, "_"); Term.Var (-1, "_")]))
|
||||
let result = resolveAll goal program cle
|
||||
Assert.True( Option.isSome result)
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Resolution - Pseudoknot formation")>]
|
||||
let testPseudoknot () =
|
||||
let provider1 = RulesDSD.Syntax.makeProvider ()
|
||||
let ps1 = psite provider1 true
|
||||
let program = Parser.from_string (RulesDSD.Parser.pprogram cle (fun x -> psite x false)) """
|
||||
bind(P,Q,D!i) :-
|
||||
P = C [D] [D'], compl(D, D'),
|
||||
Q = C [D!i] [D'!i], freshBond(D!i, P).
|
||||
|
||||
displace(P,Q,E!j,D!i) :-
|
||||
P = C [E!j D] [D!i] [D'!i E'!j],
|
||||
Q = C [E!j D!i] [D] [D'!i E'!j].
|
||||
|
||||
displaceL(P,Q,E!j,D!i) :-
|
||||
P = C [D!i] [D E!j] [E'!j D'!i],
|
||||
Q = C [D] [D!i E!j] [E'!j D'!i].
|
||||
|
||||
unbind(P,Q,D!i) :-
|
||||
P = C [D!i] [D'!i], toehold(D),
|
||||
Q = C [D] [D'], not adjacent(D!i,_,P).
|
||||
|
||||
adjacent(D!i,E!j,P) :- P = C [D!i E!j] [E'!j D'!i].
|
||||
adjacent(D!i,E!j,P) :- P = C [E!j D!i] [D'!i E'!j].
|
||||
|
||||
reaction([P], "bind",Q) :- bind(P,Q,_).
|
||||
reaction([P],"displace",Q) :- displace(P,Q,_,_).
|
||||
reaction([P],"displace",Q) :- displaceL(P,Q,_,_).
|
||||
reaction([P],"unbind",Q) :- unbind(P,Q,_)."""
|
||||
|
||||
let strands = Parser.from_string (RulesDSD.Parser.psystem ps1)
|
||||
"""<a b a* b*>"""
|
||||
let goal = Pos (Pred("reaction", [Term.TList [Term.Proc strands]; Term.Var (-1, "_"); Term.Var (-1, "Q")]))
|
||||
let result = resolveAll goal program cle
|
||||
Assert.True( Option.isSome result)
|
||||
|
|
@ -0,0 +1,8 @@
|
|||
group DOTNETCORE
|
||||
|
||||
#FsCheck
|
||||
FSharp.Core
|
||||
FsUnit.xUnit
|
||||
xunit.core
|
||||
xunit.runner.console
|
||||
xunit.runner.visualstudio
|
||||
|
|
@ -0,0 +1,635 @@
|
|||
module RulesDSD.ParserTests
|
||||
|
||||
open FsUnit
|
||||
open Xunit
|
||||
open FsUnit.Xunit
|
||||
|
||||
open RulesDSD.Syntax
|
||||
open RulesDSD.Unification
|
||||
open RulesDSD.Substitution
|
||||
open RulesDSD.Resolution
|
||||
open RulesDSD.Parser
|
||||
open Parser
|
||||
open ResolutionTests
|
||||
open System.Text.RegularExpressions
|
||||
open Microsoft.Research.DNA.LogicDSD
|
||||
|
||||
let cle = Microsoft.Research.DNA.LogicDSD.engine
|
||||
|
||||
let flattenDict (x:System.Collections.Generic.IDictionary<(string * int),Set<Clause<SiteT>>>) =
|
||||
x.Values
|
||||
|> Seq.concat
|
||||
|> Seq.toList
|
||||
|
||||
let removeVarNumbers x = Regex.Replace(x, "\([0-9]*\)", "")
|
||||
let print = List.map (Clause.ToStringWith cle >> removeVarNumbers) >> Seq.sortWith (fun x y -> System.String.Compare(x, y)) >> String.concat "\n"
|
||||
let printClause = Clause.ToStringWith cle >> removeVarNumbers
|
||||
|
||||
[<Fact(DisplayName="Logic Engine - Parsing - numbers")>]
|
||||
let parsingNumbers() =
|
||||
let text = """1"""
|
||||
let cache = idProvider ()
|
||||
let ps = fun _ -> failwith ""
|
||||
let parsed = Parser.from_string (pterm ps cle cache engine.domainKeywords) text
|
||||
|
||||
Assert.Equal<Term<SiteT>>(Term.Float 1.0, parsed)
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Parsing - anchored predicate")>]
|
||||
let parsingAnchoredPredicateTest() =
|
||||
let text = """
|
||||
strandDisplacementRule(P, Q) :-
|
||||
P = C [E!j D] [D!i] [D'!i F!k],
|
||||
Q = C [E!j D!i] [D] [D'!i F!k],
|
||||
junction(E!j, F!k, Q).
|
||||
|
||||
junction(E!j,F!j,_).
|
||||
|
||||
junction(E!j,F!k,Q) :-
|
||||
Q = C [G!l E'!j] [E!j],
|
||||
junction(G!l,F!k,Q).
|
||||
"""
|
||||
|
||||
let parsed = Parser.from_string (pprogram cle (fun x -> psite cle x false)) text |> flattenDict
|
||||
let expected = anchoredPredicateFailProgram |> flattenDict
|
||||
// TODO: parse <a*!1> | <a!1 b> | <b!2> | <a!3> | <c!4> | <c*!4 b*!2 a*!3>
|
||||
Assert.Equal<string>(print expected, print parsed)
|
||||
|
||||
let hiddenProgramText = """
|
||||
hidden(D!i, P) :-
|
||||
P = C [D!i] [A @ Start D'!i @ End],
|
||||
path(A@Start, _@Start, End, P, "left", [], Path),
|
||||
not (member(D!i, Path)).
|
||||
|
||||
path(_, End, End, _, _, Visited, Path) :-
|
||||
reverse(Visited, Path).
|
||||
|
||||
path(X, Start, End, P, "left", Visited, Path) :-
|
||||
not (Start = End),
|
||||
P = C[ Y@Start' _@Start],
|
||||
// prevDomain(Start, [Y; Start'], P),
|
||||
not member([Y; Start'], Visited),
|
||||
path(Y, Start', End, P, "left", [[X; Start] # Visited], Path).
|
||||
|
||||
path(X, Start, End, P, "right", Visited, Path) :-
|
||||
not (Start = End),
|
||||
// nextDomain(Start, [Y; Start'], P),
|
||||
P = C[ _@Start Y@Start' ],
|
||||
not member([Y; Start'], Visited),
|
||||
path(Y, Start', End, P, "right", [[X; Start] # Visited], Path).
|
||||
|
||||
path(X, Start, End, P, "any", Visited, Path) :-
|
||||
not (Start = End),
|
||||
path(X, Start, End, P, "left", Visited, Path).
|
||||
|
||||
path(X, Start, End, P, "any", Visited, Path) :-
|
||||
not (Start = End),
|
||||
path(X, Start, End, P, "right", Visited, Path).
|
||||
|
||||
path(D!i, Start, _@End, P, _, Visited, Path) :-
|
||||
not (Start = _@End),
|
||||
P = C [D!i] [D'!i@Start'],
|
||||
// pos(1, 0, C, Start'),
|
||||
not member([D'!i; Start'], Visited),
|
||||
path(D'!i, _@Start', _@End, P, "any", [[D!i; Start] # Visited], Path).
|
||||
"""
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Parsing - hidden predicate")>]
|
||||
let parsingHiddenPredicateTest() =
|
||||
let parsed = Parser.from_string (pprogram cle (fun x -> psite cle x false)) hiddenProgramText
|
||||
|> fun x -> x.Values
|
||||
|> Seq.concat
|
||||
|> Seq.toList
|
||||
let expected = hiddenProg
|
||||
Assert.Equal<string>(print expected, print parsed)
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Parsing - hierarchy")>]
|
||||
let parsingHierarchyTest() =
|
||||
let text = """rule("fast", P, Q) :-
|
||||
P = C [E!j D] [D!i] [D'!i F!k],
|
||||
Q = C [E!j D!i] [D] [D'!i F!k],
|
||||
junction(E!j, F!k, Q).
|
||||
|
||||
junction(E!j,F!j,_).
|
||||
|
||||
junction(E!j,F!k,Q):-
|
||||
// Q = C [G!l E'!j] [E!j] [F!k],
|
||||
Q = C [F!k] [E!j] [G!l E'!j],
|
||||
junction(G!l, F!k, Q).
|
||||
|
||||
rule("loop", P, Q, Q, V). // V for visited
|
||||
rule("loop", P, Q, R, V) :-
|
||||
rule("hierarchy", Q, R, V).
|
||||
|
||||
rule("hierarchy", P, R, V) :-
|
||||
rule("fast", P, Q),
|
||||
not member(Q, V),
|
||||
rule("loop", P, Q, R, [Q # V]).
|
||||
|
||||
rule("rxn", P ,Q) :-
|
||||
rule("hierarchy", P, Q, [P]),
|
||||
not rule("fast", Q, _).
|
||||
"""
|
||||
let parsed = Parser.from_string (pprogram cle (fun x -> psite cle x false)) text |> flattenDict
|
||||
let expected = hierarchyProgram |> flattenDict
|
||||
Assert.Equal<string>(print expected, print parsed)
|
||||
|
||||
|
||||
(****************************)
|
||||
(* Strand Graphs semantics *)
|
||||
(****************************)
|
||||
[<Fact(DisplayName="Logic DSD - Parsing - SG binding rule")>]
|
||||
let parsingBindingRuleTest() =
|
||||
let text = hiddenProgramText + """
|
||||
bindingRule(P, Q) :-
|
||||
P = C [D][D'],
|
||||
freshBond(D!i, P),
|
||||
compl(D, D'),
|
||||
Q = C [D!i] [D'!i],
|
||||
not hidden(D!i, Q).
|
||||
"""
|
||||
let parsed = Parser.from_string (pprogram cle (fun x -> psite cle x false)) text |> flattenDict
|
||||
let expected = bindingProgram |> flattenDict
|
||||
let s1 = print expected
|
||||
let s2 = print parsed
|
||||
Assert.Equal<string>(print expected, print parsed)
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Parsing - SG unbinding rule")>]
|
||||
let parsingUnbindingRuleTest() =
|
||||
let text = """
|
||||
rule("unbinding", P, Q) :-
|
||||
P = C [X!i] [X'!i],
|
||||
// toehold(X),
|
||||
Q = C [X] [X'],
|
||||
not junction(X!i, P).
|
||||
|
||||
junction(_!i, P) :-
|
||||
P = C [X!i E!j] [F!k X'!i],
|
||||
junction(X!i E!j, F!k X'!i, P).
|
||||
|
||||
junction(E!j,F!j,_).
|
||||
|
||||
junction(E!j,F!k,Q):-
|
||||
Q = C [F!k] [E!j] [G!l E'!j],
|
||||
junction(G!l,F!k,Q).
|
||||
"""
|
||||
let parsed = Parser.from_string (pprogram cle (fun x -> psite cle x false)) text |> flattenDict
|
||||
let expected = unbindingProgram |> flattenDict
|
||||
Assert.Equal<string>(print expected, print parsed)
|
||||
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Parsing - SG strand displacement rule")>]
|
||||
let parsingStrandDisplacementRuleTest() =
|
||||
let text = """
|
||||
junction(_!i, P) :-
|
||||
P = C [X!i E!j] [F!k X'!i],
|
||||
junction(E!j, F!k, P).
|
||||
|
||||
junction(E!j,F!j,_).
|
||||
|
||||
junction(E!j,F!k,Q):-
|
||||
Q = C [F!k] [G!l E'!j] [E!j],
|
||||
junction(G!l,F!k,Q).
|
||||
|
||||
strandDisplacementRule(P, Q) :-
|
||||
P = C [E!j D] [D!i] [D'!i E'!j],
|
||||
Q = C [E!j D!i] [D] [D'!i E'!j],
|
||||
junction(D!i, Q).
|
||||
"""
|
||||
|
||||
let parsed = Parser.from_string (pprogram cle (fun x -> psite cle x false)) text
|
||||
|> fun x -> x.Values
|
||||
|> Seq.concat
|
||||
|> Seq.toList
|
||||
let expected = strandDisplacementProgram
|
||||
|> fun x -> x.Values
|
||||
|> Seq.concat
|
||||
|> Seq.toList
|
||||
Assert.Equal<string>(print expected, print parsed)
|
||||
|
||||
|
||||
(* This case implements the branch migration rule for N junctions in the most general case possible. Because of this its implementation is rather convoluted, and uses experimental features like the C[[X]] construct, where X is a list of N patterns created dynamically, which encodes a context C[\pi_1] ... [\pi_N]. *)
|
||||
[<Fact(DisplayName="Logic DSD - Parsing - SG branch migration rule")>]
|
||||
let parsingBranchMigrationRule() =
|
||||
let text = """// create a pattern of the form [D!i1][D'!i1][D!i2][D'!i2] ... [D!iN][D'!iN]
|
||||
makeNHoles(D, D', [D!i; D'!i], [D!i], 1).
|
||||
makeNHoles(D, D', [D!i; D'!i # RestOfPatterns], [D!i # FreshBonds], N):-
|
||||
N > 1,
|
||||
M is N - 1,
|
||||
makeNHoles(D, D', RestOfPatterns, FreshBonds, M).
|
||||
|
||||
// turn [D!i1][D'!i1][D!i2][D'!i2] ... [D!iN][D'!iN] into [D!i1][D'!i2][D!i2][D'!i3] ... [D!iN][D'!i1]
|
||||
migrationPattern([D!i; D'!j], [D!i; D'!j]).
|
||||
migrationPattern([ D!i // 1
|
||||
; D'!j // 2
|
||||
; D!k // 3
|
||||
; D'!k // 4
|
||||
# RestOfStartingPattern ],
|
||||
[ D!i // 1
|
||||
; D'!k // 4
|
||||
# RestOfMigrationPattern ]) :-
|
||||
migrationPattern([ D!k // 3
|
||||
; D'!j // 2
|
||||
# RestOfStartingPattern],
|
||||
RestOfMigrationPattern).
|
||||
|
||||
findLoop(E!j, Q, Loop) :-
|
||||
// encoding of Q = C [(E@Start)!j] [(E'@End)!j]
|
||||
Q = C [E!j @ Start] [E'!j @ End],
|
||||
path(E!j, Start, End, Q, "any", [], [_ # Loop] (* discards E!j from the loop*)),
|
||||
not (Loop = []).
|
||||
|
||||
branchesOnly([]).
|
||||
branchesOnly([[E!j; _]; [E'!j; _] # Rest]) :-
|
||||
branchesOnly(Rest).
|
||||
|
||||
junctionPath(E!j, Q) :-
|
||||
findLoop(E!j, Q, Loop),
|
||||
branchesOnly(Loop).
|
||||
|
||||
checkAllAnchored([], Q).
|
||||
checkAllAnchored([D!i#Rest], Q) :-
|
||||
junctionPath(D!i, Q),
|
||||
checkAllAnchored(Rest, Q).
|
||||
|
||||
// perform N-way migration on D
|
||||
branchMigration(D, P, Q, N) :-
|
||||
unbound(D),
|
||||
compl(D, D'),
|
||||
makeNHoles(D, D', Junctions, FreshBonds, N),
|
||||
P = C[[Junctions]],
|
||||
migrationPattern(Junctions, MigratedJunctions),
|
||||
Q = C[[MigratedJunctions]],
|
||||
checkAllAnchored(FreshBonds, Q).
|
||||
|
||||
siteMatchesDomain(D!_, D).
|
||||
|
||||
countSitesInStrand(_, [], 0).
|
||||
countSitesInStrand(D, [Site # Rest], N) :-
|
||||
siteMatchesDomain(Site, D),
|
||||
countSitesInStrand(D, Rest, M),
|
||||
N is M + 1.
|
||||
countSitesInStrand(D, [Site # Rest], N) :-
|
||||
not siteMatchesDomain(Site, D),
|
||||
countSitesInStrand(D, Rest, N).
|
||||
|
||||
countSites(_, [], 0).
|
||||
countSites(D, [Strand # Rest], N) :-
|
||||
countSitesInStrand(D, Strand, X),
|
||||
countSites(D, Rest, Y),
|
||||
N is X + Y.
|
||||
|
||||
rangeTo(2,[2]).
|
||||
rangeTo(N, [N # Rest]) :-
|
||||
N > 2,
|
||||
M is N - 1,
|
||||
rangeTo(M, Rest).
|
||||
|
||||
getDomain(D, D) :- unbound(D).
|
||||
getDomain(D!_, D).
|
||||
|
||||
branchMigrationRule(P, Q) :-
|
||||
// get all the domains in P
|
||||
toDomains(P, DomainsList),
|
||||
|
||||
// pick a domain in P
|
||||
member(Domain, DomainsList),
|
||||
// optimization: search for junctions only on D domains, not on D* domains too
|
||||
not complementary(Domain),
|
||||
// get all strands in P
|
||||
toList(P, Strands),
|
||||
countSites(Domain, Strands, JunctionsCount),
|
||||
JunctionsCount >= 2,
|
||||
// create a list [2.. max number of junctions over D]
|
||||
rangeTo(JunctionsCount, Range),
|
||||
// pick a number N in that range
|
||||
member(N, Range),
|
||||
// perform branch migration over N branches on D
|
||||
branchMigration(Domain, P, Q, N)."""
|
||||
let parsed = Parser.from_string (pprogram cle (fun x -> psite cle x false)) text
|
||||
|> fun x -> x.Values
|
||||
|> Seq.concat
|
||||
|> Seq.toList
|
||||
|
||||
let otherProgs = junctionProgram @ hiddenProg |> Set.ofList
|
||||
let branchMP' = Set.difference (branchMigrationProgram |> flattenDict |> Set.ofList) otherProgs
|
||||
let expected = branchMP' |> Set.toList
|
||||
let y = print expected
|
||||
let x = print parsed
|
||||
Assert.Equal<string>(print expected, print parsed)
|
||||
|
||||
|
||||
(* Instance of the N-way branch migration rule *)
|
||||
[<Fact(DisplayName="Logic DSD - Parsing - SG 4-way branch migration rule")>]
|
||||
let parsing4wayBranchMigrationRule() =
|
||||
let text = """
|
||||
(* Encoding of the junction predicate using the path predicate *)
|
||||
findLoop(E!j, Q, Loop) :-
|
||||
// encoding of Q = C [(E@Start)!j] [(E'@End)!j]
|
||||
Q = C [E!j] [E'!j],
|
||||
pos(0, 0, C, Start),
|
||||
pos(1, 0, C, End),
|
||||
path(E!j, Start, End, Q, "any", [], [_ # Loop] (* discards E!j from the loop*)),
|
||||
not (Loop = []).
|
||||
|
||||
branchesOnly([]).
|
||||
branchesOnly([[E!j; _]; [E'!j; _] # Rest]) :-
|
||||
branchesOnly(Rest).
|
||||
|
||||
junction(E!j, Q) :-
|
||||
findLoop(E!j, Q, Loop),
|
||||
branchesOnly(Loop).
|
||||
|
||||
// perform N-way migration on D
|
||||
branchMigration(P, Q) :-
|
||||
P = C [D!i1] [D'!i1] [D!i2] [D'!i2],
|
||||
Q = C [D!i1] [D'!i2] [D!i2] [D'!i1],
|
||||
junction(D!i1, Q),
|
||||
junction(D!i2, Q).
|
||||
"""
|
||||
Parser.from_string (pprogram cle (fun x -> psite cle x false)) text
|
||||
|> ignore
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Resolution - locations")>]
|
||||
let testLocations() =
|
||||
let text = """
|
||||
testLocations(P, X, Y, Z) :-
|
||||
P = C1 [a!I@X],
|
||||
P = C2 [_@X _@Y],
|
||||
P = C3 [e@Z].
|
||||
"""
|
||||
|
||||
let provider = makeProvider ()
|
||||
let ps = psite cle provider true
|
||||
let strands = Parser.from_string (psystem ps)"<d a!1 b!2> | <c!3 e> | <c*!3 b*!2 a*!1>"
|
||||
|
||||
let program = Parser.from_string (pprogram cle (fun x -> psite cle x false)) text
|
||||
let query = Pos (Pred("testLocations", [Proc strands; Term.Var (0, "X"); Term.Var (1, "Y"); Term.Var (2, "Z")]))
|
||||
|
||||
let theta = match resolve query program cle with
|
||||
| Some s -> s
|
||||
| None -> failwith "Strand displacement rule failed."
|
||||
|
||||
let x = theta.Apply (Term.Var (0, "X"), cle)
|
||||
let y = theta.Apply (Term.Var (1, "Y"), cle)
|
||||
let z = theta.Apply (Term.Var (2, "Z"), cle)
|
||||
Assert.Equal(Term.Pat <| Pattern.Inner[SiteT.Var (-1, "_"), Location.Loc (0,1)], x)
|
||||
Assert.Equal(Term.Pat <| Pattern.Inner[SiteT.Var (-1, "_"), Location.Loc (0,2)], y)
|
||||
Assert.Equal(Term.Pat <| Pattern.Inner[SiteT.Var (-1, "_"), Location.Loc (1,1)], z)
|
||||
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Parsing - Indeterminate list")>]
|
||||
let testIndetList () =
|
||||
let provider1 = makeProvider ()
|
||||
let ts1 = psite cle provider1 false
|
||||
let actualT = from_string (pterm ts1 cle provider1 engine.domainKeywords) "[Q # V]"
|
||||
let provider2 = makeProvider ()
|
||||
let ts2 = psite cle provider2 false
|
||||
let q = from_string (pterm ts2 cle provider2 engine.domainKeywords) "Q"
|
||||
let v = from_string (pterm ts2 cle provider2 engine.domainKeywords) "V"
|
||||
let expectedT = TCons(q, v)
|
||||
Assert.Equal(expectedT, actualT)
|
||||
|
||||
let provider3 = makeProvider ()
|
||||
let ts3 = psite cle provider3 false
|
||||
let actualP = from_string (ppredicate cle ts3 provider3 engine.domainKeywords) "rule(\"loop\", P, Q, R, [Q # V])"
|
||||
let provider4 = makeProvider ()
|
||||
let ts4 = psite cle provider4 false
|
||||
let pt = from_string (pterm ts4 cle provider4 engine.domainKeywords)
|
||||
let p = pt "P"
|
||||
let q = pt "Q"
|
||||
let r = pt "R"
|
||||
let v = pt "V"
|
||||
let expectedP = Pred("rule", [Const "loop"; p; q; r; TCons(q, v)])
|
||||
Assert.Equal(expectedP |> Predicate.ToStringWith cle |> removeVarNumbers,
|
||||
actualP |> Predicate.ToStringWith cle |> removeVarNumbers)
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Parsing - Domain")>]
|
||||
let testDom () =
|
||||
let provider = makeProvider ()
|
||||
let ts = psite cle provider false
|
||||
let actualT = from_string (pterm ts cle provider engine.domainKeywords) """a!i"""
|
||||
let expectedT = Term.Pat
|
||||
(Pattern.Inner
|
||||
[SiteT.Site
|
||||
(Site.Bound
|
||||
(DomainT.Dom(Domain.Create("a", false, false))
|
||||
, Bond.Var (provider "i"))), Location.Var (-1,"_")])
|
||||
Assert.Equal(expectedT |> Term.ToString |> removeVarNumbers,
|
||||
actualT |> Term.ToString |> removeVarNumbers)
|
||||
|
||||
[<Fact(DisplayName="Logic DSD - Parsing - Domain tags")>]
|
||||
let testTags () =
|
||||
let provider = makeProvider ()
|
||||
let ts = psite cle provider false
|
||||
let actualT = from_string (pterm ts cle provider engine.domainKeywords) """A {tethered("x","y","z")}!i"""
|
||||
let expectedT = Term.Pat
|
||||
(Pattern.Inner
|
||||
[SiteT.Site
|
||||
(Site.Bound
|
||||
(DomainT.Var(provider "A", Tag <| Term.Func("tethered", [Const "x"; Const"y"; Const"z"]))
|
||||
, Bond.Var (provider "i"))), Location.Var (-1,"_")])
|
||||
Assert.Equal(expectedT |> Term.ToString |> removeVarNumbers,
|
||||
actualT |> Term.ToString |> removeVarNumbers)
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic Engine - Parsing - Expressions")>]
|
||||
let testArithmetics () =
|
||||
let provider = makeProvider ()
|
||||
let ts = psite cle provider false
|
||||
let actualT = from_string (pterm ts cle provider engine.domainKeywords) """N + 1 - 2 * X"""
|
||||
let n : Var = (0, "N")
|
||||
let x : Var = (1, "X")
|
||||
let t1 = Term.Func("_Plus", [Term.Func("_key", [Term.Var n]); Term.Float 1.0 ])
|
||||
let t2 = Term.Func("_Times", [Term.Float 2.0; Term.Func("_key", [ Term.Var x ]) ])
|
||||
let expectedT = Term.Func("_Minus", [t1; t2])
|
||||
Assert.Equal(expectedT |> Term.ToString |> removeVarNumbers,
|
||||
actualT |> Term.ToString |> removeVarNumbers)
|
||||
|
||||
let sub = Substitution<SiteT, unit>.Create(n, Term.Float 4.0).Add(TVar x, Term.Float 2.0, CLE.empty)
|
||||
let t' = Substitution.Apply(sub, actualT, CLE.empty)
|
||||
let exp' = Term.ToExpression t'
|
||||
let res = exp' |> Microsoft.Research.CRNEngine.Expression.eval (fun t -> match t with Term.Float n -> n | _ -> failwith "Substitution application failed")
|
||||
Assert.Equal(1.0, res)
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic Engine - Parsing - Predicates")>]
|
||||
let testPreds () =
|
||||
let provider = makeProvider ()
|
||||
let ts = psite cle provider false
|
||||
let n : Var = (0, "N")
|
||||
let x : Var = (1, "X")
|
||||
|
||||
let actualT = from_string (ppredicate cle ts provider engine.domainKeywords) """N is 1"""
|
||||
let t1 = Term.Float 1.0
|
||||
let expectedT = Predicate.Pred("is", [Term.Var n; t1 ])
|
||||
Assert.Equal(expectedT |> Predicate<_>.ToString |> removeVarNumbers,
|
||||
actualT |> Predicate<_>.ToString |> removeVarNumbers)
|
||||
|
||||
let actualT = from_string (ppredicate cle ts provider engine.domainKeywords) """N is X + 1"""
|
||||
let t1 = Term.Func("_Plus", [Term.Func("_key", [Term.Var x]); Term.Float 1.0 ])
|
||||
let expectedT = Predicate.Pred("is", [Term.Var n; t1 ])
|
||||
Assert.Equal(expectedT |> Predicate<_>.ToString |> removeVarNumbers,
|
||||
actualT |> Predicate<_>.ToString |> removeVarNumbers)
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic Engine - Parsing - Clauses")>]
|
||||
let testClauses () =
|
||||
let provider = makeProvider ()
|
||||
let ts x = psite cle x false
|
||||
let p : Var = (0, "P")
|
||||
let q : Var = (1, "Q")
|
||||
let r : Var = (2, "Rate")
|
||||
|
||||
let actualT = from_string (pclause engine ts makeProvider) """reaction([P], Rate, Q) :- Rate is 1."""
|
||||
let expectedT =
|
||||
Clause.Create(
|
||||
Predicate.Pred("reaction", [Term.TList [Term.Var p]; Term.Var r; Term.Var q ]),
|
||||
[ Pos <| Predicate.Pred("is", [Term.Var r; Float 1.0 ]) ] )
|
||||
Assert.Equal(expectedT |> Clause<_>.ToStringWith engine |> removeVarNumbers,
|
||||
actualT |> Clause<_>.ToStringWith engine |> removeVarNumbers)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic Engine - Parsing - CRNs")>]
|
||||
let testCrn () =
|
||||
let provider = makeProvider ()
|
||||
let ts = Parser.plookAhead (pname >>= fun x -> if x.Length > 0 && (x = "_" || System.Char.IsUpper (x.Chars 0)) then Parser.failParser "" else preturn ()) >>. pname
|
||||
|
||||
// Single reaction CRN
|
||||
let actualT = from_string (pterm ts CLE.empty provider engine.domainKeywords) """{ X -> Y }"""
|
||||
let expectedT = Term.Func ("_rxn", [ Term.TMSet []
|
||||
; Term.TMSet([1, Term.Var (0, "X")])
|
||||
; Term.Func("_massActionRate", [Term.Float 1.0])
|
||||
; Term.Func("",[])
|
||||
; Term.TMSet([1, Term.Var (1, "Y")])
|
||||
])
|
||||
|> List.singleton
|
||||
|> Term.TCRN
|
||||
Assert.Equal(expectedT |> Term.ToString |> removeVarNumbers,
|
||||
actualT |> Term.ToString |> removeVarNumbers)
|
||||
|
||||
|
||||
// Mass action rate
|
||||
let actualT = from_string (pterm ts CLE.empty provider engine.domainKeywords) """{ X ->{k} Y }"""
|
||||
let expectedT = Term.Func ("_rxn", [ Term.TMSet []
|
||||
; Term.TMSet [1, Term.Var (0, "X")]
|
||||
; Term.Func("_massActionRate", [Term.Func("_key", [Term.Pat (Pattern.Inner ["k", Location.Var (-1, "_")]) ]) ])
|
||||
; Term.Func("",[])
|
||||
; Term.TMSet [1, Term.Var (1, "Y")]
|
||||
])
|
||||
|> List.singleton
|
||||
|> Term.TCRN
|
||||
Assert.Equal(expectedT |> Term.ToString |> removeVarNumbers,
|
||||
actualT |> Term.ToString |> removeVarNumbers)
|
||||
|
||||
// Functional rate
|
||||
let actualT = from_string (pterm ts CLE.empty provider engine.domainKeywords) """{ X ->[[k]] Y }"""
|
||||
let expectedT = Term.Func ("_rxn", [ Term.TMSet []
|
||||
; Term.TMSet [1, Term.Var (0, "X")]
|
||||
; Term.Func("_functionalRate", [Term.Func("_key", [Term.Pat (Pattern.Inner ["k", Location.Var (-1, "_")]) ]) ])
|
||||
; Term.Func("",[])
|
||||
; Term.TMSet [1, Term.Var (1, "Y")]
|
||||
])
|
||||
|> List.singleton
|
||||
|> Term.TCRN
|
||||
Assert.Equal(expectedT |> Term.ToString |> removeVarNumbers,
|
||||
actualT |> Term.ToString |> removeVarNumbers)
|
||||
|
||||
// Ground reaction
|
||||
let actualT = from_string (pterm ts CLE.empty provider engine.domainKeywords) """{ a ->{k} b }"""
|
||||
let expectedT = Term.Func ("_rxn", [ Term.TMSet []
|
||||
; Term.TMSet [1, Term.Pat (Pattern.Inner ["a", Location.Var (-1, "_")]) ]
|
||||
; Term.Func("_massActionRate", [Term.Func("_key", [Term.Pat (Pattern.Inner ["k", Location.Var (-1, "_")]) ]) ])
|
||||
; Term.Func("",[])
|
||||
; Term.TMSet [1, Term.Pat (Pattern.Inner ["b", Location.Var (-1, "_")]) ]
|
||||
])
|
||||
|> List.singleton
|
||||
|> Term.TCRN
|
||||
Assert.Equal(expectedT |> Term.ToString |> removeVarNumbers,
|
||||
actualT |> Term.ToString |> removeVarNumbers)
|
||||
|
||||
// multisets
|
||||
let actualT = from_string (pterm ts CLE.empty provider engine.domainKeywords) """{ 2a + 3b ->{k} c + 4d}"""
|
||||
let expectedT = Term.Func ("_rxn", [ Term.TMSet []
|
||||
; Term.TMSet [ 2, Term.Pat (Pattern.Inner ["a", Location.Var (-1, "_")])
|
||||
; 3, Term.Pat (Pattern.Inner ["b", Location.Var (-1, "_")]) ]
|
||||
; Term.Func("_massActionRate", [Term.Func("_key", [Term.Pat (Pattern.Inner ["k", Location.Var (-1, "_")]) ]) ])
|
||||
; Term.Func("",[])
|
||||
; Term.TMSet [1, Term.Pat (Pattern.Inner ["c", Location.Var (-1, "_")])
|
||||
4, Term.Pat (Pattern.Inner ["d", Location.Var (-1, "_")]) ]
|
||||
])
|
||||
|> List.singleton
|
||||
|> Term.TCRN
|
||||
Assert.Equal(expectedT |> Term.ToString |> removeVarNumbers,
|
||||
actualT |> Term.ToString |> removeVarNumbers)
|
||||
|
||||
|
||||
// catalytic reaction
|
||||
let actualT = from_string (pterm ts CLE.empty provider engine.domainKeywords) """{ a ~ b ->{k} c }"""
|
||||
let expectedT = Term.Func ("_rxn", [ Term.TMSet [1, Term.Pat (Pattern.Inner ["a", Location.Var (-1, "_")]) ]
|
||||
; Term.TMSet [1, Term.Pat (Pattern.Inner ["b", Location.Var (-1, "_")]) ]
|
||||
; Term.Func("_massActionRate", [Term.Func("_key", [Term.Pat (Pattern.Inner ["k", Location.Var (-1, "_")]) ]) ])
|
||||
; Term.Func("",[])
|
||||
; Term.TMSet [1, Term.Pat (Pattern.Inner ["c", Location.Var (-1, "_")]) ]
|
||||
])
|
||||
|> List.singleton
|
||||
|> Term.TCRN
|
||||
Assert.Equal(expectedT |> Term.ToString |> removeVarNumbers,
|
||||
actualT |> Term.ToString |> removeVarNumbers)
|
||||
|
||||
// reversible reaction
|
||||
let actualT = from_string (pterm ts CLE.empty provider engine.domainKeywords) """{ a <->{k}[[l]] b }"""
|
||||
let expectedT = Term.Func ("_rxn", [ Term.TMSet []
|
||||
; Term.TMSet [1, Term.Pat (Pattern.Inner ["a", Location.Var (-1, "_")]) ]
|
||||
; Term.Func("_massActionRate", [Term.Func("_key", [Term.Pat (Pattern.Inner ["k", Location.Var (-1, "_")]) ]) ])
|
||||
; Term.Func("_functionalRate", [Term.Func("_key", [Term.Pat (Pattern.Inner ["l", Location.Var (-1, "_")]) ]) ])
|
||||
; Term.TMSet [1, Term.Pat (Pattern.Inner ["b", Location.Var (-1, "_")]) ]
|
||||
])
|
||||
|> List.singleton
|
||||
|> Term.TCRN
|
||||
Assert.Equal(expectedT |> Term.ToString |> removeVarNumbers,
|
||||
actualT |> Term.ToString |> removeVarNumbers)
|
||||
|
||||
// rate expression
|
||||
let actualT = from_string (pterm ts CLE.empty provider engine.domainKeywords) """{ a ->{k + 2 * X} b }"""
|
||||
let expectedT = Term.Func ("_rxn", [ Term.TMSet []
|
||||
; Term.TMSet [1, Term.Pat (Pattern.Inner ["a", Location.Var (-1, "_")]) ]
|
||||
; Term.Func("_massActionRate", [Term.Func("_Plus", [ Term.Func("_key", [Term.Pat (Pattern.Inner ["k", Location.Var (-1, "_")]) ])
|
||||
; Term.Func("_Times", [Term.Float 2.0 ; Term.Func("_key", [Term.Var (0, "X")])]) ]) ])
|
||||
; Term.Func("",[])
|
||||
; Term.TMSet [1, Term.Pat (Pattern.Inner ["b", Location.Var (-1, "_")]) ]
|
||||
])
|
||||
|> List.singleton
|
||||
|> Term.TCRN
|
||||
Assert.Equal(expectedT |> Term.ToString |> removeVarNumbers,
|
||||
actualT |> Term.ToString |> removeVarNumbers)
|
||||
|
||||
// multiple reactions
|
||||
let actualT = from_string (pterm ts CLE.empty provider engine.domainKeywords) """{ | a ->{k + 2 * X} b
|
||||
| c ->[log([z])] 2d + 3e}"""
|
||||
let reaction1 = Term.Func ("_rxn", [ Term.TMSet []
|
||||
; Term.TMSet [1, Term.Pat (Pattern.Inner ["a", Location.Var (-1, "_")]) ]
|
||||
; Term.Func("_massActionRate", [Term.Func("_Plus", [ Term.Func("_key", [Term.Pat (Pattern.Inner ["k", Location.Var (-1, "_")]) ])
|
||||
; Term.Func("_Times", [Term.Float 2.0 ; Term.Func("_key", [Term.Var (0, "X")])]) ]) ])
|
||||
; Term.Func("",[])
|
||||
; Term.TMSet [1, Term.Pat (Pattern.Inner ["b", Location.Var (-1, "_")]) ] ])
|
||||
let reaction2 = Term.Func ("_rxn", [ Term.TMSet []
|
||||
; Term.TMSet [1, Term.Pat (Pattern.Inner ["c", Location.Var (-1, "_")]) ]
|
||||
; Term.Func("_functionalRate", [Term.Func("_Log", [ Term.Func("_key", [Term.Pat (Pattern.Inner ["z", Location.Var (-1, "_")]) ]) ]) ])
|
||||
; Term.Func("",[])
|
||||
; Term.TMSet [2, Term.Pat (Pattern.Inner ["d", Location.Var (-1, "_")])
|
||||
3, Term.Pat (Pattern.Inner ["e", Location.Var (-1, "_")]) ] ])
|
||||
let expectedT = Term.TCRN [ reaction1; reaction2 ]
|
||||
|
||||
Assert.Equal(expectedT |> Term.ToString |> removeVarNumbers,
|
||||
actualT |> Term.ToString |> removeVarNumbers)
|
||||
Разница между файлами не показана из-за своего большого размера
Загрузить разницу
|
|
@ -0,0 +1,192 @@
|
|||
module RulesDSD.UnificationTests
|
||||
|
||||
open FsUnit
|
||||
open Xunit
|
||||
open FsUnit.Xunit
|
||||
|
||||
open RulesDSD.Syntax
|
||||
open RulesDSD.Unification
|
||||
open Microsoft.Research.DNA.LogicDSD
|
||||
|
||||
let X = Term.Var (0, "X")
|
||||
let Y = Term.Var (1, "Y")
|
||||
let Z = Term.Var (2, "Z")
|
||||
|
||||
let cle = Microsoft.Research.DNA.LogicDSD.engine
|
||||
|
||||
[<Fact(DisplayName="Logic Engine - Unification - var/const")>]
|
||||
let varConst() =
|
||||
let eqs = [TEq (X, Const "c")]
|
||||
let sol = match unify cle eqs with
|
||||
| [theta] -> theta
|
||||
| _ -> failwith "Unification failed"
|
||||
Assert.Equal(Const "c", sol.Apply(X, cle))
|
||||
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic Engine - Unification - var/func")>]
|
||||
let varFunc () =
|
||||
let eqs = [TEq (X, Func("f", [Const "c"; Y]) )]
|
||||
let sol = match unify cle eqs with
|
||||
| [theta] -> theta
|
||||
| _ -> failwith "Unification failed"
|
||||
Assert.Equal(Func("f", [Const "c"; Y]), sol.Apply(X, cle))
|
||||
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic Engine - Unification - func/func")>]
|
||||
let funcFunc () =
|
||||
let eqs = [TEq (Func ("f", [X; Float 1.0]), Func("f", [Const "c"; Y]) )]
|
||||
let sol = match unify cle eqs with
|
||||
| [theta] -> theta
|
||||
| _ -> failwith "Unification failed"
|
||||
Assert.Equal(Const "c", sol.Apply(X, cle))
|
||||
Assert.Equal(Float 1.0, sol.Apply(Y, cle))
|
||||
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic Engine - Unification - mixed")>]
|
||||
let mixed() =
|
||||
let eqs = [ TEq (Func ("f", [X; Z]), Func("f", [Y; Const "2"]) );
|
||||
TEq (X, Const "c")]
|
||||
let sol = match unify cle eqs with
|
||||
| [theta] -> theta
|
||||
| _ -> failwith "Unification failed"
|
||||
Assert.Equal(Const "c", sol.Apply (X, cle))
|
||||
Assert.Equal(Const "c", sol.Apply (Y, cle))
|
||||
Assert.Equal(Const "2", sol.Apply (Z, cle))
|
||||
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic Engine - Unification - fibonacci")>]
|
||||
let fibonacci() =
|
||||
let eqs = [TEq (Func("fib", [X; Float 1.0]), Func("fib", [Float 0.0; Float 1.0]) )]
|
||||
let sol = match unify cle eqs with
|
||||
| [theta] -> theta
|
||||
| _ -> failwith "Unification failed"
|
||||
Assert.Equal(Float 0.0, sol.Apply(X,cle))
|
||||
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic Engine - Unification - nicking pattern matching")>]
|
||||
let nick() =
|
||||
let domA = Dom {name = "a"; isComplementary = false; isToehold = false; tag = NoTag}
|
||||
let domB = Dom {name = "b"; isComplementary = false; isToehold = false; tag = NoTag}
|
||||
let a = Site (Unbound domA), Location.Var (-1, "_")
|
||||
let b = Site (Unbound domB), Location.Var (-1, "_")
|
||||
let p1 = Pat (Nicking ([SiteT.Var (0, "X"), Location.Var (-1, "_")],[b]))
|
||||
let p2 = Pat (Nicking ([a],[SiteT.Var (1, "Y"), Location.Var (-1, "_")]))
|
||||
let eqs = [TEq (p1, p2)]
|
||||
let sol = match unify cle eqs with
|
||||
| [theta] -> theta
|
||||
| sub -> failwith "Unification failed"
|
||||
Assert.Equal(a, sol.Apply(((SiteT.Var (0, "X")), Location.Var (-1, "_")), cle))
|
||||
Assert.Equal(b, sol.Apply(((SiteT.Var (1, "Y")), Location.Var (-1, "_")), cle))
|
||||
|
||||
|
||||
|
||||
|
||||
[<Fact(DisplayName="Logic Engine - Unification - Multi-sets")>]
|
||||
let mset1() =
|
||||
let t1 : Term<unit> = Term.TMSet [1, Term.Const "A"; 2, Term.Const "B"]
|
||||
let t2 : Term<unit> = Term.TMSet [2, Term.Const "B"; 1, Term.Const "A"]
|
||||
match unify CLE.empty [TEq (t1, t2)] with
|
||||
| [theta] -> if theta <> Substitution.Substitution.id then failwith "Unification failed (1.1)"
|
||||
| sub -> failwith "Unification failed (1)"
|
||||
|
||||
let t1 : Term<unit> = Term.TMSet [1, Term.Const "A"; 2, Term.Const "B"]
|
||||
let t2 : Term<unit> = Term.TMSet [2, Term.Const "B"; 1, Term.Var (1, "X")]
|
||||
match unify CLE.empty [TEq (t1, t2)] with
|
||||
| [theta] -> Assert.Equal(Term.Const "A", theta.Apply(Term.Const "A", CLE<unit,unit>.empty))
|
||||
| sub -> failwith "Unification failed (2)"
|
||||
|
||||
let t1 = Term.TMSet [1, Term.Const "A"; 2, Term.Const "B"]
|
||||
let t2 = Term.TMSet [1, Term.Var (1, "X"); 1, Term.Const "A"; 1, Term.Var(1, "Y")]
|
||||
match unify CLE.empty [TEq (t1, t2)] with
|
||||
| [theta] -> Assert.Equal(Term.Const "B", theta.Apply(Term.Var (1, "X"), CLE<unit,unit>.empty))
|
||||
Assert.Equal(Term.Const "B", theta.Apply(Term.Var (1, "Y"), CLE<unit,unit>.empty))
|
||||
| sub -> failwith "Unification failed (3)"
|
||||
|
||||
()
|
||||
|
||||
[<Fact(DisplayName="Logic Engine - Unification - CRNs")>]
|
||||
let crn1() =
|
||||
// test 1
|
||||
let crn1 = Term.TCRN [
|
||||
// A + B -> 2C
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "A"; 1, Term.Const "B"]; Term.Const "k"; Term.TMSet [2, Term.Const "C"] ]);
|
||||
]
|
||||
let crn2 = Term.TCRN [
|
||||
// B + A -> 2C
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "B"; 1, Term.Const "A"]; Term.Const "k"; Term.TMSet [2, Term.Const "C"] ]);
|
||||
]
|
||||
match unify CLE.empty [TEq (crn1, crn2)] with
|
||||
| [theta] -> if theta <> Substitution.Substitution.id then failwith "Unification failed (1.1)"
|
||||
| sub -> failwith "Unification failed (1)"
|
||||
|
||||
// test 2
|
||||
let crn1 = Term.TCRN [
|
||||
// A + B -> 2C
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "A"; 1, Term.Const "B"]; Term.Const "k"; Term.TMSet [2, Term.Const "C"] ]);
|
||||
]
|
||||
let crn2 = Term.TCRN [
|
||||
// B + A -> X
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "B"; 1, Term.Const "A"]; Term.Const "k"; Term.Var(-1, "X") ]);
|
||||
]
|
||||
match unify CLE.empty [TEq (crn1, crn2)] with
|
||||
| [theta] -> Assert.Equal(Term.TMSet [2, Term.Const "C"], theta.Apply(Term.Var(-1, "X"), CLE<unit,unit>.empty))
|
||||
| sub -> failwith "Unification failed (1)"
|
||||
|
||||
// test 3: multiple ground reactions
|
||||
let crn1 = Term.TCRN [
|
||||
// A + B -> 2C
|
||||
// C -> 2A + B
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "A"; 1, Term.Const "B"]; Term.Const "k1"; Term.TMSet [2, Term.Const "C"] ])
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "C"]; Term.Const "k2"; Term.TMSet [2, Term.Const "A"; 1, Term.Const "B"] ]) ]
|
||||
let crn2 = Term.TCRN [
|
||||
// C -> B + 2A
|
||||
// B + A -> 2C
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "C"]; Term.Const "k2"; Term.TMSet [1, Term.Const "B"; 2, Term.Const "A"] ])
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "B"; 1, Term.Const "A"]; Term.Const "k1"; Term.TMSet [2, Term.Const "C" ] ]) ]
|
||||
|
||||
match unify CLE.empty [TEq (crn1, crn2)] with
|
||||
| [theta] -> if theta <> Substitution.Substitution.id then failwith "Unification failed (3.1)"
|
||||
| sub -> failwith "Unification failed (3)"
|
||||
|
||||
// test 4: multiple reactions with variables, 1 possible solution
|
||||
let crn1 = Term.TCRN [
|
||||
// A + B -> 2C
|
||||
// C -> 2A + B
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "A"; 1, Term.Const "B"]; Term.Const "k1"; Term.TMSet [2, Term.Const "C"] ])
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "C"]; Term.Const "k2"; Term.TMSet [2, Term.Const "A"; 1, Term.Const "B"] ]) ]
|
||||
let crn2 = Term.TCRN [
|
||||
// C -> B + 2A
|
||||
// B + A -> 2C
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "C"]; Term.Const "k2"; Term.TMSet [1, Term.Const "B"; 2, Term.Var (2, "Y")] ])
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "B"; 1, Term.Var (1, "X")]; Term.Const "k1"; Term.TMSet [2, Term.Const "C" ] ]) ]
|
||||
|
||||
match unify CLE.empty [TEq (crn1, crn2)] with
|
||||
| [theta] -> Assert.Equal(Term.Const "A", theta.Apply(Term.Var(1, "X"), CLE<unit,unit>.empty))
|
||||
Assert.Equal(Term.Const "A", theta.Apply(Term.Var(2, "Y"), CLE<unit,unit>.empty))
|
||||
| sub -> failwith "Unification failed (4)"
|
||||
|
||||
// test 5: multiple reactions with variables, many possible solutions
|
||||
let crn1 = Term.TCRN [
|
||||
// A + B -> 2C
|
||||
// C -> 2A + B
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "A"; 1, Term.Const "B"]; Term.Const "k1"; Term.TMSet [2, Term.Const "C"] ])
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "C"]; Term.Const "k2"; Term.TMSet [2, Term.Const "A"; 1, Term.Const "B"] ]) ]
|
||||
let crn2 = Term.TCRN [
|
||||
// C -> B + 2A
|
||||
// B + A -> 2C
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Const "C"]; Term.Const "k2"; Term.TMSet [1, Term.Const "B"; 2, Term.Var (3, "Z")] ])
|
||||
Term.Func("_rxn", [Term.TMSet [1, Term.Var (1, "X"); 1, Term.Var (2, "Y")]; Term.Const "k1"; Term.TMSet [2, Term.Const "C" ] ]) ]
|
||||
|
||||
match unify CLE.empty [TEq (crn1, crn2)] with
|
||||
| [theta1; theta2] -> let sol1 = [theta1.Apply(Term.Var(1, "X"), CLE<unit,unit>.empty); theta1.Apply(Term.Var(2, "Y"), CLE<unit,unit>.empty)]
|
||||
let sol2 = [theta2.Apply(Term.Var(2, "Y"), CLE<unit,unit>.empty); theta2.Apply(Term.Var(1, "X"), CLE<unit,unit>.empty)]
|
||||
let x = sol1 = sol2
|
||||
Assert.True(x)
|
||||
|
||||
| sub -> failwith "Unification failed (5)"
|
||||
()
|
||||
Загрузка…
Ссылка в новой задаче