diff options
Diffstat (limited to 'src/Term/Semantics.idr')
| -rw-r--r-- | src/Term/Semantics.idr | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr index 62e2be7..c31a9e6 100644 --- a/src/Term/Semantics.idr +++ b/src/Term/Semantics.idr @@ -33,6 +33,29 @@ restrict (Keep thin) = [| mapInit (restrict thin) |] indexVar : All p [<x] -> p x indexVar [<px] = px +arb : (ty : Ty) -> TypeOf ty +arb N = 0 +arb (ty ~> ty') = const (arb ty') + +swap : (ty1, ty2 : Ty) -> TypeOf (ty1 <+> ty2) -> TypeOf (ty2 <+> ty1) +swap N N = id +swap N (ty2 ~> ty2') = (swap N ty2' .) +swap (ty1 ~> ty1') N = (swap ty1' N .) +swap (ty1 ~> ty1') (ty2 ~> ty2') = (swap ty1' ty2' .) . (. swap ty2 ty1) + +inl : (ty1, ty2 : Ty) -> TypeOf ty1 -> TypeOf (ty1 <+> ty2) +prl : (ty1, ty2 : Ty) -> TypeOf (ty1 <+> ty2) -> TypeOf ty1 + +inl N N = id +inl N (ty2 ~> ty2') = const . inl N ty2' +inl (ty1 ~> ty1') N = (inl ty1' N .) +inl (ty1 ~> ty1') (ty2 ~> ty2') = (inl ty1' ty2' .) . (. prl ty1 ty2) + +prl N N = id +prl N (ty2 ~> ty2') = prl N ty2' . ($ arb ty2) +prl (ty1 ~> ty1') N = (prl ty1' N .) +prl (ty1 ~> ty1') (ty2 ~> ty2') = (prl ty1' ty2' .) . (. inl ty1 ty2) + %inline opSem : Operator tys ty -> TypeOf (foldr (~>) ty tys) opSem (Lit n) = n @@ -43,6 +66,11 @@ opSem Pred = pred opSem Minus = minus opSem Div = div opSem Mod = mod +opSem (Inl ty1 ty2) = inl ty1 ty2 +opSem (Inr ty1 ty2) = swap ty2 ty1 . inl ty2 ty1 +opSem (Prl ty1 ty2) = prl ty1 ty2 +opSem (Prr ty1 ty2) = prl ty2 ty1 . swap ty1 ty2 +opSem (Arb ty) = arb ty %inline sem' : Monad m => Term ty ctx -> m (All TypeOf ctx -> TypeOf ty) |