add formal model to tl on Arend

VKCOM · Nov 13, 2024 · c65f013 · c65f013
1 parent 13b6b35
commit c65f013
Show file tree

Hide file tree

Showing 4 changed files with 268 additions and 0 deletions.
diff --git a/internal/tlmodel/README.md b/internal/tlmodel/README.md
@@ -0,0 +1,38 @@
+### TL Formal Model on Arend
+
+В `src/Model.ard` описаны примитивы для описания типов на языке TL.
+* В данной модели нет _Boxed_ на момент написания этого файла (13.11.24)
+* Для описания типа создайте объект типа `TLType` (разница между union-type и обычными типа лишь в количестве конструкторов)
+
+Пример для `pair {X: Type} {Y: Type} left:X property:Y = Pair;`:
+```haskell
+\func TLPair : TLType => \new TLType {
+  | typeHeader => tl-new-type 1 (^Type :: (^Type :: nil))
+  | constructorsCount => 1
+  | constructors => (\new TLConstructor {
+    | fields-count => 2
+    | fields =>
+      (\new TLFieldDefinition {
+        | fieldProp => idp
+        | fieldMask => nothing
+        | fieldType => field-generic (\new TLGenericRef {
+          | i => 0
+          | isGeneric => idp
+        })
+      }) eac-::
+      (\new TLFieldDefinition {
+        | fieldProp => idp
+        | fieldMask => nothing
+        | fieldType => field-generic (\new TLGenericRef {
+          | i => 1
+          | isGeneric => idp
+        })
+      }) eac-::
+      eac-nil
+  }) eac-:: eac-nil
+  | newType => is-new-type
+  | nonEmpty => contradiction
+}
+```
+
+Другие примеры лежат в `src/Types.ard`. Также там есть пример не выводимой в тле конструкции (которая не компилиться в Arend)
diff --git a/internal/tlmodel/arend.yaml b/internal/tlmodel/arend.yaml
@@ -0,0 +1,4 @@
+langVersion: 1.10
+sourcesDir: src
+binariesDir: bin
+dependencies: [arend-lib]
diff --git a/internal/tlmodel/src/Model.ard b/internal/tlmodel/src/Model.ard
@@ -0,0 +1,95 @@
+\import Arith.Nat
+\import Data.Bool
+\import Data.List
+\import Data.Maybe
+\import Data.Or
+\import Logic
+\import Order.StrictOrder
+\import Paths.Meta
+
+\data TypeArgument
+  | ^Type
+  | #
+  \where {
+    \func isNat (td : TypeArgument) : Bool \elim td
+      | ^Type => false
+      | # => true
+  }
+
+\data TypeData
+  | tl-nat
+  | tl-builtin-array
+  | tl-new-type (typeNo : Nat) (args : List TypeArgument)
+  \where {
+    \func args (t : TypeData) : List TypeArgument \elim t
+      | tl-nat => nil
+      | tl-builtin-array => # :: ^Type :: nil
+      | tl-new-type typeNo args => args
+  }
+
+\record TLGenericRef
+  | deps : List TypeArgument
+  | i : Fin (length deps)
+  | isGeneric : deps !! i = ^Type
+
+\data TLNatRef (deps : List TypeArgument) (prevNats : List Bool)
+  | fromDep (i : Fin (length deps)) (isNat : deps !! i = #)
+  | fromPrevField (i : Fin (length prevNats)) (isNat : So (prevNats !! i))
+
+\data TLTypeArguments (args : List TypeArgument) (prevNats : List Bool) (restArgs : List TypeArgument) \elim restArgs
+  | nil => end-args
+  | # :: restArgs => applyConst (n : Nat) (TLTypeArguments args prevNats restArgs)
+  | # :: restArgs => applyNatRef (ref : TLNatRef args prevNats) (TLTypeArguments args prevNats restArgs)
+  | ^Type :: restArgs => applyGeneric (gen : TLGenericRef args) (TLTypeArguments args prevNats restArgs)
+  | ^Type :: restArgs => applyType (t : TypeData) (tArgs : TLTypeArguments args prevNats (TypeData.args t)) (TLTypeArguments args prevNats restArgs)
+
+\record TLFieldMask (deps : List TypeArgument) (prevNats : List Bool) (v : TLNatRef deps prevNats) (bit : Fin 32)
+
+\record TLFieldDefinition
+  | args : List TypeArgument
+  | prevNats : List Bool
+  | fieldNo : Nat
+  | fieldProp : fieldNo = length prevNats
+  | fieldMask : Maybe (TLFieldMask args prevNats)
+  | fieldType : TLFieldType args prevNats
+
+\data TLFieldType (deps : List TypeArgument) (prevNats : List Bool)
+  | field-generic (TLGenericRef deps)
+  | field-application (t : TypeData) (tArgs : TLTypeArguments deps prevNats (TypeData.args t))
+
+\record TLConstructor
+  | type-header : TypeData
+  | type-constructor-count : Nat
+  | constructor-id : Fin type-constructor-count
+  | fields-count : Nat
+  | fields :
+  EnumarateArrayWithAccum
+      fields-count
+      {List Bool}
+      (\lam fi nats => TLFieldDefinition (TypeData.args type-header) nats fi)
+      nil
+      (\lam _ acc cur => \case cur \with {
+        | (p,m, field-application tl-nat end-args) => true :: acc
+        | _ => false :: acc
+      })
+
+\data IsNewType (t : TypeData) \elim t
+  | tl-new-type typeNo args => is-new-type
+
+\record TLType
+  | typeHeader : TypeData
+  | constructorsCount : Nat
+  | constructors : EnumarateArray constructorsCount (\lam fi => TLConstructor typeHeader constructorsCount fi)
+  | newType : IsNewType typeHeader
+  | nonEmpty : constructorsCount /= 0
+
+\data EnumarateArrayWithAccum
+  (n : Nat)
+  {C : \Type}
+  (A : \Pi (fi : Fin n) -> C -> \Type)
+  (cur : C)
+  (next : \Pi (fi : Fin n) (acc : C) (cur : A fi acc) -> C) \elim n
+  | 0 => eac-nil
+  | (suc n) => \infixr 5 eac-:: (a : A 0 cur) (EnumarateArrayWithAccum n {C} (\lam f c => A (suc f) c) (next 0 cur a) (\lam f acc cur => next (suc f) acc cur))
+
+\func EnumarateArray (n : Nat) (A : \Pi (fi : Fin n) -> \Type) => EnumarateArrayWithAccum n {Nat} (\lam fi _ => A fi) 0 (\lam _ _ _ => 0)
diff --git a/internal/tlmodel/src/Types.ard b/internal/tlmodel/src/Types.ard
@@ -0,0 +1,131 @@
+\import Data.List
+\import Data.Maybe
+\import Logic.Meta
+\import Model
+
+\func TLInt : TLType => \new TLType {
+  | typeHeader => tl-new-type 0 nil
+  | constructorsCount => 1
+  | constructors => (\new TLConstructor {
+    | fields-count => 0
+    | fields => eac-nil
+  }) eac-:: eac-nil
+  | nonEmpty => contradiction
+  | newType => is-new-type
+}
+
+\func TLPair : TLType => \new TLType {
+  | typeHeader => tl-new-type 1 (^Type :: (^Type :: nil))
+  | constructorsCount => 1
+  | constructors => (\new TLConstructor {
+    | fields-count => 2
+    | fields =>
+      (\new TLFieldDefinition {
+        | fieldProp => idp
+        | fieldMask => nothing
+        | fieldType => field-generic (\new TLGenericRef {
+          | i => 0
+          | isGeneric => idp
+        })
+      }) eac-::
+      (\new TLFieldDefinition {
+        | fieldProp => idp
+        | fieldMask => nothing
+        | fieldType => field-generic (\new TLGenericRef {
+          | i => 1
+          | isGeneric => idp
+        })
+      }) eac-::
+      eac-nil
+  }) eac-:: eac-nil
+  | newType => is-new-type
+  | nonEmpty => contradiction
+}
+
+\func TLVector : TLType => \new TLType {
+  | typeHeader => tl-new-type 2 (^Type :: nil)
+  | constructorsCount => 1
+  | constructors => (\new TLConstructor {
+    | fields-count => 2
+    | fields =>
+      (\new TLFieldDefinition {
+        | fieldProp => idp
+        | fieldMask => nothing
+        | fieldType => field-application tl-nat end-args
+      }) eac-::
+      (\new TLFieldDefinition {
+        | fieldProp => idp
+        | fieldMask => nothing
+        | fieldType => field-application tl-builtin-array (applyNatRef (fromPrevField 0 ()) (applyGeneric (\new TLGenericRef {
+          | i => 0
+          | isGeneric => idp
+        }) end-args))
+      }) eac-::
+      eac-nil
+  }) eac-:: eac-nil
+  | newType => is-new-type
+  | nonEmpty => contradiction
+}
+-- struct f1:# f2:f1.0?# f3:f2.31?# = Struct;
+\func TlNikitaStruct : TLType => \new TLType {
+  | typeHeader => tl-new-type 4 nil
+  | constructorsCount => 1
+  | constructors =>
+    (\new TLConstructor {
+      | fields-count => 3
+      | fields =>
+        (\new TLFieldDefinition {
+          | fieldProp => idp
+          | fieldMask => nothing
+          | fieldType => field-application tl-nat end-args
+        }) eac-::
+        (\new TLFieldDefinition {
+          | fieldProp => idp
+          | fieldMask => just (\new TLFieldMask {
+            | v => fromPrevField 0 ()
+            | bit => 0
+          })
+          | fieldType => field-application tl-nat end-args
+        }) eac-::
+        (\new TLFieldDefinition {
+          | fieldProp => idp
+          | fieldMask => just (\new TLFieldMask {
+            | v => fromPrevField 1 ()
+            | bit => 31
+          })
+          | fieldType => field-application tl-nat end-args
+        }) eac-::
+        eac-nil
+    })
+      eac-:: eac-nil
+  | newType => is-new-type
+  | nonEmpty => contradiction
+}
+
+-- struct f1:int f2:f1.0?# = Struct;
+\func NonTLStruct : TLType => \new TLType {
+  | typeHeader => tl-new-type 1488 nil
+  | constructorsCount => 1
+  | constructors =>
+    (\new TLConstructor {
+      | fields-count => 2
+      | fields =>
+        (\new TLFieldDefinition {
+          | fieldProp => idp
+          | fieldMask => nothing
+          | fieldType => field-application TLInt.typeHeader end-args
+        }) eac-::
+        (\new TLFieldDefinition {
+          | fieldProp => idp
+          | fieldMask => just (\new TLFieldMask {
+            | v => fromPrevField 0 {?}
+            | bit => 0
+          })
+          | fieldType => field-application tl-nat end-args
+        }) eac-::
+        eac-nil
+    }) eac-::
+    eac-nil
+  | newType => is-new-type
+  | nonEmpty => contradiction
+}