Skip to content

Commit

Permalink
Merge pull request #2455 from ucsd-progsys/fd/tyvar-detection
Browse files Browse the repository at this point in the history
Fix detection of tyvars when generalizing sorts of gsImpAxioms
  • Loading branch information
facundominguez authored Dec 3, 2024
2 parents dd3030c + 0c88b71 commit b159872
Showing 1 changed file with 4 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -222,14 +222,16 @@ measEnv sp xts cbs _tcb lt1s lt2s asms itys hs info = CGE
lts = lt1s ++ lt2s
tcb' = []

-- | Given an equation whose sorts are @FObj "a"@, @FObj "b"@, etc,
-- | Given an equation whose sorts are @FObj "a##..."@, @FObj "b##..."@, etc,
-- replaces those with @FVar@s.
eqToPolySort :: F.EquationV v -> F.Sort
eqToPolySort e =
let s = foldr (F.FFunc . snd) (F.eqSort e) (F.eqArgs e)
ss = filter (all isLower . take 1 . F.symbolString) $ S.toList $ F.sortSymbols s
ss = filter (isTyVarName . F.symbolString) $ S.toList $ F.sortSymbols s
su = F.mkSortSubst $ zip ss $ map F.FVar [0..]
in F.mkPoly (length ss - 1) $ F.sortSubst su s
where
isTyVarName s = all isLower (take 1 s) && L.isInfixOf "##" s

assm :: TargetInfo -> [(Var, SpecType)]
assm = assmGrty (giImpVars . giSrc)
Expand Down

0 comments on commit b159872

Please sign in to comment.