mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-23 11:42:49 -06:00
version 2 of doc
This commit is contained in:
@@ -19,7 +19,6 @@ abstract Imper = PredefAbs ** {
|
|||||||
(Fun AS V -> Rec AS) -> Program ;
|
(Fun AS V -> Rec AS) -> Program ;
|
||||||
FunctNil : (V : Typ) ->
|
FunctNil : (V : Typ) ->
|
||||||
Stm -> (Fun NilTyp V -> Program) -> Program ;
|
Stm -> (Fun NilTyp V -> Program) -> Program ;
|
||||||
|
|
||||||
RecOne : (A : Typ) -> (Var A -> Stm) -> Program -> Rec (ConsTyp A NilTyp) ;
|
RecOne : (A : Typ) -> (Var A -> Stm) -> Program -> Rec (ConsTyp A NilTyp) ;
|
||||||
RecCons : (A : Typ) -> (AS : ListTyp) ->
|
RecCons : (A : Typ) -> (AS : ListTyp) ->
|
||||||
(Var A -> Rec AS) -> Program -> Rec (ConsTyp A AS) ;
|
(Var A -> Rec AS) -> Program -> Rec (ConsTyp A AS) ;
|
||||||
@@ -38,16 +37,15 @@ abstract Imper = PredefAbs ** {
|
|||||||
EInt : Int -> Exp (TNum TInt) ;
|
EInt : Int -> Exp (TNum TInt) ;
|
||||||
EFloat : Int -> Int -> Exp (TNum TFloat) ;
|
EFloat : Int -> Int -> Exp (TNum TFloat) ;
|
||||||
ELt : (n : NumTyp) -> let Ex = Exp (TNum n) in Ex -> Ex -> Exp (TNum TInt) ;
|
ELt : (n : NumTyp) -> let Ex = Exp (TNum n) in Ex -> Ex -> Exp (TNum TInt) ;
|
||||||
EApp : (AS : ListTyp) -> (V : Typ) -> Fun AS V -> ListExp AS -> Exp V ;
|
|
||||||
EAdd, EMul, ESub : (n : NumTyp) -> let Ex = Exp (TNum n) in Ex -> Ex -> Ex ;
|
EAdd, EMul, ESub : (n : NumTyp) -> let Ex = Exp (TNum n) in Ex -> Ex -> Ex ;
|
||||||
|
EAppNil : (V : Typ) -> Fun NilTyp V -> Exp V ;
|
||||||
|
EApp : (AS : ListTyp) -> (V : Typ) -> Fun AS V -> ListExp AS -> Exp V ;
|
||||||
|
|
||||||
TNum : NumTyp -> Typ ;
|
TNum : NumTyp -> Typ ;
|
||||||
TInt, TFloat : NumTyp ;
|
TInt, TFloat : NumTyp ;
|
||||||
|
|
||||||
NilTyp : ListTyp ;
|
NilTyp : ListTyp ;
|
||||||
ConsTyp : Typ -> ListTyp -> ListTyp ;
|
ConsTyp : Typ -> ListTyp -> ListTyp ;
|
||||||
|
|
||||||
NilExp : ListExp NilTyp ;
|
|
||||||
OneExp : (A : Typ) -> Exp A -> ListExp (ConsTyp A NilTyp) ;
|
OneExp : (A : Typ) -> Exp A -> ListExp (ConsTyp A NilTyp) ;
|
||||||
ConsExp : (A : Typ) -> (AS : ListTyp) ->
|
ConsExp : (A : Typ) -> (AS : ListTyp) ->
|
||||||
Exp A -> ListExp AS -> ListExp (ConsTyp A AS) ;
|
Exp A -> ListExp AS -> ListExp (ConsTyp A AS) ;
|
||||||
|
|||||||
@@ -43,6 +43,7 @@ concrete ImperC of Imper = open ResImper in {
|
|||||||
ESub _ = infixL 2 "-" ;
|
ESub _ = infixL 2 "-" ;
|
||||||
ELt _ = infixN 1 "<" ;
|
ELt _ = infixN 1 "<" ;
|
||||||
|
|
||||||
|
EAppNil val f = constant (f.s ++ paren []) ;
|
||||||
EApp args val f exps = constant (f.s ++ paren exps.s) ;
|
EApp args val f exps = constant (f.s ++ paren exps.s) ;
|
||||||
|
|
||||||
TNum t = t ;
|
TNum t = t ;
|
||||||
@@ -50,8 +51,6 @@ concrete ImperC of Imper = open ResImper in {
|
|||||||
TFloat = ss "float" ;
|
TFloat = ss "float" ;
|
||||||
NilTyp = ss [] ;
|
NilTyp = ss [] ;
|
||||||
ConsTyp = cc2 ;
|
ConsTyp = cc2 ;
|
||||||
|
|
||||||
NilExp = ss [] ;
|
|
||||||
OneExp _ e = e ;
|
OneExp _ e = e ;
|
||||||
ConsExp _ _ e es = ss (e.s ++ "," ++ es.s) ;
|
ConsExp _ _ e es = ss (e.s ++ "," ++ es.s) ;
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -75,6 +75,9 @@ flags lexer=codevars ; unlexer=code ; startcat=Stm ;
|
|||||||
ESub = binopt "_sub" ;
|
ESub = binopt "_sub" ;
|
||||||
EMul = binopt "_mul" ;
|
EMul = binopt "_mul" ;
|
||||||
ELt t = binop ("invokestatic" ++ t.s ++ "runtime/lt" ++ paren (t.s ++ t.s) ++ "i") ;
|
ELt t = binop ("invokestatic" ++ t.s ++ "runtime/lt" ++ paren (t.s ++ t.s) ++ "i") ;
|
||||||
|
EAppNil val f = instr (
|
||||||
|
"invokestatic" ++ f.s ++ paren [] ++ val.s
|
||||||
|
) ;
|
||||||
EApp args val f exps = instr (
|
EApp args val f exps = instr (
|
||||||
exps.s ++
|
exps.s ++
|
||||||
"invokestatic" ++ f.s ++ paren args.s ++ val.s
|
"invokestatic" ++ f.s ++ paren args.s ++ val.s
|
||||||
@@ -83,11 +86,8 @@ flags lexer=codevars ; unlexer=code ; startcat=Stm ;
|
|||||||
TNum t = t ;
|
TNum t = t ;
|
||||||
TInt = ss "i" ;
|
TInt = ss "i" ;
|
||||||
TFloat = ss "f" ;
|
TFloat = ss "f" ;
|
||||||
|
|
||||||
NilTyp = ss [] ;
|
NilTyp = ss [] ;
|
||||||
ConsTyp = cc2 ;
|
ConsTyp = cc2 ;
|
||||||
|
|
||||||
NilExp = ss [] ;
|
|
||||||
OneExp _ e = e ;
|
OneExp _ e = e ;
|
||||||
ConsExp _ _ = cc2 ;
|
ConsExp _ _ = cc2 ;
|
||||||
}
|
}
|
||||||
|
|||||||
File diff suppressed because it is too large
Load Diff
Reference in New Issue
Block a user