0 | module Language.Mk
 1 |
 2 | --import public Data.SortedMap {- this import is a workaround of idris-lang/Idris2#2439 -}
 3 | --import public Data.SortedMap.Dependent {- this import is a workaround of idris-lang/Idris2#2439 -}
 4 | --import public Data.SortedSet {- `public` is a workaround of idris-lang/Idris2#2439 -}
 5 |
 6 | import public Language.Reflection
 7 |
 8 | %default total
 9 |
10 | --record TyCon where
11 | --  constructor MkTyCon
12 | --  typeConstructor : Name
13 | --  appliedArgs : List $ Argument $ Maybe TTImp -- Nothing means "unapplied"
14 | --  cons : List (Name, TTImp)
15 | --
16 | --tyConAndArgs : Elaboration m =>
17 | --               (boundNames : SortedSet (FC, Name)) ->
18 | --               (usedFreeNames : SortedSet Name) ->
19 | --               TTImp ->
20 | --               m $ List (Name, List $ Argument $ Maybe TTImp)
21 | --tyConAndArgs boundNames usedFreeNames $ ILam fc _ _ Nothing argTy rest = failAt fc "Expected a type constructor, got an unnamed lambda"
22 | --tyConAndArgs boundNames usedFreeNames $ ILam fc cnt pii (Just nm) argTy rest = tyConAndArgs (insert (fc, nm) boundNames) usedFreeNames rest
23 | --tyConAndArgs boundNames usedFreeNames _ = ?tyConAndArgs_rest
24 | --
25 | --getTyCon : Elaboration m => TTImp -> m $ List TyCon
26 | --getTyCon expr = ?foo
27 |
28 | isTyCon : NameInfo -> Bool
29 | isTyCon $ MkNameInfo $ TyCon {} = True
30 | isTyCon _                       = False
31 |
32 | export
33 | getMk' : (t : ty) -> Elab (FC, Name)
34 | getMk' t = do
35 |   expr <- quote t
36 |   let fc = getFC expr
37 |   let IVar _ name = expr
38 |     | IPrimVal {} => failAt fc "Expression must not be a primitive value or type"
39 |     | expr        => failAt fc "Expression must be just a name"
40 |   [(name, _)] <- getInfo name <&> filter (isTyCon . snd)
41 |     | []      => failAt fc "Expression must be an unambiguous type"
42 |     | _::_::_ => failAt fc "Given name `\{show name}` is ambiguous type"
43 |   [conName] <- getCons name
44 |     | []      => failAt fc "No constructors found for `\{show name}`"
45 |     | _::_::_ => failAt fc "Given type `\{show name}` has more than one constructor"
46 |   pure (fc, conName)
47 |
48 | export
49 | getMk : (t : ty) -> Elab Name
50 | getMk = map snd . getMk'
51 |
52 | export %macro %inline
53 | Mk : (t : ty) -> Elab a
54 | Mk t = do
55 |   (fc, conName) <- getMk' t
56 |   check $ IVar fc conName
57 |