diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-22 00:02:23 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-22 00:02:23 +0000 |
| commit | 02cb45707da07d5e6faca92158d10a6e454a6bac (patch) | |
| tree | 0957f3a54a7c75c3b4ae2437fc0d05b1ed0d5982 /src/Obs/Typing | |
| parent | a8a4ef9933a1a07b6fbf2d257df2a5fb40b1e87d (diff) | |
Add Container types.
Diffstat (limited to 'src/Obs/Typing')
| -rw-r--r-- | src/Obs/Typing/Conversion.idr | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr index 20198c5..37bdf67 100644 --- a/src/Obs/Typing/Conversion.idr +++ b/src/Obs/Typing/Conversion.idr @@ -42,6 +42,11 @@ convert t u (Cnstr (Sigma s s' var a b)) (Set k) = do convert t2 u2 b s' -- In type Sum (manually expanding definition of doCase) convert t u (Cnstr (Sum s s' a b)) (Set _) = convertSum t u s s' a b +-- In type Container +convert t u (Cnstr (Container s a s' s'')) (Set l) = do + t <- expandContainer t + u <- expandContainer u + convert (Cnstr t) (Cnstr u) (Cnstr (expandContainerTy s a s' s'')) (Set l) -- Default convert t u a s = inScope "invalid conversion" $ fatal $ @@ -57,6 +62,9 @@ convertSet (Cnstr (Sigma s s' _ a b)) (Cnstr (Sigma l l' _ a' b')) = convertSet (Cnstr (Sum s s' a b)) (Cnstr (Sum l l' a' b')) = pure $ s == l && s' == l' && !(convertSet a a') && !(convertSet b b') +convertSet (Cnstr (Container s a s' s'')) (Cnstr (Container l a' l' l'')) = + pure $ + s == l && s' == l' && s'' == l'' && !(convertSet a a') convertSet (Cnstr Top) (Cnstr Top) = pure True convertSet (Cnstr Bottom) (Cnstr Bottom) = pure True convertSet (Ntrl t) u = pure (Ntrl t == u) |