]> Git — Sourcephile - tmp/julm/symantic.git/blob - src/Symantic/Compiler/Term.hs
75baae939cec157289e5f4caaba182df80deb168
[tmp/julm/symantic.git] / src / Symantic / Compiler / Term.hs
1 {-# LANGUAGE AllowAmbiguousTypes #-}
2 {-# LANGUAGE ConstraintKinds #-}
3 {-# LANGUAGE InstanceSigs #-}
4 {-# LANGUAGE QuantifiedConstraints #-}
5 {-# LANGUAGE RankNTypes #-}
6 {-# LANGUAGE UndecidableInstances #-}
7 {-# OPTIONS_GHC -Wno-partial-fields #-}
8
9 module Symantic.Compiler.Term where
10
11 import Data.Function qualified as Fun
12 import Data.Monoid (Monoid)
13 import GHC.Types (Type)
14 import Symantic.Semantics.Eval (Eval (..))
15 import Symantic.Semantics.Forall
16 import Symantic.Syntaxes.Classes (Instantiable (..), Syntax, Syntaxes, Unabstractable (..))
17 import Symantic.Syntaxes.Classes qualified as Sym
18 import Type.Reflection (Typeable)
19 import Unsafe.Coerce (unsafeCoerce)
20
21 import Symantic.Typer.Type (Ty, monoTy)
22
23 -- * Class 'AbstractableTy'
24 class AbstractableTy ty sem where
25 -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
26 lamTy :: ty a -> (sem a -> sem b) -> sem (a -> b)
27
28 fun ::
29 forall prov sem a b.
30 Monoid prov =>
31 AbstractableTy (Ty prov '[]) sem =>
32 Typeable a =>
33 (sem a -> sem b) ->
34 sem (a -> b)
35 fun = lamTy (monoTy @_ @prov)
36
37 instance
38 ( forall sem. Syntaxes syns sem => AbstractableTy (Ty prov '[]) sem
39 -- , forall sem a. syn sem => AbstractableLam sem a
40 -- , forall sem. syn sem => AbstractableLam sem a
41 -- , forall sem. syn sem => Typeable sem -- user instance not accepted
42 -- , forall s1 s2. (syn s1, syn s2) => s1 ~ s2 -- crazy...
43 ) =>
44 AbstractableTy (Ty prov '[]) (Forall syns)
45 where
46 lamTy aTy f = Forall (lamTy aTy (\a -> let Forall b = f (forallSem a) in b))
47 where
48 -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
49 forallSem :: sem a -> Forall syns a
50 forallSem a = Forall (unsafeCoerce a)
51
52 -- * Type 'OpenTerm'
53 data OpenTerm (syns :: [Syntax]) (vs :: [Type]) (a :: Type) where
54 -- | 'E' contains embedded closed (i.e. already abstracted) terms.
55 E :: Forall syns a -> OpenTerm syns vs a
56 -- | 'V' represents a reference to the innermost/top environment variable, i.e. Z
57 V :: OpenTerm syns (a ': vs) a
58 -- | 'N' represents internalizing the innermost bound variable as a
59 -- function argument. In other words, we can represent an open
60 -- term referring to a certain variable as a function which
61 -- takes that variable as an argument.
62 N :: OpenTerm syns vs (a -> b) -> OpenTerm syns (a ': vs) b
63 -- | 'W' is a special variant of N for efficiency,
64 -- in the case where the term does not refer
65 -- to the topmost variable at all.
66 W :: OpenTerm syns vs b -> OpenTerm syns (a ': vs) b
67 instance
68 ( forall sem. Syntaxes syns sem => AbstractableTy (Ty prov '[]) sem
69 , Syntaxes syns (Forall syns)
70 ) =>
71 AbstractableTy (Ty prov '[]) (OpenTerm syns '[])
72 where
73 lamTy aTy f = E (lamTy aTy (unE Fun.. f Fun.. E))
74 instance
75 ( forall sem. Syntaxes syns sem => Unabstractable sem
76 , Syntaxes syns (Forall syns)
77 ) =>
78 Unabstractable (OpenTerm syns vs)
79 where
80 ap = E Sym.ap
81 const = E Sym.const
82 id = E Sym.id
83 (.) = E (Sym..)
84 flip = E Sym.flip
85 ($) = E (Sym.$)
86
87 instance AbstractableTy (Ty prov '[]) Eval where
88 lamTy _aTy f = Eval (unEval Fun.. f Fun.. Eval)
89
90 runOpenTerm :: Syntaxes syns Eval => OpenTerm syns '[] a -> a
91 runOpenTerm t | E (Forall sem) <- t = unEval sem
92
93 unE :: OpenTerm syns '[] a -> Forall syns a
94 unE t = case t of E t' -> t'
95
96 instance
97 ( forall sem. Syntaxes syns sem => Unabstractable sem
98 , forall sem. Syntaxes syns sem => Instantiable sem
99 , Syntaxes syns (Forall syns)
100 ) =>
101 Instantiable (OpenTerm syns vs)
102 where
103 (.@) = appOpenTerm
104
105 appOpenTerm ::
106 forall syns as a b.
107 ( forall sem. Syntaxes syns sem => Unabstractable sem
108 , forall sem. Syntaxes syns sem => Instantiable sem
109 , Syntaxes syns (Forall syns)
110 ) =>
111 OpenTerm syns as (a -> b) ->
112 OpenTerm syns as a ->
113 OpenTerm syns as b
114 E d `appOpenTerm` N e = N (E ((Sym..) .@ d) `appOpenTerm` e)
115 E d `appOpenTerm` V = N (E d)
116 E d `appOpenTerm` W e = W (E d `appOpenTerm` e)
117 E d1 `appOpenTerm` E d2 = E (d1 .@ d2)
118 N e `appOpenTerm` E d = N (E (Sym.flip .@ Sym.flip .@ d) `appOpenTerm` e)
119 N e `appOpenTerm` V = N (E Sym.ap `appOpenTerm` e `appOpenTerm` E Sym.id)
120 N e1 `appOpenTerm` N e2 = N (E Sym.ap `appOpenTerm` e1 `appOpenTerm` e2)
121 N e1 `appOpenTerm` W e2 = N (E Sym.flip `appOpenTerm` e1 `appOpenTerm` e2)
122 V `appOpenTerm` E d = N (E (Sym.flip .@ Sym.id .@ d))
123 V `appOpenTerm` N e = N (E (Sym.ap .@ Sym.id) `appOpenTerm` e)
124 V `appOpenTerm` W e = N (E (Sym.flip .@ Sym.id) `appOpenTerm` e)
125 W e `appOpenTerm` E d = W (e `appOpenTerm` E d)
126 W e `appOpenTerm` V = N e
127 W e1 `appOpenTerm` N e2 = N (E (Sym..) `appOpenTerm` e1 `appOpenTerm` e2)
128 W e1 `appOpenTerm` W e2 = W (e1 `appOpenTerm` e2)