2 Standalone Parenlog
#lang parenlog | package: parenlog |
Parenlog can also be used as a standalone module language.
At a high level, the body of a Parenlog module is the body of a define-model form and any REPL interaction is placed within a query-model form. There are, of course, a few caveats.
First, occurrences of (? body-query) in the module body are delayed and used as queries.
Second, all query results are printed. no is printed when there are no answeres. yes is printed when there is an empty
substitution as an answer. Otherwise, the substitution is printed using (hash-for-each subst (curry printf "~a=~a~n")), resulting in
displays like:
X=moria Y=larn
Third, next searches for another answer to the last query. If there was no last query, this evaluates to an error. If there are no more answers, done is printed.
Here is a sample module:
#lang parenlog (type Gamma numConst num) (type Gamma boolConst bool) (:- (type Gamma (if Test Then Else) Tau) (type Gamma Test bool) (type Gamma Then Tau) (type Gamma Else Tau)) (? (type mt numConst num)) (? (type mt (if boolConst numConst numConst) num)) (? (type mt (if boolConst numConst boolConst) num)) (? (type mt boolConst T)) (? (type mt (if boolConst numConst numConst) T)) (? (type mt (if boolConst numConst boolConst) T))
If this module is evaluated, it prints:
yes yes no T=bool T=num no
We can then query the model from the REPL:
> next
done
> (type mt T num)
T=numConst
> next
T=(if boolConst numConst numConst)
> next
T=(if boolConst numConst (if boolConst numConst numConst))
Syntax that may only appear within the body of a Parenlog module.
Syntax that may only appear within the body of a Parenlog module.