Codebase list cafeobj / 0d1a4c1
update md of reference manual Norbert Preining 8 years ago
1 changed file(s) with 183 addition(s) and 43 deletion(s). Raw diff Collapse all Expand all
+183
-43
doc/refman/reference.md less more
5454
5555 The predicate for behavioral equivalence, written `=*=`, is a binary
5656 operator defined on each hidden sort.
57
58 TODO: old manual very unclear ... both about `=*=` and
59 `accept =*= proof` ??? (page 46 of old manual)
6057
6158
6259 ## `=/=` ## {#notequal}
323320
324321 ## `binspect [in <module-name> :] <boolean-term> .` ## {#binspect}
325322
326 TODO
323 Start an inspection of a Boolean term, that is, and abstracted
324 form of the Boolean term is constructed. The abstracted term is shown (like calling [`bshow`](#bshow).
325
326 ### Example ###
327
328
329 ~~~~~
330 CafeOBJ> module BTE { [S]
331 preds p1 p2 p3 p4 p5 p6 p7 : S
332 ops a b c : -> S .
333 }
334 CafeOBJ> binspect in BTE : (p1(X:S) or p2(X)) and p3(Y:S) or (p4(Y) and p1(Y)) .
335 ...
336 --> ((p4(Y:S) and p1(Y)) xor ((p3(Y) and p1(X:S)) xor ((p2(X) and (p3(Y) and p1(X))) xor ((p3(Y) and p2(X)) xor ((p3(Y) and (p2(X) and (p4(Y) and p1(Y)))) xor ((p3(Y) and (p2(X) and (p1(X) and (p1(Y) and p4(Y))))) xor (p1(X) and (p3(Y) and (p1(Y) and p4(Y))))))))))
337 ...
338 ~~~~~
339
327340
328341 ## `:binspect [in <goal-name> :] <boolean-term> .` ## {#citp-binspect}
329342
330 TODO
343 See [`binspect`](#binspect)
331344
332345 ## `bop <op-spec> : <sorts> -> <sort>` ## {#bop}
333346
361374
362375 ## `{bresolve | :bresolve}` ## {#bresolve}
363376
364 TODO
377 Computes all possible variable assignments that render an abstracted
378 term `true`.
379
380 ### Example ###
381
382
383 ~~~~~
384 CafeOBJ> bresolve
385
386 ** The following assignment(s) can make the term 'true'.
387 (1): { P-5:Bool |-> true, P-4:Bool |-> true, P-3:Bool |-> true, P-2:Bool |-> true, P-1:Bool |-> true }
388 (2): { P-5:Bool |-> false, P-4:Bool |-> true, P-3:Bool |-> true, P-2:Bool |-> true, P-1:Bool |-> true }
389 ...
390 ~~~~~
391
365392
366393 ## `brule [ <label-exp> ] <term> => <term> .` ## {#brule}
367394
372399
373400 ## `{bshow | :bshow} [tree]` ## {#bshow}
374401
375 TODO
402 Shows the abstracted Boolean term computed by [`binspect`](#binspect).
403 If the argument `tree` is given, prints out a the abstracted term in tree form.
404
405 ### Example ###
406
407
408 ~~~~~
409 CafeOBJ> bshow
410 ((P-1:Bool and (P-2:Bool and (P-3:Bool and P-4:Bool))) xor ((P-1 and (P-2 and (P-4 and (P-5:Bool and P-3)))) xor ((P-2 and (P-1 and (P-5 and P-3))) xor ((P-5 and P-3) xor ((P-4 and (P-3 and P-5)) xor ((P-4 and P-3) xor (P-2 and P-1)))))))
411 where
412 P-1:Bool |-> p4(Y:S)
413 P-2:Bool |-> p1(Y:S)
414 P-3:Bool |-> p3(Y:S)
415 P-4:Bool |-> p1(X:S)
416 P-5:Bool |-> p2(X:S)
417 ~~~~~
418
376419
377420 ## `bsort` ## {#bsort}
378421
466509
467510 The sub-system provides a certain level of automatization for theorem proving.
468511
469 TODO TODO
470
471
472 Related: [`:define`](#citp-def), [`:ctf-`](#citp-ctf-), [`:ctf`](#citp-ctf), [`:csp-`](#citp-csp-), [`:csp`](#citp-csp), [`:red`](#citp-red), [`:select`](#citp-select), [`:backward`](#citp-backward), [`:rule`](#citp-rule), [`:equation`](#citp-equation), [`:cp`](#citp-cp), [`:init`](#citp-init), [`:roll`](#citp-roll), [`:auto`](#citp-auto), [`:ind`](#citp-ind), [`:apply`](#citp-apply), [`:goal`](#citp-goal)
512 Please see the accompanying manual for CITP for details.
513
514
515 Related: [`:imp`](#citp-imply), [`:def`](#citp-def), [`:ctf-`](#citp-ctf-), [`:ctf`](#citp-ctf), [`:csp-`](#citp-csp-), [`:csp`](#citp-csp), [`:red`](#citp-red), [`:select`](#citp-select), [`:backward`](#citp-backward), [`:rule`](#citp-rule), [`:equation`](#citp-equation), [`:cp`](#citp-cp), [`:init`](#citp-init), [`:roll`](#citp-roll), [`:auto`](#citp-auto), [`:ind`](#citp-ind), [`:apply`](#citp-apply), [`:goal`](#citp-goal)
473516
474517 ## `clause <term> .` ## {#clause}
475518
524567
525568
526569
527 ## `:cp { "[" <label> "]" | "(" <sentense> . ")" } >< { "[" <label> "]" | "(" <sentence> .")" }` ## {#citp-cp}
570 ## `:cp { "[" <label> "]" | "(" <sentence> . ")" } >< { "[" <label> "]" | "(" <sentence> .")" }` ## {#citp-cp}
528571
529572 TODO specify critical pair
530573
539582
540583 ## `:csp { eq [ <label-exp>] <term> = <term> . ...}` ## {#citp-csp}
541584
542 TODO applies case splitting after general equations TODO
585 Applies case splitting after a set of equations. Each of these
586 equations creates one new sub-goal with the equation added.
587
588 The system does not check whether given set of equations exhausts all
589 possible values.
590
591 Not discharged sub-goals will remain in the reduced form.
543592
544593 Related: [`:csp-`](#citp-csp-), [`citp`](#citp)
545594
546595 ## `:csp- { eq [ <label-exp>] <term> = <term> . ...}` ## {#citp-csp-}
547596
548 TODO
597 Like [`:csp`](#:csp), but if sub-goals are not discharged, the
598 CITP prover returns to the original state before the reduce action.
549599
550600 Related: [`:csp`](#citp-csp), [`citp`](#citp)
551601
552602 ## `:ctf { eq [ <label-exp> ] <term> = <term> .}` ## {#citp-ctf}
553603
554 TODO Applies case splitting after a set of boolean expressions.
604 Applies case splitting after a set of boolean expressions.
605 Not discharged sub-goals will remain in the reduced form.
555606
556607 Related: [`:ctf-`](#citp-ctf-), [`citp`](#citp)
557608
558609 ## `:ctf- { eq [ <label-exp> ] <term> = <term> .}` ## {#citp-ctf-}
559610
560 TODO
611 Like [`:ctf`](#:ctf), but if sub-goals are not discharged, the
612 CITP prover returns to the original state before the reduce action.
561613
562614 Related: [`:ctf`](#citp-ctf), [`citp`](#citp)
563615
583635
584636 ### Example ###
585637
586 `````
638 ~~~~~
587639 :def name-1 = ctf [ <Term> . ]
588640 :def name-2 = ctf-{ eq LHS = RHS . }
589641 :def name-3 = csp { eq lhs1 = rhs1 . eq lhs2 = rhs2 . }
590642 :def name-4 = csp-{ eq lhs3 = rhs3 . eq lhs4 = rhs4 . }
591643 :apply(SI TC name-1 name-2 name-3 name-4)
592 `````
644 ~~~~~
593645
594646
595647 ## `demod` ## {#demod}
597649 (pignose)
598650
599651
600 ## `:describe <something>` ## {#citp-describe}
601
602 Similar to the `:show` command but with more details. Call `:describe ?` for
603 the possible set of invocations.
604
652 ## `:describe proof` ## {#citp-describe}
653
654 Describes the current proof in more detail.
605655
606656 Related: [`:show`](#citp-show), [`citp`](#citp)
657
658 ### Example ###
659
660
661 ~~~~~
662 PNAT> :describe proof
663 ==> root*
664 -- context module: #Goal-root
665 -- targeted sentences:
666 eq [lemma-1]: M:PNat + 0 = M .
667 eq [lemma-2]: M:PNat + s N:PNat = s (M + N) .
668 [si] 1*
669 -- context module: #Goal-1
670 -- targeted sentences:
671 eq [lemma-1]: 0 + 0 = 0 .
672 eq [lemma-2]: 0 + s N:PNat = s (0 + N) .
673 ...
674 ~~~~~
675
607676
608677 ## `describe <something>` ## {#describe}
609678
615684
616685 ## `dirs` ## {#dirs}
617686
618
619
687 Displays the current push stack.
688
689
690 Related: [`popd`](#popd), [`pwd`](#pwd), [`pushd`](#pushd), [`cd`](#cd), [`ls`](#ls)
620691
621692 ## `dribble` ## {#dribble}
622693
762833
763834 ## `:goal { <sentence> . ... }` ## {#citp-goal}
764835
836 Define the initial goal for CITP
837
838 Related: [`citp`](#citp)
839
840 ### Example ###
841
842
843 ~~~~~
844 CafeOBJ> select PNAT .
845 PNAT> :goal {
846 eq [lemma-1]: M:PNat + 0 = M .
847 eq [lemma-2]: M:PNat + s N:PNat = s( M + N ) .
848 }
849 ~~~~~
850
851
852 ## `goal <term> .` ## {#goal}
853
854 (pignose)
855
856
857 ## `:imp "[" <label> "]" by "{" <variable> <- <term>; ..."}"` ## {#citp-imply}
858
765859 TODO
766860
767 ## `goal <term> .` ## {#goal}
768
769 (pignose)
770
861 Related: [`citp`](#citp)
771862
772863 ## `imports { <import-decl> }` ## {#imports}
773864
813904
814905 Related: [`citp`](#citp)
815906
816 ## `:init { "[" <label> "]" | "(" <sentence> "")} "{" <variable> <- <term>; ... "}"` ## {#citp-init}
907 ### Example ###
908
909
910 ~~~~~
911 :ind on (M:PNat)
912 ~~~~~
913
914
915 ## `:init { "[" <label> "]" | "(" <sentence> "")} by "{" <variable> <- <term>; ... "}"` ## {#citp-init}
817916
818917 TODO
819918
9561055
9571056 ## `look up <something>` ## {#lookup}
9581057
959 TODO (memory-fault on sbcl)
1058 displays the location (module) and further information
1059 where `<something>` has been defined.
1060
1061
1062 ### Example ###
1063
1064 ~~~~~
1065 open INT .
1066 %INT> look up Nat .
1067
1068 Nat
1069 - sort declared in NAT-VALUE
1070 - operator:
1071 op Nat : -> SortId { constr prec: 0 }
1072 -- declared in module NAT-VALUE
1073
1074 %INT>
1075 ~~~~~
9601076
9611077
9621078 ## `ls <pathname>` ## {#ls}
13021418
13031419 ## `popd` ## {#popd}
13041420
1305
1306
1421 Changes the current working directory to the last on on the push stack.
1422
1423
1424 Related: [`dirs`](#dirs), [`pwd`](#pwd), [`pushd`](#pushd), [`cd`](#cd), [`ls`](#ls)
13071425
13081426 ## `pred <op-spec> : <sorts>` ## {#pred}
13091427
13701488
13711489 ## `pushd <directory>` ## {#pushd}
13721490
1373
1374
1491 Changes the working directory to `<directory>`, and puts the
1492 current directory onto the push stack. Going back can be done with `pop`.
1493
1494
1495 Related: [`dirs`](#dirs), [`pwd`](#pwd), [`popd`](#popd), [`cd`](#cd), [`ls`](#ls)
13751496
13761497 ## `pvar <var-name> : <sort-name>` ## {#pvar}
13771498
13851506 Prints the current working directory.
13861507
13871508
1388 Related: [`ls`](#ls), [`cd`](#cd)
1509 Related: [`dirs`](#dirs), [`popd`](#popd), [`pushd`](#pushd), [`ls`](#ls), [`cd`](#cd)
13891510
13901511 ## qualified sort/operator/parameter ## {#qualifiedother}
13911512
16371758 Set or show various flags of CITP CafeOBJ.
16381759
16391760
1761 Related: [`citp`](#citp)
1762
16401763 ## `set <name> [option] <value>` ## {#set}
16411764
16421765 Depending on the type of the switch, options and value specification varies.
16501773
16511774 Related: [`switches`](#switches), [`show`](#show)
16521775
1653 ## `:show <something>` ## {#citp-show}
1654
1655 TODO
1776 ## `:show goal|unproved|proof` ## {#citp-show}
1777
1778 Shows the current goal, the up-to-now unproven (sub-)goals, and the current proof.
16561779
16571780 Related: [`:describe`](#citp-describe), [`citp`](#citp)
1781
1782 ### Example ###
1783
1784
1785 ~~~~~
1786 PNAT> :show proof
1787 root*
1788 [si] 1*
1789 [ca] 1-1*
1790 [ca] 1-2*
1791 [tc] 1-2-1*
1792 [si] 2*
1793 [ca] 2-1*
1794 [ca] 2-2*
1795 [tc] 2-2-1*
1796 PNAT>
1797 ~~~~~
1798
16581799
16591800 ## `show <something>` ## {#show}
16601801
16781819 ## `show mode` switch ## {#switch-show-mode}
16791820
16801821 Possible values for `set show mode <mode>` are `cafeobj` and `meta`.
1681
1682 TODO no further information on what this changes
16831822
16841823
16851824 ## `sigmatch (<mod-exp>) to (<mod-exp>)` ## {#sigmatch}
17921931 : set (or unset) max number of rewrite
17931932
17941933 Other standard CafeOBJ commands that can be used are [`show`](#show),
1795 [`describe`](#describe), [`set`](#set), [`cd`](#cd), [`ls`](#ls),
1796 [`pwd`](#pwd), [`lisp`](#lisp), [`lispq`](#lisp), and (on Unix only)
1934 [`describe`](#describe), [`dirs`](#dirs), [`set`](#set), [`cd`](#cd),
1935 [`ls`](#ls), [`pwd`](#pwd), [`pushd`](#pushd), [`popd`](#popd),
1936 [`lisp`](#lisp), [`lispq`](#lisp), and (on Unix only)
17971937 [`!`](#commandexec).
17981938
17991939