git.iko.soy/Idris-dev
on 496cf41 help sign in
Idris-dev/src/Idris/AbsSyntax.hs
1110 lines 45 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
6import Core.TT
7import Core.Evaluate
8import Core.Elaborate hiding (Tactic(..))
9import Core.Typecheck
10import Idris.AbsSyntaxTree
11import IRTS.CodegenCommon
13import Paths_idris
15import System.Console.Haskeline
17import Control.Monad.State
19import Data.List
20import Data.Char
21import Data.Either
23import Debug.Trace
25import Util.Pretty
28getContext :: Idris Context
29getContext = do i <- get; return (tt_ctxt i)
31getObjectFiles :: Idris [FilePath]
32getObjectFiles = do i <- get; return (idris_objs i)
34addObjectFile :: FilePath -> Idris ()
35addObjectFile f = do i <- get; put (i { idris_objs = f : idris_objs i })
37getLibs :: Idris [String]
38getLibs = do i <- get; return (idris_libs i)
40addLib :: String -> Idris ()
41addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })
43addHdr :: String -> Idris ()
44addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })
46totcheck :: (FC, Name) -> Idris ()
47totcheck n = do i <- get; put (i { idris_totcheck = idris_totcheck i ++ [n] })
49setFlags :: Name -> [FnOpt] -> Idris ()
50setFlags n fs = do i <- get; put (i { idris_flags = addDef n fs (idris_flags i) })
52setAccessibility :: Name -> Accessibility -> Idris ()
53setAccessibility n a
54 = do i <- get
55 let ctxt = setAccess n a (tt_ctxt i)
56 put (i { tt_ctxt = ctxt })
58setTotality :: Name -> Totality -> Idris ()
59setTotality n a
60 = do i <- get
61 let ctxt = setTotal n a (tt_ctxt i)
62 put (i { tt_ctxt = ctxt })
64getTotality :: Name -> Idris Totality
65getTotality n
66 = do i <- get
67 case lookupTotal n (tt_ctxt i) of
68 [t] -> return t
69 _ -> return (Total [])
71addToCG :: Name -> CGInfo -> Idris ()
72addToCG n cg
73 = do i <- get
74 put (i { idris_callgraph = addDef n cg (idris_callgraph i) })
76addDocStr :: Name -> String -> Idris ()
77addDocStr n doc
78 = do i <- get
79 put (i { idris_docstrings = addDef n doc (idris_docstrings i) })
81addToCalledG :: Name -> [Name] -> Idris ()
82addToCalledG n ns = return () -- TODO
84-- Add a class instance function. Dodgy hack: Put integer instances first in the
85-- list so they are resolved by default.
86-- Dodgy hack 2: put constraint chasers (@@) last
88addInstance :: Bool -> Name -> Name -> Idris ()
89addInstance int n i
90 = do ist <- get
91 case lookupCtxt Nothing n (idris_classes ist) of
92 [CI a b c d ins] ->
93 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
94 put (ist { idris_classes = cs })
95 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
96 put (ist { idris_classes = cs })
97 where addI i ins | int = i : ins
98 | chaser n = ins ++ [i]
99 | otherwise = insI i ins
100 insI i [] = [i]
101 insI i (n : ns) | chaser n = i : n : ns
102 | otherwise = n : insI i ns
104 chaser (UN ('@':'@':_)) = True
105 chaser (NS n _) = chaser n
106 chaser _ = False
108addClass :: Name -> ClassInfo -> Idris ()
109addClass n i
110 = do ist <- get
111 let i' = case lookupCtxt Nothing n (idris_classes ist) of
112 [c] -> c { class_instances = class_instances i }
113 _ -> i
114 put (ist { idris_classes = addDef n i' (idris_classes ist) })
116addIBC :: IBCWrite -> Idris ()
117addIBC ibc@(IBCDef n)
118 = do i <- get
119 when (notDef (ibc_write i)) $
120 put (i { ibc_write = ibc : ibc_write i })
121 where notDef [] = True
122 notDef (IBCDef n': is) | n == n' = False
123 notDef (_ : is) = notDef is
124addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })
126clearIBC :: Idris ()
127clearIBC = do i <- get; put (i { ibc_write = [] })
129getHdrs :: Idris [String]
130getHdrs = do i <- get; return (idris_hdrs i)
132setErrLine :: Int -> Idris ()
133setErrLine x = do i <- get;
134 case (errLine i) of
135 Nothing -> put (i { errLine = Just x })
136 Just _ -> return ()
138clearErr :: Idris ()
139clearErr = do i <- get
140 put (i { errLine = Nothing })
142getSO :: Idris (Maybe String)
143getSO = do i <- get
144 return (compiled_so i)
146setSO :: Maybe String -> Idris ()
147setSO s = do i <- get
148 put (i { compiled_so = s })
150getIState :: Idris IState
151getIState = get
153putIState :: IState -> Idris ()
154putIState = put
156getName :: Idris Int
157getName = do i <- get;
158 let idx = idris_name i;
159 put (i { idris_name = idx + 1 })
160 return idx
162checkUndefined :: FC -> Name -> Idris ()
163checkUndefined fc n
164 = do i <- getContext
165 case lookupTy Nothing n i of
166 (_:_) -> fail $ show fc ++ ":" ++
167 show n ++ " already defined"
168 _ -> return ()
170isUndefined :: FC -> Name -> Idris Bool
171isUndefined fc n
172 = do i <- getContext
173 case lookupTy Nothing n i of
174 (_:_) -> return False
175 _ -> return True
177setContext :: Context -> Idris ()
178setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
180updateContext :: (Context -> Context) -> Idris ()
181updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
183addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
184addConstraints fc (v, cs)
185 = do i <- get
186 let ctxt = tt_ctxt i
187 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
188 next_tvar = v }
189 let ics = zip cs (repeat fc) ++ idris_constraints i
190 put (i { tt_ctxt = ctxt', idris_constraints = ics })
192addDeferred :: [(Name, Type)] -> Idris ()
193addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
194 i <- get
195 put (i { idris_metavars = map fst ns ++ idris_metavars i })
196 where tidyNames used (Bind (MN i x) b sc)
197 = let n' = uniqueName (UN x) used in
198 Bind n' b $ tidyNames (n':used) sc
199 tidyNames used (Bind n b sc)
200 = let n' = uniqueName n used in
201 Bind n' b $ tidyNames (n':used) sc
202 tidyNames used b = b
204solveDeferred :: Name -> Idris ()
205solveDeferred n = do i <- get
206 put (i { idris_metavars = idris_metavars i \\ [n] })
208iputStrLn :: String -> Idris ()
209iputStrLn = liftIO . putStrLn
211iWarn :: FC -> String -> Idris ()
212iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
214setLogLevel :: Int -> Idris ()
215setLogLevel l = do i <- get
216 let opts = idris_options i
217 let opt' = opts { opt_logLevel = l }
218 put (i { idris_options = opt' } )
220setCmdLine :: [Opt] -> Idris ()
221setCmdLine opts = do i <- get
222 let iopts = idris_options i
223 put (i { idris_options = iopts { opt_cmdline = opts } })
225getDumpDefun :: Idris (Maybe FilePath)
226getDumpDefun = do i <- get
227 return $ findC (opt_cmdline (idris_options i))
228 where findC [] = Nothing
229 findC (DumpDefun x : _) = Just x
230 findC (_ : xs) = findC xs
232getDumpCases :: Idris (Maybe FilePath)
233getDumpCases = do i <- get
234 return $ findC (opt_cmdline (idris_options i))
235 where findC [] = Nothing
236 findC (DumpCases x : _) = Just x
237 findC (_ : xs) = findC xs
239logLevel :: Idris Int
240logLevel = do i <- get
241 return (opt_logLevel (idris_options i))
243setErrContext :: Bool -> Idris ()
244setErrContext t = do i <- get
245 let opts = idris_options i
246 let opt' = opts { opt_errContext = t }
247 put (i { idris_options = opt' })
249errContext :: Idris Bool
250errContext = do i <- get
251 return (opt_errContext (idris_options i))
253useREPL :: Idris Bool
254useREPL = do i <- get
255 return (opt_repl (idris_options i))
257setREPL :: Bool -> Idris ()
258setREPL t = do i <- get
259 let opts = idris_options i
260 let opt' = opts { opt_repl = t }
261 put (i { idris_options = opt' })
263setTarget :: Target -> Idris ()
264setTarget t = do i <- get
265 let opts = idris_options i
266 let opt' = opts { opt_target = t }
267 put (i { idris_options = opt' })
269target :: Idris Target
270target = do i <- get
271 return (opt_target (idris_options i))
273setOutputTy :: OutputType -> Idris ()
274setOutputTy t = do i <- get
275 let opts = idris_options i
276 let opt' = opts { opt_outputTy = t }
277 put (i { idris_options = opt' })
279outputTy :: Idris OutputType
280outputTy = do i <- get
281 return $ opt_outputTy $ idris_options i
283verbose :: Idris Bool
284verbose = do i <- get
285 return (opt_verbose (idris_options i))
287setVerbose :: Bool -> Idris ()
288setVerbose t = do i <- get
289 let opts = idris_options i
290 let opt' = opts { opt_verbose = t }
291 put (i { idris_options = opt' })
293typeInType :: Idris Bool
294typeInType = do i <- get
295 return (opt_typeintype (idris_options i))
297setTypeInType :: Bool -> Idris ()
298setTypeInType t = do i <- get
299 let opts = idris_options i
300 let opt' = opts { opt_typeintype = t }
301 put (i { idris_options = opt' })
303coverage :: Idris Bool
304coverage = do i <- get
305 return (opt_coverage (idris_options i))
307setCoverage :: Bool -> Idris ()
308setCoverage t = do i <- get
309 let opts = idris_options i
310 let opt' = opts { opt_coverage = t }
311 put (i { idris_options = opt' })
313setIBCSubDir :: FilePath -> Idris ()
314setIBCSubDir fp = do i <- get
315 let opts = idris_options i
316 let opt' = opts { opt_ibcsubdir = fp }
317 put (i { idris_options = opt' })
319valIBCSubDir :: IState -> Idris FilePath
320valIBCSubDir i = return (opt_ibcsubdir (idris_options i))
322addImportDir :: FilePath -> Idris ()
323addImportDir fp = do i <- get
324 let opts = idris_options i
325 let opt' = opts { opt_importdirs = fp : opt_importdirs opts }
326 put (i { idris_options = opt' })
328setImportDirs :: [FilePath] -> Idris ()
329setImportDirs fps = do i <- get
330 let opts = idris_options i
331 let opt' = opts { opt_importdirs = fps }
332 put (i { idris_options = opt' })
334allImportDirs :: IState -> Idris [FilePath]
335allImportDirs i = do let optdirs = opt_importdirs (idris_options i)
336 return ("." : optdirs)
338impShow :: Idris Bool
339impShow = do i <- get
340 return (opt_showimp (idris_options i))
342setImpShow :: Bool -> Idris ()
343setImpShow t = do i <- get
344 let opts = idris_options i
345 let opt' = opts { opt_showimp = t }
346 put (i { idris_options = opt' })
348logLvl :: Int -> String -> Idris ()
349logLvl l str = do i <- get
350 let lvl = opt_logLevel (idris_options i)
351 when (lvl >= l)
352 $ do liftIO (putStrLn str)
353 put (i { idris_log = idris_log i ++ str ++ "\n" } )
355cmdOptType :: Opt -> Idris Bool
356cmdOptType x = do i <- get
357 return $ x `elem` opt_cmdline (idris_options i)
359iLOG :: String -> Idris ()
360iLOG = logLvl 1
362noErrors :: Idris Bool
363noErrors = do i <- get
364 case errLine i of
365 Nothing -> return True
366 _ -> return False
368setTypeCase :: Bool -> Idris ()
369setTypeCase t = do i <- get
370 let opts = idris_options i
371 let opt' = opts { opt_typecase = t }
372 put (i { idris_options = opt' })
375-- For inferring types of things
377bi = FC "builtin" 0
379inferTy = MN 0 "__Infer"
380inferCon = MN 0 "__infer"
381inferDecl = PDatadecl inferTy
382 PType
383 [("", inferCon, PPi impl (MN 0 "A") PType (
384 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))
385 (PRef bi inferTy)), bi)]
387infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]
388infP = P (TCon 6 0) inferTy (TType (UVal 0))
390getInferTerm, getInferType :: Term -> Term
391getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
392getInferTerm (App (App _ _) tm) = tm
393getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
395getInferType (Bind n b sc) = Bind n b $ getInferType sc
396getInferType (App (App _ ty) _) = ty
398-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
400primNames = [unitTy, unitCon,
401 falseTy, pairTy, pairCon,
402 eqTy, eqCon, inferTy, inferCon]
404unitTy = MN 0 "__Unit"
405unitCon = MN 0 "__II"
406unitDecl = PDatadecl unitTy PType
407 [("", unitCon, PRef bi unitTy, bi)]
409falseTy = MN 0 "__False"
410falseDecl = PDatadecl falseTy PType []
412pairTy = MN 0 "__Pair"
413pairCon = MN 0 "__MkPair"
414pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
415 [("", pairCon, PPi impl (n "A") PType (
416 PPi impl (n "B") PType (
417 PPi expl (n "a") (PRef bi (n "A")) (
418 PPi expl (n "b") (PRef bi (n "B"))
419 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
420 pexp (PRef bi (n "B"))])))), bi)]
421 where n a = MN 0 a
423eqTy = UN "="
424eqCon = UN "refl"
425eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),
426 (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]
427 PType)
428 [("", eqCon, PPi impl (n "a") PType (
429 PPi impl (n "x") (PRef bi (n "a"))
430 (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,
431 pimp (n "b") Placeholder,
432 pexp (PRef bi (n "x")),
433 pexp (PRef bi (n "x"))])), bi)]
434 where n a = MN 0 a
436-- Defined in builtins.idr
437sigmaTy = UN "Exists"
438existsCon = UN "Ex_intro"
440piBind :: [(Name, PTerm)] -> PTerm -> PTerm
441piBind = piBindp expl
443piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
444piBindp p [] t = t
445piBindp p ((n, ty):ns) t = PPi p n ty (piBind ns t)
447-- Dealing with parameters
449expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
450 [Name] -> -- all names
451 [Name] -> -- names with no declaration
452 PTerm -> PTerm
453expandParams dec ps ns infs tm = en tm
454 where
455 -- if we shadow a name (say in a lambda binding) that is used in a call to
456 -- a lifted function, we need access to both names - once in the scope of the
457 -- binding and once to call the lifted functions. So we'll explicitly shadow
458 -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
459 -- but we didn't...)
461 mkShadow (UN n) = MN 0 n
462 mkShadow (MN i n) = MN (i+1) n
463 mkShadow (NS x s) = NS (mkShadow x) s
465 en (PLam n t s)
466 | n `elem` map fst ps
467 = let n' = mkShadow n in
468 PLam n' (en t) (en (shadow n n' s))
469 | otherwise = PLam n (en t) (en s)
470 en (PPi p n t s)
471 | n `elem` map fst ps
472 = let n' = mkShadow n in
473 PPi p n' (en t) (en (shadow n n' s))
474 | otherwise = PPi p n (en t) (en s)
475 en (PLet n ty v s)
476 | n `elem` map fst ps
477 = let n' = mkShadow n in
478 PLet n' (en ty) (en v) (en (shadow n n' s))
479 | otherwise = PLet n (en ty) (en v) (en s)
480 en (PEq f l r) = PEq f (en l) (en r)
481 en (PTyped l r) = PTyped (en l) (en r)
482 en (PPair f l r) = PPair f (en l) (en r)
483 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
484 en (PAlternative a as) = PAlternative a (map en as)
485 en (PHidden t) = PHidden (en t)
486 en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
487 en (PProof ts) = PProof (map (fmap en) ts)
488 en (PTactics ts) = PTactics (map (fmap en) ts)
490 en (PQuote (Var n))
491 | n `nselem` ns = PQuote (Var (dec n))
492 en (PApp fc (PInferRef fc' n) as)
493 | n `nselem` ns = PApp fc (PInferRef fc' (dec n))
494 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
495 en (PApp fc (PRef fc' n) as)
496 | n `elem` infs = PApp fc (PInferRef fc' (dec n))
497 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
498 | n `nselem` ns = PApp fc (PRef fc' (dec n))
499 (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))
500 en (PRef fc n)
501 | n `elem` infs = PApp fc (PInferRef fc (dec n))
502 (map (pexp . (PRef fc)) (map fst ps))
503 | n `nselem` ns = PApp fc (PRef fc (dec n))
504 (map (pexp . (PRef fc)) (map fst ps))
505 en (PInferRef fc n)
506 | n `nselem` ns = PApp fc (PInferRef fc (dec n))
507 (map (pexp . (PRef fc)) (map fst ps))
508 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
509 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
510 en t = t
512 nselem x [] = False
513 nselem x (y : xs) | nseq x y = True
514 | otherwise = nselem x xs
516 nseq x y = nsroot x == nsroot y
518expandParamsD :: Bool -> -- True = RHS only
519 IState ->
520 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
521expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
522 = if n `elem` ns && (not rhsonly)
523 then -- trace (show (n, expandParams dec ps ns ty)) $
524 PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns [] ty))
525 else --trace (show (n, expandParams dec ps ns ty)) $
526 PTy doc syn fc o n (expandParams dec ps ns [] ty)
527expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
528 = if n `elem` ns && (not rhsonly)
529 then -- trace (show (n, expandParams dec ps ns ty)) $
530 PPostulate doc syn fc o (dec n) (piBind ps
531 (expandParams dec ps ns [] ty))
532 else --trace (show (n, expandParams dec ps ns ty)) $
533 PPostulate doc syn fc o n (expandParams dec ps ns [] ty)
534expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
535 = let n' = if n `elem` ns then dec n else n in
536 PClauses fc opts n' (map expandParamsC cs)
537 where
538 expandParamsC (PClause fc n lhs ws rhs ds)
539 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
540 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
541 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
542 n' = if n `elem` ns then dec n else n in
543 PClause fc n' lhs'
544 (map (expandParams dec ps'' ns []) ws)
545 (expandParams dec ps'' ns [] rhs)
546 (map (expandParamsD True ist dec ps'' ns) ds)
547 expandParamsC (PWith fc n lhs ws wval ds)
548 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
549 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
550 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
551 n' = if n `elem` ns then dec n else n in
552 PWith fc n' lhs'
553 (map (expandParams dec ps'' ns []) ws)
554 (expandParams dec ps'' ns [] wval)
555 (map (expandParamsD rhsonly ist dec ps'' ns) ds)
556 updateps yn nm [] = []
557 updateps yn nm (((a, t), i):as)
558 | (a `elem` nm) == yn = (a, t) : updateps yn nm as
559 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as
560expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
561 = PData doc syn fc co (expandPData pd)
562 where
563 -- just do the type decl, leave constructors alone (parameters will be
564 -- added implicitly)
565 expandPData (PDatadecl n ty cons)
566 = if n `elem` ns
567 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
568 (map econ cons)
569 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
570 econ (doc, n, t, fc)
571 = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)
572expandParamsD rhs ist dec ps ns (PParams f params pds)
573 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
574 (map (expandParamsD True ist dec ps ns) pds)
575-- (map (expandParamsD ist dec ps ns) pds)
576expandParamsD rhs ist dec ps ns (PMutual f pds)
577 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
578expandParamsD rhs ist dec ps ns (PClass doc info f cs n params decls)
579 = PClass doc info f
580 (map (expandParams dec ps ns []) cs)
581 n
582 (map (mapsnd (expandParams dec ps ns [])) params)
583 (map (expandParamsD rhs ist dec ps ns) decls)
584expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
585 = PInstance info f
586 (map (expandParams dec ps ns []) cs)
587 n
588 (map (expandParams dec ps ns []) params)
589 (expandParams dec ps ns [] ty)
590 cn
591 (map (expandParamsD rhs ist dec ps ns) decls)
592expandParamsD rhs ist dec ps ns d = d
594mapsnd f (x, t) = (x, f t)
596-- Calculate a priority for a type, for deciding elaboration order
597-- * if it's just a type variable or concrete type, do it early (0)
598-- * if there's only type variables and injective constructors, do it next (1)
599-- * if there's a function type, next (2)
600-- * finally, everything else (3)
602getPriority :: IState -> PTerm -> Int
603getPriority i tm = 1 -- pri tm
604 where
605 pri (PRef _ n) =
606 case lookupP Nothing n (tt_ctxt i) of
607 ((P (DCon _ _) _ _):_) -> 1
608 ((P (TCon _ _) _ _):_) -> 1
609 ((P Ref _ _):_) -> 1
610 [] -> 0 -- must be locally bound, if it's not an error...
611 pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
612 pri (PTrue _) = 0
613 pri (PFalse _) = 0
614 pri (PRefl _ _) = 1
615 pri (PEq _ l r) = max 1 (max (pri l) (pri r))
616 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
617 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
618 pri (PTyped l r) = pri l
619 pri (PPair _ l r) = max 1 (max (pri l) (pri r))
620 pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
621 pri (PAlternative a as) = maximum (map pri as)
622 pri (PConstant _) = 0
623 pri Placeholder = 1
624 pri _ = 3
626addStatics :: Name -> Term -> PTerm -> Idris ()
627addStatics n tm ptm =
628 do let (statics, dynamics) = initStatics tm ptm
629 let stnames = nub $ concatMap freeNames (map snd statics)
630 let dnames = nub $ concatMap freeNames (map snd dynamics)
631 when (not (null statics)) $
632 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics
633 ++ "\n" ++ show stnames ++ "\n" ++ show dnames
634 let statics' = nub $ map fst statics ++
635 filter (\x -> not (elem x dnames)) stnames
636 let stpos = staticList statics' tm
637 i <- get
638 put (i { idris_statics = addDef n stpos (idris_statics i) })
639 addIBC (IBCStatic n)
640 where
641 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)
642 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
643 if pstatic p == Static then ((n, ty) : static, dynamic)
644 else (static, (n, ty) : dynamic)
645 initStatics t pt = ([], [])
647 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc
648 staticList _ _ = []
650-- Dealing with implicit arguments
652-- Add implicit Pi bindings for any names in the term which appear in an
653-- argument position.
655-- This has become a right mess already. Better redo it some time...
657implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
658implicit syn n ptm = implicit' syn [] n ptm
660implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
661implicit' syn ignore n ptm
662 = do i <- get
663 let (tm', impdata) = implicitise syn ignore i ptm
664-- let (tm'', spos) = findStatics i tm'
665 put (i { idris_implicits = addDef n impdata (idris_implicits i) })
666 addIBC (IBCImp n)
667 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
668-- i <- get
669-- put (i { idris_statics = addDef n spos (idris_statics i) })
670 return tm'
672implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
673implicitise syn ignore ist tm
674 = let (declimps, ns') = execState (imps True [] tm) ([], [])
675 ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
676 ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in
677 if null ns
678 then (tm, reverse declimps)
679 else implicitise syn ignore ist (pibind uvars ns tm)
680 where
681 uvars = using syn
682 pvars = syn_params syn
684 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
685 | otherwise = x : dropAll xs ys
686 dropAll [] ys = []
688 imps top env (PApp _ f as)
689 = do (decls, ns) <- get
690 let isn = concatMap (namesIn uvars ist) (map getTm as)
691 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
692 imps top env (PPi (Imp l _ doc) n ty sc)
693 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
694 (decls , ns) <- get
695 put (PImp (getPriority ist ty) l n ty doc : decls,
696 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
697 imps True (n:env) sc
698 imps top env (PPi (Exp l _ doc) n ty sc)
699 = do let isn = nub (namesIn uvars ist ty ++ case sc of
700 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
701 _ -> [])
702 (decls, ns) <- get -- ignore decls in HO types
703 put (PExp (getPriority ist ty) l ty doc : decls,
704 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
705 imps True (n:env) sc
706 imps top env (PPi (Constraint l _ doc) n ty sc)
707 = do let isn = nub (namesIn uvars ist ty ++ case sc of
708 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
709 _ -> [])
710 (decls, ns) <- get -- ignore decls in HO types
711 put (PConstraint 10 l ty doc : decls,
712 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
713 imps True (n:env) sc
714 imps top env (PPi (TacImp l _ scr doc) n ty sc)
715 = do let isn = nub (namesIn uvars ist ty ++ case sc of
716 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
717 _ -> [])
718 (decls, ns) <- get -- ignore decls in HO types
719 put (PTacImplicit 10 l n scr ty doc : decls,
720 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
721 imps True (n:env) sc
722 imps top env (PEq _ l r)
723 = do (decls, ns) <- get
724 let isn = namesIn uvars ist l ++ namesIn uvars ist r
725 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
726 imps top env (PTyped l r)
727 = imps top env l
728 imps top env (PPair _ l r)
729 = do (decls, ns) <- get
730 let isn = namesIn uvars ist l ++ namesIn uvars ist r
731 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
732 imps top env (PDPair _ (PRef _ n) t r)
733 = do (decls, ns) <- get
734 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
735 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
736 imps top env (PDPair _ l t r)
737 = do (decls, ns) <- get
738 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
739 namesIn uvars ist r
740 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
741 imps top env (PAlternative a as)
742 = do (decls, ns) <- get
743 let isn = concatMap (namesIn uvars ist) as
744 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
745 imps top env (PLam n ty sc)
746 = do imps False env ty
747 imps False (n:env) sc
748 imps top env (PHidden tm) = imps False env tm
749 imps top env _ = return ()
751 pibind using [] sc = sc
752 pibind using (n:ns) sc
753 = case lookup n using of
754 Just ty -> PPi (Imp False Dynamic "") n ty (pibind using ns sc)
755 Nothing -> PPi (Imp False Dynamic "") n Placeholder
756 (pibind using ns sc)
758-- Add implicit arguments in function calls
759addImplPat :: IState -> PTerm -> PTerm
760addImplPat = addImpl' True [] []
762addImplBound :: IState -> [Name] -> PTerm -> PTerm
763addImplBound ist ns = addImpl' False ns [] ist
765addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
766addImplBoundInf ist ns inf = addImpl' False ns inf ist
768addImpl :: IState -> PTerm -> PTerm
769addImpl = addImpl' False [] []
771-- TODO: in patterns, don't add implicits to function names guarded by constructors
772-- and *not* inside a PHidden
774addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
775addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
776 where
777 ai env (PRef fc f)
778 | f `elem` infns = PInferRef fc f
779 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []
780 ai env (PHidden (PRef fc f))
781 | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []
782 ai env (PEq fc l r) = let l' = ai env l
783 r' = ai env r in
784 PEq fc l' r'
785 ai env (PTyped l r) = let l' = ai env l
786 r' = ai env r in
787 PTyped l' r'
788 ai env (PPair fc l r) = let l' = ai env l
789 r' = ai env r in
790 PPair fc l' r'
791 ai env (PDPair fc l t r) = let l' = ai env l
792 t' = ai env t
793 r' = ai env r in
794 PDPair fc l' t' r'
795 ai env (PAlternative a as) = let as' = map (ai env) as in
796 PAlternative a as'
797 ai env (PApp fc (PInferRef _ f) as)
798 = let as' = map (fmap (ai env)) as in
799 PApp fc (PInferRef fc f) as'
800 ai env (PApp fc ftm@(PRef _ f) as)
801 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)
802 | not (f `elem` map fst env)
803 = let as' = map (fmap (ai env)) as in
804 handleErr $ aiFn inpat False ist fc f as'
805 | Just (Just ty) <- lookup f env
806 = let as' = map (fmap (ai env)) as
807 arity = getPArity ty in
808 mkPApp fc arity ftm as'
809 ai env (PApp fc f as) = let f' = ai env f
810 as' = map (fmap (ai env)) as in
811 mkPApp fc 1 f' as'
812 ai env (PCase fc c os) = let c' = ai env c
813 os' = map (pmap (ai env)) os in
814 PCase fc c' os'
815 ai env (PLam n ty sc) = let ty' = ai env ty
816 sc' = ai ((n, Just ty):env) sc in
817 PLam n ty' sc'
818 ai env (PLet n ty val sc)
819 = let ty' = ai env ty
820 val' = ai env val
821 sc' = ai ((n, Just ty):env) sc in
822 PLet n ty' val' sc'
823 ai env (PPi p n ty sc) = let ty' = ai env ty
824 sc' = ai ((n, Just ty):env) sc in
825 PPi p n ty' sc'
826 ai env (PHidden tm) = PHidden (ai env tm)
827 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
828 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
829 ai env tm = tm
831 handleErr (Left err) = PElabError err
832 handleErr (Right x) = x
834-- if in a pattern, and there are no arguments, and there's no possible
835-- names with zero explicit arguments, don't add implicits.
837aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
838aiFn inpat True ist fc f []
839 = case lookupDef Nothing f (tt_ctxt ist) of
840 [] -> Right $ PPatvar fc f
841 alts -> let ialts = lookupCtxt Nothing f (idris_implicits ist) in
842 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
843 if (not (vname f) || tcname f
844 || any constructor alts || any allImp ialts)
845 then aiFn inpat False ist fc f [] -- use it as a constructor
846 else Right $ PPatvar fc f
847 where imp (PExp _ _ _ _) = False
848 imp _ = True
849 allImp [] = False
850 allImp xs = all imp xs
851 constructor (TyDecl (DCon _ _) _) = True
852 constructor _ = False
854 vname (UN n) = True -- non qualified
855 vname _ = False
857aiFn inpat expat ist fc f as
858 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
859aiFn inpat expat ist fc f as
860 -- This is where namespaces get resolved by adding PAlternative
861 = case lookupCtxtName Nothing f (idris_implicits ist) of
862 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
863 [] -> if f `elem` idris_metavars ist
864 then Right $ PApp fc (PRef fc f) as
865 else Right $ mkPApp fc (length as) (PRef fc f) as
866 alts -> Right $
867 PAlternative True $
868 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
869 (insertImpl ns as)) alts
870 where
871 insertImpl :: [PArg] -> [PArg] -> [PArg]
872 insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
873 PExp p l tm d : insertImpl ps given
874 insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
875 PConstraint p l tm d : insertImpl ps given
876 insertImpl (PConstraint p l ty d : ps) given =
877 PConstraint p l (PResolveTC fc) d : insertImpl ps given
878 insertImpl (PImp p l n ty d : ps) given =
879 case find n given [] of
880 Just (tm, given') -> PImp p l n tm "" : insertImpl ps given'
881 Nothing -> PImp p l n Placeholder "" : insertImpl ps given
882 insertImpl (PTacImplicit p l n sc ty d : ps) given =
883 case find n given [] of
884 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
885 Nothing -> if inpat
886 then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
887 else PTacImplicit p l n sc sc "" : insertImpl ps given
888 insertImpl expected [] = []
889 insertImpl _ given = given
891 find n [] acc = Nothing
892 find n (PImp _ _ n' t _ : gs) acc
893 | n == n' = Just (t, reverse acc ++ gs)
894 find n (PTacImplicit _ _ n' _ t _ : gs) acc
895 | n == n' = Just (t, reverse acc ++ gs)
896 find n (g : gs) acc = find n gs (g : acc)
898mkPApp fc a f [] = f
899mkPApp fc a f as = let rest = drop a as in
900 appRest fc (PApp fc f (take a as)) rest
901 where
902 appRest fc f [] = f
903 appRest fc f (a : as) = appRest fc (PApp fc f [a]) as
905-- Find 'static' argument positions
906-- (the declared ones, plus any names in argument position in the declared
907-- statics)
908-- FIXME: It's possible that this really has to happen after elaboration
910findStatics :: IState -> PTerm -> (PTerm, [Bool])
911findStatics ist tm = trace (showImp True tm) $
912 let (ns, ss) = fs tm in
913 runState (pos ns ss tm) []
914 where fs (PPi p n t sc)
915 | Static <- pstatic p
916 = let (ns, ss) = fs sc in
917 (namesIn [] ist t : ns, n : ss)
918 | otherwise = let (ns, ss) = fs sc in
919 (ns, ss)
920 fs _ = ([], [])
922 inOne n ns = length (filter id (map (elem n) ns)) == 1
924 pos ns ss (PPi p n t sc)
925 | elem n ss = do sc' <- pos ns ss sc
926 spos <- get
927 put (True : spos)
928 return (PPi (p { pstatic = Static }) n t sc')
929 | otherwise = do sc' <- pos ns ss sc
930 spos <- get
931 put (False : spos)
932 return (PPi p n t sc')
933 pos ns ss t = return t
935-- Debugging/logging stuff
937dumpDecls :: [PDecl] -> String
938dumpDecls [] = ""
939dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
941dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
942dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
943dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)
944dumpDecl (PData _ _ _ _ d) = showDImp True d
945dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
946dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"
947dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
948dumpDecl (PClass _ _ _ cs n ps ds)
949 = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
950dumpDecl (PInstance _ _ cs n _ t _ ds)
951 = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
952dumpDecl _ = "..."
953-- dumpDecl (PImport i) = "import " ++ i
955-- for 6.12/7 compatibility
956data EitherErr a b = LeftErr a | RightOK b
958instance Monad (EitherErr a) where
959 return = RightOK
961 (LeftErr e) >>= k = LeftErr e
962 RightOK v >>= k = k v
964toEither (LeftErr e) = Left e
965toEither (RightOK ho) = Right ho
967-- syntactic match of a against b, returning pair of variables in a
968-- and what they match. Returns the pair that failed if not a match.
970matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
971matchClause = matchClause' False
973matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
974matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
975 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
977 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
978 fullApp x = x
980 match' x y = match (fullApp x) (fullApp y)
981 match (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x]) x'
982 | PConstant (I _) <- getTm x = match (getTm x) x'
983 match x' (PApp _ (PRef _ (NS (UN "fromInteger") ["builtins"])) [_,_,x])
984 | PConstant (I _) <- getTm x = match (getTm x) x'
985 match (PApp _ (PRef _ (UN "lazy")) [_,x]) x' = match (getTm x) x'
986 match x (PApp _ (PRef _ (UN "lazy")) [_,x']) = match x (getTm x')
987 match (PApp _ f args) (PApp _ f' args')
988 | length args == length args'
989 = do mf <- match' f f'
990 ms <- zipWithM matchArg args args'
991 return (mf ++ concat ms)
992-- match (PRef _ n) (PRef _ n') | n == n' = return []
993-- | otherwise = Nothing
994 match (PRef f n) (PApp _ x []) = match (PRef f n) x
995 match (PApp _ x []) (PRef f n) = match x (PRef f n)
996 match (PRef _ n) tm@(PRef _ n')
997 | n == n' && not names &&
998 (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
999 = return [(n, tm)]
1000 | n == n' = return []
1001 match (PRef _ n) tm
1002 | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)
1003 = return [(n, tm)]
1004 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
1005 mr <- match' r r'
1006 return (ml ++ mr)
1007 match (PTyped l r) (PTyped l' r') = do ml <- match l l'
1008 mr <- match r r'
1009 return (ml ++ mr)
1010 match (PTyped l r) x = match l x
1011 match x (PTyped l r) = match x l
1012 match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
1013 mr <- match' r r'
1014 return (ml ++ mr)
1015 match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
1016 mt <- match' t t'
1017 mr <- match' r r'
1018 return (ml ++ mt ++ mr)
1019 match (PAlternative a as) (PAlternative a' as')
1020 = do ms <- zipWithM match' as as'
1021 return (concat ms)
1022 match a@(PAlternative _ as) b
1023 = do let ms = zipWith match' as (repeat b)
1024 case (rights (map toEither ms)) of
1025 (x: _) -> return x
1026 _ -> LeftErr (a, b)
1027 match (PCase _ _ _) _ = return [] -- lifted out
1028 match (PMetavar _) _ = return [] -- modified
1029 match (PInferRef _ _) _ = return [] -- modified
1030 match (PQuote _) _ = return []
1031 match (PProof _) _ = return []
1032 match (PTactics _) _ = return []
1033 match (PRefl _ _) (PRefl _ _) = return []
1034 match (PResolveTC _) (PResolveTC _) = return []
1035 match (PTrue _) (PTrue _) = return []
1036 match (PFalse _) (PFalse _) = return []
1037 match (PReturn _) (PReturn _) = return []
1038 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1039 ms <- match' s s'
1040 return (mt ++ ms)
1041 match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
1042 ms <- match' s s'
1043 return (mt ++ ms)
1044 match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
1045 mty <- match' ty ty'
1046 ms <- match' s s'
1047 return (mt ++ mty ++ ms)
1048 match (PHidden x) (PHidden y) = match' x y
1049 match Placeholder _ = return []
1050 match _ Placeholder = return []
1051 match (PResolveTC _) _ = return []
1052 match a b | a == b = return []
1053 | otherwise = LeftErr (a, b)
1055 checkRpts (RightOK ms) = check ms where
1056 check ((n,t):xs)
1057 | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
1058 then Left (t, t')
1059 else check xs
1060 check (_:xs) = check xs
1061 check [] = Right ms
1062 checkRpts (LeftErr x) = Left x
1064substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
1065substMatches ms = substMatchesShadow ms []
1067substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
1068substMatchesShadow [] shs t = t
1069substMatchesShadow ((n,tm):ns) shs t
1070 = substMatchShadow n shs tm (substMatchesShadow ns shs t)
1072substMatch :: Name -> PTerm -> PTerm -> PTerm
1073substMatch n = substMatchShadow n []
1075substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
1076substMatchShadow n shs tm t = sm shs t where
1077 sm xs (PRef _ n') | n == n' = tm
1078 sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
1079 sm xs (PPi p x t sc)
1080 | x `elem` xs
1081 = let x' = nextName x in
1082 PPi p x' (sm (x':xs) (substMatch x (PRef (FC "" 0) x') t))
1083 (sm (x':xs) (substMatch x (PRef (FC "" 0) x') sc))
1084 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
1085 sm xs (PApp f x as) = PApp f (sm xs x) (map (fmap (sm xs)) as)
1086 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
1087 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
1088 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
1089 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
1090 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
1091 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
1092 sm xs (PHidden x) = PHidden (sm xs x)
1093 sm xs x = x
1095shadow :: Name -> Name -> PTerm -> PTerm
1096shadow n n' t = sm t where
1097 sm (PRef fc x) | n == x = PRef fc n'
1098 sm (PLam x t sc) = PLam x (sm t) (sm sc)
1099 sm (PPi p x t sc) = PPi p x (sm t) (sm sc)
1100 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
1101 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
1102 sm (PEq f x y) = PEq f (sm x) (sm y)
1103 sm (PTyped x y) = PTyped (sm x) (sm y)
1104 sm (PPair f x y) = PPair f (sm x) (sm y)
1105 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
1106 sm (PAlternative a as) = PAlternative a (map sm as)
1107 sm (PHidden x) = PHidden (sm x)
1108 sm x = x