Commit 9a4d21bb3d2403532a21791631b0b80bd29f79e4 - cafeobj

* Experimental implementation of online help system. * Introduces 'cl-ppcre' for manipulating Markdown formatted documents. tswd 9 years ago

15 changed file(s) with 1405 addition(s) and 1577 deletion(s). Raw diff Collapse all Expand all

+24

-78

cafeobj/command-top.lisp less more

273	273	;;;
274	274	(defparameter .?-invalid-chars. '("." "#" "'" "`"))
275	275
	276	#\|\|
276	277	(defun cafeobj-what-is (inp)
277	278	(flet ((check-pat (pat)
278	279	(if (not (some #'(lambda (str)

297	298	(if desc
298	299	(format t desc)
299	300	(format t "~&Unknown command/switch or message ID: ~{~a ~^~}." (cdr inp))))))
	301	\|\|#
	302
	303	(defun cafeobj-what-is (inp)
	304	(let* ((ask (intern (car inp)))
	305	(question (cdr inp))
	306	(key (reduce #'(lambda (x y) (concatenate 'string x y)) question))
	307	(description nil))
	308	(case ask
	309	(\|?\| (setq description (get-document-string key)))
	310	;; (\|??\| (setq description (get-detailed-document key)))
	311	;; ((\|?ex\| \|?example\|) (setq description (get-example key)))
	312	(otherwise
	313	;; this cannot happen
	314	(with-output-chaos-error ('internal-error)
	315	(format t "Unknown help command ~a" (car inp)))))
	316	(cond (description
	317	(format t (format-description description)))
	318	(t (with-output-chaos-warning ()
	319	(format t "System does not know about \"~{~a~^~}\"." question))))))
300	320
301	321	;;;
302	322	(defun get-command-description (level id)

459	479	#+CLISP (ext::exit))
460	480
461	481	;;;
462		;;; DEFCOM
463		;;;
464		(defvar cafeobj-commands (make-hash-table :test #'equal))
465
466		(defstruct (command (:print-function print-command))
467		(name "" :type string) ; command name
468		(category nil :type symbol) ; command types
469		(parser nil :type symbol) ; parser function
470		(evaluator nil :type symbol) ; evaluator function
471		(help-string "" :type string)) ; command's help string
472
473		(defun print-command (me &optional (stream standard-output) &rest ignore)
474		(declare (ignore ignore))
475		(format stream "~&** command : ~a" (command-name me))
476		(format stream "~% category : ~a" (command-category me))
477		(format stream "~% parser : ~a" (command-parser me))
478		(format stream "~% evaluator : ~a" (command-evaluator me))
479		(format stream "~% description : ~a" (command-help-string me)))
480
481		(defun print-command-usage (command &optional (stream standard-output))
482		(let ((com (if (command-p command)
483		command
484		(and (stringp command)
485		(gethash command cafeobj-commands)))))
486		(unless com
487		(with-output-chaos-error ('no-com)
488		(format t "No such command '~a'" command)))
489		(format stream "~&~a : ~a" (command-name com) (command-help-string com))))
490
491		(defmacro defcom ((&rest names) doc-string category parser evaluator)
492		(unless (fboundp parser) (warn "no parser ~s" parser))
493		(unless (fboundp evaluator) (warn "no evaluator ~s" evaluator))
494		`(dolist (name ',names)
495		(setf (gethash name cafeobj-commands)
496		(make-command :name name
497		:category ',category
498		:parser ',parser
499		:evaluator ',evaluator
500		:help-string ,doc-string))))
501		;;;
502		;;; DEFDECL
503		;;;
504		(defstruct (decl (:print-function print-decl) (:include command)))
505
506		(defmacro defdecl ((&rest names) doc-string category parser evaluator)
507		(unless (fboundp parser) (warn "no parser ~s" parser))
508		(unless (fboundp evaluator) (warn "no evaluator ~s" evaluator))
509		`(dolist (name ',names)
510		(setf (gethash name cafeobj-declarations)
511		(make-decl :name name
512		:category ',category
513		:parser ',parser
514		:evaluator ',evaluator
515		:help-string ,doc-string))))
516
517		(defun print-decl (me &optional (stream standard-output) &rest ignore)
518		(declare (ignore ignore))
519		(format stream "~&** declaration : ~a" (decl-name me))
520		(format stream "~% category : ~a" (decl-category me))
521		(format stream "~% parser : ~a" (decl-parser me))
522		(format stream "~% evaluator : ~a" (decl-evaluator me))
523		(format stream "~% description : ~a" (decl-help-string me)))
524
525		(defun print-decl-usage (decl &optional (stream standard-output))
526		(let ((decl (if (decl-p decl)
527		decl
528		(and (stringp decl)
529		(gethash decl cafeobj-declarations)))))
530		(unless decl
531		(with-output-chaos-error ('no-decl)
532		(format t "No such declaration form '~a'" decl)))
533		(format stream "~&~a : ~a" (decl-name decl) (decl-help-string decl))))
534
535		;;;
536	482	;;; NOP
537	483	;;;
538	484	(defun cafeobj-nop (&rest ignore)

543	489	;;;
544	490	(defun cafeobj-evaluate-command (key inp)
545	491	(declare (type string key))
546		(let ((com (gethash key cafeobj-commands)))
	492	(let ((com (get-command-info key)))
547	493	(unless com
548	494	(with-output-chaos-error ('no-commands)
549	495	(format t "No such command or declaration keyword '~a'." key)))
550		(let ((parser (command-parser com)))
	496	(let ((parser (comde-parser com)))
551	497	(unless parser
552	498	(with-output-chaos-error ('no-parser)
553	499	(format t "No parser is defined for command ~a" key)))

556	502	(with-output-chaos-error ('parse-error)
557	503	(format t "Invalid argument to command ~a." key)))
558	504	(if (eq pform :help)
559		(print-command-usage com)
560		(let ((evaluator (command-evaluator com)))
	505	(print-comde-usage com)
	506	(let ((evaluator (comde-evaluator com)))
561	507	(unless evaluator
562	508	(with-output-chaos-error ('no-evaluator)
563	509	(format t "No evaluator is defined for command ~a." key)))

+962

-0

cafeobj/commands.lisp less more

	0	;;;-- Mode:LISP; Package:CHAOS; Base:10; Syntax:Common-lisp --
	1	#\|==============================================================================
	2	System: CHAOS
	3	Module: cafeobj
	4	File: commands.lisp
	5	==============================================================================\|#
	6	(in-package :chaos)
	7	#-:chaos-debug
	8	(declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
	9	#+:chaos-debug
	10	(declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
	11
	12	(eval-when (:execute :load-toplevel)
	13
	14	;;; ---------------------------------------------------------------------------
	15	;;; these hash tables are used for register keywords, document strings.
	16	;;; these are used by toplevel command interpreter
	17	;;; and cafeobj language construct evaluators.
	18	;;; ---------------------------------------------------------------------------
	19
	20	;; halds systems toplevel commands, declarations accepted by top level
	21	(clrhash cafeobj-top-commands)
	22
	23	;; holds all of the declaration forms
	24	(clrhash cafeobj-declarations)
	25
	26	;; this holds each commands/language constructs document strings.
	27	;; systems' doc-generator refers to this hash table.
	28	(clrhash cafeobj-doc-db)
	29
	30	;;; --------------------------------------------------------------------------
	31	;;; all of the declarations/commands in alphabetical order.
	32	;;; --------------------------------------------------------------------------
	33
	34	(define ("??" "?")
	35	:category :help
	36	:parser identity
	37	:evaluator cafeobj-top-level-help
	38	:doc "
	39	## `?` ## {#help}
	40
	41	lists all top-level commands. The `?` can be used after many of the
	42	top-level commands to obtain help.
	43	")
	44
	45
	46	(define ("!")
	47	:category :misc
	48	:parser parse-shell-command
	49	:evaluator eval-ast
	50	:doc "
	51	## `! <command>` ## {#commandexec}
	52
	53	TODO Currently not working!!
	54
	55	On Unix only, forks a shell and executes the given `<command>`.
	56	")
	57
	58
	59	(define ("--" "**")
	60	:category :decl-toplevel
	61	:parser parse-comment-command
	62	:evaluator identity
	63	:doc "
	64	")
	65
	66
	67	(define ("-->" "**>")
	68	:doc "
	69	"
	70	:category :decl-toplevel
	71	:parser parse-comment-command
	72	:evaluator eval-ast)
	73
	74	(define ("=")
	75	:type :doc-only
	76	:doc "
	77	## `=` ## {#axeq}
	78
	79	The syntax element `=` introduces an axiom of the equational theory,
	80	and is different from `==` which specifies an equality based on
	81	rewriting.
	82
	83	Related: [`==`](#equality) [`eq`](#eq)
	84	")
	85
	86	(define ("==")
	87	:type :doc-only
	88	:doc "
	89	## `==` ## {#equality}
	90
	91	The predicate `==` is a binary operator defined for each visible sort
	92	and is defined in terms of evaluation. That is, for ground terms `t`
	93	and `t'` of the same sort, `t == t'` evaluates to `true` iff terms
	94	reduce to a common term. This is different from the equational `=`
	95	which specifies the equality of the theory.
	96	")
	97
	98	(define ("=>")
	99	:type :doc-only
	100	:doc
	101	"
	102	## `==>` ## {#transrel}
	103
	104	This binary predicate is defined on each visible sort, and defines the
	105	transition relation, which is reflexive, transitive, and closed under
	106	operator application. It expresses the fact that two states (terms)
	107	are connected via transitions.
	108	Related: [`trans`](#trans) [`=(*)=>`](#transsearch)
	109	")
	110
	111	(define ("=*=")
	112	:type :doc-only
	113	:doc "
	114	## `=*=` ## {#bequality}
	115
	116	The predicate for behavioural equivalence, written `=*=`, is a binary
	117	operator defined on each hidden sort.
	118
	119	TODO: old manual very unclear ... both about `=*=` and
	120	`accept =*= proof` ??? (page 46 of old manual)
	121	")
	122
	123	(define ("dribble")
	124	:category :misc
	125	:parser parse-dribble-command
	126	:evaluator eval-ast
	127	:doc "
	128	")
	129
	130	(define ("mod" "module" "module" "mod" "module!" "mod!" "sys:mod!" "sys:module!" "sys:mod" "sys:module")
	131	:category :decl-toplevel
	132	:parser process-module-declaration-form
	133	:evaluator eval-ast
	134	:doc "
	135	## `module[!\|*] <modname> [ ( <params> ) ] [ <principal_sort_spec> ] { mod_elements ... }` ## {#module}
	136
	137	Alias: `mod`
	138
	139	defines a module, the basic building block of \_cafeobj. Possible elements
	140	are declarations of
	141
	142	- import - see `protecting`, `extending`, `including`, `using`
	143	- sorts - see `sort declaration`
	144	- variable - see `var`
	145	- equation - see `op`, `eq`, `ceq`, `bop`, `beq`, `bceq`
	146	- transition - see `trans`, `ctrans`, `btrans`, `bctrans`
	147
	148	`modname` is an arbitrary string.
	149
	150	`module*` introduces a loose semantic based module.
	151
	152	`module!` introduces a strict semantic based module.
	153
	154	`module` introduces a module without specified semantic type.
	155
	156	If `params` are given, it is a parametrized module. See `parametrized module`
	157	for more details.
	158
	159	If `principal_sort_spec` is given, it has to be of the form
	160	`principal-sort <sortname>` (or `p-sort <sortname>`). The principal
	161	sort of the module is specified, which allows more concise `view`s from
	162	single-sort modules as the sort mapping needs not be given.
	163	")
	164
	165	(define ("view")
	166	:category :decl-toplevel
	167	:parser process-view-declaration-form
	168	:evaluator eval-ast
	169	:doc "
	170	## `view <name> from <modname> to <modname> { <viewelems> }` ## {#view}
	171
	172	A view specifies ways to bind actual parameters to formal parameters
	173	(see [parametrized module](#parametrizedmodule)). The view has to
	174	specify the mapping of the sorts as well as the operators.
	175
	176	The `<viewelems>` is a comma-separated list of expressions specifying
	177	these mappings:
	178
	179	~~~~
	180	sort <sortname> -> <sortname>
	181	hsort <sortname> -> <sortname>
	182	op <opname> -> <opname>
	183	bop <opname> -> <opname>
	184	~~~~
	185
	186	and also can contain variable declarations.
	187
	188	Infix operators are represented as terms containing the operator with
	189	either literal underscores `_`, or variables: `__` or `X Y`.
	190	The `<opname>` can be qualified.
	191
	192	Example: Assume a module `MONOID` with sort `M` and ops `e` and `*`
	193	are given, and another `SIMPLE-NAT` with sort `Nat` and operators `0`
	194	and `+` (with the same arity). Then the following expression
	195	constitutes a view:
	196
	197	~~~~~
	198	view NAT-AS-MONOID from MONOID to SIMPLE-NAT {
	199	sort M -> Nat,
	200	op e -> 0,
	201	op _*_ -> _+_
	202	}
	203	~~~~~
	204
	205	In specifying views some rules can be omitted:
	206
	207	1. If the source and target modules have common submodules, all the
	208	sorts and modules decalred therein are assumed to be mapped to
	209	themselves;
	210
	211	2. If the source and target modules have sorts and/or operators with
	212	identical names, they are mapped to their respective counterparts;
	213
	214	3. If the source module has a single sort and the target has a
	215	principal sort, the single sort is mapped to the principal sort.
	216	")
	217
	218	(define ("check")
	219	:category :checker
	220	:parser parse-check-command
	221	:evaluator eval-ast
	222	:doc "
	223	## `check <options>` ## {#check}
	224
	225	This command allows for checking of certain properties of modules and
	226	operators.
	227
	228	`check regularity <mod_exp>`
	229	~ Checks whether the module given by the module expression
	230	`<mod_exp>` is regular.
	231
	232	`check compatibility <mod_exp>`
	233	~ Checks whether term rewriting system of the module given by the
	234	module expression `<mod_exp>` is compatible, i.e., every
	235	application of every rewrite rule to every well-formed term
	236	results in a well-formed term. (This is not necessarily the case
	237	in order-sorted rewriting!)
	238
	239	`check laziness <op_name>`
	240	~ Checks whether the given operator can be evaluated lazily. If not
	241	`<op_name>` is given, all operators of the current module are
	242	checked.
	243
	244	Related: [`regularize`](#regularize)
	245	")
	246
	247	(define ("regularize")
	248	:category :module
	249	:parser parse-regularize-command
	250	:evaluator eval-ast
	251	:doc "
	252	## `regularize <mod-name>` ## {#regularize}
	253
	254	Regularizes the signature of the given module, ensuring that every
	255	term has exactely one minimal parse tree. In this process additional
	256	sorts are generated to ensure unique least sort of all terms.
	257
	258	Modules can be automatically regularized by the interpreter if the
	259	`regularize signature` switch is turn to `on`.
	260
	261	TODO -- should we give more details here -- unclear to me.
	262	")
	263
	264	(define ("exec" "execute")
	265	:category :rewrite
	266	:parser parse-exec-command
	267	:evaluator eval-ast
	268	:doc "
	269	## `execute [ in <mod-exp> : ] <term> .` ## {#execute}
	270
	271	Alias: `exec`
	272
	273	Reduce the given term in the given module, if `<mod-exp>` is given,
	274	otherwise in the current module.
	275
	276	For `execute` equations and transitions, possibly conditional, are taken
	277	into account for reduction.
	278
	279	Related: [`breduce`](#breduce) [`reduce`](#reduce)
	280	")
	281
	282	(define ("red" "reduce")
	283	:category :rewrite
	284	:parser parse-reduce-command
	285	:evaluator eval-ast
	286	:doc "
	287	reduce [in <Modexpr> :] <Term> . ~%Rewrite <Term> by axioms of the module.
	288	")
	289
	290	(define ("exec!" "execute!")
	291	:category :rewrite
	292	:parser parse-exec+-command
	293	:evaluator eval-ast
	294	:doc "
	295	exec! [in <Modexpr> :] <Term> .
	296	")
	297
	298	(define ("bred" "breduce")
	299	:category :rewrite
	300	:parser parse-bred-command
	301	:evaluator eval-ast
	302	:doc "
	303	")
	304
	305	(define ("version")
	306	:category :misc
	307	:parser parse-version-command
	308	:evaluator princ
	309	:doc "
	310	prints version number of the system.
	311	")
	312
	313	(define ("cbred")
	314	:category :rewrite
	315	:parser parse-cbred-command
	316	:evaluator eval-ast
	317	:doc "
	318	")
	319
	320	(define ("stop")
	321	:category :rewrite
	322	:parser parse-stop-at
	323	:evaluator eval-ast
	324	:doc "
	325	")
	326
	327	(define ("parse")
	328	:category :parse
	329	:parser parse-parse-command
	330	:evaluator eval-ast
	331	:doc "
	332	")
	333
	334	(define ("match" "unify")
	335	:category :inspect
	336	:parser parse-match-command
	337	:evaluator eval-ast
	338	:doc "
	339	")
	340
	341	(define ("lisp" "ev")
	342	:category :system
	343	:parser parse-eval-lisp
	344	:evaluator cafeobj-eval-lisp-proc
	345	:doc "
	346	")
	347
	348	(define ("lispq" "evq")
	349	:category :system
	350	:parser parse-eval-lisp
	351	:evaluator cafeobj-eval-lisp-q-proc
	352	:doc "
	353	")
	354
	355	(define ("make")
	356	:category :decl-toplevel
	357	:parser parse-make-command
	358	:evaluator eval-ast
	359	:doc "
	360	")
	361
	362	(define ("in" "input")
	363	:category :misc
	364	:parser parse-input-command
	365	:evaluator cafeobj-eval-input-proc
	366	:doc "
	367	")
	368
	369	(define ("save")
	370	:category :io
	371	:parser parse-save-command
	372	:evaluator eval-ast
	373	:doc "
	374	")
	375
	376	(define ("restore")
	377	:category :io
	378	:parser parse-restore-command
	379	:evaluator eval-ast
	380	:doc "
	381	")
	382
	383	(define ("reset")
	384	:category :system
	385	:parser parse-reset-command
	386	:evaluator eval-ast
	387	:doc (("reset"
	388	"
	389	remove declarations of user defined modules and views from the system.
	390	")))
	391
	392	(define ("full" "full-reset")
	393	:doc ((("full reset" "full-reset") "reset system to initial status."))
	394	:category :system
	395	:parser parse-full-reset-command
	396	:evaluator eval-ast)
	397
	398	(define ("clean")
	399	:category :rewrite
	400	:parser identity
	401	:evaluator cafeobj-eval-clear-memo-proc
	402	:doc "
	403	")
	404
	405	(define ("prelude")
	406	:category :library
	407	:parser parse-prelude-command
	408	:evaluator cafeobj-eval-prelude-proc
	409	:doc "
	410	")
	411
	412	(define ("let")
	413	:category :decl-toplevel
	414	:parser process-let-declaration-form
	415	:evaluator eval-ast
	416	:doc "
	417	")
	418
	419	(define ("imports")
	420	:category :module-element
	421	:parser identity
	422	:evaluator cafeobj-eval-module-element-proc
	423	:doc "
	424	## `imports { <import-decl> }` ## {#imports}
	425
	426	Block enclosing import of other modules (`protecting` etc).
	427	Other statements are not allowed within the `imports` block.
	428	Optional structuring of the statements in a module.
	429
	430	Related: [`signature`](#signature) [`axioms`](#axioms)
	431	[`extending`](#extending) [`including`](#including)
	432	[`protecting`](#protecting) [`using`](#using)
	433	")
	434
	435	(define ("ex" "extending")
	436	:category :module-element
	437	:parser identity
	438	:evaluator cafeobj-eval-module-element-proc
	439	:doc "
	440	## `extending ( <modexp> )` ## {#extending}
	441
	442	Alias: `ex`
	443
	444	imports the object specified by `modexp` into the current
	445	module, allowing models to be inflated, but not collapsing.
	446	See [`module expression`](#moduleexpression) for format of `modexp`.
	447
	448	Related: [`including`](#including) [`protecting`](#protecting)
	449	[`using`](#using)
	450	")
	451
	452	(define ("pr" "protecting")
	453	:category :module-element
	454	:parser identity
	455	:evaluator cafeobj-eval-module-element-proc
	456	:doc "
	457	")
	458
	459	(define ("us" "using")
	460	:category :module-element
	461	:parser identity
	462	:evaluator cafeobj-eval-module-element-proc
	463	:doc "
	464	")
	465
	466	(define ("inc" "including")
	467	:category :module-element
	468	:parser identity
	469	:evaluator cafeobj-eval-module-element-proc
	470	:doc "
	471	")
	472
	473	(define ("[")
	474	:category :module-element
	475	:parser identity
	476	:evaluator cafeobj-eval-module-element-proc
	477	:doc "
	478	")
	479
	480	(define ("*")
	481	:category :module-element
	482	:parser identity
	483	:evaluator cafeobj-eval-module-element-proc
	484	:doc "
	485	")
	486
	487	(define ("bsort")
	488	:category :module-element
	489	:parser identity
	490	:evaluator cafeobj-eval-module-element-proc
	491	:doc "
	492	")
	493
	494	(define ("op" "ops")
	495	:category :module-element
	496	:parser identity
	497	:evaluator cafeobj-eval-module-element-proc
	498	:doc "
	499	")
	500
	501	(define ("bop" "bops")
	502	:category :module-element
	503	:parser identity
	504	:evaluator cafeobj-eval-module-element-proc
	505	:doc "
	506	")
	507
	508	(define ("pred")
	509	:category :module-element
	510	:parser identity
	511	:evaluator cafeobj-eval-module-element-proc
	512	:doc "
	513	")
	514
	515	(define ("bpred")
	516	:category :module-element
	517	:parser identity
	518	:evaluator cafeobj-eval-module-element-proc
	519	:doc "
	520	")
	521
	522	(define ("dpred") ; only for pignose
	523	:category :module-element
	524	:parser identity
	525	:evaluator cafeobj-eval-module-element-proc
	526	:doc "
	527	")
	528
	529	(define ("dbpred") ; only for pignose
	530	:category :module-element
	531	:parser identity
	532	:evaluator cafeobj-eval-module-element-proc
	533	:doc "
	534	")
	535
	536	(define ("sig" "signature")
	537	:category :module-element
	538	:parser identity
	539	:evaluator cafeobj-eval-module-element-proc
	540	:doc "
	541	")
	542
	543	(define ("axiom" "ax")
	544	:category :module-element
	545	:parser identity
	546	:evaluator cafeobj-eval-module-element-proc
	547	:doc "
	548	")
	549
	550	(define ("axioms" "axs")
	551	:category :module-element
	552	:parser identity
	553	:evaluator cafeobj-eval-module-element-proc
	554	:doc "
	555	")
	556
	557	(define ("ax") ; pignose
	558	:category :module-element
	559	:parser identity
	560	:evaluator cafeobj-eval-module-element-proc
	561	:doc "
	562	")
	563
	564	(define ("bax") ; pignose
	565	:category :module-element
	566	:parser identity
	567	:evaluator cafeobj-eval-module-element-proc
	568	:doc "
	569	")
	570
	571	(define ("goal") ; pignose
	572	:category :module-element
	573	:parser identity
	574	:evaluator cafeobj-eval-module-element-proc
	575	:doc "
	576	")
	577
	578	(define ("bgoal") ; pignose
	579	:category :module-element
	580	:parser identity
	581	:evaluator cafeobj-eval-module-element-proc
	582	:doc "
	583	")
	584
	585	(define ("#define")
	586	:category :module-element
	587	:parser identity
	588	:evaluator cafeobj-eval-module-element-proc
	589	:doc "
	590	")
	591
	592	(define ("var" "vars")
	593	:category :module-element
	594	:parser identity
	595	:evaluator cafeobj-eval-module-element-proc
	596	:doc "
	597	")
	598
	599	(define ("pvar" "pvars")
	600	:category :module-element
	601	:parser identity
	602	:evaluator cafeobj-eval-module-element-proc
	603	:doc "
	604	")
	605
	606	(define ("eq" "ceq" "cq")
	607	:category :module-element
	608	:parser identity
	609	:evaluator cafeobj-eval-module-element-proc
	610	:doc "
	611	")
	612
	613	(define ("beq" "bceq" "bcq")
	614	:category :module-element
	615	:parser identity
	616	:evaluator cafeobj-eval-module-element-proc
	617	:doc "
	618	")
	619
	620	(define ("trans" "ctrans")
	621	:category :module-element
	622	:parser identity
	623	:evaluator cafeobj-eval-module-element-proc
	624	:doc "
	625	")
	626
	627	(define ("trns" "ctrns")
	628	:category :module-element
	629	:parser identity
	630	:evaluator cafeobj-eval-module-element-proc
	631	:doc "
	632	")
	633
	634	(define ("rule" "crule")
	635	:category :module-element
	636	:parser identity
	637	:evaluator cafeobj-eval-module-element-proc
	638	:doc "
	639	")
	640
	641	(define ("rl" "crl")
	642	:category :module-element
	643	:parser identity
	644	:evaluator cafeobj-eval-module-element-proc
	645	:doc "
	646	")
	647
	648	(define ("btrans" "bctrans")
	649	:category :module-element
	650	:parser identity
	651	:evaluator cafeobj-eval-module-element-proc
	652	:doc "
	653	")
	654
	655	(define ("brule" "bcrule")
	656	:category :module-element
	657	:parser identity
	658	:evaluator cafeobj-eval-module-element-proc
	659	:doc "
	660	")
	661
	662	(define ("btrns" "bctrns")
	663	:category :module-element
	664	:parser identity
	665	:evaluator cafeobj-eval-module-element-proc
	666	:doc "
	667	")
	668
	669	(define ("brl" "bcrl")
	670	:category :module-element
	671	:parser identity
	672	:evaluator cafeobj-eval-module-element-proc
	673	:doc "
	674	")
	675
	676	(define ("open")
	677	:category :proof
	678	:parser parse-open-command
	679	:evaluator eval-ast
	680	:doc "
	681	")
	682
	683	(define ("close")
	684	:category :proof
	685	:parser parse-close-command
	686	:evaluator eval-ast
	687	:doc "
	688	")
	689
	690	(define ("start")
	691	:category :proof
	692	:parser parse-start-command
	693	:evaluator eval-ast
	694	:doc "
	695	")
	696
	697	(define ("apply")
	698	:category :proof
	699	:parser parse-apply-command
	700	:evaluator eval-ast
	701	:doc "
	702	")
	703
	704	(define ("choose")
	705	:category :proof
	706	:parser parse-choose-command
	707	:evaluator eval-ast
	708	:doc "
	709	")
	710
	711	(define ("inspect")
	712	:category :proof
	713	:parser parse-inspect-term-command
	714	:evaluator eval-ast
	715	:doc "
	716	")
	717
	718	(define ("find")
	719	:category :proof
	720	:parser parse-find-command
	721	:evaluator eval-ast
	722	:doc "
	723	")
	724
	725	(define ("show" "sh")
	726	:category :inspect
	727	:parser parse-show-command
	728	:evaluator eval-ast
	729	:doc "
	730	")
	731
	732	(define ("set")
	733	:category :switch
	734	:parser parse-set-command
	735	:evaluator eval-ast
	736	:doc "
	737	")
	738
	739	(define ("protect")
	740	:category :system
	741	:parser parse-protect-command
	742	:evaluator eval-ast
	743	:doc "
	744	")
	745
	746	(define ("unprotect")
	747	:category :system
	748	:parser parse-unprotect-command
	749	:evaluator eval-ast
	750	:doc "
	751	")
	752
	753	(define ("select")
	754	:category :proof
	755	:parser parse-show-command
	756	:evaluator eval-ast
	757	:doc "
	758	")
	759
	760	(define ("describe" "desc")
	761	:category :inspect
	762	:parser parse-show-command
	763	:evaluator eval-ast
	764	:doc "
	765	")
	766
	767	(define ("autoload")
	768	:category :library
	769	:parser parse-autoload-command
	770	:evaluator eval-ast
	771	:doc "
	772	")
	773
	774	(define ("provide")
	775	:category :library
	776	:parser parse-provide-command
	777	:evaluator eval-ast
	778	:doc "
	779	")
	780
	781	(define ("require")
	782	:category :library
	783	:parser parse-require-command
	784	:evaluator eval-ast
	785	:doc "
	786	")
	787
	788	(define ("pwd")
	789	:category :misc
	790	:parser parse-pwd-command
	791	:evaluator eval-ast
	792	:doc "
	793	")
	794
	795	(define ("cd")
	796	:category :misc
	797	:parser parse-cd-command
	798	:evaluator eval-ast
	799	:doc "
	800	")
	801
	802	(define ("pushd")
	803	:category :misc
	804	:parser parse-pushd-command
	805	:evaluator eval-ast
	806	:doc "
	807	")
	808
	809	(define ("popd")
	810	:category :misc
	811	:parser parse-popd-command
	812	:evaluator eval-ast
	813	:doc "
	814	")
	815
	816	(define ("dirs")
	817	:category :misc
	818	:parser parse-dirs-command
	819	:evaluator eval-ast
	820	:doc "
	821	")
	822
	823	(define ("ls")
	824	:category :misc
	825	:parser parse-ls-command
	826	:evaluator eval-ast
	827	:doc "
	828	")
	829
	830	(define ("")
	831	:category :misc
	832	:parser identity
	833	:evaluator cafeobj-eval-control-d
	834	:doc "
	835	")
	836
	837	(define ("cont" "continue")
	838	:category :rewrite
	839	:parser parse-continue-command
	840	:evaluator eval-ast
	841	:doc "
	842	")
	843
	844	(define ("look")
	845	:category :inspect
	846	:parser parse-look-up-command
	847	:evaluator eval-ast
	848	:doc "
	849	")
	850
	851	(define ("names" "name")
	852	:category :inspect
	853	:parser parse-name-command
	854	:evaluator eval-ast
	855	:doc "
	856	show
	857	")
	858
	859
	860	(define ("scase")
	861	:category :proof
	862	:parser parse-case-command
	863	:evaluator eval-ast
	864	:doc "
	865	")
	866
	867	(define ("sos" "passive")
	868	:category :proof
	869	:parser pignose-parse-sos
	870	:evaluator eval-ast
	871	:doc "
	872	")
	873
	874	(define ("db")
	875	:category :proof
	876	:parser pignose-parse-db
	877	:evaluator eval-ast
	878	:doc "
	879	")
	880
	881	(define ("clause")
	882	:category :proof
	883	:parser pignose-parse-clause
	884	:evaluator eval-ast
	885	:doc "
	886	")
	887
	888	(define ("list")
	889	:category :proof
	890	:parser pignose-parse-list-command
	891	:evaluator eval-ast
	892	:doc "
	893	")
	894
	895	(define ("flag")
	896	:category :proof
	897	:parser pignose-parse-flag
	898	:evaluator eval-ast
	899	:doc "
	900	")
	901
	902	(define ("param")
	903	:category :proof
	904	:parser pignose-parse-param
	905	:evaluator eval-ast
	906	:doc "
	907	")
	908
	909	(define ("option")
	910	:category :proof
	911	:parser pignose-parse-option
	912	:evaluator eval-ast
	913	:doc "
	914	")
	915
	916	(define ("resolve")
	917	:category :proof
	918	:parser pignose-parse-resolve
	919	:evaluator eval-ast
	920	:doc "
	921	")
	922
	923	(define ("demod")
	924	:category :proof
	925	:parser pignose-parse-demod
	926	:evaluator eval-ast
	927	:doc "
	928	")
	929
	930	(define ("save-option")
	931	:category :proof
	932	:parser pignose-parse-save-option
	933	:evaluator eval-ast
	934	:doc "
	935	")
	936
	937	(define ("sigmatch")
	938	:category :proof
	939	:parser pignose-parse-sigmatch
	940	:evaluator eval-ast
	941	:doc "
	942	")
	943
	944	(define ("lex")
	945	:category :proof
	946	:parser pignose-parse-lex
	947	:evaluator eval-ast
	948	:doc "
	949	")
	950
	951	(define (".")
	952	:category :misc
	953	:parser identity
	954	:evaluator cafeobj-nop
	955	:doc "
	956	")
	957
	958
	959	;;;
	960	) ; end eval-when
	961	;;; EOF

-644

~~cafeobj/creader-.lisp~~ less more

0		;;;-- Mode: Lisp; Syntax:CommonLisp; Package:CHAOS; Base:10 --
1		;;; $Id: creader.lisp,v 1.15 2010-08-09 00:43:37 sawada Exp $
2		(in-package :chaos)
3		#-:chaos-debug
4		(declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
5		#+:chaos-debug
6		(declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
7
8		#\|=============================================================================
9		System:CHAOS
10		Module: cafeobj
11		File: creader.lisp
12		==============================================================================\|#
13
14		;;;=============================================================================
15		;;; Schema based generalized reader based on OBJ3 implementation.
16		;;;=============================================================================
17
18		;;; TOP-LEVEL module parser invokes 'reader' with schemas for modules
19
20		(defun cafeobj-parse ()
21		(reader 'Top-form cafeobj-schemas))
22
23		;;; SCHEMA
24		;;; schema for top-level of CafeOBJ ===========================================
25
26		;;;=============================================================================
27		;;; CafeOBJ Schemas
28		;;;-----------------------------------------------------------------------------
29
30		(eval-when (eval compile load)
31
32		;;;-----------------------------------------------------------------------------
33		;;; SORT/SUBSORT DECLARATION
34		;;;-----------------------------------------------------------------------------
35
36		;;; VISIBLE SORTS
37
38		(defparameter SortDeclaration
39		' (\|[\| (:upto (< \|,\| \|]\|) :sorts)
40		:append (:seq-of (:one-of (<) (\|,\|))
41		(:upto (< \|,\| \|]\|) :sorts))
42		\|]\|))
43
44		;;; HIDDEN SORTS
45
46		(defparameter HSortDeclaration
47		'(*
48		(\|[\| (:upto (< \|,\| \|]\|) :sorts)
49		:append (:seq-of (:one-of (<) (\|,\|))
50		(:upto (< \|,\| \|]\|) :sorts))
51		\|]\|)
52		*))
53
54		(defparameter HRCSortDeclaration
55		'(*record :symbol (:optional (:! Supers))
56		\|{\|
57		(:optional (:! Sv-pairs))
58		\|}\|)
59		)
60
61		;;; BUILTIN SORT
62
63		(defparameter BSortDeclaration
64		'(bsort :symbol (:call (read))))
65
66		;;; BUILTIN HIDDEN SORT
67
68		(defparameter BHSortDeclaration
69		'(hbsort :symbol (:call (read))))
70
71		;;;-----------------------------------------------------------------------------
72		;;; OPERATOR DECLARATION
73		;;;-----------------------------------------------------------------------------
74
75		;;; GENERAL OPERATORs
76
77		(defparameter OperatorDeclaration
78		'((:+ op ops) (:seq-of :opname) \|:\| :sorts -> :sort
79		(:if-present
80		\|{\| (:many-of
81		((:+ assoc comm idem associative commutative idempotent))
82		(\|id:\| :chaos-item)
83		(\|identity:\| :chaos-item)
84		(\|idr:\| :chaos-item)
85		(\|identity-rules:\| :chaos-item)
86		((:pred general-read-numberp))
87		((:+ prec precedence \|prec:\| \|pecedence:\|) :int)
88		(\|(\| (:seq-of :int) \|)\|)
89		((:+ strat strategy \|strat:\| \|strategy:\|)
90		\|(\| (:seq-of :int) \|)\|)
91		((:+ l-assoc r-assoc left-associative right-associative))
92		((:+ constr constructor))
93		((:+ coherent beh-coherent))
94		(memo)
95		)
96		\|}\|
97		)))
98
99		;;; BEHAVIOURAL OPERATOR DECLARATION
100
101		(defparameter BOperatorDeclaration
102		'((:+ bop bops) (:seq-of :opname) \|:\| :sorts -> :sort
103		(:if-present
104		\|{\| (:many-of
105		((:+ assoc comm idem associative commutative idempotent))
106		(\|id:\| :chaos-item)
107		(\|identity:\| :chaos-item)
108		(\|idr:\| :chaos-item)
109		(\|identity-rules:\| :chaos-item)
110		((:pred general-read-numberp))
111		((:+ prec precedence \|prec:\| \|pecedence:\|) :int)
112		(\|(\| (:seq-of :int) \|)\|)
113		((:+ strat strategy \|strat:\| \|strategy:\|)
114		\|(\| (:seq-of :int) \|)\|)
115		((:+ l-assoc r-assoc left-associative right-associative))
116		((:+ constr constructor))
117		(memo)
118		)
119		\|}\|
120		)))
121
122		;;; PREDICATE -- short hand for bool-valued ops.
123
124		(defparameter PredicateDeclaration
125		'(pred (:seq-of :opname) \|:\|
126		(:upto (op ops bop bops \|[\| pred preds bpred bpreds hidden signature sig
127		axioms ax axiom imports dpred
128		\|{\| \|}\| \|.\| -- --> > class record eq rule rl ceq crule crl
129		bq bcq beq bceq brule brl bcrule bcrl trans trns btrans btrns
130		bctrans bctrns fax bfax
131		var vars parse ev evq lisp lispq let)
132		:sorts)
133		(:if-present
134		\|{\| (:many-of
135		((:+ assoc comm idem associative commutative idempotent))
136		(\|id:\| :chaos-item)
137		(\|identity:\| :chaos-item)
138		(\|idr:\| :chaos-item)
139		(\|identity-rules:\| :chaos-item)
140		;; ((:pred general-read-numberp))
141		((:+ prec precedence \|prec:\| \|pecedence:\|) :int)
142		(\|(\| (:seq-of :int) \|)\|)
143		((:+ strat strategy \|strat:\| \|strategy:\|)
144		\|(\| (:seq-of :int) \|)\|)
145		((:+ l-assoc r-assoc left-associative right-associative))
146		((:+ constr constructor))
147		((:+ coherent beh-coherent))
148		((:+ meta-demod demod))
149		(memo)
150		)
151		\|}\|
152		)))
153
154		(defparameter BPredicateDeclaration
155		'(bpred (:seq-of :opname) \|:\|
156		(:upto (op ops bop bops \|[\| pred preds bpred bpreds hidden signature sig
157		axioms ax axiom imports
158		\|{\| \|}\| \|.\| -- --> > class record eq rule rl ceq crule crl
159		bq bcq beq bceq brule brl bcrule bcrl trans trns btrans btrns
160		bctrans bctrns fax bfax
161		var vars parse ev evq lisp lispq let)
162		:sorts)
163		(:if-present
164		\|{\| (:many-of
165		((:+ assoc comm idem associative commutative idempotent))
166		(\|id:\| :chaos-item)
167		(\|identity:\| :chaos-item)
168		(\|idr:\| :chaos-item)
169		(\|identity-rules:\| :chaos-item)
170		;; ((:pred general-read-numberp))
171		((:+ prec precedence \|prec:\| \|pecedence:\|) :int)
172		(\|(\| (:seq-of :int) \|)\|)
173		((:+ strat strategy \|strat:\| \|strategy:\|)
174		\|(\| (:seq-of :int) \|)\|)
175		((:+ l-assoc r-assoc left-associative right-associative))
176		((:+ constr constructor))
177		((:+ coherent beh-coherent))
178		(memo)
179		((:+ demod meta-demod))
180		)
181		\|}\|
182		)))
183
184		;;; OPERATOR ATTRIBUTES
185		;;; Now almost obsolate.
186
187		(defparameter OperatorAttribute
188		'((:+ attr attrs) (:seq-of :opname)
189		\|{\|
190		(:many-of
191		((:+ assoc comm idem associative commutative idempotent))
192		(\|id:\| :chaos-item)
193		(\|identity:\| :chaos-item)
194		(\|idr:\| :chaos-item)
195		(\|identity-rules:\| :chaos-item)
196		;; ((:pred general-read-numberp))
197		((:+ prec precedence \|prec:\| \|pecedence:\|) :int)
198		(\|(\| (:seq-of :int) \|)\|)
199		((:+ strat strategy \|strat:\| \|strategy:\|) \|(\| (:seq-of :int) \|)\|)
200		((:+ l-assoc r-assoc))
201		;; ((:+ constr constructor))
202		(memo)
203		)
204		\|}\|))
205
206		;;;-----------------------------------------------------------------------------
207		;;; RECORD DECLARATION
208		;;; NOTE class is not part of CafeOBJ language.
209		;;;-----------------------------------------------------------------------------
210
211		(defparameter R-C-Declaration
212		'((:+ record class) :symbol (:optional (:! Supers)) \|{\|
213		(:optional (:! Sv-pairs))
214		\|}\|))
215
216		;;;-----------------------------------------------------------------------------
217		;;; LET
218		;;;-----------------------------------------------------------------------------
219
220		(defparameter LetDeclaration
221		'(let :symbol (:optional \|:\| :sort) = :term \|.\|))
222
223		;;;-----------------------------------------------------------------------------
224		;;; VARIABLE DECLARATION
225		;;;-----------------------------------------------------------------------------
226		(defparameter VarDeclaration
227		'(var :symbol \|:\| :sort))
228		(defparameter VarsDeclaration
229		'(vars :symbols \|:\| :sort))
230		(defparameter PVarDeclaration
231		'(pvar :symbol \|:\| :sort))
232		(defparameter PVarsDeclaration
233		'(pvars :symbols \|:\| :sort))
234
235		;;;-----------------------------------------------------------------------------
236		;;; MACRO
237		;;;-----------------------------------------------------------------------------
238		(defparameter MacroDeclaration
239		'(\|#define\| :term \|::=\| :term \|.\|))
240
241		;;;-----------------------------------------------------------------------------
242		;;; AXIOMS
243		;;;-----------------------------------------------------------------------------
244
245		;;; EQUATION
246
247		(defparameter EqDeclaration
248		'(eq (:optional \|[\| (:seq-of :symbol (:upto (\|]\| \|:\|)))) :term = :term \|.\|))
249		(defparameter BEqDeclaration
250		'((:+ beq bq) :term = :term \|.\|))
251		(defparameter CEQDeclaration
252		'((:+ ceq cq) :term = :term if :term \|.\|))
253		(defparameter BCEQDeclaration
254		'((:+ bceq bcq) :term = :term if :term \|.\|))
255		(defparameter FoplAXDeclaration
256		'((:+ fax bfax ax bax frm bfrm) :term \|.\|))
257		(defparameter FoplGoalDeclaration
258		'((:+ goal bgoal) :term \|.\|))
259
260		;;; STATE TRANSITION
261
262		(defparameter RlDeclaration
263		'((:+ rule rl trans trns) :term => :term \|.\|))
264		(defparameter BRLDeclaration
265		'((:+ brule brl btrans btrns) :term => :term \|.\|))
266		(defparameter CRLDeclaration
267		'((:+ crule crl ctrans ctrns) :term => :term if :term \|.\|))
268		(defparameter BCRLDeclaration
269		'((:+ bcrule brl bctrans bctrns) :term => :term if :term \|.\|))
270
271		;;;-----------------------------------------------------------------------------
272		;;; IMPORTATIONS
273		;;;-----------------------------------------------------------------------------
274
275		(defparameter ExDeclaration
276		'((:+ ex extending) \|(\| :modexp \|)\|))
277		(defparameter PrDeclaration
278		'((:+ pr protecting) \|(\| :modexp \|)\|))
279		(defparameter UsDeclaration
280		'((:+ us using) \|(\| :modexp \|)\|))
281		(defparameter IncDeclaration
282		'((:+ inc including) \|(\| :modexp \|)\|))
283
284		)
285
286		;;;-----------------------------------------------------------------------------
287		;;; THE SCHEME OF WHOLE ALLOWABLE INPUTS
288		;;;-----------------------------------------------------------------------------
289
290		(eval-when (eval load)
291		(setq cafeobj-schemas
292		'(
293		(Top-form
294		(:one-of
295		(;; MODULE : Its Constructs
296		;; --------------------------------------------------
297		(:+ mod module module* module! mod* mod!
298		\|sys:mod\| \|sys:mod*\| \|sys:mod!\|
299		\|sys:module\| \|sys:module*\| \|sys:module!\|
300		\|hwd:module!\| \|hwd:module*\| \|hwd:module\|
301		ots \|sys:ots\| \|hwd:ots\|
302		)
303		:symbol ; (:optional (:! Params))
304		(:if-present (:+ \( \[) (:! Param) :append (:seq-of \|,\| (:! Param))
305		(:+ \) \]))
306		(:if-present principal-sort :sort)
307		;; (:if-present psort :sort)
308		\|{\|
309		(:many-of
310
311		;; MODULE IMPORTATIONS
312		;; NOTE imports { ... } is not in MANUAL, and does not have
313		;; translater to Chaos now.
314		((:+ imports import)
315		\|{\|
316		(:many-of
317		#.ExDeclaration
318		#.PrDeclaration
319		#.UsDeclaration
320		#.IncDeclaration
321		((:+ --> **>) :comment)
322		((:+ -- **) :comment)
323		)
324		\|}\|)
325		#.ExDeclaration
326		#.PrDeclaration
327		#.UsDeclaration
328		#.IncDeclaration
329
330		;; SIGNATURE
331		((:+ sig signature) \|{\|
332		(:many-of
333		#.BSortDeclaration
334		#.BHSortDeclaration
335		#.HSortDeclaration
336		#.SortDeclaration
337		#.OperatorDeclaration
338		#.BOperatorDeclaration
339		#.PredicateDeclaration
340		#.BPredicateDeclaration
341		#.OperatorAttribute
342		#.R-C-Declaration
343		((:+ --> **>) :comment)
344		((:+ -- **) :comment)
345		)
346		\|}\|)
347
348		;; AXIOMS
349		((:+ axiom axioms axs) \|{\|
350		(:many-of
351		#.LetDeclaration
352		#.MacroDeclaration
353		#.VarDeclaration
354		#.VarsDeclaration
355		#.EqDeclaration
356		#.CeqDeclaration
357		#.RlDeclaration
358		#.CRlDeclaration
359		#.BeqDeclaration
360		#.BCeqDeclaration
361		#.BRLDeclaration
362		#.BCRLDeclaration
363		#.FoplAXDeclaration
364		#.FoplGoalDeclaration
365		((:+ --> **>) :comment)
366		((:+ -- **) :comment)
367		)
368		\|}\|)
369
370		;; Module elements without signature/axioms.
371		#.BSortDeclaration
372		#.BHSortDeclaration
373		#.SortDeclaration
374		#.HSortDeclaration
375		#.BHSortDeclaration
376		#.R-C-Declaration
377		#.OperatorDeclaration
378		#.BOperatorDeclaration
379		#.PredicateDeclaration
380		#.BPredicateDeclaration
381		#.OperatorAttribute
382		#.LetDeclaration
383		#.MacroDeclaration
384		#.VarDeclaration
385		#.VarsDeclaration
386		#.EqDeclaration
387		#.BEqDeclaration
388		#.CeqDeclaration
389		#.BCeqDeclaration
390		#.RlDeclaration
391		#.CRlDeclaration
392		#.BRlDeclaration
393		#.BCRLDeclaration
394		#.FoplAXDeclaration
395		#.FoplGoalDeclaration
396		((:+ --> **>) :comment)
397		((:+ -- **) :comment)
398
399		;; Misc elements.
400		(parse :term \|.\|)
401		((:+ ev lisp evq lispq) (:call (read)))
402		;; allow sole ".", and do nothing
403		(\|.\|)
404		)
405		\|}\|
406		) ; end module
407
408		;; VIEW DECLARATION
409		;; --------------------------------------------------
410		(view :symbol
411		:modexp
412		\|}\|)
413
414		;; MAKE
415		;; --------------------------------------------------
416		(make :symbol \|(\| :modexp \|)\|)
417
418		;; TOP LEVEL COMMANDS
419		;; --------------------------------------------------
420		((:+ reduce red execute exec exec! execute! breduce bred)
421		(:if-present in :modexp \|:\|) (:seq-of :term) \|.\|)
422		(tram (:+ compile execute exec red reduce reset)
423		(:if-present in :modexp \|:\|)
424		(:seq-of :term) \|.\|)
425		((:+ cbred)
426		(:if-present in :modexp \|:\|)
427		(:seq-of :term) \|.\|)
428		(version)
429		;;
430		(autoload :symbol :symbol)
431		;; (stop at :term \|.\|)
432		;; ((:+ rwt) limit :symbol)
433		(test (:+ reduction red execution exec) (:if-present in :modexp \|:\|)
434		(:seq-of :term)
435		(:+ \|:expect\| \|expect:\| expect) (:seq-of :term) \|.\|)
436		;; ((:+ match unify) (:seq-of :term) (:+ to :to) (:seq-of :term) \|.\|)
437		(match :term (:+ to with) :term \|.\|)
438		(unify :term (:+ to with) :term \|.\|)
439		;; (call-that :symbol)
440		;; ((:+ language lang) :symbol)
441		((:+ input in) :symbol)
442		(check (:seq-of :top-opname))
443		(regularize (:seq-of :top-opname))
444		(save :symbol)
445		(restore :symbol)
446		(prelude :symbol)
447		(save-system :symbol)
448		(protect (:seq-of :top-opname))
449		(unprotect (:seq-of :top-opname))
450		(clean memo)
451		(reset)
452		(full-reset)
453		(full reset)
454		((:+ --> **>) :comment)
455		((:+ -- **) :comment)
456		(parse (:if-present in :modexp \|:\|) (:seq-of :term) \|.\|)
457		((:+ lisp ev eval evq lispq)
458		(:call (read)))
459		(;; (:+ show sh set select describe desc) ; do
460		set
461		(:seq-of :top-opname))
462		;; (select :modexp :args)
463		((:+ show sh select describe desc) :args)
464		(trans-chaos (:seq-of :top-opname))
465
466		;; module elements which can appear at top(iff a module is opened.)
467
468		#.PrDeclaration
469		#.ExDeclaration
470		#.UsDeclaration
471		#.IncDeclaration
472		#.BSortDeclaration
473		#.BHSortDeclaration
474		#.HSortDeclaration
475		#.SortDeclaration
476		#.OperatorDeclaration
477		#.BOperatorDeclaration
478		#.PredicateDeclaration
479		#.BPredicateDeclaration
480		#.LetDeclaration
481		#.MacroDeclaration
482		#.VarDeclaration
483		#.VarsDeclaration
484		#.PVarDeclaration
485		#.PVarsDeclaration
486		#.EqDeclaration
487		#.CEqDeclaration
488		#.BEqDeclaration
489		#.BCEqDeclaration
490		#.RlDeclaration
491		#.CRlDeclaration
492		#.BRlDeclaration
493		#.BCRLDeclaration
494		#.FoplAXDeclaration
495		#.FoplGoalDeclaration
496		;; theorem proving stuff.
497		;; (open (:seq-of :top-opname))
498		(open :modexp \|.\|)
499		(close)
500		(start :term \|.\|)
501		;; trace/untrace
502		((:+ trace untrace) :symbol)
503		;; apply
504		(apply (:one-of-default
505		(:symbol (:upto
506		(within at)
507		(:optional with :symbol
508		= (:upto (\|,\| within at) :term)
509		:append
510		(:seq-of \|,\| :symbol
511		= (:upto (\|,\| within at) :term))))
512		(:+ within at)
513		(:one-of
514		((:+ top it term subterm))
515		((:+ \|(\| \|{\| \|[\|)
516		:unread
517		((:! Selector))
518		(:seq-of of ((:! Selector)))
519		\|.\|)))
520		(?)))
521		;;
522		(choose (:one-of
523		((:+ top term subterm))
524		((:+ \|(\| \|{\| \|[\|)
525		:unread
526		((:! Selector))
527		(:seq-of of ((:! Selector)))
528		\|.\|)))
529
530		(find (:+ rule -rule +rule rules -rules +rules))
531
532		;; RWL related commands
533		((:+ cont continue) :args)
534
535		;; PROVIDE/REQUIRE
536		(provide :symbol)
537		(require :top-term)
538		(autoload :symbol :symbol)
539
540		;; PigNose commands
541		#+:bigpink (db reset)
542		#+:bigpink ((:+ sos passive) (:+ = + -)
543		\|{\|
544		(:upto (\|,\| \|}\|) :sorts)
545		:append (:seq-of \|,\|
546		(:upto (\|}\| \|,\|) :sorts))
547		\|}\|)
548		#+:bigpink (list
549		(:+ axiom axioms
550		sos usable
551		flag param flags parameter parameters
552		option options passive
553		demod demodulator demodulators))
554		#+:bigpink (clause :term \|.\|)
555		#+:bigpink (option (:one-of (reset)
556		(= :symbol)))
557		#+:bigpink ((:+ save-option save-options) :symbol)
558		#+:bigpink (flag \|(\| :symbol \|,\| (:+ on off set clear) \|)\|)
559		#+:bigpink (param \|(\| :symbol \|,\| :int \|)\|)
560		#+:bigpink (resolve :args)
561		#+:bigpink (demod (:if-present in :modexp \|:\|) (:seq-of :term) \|.\|)
562		#+:bigpink (sigmatch \|(\| :modexp \|)\| (:+ to with) \|(\| :modexp \|)\|)
563
564		#+:bigpink (lex \|(\|
565		(:upto (\|,\| \|)\|) :opname)
566		:append (:seq-of \|,\|
567		(:upto (\|,\| \|)\|) :opname))
568		\|)\|)
569		;; misc toplevel commands
570		(eof)
571		#-CMU (#\^D)
572		#+CMU (#\)
573		(prompt (:seq-of :top-opname))
574		((:+ quit q \|:q\| \|:quit\|))
575		(cd :args)
576		(pushd :args)
577		(popd :args)
578		(dirs)
579		;; #-(or GCL LUCID CMU) (ls :symbol)
580		;; #+(or GCL LUCID CMU)
581		;; (ls :top-opname)
582		(ls :args)
583		(dribble :symbol)
584		(pwd)
585		(! :top-term) ; shell escape
586		(? :args) ; help/messege description
587		(?? :args) ; detailed help
588		(\|.\|)
589		(chaos :args)
590		)) ; end Top-Form
591
592		;; some separated definitions of non-terminals.
593		;; --------------------------------------------------
594		;; subterm specifier
595
596		(Selector
597		(:one-of
598		;; (term) (top) (subterm)
599		(\|{\| :int :append (:seq-of \|,\| :int) \|}\|)
600		(\|(\| (:seq-of :int) \|)\|)
601		(\[ :int (:optional \|..\| :int) \])))
602
603		;; parameter part
604		;; (Params (\[ (:! Param) :append (:seq-of \|,\| (:! Param)) \]))
605		(Param
606		(:one-of-default
607		(:symbols \|::\| (:upto (\|,\| \] \)) :modexp))
608		((:+ ex extending us using pr protecting inc including)
609		:symbols \|::\| (:upto (\|,\| \] \)) :modexp))))
610
611		;; importation modexp
612		#\|\|
613		(ImportModexp
614		(:symbol :modexp))
615		(IM (:one-of-default
616		(:modexp)
617		(\|::\| :modexp)))
618		\|\|#
619		;; (sortConst
620		;; (:one-of-default
621		;; (:sorts)
622		;; (:symbol = { :term \|:\| :sorts })))
623
624		;; super reference.
625		(Supers (\[ (:! Super) :append (:seq-of \|,\| (:! Super)) \]))
626		(Super ((:upto (\|,\| \]) :super)))
627		;; slot/value pairs
628		(SV-Pairs
629		((:! Sv-pair) :append (:seq-of (:! Sv-pair)) ;(:seq-of \|,\| (:! Sv-pair))
630		))
631		(Sv-Pair
632		(:one-of-default
633		(:symbol (:upto (\|}\|))
634		(:one-of (\|:\| :sort)
635		(= \|(\| :term \|)\| \|:\| :sort)))
636		((:+ -- **) :comment)
637		((:+ --> **>) :comment))
638		)
639		))
640		)
641
642
643		;;; EOF

+201

-0

cafeobj/declarations.lisp less more

	0	;;;-- Mode:LISP; Package:CHAOS; Base:10; Syntax:Common-lisp --
	1	#\|==============================================================================
	2	System: CHAOS
	3	Module: cafeobj
	4	File: declarations.lisp
	5	==============================================================================\|#
	6	(in-package :chaos)
	7	#-:chaos-debug
	8	(declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
	9	#+:chaos-debug
	10	(declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
	11
	12	;;; ----------------------------------------
	13	;;; register declarations keywords
	14	;;; ----------------------------------------
	15	(eval-when (:execute :load-toplevel)
	16	(clrhash cafeobj-declarations)
	17
	18	;;;
	19	;;; All the Declaration forms --------------------------------------------------------------
	20	;;;
	21
	22	(define ("bsort")
	23	:type :inner-module
	24	:category :signature
	25	:parser process-bsort-declaration
	26	:evaluator eval-ast)
	27
	28	(define ("[")
	29	:type :inner-module
	30	:category :signature
	31	:parser process-sort-and-subsort-form
	32	:evaluator eval-ast)
	33
	34	(define ("hidden" "*")
	35	:type :inner-module
	36	:category :signature
	37	:parser process-hidden-sort-form
	38	:evaluator eval-ast)
	39
	40	(define ("op")
	41	:type :inner-module
	42	:category :signature
	43	:parser process-operator-declaration-form
	44	:evaluator eval-ast)
	45
	46	(define ("ops")
	47	:type :inner-module
	48	:category :signature
	49	:parser process-operators-declaration-form
	50	:evaluator eval-ast)
	51
	52	(define ("bop")
	53	:type :inner-module
	54	:category :signature
	55	:parser process-operator-declaration-form
	56	:evaluator eval-ast)
	57
	58	(define ("bops")
	59	:type :inner-module
	60	:category :signature
	61	:parser process-boperators-declaration-form
	62	:evaluator eval-ast)
	63
	64	(define ("pred")
	65	:type :inner-module
	66	:category :signature
	67	:parser process-predicate-declaration-form
	68	:evaluator eval-ast)
	69
	70	(define ("dpred")
	71	:type :inner-module
	72	:category :signature
	73	:parser process-predicate-declaration-form
	74	:evaluator eval-ast)
	75
	76	(define ("bpred")
	77	:type :inner-module
	78	:category :signature
	79	:parser process-predicate-declaration-form
	80	:evaluator eval-ast)
	81
	82	(define ("dbpred")
	83	:type :inner-module
	84	:category :signature
	85	:parser process-predicate-declaration-form
	86	:evaluator eval-ast)
	87
	88	(define ("rec" "record")
	89	:type :inner-module
	90	:category :signature
	91	:parser process-record-declaration-form
	92	:evaluator eval-ast)
	93
	94	(define ("let")
	95	:type :inner-module
	96	:category :axiom
	97	:parser process-let-declaration-form
	98	:evaluator eval-ast)
	99
	100	(define ("#define")
	101	:type :inner-module
	102	:category :axiom
	103	:parser process-macro-declaration-form
	104	:evaluator eval-ast)
	105
	106	(define ("eq" "cq" "ceq" "rule" "rl" "crl" "crule" "trans" "ctrans" "trns" "ctrns"
	107	"beq" "bceq" "brule" "brl" "bcrule" "bcrl" "btrans" "btrns"
	108	"bctrans" "bctrns")
	109	:type :inner-module
	110	:category :axiom
	111	:parser process-axiom-form
	112	:evaluator eval-ast)
	113
	114	(define ("var" "vars")
	115	:type :inner-module
	116	:category :axiom
	117	:parser process-variable-declaration-form
	118	:evaluator eval-ast)
	119
	120	(define ("pvar" "pvars")
	121	:type :inner-module
	122	:category :axiom
	123	:parser process-pseud-variable-declaration-form
	124	:evaluator eval-ast)
	125
	126	(define ("fax" "bfax" "ax" "bax" "frm" "bfrm")
	127	:type :inner-module
	128	:category :axiom
	129	:parser pignose-process-fax-proc
	130	:evaluator eval-ast)
	131
	132	(define ("goal" "bgoal")
	133	:type :inner-module
	134	:category :axiom
	135	:parser pignose-process-goal-proc
	136	:evaluator eval-ast)
	137
	138	(define ("imports" "import")
	139	:type :inner-module
	140	:category :signature
	141	:parser parse-imports-form
	142	:evaluator eval-ast)
	143
	144	(define ("pr" "protecting" "ex" "extending" "us" "using" "inc" "including")
	145	:type :inner-module
	146	:category :import
	147	:parser process-importation-form
	148	:evaluator eval-ast)
	149
	150	(define ("--" "**")
	151	:type :inner-module
	152	:category :ignore
	153	:parser parse-decl-do-nothing
	154	:evaluator eval-decl-do-nothing)
	155
	156	(define ("-->")
	157	:type :inner-module
	158	:category :ignore
	159	:parser parse-dynamic-comment-1
	160	:evaluator eval-decl-do-nothing)
	161
	162	(define ("**>")
	163	:type :inner-module
	164	:category :ignore
	165	:parser parse-dynamic-comment-2
	166	:evaluator eval-decl-do-nothing)
	167
	168	(define ("ev" "lisp" "evq" "lispq")
	169	:type :inner-module
	170	:category :ignore
	171	:parser process-ev-lisp-form
	172	:evaluator eval-decl-do-nothing)
	173
	174	(define ("eval")
	175	:type :inner-module
	176	:category :misc
	177	:parser parse-eval-form
	178	:evaluator eval-ast)
	179
	180	(define ("sig" "signature")
	181	:type :inner-module
	182	:category :signature
	183	:parser process-signature
	184	:evaluator eval-ast)
	185
	186	(define ("axioms" "axiom" "axs")
	187	:type :inner-module
	188	:category :axiom
	189	:parser process-axioms-declaration
	190	:evaluator eval-ast)
	191
	192	(define (".") ; sole dots
	193	:type :inner-module
	194	:category :ignore
	195	:parser parse-decl-do-nothing
	196	:evaluator eval-decl-do-nothing)
	197
	198	;;;
	199	) ; end eval-when
	200	;;; EOF

-841

~~cafeobj/defcommand.lisp~~ less more

0		;;;-- Mode:LISP; Package:CHAOS; Base:10; Syntax:Common-lisp --
1		#\|==============================================================================
2		System: CHAOS
3		Module: cafeobj
4		File: defcommand.lisp
5		==============================================================================\|#
6		(in-package :chaos)
7		#-:chaos-debug
8		(declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
9		#+:chaos-debug
10		(declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
11
12		;;; ----------------------------------------
13		;;; register commands & declaration keywords
14		;;; ----------------------------------------
15		(eval-when (:execute :load-toplevel)
16
17		(clrhash cafeobj-commands)
18		(clrhash cafeobj-declarations)
19
20		;;;
21		;;; declarations/commands which can apper at top-level --------------------------------------
22		;;;
23
24		(defcom ("mod" "module" "module" "mod" "module!" "mod!" "sys:mod!" "sys:module!" "sys:mod" "sys:module")
25		"declares module.~%module <Name> [<Parameters>] [<PrincipalSort>] { <ModuleBody> }."
26		:toplevel-declaration
27		process-module-declaration-form
28		eval-ast)
29
30		(defcom ("view")
31		"declares view.~%view <Name> { <Map> ... }"
32		:topelevel-declaration
33		process-view-declaration-form
34		eval-ast)
35
36		(defcom ("check")
37		"check current module's various properties.~
38		~%check regularity : checks whether module's signagure is regular or not"
39		:checker
40		parse-check-command
41		eval-ast)
42
43		(defcom ("regularize")
44		"destructively makes current module's signature to be regular by adding sorts and operators."
45		:module
46		parse-regularize-command
47		eval-ast)
48
49		(defcom ("exec" "execute")
50		"exec [in <Modexpr> :] <Term> . ~%Rewrite <Term> by '(c)trans' axioms of the module."
51		:rewrite
52		parse-exec-command
53		eval-ast)
54
55		(defcom ("red" "reduce")
56		"reduce [in <Modexpr> :] <Term> . ~%Rewrite <Term> by axioms of the module."
57		:rewrite
58		parse-reduce-command
59		eval-ast)
60
61		(defcom ("exec!" "execute!")
62		"exec! [in <Modexpr> :] <Term> . "
63		:rewrite
64		parse-exec+-command
65		eval-ast)
66
67		(defcom ("bred" "breduce")
68		""
69		:rewrite
70		parse-bred-command
71		eval-ast)
72
73		(defcom ("version")
74		"prints version number of the system."
75		:misc
76		parse-version-command
77		princ)
78
79		(defcom ("cbred")
80		""
81		:rewrite
82		parse-cbred-command
83		eval-ast)
84
85		(defcom ("stop")
86		""
87		:rewrite
88		parse-stop-at
89		eval-ast)
90
91		(defcom ("parse")
92		""
93		:inspect
94		parse-parse-command
95		eval-ast)
96
97		(defcom ("match" "unify")
98		""
99		:inspect
100		parse-match-command
101		eval-ast)
102
103		(defcom ("lisp" "ev")
104		""
105		:system
106		parse-eval-lisp
107		cafeobj-eval-lisp-proc)
108
109		(defcom ("lispq" "evq")
110		""
111		:system
112		parse-eval-lisp
113		cafeobj-eval-lisp-q-proc)
114
115		;;; (defcom ("eval")
116		;;; ""
117		;;; :system
118		;;; parse-meta-eval
119		;;; eval-ast)
120
121		(defcom ("make")
122		""
123		:toplevel-decl
124		parse-make-command
125		eval-ast)
126
127		(defcom ("in" "input")
128		""
129		:io
130		parse-input-command
131		cafeobj-eval-input-proc)
132
133		(defcom ("save")
134		""
135		:io
136		parse-save-command
137		eval-ast)
138
139		(defcom ("restore")
140		""
141		:io
142		parse-restore-command
143		eval-ast)
144
145		(defcom ("reset")
146		""
147		:system-state
148		parse-reset-command
149		eval-ast)
150
151		(defcom ("full" "full-reset")
152		""
153		:system-state
154		parse-full-reset-command
155		eval-ast)
156
157		(defcom ("clean")
158		""
159		:rewrite
160		identity
161		cafeobj-eval-clear-memo-proc)
162
163		(defcom ("prelude")
164		""
165		:library
166		parse-prelude-command
167		cafeobj-eval-prelude-proc)
168
169		(defcom ("let")
170		""
171		:toplevel-declaration
172		process-let-declaration-form
173		eval-ast)
174
175		(defcom ("--" "**")
176		""
177		:toplevel-declaration
178		parse-comment-command
179		identity)
180
181		(defcom ("-->" "**>")
182		""
183		:toplevel-declaration
184		parse-comment-command
185		eval-ast)
186
187		(defcom ("imports")
188		""
189		:module-element
190		identity
191		cafeobj-eval-module-element-proc)
192
193		(defcom ("ex" "extending")
194		""
195		:module-element
196		identity
197		cafeobj-eval-module-element-proc)
198
199		(defcom ("pr" "protecting")
200		""
201		:module-element
202		identity
203		cafeobj-eval-module-element-proc)
204
205		(defcom ("us" "using")
206		""
207		:module-element
208		identity
209		cafeobj-eval-module-element-proc)
210
211		(defcom ("inc" "including")
212		""
213		:module-element
214		identity
215		cafeobj-eval-module-element-proc)
216
217		(defcom ("[")
218		""
219		:module-element
220		identity
221		cafeobj-eval-module-element-proc)
222
223		(defcom ("*")
224		""
225		:module-element
226		identity
227		cafeobj-eval-module-element-proc)
228
229		(defcom ("bsort")
230		""
231		:module-element
232		identity
233		cafeobj-eval-module-element-proc)
234
235		(defcom ("op" "ops")
236		""
237		:module-element
238		identity
239		cafeobj-eval-module-element-proc)
240
241		(defcom ("bop" "bops")
242		""
243		:module-element
244		identity
245		cafeobj-eval-module-element-proc)
246
247		(defcom ("pred")
248		""
249		:module-element
250		identity
251		cafeobj-eval-module-element-proc)
252
253		(defcom ("bpred")
254		""
255		:module-element
256		identity
257		cafeobj-eval-module-element-proc)
258
259		(defcom ("dpred") ; only for pignose
260		""
261		:module-element
262		identity
263		cafeobj-eval-module-element-proc)
264
265		(defcom ("dbpred") ; only for pignose
266		""
267		:module-element
268		identity
269		cafeobj-eval-module-element-proc)
270
271		(defcom ("sig" "signature")
272		""
273		:module-element
274		identity
275		cafeobj-eval-module-element-proc)
276
277		(defcom ("axiom" "ax")
278		""
279		:module-element
280		identity
281		cafeobj-eval-module-element-proc)
282
283		(defcom ("axioms" "axs")
284		""
285		:module-element
286		identity
287		cafeobj-eval-module-element-proc)
288
289		(defcom ("ax") ; pignose
290		""
291		:module-element
292		identity
293		cafeobj-eval-module-element-proc)
294
295		(defcom ("bax") ; pignose
296		""
297		:module-element
298		identity
299		cafeobj-eval-module-element-proc)
300
301		(defcom ("goal") ; pignose
302		""
303		:module-element
304		identity
305		cafeobj-eval-module-element-proc)
306
307		(defcom ("bgoal") ; pignose
308		""
309		:module-element
310		identity
311		cafeobj-eval-module-element-proc)
312
313		(defcom ("#define")
314		""
315		:module-element
316		identity
317		cafeobj-eval-module-element-proc)
318
319		(defcom ("var" "vars")
320		""
321		:module-element
322		identity
323		cafeobj-eval-module-element-proc)
324
325		(defcom ("pvar" "pvars")
326		""
327		:module-element
328		identity
329		cafeobj-eval-module-element-proc)
330
331		(defcom ("eq" "ceq" "cq")
332		""
333		:module-element
334		identity
335		cafeobj-eval-module-element-proc)
336
337		(defcom ("beq" "bceq" "bcq")
338		""
339		:module-element
340		identity
341		cafeobj-eval-module-element-proc)
342
343		(defcom ("trans" "ctrans")
344		""
345		:module-element
346		identity
347		cafeobj-eval-module-element-proc)
348
349		(defcom ("trns" "ctrns")
350		""
351		:module-element
352		identity
353		cafeobj-eval-module-element-proc)
354
355		(defcom ("rule" "crule")
356		""
357		:module-element
358		identity
359		cafeobj-eval-module-element-proc)
360
361		(defcom ("rl" "crl")
362		""
363		:module-element
364		identity
365		cafeobj-eval-module-element-proc)
366
367		(defcom ("btrans" "bctrans")
368		""
369		:module-element
370		identity
371		cafeobj-eval-module-element-proc)
372
373		(defcom ("brule" "bcrule")
374		""
375		:module-element
376		identity
377		cafeobj-eval-module-element-proc)
378
379		(defcom ("btrns" "bctrns")
380		""
381		:module-element
382		identity
383		cafeobj-eval-module-element-proc)
384
385		(defcom ("brl" "bcrl")
386		""
387		:module-element
388		identity
389		cafeobj-eval-module-element-proc)
390
391		(defcom ("open")
392		""
393		:proof
394		parse-open-command
395		eval-ast)
396
397		(defcom ("close")
398		""
399		:proof
400		parse-close-command
401		eval-ast)
402
403		(defcom ("start")
404		""
405		:proof
406		parse-start-command
407		eval-ast)
408
409		(defcom ("apply")
410		""
411		:proof
412		parse-apply-command
413		eval-ast)
414
415		(defcom ("choose")
416		""
417		:proof
418		parse-choose-command
419		eval-ast)
420
421		(defcom ("inspect")
422		""
423		:proof
424		parse-inspect-term-command
425		eval-ast)
426
427		(defcom ("find")
428		""
429		:proof
430		parse-find-command
431		eval-ast)
432
433		(defcom ("show" "sh")
434		""
435		:inspect
436		parse-show-command
437		eval-ast)
438
439		(defcom ("set")
440		""
441		:switch
442		parse-set-command
443		eval-ast)
444
445		(defcom ("protect")
446		""
447		:system-status
448		parse-protect-command
449		eval-ast)
450
451		(defcom ("unprotect")
452		""
453		:system-status
454		parse-unprotect-command
455		eval-ast)
456
457		(defcom ("select")
458		""
459		:proof
460		parse-show-command
461		eval-ast)
462
463		(defcom ("describe" "desc")
464		""
465		:inspect
466		parse-show-command
467		eval-ast)
468
469		(defcom ("autoload")
470		""
471		:library
472		parse-autoload-command
473		eval-ast)
474
475		(defcom ("provide")
476		""
477		:library
478		parse-provide-command
479		eval-ast)
480
481		(defcom ("require")
482		""
483		:library
484		parse-require-command
485		eval-ast)
486
487		(defcom ("??" "?")
488		""
489		:help
490		identity
491		cafeobj-top-level-help)
492
493		(defcom ("dribble")
494		""
495		:misc
496		parse-dribble-command
497		eval-ast)
498
499		(defcom ("pwd")
500		""
501		:misc
502		parse-pwd-command
503		eval-ast)
504
505		(defcom ("cd")
506		""
507		:misc
508		parse-cd-command
509		eval-ast)
510
511		(defcom ("pushd")
512		""
513		:misc
514		parse-pushd-command
515		eval-ast)
516
517		(defcom ("popd")
518		""
519		:misc
520		identity
521		parse-pushd-command)
522
523		(defcom ("dirs")
524		""
525		:misc
526		parse-dirs-command
527		eval-ast)
528
529		(defcom ("ls")
530		""
531		:misc
532		parse-ls-command
533		eval-ast)
534
535		(defcom ("!")
536		""
537		:misc
538		parse-shell-command
539		eval-ast)
540
541		(defcom ("")
542		""
543		:misc
544		identity
545		cafeobj-eval-control-d)
546
547		(defcom ("cont" "continue")
548		""
549		:rewrite
550		parse-continue-command
551		eval-ast)
552
553		(defcom ("look")
554		""
555		:inspect
556		parse-look-up-command
557		eval-ast)
558
559		(defcom ("names" "name")
560		""
561		:inspect
562		parse-name-command
563		eval-ast)
564
565		(defcom ("scase")
566		""
567		:proof
568		parse-case-command
569		eval-ast)
570
571		(defcom ("sos" "passive")
572		""
573		:proof
574		pignose-parse-sos
575		eval-ast)
576
577		(defcom ("db")
578		""
579		:proof
580		pignose-parse-db
581		eval-ast)
582
583		(defcom ("clause")
584		""
585		:proof
586		pignose-parse-clause
587		eval-ast)
588
589		(defcom ("list")
590		""
591		:proof
592		pignose-parse-list-command
593		eval-ast)
594
595		(defcom ("flag")
596		""
597		:proof
598		pignose-parse-flag
599		eval-ast)
600
601		(defcom ("param")
602		""
603		:proof
604		pignose-parse-param
605		eval-ast)
606
607		(defcom ("option")
608		""
609		:proof
610		pignose-parse-option
611		eval-ast)
612
613		(defcom ("resolve")
614		""
615		:proof
616		pignose-parse-resolve
617		eval-ast)
618
619		(defcom ("demod")
620		""
621		:proof
622		pignose-parse-demod
623		eval-ast)
624
625		(defcom ("save-option")
626		""
627		:proof
628		pignose-parse-save-option
629		eval-ast)
630
631		(defcom ("sigmatch")
632		""
633		:proof
634		pignose-parse-sigmatch
635		eval-ast)
636
637		(defcom ("lex")
638		""
639		:proof
640		pignose-parse-lex
641		eval-ast)
642
643		(defcom (".")
644		""
645		:misc
646		identity
647		cafeobj-nop)
648
649		;;;
650		;;; All the Declaration forms --------------------------------------------------------------
651		;;;
652
653		(defdecl ("bsort")
654		""
655		:sig
656		process-bsort-declaration
657		eval-ast)
658
659		(defdecl ("[")
660		""
661		:sig
662		process-sort-and-subsort-form
663		eval-ast)
664
665		(defdecl ("hidden" "*")
666		""
667		:sig
668		process-hidden-sort-form
669		eval-ast)
670
671		(defdecl ("op")
672		""
673		:sig
674		process-operator-declaration-form
675		eval-ast)
676
677		(defdecl ("ops")
678		""
679		:sig
680		process-operators-declaration-form
681		eval-ast)
682
683		(defdecl ("bop")
684		""
685		:sig process-operator-declaration-form
686		eval-ast)
687
688		(defdecl ("bops")
689		""
690		:sig
691		process-boperators-declaration-form
692		eval-ast)
693
694		(defdecl ("pred")
695		""
696		:sig
697		process-predicate-declaration-form
698		eval-ast)
699
700		(defdecl ("dpred")
701		""
702		:sig
703		process-predicate-declaration-form
704		eval-ast)
705
706		(defdecl ("bpred")
707		""
708		:sig
709		process-predicate-declaration-form
710		eval-ast)
711
712		(defdecl ("dbpred")
713		""
714		:sig
715		process-predicate-declaration-form
716		eval-ast)
717
718		;;;(defdecl ("opattr" "attr" "attrs")
719		;;; ""
720		;;; :sig
721		;;; process-opattr-declaration-form
722		;;; eval-ast)
723
724		(defdecl ("rec" "record")
725		""
726		:sig
727		process-record-declaration-form
728		eval-ast)
729
730		;;(defdecl ("cls" "class")
731		;; ""
732		;; :sig process-class-declaration-form
733		;; eval-ast)
734
735		(defdecl ("let")
736		""
737		:ax
738		process-let-declaration-form
739		eval-ast)
740
741		(defdecl ("#define")
742		""
743		:ax
744		process-macro-declaration-form
745		eval-ast)
746
747		(defdecl ("eq" "cq" "ceq" "rule" "rl" "crl" "crule" "trans" "ctrans" "trns" "ctrns"
748		"beq" "bceq" "brule" "brl" "bcrule" "bcrl" "btrans" "btrns"
749		"bctrans" "bctrns")
750		""
751		:ax
752		process-axiom-form
753		eval-ast)
754
755		(defdecl ("var" "vars")
756		""
757		:ax
758		process-variable-declaration-form
759		eval-ast)
760
761		(defdecl ("pvar" "pvars")
762		""
763		:ax
764		process-pseud-variable-declaration-form
765		eval-ast)
766
767		(defdecl ("fax" "bfax" "ax" "bax" "frm" "bfrm")
768		""
769		:ax
770		pignose-process-fax-proc
771		eval-ast)
772
773		(defdecl ("goal" "bgoal")
774		""
775		:ax
776		pignose-process-goal-proc
777		eval-ast)
778
779		(defdecl ("imports" "import")
780		""
781		:sig
782		parse-imports-form
783		eval-ast)
784
785		(defdecl ("pr" "protecting" "ex" "extending" "us" "using" "inc" "including")
786		""
787		:sig
788		process-importation-form
789		eval-ast)
790
791		(defdecl ("--" "**")
792		""
793		:ignore
794		parse-decl-do-nothing
795		eval-decl-do-nothing)
796
797		(defdecl ("-->")
798		""
799		:ignore
800		parse-dynamic-comment-1
801		eval-decl-do-nothing)
802
803		(defdecl ("**>")
804		""
805		:ignore
806		parse-dynamic-comment-2
807		eval-decl-do-nothing)
808
809		(defdecl ("ev" "lisp" "evq" "lispq")
810		""
811		:ignore
812		process-ev-lisp-form
813		eval-decl-do-nothing)
814
815		(defdecl ("eval")
816		""
817		:misc
818		parse-eval-form
819		eval-ast)
820
821		(defdecl ("sig" "signature")
822		""
823		:sig
824		process-signature
825		eval-ast)
826
827		(defdecl ("axioms" "axiom" "axs")
828		""
829		:ax
830		process-axioms-declaration
831		eval-ast)
832
833		(defdecl (".") ; sole dots
834		""
835		:ignore
836		parse-decl-do-nothing
837		eval-decl-do-nothing)
838
839
840		)

+199

-0

cafeobj/define.lisp less more

	0	;;;-- Mode:LISP; Package:CHAOS; Base:10; Syntax:Common-lisp --
	1	#\|==============================================================================
	2	System: CHAOS
	3	Module: cafeobj
	4	File: define.lisp
	5	==============================================================================\|#
	6	(in-package :chaos)
	7	#-:chaos-debug
	8	(declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
	9	#+:chaos-debug
	10	(declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
	11
	12
	13	;;; *****************************************************
	14	;;; On line document for commands, declarations or others
	15	;;; *****************************************************
	16
	17	(defvar cafeobj-doc-db (make-hash-table :test #'equal))
	18
	19	(defstruct (oldoc (:print-function print-online-document))
	20	(key "" :type string) ;
	21	(doc-string "" :type string) ; document string of commad/declaration
	22	(names nil :type list) ;
	23	)
	24
	25	(defun print-online-document (doc &optional (stream standard-output) &rest ignore)
	26	(declare (ignore ignore))
	27	(format stream "~%*** key : ~a" (oldoc-key doc))
	28	(format stream "~&doc-string : ~a" (oldoc-doc-string doc))
	29	(format stream "~&name : ~a" (oldoc-names doc)))
	30
	31	(defun get-document-string (key)
	32	(let ((doc (gethash key cafeobj-doc-db)))
	33	(if doc
	34	(oldoc-doc-string doc)
	35	nil)))
	36
	37	(defun show-doc-entries ()
	38	(let ((keys nil))
	39	(maphash #'(lambda (k v) (declare (ignore v)) (push k keys)) cafeobj-doc-db)
	40	(setq keys (sort keys #'string<=))
	41	(dolist (key keys)
	42	(let ((oldoc (get-document-string key)))
	43	(format t "~s" oldoc)))))
	44
	45	;;;
	46	;;; register-online-help : names doc
	47	;;;
	48
	49	(defun make-doc-key-from-string (str)
	50	(when (atom str)
	51	(setq str (list str)))
	52	(let ((keys nil))
	53	(dolist (s str)
	54	(let ((keyl (remove "" (parse-with-delimiter s #\space))))
	55	(push (reduce #'(lambda (x y) (concatenate 'string x y)) keyl) keys)))
	56	keys))
	57
	58	(defun register-online-help (names doc)
	59	(unless doc (return-from register-online-help nil))
	60	(cond ((stringp doc)
	61	(dolist (name names)
	62	(dolist (key (make-doc-key-from-string name))
	63	(setf (gethash key cafeobj-doc-db) (make-oldoc :key key
	64	:doc-string doc
	65	:names name)))))
	66	(t (dolist (a-doc doc)
	67	(let ((key-parts (butlast a-doc))
	68	(doc-string (car (last a-doc))))
	69	(dolist (keyp key-parts)
	70	(dolist (key (make-doc-key-from-string keyp))
	71	(setf (gethash key cafeobj-doc-db) (make-oldoc :key key
	72	:doc-string doc-string
	73	:names keyp)))))))))
	74
	75	(defparameter .md-special-chars.
	76	'((#\# #\null)
	77	(#\` #\')
	78	(#\~ #\null)))
	79
	80	(defun format-description (doc)
	81	(parallel-substitute .md-special-chars. doc))
	82	;;; ******
	83	;;; DEFINE : define command or declaration
	84	;;; ******
	85
	86	(defvar cafeobj-top-commands (make-hash-table :test #'equal))
	87	(defvar cafeobj-declarations (make-hash-table :test #'equal))
	88
	89	(defstruct (comde (:print-function print-comde))
	90	(key "" :type string) ; command/declaration keyword
	91	(type nil :type symbol) ; command or declaration
	92	(category nil :type symbol) ; kind of command/declaration
	93	(parser nil :type symbol) ; parser function
	94	(evaluator nil :type symbol) ; evaluator function
	95	)
	96
	97	(defparameter .valid-comde-types. '(:top :inner-module :doc-only))
	98	(defparameter .valid-decl-categories.
	99	'(:decl-toplevel ; toplevel declaration, such as 'module', 'view', e.t.c.
	100	; i.e., declarations which can apper at toplevel.
	101	:signature ; signature part of module body, such as 'op' '[', e.t.c
	102	:axiom ; axiom part of mdoule body, such as 'eq, ceq', e.t.c
	103	:ignore ; comments, dot (.), lisp, ev, e.t.c.
	104	:import ; import part of module body, such as 'protecting'
	105	:misc
	106	))
	107
	108	(defparameter .valid-com-categories.
	109	'(:decl-toplevel ; toplevel declaration, such as 'module', 'view', e.t.c.
	110	:checker ; check command
	111	:module ; apply some modifications to a module, such as regularize
	112	:rewrite ; commands related to rewriting, such as 'reduce', 'execute', e.t.c.
	113	:parse ; commands related to parsing terms, such as 'parse', e.t.c
	114	:inspect ; commands inspecting modules, terms, such as 'show', 'match', e.t.c
	115	:module-element ; declarations which can apper when a module is open.
	116	:proof ; commands related to proof stuff, such as 'open', 'apply, e.t.c.
	117	:switch ; 'set' commands
	118	:system ; various system related commands, such as 'protect', 'reset', e.t.c.
	119	:library ; library related commands, such as 'autoload', 'provide', e.t.c.
	120	:help ; '?', '??'
	121	:io ; 'input', 'save', e.t.c.
	122	:misc ;
	123	))
	124
	125	(defun print-comde (me &optional (stream standard-output) &rest ignore)
	126	(declare (ignore ignore))
	127	(format stream "~%** key : ~a" (comde-key me))
	128	(format stream "~% type : ~a" (comde-type me))
	129	(format stream "~% category : ~a" (comde-category me))
	130	(format stream "~% parser : ~a" (comde-parser me))
	131	(format stream "~% evaluator : ~a" (comde-evaluator me)))
	132
	133	;;;
	134	;;; get-command-info
	135	;;;
	136	(defun get-command-info (key)
	137	(gethash key cafeobj-top-commands))
	138
	139
	140	(defun show-top-entries ()
	141	(let ((keys nil))
	142	(maphash #'(lambda (k v) (declare (ignore v)) (push k keys)) cafeobj-top-commands)
	143	(setq keys (sort keys #'string<=))
	144	(dolist (key keys)
	145	(format t "~s" (get-command-info key)))))
	146
	147	;;;
	148	;;; get-decl-info
	149	;;;
	150	(defun get-decl-info (key)
	151	(gethash key cafeobj-declarations))
	152
	153	(defun show-decl-entries ()
	154	(let ((keys nil))
	155	(maphash #'(lambda (k v) (declare (ignore v)) (push k keys)) cafeobj-declarations)
	156	(setq keys (sort keys #'string<=))
	157	(dolist (key keys)
	158	(format t "~s" (get-decl-info key)))))
	159
	160	;;;
	161	;;; DEFINE
	162	;;;
	163	(defmacro define ((&rest keys) &key (type :top)
	164	(category :misc)
	165	(parser nil)
	166	(evaluator 'eval-ast)
	167	(doc nil))
	168	(case type
	169	(:top (unless (member category .valid-com-categories.)
	170	(error "Internal error, invalid category ~s" category)))
	171	(:inner-module (unless (member category .valid-decl-categories.)
	172	(error "Internal error, invalid category ~s" category)))
	173	(:doc-only)
	174	(:otherwise (error "Internal error, invalid type ~s" type)))
	175	(unless (eq type :doc-only)
	176	(unless (fboundp parser) (warn "no parser ~s" parser))
	177	(unless (fboundp evaluator) (warn "no evaluator ~s" evaluator)))
	178	;;
	179	`(progn
	180	(unless (eq ,type :doc-only)
	181	(let ((hash (if (or (eq ,type :top)
	182	(eq ,category :decl-toplevel))
	183	cafeobj-top-commands
	184	cafeobj-declarations)))
	185	(dolist (key ',keys)
	186	(setf (gethash key hash) (make-comde :key key
	187	:type ',type
	188	:category ',category
	189	:parser ',parser
	190	:evaluator ',evaluator)))))
	191	;; set online help
	192	(register-online-help ',keys ',doc)))
	193
	194	(defun print-comde-usage (com)
	195	(format t "~&[Usage] ~s, not yet" com))
	196
	197
	198	;;; EOF

-7

cafeobj/trans-decl.lisp less more

24	24	;;; parser were more well done, the translators would be no more needed, or
25	25	;;; would be more clean. This should be done in the near future.
26	26	;;; ****************************************************************************
27
28		(defvar cafeobj-declarations (make-hash-table :test #'equal))
29	27
30	28	;;; ***************
31	29	;;; INTERFACE FORM____________________________________________________________

769	767	(parse-module-element e)
770	768	(case kind
771	769	((:ignore :misc) nil)
772		(:sig (setq sig (nconc sig elt)))
773		(:ax (setq ax (nconc ax elt))))))
	770	(:signature (setq sig (nconc sig elt)))
	771	(:import (setq sig (nconc sig elt)))
	772	(:axiom (setq ax (nconc ax elt))))))
774	773	(setf body (append sig ax))
775	774	body))
776	775
777	776	(defun parse-module-element (e &rest ignore)
778	777	(declare (ignore ignore))
779		(let ((decl (gethash (car e) cafeobj-declarations)))
	778	(let ((decl (get-decl-info (car e))))
780	779	(unless decl
781	780	(with-output-chaos-error ('no-decl)
782	781	(format t "No such declaration '~a'" (car e))))
783		(let ((parser (decl-parser decl)))
	782	(let ((parser (comde-parser decl)))
784	783	(unless parser
785	784	(with-output-chaos-error ('no-parser)
786	785	(format t "No parser is defined for declaration ~a" (car e))))

788	787	(declare (list ast))
789	788	(when (and ast (atom (car ast)))
790	789	(setq ast (list ast)))
791		(values (decl-category decl) ast)))))
	790	(values (comde-category decl) ast)))))
792	791
793	792	(defun parse-module-element-1 (e &rest ignore)
794	793	(multiple-value-bind (type elt)

-2

chaos/tools/help.lisp less more

1	1	(in-package :chaos)
2	2	#\|==============================================================================
3	3	System: CHAOS
4		Module: chaos/tools
5		File: help.lisp
	4	Module: chaos/tools
	5	File: help.lisp
6	6	==============================================================================\|#
7	7	#-:chaos-debug
8	8	(declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))

-0

cl-ppcre less more

(New empty file)

-1

configure less more

1694	1694	VERSION=1.4
1695	1695	VMINOR=.13
1696	1696	VMEMO=PigNose0.99
1697		PATCHLEVEL=p7
	1697	PATCHLEVEL=p9
1698	1698
1699	1699
1700	1700

-1

configure.in less more

7	7	VERSION=1.4
8	8	VMINOR=.13
9	9	VMEMO=PigNose0.99
10		PATCHLEVEL=p7
	10	PATCHLEVEL=p9
11	11	AC_SUBST(PACKAGE)
12	12	AC_SUBST(VERSION)
13	13	AC_SUBST(VMINOR)

-0

make-cafeobj.lisp less more

191	191	;; (mk::operate-on-system :chaosx :compile)
192	192	(setq chaos::compile-builtin-axiom nil)
193	193	(load "sysdef.asd")
	194	(load "cl-ppcre/cl-ppcre.asd")
	195	(asdf:oos 'asdf:load-op :cl-ppcre)
194	196	(asdf:oos 'asdf:load-op 'chaosx)
195	197	(make-exec-image
196	198	(concatenate 'string chaos-root

-1

sysdef.asd less more

188	188	:serial t
189	189	:components ((:file "cafeobjvar")
190	190	(:file "creader")
	191	(:file "define")
191	192	(:file "trans-com")
192	193	(:file "trans-decl")
193	194	(:file "trans-form")
194	195	;; (:file "command-proc")
195	196	(:file "command-top")
196		(:file "defcommand")
	197	(:file "commands")
	198	(:file "declarations")
197	199	(:file "cafeobj-top")
198	200	))
199	201

-1

sysdef.cl less more

193	193	"cafeobj/cafeobjvar"
194	194	(:serial
195	195	"cafeobj/creader"
	196	"cafeobj/define"
196	197	"cafeobj/trans-com"
197	198	"cafeobj/trans-decl"
198	199	;; "cafeobj/command-proc"
199	200	"cafeobj/command-top"
200		"cafeobj/defcommand"
	201	"cafeobj/commands"
	202	"cafeobj/declarations"
201	203	"cafeobj/cafeobj-top")))
202	204
203	205	"acl-init"

-1

version.lisp less more

8	8	(eval-when (:execute :load-toplevel :compile-toplevel)
9	9	(setq cafeobj-version-major "1.4")
10	10	(setq cafeobj-version-memo (format nil "~a" "PigNose0.99"))
11		(setq patch-level (format nil "~a" "p7"))
	11	(setq patch-level (format nil "~a" "p9"))
12	12	(if (not (equal "" cafeobj-version-memo))
13	13	(if (not (equal "" patch-level))
14	14	(setq cafeobj-version-minor