Commit cf45fb42 authored by André Pacak's avatar André Pacak

remove pair/prod because it is not needed for sums

parent 06a48087
......@@ -39,10 +39,6 @@ matchFun :: Type -> String -> Infer (Type, Type)
matchFun (Fun ty1 ty2) _ = return (ty1, ty2)
matchFun ty err = fail $ funError ty err
matchProd :: Type -> String -> Infer (Type, Type)
matchProd (Prod ty1 ty2) _ = return (ty1, ty2)
matchProd ty err = fail $ prodError ty err
matchType :: Type -> Type -> String -> Check
matchType ty1 ty2 _
| ty1 == ty2 = return ()
......@@ -83,24 +79,12 @@ inferType ctx (App t1 t2 _) = do
(ty1, ty2) <- matchFun ty (show t1)
checkType ctx t2 ty1
return ty2
inferType ctx (Fst t _) = do
ty <- inferType ctx t
(ty1, _) <- matchProd ty (show t)
return ty1
inferType ctx (Snd t _) = do
ty <- inferType ctx t
(_, ty2) <- matchProd ty (show t)
return ty2
inferType _ t = fail $ "Cannot infer type of term " ++ show t
checkType :: Ctx -> Term -> Type -> Check
checkType ctx p@(Lam name t _) ty = do
(ty1, ty2) <- matchFun ty (show p)
checkType (Bind ctx name ty1) t ty2
checkType ctx p@(Pair t1 t2 _) ty = do
(ty1, ty2) <- matchProd ty (show p)
checkType ctx t1 ty1
checkType ctx t2 ty2
checkType ctx p@(InL t _) ty = do
(ty1, ty2) <- matchSum ty (show p)
checkType ctx t ty1
......
......@@ -77,10 +77,6 @@ matchFun :: Type -> String -> Infer (Type, Type)
matchFun (Fun ty1 ty2) _ = return (ty1, ty2)
matchFun ty err = fail [funError ty err]
matchProd :: Type -> String -> Infer (Type, Type)
matchProd (Prod ty1 ty2) _ = return (ty1, ty2)
matchProd ty err = fail [prodError ty err]
matchType :: Type -> Type -> String -> Check
matchType ty1 ty2 _ | ty1 >= ty2 = return ()
matchType ty1 ty2 err = fail [generalError (show ty1) ty2 err]
......@@ -119,24 +115,12 @@ inferType ctx (App t1 t2 _) = do
(ty1, ty2) <- matchFun ty (show t1)
checkType ctx t2 ty1
return ty2
inferType ctx (Fst t _) = do
ty <- inferType ctx t
(ty1, _) <- matchProd ty (show t)
return ty1
inferType ctx (Snd t _) = do
ty <- inferType ctx t
(_, ty2) <- matchProd ty (show t)
return ty2
inferType _ t = fail ["Cannot infer type of term " ++ show t]
checkType :: Ctx -> Term -> Type -> Check
checkType ctx p@(Lam name t _) ty = do
(ty1, ty2) <- matchFun ty (show p)
checkType(Bind ctx name ty1) t ty2
checkType ctx p@(Pair t1 t2 _) ty = do
(ty1, ty2) <- matchProd ty (show p)
checkType ctx t1 ty1
checkType ctx t2 ty2
checkType ctx p@(InL t _) ty = do
(ty1, ty2) <- matchSum ty (show p)
checkType ctx t ty1
......
......@@ -77,10 +77,6 @@ matchFun :: Type -> String -> Infer (Type, Type)
matchFun (Fun ty1 ty2) _ = Inferred (ty1, ty2)
matchFun ty err = NotInferred [funError ty err]
matchProd :: Type -> String -> Infer (Type, Type)
matchProd (Prod ty1 ty2) _ = Inferred (ty1, ty2)
matchProd ty err = NotInferred [prodError ty err]
matchType :: Type -> Type -> String -> Check
matchType ty1 ty2 _ | ty1 >= ty2 = Inferred ()
matchType ty1 ty2 err = NotInferred [generalError (show ty1) ty2 err]
......@@ -121,10 +117,6 @@ lookup t x = case parent t of
lookup p x
Just p@(App t1 t2 _) | t == t2 -> do
lookup p x
Just p@(Fst t _) -> do
lookup p x
Just p@(Snd t _) -> do
lookup p x
Just p@(Lam name term _) ->
if name == x
then do
......@@ -132,10 +124,6 @@ lookup t x = case parent t of
(ty1, ty2) <- matchFun ty (show p)
return ty1
else lookup p x
Just p@(Pair t1 t2 _) | t == t1 -> do
lookup p x
Just p@(Pair t1 t2 _) | t == t2 -> do
lookup p x
Just p@(InL term _) -> do
lookup p x
Just p@(InR term _) -> do
......@@ -183,14 +171,6 @@ inferType (App t1 t2 _) = do
(ty1, ty2) <- matchFun ty (show t1)
checkType t2
return ty2
inferType (Fst t _) = do
ty <- inferType t
(ty1, _) <- matchProd ty (show t)
return ty1
inferType (Snd t _) = do
ty <- inferType t
(_, ty2) <- matchProd ty (show t)
return ty2
inferType t = fail ["Cannot infer type of term " ++ show t]
checkType :: Term -> Check
......@@ -198,11 +178,6 @@ checkType p@(Lam name t _) = do
ty <- requiredType p
(ty1, ty2) <- matchFun ty (show p)
checkType t
checkType p@(Pair t1 t2 _) = do
ty <- requiredType p
(ty1, ty2) <- matchProd ty (show p)
checkType t1
checkType t2
checkType p@(InL t _) = do
ty <- requiredType p
(ty1, ty2) <- matchSum ty (show p)
......@@ -242,14 +217,6 @@ requiredType t = case parent t of
ty <- requiredType p
(ty1, ty2) <- matchFun ty (show p)
return ty2
Just p@(Pair t1 t2 _) | t == t1 -> do
ty <- requiredType p
(ty1, ty2) <- matchProd ty (show p)
return ty1
Just p@(Pair t1 t2 _) | t == t2 -> do
ty <- requiredType p
(ty1, ty2) <- matchProd ty (show p)
return ty2
Just p@(InL term _) | t == term -> do
ty <- requiredType p
(ty1, ty2) <- matchSum ty (show p)
......
......@@ -76,10 +76,6 @@ matchFun :: Type -> String -> Infer (Type, Type)
matchFun (Fun ty1 ty2) _ = return (ty1, ty2)
matchFun ty err = fail [funError ty err]
matchProd :: Type -> String -> Infer (Type, Type)
matchProd (Prod ty1 ty2) _ = return (ty1, ty2)
matchProd ty err = fail [prodError ty err]
matchSum :: Type -> String -> Infer (Type, Type)
matchSum (Sum ty1 ty2) _ = return (ty1, ty2)
matchSum ty err = fail [sumError ty err]
......@@ -118,14 +114,6 @@ inferType ctx (App t1 t2 _) = do
(ty1, ty2) <- matchFun ty (show t1)
checkType ctx t2
return ty2
inferType ctx (Fst t _) = do
ty <- inferType ctx t
(ty1, _) <- matchProd ty (show t)
return ty1
inferType ctx (Snd t _) = do
ty <- inferType ctx t
(_, ty2) <- matchProd ty (show t)
return ty2
inferType _ t = fail ["Cannot infer type of term " ++ show t]
checkType :: Ctx -> Term -> Check
......@@ -134,11 +122,6 @@ checkType ctx p@(Lam name t _) = do
(ty1, ty2) <- matchFun ty (show p)
let ctx' = (Bind ctx name ty1)
checkType ctx' t
checkType ctx p@(Pair t1 t2 _) = do
ty <- requiredType ctx p
(ty1, ty2) <- matchProd ty (show p)
checkType ctx t1
checkType ctx t2
checkType ctx p@(InL t _) = do
ty <- requiredType ctx p
(ty1, ty2) <- matchSum ty (show p)
......@@ -180,14 +163,6 @@ requiredType ctx t = case parent t of
ty <- requiredType ctx' p
(ty1, ty2) <- matchFun ty (show p)
return ty2
Just p@(Pair t1 t2 _) | t == t1 -> do
ty <- requiredType ctx p
(ty1, ty2) <- matchProd ty (show p)
return ty1
Just p@(Pair t1 t2 _) | t == t2 -> do
ty <- requiredType ctx p
(ty1, ty2) <- matchProd ty (show p)
return ty2
Just p@(InL term _) | t == term -> do
ty <- requiredType ctx p
(ty1, ty2) <- matchSum ty (show p)
......
......@@ -36,10 +36,6 @@ matchFun :: Type -> String -> Infer (Type, Type)
matchFun (Fun ty1 ty2) _ = return (ty1, ty2)
matchFun ty err = fail $ funError ty err
matchProd :: Type -> String -> Infer (Type, Type)
matchProd (Prod ty1 ty2) _ = return (ty1, ty2)
matchProd ty err = fail $ prodError ty err
matchType :: Type -> Type -> String -> Check
matchType ty1 ty2 _ | ty1 == ty2 = return ()
matchType ty1 ty2 err = fail $ generalError (show ty1) ty2 err
......@@ -78,24 +74,12 @@ inferType ctx (App t1 t2 _) = do
(ty1, ty2) <- matchFun ty (show t1)
checkType ctx t2 ty1
return ty2
inferType ctx (Fst t _) = do
ty <- inferType ctx t
(ty1, _) <- matchProd ty (show t)
return ty1
inferType ctx (Snd t _) = do
ty <- inferType ctx t
(_, ty2) <- matchProd ty (show t)
return ty2
inferType _ t = fail $ "Cannot infer type of term " ++ show t
checkType :: Ctx -> Term -> Type -> Check
checkType ctx p@(Lam name t _) ty = do
(ty1, ty2) <- matchFun ty (show p)
checkType(Bind ctx name ty1) t ty2
checkType ctx p@(Pair t1 t2 _) ty = do
(ty1, ty2) <- matchProd ty (show p)
checkType ctx t1 ty1
checkType ctx t2 ty2
checkType ctx p@(InL t _) ty = do
(ty1, ty2) <- matchSum ty (show p)
checkType ctx t ty1
......
......@@ -16,10 +16,6 @@ data Term =
Succ Term Parent |
Add Term Term Parent |
Mult Term Term Parent |
-- pair constructs
Pair Term Term Parent |
Fst Term Parent |
Snd Term Parent |
-- let binding
Let Name Term Term Parent |
-- sum types
......@@ -36,9 +32,6 @@ instance Eq Term where
(Succ t _) == (Succ t' _) = t == t'
(Add t1 t2 _) == (Add t1' t2' _) = t1 == t1' && t2 == t2'
(Mult t1 t2 _) == (Mult t1' t2' _) = t1 == t1' && t2 == t2'
(Pair t1 t2 _) == (Pair t1' t2' _) = t1 == t1' && t2 == t2'
(Fst t _) == (Fst t' _) = t == t'
(Snd t _) == (Snd t' _) = t == t'
(Let n t1 t2 _) == (Let n' t1' t2' _) = n == n' && t1 == t1' && t2 == t2'
(InL t _) == (InL t' _) = t == t'
(InR t _) == (InR t' _) = t == t'
......@@ -56,9 +49,6 @@ parent (Zero p) = p
parent (Succ _ p) = p
parent (Add _ _ p) = p
parent (Mult _ _ p) = p
parent (Pair _ _ p) = p
parent (Fst _ p) = p
parent (Snd _ p) = p
parent (Let _ _ _ p) = p
parent (InL _ p) = p
parent (InR _ p) = p
......@@ -93,9 +83,6 @@ succ = cons1 Succ
add = cons2 Add
mult = cons2 Mult
pair = cons2 Pair
fst' = cons1 Fst
snd' = cons1 Snd
let' n = cons2 (Let n)
......@@ -120,21 +107,17 @@ instance Show Term where
showsPrec p (Add l r _) = showString "Add " . showsPrec (p + 1) l . showString " " . showsPrec (p + 1) r
showsPrec p (Mult l r _) = showString "Mult " . showsPrec (p + 1) l . showString " " . showsPrec (p + 1) r
showsPrec p (Pair l r _) = showString "{" . showsPrec (p + 1) l . showString ", ". showsPrec (p + 1) r . showString "}"
showsPrec p (Fst e _) = showsPrec (p + 1) e . showString ".1"
showsPrec p (Snd e _) = showsPrec (p + 1) e . showString ".2"
showsPrec p (Let n e b _) =
showString "let " . showString n . showString " = " . showsPrec (p + 1) e . showString " in " . showsPrec (p + 1) b
showsPrec p (InL t _) = showString "InL " . showsPrec (p + 1) t
showsPrec p (InR t _) = showString "InR " . showsPrec (p + 1) t
data Type = Nat | Fun Type Type | Prod Type Type | Sum Type Type | AnyType
data Type = Nat | Fun Type Type | Sum Type Type | AnyType
deriving (Show, Eq)
instance PO.PartialOrd Type where
_ <= AnyType = True
(Fun t1 t2) <= (Fun u1 u2) = t1 <= u1 && t2 <= u2
(Prod t1 t2) <= (Prod u1 u2) = t1 <= u1 && t2 <= u2
(Sum t1 t2) <= (Sum u1 u2) = t1 <= u1 && t2 <= u2
ty1 <= ty2 = ty1 == ty2
......
......@@ -31,12 +31,6 @@ sharedSpec inferType = do
let res = convert $ inferType tOkArithmetic in res `shouldBe` B.Inferred Nat
it "should infer let binding with arithmetic expression to be of type Nat" $ do
let res = convert $ inferType tOkLetBindingWithArith in res `shouldBe` B.Inferred Nat
it "should infer expression to be of type (Prod Nat (Prod Nat Nat))" $ do
let res = convert $ inferType tOkProd in res `shouldBe` B.Inferred (Prod Nat (Prod Nat Nat))
it "should infer projection for first element to be of type Nat" $ do
let res = convert $ inferType tOkProjection1 in res `shouldBe` B.Inferred Nat
it "should infer projection for second element to be of type (Prod Nat Nat)" $ do
let res = convert $ inferType tOkProjection2 in res `shouldBe` B.Inferred (Prod Nat Nat)
it "should infer nested lambda expressions" $ do
let res = convert $ inferType tOkAppLambdaAnno in res `shouldBe` B.Inferred Nat
it "should infer annotated lambda to be of type (Fun Nat Nat)" $ do
......@@ -45,14 +39,10 @@ sharedSpec inferType = do
let res = convert $ inferType tOkAnno in res `shouldBe` B.Inferred (Fun (Fun Nat Nat) (Fun (Fun Nat Nat) (Fun Nat Nat)))
it "should infer let binding with annotation in named expression" $ do
let res = convert $ inferType tOkAnnoInBindingLet in res `shouldBe` B.Inferred Nat
it "should infer let binding in pair(fst)" $ do
let res = convert $ inferType tOkLetInPairFst in res `shouldBe` B.Inferred (Prod Nat (Fun Nat Nat))
it "should infer let binding in pair(snd)" $ do
let res = convert $ inferType tOkLetInPairSnd in res `shouldBe` B.Inferred (Prod (Fun Nat Nat) Nat)
it "should infer left injection " $ do
let res = convert $ inferType tOkInL in res `shouldBe` B.Inferred (Sum Nat (Fun Nat Nat))
it "should infer right injection " $ do
let res = convert $ inferType tOkInR in res `shouldBe` B.Inferred (Sum Nat (Prod Nat (Fun Nat Nat)))
let res = convert $ inferType tOkInR in res `shouldBe` B.Inferred (Sum Nat (Fun Nat Nat))
it "should infer case for left injection " $ do
let res = convert $ inferType tOkCaseLeft in res `shouldBe` B.Inferred Nat
it "should infer case for right injection " $ do
......@@ -64,18 +54,8 @@ sharedSpec inferType = do
let res = isInferred $ convert $ inferType tFailArithmetic in res `shouldBe` False
it "should fail while inferring an application of a lambda expression without type annotation" $ do
let res = isInferred $ convert $ inferType tFailLambdaNoAnno in res `shouldBe` False
it "should fail while inferring an add expression that has a product as an argument" $ do
let res = isInferred $ convert $ inferType tFailProdInAdd in res `shouldBe` False
it "should fail while trying to infer an annotated expression that should be of type Nat but is (Prod Nat Nat)" $ do
let res = isInferred $ convert $ inferType tFailLambdaInProd in res `shouldBe` False
it "should fail while trying to infer a projection on a Nat type" $ do
let res = isInferred $ convert $ inferType tFailProjectionOnNat in res `shouldBe` False
it "should fail while trying to infer a let binding without annotation of lambda in named expression" $ do
let res = isInferred $ convert $ inferType tFailLambdaNotAnnoInBindingLet in res `shouldBe` False
it "should fail while inferering let binding in pair(fst)" $ do
let res = isInferred $ convert $ inferType tFailLetInPairFst in res `shouldBe` False
it "should fail while infering let binding in pair(snd)" $ do
let res = isInferred $ convert $ inferType tFailLetInPairSnd in res `shouldBe` False
it "should fail while infering left injection" $ do
let res = isInferred $ convert $ inferType tFailInL in res `shouldBe` False
it "should fail while infering right injection" $ do
......
......@@ -8,33 +8,22 @@ tOkZero = root zero
tOkSucc = root $ succ $ succ zero
tOkArithmetic = root $ (add (succ $ succ zero) (mult zero (succ $ succ $ succ $ succ zero)))
tOkLetBindingWithArith = root $ (let' "x" (add zero (succ zero)) (mult (var "x") (succ $ succ zero)))
tOkProd = root $ (anno (Prod Nat (Prod Nat Nat)) (pair (succ $ succ zero) (pair zero (succ zero))))
tOkProjection1 = root $ fst' (anno (Prod Nat Nat) (pair (mult zero zero) (add (succ zero) zero)))
tOkProjection2 = root $ snd' (anno (Prod Nat (Prod Nat Nat)) (pair (succ $ succ zero) (pair zero (succ zero))))
tOkAnno = root $ (anno (Fun (Fun Nat Nat) (Fun (Fun Nat Nat) (Fun Nat Nat))) (lam "f" $ lam "g" $ lam "b" (app (var "g") (app (var "f") (var "b")))))
tOkLambdaAnno = root $ (anno (Fun Nat Nat) (lam "a" (add (var "a") zero)))
tOkAppLambdaAnno = root $ (app (anno (Fun Nat Nat) (lam "b" (add (var "b") zero))) (succ $ succ zero))
tOkAnnoInBindingLet = root $ (let' "e" (anno Nat (add zero (succ zero))) (mult (var "e") (succ zero)))
tOkLetInPairFst = root $ (anno (Prod Nat (Fun Nat Nat)) (pair (let' "e" zero (succ $ succ (var "e"))) (lam "a" (succ (var "a")))))
tOkLetInPairSnd = root $ (anno (Prod (Fun Nat Nat) Nat) (pair (lam "n" (var "n")) (let' "e" zero (succ $ succ (var "e")))))
tOkInL = root $ (anno (Sum Nat (Fun Nat Nat)) (inl $ succ zero))
tOkInR = root $ (anno (Sum Nat (Prod Nat (Fun Nat Nat))) (inr (pair (succ $ succ zero) (anno (Fun Nat Nat) (lam "b" zero)))))
tOkCaseLeft = root $ (anno Nat (case' (anno (Sum Nat (Prod Nat Nat)) (inl $ succ zero)) "a" (var "a") "b" zero))
tOkInR = root $ (anno (Sum Nat (Fun Nat Nat)) (inr (anno (Fun Nat Nat) (lam "b" zero))))
tOkCaseLeft = root $ (anno Nat (case' (anno (Sum Nat Nat) (inl $ zero)) "a" (var "a") "b" zero))
tOkCaseRight = root $ (anno Nat (case' (anno (Sum Nat (Fun Nat Nat)) (inr $ lam "x" $ add zero $ var "x")) "a" zero "b" (app (var "b") (succ $ succ zero))))
tOkCaseLeftShadowBinding = root $ (let' "a" zero (anno Nat (case' (anno (Sum (Fun Nat Nat) Nat) (inl $ lam "x" zero)) "a" (app (var "a") zero) "b" (var "a"))))
tFailArithmetic = root $ (add (succ $ succ zero) (mult (anno (Fun Nat Nat) (lam "f" (var "f"))) (succ $ succ $ succ $ succ zero)))
tFailLambdaNoAnno = root $ (anno Nat (app (lam "b" (add (var "b") zero)) (succ $ succ zero)))
tFailProdInAdd = root $ (anno Nat (add (anno (Prod Nat Nat) (pair zero zero)) zero))
tFailLambdaInProd = root $ (anno Nat (snd' (anno (Prod Nat Nat) (pair (anno (Fun Nat Nat) (lam "a" (var "a"))) zero))))
tFailProjectionOnNat = root $ snd' $ succ $ succ zero
tFailLambdaNotAnnoInBindingLet = root $ (let' "e" (lam "n" (add (var "n") (succ zero))) (mult (app (var "e") zero) (succ zero)))
tFailLetInPairFst = root $ (anno (Prod (Fun Nat Nat) (Fun Nat Nat)) (pair (let' "e" zero $ succ $ succ $ var "e") (lam "a" $ succ $ var "a")))
tFailLetInPairSnd = root $ (anno (Prod Nat (Fun Nat Nat)) (pair (lam "n" $ var "n") (let' "e" zero $ succ $ succ $ var "e")))
tFailInL = root $ (anno (Sum Nat Nat) (inl (pair zero zero)))
tFailInL = root $ (anno (Sum Nat Nat) (inl (lam "b" zero)))
tFailInR = root $ (anno (Sum Nat Nat) (inr (lam "x" $ var "x")))
tFailCaseUnequalReturnTypes = root $ (anno (Prod Nat Nat) (case' (anno Nat (inl $ succ $ succ zero)) "a" (pair zero zero) "b" zero))
tFailCaseUnequalReturnTypes = root $ (anno (Fun Nat Nat) (case' (anno Nat (inl $ succ $ succ zero)) "a" (lam "x" (add (var "a") zero)) "b" zero))
tFailCaseRightShadowBinding = root $ (let' "a" zero (anno Nat (case' (anno (Sum Nat (Fun Nat Nat)) (inr $ lam "x" zero)) "a" zero "b" (var "b"))))
This diff is collapsed.
......@@ -14,12 +14,11 @@
<child id="5790571747095872621" name="elems" index="1gj3CY" />
</concept>
<concept id="1894367444356278387" name="SumTypes.structure.Case" flags="ng" index="1SCoPk">
<property id="7315585726620957708" name="name2" index="aFH9T" />
<property id="7315585726620957706" name="name1" index="aFH9Z" />
<child id="1894367444356278392" name="matchee" index="1SCoPv" />
<child id="1894367444356278454" name="c1" index="1SCoQh" />
<child id="1894367444356278461" name="c2" index="1SCoQq" />
</concept>
<concept id="1894367444356278442" name="SumTypes.structure.CaseCase" flags="ng" index="1SCoQd">
<child id="1894367444356278447" name="t" index="1SCoQ8" />
<child id="1894367444356278454" name="t1" index="1SCoQh" />
<child id="1894367444356278461" name="t2" index="1SCoQq" />
</concept>
<concept id="1894367444356272930" name="SumTypes.structure.Lam" flags="ng" index="1SCro5">
<child id="1894367444356272950" name="t" index="1SCroh" />
......@@ -65,6 +64,8 @@
<node concept="1SCrvP" id="7Sr$8awKhGn" role="1SCrpD" />
<node concept="1SCrpo" id="7Sr$8awKhGs" role="1SCrpP">
<node concept="1SCoPk" id="7Sr$8awKhGZ" role="1SCrqz">
<property role="aFH9Z" value="a" />
<property role="aFH9T" value="b" />
<node concept="1SCrpo" id="7Sr$8awKhHE" role="1SCoPv">
<node concept="1SCrp5" id="7Sr$8awKhIw" role="1SCrqz">
<node concept="1SCro5" id="7Sr$8awKhIS" role="1SCrp0">
......@@ -82,15 +83,9 @@
</node>
</node>
</node>
<node concept="1SCoQd" id="7Sr$8awKhH2" role="1SCoQh">
<property role="TrG5h" value="a" />
<node concept="1SCrvP" id="7Sr$8awKhJ4" role="1SCoQ8" />
</node>
<node concept="1SCoQd" id="7Sr$8awKhH5" role="1SCoQq">
<node concept="1SCrvP" id="4YOJ4IclD_x" role="1SCoQh" />
<node concept="1SCrv7" id="4YOJ4IclD_I" role="1SCoQq">
<property role="TrG5h" value="b" />
<node concept="1SCrv7" id="7Sr$8awKhJa" role="1SCoQ8">
<property role="TrG5h" value="b" />
</node>
</node>
</node>
<node concept="1SCrrb" id="7Sr$8awKhGz" role="1SCrrM" />
......
......@@ -14,12 +14,11 @@
<child id="5790571747095872621" name="elems" index="1gj3CY" />
</concept>
<concept id="1894367444356278387" name="SumTypes.structure.Case" flags="ng" index="1SCoPk">
<property id="7315585726620957708" name="name2" index="aFH9T" />
<property id="7315585726620957706" name="name1" index="aFH9Z" />
<child id="1894367444356278392" name="matchee" index="1SCoPv" />
<child id="1894367444356278454" name="c1" index="1SCoQh" />
<child id="1894367444356278461" name="c2" index="1SCoQq" />
</concept>
<concept id="1894367444356278442" name="SumTypes.structure.CaseCase" flags="ng" index="1SCoQd">
<child id="1894367444356278447" name="t" index="1SCoQ8" />
<child id="1894367444356278454" name="t1" index="1SCoQh" />
<child id="1894367444356278461" name="t2" index="1SCoQq" />
</concept>
<concept id="1894367444356272930" name="SumTypes.structure.Lam" flags="ng" index="1SCro5">
<child id="1894367444356272950" name="t" index="1SCroh" />
......@@ -58,6 +57,8 @@
<property role="TrG5h" value="test" />
<node concept="1SCrpo" id="7Sr$8awKhwx" role="2BHfFu">
<node concept="1SCoPk" id="7Sr$8awKhx1" role="1SCrqz">
<property role="aFH9Z" value="a" />
<property role="aFH9T" value="b" />
<node concept="1SCrpo" id="7Sr$8awKhxg" role="1SCoPv">
<node concept="1SCrpY" id="7Sr$8awKhxN" role="1SCrqz">
<node concept="1SCrvK" id="7Sr$8awKhyh" role="1SCrpT">
......@@ -68,22 +69,16 @@
</node>
<node concept="1SCrrb" id="7Sr$8awKhxn" role="1SCrrM" />
</node>
<node concept="1SCoQd" id="7Sr$8awKhx4" role="1SCoQh">
<property role="TrG5h" value="a" />
<node concept="1SCro5" id="7Sr$8awKhzr" role="1SCoQ8">
<property role="TrG5h" value="x" />
<node concept="1SCro_" id="7Sr$8awKhzy" role="1SCroh">
<node concept="1SCrv7" id="7Sr$8awKhzH" role="1SCrow">
<property role="TrG5h" value="a" />
</node>
<node concept="1SCrvP" id="7Sr$8awKhzL" role="1SCroG" />
<node concept="1SCro5" id="7Sr$8awKhzr" role="1SCoQh">
<property role="TrG5h" value="x" />
<node concept="1SCro_" id="7Sr$8awKhzy" role="1SCroh">
<node concept="1SCrv7" id="7Sr$8awKhzH" role="1SCrow">
<property role="TrG5h" value="a" />
</node>
<node concept="1SCrvP" id="7Sr$8awKhzL" role="1SCroG" />
</node>
</node>
<node concept="1SCoQd" id="7Sr$8awKhx7" role="1SCoQq">
<property role="TrG5h" value="b" />
<node concept="1SCrvP" id="7Sr$8awKhz2" role="1SCoQ8" />
</node>
<node concept="1SCrvP" id="4YOJ4IclD_m" role="1SCoQq" />
</node>
<node concept="1SCrqR" id="7Sr$8awKhwC" role="1SCrrM">
<node concept="1SCrrb" id="7Sr$8awKhwJ" role="1SCrqM" />
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment