froglet early 2023 commits

froglet: error test for 'negate implies'

froglet: context-sensitive join checks

froglet: field lookup, stop at shadows

froglet: can require from forge, but cannot use

froglet: serialize funtype, fix type=?

froglet: reachable, basic join checks

2+ args
1st arg object
Nth arg field

froglet: reachable again

3+ args: (tgt, src, acc, ...)
 [[ check the docs! ]]
 tgt must be object
 src must be object
 acc must be valid field ... for src alone? for more?

froglet: checkpoint, reachable trans.closure search

froglet, reachable march-forward analysis

stxclass: ~literal to ~datum

froglet: no obj checks for examples, insts

froglet: start checking bridge_crossing

froglet: loosen = typecheck, allow <: or :>

froglet: add paramtypes to current env

tf4: consttype parsing, ifelse delay check

checkpoint

froglet: upgrade pred names to formulas, when 0 args

tf4: fix inst-check outline

tf4: allow 'no x | x.next' etc

tf4: allow bound { field is linear }

froglet: stricter binary op checks

tf4: progress on bridge_crossing, on to pets

tf4: add a srcloc, add stx->mult

tf4: basic reltype, unop #, deparsing

tf4: hide froglet env to allow +2 imports

tf4: +2 binop names

froglet: pred, allow multiplicity on params

froglet: env-fold, use helper for fn return

froglet: parse fun output type

froglet: lookup names in param env

tf4: better ifelse checking

checkpoint

forge/tests/error/froglet-ast-notimplies.frg

@@ -0,0 +1,12 @@
+#lang froglet
+option run_sterling off
+
+sig Node {
+    next: lone Node
+}
+one sig A, B extends Node{}
+
+pred err {
+    A not implies B else C
+}
+

forge/tests/error/froglet-compareop0.frg

@@ -0,0 +1,15 @@
+#lang froglet
+
+abstract sig Position {}
+one sig Near extends Position {}
+one sig Far extends Position {}
+
+sig State {
+    torch: one Position,
+    spent: one Int
+}
+
+pred ValidState[s: State] {
+    s.torch = 0
+}
+

forge/tests/error/froglet-compareop1.frg

@@ -0,0 +1,15 @@
+#lang froglet
+
+abstract sig Position {}
+one sig Near extends Position {}
+one sig Far extends Position {}
+
+sig State {
+    torch: one Position,
+    spent: one Int
+}
+
+pred ValidState[s: State] {
+    s.spent = Near
+}
+

forge/tests/error/froglet-compareop2.frg

@@ -0,0 +1,15 @@
+#lang froglet
+
+abstract sig Position {}
+one sig Near extends Position {}
+one sig Far extends Position {}
+
+sig State {
+    torch: one Position,
+    spent: one Int
+}
+
+pred ValidState[s: State] {
+    s.torch <= 2
+}
+

forge/tests/error/froglet-compareop3.frg

@@ -0,0 +1,15 @@
+#lang froglet
+
+abstract sig Position {}
+one sig Near extends Position {}
+one sig Far extends Position {}
+
+sig State {
+    torch: one Position,
+    spent: one Int
+}
+
+pred ValidState[s: State] {
+    s.spent <= Near
+}
+

forge/tests/error/froglet-field-shadow.frg

@@ -0,0 +1,21 @@
+#lang froglet
+
+// Student created a quantified variable that's named the same as a field, then tried to use the field. (https://edstem.org/us/courses/31922/discussion/2548781?comment=5844098).
+// https://edstem.org/us/courses/31922/discussion/2548781?comment=5844098
+
+sig Person {
+  spouse: lone Person
+}
+
+pred ownGrandparent {
+  one me: Person, spouse: Person | {
+    spouse.spouse = me
+  }
+}
+
+//pred oG2 {
+//  some me: Person, spouse: Person | {
+//    spouse.spouse = me
+//  }
+//}
+//

forge/tests/error/froglet-is-linear0.frg

@@ -0,0 +1,11 @@
+#lang froglet
+option run_sterling off
+
+sig Node {
+    next: lone Node
+}
+
+pred pp {
+    next is linear
+}
+

forge/tests/error/froglet-is-linear1.frg

@@ -0,0 +1,9 @@
+#lang froglet
+option run_sterling off
+
+sig Node {
+    next: lone Node
+}
+
+check {} for { Node is linear }
+

forge/tests/error/froglet-no-field.frg

@@ -0,0 +1,13 @@
+#lang froglet
+
+// no father = disallowed at toplevel
+
+sig Person {
+ father: lone Person
+}
+one sig Tim extends Person {}
+
+pred myPred {
+  no father
+}
+

