module Gibbon.L1.Examples where

import Data.Map as M

import Gibbon.L1.Syntax

--------------------------------------------------------------------------------

treeTy :: Ty1
treeTy :: Ty1
treeTy = TyCon -> () -> Ty1
forall loc. TyCon -> loc -> UrTy loc
PackedTy TyCon
"Tree" ()

treeDD :: DDefs (UrTy ())
treeDD :: DDefs Ty1
treeDD = ([DDef Ty1] -> DDefs Ty1
forall a. [DDef a] -> DDefs a
fromListDD [Var -> [TyVar] -> [(TyCon, [(IsBoxed, Ty1)])] -> DDef Ty1
forall a. Var -> [TyVar] -> [(TyCon, [(IsBoxed, a)])] -> DDef a
DDef Var
"Tree" []
                      [ (TyCon
"Leaf",[(IsBoxed
False,Ty1
forall loc. UrTy loc
IntTy)])
                      , (TyCon
"Node",[(IsBoxed
False,Ty1
treeTy)
                                ,(IsBoxed
False,Ty1
treeTy)])]])

mkAdd1Prog :: Exp1 -> Maybe (Exp1, Ty1) -> Prog1
mkAdd1Prog :: Exp1 -> Maybe (Exp1, Ty1) -> Prog1
mkAdd1Prog Exp1
bod Maybe (Exp1, Ty1)
mainExp = DDefs (TyOf Exp1)
-> FunDefs Exp1 -> Maybe (Exp1, TyOf Exp1) -> Prog1
forall ex.
DDefs (TyOf ex) -> FunDefs ex -> Maybe (ex, TyOf ex) -> Prog ex
Prog DDefs (TyOf Exp1)
DDefs Ty1
treeDD
                              ([(Var, FunDef Exp1)] -> FunDefs Exp1
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Var
"add1",Exp1 -> FunDef Exp1
mkAdd1Fun Exp1
bod)])
                              Maybe (Exp1, TyOf Exp1)
Maybe (Exp1, Ty1)
mainExp

mkAdd1Fun :: Exp1 -> FunDef1
mkAdd1Fun :: Exp1 -> FunDef Exp1
mkAdd1Fun Exp1
bod = Var
-> [Var] -> ArrowTy (TyOf Exp1) -> Exp1 -> FunMeta -> FunDef Exp1
forall ex.
Var -> [Var] -> ArrowTy (TyOf ex) -> ex -> FunMeta -> FunDef ex
FunDef Var
"add1" [Var
"tr"] ([Ty1
treeTy],Ty1
treeTy) Exp1
bod (FunRec -> FunInline -> IsBoxed -> FunMeta
FunMeta FunRec
Rec FunInline
NoInline IsBoxed
False)

----------------

-- | The basic form of the add1 program where recursions happen
-- immediately as arguments to the data-constructor.
add1Prog :: Prog1
add1Prog :: Prog1
add1Prog = Exp1 -> Maybe (Exp1, Ty1) -> Prog1
mkAdd1Prog Exp1
exadd1Bod Maybe (Exp1, Ty1)
forall a. Maybe a
Nothing

exadd1Bod :: Exp1
exadd1Bod :: Exp1
exadd1Bod =
    Exp1 -> [(TyCon, [(Var, ())], Exp1)] -> Exp1
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec
-> [(TyCon, [(Var, loc)], PreExp ext loc dec)]
-> PreExp ext loc dec
CaseE (Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"tr") ([(TyCon, [(Var, ())], Exp1)] -> Exp1)
-> [(TyCon, [(Var, ())], Exp1)] -> Exp1
forall a b. (a -> b) -> a -> b
$
      [ (TyCon
"Leaf", [(Var
"n",())],
         Prim Ty1 -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty1
forall ty. Prim ty
AddP [Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"n", Int -> Exp1
forall (ext :: * -> * -> *) loc dec. Int -> PreExp ext loc dec
LitE Int
1])
      , (TyCon
"Node", [(Var
"x",()),(Var
"y",())],
         () -> TyCon -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
loc -> TyCon -> [PreExp ext loc dec] -> PreExp ext loc dec
DataConE () TyCon
"Node"
          [ Var -> [()] -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
"add1" [] [Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"x"]
          , Var -> [()] -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
"add1" [] [Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"y"]])
      ]

