the type checker may change the arity of an equation, so we handle it differently

This commit is contained in:
Krasimir Angelov
2026-02-13 12:23:14 +01:00
parent 14b4e82067
commit 3f35d779f1
16 changed files with 77 additions and 79 deletions
+13 -6
View File
@@ -92,7 +92,7 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
where
checkAbs js i@(c,info) =
case info of
AbsFun (Just (L loc ty)) _ _ _
AbsFun (Just (L loc ty)) _
-> do let mb_def = do
let (cxt,(_,i),_) = typeForm ty
info <- lookupIdent i js
@@ -134,7 +134,7 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
checkCnc js (c,info) =
case info of
CncFun _ d mn mf -> case lookupOrigInfo gr (am,c) of
Ok (_,AbsFun (Just (L loc ty)) _ _ _) ->
Ok (_,AbsFun (Just (L loc ty)) _) ->
do linty <- linTypeOfType gr cm (L loc ty)
return $ Map.insert c (CncFun (Just linty) d mn mf) js
_ -> do checkWarn ("function" <+> c <+> "is not in abstract")
@@ -160,16 +160,23 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
cont <- checkContext ga cont
update sm c (AbsCat (Just (L loc cont)))
AbsFun (Just (L loc typ)) ma md moper -> do
AbsFun (Just (L loc typ)) md -> do
chIn loc "the type of function" $
checkLType ga typ typeType
typ <- normalForm ga typ -- to calculate let definitions
md <- case md of
Just eqs -> do eqs <- mapM (\(L loc eq) -> chIn loc "the definition of function" $
Just (_,eqs) -> do eqs <- mapM (\(L loc eq) -> chIn loc "the definition of function" $
fmap (L loc) (checkDef ga (fst sm,c) typ eq)) eqs
return (Just eqs)
arity <-
case [length ps | L _ (ps,_) <- eqs] of
[] -> return 0
(arity : as)
| all (==arity) as -> return arity
_ -> checkError ("The following equations have different arities" $$
nest 4 (vcat [ppQIdent Unqualified (fst sm,c) <+> hsep (map (ppPatt Unqualified 2) ps) | L _ (ps,_) <- eqs]))
return (Just (arity,eqs))
Nothing -> return Nothing
update sm c (AbsFun (Just (L loc typ)) ma md moper)
update sm c (AbsFun (Just (L loc typ)) md)
CncCat mty mdef mref mpr mpmcfg -> do
mty <- case mty of
+2 -2
View File
@@ -357,11 +357,11 @@ stdPredef g = Map.fromList
evalAbsDef :: Globals -> Choice -> QIdent -> [Value] -> Value
evalAbsDef g@(Gl gr pds _) c q args =
case lookupAbsDef gr q of
Ok (Just arity,Just eqs) ->
Ok (Just (arity,eqs)) ->
case splitAt' arity args of
Nothing -> VPAP c q args
Just (_,_) -> patternMatch g c (VConst q args) (map (\(ps,t) -> ([],ps,args,t)) eqs)
Ok (_,Nothing) -> VConst q args
Ok Nothing -> VConst q args
Bad msg -> error msg
apply g (VMeta i vs0) vs = VMeta i (vs0++vs)
+3 -3
View File
@@ -53,7 +53,7 @@ compileEquations gr arity st (i:is) eqs fl bs = whilePP eqs Map.empty
whilePV ((vs, PV x : ps, t):eqs) vrs
| x == identW = whilePV eqs (( vs,ps,t) : vrs)
| otherwise = whilePV eqs (((x,i):vs,ps,t) : vrs)
whilePV ((vs, PTilde _ : ps, t):eqs) vrs = whilePV ((vs,ps,t) : eqs) vrs
whilePV ((vs, PTilde _ : ps, t):eqs) vrs = whilePV eqs (( vs,ps,t) : vrs)
whilePV ((vs, PImplArg p:ps, t):eqs) vrs = whilePV ((vs,p:ps,t):eqs) vrs
whilePV ((vs, PT _ p : ps, t):eqs) vrs = whilePV ((vs,p:ps,t):eqs) vrs
whilePV eqs vrs = let fl1 = Just (st,length bs1)
@@ -104,7 +104,7 @@ compileFun gr eval st vs (App e1 e2) h0 bs args =
in (h2,bs2,is1++is2)
compileFun gr eval st vs (Q q@(m,id)) h0 bs args =
case lookupAbsDef gr q of
Ok (_,Just _)
Ok (Just _)
-> (h0,bs,eval st (GLOBAL (showIdent id)) args)
_ -> let Ok ty = lookupFunType gr q
(ctxt,_,_) = typeForm ty
@@ -167,7 +167,7 @@ compileFun gr eval st vs e _ _ _ = error (show e)
compileArg gr st vs (Q q@(m,id)) h0 bs =
case lookupAbsDef gr q of
Ok (_,Just _) -> (h0,bs,GLOBAL (showIdent id),[])
Ok (Just _) -> (h0,bs,GLOBAL (showIdent id),[])
_ -> let Ok ty = lookupFunType gr q
(ctxt,_,_) = typeForm ty
c_arity = length ctxt
+9 -10
View File
@@ -82,13 +82,13 @@ grammar2PGF opts mb_pgf gr am probs = do
((m,c),AbsCat (Just (L _ cont))) <- adefs, let c' = i2i c]
funs = [(f', mkType [] ty, arity, bcode, toLogProb (fromMaybe 0 (Map.lookup f' funs_probs))) |
((m,f),AbsFun (Just (L _ ty)) ma mdef _) <- adefs,
let arity = mkArity ma mdef ty,
let bcode = mkDef gr arity mdef,
((m,f),AbsFun (Just (L _ ty)) mdef) <- adefs,
let arity = mkArity mdef ty,
let bcode = mkDef gr mdef,
let f' = i2i f]
funs_probs = (Map.fromList . concat . Map.elems . fmap pad . Map.fromListWith (++))
[(i2i cat,[(i2i f,Map.lookup f' probs)]) | ((m,f),AbsFun (Just (L _ ty)) _ _ _) <- adefs,
[(i2i cat,[(i2i f,Map.lookup f' probs)]) | ((m,f),AbsFun (Just (L _ ty)) _) <- adefs,
let (_,(_,cat),_) = GM.typeForm ty,
let f' = i2i f]
where
@@ -167,13 +167,12 @@ mkContext scope hyps = mapAccumL (\scope (bt,x,ty) -> let ty' = mkType scope ty
then ( scope,(bt,i2i x,ty'))
else (x:scope,(bt,i2i x,ty'))) scope hyps
mkDef gr arity (Just eqs) = generateByteCode gr arity eqs
mkDef gr arity Nothing = []
mkDef gr (Just (arity,eqs)) = generateByteCode gr arity eqs
mkDef gr Nothing = []
mkArity (Just a) _ ty = a -- known arity, i.e. defined function
mkArity Nothing (Just _) ty = 0 -- defined function with no arity - must be an axiom
mkArity Nothing _ ty = let (ctxt, _, _) = GM.typeForm ty -- constructor
in length ctxt
mkArity (Just (a,_)) ty = a -- known arity, i.e. defined function
mkArity Nothing ty = let (ctxt, _, _) = GM.typeForm ty -- constructor
in length ctxt
{-
genCncCats gr am cm cdefs = mkCncCats 0 cdefs
where
+2 -2
View File
@@ -106,7 +106,7 @@ renameIdentTerm' env@(act,imps) t0 =
info2status :: Maybe ModuleName -> Ident -> Info -> Term
info2status mq c i = case i of
AbsCat _ -> maybe Con (curry QC) mq c
AbsFun _ _ Nothing _ -> maybe Con (curry QC) mq c
AbsFun _ Nothing -> maybe Con (curry QC) mq c
ResValue _ _ -> maybe Con (curry QC) mq c
ResParam _ _ -> maybe Con (curry QC) mq c
AnyInd True m -> maybe Con (const (curry QC m)) mq c
@@ -159,7 +159,7 @@ renameInfo :: FilePath -> Status -> Module -> Ident -> Info -> Check Info
renameInfo cwd status (m,mi) i info =
case info of
AbsCat pco -> liftM AbsCat (renPerh (renameContext status) pco)
AbsFun pty pa ptr poper -> liftM4 AbsFun (renTerm pty) (return pa) (renMaybe (mapM (renLoc (renEquation status))) ptr) (return poper)
AbsFun pty ptr -> liftM2 AbsFun (renTerm pty) (renMaybe (\(a,eqs) -> fmap ((,) a) (mapM (renLoc (renEquation status)) eqs)) ptr)
ResOper pty ptr -> liftM2 ResOper (renTerm pty) (renTerm ptr)
ResOverload os tysts -> liftM (ResOverload os) (mapM (renPair (renameTerm status [])) tysts)
ResParam (Just pp) m -> do
+2 -2
View File
@@ -28,8 +28,8 @@ getLocalTags x (m,mi) =
where
getLocations :: Info -> [(String,String,String)]
getLocations (AbsCat mb_ctxt) = maybe (loc "cat") mb_ctxt
getLocations (AbsFun mb_type _ mb_eqs _) = maybe (ltype "fun") mb_type ++
maybe (list (loc "def")) mb_eqs
getLocations (AbsFun mb_type mb_eqs) = maybe (ltype "fun") mb_type ++
maybe (list (loc "def") . snd) mb_eqs
getLocations (ResParam mb_params _) = maybe (loc "param") mb_params
getLocations (ResValue mb_type _) = ltype "param-value" mb_type
getLocations (ResOper mb_type mb_def) = maybe (ltype "oper-type") mb_type ++
+8 -11
View File
@@ -174,14 +174,14 @@ extendMod gr isCompl ((name,mi),cond) base new = foldM try new $ Map.toList (jme
(b,n') = case info of
ResValue _ _ -> (True,n)
ResParam _ _ -> (True,n)
AbsFun _ _ Nothing _ -> (True,n)
AbsFun _ Nothing -> (True,n)
AnyInd b k -> (b,k)
_ -> (False,n) ---- canonical in Abs
globalizeLoc fpath i =
case i of
AbsCat mc -> AbsCat (fmap gl mc)
AbsFun mt ma md moper -> AbsFun (fmap gl mt) ma (fmap (fmap gl) md) moper
AbsFun mt md -> AbsFun (fmap gl mt) (fmap (\(a,eqs) -> (a,fmap gl eqs)) md)
ResParam mt mv -> ResParam (fmap gl mt) mv
ResValue t i -> ResValue (gl t) i
ResOper mt m -> ResOper (fmap gl mt) (fmap gl m)
@@ -200,8 +200,8 @@ unifyAnyInfo :: ModuleName -> Info -> Info -> Err Info
unifyAnyInfo m i j = case (i,j) of
(AbsCat mc1, AbsCat mc2) ->
liftM AbsCat (unifyMaybeL mc1 mc2)
(AbsFun mt1 ma1 md1 moper1, AbsFun mt2 ma2 md2 moper2) ->
liftM4 AbsFun (unifyMaybeL mt1 mt2) (unifAbsArrity ma1 ma2) (unifAbsDefs md1 md2) (unifyMaybe moper1 moper2) -- adding defs
(AbsFun mt1 md1, AbsFun mt2 md2) ->
liftM2 AbsFun (unifyMaybeL mt1 mt2) (unifAbsDefs md1 md2) -- adding defs
(ResParam mt1 mv1, ResParam mt2 mv2) ->
liftM2 ResParam (unifyMaybeL mt1 mt2) (unifyMaybe mv1 mv2)
@@ -229,10 +229,7 @@ unifyAnyInfo m i j = case (i,j) of
unifyMaybeL :: Eq a => Maybe (L a) -> Maybe (L a) -> Err (Maybe (L a))
unifyMaybeL = unifyMaybeBy unLoc
unifAbsArrity :: Maybe Int -> Maybe Int -> Err (Maybe Int)
unifAbsArrity = unifyMaybe
unifAbsDefs :: Maybe [L Equation] -> Maybe [L Equation] -> Err (Maybe [L Equation])
unifAbsDefs (Just xs) (Just ys) = return (Just (xs ++ ys))
unifAbsDefs Nothing Nothing = return Nothing
unifAbsDefs _ _ = fail ""
unifAbsDefs :: Maybe (Int,[L Equation]) -> Maybe (Int,[L Equation]) -> Err (Maybe (Int,[L Equation]))
unifAbsDefs (Just (_,xs)) (Just (_,ys)) = return (Just (0,xs ++ ys))
unifAbsDefs Nothing Nothing = return Nothing
unifAbsDefs _ _ = fail ""
+3 -3
View File
@@ -27,7 +27,7 @@ stripSourceGrammar sgr = mGrammar [(i, m{jments = Map.map stripInfo (jments m)})
stripInfo :: Info -> Info
stripInfo i = case i of
AbsCat _ -> i
AbsFun mt mi me mb -> AbsFun mt mi Nothing mb
AbsFun mt me -> AbsFun mt Nothing
ResParam mp mt -> ResParam mp Nothing
ResValue lt _ -> i ----
ResOper mt md -> ResOper mt Nothing
@@ -116,8 +116,8 @@ sizePatt p = case p of
sizeInfo :: Info -> Int
sizeInfo i = case i of
AbsCat (Just (L _ co)) -> 1 + sum [1 + sizeTerm ty | (_,_,ty) <- co]
AbsFun mt mi me mb -> 1 + msize mt +
sum [sum (map sizePatt ps) + sizeTerm t | Just es <- [me], L _ (ps,t) <- es]
AbsFun mt me -> 1 + msize mt +
sum [sum (map sizePatt ps) + sizeTerm t | Just (_,es) <- [me], L _ (ps,t) <- es]
ResParam mp mt ->
1 + sum [1 + sum [1 + sizeTerm ty | (_,_,ty) <- co] | Just (L _ ps) <- [mp], (_,co) <- ps]
ResValue _ _ -> 0
+2 -2
View File
@@ -105,7 +105,7 @@ instance Binary Rule where
instance Binary Info where
put (AbsCat x) = putWord8 0 >> put x
put (AbsFun w x y z) = putWord8 1 >> put (w,x,y,z)
put (AbsFun x y) = putWord8 1 >> put (x,y)
put (ResParam x y) = putWord8 2 >> put (x,y)
put (ResValue x y) = putWord8 3 >> put (x,y)
put (ResOper x y) = putWord8 4 >> put (x,y)
@@ -116,7 +116,7 @@ instance Binary Info where
get = do tag <- getWord8
case tag of
0 -> get >>= \x -> return (AbsCat x)
1 -> get >>= \(w,x,y,z) -> return (AbsFun w x y z)
1 -> get >>= \(x,y) -> return (AbsFun x y)
2 -> get >>= \(x,y) -> return (ResParam x y)
3 -> get >>= \(x,y) -> return (ResValue x y)
4 -> get >>= \(x,y) -> return (ResOper x y)
+2 -2
View File
@@ -323,8 +323,8 @@ allConcreteModules gr =
-- and indirection to module (/INDIR/)
data Info =
-- judgements in abstract syntax
AbsCat (Maybe (L Context)) -- ^ (/ABS/) context of a category
| AbsFun (Maybe (L Type)) (Maybe Int) (Maybe [L Equation]) (Maybe Bool) -- ^ (/ABS/) type, arrity and definition of a function
AbsCat (Maybe (L Context)) -- ^ (/ABS/) context of a category
| AbsFun (Maybe (L Type)) (Maybe (Int,[L Equation])) -- ^ (/ABS/) type, arrity and definition of a function
-- judgements in resource
| ResParam (Maybe (L [Param])) (Maybe ([Term],Int)) -- ^ (/RES/) The second argument is list of all possible values
+3 -3
View File
@@ -34,11 +34,11 @@ info2json (AbsCat mb_ctxt) =
case mb_ctxt of
Nothing -> makeObj []
Just (L _ ctxt) -> makeObj [("context", showJSON (map hypo2json ctxt))]
info2json (AbsFun mb_ty mb_arity mb_eqs _) =
info2json (AbsFun mb_ty mb_eqs) =
(makeObj . catMaybes)
[ fmap (\(L _ ty) -> ("abstype",term2json ty)) mb_ty
, fmap (\a -> ("arity",showJSON a)) mb_arity
, fmap (\eqs -> ("equations",showJSON (map (\(L _ eq) -> equation2json eq) eqs))) mb_eqs
, fmap (\(a,_) -> ("arity",showJSON a)) mb_eqs
, fmap (\(_,eqs) -> ("equations",showJSON (map (\(L _ eq) -> equation2json eq) eqs))) mb_eqs
]
info2json (ResParam mb_params _) =
makeObj [("params", case mb_params of
+13 -13
View File
@@ -226,13 +226,13 @@ countParamValues gr ptyp =
-- to normalize records and record types
sortByLbl = sortBy (\(l1,_,_) (l2,_,_) -> compare l1 l2)
lookupAbsDef :: ErrorMonad m => Grammar -> QIdent -> m (Maybe Int,Maybe [Equation])
lookupAbsDef :: ErrorMonad m => Grammar -> QIdent -> m (Maybe (Int,[Equation]))
lookupAbsDef gr q@(m,c) = errIn (render ("looking up absdef of" <+> c)) $ do
info <- lookupQIdentInfo gr q
case info of
AbsFun _ a d _ -> return (a,fmap (map unLoc) d)
AnyInd _ n -> lookupAbsDef gr (n,c)
_ -> return (Nothing,Nothing)
AbsFun a d -> return (fmap (\(a,eqs) -> (a,map unLoc eqs)) d)
AnyInd _ n -> lookupAbsDef gr (n,c)
_ -> return Nothing
lookupLincat :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m Type
lookupLincat gr m c | isPredefCat c = return defLinType --- ad hoc; not needed?
@@ -253,11 +253,11 @@ lookupAbsType gr q@(m,c)
| otherwise = do
info <- lookupQIdentInfo gr q
case info of
AbsCat (Just (L _ co)) -> return (QC q,mkProd co typeType [])
AbsFun (Just (L _ t)) _ Nothing _ -> return (QC q,t)
AbsFun (Just (L _ t)) _ (Just _) _ -> return (Q q,t)
AnyInd _ n -> lookupAbsType gr (n,c)
_ -> no_type
AbsCat (Just (L _ co)) -> return (QC q,mkProd co typeType [])
AbsFun (Just (L _ t)) Nothing -> return (QC q,t)
AbsFun (Just (L _ t)) (Just _) -> return (Q q,t)
AnyInd _ n -> lookupAbsType gr (n,c)
_ -> no_type
where
no_type = raise (render ("cannot find type of" <+> c))
@@ -266,9 +266,9 @@ lookupFunType :: ErrorMonad m => Grammar -> QIdent -> m Type
lookupFunType gr q@(m,c) = do
info <- lookupQIdentInfo gr q
case info of
AbsFun (Just (L _ t)) _ _ _ -> return t
AnyInd _ n -> lookupFunType gr (n,c)
_ -> raise (render ("cannot find type of" <+> c))
AbsFun (Just (L _ t)) _ -> return t
AnyInd _ n -> lookupFunType gr (n,c)
_ -> raise (render ("cannot find type of" <+> c))
-- | this is needed at compile time
lookupCatContext :: ErrorMonad m => Grammar -> ModuleName -> Ident -> m Context
@@ -292,7 +292,7 @@ allOpers gr =
]
where
typesIn info = case info of
AbsFun (Just ltyp) _ _ _ -> [ltyp]
AbsFun (Just ltyp) _ -> [ltyp]
ResOper (Just ltyp) _ -> [ltyp]
ResValue ltyp _ -> [ltyp]
ResOverload _ tytrs -> [ltyp | (ltyp,_) <- tytrs]
+1 -1
View File
@@ -480,7 +480,7 @@ allDependencies ism b =
ResParam (Just (L loc ps)) _ -> [Just (L loc t) | (_,cont) <- ps, (_,_,t) <- cont]
CncCat pty _ _ _ _ -> [pty]
CncFun _ pt _ _ -> [pt] ---- (Maybe (Ident,(Context,Type))
AbsFun pty _ ptr _ -> [pty] --- ptr is def, which can be mutual
AbsFun pty ptr -> [pty] --- ptr is def, which can be mutual
AbsCat (Just (L loc co)) -> [Just (L loc ty) | (_,_,ty) <- co]
_ -> []
+9 -13
View File
@@ -253,19 +253,18 @@ CatDef
FunDef :: { [(Ident,Info)] }
FunDef
: Posn ListIdent ':' Exp Posn { [(fun, AbsFun (Just (mkL $1 $5 $4)) Nothing (Just []) (Just True)) | fun <- $2] }
: Posn ListIdent ':' Exp Posn { [(fun, AbsFun (Just (mkL $1 $5 $4)) (Just (0,[]))) | fun <- $2] }
DefDef :: { [(Ident,Info)] }
DefDef
: Posn LhsNames '=' Exp Posn { [(f, AbsFun Nothing (Just 0) (Just [mkL $1 $5 ([],$4)]) Nothing) | f <- $2] }
| Posn LhsName ListPatt '=' Exp Posn { [($2,AbsFun Nothing (Just (length $3)) (Just [mkL $1 $6 ($3,$5)]) Nothing)] }
: Posn LhsNames '=' Exp Posn { [(f, AbsFun Nothing (Just (0,[mkL $1 $5 ([],$4)]))) | f <- $2] }
| Posn LhsName ListPatt '=' Exp Posn { [($2,AbsFun Nothing (Just (0,[mkL $1 $6 ($3,$5)])))] }
DataDef :: { [(Ident,Info)] }
DataDef
: Posn Ident '=' ListDataConstr Posn { ($2, AbsCat Nothing) :
[(fun, AbsFun Nothing Nothing Nothing (Just True)) | fun <- $4] }
| Posn ListIdent ':' Exp Posn { -- (snd (valCat $4), AbsCat Nothing) :
[(fun, AbsFun (Just (mkL $1 $5 $4)) Nothing Nothing (Just True)) | fun <- $2] }
[(fun, AbsFun Nothing Nothing) | fun <- $4] }
| Posn ListIdent ':' Exp Posn { [(fun, AbsFun (Just (mkL $1 $5 $4)) Nothing) | fun <- $2] }
ParamDef :: { [(Ident,Info)] }
ParamDef
@@ -797,8 +796,8 @@ listCatDef (L loc (id,cont,size)) = [catd,nilfund,consfund]
consId = mkConsId id
catd = (listId, AbsCat (Just (L loc cont')))
nilfund = (baseId, AbsFun (Just (L loc niltyp)) Nothing Nothing (Just True))
consfund = (consId, AbsFun (Just (L loc constyp)) Nothing Nothing (Just True))
nilfund = (baseId, AbsFun (Just (L loc niltyp)) Nothing)
consfund = (consId, AbsFun (Just (L loc constyp)) Nothing)
cont' = [(b,mkId x i,ty) | (i,(b,x,ty)) <- zip [0..] cont]
xs = map (\(b,x,t) -> Vr x) cont'
@@ -854,12 +853,12 @@ isOverloading t =
checkInfoType mt jment@(id,info) =
case info of
AbsCat pcont -> ifAbstract mt (locPerh pcont)
AbsFun pty _ pde _ -> ifAbstract mt (locPerh pty ++ maybe [] locAll pde)
AbsFun pty pde -> ifAbstract mt (locPerh pty ++ maybe [] (locAll.snd) pde)
CncCat pty pd pr ppn _->ifConcrete mt (locPerh pty ++ locPerh pd ++ locPerh pr ++ locPerh ppn)
CncFun _ pd ppn _ -> ifConcrete mt (locPerh pd ++ locPerh ppn)
ResParam pparam _ -> ifResource mt (locPerh pparam)
ResValue ty _ -> ifResource mt (locL ty)
ResOper pty pt -> ifOper mt pty pt
ResOper pty pt -> ifResource mt (locPerh pty ++ locPerh pt)
ResOverload _ xs -> ifResource mt (concat [[loc1,loc2] | (L loc1 _,L loc2 _) <- xs])
where
locPerh = maybe [] locL
@@ -880,9 +879,6 @@ checkInfoType mt jment@(id,info) =
ifResource MTInterface locs = return jment
ifResource MTResource locs = return jment
ifResource _ locs = illegal locs
ifOper MTAbstract pty pt = return (id,AbsFun pty (fmap (const 0) pt) (Just (maybe [] (\(L l t) -> [L l ([],t)]) pt)) (Just False))
ifOper _ pty pt = return jment
mkAlts cs = case cs of
_:_ -> do
+3 -4
View File
@@ -93,17 +93,16 @@ ppJudgement q (id, AbsCat pcont ) =
(case pcont of
Just (L _ cont) -> hsep (map (ppDecl q) cont)
Nothing -> empty) <+> ';'
ppJudgement q (id, AbsFun ptype _ pexp poper) =
ppJudgement q (id, AbsFun ptype pexp) =
let kind | isNothing pexp = "data"
| poper == Just False = "oper"
| otherwise = "fun"
in
(case ptype of
Just (L _ typ) -> kind <+> id <+> ':' <+> ppTerm q 0 typ <+> ';'
Nothing -> empty) $$
(case pexp of
Just [] -> empty
Just eqs -> "def" <+> vcat [id <+> hsep (map (ppPatt q 2) ps) <+> '=' <+> ppTerm q 0 e <+> ';' | L _ (ps,e) <- eqs]
Just (_,[]) -> empty
Just (_,eqs) -> "def" <+> vcat [id <+> hsep (map (ppPatt q 2) ps) <+> '=' <+> ppTerm q 0 e <+> ';' | L _ (ps,e) <- eqs]
Nothing -> empty)
ppJudgement q (id, ResParam pparams _) =
"param" <+> id <+>
@@ -70,7 +70,7 @@ convAbsJment (cats,funs) (name,jment) =
fail "category with context"
let cat = convId name
return (cat:cats,funs)
AbsFun (Just lt) _ oeqns _ -> do unless (null (maybe [] id oeqns)) $
AbsFun (Just lt) oeqns -> do unless (null (maybe [] snd oeqns)) $
fail "function with equations"
let f = convId name
typ <- convType (unLoc lt)
@@ -150,7 +150,7 @@ jmentList = sortBy (compare `on` (jmentLocation.snd)) . Map.toList
jmentLocation jment =
case jment of
AbsCat ctxt -> fmap loc ctxt
AbsFun ty _ _ _ -> fmap loc ty
AbsFun ty _ -> fmap loc ty
ResParam ops _ -> fmap loc ops
CncCat ty _ _ _ _ ->fmap loc ty
ResOper ty rhs -> fmap loc rhs `mplus` fmap loc ty