From 10df5a7269721ab0807ec7a0fe4b75cd1bb16d87 Mon Sep 17 00:00:00 2001 From: Inari Listenmaa Date: Tue, 22 May 2018 11:49:42 +0100 Subject: [PATCH] (gftest) Multiple concrete categories for context generation --- src/tools/gftest/Grammar.hs | 15 +++++++-------- 1 file 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 ]