exadd1BodLetLeft :: Exp1
exadd1BodLetLeft :: Exp1
exadd1BodLetLeft =
    Exp1 -> [(TyCon, [(Var, ())], Exp1)] -> Exp1
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec
-> [(TyCon, [(Var, loc)], PreExp ext loc dec)]
-> PreExp ext loc dec
CaseE (Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"tr") ([(TyCon, [(Var, ())], Exp1)] -> Exp1)
-> [(TyCon, [(Var, ())], Exp1)] -> Exp1
forall a b. (a -> b) -> a -> b
$
      [ (TyCon
"Leaf", [(Var
"n",())], Prim Ty1 -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty1
forall ty. Prim ty
AddP [Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"n", Int -> Exp1
forall (ext :: * -> * -> *) loc dec. Int -> PreExp ext loc dec
LitE Int
1])
      , (TyCon
"Node", [(Var
"x",()),(Var
"y",())],
         (Var, [()], Ty1, Exp1) -> Exp1 -> Exp1
forall (ext :: * -> * -> *) loc dec.
(Var, [loc], dec, PreExp ext loc dec)
-> PreExp ext loc dec -> PreExp ext loc dec
LetE (Var
"x2",[], Ty1
treeTy, Var -> [()] -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
"add1" [] [Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"x"]) (Exp1 -> Exp1) -> Exp1 -> Exp1
forall a b. (a -> b) -> a -> b
$
         (Var, [()], Ty1, Exp1) -> Exp1 -> Exp1
forall (ext :: * -> * -> *) loc dec.
(Var, [loc], dec, PreExp ext loc dec)
-> PreExp ext loc dec -> PreExp ext loc dec
LetE (Var
"y2",[], Ty1
treeTy, Var -> [()] -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
"add1" [] [Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"y"]) (Exp1 -> Exp1) -> Exp1 -> Exp1
forall a b. (a -> b) -> a -> b
$
         () -> TyCon -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
loc -> TyCon -> [PreExp ext loc dec] -> PreExp ext loc dec
DataConE () TyCon
"Node"
          [ Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"x2", Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"y2"])
      ]

-- | A more challenging case where recursions are performed right-to-left
exadd1BodLetRight :: Exp1
exadd1BodLetRight :: Exp1
exadd1BodLetRight =
    Exp1 -> [(TyCon, [(Var, ())], Exp1)] -> Exp1
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec
-> [(TyCon, [(Var, loc)], PreExp ext loc dec)]
-> PreExp ext loc dec
CaseE (Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"tr") ([(TyCon, [(Var, ())], Exp1)] -> Exp1)
-> [(TyCon, [(Var, ())], Exp1)] -> Exp1
forall a b. (a -> b) -> a -> b
$
      [ (TyCon
"Leaf", [(Var
"n",())], Prim Ty1 -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty1
forall ty. Prim ty
AddP [Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"n", Int -> Exp1
forall (ext :: * -> * -> *) loc dec. Int -> PreExp ext loc dec
LitE Int
1])
      , (TyCon
"Node", [(Var
"x",()),(Var
"y",())],
         (Var, [()], Ty1, Exp1) -> Exp1 -> Exp1
forall (ext :: * -> * -> *) loc dec.
(Var, [loc], dec, PreExp ext loc dec)
-> PreExp ext loc dec -> PreExp ext loc dec
LetE (Var
"y2",[], Ty1
treeTy, Var -> [()] -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
"add1" [] [Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"y"]) (Exp1 -> Exp1) -> Exp1 -> Exp1
forall a b. (a -> b) -> a -> b
$
         (Var, [()], Ty1, Exp1) -> Exp1 -> Exp1
forall (ext :: * -> * -> *) loc dec.
(Var, [loc], dec, PreExp ext loc dec)
-> PreExp ext loc dec -> PreExp ext loc dec
LetE (Var
"x2",[], Ty1
treeTy, Var -> [()] -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
"add1" [] [Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"x"]) (Exp1 -> Exp1) -> Exp1 -> Exp1
forall a b. (a -> b) -> a -> b
$
         () -> TyCon -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
loc -> TyCon -> [PreExp ext loc dec] -> PreExp ext loc dec
DataConE () TyCon
"Node"
          [ Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"x2", Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"y2"])
      ]