forge/tests/error/froglet-pubkey2.frg

@@ -0,0 +1,21 @@
+#lang froglet -- forge
+
+abstract sig Key {}
+sig Pubk, Privk extends Key {}
+
+one sig Authority {
+  pairs: func Pubk -> Privk
+}
+
+fun counterpart[k: one Key]: one Key {
+  -- this produces an error, since k is known to be a Pubk
+  /*
+  join always results in an empty relation:
+  Left argument of join "(Authority.pairs)" is in ((Pubk -> Privk))
+  Right argument of join "k" is in ((Pubk))
+  There is no possible join result
+  in: "(Authority.pairs.k)"
+  */
+  Authority.pairs.k
+}
+

forge/tests/error/froglet-reachable3.frg

@@ -0,0 +1,15 @@
+#lang froglet
+option run_sterling off
+
+sig Node {
+  next: lone Node
+}
+
+sig A {
+  field: one Node
+}
+
+pred cycle {
+  reachable[]
+}
+

forge/tests/error/froglet-reachable4.frg

@@ -0,0 +1,16 @@
+#lang froglet
+option run_sterling off
+
+sig Node {
+  next: lone Node
+}
+
+sig A {
+  field: one Node
+}
+
+pred cycle {
+  all n: Node | reachable[n.next]
+}
+
+

forge/tests/error/froglet-reachable5.frg

@@ -0,0 +1,21 @@
+#lang froglet
+option run_sterling off
+
+-- error: cannot reach target because types don't line up
+--  need NA -> NB -> NC -> NA but missing one link
+
+sig Node {}
+sig NA extends Node {
+  na: lone NB
+}
+sig NB extends Node {
+  nb: lone NC
+}
+sig NC extends Node {
+  nc: lone NA
+}
+
+pred cycle {
+  all n: NA | reachable[n, n.na, na, nb]
+}
+

forge/tests/error/froglet-reachable6.frg

@@ -0,0 +1,17 @@
+#lang froglet
+option run_sterling off
+
+-- error: useless field, cannot reach a sig that might use the field
+
+sig Node {}
+sig NA extends Node {
+  na: lone NA
+}
+sig NB extends Node {
+  nb: lone NB
+}
+
+pred cycle {
+  all n: NA | reachable[n, n.na, na, nb]
+}
+

forge/tests/error/froglet-uni-2.frg

