
   0 | module Core.SchemeEval.ToScheme
   1 | 
   2 | import Core.TT
   3 | import Libraries.Utils.Scheme
   4 | 
   5 | export
   6 | Scheme Namespace where
   7 |   toScheme x = toScheme (unsafeUnfoldNamespace x)
   8 |   fromScheme x = Just $ unsafeFoldNamespace !(fromScheme x)
   9 | 
  10 | export
  11 | Scheme UserName where
  12 |   toScheme (Basic str) = toScheme str
  13 |   toScheme (Field str) = Vector 5 [toScheme str]
  14 |   toScheme Underscore = Vector 9 []
  15 | 
  16 |   fromScheme (Vector 5 [x]) = pure $ Field !(fromScheme x)
  17 |   fromScheme (Vector 9 []) = pure Underscore
  18 |   fromScheme (StringVal x) = pure (Basic x)
  19 |   fromScheme _ = Nothing
  20 | 
  21 | export
  22 | Scheme Name where
  23 |   toScheme (NS x y) = Vector 0 [toScheme x, toScheme y]
  24 |   toScheme (UN x) = toScheme x
  25 |   toScheme (MN x y) = Vector 2 [toScheme x, toScheme y]
  26 |   toScheme (PV x y) = Vector 3 [toScheme x, toScheme y]
  27 |   toScheme (DN x y) = Vector 4 [toScheme x, toScheme y]
  28 |   toScheme (Nested x y) = Vector 6 [toScheme x, toScheme y]
  29 |   toScheme (CaseBlock x y) = Vector 7 [toScheme x, toScheme y]
  30 |   toScheme (WithBlock x y) = Vector 8 [toScheme x, toScheme y]
  31 |   toScheme (Resolved x) = toScheme x -- we'll see this most often
  32 | 
  33 |   fromScheme (Vector 0 [x, y])
  34 |       = pure $ NS !(fromScheme x) !(fromScheme y)
  35 |   fromScheme (Vector 2 [x, y])
  36 |       = pure $ MN !(fromScheme x) !(fromScheme y)
  37 |   fromScheme (Vector 3 [x, y])
  38 |       = pure $ PV !(fromScheme x) !(fromScheme y)
  39 |   fromScheme (Vector 4 [x, y])
  40 |       = pure $ DN !(fromScheme x) !(fromScheme y)
  41 |   fromScheme (Vector 5 [x, y])
  42 |       = pure $ UN (Field !(fromScheme x))
  43 |   fromScheme (Vector 6 [x, y])
  44 |       = pure $ Nested !(fromScheme x) !(fromScheme y)
  45 |   fromScheme (Vector 7 [x, y])
  46 |       = pure $ CaseBlock !(fromScheme x) !(fromScheme y)
  47 |   fromScheme (Vector 8 [x, y])
  48 |       = pure $ WithBlock !(fromScheme x) !(fromScheme y)
  49 |   fromScheme (Vector 9 [])
  50 |       = pure $ UN Underscore
  51 |   fromScheme (IntegerVal x)
  52 |       = pure $ Resolved (cast x)
  53 |   fromScheme (StringVal x)
  54 |       = pure $ UN (Basic x)
  55 |   fromScheme _ = Nothing
  56 | 
  57 | export
  58 | Scheme ModuleIdent where
  59 |   toScheme ns = toScheme (miAsNamespace ns)
  60 |   fromScheme s = Just $ nsAsModuleIdent !(fromScheme s)
  61 | 
  62 | export
  63 | Scheme OriginDesc where
  64 |   toScheme (PhysicalIdrSrc ident) = Vector 0 [toScheme ident]
  65 |   toScheme (PhysicalPkgSrc fname) = Vector 1 [toScheme fname]
  66 |   toScheme (Virtual ident) = Null
  67 | 
  68 |   fromScheme (Vector 0 [i]) = Just (PhysicalIdrSrc !(fromScheme i))
  69 |   fromScheme (Vector 1 [i]) = Just (PhysicalPkgSrc !(fromScheme i))
  70 |   fromScheme (Vector {}) = Nothing
  71 |   fromScheme _ = Just (Virtual Interactive)
  72 | 
  73 | export
  74 | Scheme FC where
  75 |   toScheme (MkFC d s e) = Vector 0 [toScheme d, toScheme s, toScheme e]
  76 |   toScheme (MkVirtualFC d s e) = Vector 1 [toScheme d, toScheme s, toScheme e]
  77 |   toScheme EmptyFC = Null
  78 | 
  79 |   fromScheme _ = Just EmptyFC
  80 | 
  81 | export
  82 | Scheme LazyReason where
  83 |   toScheme LInf = IntegerVal 0
  84 |   toScheme LLazy = IntegerVal 1
  85 |   toScheme LUnknown = IntegerVal 2
  86 | 
  87 |   fromScheme (IntegerVal 0) = Just LInf
  88 |   fromScheme (IntegerVal 1) = Just LLazy
  89 |   fromScheme _ = Just LUnknown
  90 | 
  91 | export
  92 | Scheme RigCount where
  93 |   toScheme x
  94 |       = if isErased x then IntegerVal 0
  95 |         else if isLinear x then IntegerVal 1
  96 |         else IntegerVal 2
  97 | 
  98 |   fromScheme (IntegerVal 0) = Just erased
  99 |   fromScheme (IntegerVal 1) = Just linear
 100 |   fromScheme _ = Just top
 101 | 
 102 | export
 103 | toSchemePi : PiInfo (SchemeObj Write) -> SchemeObj Write
 104 | toSchemePi Implicit = IntegerVal 0
 105 | toSchemePi Explicit = IntegerVal 1
 106 | toSchemePi AutoImplicit = IntegerVal 2
 107 | toSchemePi (DefImplicit s) = Box s
 108 | 
 109 | export
 110 | toSchemeWhy : WhyErased (SchemeObj Write) -> SchemeObj Write
 111 | toSchemeWhy Impossible = IntegerVal 0
 112 | toSchemeWhy Placeholder = IntegerVal 1
 113 | toSchemeWhy (Dotted s) = Box s
 114 |