-- | Add1 program with let bindings, recurring in left-to-right order.
add1ProgLetLeft :: Prog1
add1ProgLetLeft :: Prog1
add1ProgLetLeft = Exp1 -> Maybe (Exp1, Ty1) -> Prog1
mkAdd1Prog Exp1
exadd1BodLetLeft Maybe (Exp1, Ty1)
forall a. Maybe a
Nothing

-- | Add1 program with let bindings, recurring in right-to-left order.
add1ProgLetRight :: Prog1
add1ProgLetRight :: Prog1
add1ProgLetRight = Exp1 -> Maybe (Exp1, Ty1) -> Prog1
mkAdd1Prog Exp1
exadd1BodLetRight Maybe (Exp1, Ty1)
forall a. Maybe a
Nothing


-- | An even more challenging case where there is an (apparent) data
-- dependency where x2 depends on y2.
add1ProgChallenge :: Prog1
add1ProgChallenge :: Prog1
add1ProgChallenge =
    DDefs (TyOf Exp1)
-> FunDefs Exp1 -> Maybe (Exp1, TyOf Exp1) -> Prog1
forall ex.
DDefs (TyOf ex) -> FunDefs ex -> Maybe (ex, TyOf ex) -> Prog ex
Prog DDefs (TyOf Exp1)
DDefs Ty1
treeDD
         ([(Var, FunDef Exp1)] -> FunDefs Exp1
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (Var
"add1",Exp1 -> FunDef Exp1
mkAdd1Fun Exp1
forall {ext :: * -> * -> *}. PreExp ext () Ty1
bod)
                     , (Var
"pred", Var
-> [Var] -> ArrowTy (TyOf Exp1) -> Exp1 -> FunMeta -> FunDef Exp1
forall ex.
Var -> [Var] -> ArrowTy (TyOf ex) -> ex -> FunMeta -> FunDef ex
FunDef Var
"pred" [Var
"tr"] ([Ty1
treeTy], Ty1
forall loc. UrTy loc
BoolTy)
                        (Exp1 -> [(TyCon, [(Var, ())], Exp1)] -> Exp1
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec
-> [(TyCon, [(Var, loc)], PreExp ext loc dec)]
-> PreExp ext loc dec
CaseE (Var -> Exp1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"tr") ([(TyCon, [(Var, ())], Exp1)] -> Exp1)
-> [(TyCon, [(Var, ())], Exp1)] -> Exp1
forall a b. (a -> b) -> a -> b
$
                         [ (TyCon
"Leaf", [(Var
"n",())], Prim Ty1 -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty1
forall ty. Prim ty
MkTrue [])
                         , (TyCon
"Node", [(Var
"x",()),(Var
"y",())], Prim Ty1 -> [Exp1] -> Exp1
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty1
forall ty. Prim ty
MkFalse [])])
                        (FunRec -> FunInline -> IsBoxed -> FunMeta
FunMeta FunRec
Rec FunInline
NoInline IsBoxed
False))])
         Maybe (Exp1, TyOf Exp1)
Maybe (Exp1, Ty1)
forall a. Maybe a
Nothing
  where
   bod :: PreExp ext () Ty1
bod =
    PreExp ext () Ty1
-> [(TyCon, [(Var, ())], PreExp ext () Ty1)] -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec
-> [(TyCon, [(Var, loc)], PreExp ext loc dec)]
-> PreExp ext loc dec
CaseE (Var -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"tr") ([(TyCon, [(Var, ())], PreExp ext () Ty1)] -> PreExp ext () Ty1)
-> [(TyCon, [(Var, ())], PreExp ext () Ty1)] -> PreExp ext () Ty1
forall a b. (a -> b) -> a -> b
$
      [ (TyCon
"Leaf", [(Var
"n",())], Prim Ty1 -> [PreExp ext () Ty1] -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty1
forall ty. Prim ty
AddP [Var -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"n", Int -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Int -> PreExp ext loc dec
LitE Int
1])
      , (TyCon
"Node", [(Var
"x",()),(Var
"y",())],
         (Var, [()], Ty1, PreExp ext () Ty1)
-> PreExp ext () Ty1 -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
(Var, [loc], dec, PreExp ext loc dec)
-> PreExp ext loc dec -> PreExp ext loc dec
LetE (Var
"y2",[], Ty1
treeTy, Var -> [()] -> [PreExp ext () Ty1] -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
"add1" [] [Var -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"y"]) (PreExp ext () Ty1 -> PreExp ext () Ty1)
-> PreExp ext () Ty1 -> PreExp ext () Ty1
forall a b. (a -> b) -> a -> b
$
         (Var, [()], Ty1, PreExp ext () Ty1)
-> PreExp ext () Ty1 -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
(Var, [loc], dec, PreExp ext loc dec)
-> PreExp ext loc dec -> PreExp ext loc dec
LetE (Var
"x2",[], Ty1
treeTy,
              (PreExp ext () Ty1
-> PreExp ext () Ty1 -> PreExp ext () Ty1 -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec
-> PreExp ext loc dec -> PreExp ext loc dec -> PreExp ext loc dec
IfE (Var -> [()] -> [PreExp ext () Ty1] -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
"pred" [] [Var -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"y2"])
                   (Var -> [()] -> [PreExp ext () Ty1] -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
"add1" [] [Var -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"x"])
                   (Var -> [()] -> [PreExp ext () Ty1] -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
"add1" [] [Var -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"x"]))) (PreExp ext () Ty1 -> PreExp ext () Ty1)
-> PreExp ext () Ty1 -> PreExp ext () Ty1
forall a b. (a -> b) -> a -> b
$
         () -> TyCon -> [PreExp ext () Ty1] -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
loc -> TyCon -> [PreExp ext loc dec] -> PreExp ext loc dec
DataConE () TyCon
"Node" [ Var -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"x2", Var -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"y2"])
      ]

