mirror of
https://github.com/Smaug123/FicroKanSharp
synced 2025-10-21 18:58:39 +00:00
Add Goal.all and Goal.any
This commit is contained in:
2
FicroKanSharp.Test/TestTypedMatch.fs
Normal file
2
FicroKanSharp.Test/TestTypedMatch.fs
Normal file
@@ -0,0 +1,2 @@
|
|||||||
|
module FicroKanSharp.Test.TestTypedMatch
|
||||||
|
|
@@ -18,10 +18,20 @@ module Goal =
|
|||||||
let equiv (term1 : Term) (term2 : Term) : Goal = Goal.Equiv (term1, term2)
|
let equiv (term1 : Term) (term2 : Term) : Goal = Goal.Equiv (term1, term2)
|
||||||
|
|
||||||
let never : Goal =
|
let never : Goal =
|
||||||
equiv (Term.Symbol ("_internal", [])) (Term.Symbol ("_internal", [ Term.Symbol ("_internal", []) ]))
|
equiv (Term.Symbol ("_never", [])) (Term.Symbol ("_never2", []))
|
||||||
|
|
||||||
let always : Goal =
|
let always : Goal =
|
||||||
equiv (Term.Symbol ("_internal", [])) (Term.Symbol ("_internal", []))
|
equiv (Term.Symbol ("_always", [])) (Term.Symbol ("_always", []))
|
||||||
|
|
||||||
|
let all (goals : Goal list) : Goal =
|
||||||
|
match goals with
|
||||||
|
| [] -> always
|
||||||
|
| goal :: goals -> goals |> List.fold conj goal
|
||||||
|
|
||||||
|
let any (goals : Goal list) : Goal =
|
||||||
|
match goals with
|
||||||
|
| [] -> never
|
||||||
|
| goal :: goals -> goals |> List.fold disj goal
|
||||||
|
|
||||||
let private walk (u : Term) (s : State) : Term =
|
let private walk (u : Term) (s : State) : Term =
|
||||||
match u with
|
match u with
|
||||||
|
Reference in New Issue
Block a user