Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Stop elaborator from labelling inductive data types

Now that we have the data and idata tactics, we do not need to label inductive data types when we elaborate them. This is good, because sometimes the elaborator would attach labels in the wrong places when doing generic programming.

The IDesc elaboration/distillation/pretty-printing code has been extended to support unlabelled |IMu|s, and Desc has been tidied up a little.
  • Loading branch information...
commit 8c6c80b7f6f0eb9036d7e92f7162a385e2b2b997 1 parent 6a2a16c
adam.gundry@cis.strath.ac.uk authored
View
79 src/Features/Desc.lhs
@@ -398,23 +398,10 @@ having a certain standard format, so it does not work in general.
> makeElab' loc (MU l d :>: DCON (foldr DPAIR DVOID (DTAG s : xs)))
-When elaborating |Mu| we can attach a label for display instead of the underlying
-description. This is often useful when constructing user-visible data types. It
-is not helpful when the description is a bound variable, however, so we check
-for that case and do not label it.
-
-> makeElab' loc (SET :>: DMU Nothing d) = do
-> dt :=>: dv <- subElab loc (desc :>: d)
-> if shouldLabel dv
-> then do name <- eAnchor
-> let anchor = ANCHOR (TAG name) SET ALLOWEDEPSILON
-> return $ MU (Just anchor) dt :=>: MU (Just anchor) dv
-> else return $ MU Nothing dt :=>: MU Nothing dv
-> where
-> shouldLabel :: VAL -> Bool
-> shouldLabel (NP (_ := DECL :<: _)) = False
-> shouldLabel _ = True
-
+The following case exists only for backwards compatibility (gah). It allows
+functions on inductive types to be constructed by writing |con| in the right places.
+It can disappear as soon as someone bothers to update the test suite.
+
> makeElab' loc (PI (MU l d) t :>: DCON f) = do
> d' :=>: _ <- eQuote d
> t' :=>: _ <- eQuote t
@@ -425,6 +412,8 @@ for that case and do not label it.
> return $ N ( inductionOp :@ [d', NP x, t', tm ])
> :=>: inductionOp @@ [d, NP x, t, tmv ]
+
+
> import -> DistillRules where
The following cases turn vaguely list-like data into actual lists.
@@ -460,43 +449,32 @@ then we can (probably) turn it into a tag applied to some arguments.
> unfold t = [t]
-If a label is not in scope, we remove it, so the definition appears at the
-appropriate place when the proof state is printed.
-
-> distill es (SET :>: tm@(C (Mu ltm@(Just _ :?=: _)))) = do
-> cc <- canTy (distill es) (Set :>: Mu ltm)
-> return ((DC $ fmap termOf cc) :=>: evTm tm)
-
-
-> import -> DInTmConstructors where
-
-> import -> DInTmPretty where
-
-> import -> Pretty where
-
\subsection{Adding Primitive references in Cochon}
> import -> Primitives where
> ("Desc", descREF) :
> ("DescD", descDREF) :
+> ("DescConstructors", descConstructorsREF) :
+> ("DescBranches", descBranchesREF) :
+
\subsection{Bootstrapping}
> import -> RulesCode where
-> inDesc :: VAL
-> inDesc = SUMD constructors
-> (L $ "c" :. [.c. N $
-> switchDOp :@ [ constructors , cases , NV c] ])
-> where constructors = (CONSE (TAG "idD")
+
+> descConstructors :: Tm {In, p} x
+> descConstructors = CONSE (TAG "idD")
> (CONSE (TAG "constD")
> (CONSE (TAG "sumD")
> (CONSE (TAG "prodD")
> (CONSE (TAG "sigmaD")
> (CONSE (TAG "piD")
-> NILE))))))
-> cases = (PAIR (CONSTD UNIT)
+> NILE)))))
+
+> descBranches :: Tm {In, p} x
+> descBranches = (PAIR (CONSTD UNIT)
> (PAIR (SIGMAD SET (L $ K $ CONSTD UNIT))
-> (PAIR (SIGMAD (enumU -$ []) (L $ "E" :. [._E.
+> (PAIR (SIGMAD enumU (L $ "E" :. [._E.
> (PRODD (TAG "T") (PID (ENUMT (NV _E)) (LK IDD))
> (CONSTD UNIT))]))
> (PAIR (SIGMAD UID (L $ "u" :. PRODD (TAG "C") IDD (PRODD (TAG "D") IDD (CONSTD UNIT))))
@@ -507,17 +485,28 @@ appropriate place when the proof state is printed.
> (PRODD (TAG "T") (PID (NV _S) (LK IDD))
> (CONSTD UNIT))]))
> VOID))))))
-> descFakeREF :: REF
-> descFakeREF = [("Primitive", 0), ("Desc", 0)] := (FAKE :<: SET)
-> desc :: VAL
-> desc = MU (Just (ANCHOR (TAG "Desc") SET ALLOWEDEPSILON)) inDesc
+
+> descD :: Tm {In, p} x
+> descD = SUMD descConstructors
+> (L $ "c" :. [.c. N $
+> switchDOp :@ [ descConstructors , descBranches , NV c] ])
+
+> desc :: Tm {In, p} x
+> desc = MU (Just (ANCHOR (TAG "Desc") SET ALLOWEDEPSILON)) descD
>
> descREF :: REF
-> descREF = [("Primitive", 0), ("Desc", 0)] := (DEFN desc :<: SET)
+> descREF = [("Primitive", 0), ("Desc", 0)] := DEFN desc :<: SET
>
> descDREF :: REF
-> descDREF = [("Primitive", 0), ("DescD", 0)] := (DEFN inDesc :<: desc)
+> descDREF = [("Primitive", 0), ("DescD", 0)] := DEFN descD :<: desc
+
+> descConstructorsREF :: REF
+> descConstructorsREF = [("Primitive", 0), ("DescConstructors", 0)] :=
+> DEFN descConstructors :<: enumU
+> descBranchesREF :: REF
+> descBranchesREF = [("Primitive", 0), ("DescBranches", 0)] :=
+> DEFN descBranches :<: branchesOp @@ [descConstructors, LK desc]
The |sumlike| function determines whether a value representing a description
is a sum or a sigma from an enumerate. If so, it returns |Just| the enumeration
View
23 src/Features/IDesc.lhs
@@ -25,7 +25,10 @@ index of |IMu| to make a fully applied anchor |DIMu|.
> traverseDTIN f (DIMu s i) = (|DIMu (traverse (traverseDTIN f) s) (traverseDTIN f i)|)
> import -> DInTmPretty where
-> pretty (DIMu (Just s :?=: _) _) = pretty s
+> pretty (DIMu (Just s :?=: _) _) = pretty s
+> pretty (DIMu (Nothing :?=: (Id ii :& Id d)) i) = wrapDoc
+> (kword KwIMu <+> pretty ii ArgSize <+> pretty d ArgSize <+> pretty i ArgSize)
+> AppSize
\subsection{Plugging Canonical terms in}
@@ -386,29 +389,13 @@ index of |IMu| to make a fully applied anchor |DIMu|.
> import -> DInTmParsersSpecial where
> (AndSize, (|(DIMU Nothing) (%keyword KwIMu%) (sizedDInTm ArgSize) (sizedDInTm ArgSize) (sizedDInTm ArgSize)|)) :
-
-Just like |Mu|, when elaborating |IMu| we attach a display label if the
-description is not neutral, to improve the pretty-printed representation.
-
> import -> MakeElabRules where
> makeElab' loc (SET :>: DIMU Nothing iI d i) = do
> iI :=>: iIv <- subElab loc (SET :>: iI)
> d :=>: dv <- subElab loc (ARR iIv (idesc $$ A iIv) :>: d)
> i :=>: iv <- subElab loc (iIv :>: i)
-
-> if shouldLabel dv
-> then do
-> name <- eAnchor
-> let anchor = ANCHOR (TAG name) SET ALLOWEDEPSILON
-> return $ IMU (Just (LK anchor)) iI d i
-> :=>: IMU (Just (LK anchor)) iIv dv iv
-> else return $ IMU Nothing iI d i
-> :=>: IMU Nothing iIv dv iv
-> where
-> shouldLabel :: VAL -> Bool
-> shouldLabel (N _) = False
-> shouldLabel _ = True
+> return $ IMU Nothing iI d i :=>: IMU Nothing iIv dv iv
> makeElab' loc (ty@(IMU _ _ _ _) :>: DTag s xs) =
> makeElab' loc (ty :>: DCON (DPAIR (DTAG s) (foldr DPAIR DU xs)))
View
6 test/results/BugDescLoop.pig.log
@@ -1,5 +1,5 @@
-[ElabTrace] Hole __infoElaborate_1.h3_2 started crying:
-Error: canTy: the proposed value [?r] is not of type h1
+[ElabTrace] Hole __infoElaborate_1.h2_1 started crying:
+Error: canTy: the proposed value [?r] is not of type Mu ('sigmaD (Enum ['leaf 'node]) [('constD (Sig ())) ('prodD 'l 'idD 'idD)])
Made.
-'node l h3
+'node l h2
Loaded.
View
2  test/results/BugEqgreenMu2.pig.log
@@ -1,3 +1,3 @@
FF && FF && FF
-(Q : :- ((: Set) h1) == ((: Set) h3))(s : h1) -> h3
+(Q : :- ((: Set) (Mu ('constD (Sig ())))) == ((: Set) (Mu ('sumD ['nil] [('constD (Sig ()))]))))(s : Mu ('constD (Sig ()))) -> Mu ('sumD ['nil] [('constD (Sig ()))])
Loaded.
Please sign in to comment.
Something went wrong with that request. Please try again.