From 3a68c25ae00ca7d57769a969fef62f01900dfac2 Mon Sep 17 00:00:00 2001 From: Smaug123 Date: Sun, 26 Dec 2021 22:53:37 +0000 Subject: [PATCH] Add Goal.all and Goal.any --- FicroKanSharp.Test/TestTypedMatch.fs | 2 ++ FicroKanSharp/Goal.fs | 14 ++++++++++++-- 2 files changed, 14 insertions(+), 2 deletions(-) create mode 100644 FicroKanSharp.Test/TestTypedMatch.fs diff --git a/FicroKanSharp.Test/TestTypedMatch.fs b/FicroKanSharp.Test/TestTypedMatch.fs new file mode 100644 index 0000000..e2cb7c0 --- /dev/null +++ b/FicroKanSharp.Test/TestTypedMatch.fs @@ -0,0 +1,2 @@ +module FicroKanSharp.Test.TestTypedMatch + diff --git a/FicroKanSharp/Goal.fs b/FicroKanSharp/Goal.fs index aff355c..1929bc1 100644 --- a/FicroKanSharp/Goal.fs +++ b/FicroKanSharp/Goal.fs @@ -18,10 +18,20 @@ module Goal = let equiv (term1 : Term) (term2 : Term) : Goal = Goal.Equiv (term1, term2) let never : Goal = - equiv (Term.Symbol ("_internal", [])) (Term.Symbol ("_internal", [ Term.Symbol ("_internal", []) ])) + equiv (Term.Symbol ("_never", [])) (Term.Symbol ("_never2", [])) 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 = match u with