From: Eugene Akentyev Date: Wed, 2 Nov 2016 14:09:53 +0000 (+0300) Subject: First steps with Equality X-Git-Url: https://git.xn--bdkaa.com/?a=commitdiff_plain;h=485cdafc559ecdf56affcf0a5950e9895b38a572;p=jolie.agda.git First steps with Equality --- diff --git a/src/Expr.agda b/src/Expr.agda index b6360f3..ff1f59f 100644 --- a/src/Expr.agda +++ b/src/Expr.agda @@ -6,11 +6,7 @@ open import Variable -- TODO: add logic operations and, or data BinOp : Set where - plus : BinOp - minus : BinOp - mult : BinOp - div : BinOp - power : BinOp + plus minus mult div power : BinOp data Expr : Set where var : Variable → Expr diff --git a/src/Type.agda b/src/Type.agda index 2d8cf33..48a00af 100644 --- a/src/Type.agda +++ b/src/Type.agda @@ -1,7 +1,12 @@ module Type where +open import Relation.Nullary +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl) +open import Data.Nat using (ℕ) open import Data.String using (String) open import Data.List using (List) +open import Data.Vec using (Vec) open import Expr open import Variable @@ -16,18 +21,62 @@ Channel : Set Channel = String data Cardinality : Set where - oo : Cardinality - oi : Cardinality - ii : Cardinality + oo oi ii : Cardinality data BasicType : Set where - bool : BasicType - int : BasicType - double : BasicType - long : BasicType - string : BasicType - raw : BasicType - void : BasicType + bool int double long string raw void : BasicType + +module BasicTypeEq where + _≟_ : Decidable {A = BasicType} _≡_ + bool ≟ bool = yes refl + int ≟ int = yes refl + double ≟ double = yes refl + long ≟ long = yes refl + string ≟ string = yes refl + raw ≟ raw = yes refl + void ≟ void = yes refl + bool ≟ int = no λ() + bool ≟ double = no λ() + bool ≟ long = no λ() + bool ≟ string = no λ() + bool ≟ raw = no λ() + bool ≟ void = no λ() + int ≟ bool = no λ() + int ≟ double = no λ() + int ≟ long = no λ() + int ≟ string = no λ() + int ≟ raw = no λ() + int ≟ void = no λ() + double ≟ bool = no λ() + double ≟ int = no λ() + double ≟ long = no λ() + double ≟ string = no λ() + double ≟ raw = no λ() + double ≟ void = no λ() + long ≟ bool = no λ() + long ≟ int = no λ() + long ≟ double = no λ() + long ≟ string = no λ() + long ≟ raw = no λ() + long ≟ void = no λ() + string ≟ bool = no λ() + string ≟ int = no λ() + string ≟ double = no λ() + string ≟ long = no λ() + string ≟ raw = no λ() + string ≟ void = no λ() + raw ≟ bool = no λ() + raw ≟ int = no λ() + raw ≟ double = no λ() + raw ≟ long = no λ() + raw ≟ string = no λ() + raw ≟ void = no λ() + void ≟ bool = no λ() + void ≟ int = no λ() + void ≟ double = no λ() + void ≟ long = no λ() + void ≟ string = no λ() + void ≟ raw = no λ() data TypeTree : Set @@ -38,6 +87,15 @@ data TypeTree where leaf : BasicType → TypeTree node : BasicType → List ChildType → TypeTree +module TypeTreeEq where + _≟_ : Decidable {A = TypeTree} _≡_ + (leaf b1) ≟ (leaf b2) with BasicTypeEq._≟_ b1 b2 + ... | yes b1≡b2 = {!!} + ... | no ¬b1≡b2 = no {!!} + (node b1 cts) ≟ (node b2 cts') = {!!} + (leaf _) ≟ (node _ _) = no λ () + (node _ _) ≟ (leaf _) = no λ () + data TypeDecl : Set where outNotify : Operation → Location → TypeTree → TypeDecl outSolRes : Operation → Location → TypeTree → TypeTree → TypeDecl @@ -47,5 +105,61 @@ data TypeDecl : Set where empty : TypeDecl pair : TypeDecl → TypeDecl → TypeDecl -Ctx : Set -Ctx = List TypeDecl +module TypeDeclEq where + _≟_ : Decidable {A = TypeDecl} _≡_ + (outNotify o1 l1 t1) ≟ (outNotify o2 l2 t2) = {!!} + (outSolRes o1 l1 t1 t1') ≟ (outSolRes o2 l2 t2 t2') = {!!} + (inOneWay o1 t1) ≟ (inOneWay o2 t2) = {!!} + (inReqRes o1 t1 t1') ≟ (inReqRes o2 t2 t2') = {!!} + (var v1 t1) ≟ (var v2 t2) = {!!} + (pair t1 t1') ≟ (pair t2 t2') = {!!} + empty ≟ empty = yes refl + empty ≟ (outNotify _ _ _) = no λ() + empty ≟ (outSolRes _ _ _ _) = no λ() + empty ≟ (inOneWay _ _) = no λ() + empty ≟ (inReqRes _ _ _) = no λ() + empty ≟ (var _ _) = no λ() + empty ≟ (pair _ _) = no λ() + (outNotify _ _ _) ≟ (outSolRes _ _ _ _) = no λ() + (outNotify _ _ _) ≟ (inOneWay _ _) = no λ() + (outNotify _ _ _) ≟ (inReqRes _ _ _) = no λ() + (outNotify _ _ _) ≟ (var _ _) = no λ() + (outNotify _ _ _) ≟ empty = no λ() + (outNotify _ _ _) ≟ (pair _ _) = no λ() + (outSolRes _ _ _ _) ≟ (outNotify _ _ _) = no λ() + (outSolRes _ _ _ _) ≟ (inOneWay _ _) = no λ() + (outSolRes _ _ _ _) ≟ (inReqRes _ _ _) = no λ() + (outSolRes _ _ _ _) ≟ (var _ _) = no λ() + (outSolRes _ _ _ _) ≟ empty = no λ() + (outSolRes _ _ _ _) ≟ (pair _ _) = no λ() + (inOneWay _ _) ≟ (outNotify _ _ _) = no λ() + (inOneWay _ _) ≟ (outSolRes _ _ _ _) = no λ() + (inOneWay _ _) ≟ (inReqRes _ _ _) = no λ() + (inOneWay _ _) ≟ (var _ _) = no λ() + (inOneWay _ _) ≟ empty = no λ() + (inOneWay _ _) ≟ (pair _ _) = no λ() + (inReqRes _ _ _) ≟ (outNotify _ _ _) = no λ() + (inReqRes _ _ _) ≟ (outSolRes _ _ _ _) = no λ() + (inReqRes _ _ _) ≟ (inOneWay _ _) = no λ() + (inReqRes _ _ _) ≟ (var _ _) = no λ() + (inReqRes _ _ _) ≟ empty = no λ() + (inReqRes _ _ _) ≟ (pair _ _) = no λ() + (var _ _) ≟ (outNotify _ _ _) = no λ() + (var _ _) ≟ (outSolRes _ _ _ _) = no λ() + (var _ _) ≟ (inOneWay _ _) = no λ() + (var _ _) ≟ (inReqRes _ _ _) = no λ() + (var _ _) ≟ empty = no λ() + (var _ _) ≟ (pair _ _) = no λ() + (pair _ _) ≟ (outNotify _ _ _) = no λ() + (pair _ _) ≟ (outSolRes _ _ _ _) = no λ() + (pair _ _) ≟ (inOneWay _ _) = no λ() + (pair _ _) ≟ (inReqRes _ _ _) = no λ() + (pair _ _) ≟ (var _ _) = no λ() + (pair _ _) ≟ empty = no λ() + + decSetoid : DecSetoid _ _ + decSetoid = PropEq.decSetoid _≟_ + + +Ctx : ℕ → Set +Ctx = Vec TypeDecl diff --git a/src/Typecheck.agda b/src/Typecheck.agda index 26b2800..e5f7e3a 100644 --- a/src/Typecheck.agda +++ b/src/Typecheck.agda @@ -1,7 +1,10 @@ module Typecheck where -import Relation.Binary.PropositionalEquality as PropEq +import Data.Vec.Equality as VecEq +open import Relation.Binary.PropositionalEquality as PropEq using (decSetoid) +open import Relation.Nullary.Decidable using (⌊_⌋) open import Data.Maybe using (Maybe; just; nothing) +open import Data.Nat using (ℕ) open import Data.Bool using (if_then_else_) open import Data.Product using (_,_) open import Function @@ -22,11 +25,11 @@ type_of_var : Variable → Maybe BasicType type_of_var (leaf _ v) = just $ type_of_value v type_of_var _ = nothing -data Check (Γ : Ctx) : Behaviour → Set where +data Check {n} (Γ : Ctx n) : Behaviour → Set where yes : {b : Behaviour} → Check Γ b no : {b : Behaviour} → Check Γ b -typecheck_behaviour : (Γ : Ctx) → (b : Behaviour) → Check Γ b +typecheck_behaviour : {n : ℕ} (Γ : Ctx n) → (b : Behaviour) → Check Γ b typecheck_behaviour ctx nil = yes typecheck_behaviour ctx (if e b1 b2) = case e of λ @@ -38,7 +41,8 @@ typecheck_behaviour ctx (if e b1 b2) = -- If e : bool { (just bool) → let ctx2 = typecheck_behaviour ctx b2 in - {!!} + let module CtxEq = VecEq.DecidableEquality Data.Bool.decSetoid in + if ⌊ ctx1 CtxEq.≟ ctx2 ⌋ then yes else no ; _ → no } --case ()