% syntax.elf % % Defines: % % - source expressions (exp) % % - equality on source expressions (eqexp) % % - target terms (tm) % % - types (ty) % For convenience, we use the same type family `ty' to represent % source and target types, because they happen to be bijective. % This lets us avoid defining a type translation function. % % Source syntax: expressions (exp) % exp : type. %name exp _E. unit : exp. lam : (exp -> exp) -> exp. app : exp -> exp -> exp. merge : exp -> exp -> exp. fix : (exp -> exp) -> exp. % % Equality on source expressions % eqexp : exp -> exp -> type. eqexp/refl : eqexp E E. eqexp/lam : {EqBody : {e : exp} eqexp (E e) (E' e)} eqexp (lam ([e] E e)) (lam ([e] E' e)). eqexp/app : {Eq1 : eqexp E1 E1'} {Eq2 : eqexp E2 E2'} eqexp (app E1 E2) (app E1' E2'). eqexp/merge : {Eq1 : eqexp E1 E1'} {Eq2 : eqexp E2 E2'} eqexp (merge E1 E2) (merge E1' E2'). % % Target syntax: terms (tm) % tm : type. %name tm _M. unittm : tm. pairtm : tm -> tm -> tm. projtm : 2er -> tm -> tm. fsttm = projtm 1. sndtm = projtm 2. lamtm : (tm -> tm) -> tm. apptm : tm -> tm -> tm. fixtm : (tm -> tm) -> tm. injtm : 2er -> tm -> tm. inl = injtm 1. inr = injtm 2. inltm = inl. inrtm = inr. casetm : tm -> (tm -> tm) -> (tm -> tm) -> tm. % casetm scrutinee branch1 branch2 % % Source types (ty) % % Also used, for convenience, for target types: % the informal interpretation of each type therefore depends on % whether a source expression or target term is being typed. % This works because the type translation function ||A|| is a bijection. ty : type. %name ty _A. eqty : ty -> ty -> type. eqty/refl : eqty E E. arr : ty -> ty -> ty. % A -> B sectty : ty -> ty -> ty. % A /\ B (A & B in the compiler concrete syntax) topty : ty. % Top unty : ty -> ty -> ty. % A \/ B % % Define the "real" names of target types as synonyms. % %abbrev tp = ty. %abbrev prod = sectty. %abbrev unittp = topty. %abbrev arrtp = arr. %abbrev sumty = unty. %freeze exp. %freeze tm. %freeze ty.