mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-17 00:39:32 -06:00
51 lines
1.4 KiB
Plaintext
51 lines
1.4 KiB
Plaintext
abstract Imper = {
|
|
|
|
cat
|
|
Program ;
|
|
Typ ;
|
|
ListTyp ;
|
|
Fun ListTyp Typ ;
|
|
Body ListTyp ;
|
|
Stm ;
|
|
Exp Typ ;
|
|
Var Typ ;
|
|
ListExp ListTyp ;
|
|
|
|
fun
|
|
Empty : Program ;
|
|
Funct : (AS : ListTyp) -> (V : Typ) ->
|
|
Body AS -> (Fun AS V -> Program) -> Program ;
|
|
|
|
BodyNil : Stm -> Body NilTyp ;
|
|
BodyCons : (A : Typ) -> (AS : ListTyp) ->
|
|
(Var A -> Body AS) -> Body (ConsTyp A AS) ;
|
|
|
|
Decl : (A : Typ) -> (Var A -> Stm) -> Stm ;
|
|
Assign : (A : Typ) -> Var A -> Exp A -> Stm -> Stm ;
|
|
Return : (A : Typ) -> Exp A -> Stm ;
|
|
While : Exp TInt -> Stm -> Stm -> Stm ;
|
|
IfElse : Exp TInt -> Stm -> Stm -> Stm -> Stm ;
|
|
Block : Stm -> Stm -> Stm ;
|
|
End : Stm ;
|
|
|
|
EVar : (A : Typ) -> Var A -> Exp A ;
|
|
EInt : Int -> Exp TInt ;
|
|
EFloat : Int -> Int -> Exp TFloat ;
|
|
ELtI : Exp TInt -> Exp TInt -> Exp TInt ;
|
|
ELtF : Exp TFloat -> Exp TFloat -> Exp TInt ;
|
|
EApp : (AS : ListTyp) -> (V : Typ) -> Fun AS V -> ListExp AS -> Exp V ;
|
|
EAddI, EMulI, ESubI : Exp TInt -> Exp TInt -> Exp TInt ;
|
|
EAddF, EMulF, ESubF : Exp TFloat -> Exp TFloat -> Exp TFloat ;
|
|
|
|
TInt : Typ ;
|
|
TFloat : Typ ;
|
|
|
|
NilTyp : ListTyp ;
|
|
ConsTyp : Typ -> ListTyp -> ListTyp ;
|
|
|
|
NilExp : ListExp NilTyp ;
|
|
ConsExp : (A : Typ) -> (AS : ListTyp) ->
|
|
Exp A -> ListExp AS -> ListExp (ConsExp A AS) ;
|
|
|
|
}
|