diff options
| author | Inari Listenmaa <inari.listenmaa@gmail.com> | 2018-05-22 11:49:42 +0100 |
|---|---|---|
| committer | Inari Listenmaa <inari.listenmaa@gmail.com> | 2018-05-22 11:49:42 +0100 |
| commit | 10df5a7269721ab0807ec7a0fe4b75cd1bb16d87 (patch) | |
| tree | c9921a1064486db3478e42c37e3c453aa3042342 | |
| parent | b635cb3d5208478097b5dfd8e2476aef857e96c9 (diff) | |
(gftest) Multiple concrete categories for context generation
| -rw-r--r-- | src/tools/gftest/Grammar.hs | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/tools/gftest/Grammar.hs b/src/tools/gftest/Grammar.hs index f8c507acd..4e6d0c6e9 100644 --- a/src/tools/gftest/Grammar.hs +++ b/src/tools/gftest/Grammar.hs @@ -990,10 +990,7 @@ testFun debug gr trans startcat funname = if debug then tp { ctyp = (fst $ ctyp tp, coe)} else tp ] - -- Usually start category is a single {s:Str}, i.e. only one concrete category. - -- If you try this out for start categories with more parameters and fields, - -- you probably get wrong or missing results. - (start:_) = ccats gr startcat + starts = ccats gr startcat hl f c1 c2 = f (c1 dummyHole) == f (c2 dummyHole) -- applyHole = hl id -- TODO why doesn't this work for equality of contexts? @@ -1007,16 +1004,18 @@ testFun debug gr trans startcat funname = [ (goalcat,(testcase,ctxs)) | testcase <- treesUsingFun gr funs , let goalcat = ccatOf testcase -- never a coercion (coercions can't be goals) - , let ctxs = contextsFor gr start goalcat ] :: M.Map ConcrCat (Tree,[Tree->Tree]) + , let ctxs = [ ctx | st <- starts + , ctx <- contextsFor gr st goalcat ] + ] :: M.Map ConcrCat (Tree,[Tree->Tree]) goalcats = M.keys cat_testcase_ctxs coercion_goalcats_commonCtxs = [ (coe,coveredGoalcats,ctxs) | coe@(CC Nothing _) <- S.toList $ nonEmptyCats gr -- only coercions , let coveredGoalcats = filter (coerces gr coe) goalcats - , let ctxs = [ ctx -- Contexts that have - | ctx <- contextsFor gr start coe -- a) hole of coercion, and are - , any (applyHole ctx) allCtxs ] -- b) relevant for the function we test + , let ctxs = [ ctx | st <- starts -- Contexts that have + , ctx <- contextsFor gr st coe -- a) hole of coercion, and are + , any (applyHole ctx) allCtxs ] -- b) relevant for the function we test , length coveredGoalcats >= 2 -- no use if the coercion covers 0 or 1 categories , not $ null ctxs ] |