컴포지트 표현식 카탈로그

let: Π1 → Π2

let x = expr1 in expr2

이 표현식은 expr1을 평가하는 expr2x 변수에 대한 모든 참조와 함께 expr2를 평가합니다. expr1expr2에 각각 Π 유형이 몇 가지 있어야 하지만 이러한 표현식 유형은 동일하지 않아야 합니다. 즉, expr1에 유형 Π1이 있고 expr2에 유형 Π2가 있는 경우 Π1 = Π2일 필요는 없습니다.

   let x = 5 in x + 7 ⇒ 12
   (let x = 5 in x + 7) + 3 ⇒ 15
   let x = 5 in let y = 7 in x + y ⇒ 12
   let x = 5 + 7 in x + 3 ⇒ 15
   let x = 5 in let x = x * x in x ⇒ 25
   let x = model in class x ⇒ Model
   let x = all "Class" in size x <> 0 ⇒ true
   let x = all "Class" in size x <> 0 implies
   (there_exists y in x => $name of y = "Dishwasher") ⇒ true
   let x = all "Class" in size x <> 0 implies
   (there_exists y in x => $name of y = "FooBar") ⇒ false

if: boolean x Π x Π → Π

if test then expr1 else expr2

이 표현식 값은 테스트 값에 따라 달라집니다. 테스트에서 true로 평가되는 경우 전체 표현식이 expr1을 평가합니다. 그렇지 않으면 전체 표현식이 expr2를 평가합니다. 테스트 유형은 boolean이어야 하며, expr1expr2 모두의 유형이 일부 Π여야 합니다. expr1expr2의 유형은 동일해야 합니다. 즉, expr1에 유형 Π1이 있고 expr2에 유형 Π2가 있는 경우 Π1 = Π2여야 합니다.

   if true then 1 else 0 => 1
   if class x = "Operation"
   then "Found Operation"
   else "Found " + class x => Found Model
   (if false then "abc" else "123") + "def" => 123def

for_all: object collection x (object → boolean) → boolean

for_all x in ocoll => predicate ≡ not (there_exists x in ocoll => not
predicate)

there_exists: object collection x (object → boolean) → boolean

there_exists x in ocoll => predicate ≡ not (for_all x in ocoll => not
predicate)

이러한 표현식은 검증 ∀xεocoll(predicate(x)) 및 ∃xεocoll(predicate(x))을 평가합니다. 즉, for_all은 둘 중 하나가 비어 있거나 모든 오브젝트가 술어를 만족하는 경우에만 true를 리턴합니다. there_existsocoll술어를 만족하는 오브젝트가 하나 이상 있는 경우에만 true를 리턴합니다.

이러한 표현식의 실제 평가는 다음과 같은 방식으로 수행됩니다. for_allthere_exists의 경우 모두 ocoll의 각 오브젝트에 변수 x가 차례로 바인드되고 x의 바인딩에 대한 컨텍스트에서 술어가 평가됩니다. 술어가 false로 평가되면 for_all도 false로 평가됩니다. 술어가 true로 평가되면 there_exists도 true로 평가됩니다. ocoll의 모든 오브젝트가 테스트되기 전에 두 조건이 모두 발생하지 않으면 for_all은 true로 평가되고 there_exists는 false로 평가됩니다. 또한 이러한 표현식이 각 x 바인딩에서 퍼베이시브 변수 currentx에 바인딩합니다.

표현식 ocoll의 유형은 오브젝트 콜렉션이어야 하며 술어의 유형은 부울이어야 합니다(오브젝트부울(x술어에 대한 암시적 매개변수임)).

다음 예제에서는 세 개의 클래스, 이름이 지정된 트리, 분기 및 리프가 있다고 가정합니다.

   for_all x in all "Class" => class x = "Class" ≡
   for_all x in all "Class" => class current = "Class" ⇒ true
   there_exists x in all "Class" => $name = "Leaf" ⇒ true
   for_all x in all "Class" => $name = "Leaf" ⇒ false
   not (for_all x in all "Class" => $name <> "Leaf") ⇒ true
   for_all x in anEmptyCollection => false ⇒ true
   for_all x in anyCollection => current = x ≡ true ⇒ true
   for_all class in all "Class" =>
      there_exists op in class->[operation] =>
         $name of op = "grow" ⇒ false

피드백