Merge branch 'dev' into site

tnelson · Apr 5, 2024 · 673469e · 673469e
2 parents 68224ea + d939200
commit 673469e
Show file tree

Hide file tree

Showing 94 changed files with 1,603 additions and 408 deletions.
diff --git a/README.md b/README.md
@@ -32,10 +32,10 @@ To install from source, use the following commands. Make sure that you have [Rac
 
 ```
 git clone https://github.com/tnelson/Forge
-cd Forge/forge
-raco pkg install
+cd Forge
+raco pkg install ./forge ./froglet
 ```
 
-To update, `git pull` the repo and run `raco setup forge`.
+To update, `git pull` the repo and run `raco setup forge` to recompile.
 
-Running on the development branch, `dev`, requires only `checkout dev` before installing; this may be unstable, however.
+Running on the development branch, `dev`, requires `checkout dev` before installing; this may be unstable, however.
diff --git a/forge/breaks.rkt b/forge/breaks.rkt
@@ -652,11 +652,18 @@
 
     (define (funcformula rllst quantvarlst)
         (cond
-            [(empty? (rest (rest rllst))) 
-                (let ([a (gensym)])
-                    (@all/info (@just-location-info loc) ([a (first rllst)]) (@one (funcformulajoin (cons a quantvarlst)))))]
-            [else (let ([a (gensym)])
-                    (@all/info (@just-location-info loc) ([a (first rllst)]) (funcformula (rest rllst) (cons a quantvarlst))))]))
+          [(empty? (rest (rest rllst)))
+           (let* ([var-id (gensym 'pfunc)]
+                  [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
+             (@quantified-formula (@just-location-info loc) 'all
+                                  (list (cons a (first rllst)))
+                                  (@one (funcformulajoin (cons a quantvarlst)))))]
+            [else
+             (let* ([var-id (gensym 'pfunc)]
+                  [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
+             (@quantified-formula (@just-location-info loc) 'all
+                                  (list (cons a (first rllst)))
+                                  (funcformula (rest rllst) (cons a quantvarlst))))]))
     (define formulas (set (funcformula rel-list (list))))
 
     ; OLD CODE
@@ -716,22 +723,31 @@
             (λ () (break bound formulas)))
 ))
 
-(add-strategy 'pfunc (λ (pri rel bound atom-lists rel-list [loc #f])
-
-    (define (pfuncformulajoin quantvarlst) 
-        (cond 
-            [(empty? (rest quantvarlst)) (@join (first quantvarlst) rel)]
-            [else (@join (first quantvarlst) (pfuncformulajoin (rest quantvarlst)))]))
-    (define (pfuncformula rllst quantvarlst)
-        (cond
-            [(empty? (rest (rest rllst))) 
-                (let ([a (gensym)])
-                    (@all/info (@just-location-info loc) ([a (first rllst)]) (@lone (pfuncformulajoin (cons a quantvarlst)))))]
-            [else (let ([a (gensym)])
-                    (@all/info (@just-location-info loc) ([a (first rllst)]) (pfuncformula (rest rllst) (cons a quantvarlst))))]))
-
-    (define formulas (set (pfuncformula rel-list (list))))
 
+(add-strategy 'pfunc
+              (λ (pri rel bound atom-lists rel-list [loc #f])
+                (define (pfuncformulajoin quantvarlst) 
+                  (cond
+                    ; x_n.rel
+                    [(empty? (rest quantvarlst)) (@join (first quantvarlst) rel)]
+                    ; ... x_n-1.x_n.rel
+                    [else (@join (first quantvarlst) (pfuncformulajoin (rest quantvarlst)))]))
+                (define (pfuncformula rllst quantvarlst)
+                  (cond
+                    [(empty? (rest (rest rllst)))
+                     (let* ([var-id (gensym 'pfunc)]
+                            [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
+                       (@quantified-formula (@just-location-info loc) 'all
+                                            (list (cons a (first rllst)))
+                                            (@lone (pfuncformulajoin (cons a quantvarlst)))))]
+                    [else (let* ([var-id (gensym 'pfunc)]
+                                 [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
+                            (@quantified-formula (@just-location-info loc) 'all
+                                                 (list (cons a (first rllst)))
+                                                 (pfuncformula (rest rllst) (cons a quantvarlst))))]))
+                (define pf-fmla (pfuncformula rel-list (list)))
+                (define formulas (set pf-fmla))
+
     ; OLD CODE
     ; (if (equal? A B)
     ;     (formula-breaker pri ; TODO: can improve, but need better symmetry-breaking predicates

diff --git a/forge/evaluator.rkt b/forge/evaluator.rkt
@@ -21,21 +21,21 @@
     (raise-user-error (format "Can't evaluate on unsat run. Expression: ~a" expression)))
   (define-values (expr-name interpretter)
     (cond [(node/expr? expression)
-           (checkExpression (Run-run-spec run) expression '() (get-checker-hash))
+           (checkExpression run expression '() (get-checker-hash))
            (define currents (Run-kodkod-currents run))
            (define expression-number (Kodkod-current-expression currents)) 
            (set-Kodkod-current-expression! currents (add1 expression-number))
            (values (pardinus:e expression-number)
                    interpret-expr)]
           [(node/formula? expression)
-           (checkFormula (Run-run-spec run) expression '() (get-checker-hash))
+           (checkFormula run expression '() (get-checker-hash))
            (define currents (Run-kodkod-currents run))
            (define formula-number (Kodkod-current-formula currents)) 
            (set-Kodkod-current-formula! currents (add1 formula-number))
            (values (pardinus:f formula-number)
                    interpret-formula)]
           [(node/int? expression)
-           ; ? No last-checker?
+           (checkInt run expression '() (get-checker-hash))
            (define currents (Run-kodkod-currents run))
            (define int-number (Kodkod-current-int currents)) 
            (set-Kodkod-current-int! currents (add1 int-number))

diff --git a/forge/info.rkt b/forge/info.rkt
@@ -2,7 +2,7 @@
 
 (define collection "forge")
 
-(define version "3.3")
+(define version "3.4.1")
 
 (define implies '("froglet"))
 (define deps '("base"

diff --git a/forge/lang/alloy-syntax/lexer.rkt b/forge/lang/alloy-syntax/lexer.rkt
@@ -108,7 +108,8 @@
    ["some"      (token+ `SOME-TOK "" lexeme "" lexeme-start lexeme-end)]
    ["sum"       (token+ `SUM-TOK "" lexeme "" lexeme-start lexeme-end #f #t)]
    ["test"      (token+ `TEST-TOK "" lexeme "" lexeme-start lexeme-end)]
-   ["theorem"   (token+ `THEOREM-TOK "" lexeme "" lexeme-start lexeme-end)] 
+   ["theorem"   (token+ `THEOREM-TOK "" lexeme "" lexeme-start lexeme-end)]
+   ["forge_error" (token+ `FORGE_ERROR-TOK "" lexeme "" lexeme-start lexeme-end)]
    ["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)]  

diff --git a/forge/lang/alloy-syntax/parser.rkt b/forge/lang/alloy-syntax/parser.rkt
@@ -85,7 +85,8 @@ ParaDecls : /LEFT-PAREN-TOK @ParaDeclList? /RIGHT-PAREN-TOK
 AssertDecl : /ASSERT-TOK Name? Block
 CmdDecl :  (Name /COLON-TOK)? (RUN-TOK | CHECK-TOK) (QualName | Block)? Scope? (/FOR-TOK Bounds)?
 
-TestDecl : (Name /COLON-TOK)? (QualName | Block)? Scope? (/FOR-TOK Bounds)? /IS-TOK (SAT-TOK | UNSAT-TOK | THEOREM-TOK)
+TestDecl : (Name /COLON-TOK)? (QualName | Block) Scope? (/FOR-TOK Bounds)? /IS-TOK
+           (SAT-TOK | UNSAT-TOK | THEOREM-TOK | FORGE_ERROR-TOK)
 TestExpectDecl : TEST-TOK? EXPECT-TOK Name? TestBlock
 TestBlock : /LEFT-CURLY-TOK TestDecl* /RIGHT-CURLY-TOK
 Scope : /FOR-TOK Number (/BUT-TOK @TypescopeList)?