blob: bac6d0470ea24dd376d1d4daa22c210c91462b52 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
module Obs.Abstract
import Data.Fin
import Data.String
import Obs.Syntax
import Obs.Term
import System
import Text.Bounded
%default total
public export
Context : Nat -> Type
Context n = List (String, Fin n)
bind : Context n -> String -> Context (S n)
bind ctx str = (str, 0) :: map (mapSnd FS) ctx
Error : Type -> Type
Error = Either (Bounds, String)
report : Bounds -> String -> Error a
report = curry Left
export
printErr : Error a -> IO a
printErr (Left (b, str)) = do
() <- putStrLn "error: \{show b.startLine}:\{show b.startCol}-\{show b.endLine}:\{show b.endCol}: \{str}"
exitFailure
printErr (Right x) = pure x
export
abstractSyntax : Context n -> Syntax -> Error (Term n)
abstractSyntax ctx (Var b str) = do
let Just i = lookup str ctx
| Nothing => report b "unbound variable: \{str}"
pure (Var b i)
abstractSyntax ctx (Sort b s) = pure (Sort b s)
export
abstractDefinition : Context n -> Definition -> Error (Definition n)
abstractDefinition ctx def = pure $ MkDefinition
{ name = def.name
, bounds = def.bounds
, ty = !(abstractSyntax ctx def.ty)
, tm = !(abstractSyntax ctx def.tm)
}
export
abstractBlock : (defs : List Definition) -> Error (Block (length defs))
abstractBlock defs =
let asContext : Block n -> Context n
asContext [] = []
asContext (defs :< def) = bind (asContext defs) def.name
in let helper : Block n -> (defs : List Definition) -> Error (Block (length defs + n))
helper blk [] = pure blk
helper blk (def :: defs) = do
def <- abstractDefinition (asContext blk) def
(rewrite plusSuccRightSucc (length defs) n in helper (blk :< def) defs)
in rewrite sym $ plusZeroRightNeutral (length defs) in helper [] defs
|