@@ -11,5 +11,5 @@ sig Person {
 one sig Tim extends Person {}
 
 pred myPred {
- some father
+  some father
 }

forge/tests/error/froglet-uni-5.frg

@@ -0,0 +1,15 @@
+#lang froglet
+option run_sterling off
+
+sig University {}
+one sig BrownU extends University {}
+sig Person {
+ father: lone Person,
+ mother: lone Person,
+ grad: lone University
+}
+one sig Tim extends Person {}
+
+pred myPred {
+ some Tim.Tim
+}

forge/tests/error/main.rkt

@@ -53,9 +53,17 @@
     (list "froglet-ast-star.frg" #rx"\\* operator is not")
     (list "froglet-ast-transitive-closure.frg" #rx"\\^ operator is not")
     (list "froglet-ast-transpose.frg" #rx"~ operator is not")
+    (list "froglet-ast-notimplies.frg" #rx"parsing error")
     (list "froglet-arrow.frg" #rx"-> operator is not")
+    (list "froglet-compareop0.frg" #rx"inputs to = must have similar type")
+    (list "froglet-compareop1.frg" #rx"inputs to = must have similar type")
+    (list "froglet-compareop2.frg" #rx"expected an Int")
+    (list "froglet-compareop3.frg" #rx"expected an Int")
     (list "froglet-http.frg" #rx"field declaration")
     (list "froglet-int-minus.frg" #rx"- operator is not")
+    (list "froglet-field-shadow.frg" #rx"expected a field")
+    (list "froglet-is-linear0.frg" #rx"outside of bounds block")
+    (list "froglet-is-linear1.frg" #rx"expected a field")
     (list "froglet-join-right.frg" #rx"not an object")
     (list "froglet-join-right2.frg" #rx"not an object")
     (list "froglet-join-right3.frg" #rx"not an object")
@@ -65,16 +73,40 @@
     (list "froglet-join.frg" #rx"not an object")
     (list "froglet-join2.frg" #rx"not a singleton") ;; TODO incomplete or partial?
     (list "froglet-join3.frg" #rx"not an object")
+    (list "froglet-no-field.frg" #rx"expected an object")
     (list "froglet-pred.frg" #rx"expected a formula")
-    (list "froglet-reachable.frg" #rx"field") ;; TODO
-    (list "froglet-reachable2.frg" #rx"not a singleton") ;; TODO
+    (list "froglet-reachable1.frg" #rx"no field match")
+    (list "froglet-reachable2.frg" #rx"expected an object")
+    (list "froglet-reachable3.frg" #rx"parsing error")
+    (list "froglet-reachable4.frg" #rx"reachable expects 2 or more arguments")
+    (list "froglet-reachable5.frg" #rx"reachable found no path to target")
+    (list "froglet-reachable6.frg" #rx"reachable cannot use field")
     (list "froglet-set-singleton-equal.frg" #rx"not a singleton") ;;(#rx"= expects two objects, sig Node is not an object")
     (list "froglet-set.frg" #rx"not a singleton") #;( "pred must return an object, not a set")
-;    (list "froglet-uni-0.frg" #rx"expected a sig")
-;    (list "froglet-uni-1.frg" #rx"expected a sig")
-;    (list "froglet-uni-2.frg" #rx"is not a value") ;; TODO better block checking
-;    (list "froglet-uni-3.frg" #rx"expected a sig")
-;    (list "froglet-uni-4.frg" #rx"expected a sig") ;; TODO reachable, double-check
+    (list "froglet-uni-0.frg" #rx"expected an object")
+    (list "froglet-uni-1.frg" #rx"expected an object")
+    (list "froglet-uni-2.frg" #rx"expected an object") ;; or, a singleton
+    (list "froglet-uni-3.frg" #rx"expected an object")
+    (list "froglet-uni-4.frg" #rx"expected a field")
+    (list "froglet-uni-5.frg" #rx"expected a field")
+    (list "froglet-pubkey2.frg" #rx"field 'k' not found")
+
+    ;; challenge
+    ;; - [X] pubkey2 froglet expected a field got k
+    ;;   ... lookup works for `pairs`, not for `k`,
+    ;;       should find the k parameter in the environment!
+    ;; - [X] expected a formula (why?!) given a name in k
+    ;; - [X] pubkey2: why unknown type for 1st branch
+    ;; - [ ] pubkey2
+    ;;   froglet: binop-check: (#<syntax in> '#s(type #<syntax Unknown>)
+    ;;   '#s((nametype type 1) #<syntax:pubkey2.frg:30:34 Pubk>))
+    ;; - [ ] pubkey2: refine branch type
+    ;; - [ ] pubkey2: is function type parsing broken?
+    ;; TODO catch all bsl errors from here
+    ;; TODO check Ed for bounds errors
+    ;; TODO modeling in anger ... invalid bounds
+
+    ;; FYI forge has an evaluator, used to eval in inst specs, typechecker may need it too!
 
     (list "example_electrum.frg" #rx"example foo: .* temporal")
     (list "example_impossible.frg" #rx"Invalid example 'onlyBabies'")

forge/tests/froglet/forge.frg

@@ -0,0 +1,4 @@
+#lang forge
+
+sig A {}
+

forge/tests/froglet/froglet-uni.frg

@@ -14,7 +14,15 @@ pred myPred {
  some p: Person | reachable[p, Tim, father, mother]
 }
 
+pred p2 {
+  no Tim.father
+}
+
 test expect {
  myPred is sat
 }
 
+example ex1 is { p2 } for {
+  no father
+}
+

forge/tests/froglet/require-forge.frg

@@ -0,0 +1,8 @@
+#lang froglet
+
+open "forge.frg"
+
+sig B {
+  // a: lone A
+}
+

froglet/lang/reader.rkt

@@ -4,7 +4,7 @@
 
 (require
   (only-in froglet/util lang-name type-env-name)
-  (only-in froglet/typecheck/main typecheck)
+  (only-in froglet/typecheck/main typecheck env-serialize)
   (only-in forge/lang/reader coerce-ints-to-atoms)
   (only-in forge/lang/alloy-syntax/main parse make-tokenizer)
   (prefix-in log: forge/logging/2022/main))
@@ -43,7 +43,7 @@
        ;; Override default exception handler
 
        (require (only-in racket/base define-values))
-       (define-values (,type-env-name) ',type-env)
+       (module+ ,type-env-name (define-values (,type-env-name) ',(env-serialize type-env)) (provide ,type-env-name))
        ,alloymod
 
        (module+ execs)

froglet/typecheck/error.rkt

@@ -11,6 +11,8 @@
 (require
   froglet/util)
 
+(error-print-context-length 4)
+
 ;; ---
 
 (define who 'froglet)