joshua/nominal-lstar
1
Fork 0
mirror of https://github.com/Jaxan/nominal-lstar.git synced 2025-04-28 07:07:46 +02:00
Code Issues Releases Activity

Optimization of incompleteness function.

Browse source
This commit is contained in:
Michał Szynwelski 2016-06-17 13:23:14 +02:00
parent c3c6645039
commit fbcba8c580
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Main.hs
View file

@ -19,8 +19,9 @@ import Prelude hiding (and, curry, filter, lookup, map, not,
incompleteness :: NominalType i => State i -> Set [i] incompleteness :: NominalType i => State i -> Set [i]
incompleteness State{..} = filter (not . hasEqRow) ssa incompleteness State{..} = filter (not . hasEqRow) ssa
where where
sss = map (row t) ss
-- true if the sequence sa has an equivalent row in ss -- true if the sequence sa has an equivalent row in ss
hasEqRow sa = exists (\s2 -> eq (row t sa) (row t s2)) ss hasEqRow = contains sss . row t
-- We can determine its consistency with the following -- We can determine its consistency with the following
-- Returns equivalent rows (fst) with all inequivalent extensions (snd) -- Returns equivalent rows (fst) with all inequivalent extensions (snd)