-- | This program is a challenge because a packed value flows to two destinations.
add1ProgSharing :: Prog1
add1ProgSharing :: Prog1
add1ProgSharing = DDefs (TyOf Exp1)
-> FunDefs Exp1 -> Maybe (Exp1, TyOf Exp1) -> Prog1
forall ex.
DDefs (TyOf ex) -> FunDefs ex -> Maybe (ex, TyOf ex) -> Prog ex
Prog DDefs (TyOf Exp1)
DDefs Ty1
treeDD ([(Var, FunDef Exp1)] -> FunDefs Exp1
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Var
"add1",Exp1 -> FunDef Exp1
mkAdd1Fun Exp1
forall {ext :: * -> * -> *}. PreExp ext () Ty1
bod)]) Maybe (Exp1, TyOf Exp1)
Maybe (Exp1, Ty1)
forall a. Maybe a
Nothing
  where
   bod :: PreExp ext () Ty1
bod =
    PreExp ext () Ty1
-> [(TyCon, [(Var, ())], PreExp ext () Ty1)] -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
PreExp ext loc dec
-> [(TyCon, [(Var, loc)], PreExp ext loc dec)]
-> PreExp ext loc dec
CaseE (Var -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"tr") ([(TyCon, [(Var, ())], PreExp ext () Ty1)] -> PreExp ext () Ty1)
-> [(TyCon, [(Var, ())], PreExp ext () Ty1)] -> PreExp ext () Ty1
forall a b. (a -> b) -> a -> b
$
      [ (TyCon
"Leaf", [(Var
"n",())], Prim Ty1 -> [PreExp ext () Ty1] -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
Prim dec -> [PreExp ext loc dec] -> PreExp ext loc dec
PrimAppE Prim Ty1
forall ty. Prim ty
AddP [Var -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"n", Int -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Int -> PreExp ext loc dec
LitE Int
1])
      , (TyCon
"Node", [(Var
"x",()),(Var
"y",())],
         (Var, [()], Ty1, PreExp ext () Ty1)
-> PreExp ext () Ty1 -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
(Var, [loc], dec, PreExp ext loc dec)
-> PreExp ext loc dec -> PreExp ext loc dec
LetE (Var
"x2",[], Ty1
treeTy, Var -> [()] -> [PreExp ext () Ty1] -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
Var -> [loc] -> [PreExp ext loc dec] -> PreExp ext loc dec
AppE Var
"add1" [] [Var -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"x"]) (PreExp ext () Ty1 -> PreExp ext () Ty1)
-> PreExp ext () Ty1 -> PreExp ext () Ty1
forall a b. (a -> b) -> a -> b
$
         () -> TyCon -> [PreExp ext () Ty1] -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec.
loc -> TyCon -> [PreExp ext loc dec] -> PreExp ext loc dec
DataConE () TyCon
"Node" [ Var -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"x2", Var -> PreExp ext () Ty1
forall (ext :: * -> * -> *) loc dec. Var -> PreExp ext loc dec
VarE Var
"x2"])
      ]