add flag to hide preds (#181)

forge/lang/alloy-syntax/lexer.rkt

@@ -112,6 +112,7 @@
    ["two"       (token+ `TWO-TOK "" lexeme "" lexeme-start lexeme-end)]
    ["univ"      (token+ `UNIV-TOK "" lexeme "" lexeme-start lexeme-end)]
    ["unsat"     (token+ `UNSAT-TOK "" lexeme "" lexeme-start lexeme-end)]  
+   ["wheat"     (token+ `WHEAT-TOK "" lexeme "" lexeme-start lexeme-end)]
    ["break"     (token+ `BREAK-TOK "" lexeme "" lexeme-start lexeme-end)]  
    ["sufficient"     (token+ `SUFFICIENT-TOK "" lexeme "" lexeme-start lexeme-end)]  
    ["necessary"     (token+ `NECESSARY-TOK "" lexeme "" lexeme-start lexeme-end)]  
@@ -297,4 +298,4 @@
                      (pos lex-start) l0 l1)
            #:skip? skip?)))
 
-(provide forge-lexer keyword? paren?)
+(provide forge-lexer keyword? paren?)

forge/lang/alloy-syntax/parser.rkt

@@ -59,7 +59,8 @@ Decl : DISJ-TOK? NameList /COLON-TOK SET-TOK? Expr
 ; note the optional VAR for Electrum. Remember that a preceding / means
 ;  to cut the token; it won't get included in the AST.
 ArrowDecl : VAR-TOK? NameList /COLON-TOK ArrowMult ArrowExpr
-PredDecl : /PRED-TOK (QualName DOT-TOK)? Name ParaDecls? Block
+PredType : WHEAT-TOK
+PredDecl : /PRED-TOK PredType? (QualName DOT-TOK)? Name ParaDecls? Block
 
 ; A function declaration should only ever contain a single expression in its body
 FunDecl : /FUN-TOK (QualName DOT-TOK)? Name ParaDecls? /COLON-TOK Expr /LEFT-CURLY-TOK Expr /RIGHT-CURLY-TOK
@@ -240,4 +241,4 @@ QueryDecl : @Name /COLON-TOK ArrowExpr /EQ-TOK Expr
 NumberList : Number
            | Number /COMMA-TOK @NumberList
 
-Number : NUM-CONST-TOK
+Number : NUM-CONST-TOK

forge/lang/ast.rkt

@@ -36,6 +36,8 @@
 ;       * ...
 ;     * node/formula/quantified (TODO FILL)  -- quantified formula
 ;     * node/formula/multiplicity (TODO FILL) -- multiplicity formula
+;     * node/formula/sealed
+;       * wheat
 ;   * node/int -- integer expression
 ;     * node/int/op (children)
 ;       * node/int/op/add
@@ -884,6 +886,27 @@
        (let* ([x1 (node/expr/quantifier-var (nodeinfo #,(build-source-location stx) check-lang) (node/expr-arity r1) (gensym (format "~a_sum" 'x1)) 'x1)] ...)
          (sum-quant-expr (nodeinfo #,(build-source-location stx) check-lang) (list (cons x1 r1) ...) int-expr)))]))
 
+
+;; -- sealing (for examplar) -----------------------------------------------------------
+
+(define (simple-write-proc str)
+  (lambda (v port mode)
+    (fprintf port "#<~a>" str)))
+
+(struct node/formula/sealed node/formula []
+  #:methods gen:custom-write [(define write-proc (simple-write-proc "node/formula/sealed"))])
+(struct wheat node/formula/sealed []
+  #:methods gen:custom-write [(define write-proc (simple-write-proc "wheat"))]
+  #:extra-constructor-name make-wheat)
+(struct chaff node/formula/sealed []
+  #:methods gen:custom-write [(define write-proc (simple-write-proc "chaff"))]
+  #:extra-constructor-name make-chaff)
+
+(define (unseal-node/formula x)
+  (if (node/formula/sealed? x)
+    (node-info x)
+    x))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ; Build syntax for a generic equals/hash that's robust to new node subtypes
@@ -1174,6 +1197,8 @@
 
 (define (deparse-formula formula parent-priority)
   (match formula
+    [(? node/formula/sealed?)
+     (format "~a" formula)]
     [(node/formula/constant info type)
      (format "~a" type)]
     [(node/formula/op info args)

forge/lang/expander.rkt

@@ -224,9 +224,16 @@
               (~optional name:NameClass)
               block:BlockClass)))
 
+  (define-syntax-class PredTypeClass
+    #:datum-literals (PredType)
+    #:attributes (kw)
+    (pattern (PredType "wheat")
+      #:attr kw #'#:wheat))
+
   ; PredDecl : /PRED-TOK (QualName DOT-TOK)? Name ParaDecls? Block
   (define-syntax-class PredDeclClass
     (pattern ((~literal PredDecl)
+              (~optional _:PredTypeClass)
               (~optional (~seq prefix:QualNameClass "."))
               name:NameClass
               (~optional decls:ParaDeclsClass)
@@ -648,16 +655,18 @@
 ; PredDecl : /PRED-TOK (QualName DOT-TOK)? Name ParaDecls? Block
 (define-syntax (PredDecl stx)
   (syntax-parse stx
-  [((~literal PredDecl) (~optional (~seq prefix:QualNameClass "."))
+  [((~literal PredDecl) (~optional pt:PredTypeClass)
+                        (~optional (~seq prefix:QualNameClass "."))
                         name:NameClass
                         block:BlockClass)
    (with-syntax ([block #'block])
      (quasisyntax/loc stx (begin
        (~? (raise (format "Prefixes not allowed: ~a" 'prefix)))
        ; preserve stx location in Racket *sub*expression
-       #,(syntax/loc stx (pred (#:lang (get-check-lang)) name.name block)))))]
+       #,(syntax/loc stx (pred (~? pt.kw) (#:lang (get-check-lang)) name.name block)))))]
 
-  [((~literal PredDecl) (~optional (~seq prefix:QualNameClass "."))
+  [((~literal PredDecl) (~optional pt:PredTypeClass)
+                        (~optional (~seq prefix:QualNameClass "."))
                         name:NameClass
                         decls:ParaDeclsClass
                         block:BlockClass)
@@ -667,7 +676,7 @@
      (quasisyntax/loc stx (begin
        (~? (raise (format "Prefixes not allowed: ~a" 'prefix)))
        ; preserve stx location in Racket *sub*expression
-       #,(syntax/loc stx (pred (#:lang (get-check-lang)) decl block)))))]))
+       #,(syntax/loc stx (pred (~? pt.kw) (#:lang (get-check-lang)) decl block)))))]))
 
 ; FunDecl : /FUN-TOK (QualName DOT-TOK)? Name ParaDecls? /COLON-TOK Expr Block
 (define-syntax (FunDecl stx)

forge/last-checker.rkt

@@ -67,6 +67,8 @@
                               (let ([new-quantvars (append (map assocify decls) quantvars)])       
                                 ; CHECK: recur into subformula
                                 (checkFormula run-or-state subform new-quantvars checker-hash))))]
+    [(node/formula/sealed info)
+     (checkFormula run-or-state info quantvars)]
     [else (error (format "no matching case in checkFormula for ~a" (deparse formula)))]))
 
 (define (assocify a-pair)  

forge/sigs.rkt

@@ -372,37 +372,37 @@
          (~@ (check-temporal-for-var isv true-name))
          (update-state! (state-add-relation curr-state true-name name))))]))
 
+(begin-for-syntax
+  (define-splicing-syntax-class pred-type
+    #:description "optional pred flag"
+    #:attributes ((seal 0))
+    (pattern (~datum #:wheat)
+      #:attr seal #'make-wheat)
+    (pattern (~seq)
+      #:attr seal #'values)))
+
 ; Declare a new predicate
 ; (pred info name cond ...)
 ; (pred info (name var ...) cond ...)
 ;   or same without info
 (define-syntax (pred stx)
   (syntax-parse stx
-    [(pred name:id conds:expr ...+)
+    [(pred pt:pred-type
+           (~optional (#:lang check-lang) #:defaults ([check-lang #''checklangNoCheck]))
+           name:id conds:expr ...+)
      (quasisyntax/loc stx
        (begin
          ; use srcloc of actual predicate, not this location in sigs
-         (define name (&&/info (nodeinfo #,(build-source-location stx) 'checklangNoCheck) conds ...))
+         (define name (pt.seal (&&/info (nodeinfo #,(build-source-location stx) check-lang) conds ...)))
          (update-state! (state-add-pred curr-state 'name name))))]
-    [(pred (name:id args:id ...+) conds:expr ...+)
+    [(pred pt:pred-type
+           (~optional (#:lang check-lang) #:defaults ([check-lang #''checklangNoCheck]))
+           (name:id args:id ...+) conds:expr ...+)
      (quasisyntax/loc stx
        (begin 
-         (define (name args ...) (&&/info (nodeinfo #,(build-source-location stx) 'checklangNoCheck) conds ...))
-         (update-state! (state-add-pred curr-state 'name name))))]
-
-    ; Case: check-lang
-    [(pred (#:lang check-lang) name:id conds:expr ...+)
-     (quasisyntax/loc stx
-       (begin
-         ; use srcloc of actual predicate, not this location in sigs
-         (define name (&&/info (nodeinfo #,(build-source-location stx) check-lang) conds ...))
-         (update-state! (state-add-pred curr-state 'name name))))]
-    [(pred (#:lang check-lang) (name:id args:id ...+) conds:expr ...+)
-     (quasisyntax/loc stx
-       (begin 
-         (define (name args ...) (&&/info (nodeinfo #,(build-source-location stx) check-lang) conds ...))
+         (define (name args ...) (pt.seal (&&/info (nodeinfo #,(build-source-location stx) check-lang) conds ...)))
          (update-state! (state-add-pred curr-state 'name name))))]))
-                                   
+
 ; Declare a new function
 ; (fun (name var ...) result)
 (define-syntax (fun stx)

forge/tests/error/hidden-wheat.frg

@@ -0,0 +1,11 @@
+#lang forge
+
+sig Node {edges: set Node}
+
+pred wheat hiddenPred {
+    edges = ~edges
+}
+
+check { true } for { hiddenPred }
+// Invalid bounds should not print the hidden pred
+

forge/tests/error/main.rkt

@@ -89,6 +89,7 @@
     (list "formula_comprehension_cardinality.frg" #rx"expected to be given")
     (list "formula_comprehension_multiplicity.frg" #rx"expected to be given")
     (list "hello.frg" #rx"parsing error")
+    (list "hidden-wheat.frg" #rx"^Invalid bind: #<wheat>$")
     (list "ill_typed_inst_columns_reversed.frg" #rx"age")
     (list "inst-undefined-bound-child-one.frg" #rx"for an ancestor of")
     (list "invalid-example.frg" #rx"Invalid example 'onlyBabies'")
@@ -106,7 +107,7 @@
     (with-check-info*
       (list (make-check-name test-name))
       (lambda ()
-        (check-exn pred (lambda () (run-error-test test-name)))))
+        (check-exn pred (lambda () (re-raise-strings (run-error-test test-name))))))
     (void)))
 
 (define (run-error-test test-name)
@@ -116,6 +117,9 @@
       (dynamic-require root-module #f)
       (dynamic-require `(submod ,root-module execs) #f))))
 
+(define-syntax-rule (re-raise-strings expr)
+  (with-handlers ([string? raise-user-error]) expr))
+
 ;; -----------------------------------------------------------------------------
 
 (module+ main

forge/translate-to-kodkod-cli.rkt

@@ -42,6 +42,8 @@
      (print-cmd-cont ") ")
      (interpret-formula run-or-state form relations atom-names new-quantvars)
      (print-cmd-cont ")")]
+    [(node/formula/sealed info)
+     (interpret-formula info relations atom-names quantvars)]
 
      ; (let ([quantvars (cons var quantvars)])
      ;   ( print-cmd-cont (format "(~a ([~a : ~a " quantifier (v (get-var-idx var quantvars)) (if (@> (node/expr-arity var) 1) "set" "one")))