/* This is a literate program.

This section supports command line interaction with the user.  The user may create definitions, list them and delete or edit them.  It is also possible to define new operators.  A list of commands may be read from a file, and all current definitions may be saved to a file.

The 'let' command maps an atom to any expression.  The same atom may map to several expressions at the same time.  The current list of definitions is stored as a set of facts.  

It is important first to exclude names beginning with capital letters, as these are reserved for self-defining constants.  Also some operators are so fundamental, they may not be given definitions.  A definition is preprocessed, then failed to release bindings, otherwise some clutter is displayed.

 */ (let Exp) :- process_let(Exp),!,fail. /*

 */ process_let((Name->_)) :- var(Name),!,write('The left side of a definition must be an atom.'),nl. /*
 */ process_let((Name->_)) :- literal(Name),!,write('Upper case names are self-defining.'),nl. /*
 */ process_let((Name->_)) :- reserved(Name),!,write(Name),write(' is a reserved operator.'),nl. /*

 */ process_let((Name->Def)) :- atom(Name),preprocess(Def,Def1,[[]],_,(let Name->Def)),!,assert_once(define(Name,Def1)),
numbervars(Def,0,_),pretty(Def),nl,numbervars(Def1,0,_),pretty(Def1),nl. /*

There is no other valid form of 'let' command.

 */ process_let(Err) :- write('Error in ''let'' definition.'),nl,display_exp((let Err)),nl,fail. /*

If commands are read from a file, it is likely that duplicates will become stored, so 'assert_once' checks for an existing definition, differening perhaps only in its variable names. 

 */ assert_once(define(R,Def1)):- clause(define(R,Def2),true),isomorphic(Def1,Def2),!. /*
 */ assert_once(define(R,Def1)):- assert(define(R,Def1)),!. /*

Two definitions are isomorphic if their variable names in corresponding positions agree ...

 */ isomorphic(X,Y) :- heteromorphic(X,Y),!,fail. /*
 */ isomorphic(_,_) :- true. /*

 */ heteromorphic(X,Y) :- numbervars(X,0,_),numbervars(Y,0,_),X=Y,!,fail. /*
 */ heteromorphic(_,_) :- true. /*

The 'find' command simplifies an expression.  The result may be grounded, i.e., free of variables, or symbolic, i.e., containing free variables.  The results are translated back into input format, except syntactical variants are normalised, and the fully bracketed parse is shown.  There may be several solutions, generated by back-tracking.  They are currently displayed without user interaction.

 */ (? X) :- (find X). /* (? is a variant form of find)

 */ (find X) :- clear_decks,preprocess(X,X1,[[]],_,(find X)),simplify(X1,Exp),display_result(Exp),fail. /*
 */ (find _) :- true. /*

 */ clear_decks :- abolish(counter,2),abolish(unique,1),abolish(unique,2),
                   abolish(input_file,2),abolish(output_file,1),told,seen. /*

 */ display_result(_) :- !. /*
 */ display_result(null) :- !. /*
 */ display_result(X) :- display_exp(X),nl. /*

 */ display_exp(E) :- numbervars(E,0,_),pretty(E),fail. /*
 */ display_exp(_) :- !. /*

The seven 'Op <mode> Pr' commands establish Op as an operator with mode <mode> and precedence Pr.  Op may not be a reserved atom, and Pr must be positive.  As a rule Pr will be of the form prec(Op), where Op is an existing operator.  In case the same 'use' file is read twice, duplicate definitions are ignored.  Redefinitions are allowed, but flagged.  All symbols defined as operators are recorded, so that 'drop' can retract them.  Separate lists are kept of unary and binary operators.

 */ (Op fx Pr) :- !,def_unary(Op,fx,Pr). /*
 */ (Op fy Pr) :- !,def_unary(Op,fy,Pr). /*
 */ (Op xf Pr) :- !,def_unary(Op,xf,Pr). /*
 */ (Op yf Pr) :- !,def_unary(Op,yf,Pr). /*

 */ def_unary(Op,_,_) :- literal(Op),write('A literal can''t be an operator.'),nl. /*
 */ def_unary(Op,M,Pr) :- atom(Op),simplify(Pr,Pr1),integer(Pr1),Pr1>0,Pr1=<1200,!,def_unary2(Op,M,Pr1). /*
 */ def_unary(Op,_,_) :- atom(Op),!,write('Operator precedences must be in the range 1..1200.'),nl. /*
 */ def_unary(_,_,_) :- write('An operator must be an atom.'),nl. /*

 */ def_unary2(Op,M,Pr) :- current_op(Pr,M,Op),!,seeing(user),write('Done.'),nl. /*
 */ def_unary2(Op,_,_) :- reserved(Op),!,write(''''),display_exp(Op),write(''' is a reserved operator.'),nl. /*
 */ def_unary2(Op,M,Pr) :- clause(unary(Op,_,_),true),!,op(Pr,M,Op),write('The definition of '''),write(Op),
                           write(''' has been changed.'),nl,retract(unary(Op,_,_)),assert(unary(Op,M,Pr)). /*
 */ def_unary2(Op,M,Pr) :- !,op(Pr,M,Op),assert(unary(Op,M,Pr)),seeing(user),write('Done.'),nl. /*

 */ (Op xfx Pr) :- !,def_binary(Op,fx,Pr). /*
 */ (Op xfy Pr) :- !,def_binary(Op,fy,Pr). /*
 */ (Op xfy Pr) :- !,def_binary(Op,xf,Pr). /*

 */ def_binary(Op,_,_) :- literal(Op),write('A literal can''t be an operator.'),nl. /*
 */ def_binary(Op,M,Pr) :- atom(Op),simplify(Pr,Pr1),integer(Pr1),Pr1>0,Pr1=<1200,!,def_binary2(Op,M,Pr1). /*
 */ def_binary(Op,_,_) :- atom(Op),!,write('Operator precedences must be in the range 1..1200.'),nl. /*
 */ def_binary(_,_,_) :- write('An operator must be an atom.'),nl. /*


 */ def_binary2(Op,M,Pr) :- current_op(Pr,M,Op),!,seeing(user),write('Done.'),nl. /*
 */ def_binary2(Op,_,_) :- reserved(Op),!,write(''''),display_exp(Op),write(''' is a reserved operator.'),nl. /*
 */ def_binary2(Op,M,Pr) :- clause(binary(Op,_,_),true),!,op(Pr,M,Op),write('The definition of '''),write(Op),
                           write(''' has been changed.'),nl,retract(binary(Op,_,_)),assert(binary(Op,M,Pr)). /*
 */ def_binary2(Op,M,Pr) :- !,op(Pr,M,Op),assert(binary(Op,M,Pr)),seeing(user),write('Done.'),nl. /*

The command 'drop X.' removes all definitions of X.  The 'drop.' command removes all definitions of everything.  Both commands also remove any user created operator definitions of X.

 */ (drop Op) :- retract(unary(Op,M,_)),current_op(0,M,Op),fail. /*
 */ (drop Op) :- retract(binary(Op,M,_)),current_op(0,M,Op),fail. /*
 */ (drop N) :- retract(define(N,_)),fail. /*
 */ (drop _) :- true. /*

 */ drop :- retract(unary(Op,M,_)),current_op(0,M,Op),fail. /*
 */ drop :- retract(binary(Op,M,_)),current_op(0,M,Op),fail. /*
 */ drop :- abolish(define,2). /*

The command 'show X.' displays all current user definitions of X, including whether it is defined as an operator.  The variant 'show.' displays ALL operators and definitions.

 */ show :- !,show_unary(_),show_binary(_),show_defs(_). /*

 */ (show R) :- show_unary(R),show_binary(R),show_defs(R). /*

 */ show_defs(N) :- clause(define(N,E),true),show_def(N,E),fail. /*
 */ show_defs(_) :- true. /*

 */ show_def(N,E) :- write(N),write(' -> '),display_exp(E),write(' .'),nl. /*

 */ show_unary(Op) :- clause(unary(Op,M,Pr),true),write(Op),write(' '),write(M),write(' '),write(Pr),write(' .'),nl,!. /*
 */ show_unary(_) :- true. /*

 */ show_binary(Op) :- clause(binary(Op,M,Pr),true),write(Op),write(' '),write(M),write(' '),write(Pr),write(' .'),nl,!. /*
 */ show_binary(_) :- true. /*

The 'use' command is used to read a list of commands from a source file.  It saves and restores the current command source file, so that source files may contain nested 'use' commands.  Because atoms may be given many definitions, no attempt is made to remove existing ones in the manner of 'reconsult'.  However, the 'let' command will prevent the same definition from being made twice.

 */ (use Lib) :- !,seeing(Old),process_use(Lib,Old). /*

 */ process_use(Lib,Old) :- see(Lib),!,write('Reading '),write(Lib),write('...  '),nl,libra,seen,see(Old). /*
 */ process_use(Lib,Old) :- write(Lib),write(' can''t be seen.'),write(Lib),nl,see(Old). /*

 */ libra :- repeat,read(Term),process(Term). /*

 */ process(end_of_file) :- !. /*
 */ process((let Exp)) :- !,process_let(Exp),confirm,fail. /*
 */ process((Name->Exp)) :- !,process_let((Name->Exp)),confirm,fail. /*
 */ process(Command) :- seeing(In),call(Command),!,see(In),tell(user),confirm,fail. /*
 */ process(X) :- display_line(X),write('Isn''t a command.'),nl,!,fail. /*

 */ confirm :- seeing(user),!,write('Done'),nl. /*
 */ confirm :- true. /*

The 'reuse' command is equivalent to 'drop' followed by 'use'.

*/ (reuse Lib) :- drop,use(Lib). /*

The command 'dump X.' dumps the current definitions to a file.

 */ (dump File) :- telling(Old),tell(File),(show),told,tell(Old). /*

The command 'edit X' displays the definitions of X one at a time.  Each definition can then be retained or deleted.  (It can be replaced by a 'let' command.)  

 */ (edit R) :- edit_unary(R),edit_binary(R),edit_defs(R). /*

 */ edit_unary(X) :- clause(unary(X,_,_),true),show_unary(X),get_ans(A),retract_unary(A,X). /*
 */ edit_unary(_) :- true. /*

 */ edit_binary(X) :- clause(binary(X,_,_),true),show_binary(X),get_ans(A),retract_binary(A,X). /*
 */ edit_binary(_) :- true. /*

 */ edit_defs(R) :- clause(define(R,Exp),true),show_def(R,Exp),get_ans(A),retract_def(A,R,Exp),fail. /*
 */ edit_defs(_) :- true. /*

The user types '+' (or '=') to retain a definition, and '-' to delete it.  Any other reply prompts the same question.  Only the first character on the line is considered

 */ ask(R,Exp) :- get_ans(A),retract_define(A,R,Exp). /*
 
 */ get_ans(A) :- write('     Keep it (+) or drop it (-)? '),get(X),skipeol(X,_),test_ans(X,A). /*

 */ skipeol(31,31):- !. /*
 */ skipeol(_,Z)  :- get(Y),skipeol(Y,Z). /*

 */ test_ans(X,+) :- [X|[]]="+",!. /*
 */ test_ans(X,-) :- [X|[]]="-",!. /*
 */ test_ans(X,-) :- [X|[]]="=",!. /*
 */ test_ans(_,A) :- get_ans(A). /*

 */ retract_def(-,R,Exp) :- retract(define(R,Exp)). /* 
 */ retract_def(+,_,_) :- true. /* 

 */ retract_unary(-,X) :- retract(unary(X,_,_)). /* 
 */ retract_unary(+,_) :- true. /* 

 */ retract_binary(-,X) :- retract(binary(X,_,_)). /* 
 */ retract_binary(+,_) :- true. /* 

The 'commands.' command displays the purpose of each command.  The command 'help X.' gives more details about command X.

 */ commands :- 
write('The following commands may be typed:'),nl,nl,
write('  ''let Name->Exp.'' adds expression ''Exp'' to the definitions of ''Name''.'),nl,
write('  ''Op fx Pr.''      makes ''Op'' a non-associative prefix operator, precedence ''Pr''.'),nl,
write('  ''Op fy Pr.''      makes ''Op'' an associative prefix operator, precedence ''Pr''.'),nl,
write('  ''Op xf Pr.''      makes ''Op'' a non-associative postfix operator, precedence ''Pr''.'),nl,
write('  ''Op yf Pr.''      makes ''Op'' an associative postfix operator, precedence ''Pr''.'),nl,
write('  ''Op xfx Pr.''     makes ''Op'' a non-associative binary operator, precedence ''Pr''.'),nl,
write('  ''Op xfy Pr.''     makes ''Op'' a  right-associative binary operator, precedence ''Pr''.'),nl,
write('  ''Op yfx Pr.''     makes ''Op'' a left-associative binary operator, precedence ''Pr''.'),nl,
write('  ''show Name.''     displays the current definitions of ''Name''.'),nl,
write('  ''show.''          displays ALL current definitions.'),nl,
write('  ''find Exp.''      displays all the values of expression ''Exp''.'),nl,
write('  ''drop Name.''     deletes all definitions of ''Name''.'),nl,
write('  ''drop.''          deletes ALL current definitions.'),nl,
write('  ''edit Name.''     lets the user delete selected values of ''Name''.'),nl,
write('  ''use File.''      reads the program source file ''File''.'),nl,
write('  ''reuse File.''    is equivalent to ''drop'' followed by ''use File''.'),nl,
write('  ''dump File.''     writes ALL definitions to the file ''File''.'),nl,
write('  ''help Command.''  explains a command, where ''Command'' is:'),nl,
write('                   let, fx, fy, xf, yf, xfx, xfy, yfx, show, find, drop, '),nl,
write('                   edit, use, reuse, or dump.'),nl,nl. /*
            
 */ (help let) :- 
    write('''let Name -> Expression.'' adds ''Expression'' to the definitions of ''Name''.'),nl,
    write('Example: ''let swap -> {X,Y -> Y,X}.''.'),nl,nl,
    write('''Name'' must be an atom that does not start with a capital letter.'),nl,
    write('''Expression'' is typically a relation, but may be any expression.'),nl,
    write('The (Name,Expression) pair is added to the list of current definitions.'),nl,
    write('If ''Name'' is given more than one definition, it will be evaluated to each in turn.'),nl,
    write('Unwanted definitions can be removed using ''drop'' or ''edit''.'),nl,
    write('(The word ''let'' is optional.)'),nl,nl,!. /*            
 */ (help fx) :- 
    write('  ''Op fx Pr.'' makes ''Op'' a non-associative prefix operator, precedence ''Pr''.'),nl,
    write('Example: ''abs fx unary_prec(+).'' gives ''abs'' the same precedence as unary ''+''.'),nl,nl,help_op,!. /*
 */ (help fy) :- 
    write('  ''Op fy Pr.'' makes ''Op'' an associative prefix operator, precedence ''Pr''.'),nl,
    write('Example: ''abs fy unary_prec(+).'' gives ''not'' the same precedence as unary ''+''.'),nl,nlhelp_op,!. /*
 */ (help xf) :- 
    write('  ''Op xf Pr.'' makes ''Op'' a non-associative postfix operator, precedence ''Pr''.'),nl,
    write('Example: ''^@ xf unary_prec(+).'' gives ''^@'' the same precedence as unary ''+''.'),nl,nl,help_op,!. /*
 */ (help yf) :- 
    write('  ''Op yf Pr.'' makes ''Op'' an associative postfix operator, precedence ''Pr''.'),nl,
    write('Example: ''^@ yf unary_prec(+).'' gives ''^@'' the same precedence as unary ''+''.'),nl,nl,help_op,!. /*
 */ (help xfx) :- 
    write('  ''Op xfx Pr.'' makes ''Op'' a non-associative binary operator, precedence ''Pr''.'),nl,
    write('Example: ''rem xfx binary_prec(+).'' gives ''rem'' the precedence of binary ''+''.'),nl,nl,help_op. /*
 */ (help xfy) :- 
    write('  ''Op xfy Pr.'' makes ''Op'' a  right-associative binary operator, precedence ''Pr''.'),nl,
    write('Example: ''rem xfy binary_prec(+).'' gives ''rem'' the precedence of binary ''+''.'),nl,nl,help_op,!. /*
 */ (help yfx) :- 
    write('  ''Op yfx Pr.'' makes ''Op'' a left-associative binary operator, precedence ''Pr''.'),nl,
    write('Example: ''rem yfx binary_prec(+).'' gives ''rem'' the precedence of binary ''+''.'),nl,nl,help_op,!. /*
 */ (help show) :- 
    write('''show Name.'' displays the current definitions of ''Name''.'),nl,
    write('''show.'' displays ALL current definitions.'),nl,
    write('Example: ''show swap.''.'),nl,nl,
    write('''Definitions are created by ''fx'', etc., and ''let'' commands.'),nl,
    write('Any variables present in the definitions are replaced by ''A'', ''B'', ''C'' and so on.'),nl,
    write('Expressions are fully parenthesised to make operator precedences explicit.'),nl, 
    write('Unwanted definitions can be removed using ''drop'' or ''edit''.'),nl,nl,!. /*            
 */ (help ?) :- (help find). /*
 */ (help find) :- 
    write('''find Expression.'' evaluates ''Expression'' and displays all its values.'),nl,
    write('Example: ''find (1,2)!swap.''.'),nl,nl,
    write('If the expression has no grounded value, ''find'' will attempt to simplify it.'),nl,
    write('(The symbol ''?'' can be used as an alternative to ''find''.)'),nl,nl,!. /*            
 */ (help drop) :- 
    write('''drop Name.'' deletes all definitions and operator properties of ''Name''.'),nl,
    write('''drop.'' deletes ALL current definitions and operator properties.'),nl,
    write('Example: ''drop swap.''.'),nl,nl,
    write('''Definitions are created by ''fx'', etc., and ''let'' commands.'),nl,
    write('A ''drop'' command is also implied by the ''reuse'' command.'),nl,nl,!. /*
 */ (help edit) :- 
    write('''edit Name.'' lets the user delete selected values of ''Name'' interactively.'),nl,
    write('Example: ''edit swap.''.'),nl,nl,
    write('Each definition is displayed in turn.  The user types ''+'' to retain a definition, or'),nl,
    write('''-'' to delete one.  New definitions may be added using ''fx'', etc., or ''let''.'),nl,
    write('There is no command to edit the text of a definition, but source files can be'),nl,
    write('prepared with an editor, then read in with the ''use'' or ''reuse'' command.'),nl,nl,!. /*            
 */ (help use) :-            
    write('''use File.'' reads the file ''File'', which should comprise a list of commands.'),nl,
    write('Example: ''use matrices.''.'),nl,nl,
    write('Typically, the file will consist of a source program or part of a source program,'),nl,
    write('and consist of a series of ''fx'' etc., and ''let'' commands.'),nl,
    write('Consequently, the definitions they make are added to those already in existence.'),nl,
    write('Commands are executed as they are read, so ''fx'', etc. commands for a given'),nl,
    write('name must precede its first use as an operator.  A file may be made self-executing by'),nl,
    write('including one or more ''find'' commands at the end of it.'),nl,
    write('The file may itself contain ''let'' commands, allowing source files to be nested.'),
    nl,nl,!. /*
 */ (help reuse) :-            
    write('''reuse File.'' is equivalent to ''drop.'' followed by ''use File.''.'),nl,
    write('Example: ''reuse matrices.''.'),nl,nl,
    write('Its use is appropriate when loading the first or only file defining a program.'),nl,
    write('Subsequent or nested files should be loaded by the ''use'' command.'),nl,nl,!. /*
 */ (help dump) :-            
    write('''dump File.'' writes all definitions to the file ''File''.'),nl,
    write('Example: ''dump checkpoint.''.'),nl,nl,
    write('Any operator definitions are written first, followed by any ''let'''),nl,
    write('definitions.  The format is the same as for the ''show'' command.'),nl,
    write('A saved file can be restored by a ''use'' or ''reuse'' command.'),nl,nl,!. /*
 */ (help _) :- help. /*

 */ help_op :- 
    write('It is better to define operator precedences relative to existing ones using the'),nl,            
    write('''unary_prec'' and ''binary_prec'' functions, to ensure portability.'),nl,
    write('An operator definition can be removed by an ''edit'' or a ''drop'' command.'),nl,nl. /*            

'Simplify(X,Y)' simplifies X to Y recursively.  There may be more than one result.  'Simplify' has very incestuous relationships with 'construct', 'generate', 'filter' and 'built_in', which all call each other recursively.  A major worry is that there is an infinite recursion somewhere.  

'Built_in' incorporates the rules for all the operators that don't evaluate both their operands.  For the sake of completeness, it does all the built-in operators and functions.  In contrast 'construct', 'filter' and 'generate' know that their arguments have been simplified, and incorporate the knowledge about how to apply relational expressions.

The Simplify Predicate
======================
The first case of 'simplify' that must be tested is for a variable, otherwise it will falsely bind to any expression.

 */ simplify(X,X) :- var(X),!. /*

Before we can deal with compounds in general, we have to deal with some special cases that might be mistaken for ordinary relational application.  These cases cover basic structures and punctuation.

But before we deal with the special cases, we have to eliminate two very special cases.  Because a shift sequence could be mistaken for a more general set, the special notations for shift sequences and ranges are processed first, and caught.  

 */ simplify(({X..Y}),Z) :- !,simplify(X,X1),simplify(Y,Y1),integer(X1),integer(Y1),
                            findall(W,generate({X1..Y1},W),U),sort(U,Z). /*
 */ simplify([X..Y],Z) :- !,simplify(X,X1),simplify(Y,Y1),integer(X1),integer(Y1),
                          findall(W,generate([X1..Y1],W),U),sort(U,Z). /*

The next cases concern structures.  A set, represented in this implementation by an ordered list, is simplified by simplifying its terms.

 */ simplify([],[]) :- !. /*
 */ simplify([H|T],[H1|T1]) :- !,simplify(H,H1),simplify(T,T1). /*

We need to trap pairs, otherwise (X,Y) would be read as the application of ',' to (X,Y), i.e., ','(X,Y), leading to an infinite recursion.

 */ simplify((X,Y),(X1,Y1)) :- !,simplify(X,X1),simplify(Y,Y1). /*

The ':' operator also needs to be copied as is, rather than applied to its operands. 

 */ simplify((X:Y),(X1:Y1)) :- !,simplify(X,X1),simplify(Y,Y1). /*

Predefined & User-Defined Relations
===================================
Just about any name can be overloaded by the user.  If the name is defined as an operator, it will look like a relational application.  For example, 1+2 is indistinguishable from +(1,2), and should be treated just like (1,2)!(+).  There may be multiple results, as in @{0;2}+@{0;1}, which yields 0,1,2,3 in turn.

 */ simplify(X,Z) :- compound(X),!,X=..[R|L],simplify_compound(L,R,Z). /*

We need to be cautious about simplifying a compound term.  First, we may have a literal rather than a name.  At the moment, literals serve no particular purpose, so they are copied.  (Perhaps they could serve some future purpose in 'typed' pattern matching.)    

 */ simplify_compound(L,R,Z) :- literal(R),!,simplify(L,L1),Z=..[R|L1]. /* 

If its functor isn't user-defined, we don't want to simplify its arguments, because the built-in operators often don't evaluate their operands in the usual way.  The definition of the functor is then applied to the arguments.  There is no 'cut', because a user definition overloads but doesn't replace a built-in one.

 */ simplify_compound(L,R,Z) :- look_up(R,Def),list_to_tuple(L,X),simplify(X,Y),construct(Y,Def,Z). /* 

Finally, if the functor is a predefined relation, we call the 'built_in' predicate.

 */ simplify_compound(L,R,Z) :- predefined(R),list_to_tuple(L,X),built_in(R,X,Z). /*
  
Odd Cases
=========
There are two kinds of atoms.  Those that begin with capital letters are literals.  All others should be defined as expressions to be substituted.  However, in the event that the atom is predefined, it is copied; otherwise built-in relations could not be passed as arguments.

 */ simplify(X,Y) :- atom(X),!,simplify_atom(X,Y). /*

 */ simplify_atom(X,Y) :- literal(X),!,X=Y. /*
 */ simplify_atom(X,Y) :- look_up(X,Def),!,simplify(Def,Y). /*
 */ simplify_atom(X,X) :- predefined(X),!. /*

Integers are definitely grounded, and have one value.

 */ simplify(X,Y) :- integer(X),!,X=Y. /*


Utilities
=========
The 'list_to_tuple' predicate converts a list to a tuple.

 */ list_to_tuple([H],H) :- var(H),!. /*
 */ list_to_tuple([X,Y|T],(X,T1)) :- !,list_to_tuple([Y|T],T1). /*
 */ list_to_tuple([H],H) :- true. /*

Its inverse is 'tuple_to_list'.

 */ tuple_to_list(T,[T]) :- var(T),!. /*
 */ tuple_to_list((H,T),[H|T1]) :- !,tuple_to_list(T,T1). /*
 */ tuple_to_list(T,[T]) :- true. /*

'Seq_to_list' converts a sequence of characters to a Prolog list.

 */ seq_to_list([],[]) :- true. /*
 */ seq_to_list([(_,H)|T],[H|T1]) :- seq_to_list(T,T1). /*

The call 'list_to_seq(1,L,S)' converts list L to sequence S.  

 */ list_to_seq(_,[],[]) :- !. /*
 */ list_to_seq(N,[X|T],[(N,X)|T1]) :- N1 is N+1,list_to_seq(N1,T,T1). /*

The 'look_up' utility predicate copies the definitions of a name created by a 'let' statement.

 */ look_up(X,_) :- undefined_atom(X),!,write(''''),write(X),
                    write(''' is neither built-in nor defined by ''let''.'),nl,fail. /*
 */ look_up(Name,Def) :- atom(Name),clause(define(Name,Def),true),!. /*

An atom is undefined unless it is predefined (built-in) or previously defined by at least one 'let' statement:

 */ undefined_atom(X) :- predefined(X),!,fail. /*
 */ undefined_atom(X) :- atom(X),clause(define(X,_),true),!,fail. /*
 */ undefined_atom(X) :- atom(X). /*

The predicate 'symbolic' is true if an expression contains at least one free variable.

 */ symbolic(X) :- var(X),!. /*
 */ symbolic([H|_]) :- symbolic(H),!. /*
 */ symbolic([_|T]) :- !,symbolic(T). /*
 */ symbolic(X) :- compound(X),!,X=..[_|Args],symbolic(Args). /*

The predicate 'grounded' is true if an expression contains no free variables.  

 */ grounded(X) :- symbolic(X),!,fail. /*
 */ grounded(_) :- true. /*

Pretty Printing
===============
The pretty printer is used by 'find', 'show' and 'edit'.  Before calling 'pretty', a call is made to 'numbervars', to replace variables by terms of the form "'$VAR'(X)".  Write will display these terms as variable names, A-Z, A1-Z1, and so on.  It is therefore a bug if 'pretty' is asked to process a variable.

 */ pretty(X)          :- var(X),!,write('Bug: Unbound variable in ''pretty'''),nl. /*
 */ pretty('$VAR'(X))  :- !,write('$VAR'(X)). /*

The special set and list notations don't need unusual attention, but have to be caught in case they are confused with other lists.

 */ pretty({X..Y})     :- !,write('{'),pretty(X),write('..'),pretty(Y),write('}'). /*
 */ pretty([X..Y])     :- !,write('['),pretty(X),write('..'),pretty(Y),write(']'). /*

An empty list could be either the empty set or the empty sequence - both being exactly the same thing.  We opt for displaying an empty set.

 */ pretty([])         :- !,write('{}'). /*

A list represents a set, but the set may be a sequence.  If it is, it should be displayed appropriately.

 */ pretty([H|T])      :- is_ascii_str([H|T],1),!,write('"'),pretty_ascii([H|T]),write('"'). /*
 */ pretty([H|T])      :- is_seq([H|T],1),!,write('['),pretty_seq([H|T]),write(']'). /*
 */ pretty([H|T])      :- !,write('{'),pretty_set([H|T]),write('}'). /*

The predicate 'is_ascii_str(S,N)' is true iff S is the tail of a string of ASCII characters starting at its Nth position.

 */ is_ascii_str([],_). /*
 */ is_ascii_str([(H,C)|T],N) :- !,integer(H),ascii(C),H=N,N1 is N+1,is_ascii_str(T,N1). /*

The predicate 'ascii(C)' is true iff C is a printable ASCII character.

 */ ascii(C) :- integer(C),C>=32,C<127. /*

The predicate 'pretty_ascii(S)' writes S as a string of ASCII characters.

 */ pretty_ascii([(_,H)|[]]) :- !,put(H). /*
 */ pretty_ascii([(_,H)|T]) :- put(H),pretty_ascii(T). /*

The predicate 'pretty_seq' writes a non-empty list of terms separated by commas.  The last or only term must not be followed by a comma.  The left of each pair is its ordinal position, and is not written. 

 */ pretty_seq([(_,H)|[]]) :- !,pretty(H). /*
 */ pretty_seq([(_,H)|T]) :- pretty(H),write(', '),pretty_seq(T). /*

The predicate 'pretty_set' writes a non-empty list of members separated by semicolons.  The last or only member must not be followed by a seicolon. 

 */ pretty_set([H|[]]) :- !,pretty(H). /*
 */ pretty_set([H|T]) :- pretty(H),write(';'),pretty_set(T). /*

Pairs and tuples are not really a special case, but they look better without spaces.

 */ pretty((X,Y)) :- !,write('('),pretty(X),write(','),pretty(Y),write(')'). /*

Self-defining terms should be shown enclosed in single quotes, as they were originally written.
 
 */ pretty(X) :- literal(X),!,write(''''),write(X),write(''''). /*

The predicate 'literal' succeeds if the first character of an atom is a capital letter.

 */ literal(X) :- atom(X),name(X,[H|_]),H>="A",H=<"Z",!. /*

Other atoms and integers don't want quotes around them.

 */ pretty(X) :- atomic(X),!,write(X). /*

A compound expression needs treating carefully, as most functors will prove to be operators.  If the functor is not an operator, it is written in the usual functional format.

 */ pretty(X) :- compound(X),!,X =..[F|A],pretty_functor(F,A). /*

 */ pretty_functor(F,A) :- current_op(_,M,F),!,pretty_op(M,F,A). /*
 */ pretty_functor(F,A) :- literal(F),!,
             write(''''),write(F),write('''('),pretty_list(A),write(')'). /*
 */ pretty_functor(F,A) :- write(F),write('('),pretty_list(A),write(')'). /*

 */ pretty_list([H|[]]) :- !,pretty(H). /*
 */ pretty_list([H|T]) :- pretty(H),write(','),pretty_list(T). /*

Unary operators must be written in prefix or postfix form according to their declarations.

 */ pretty_op(fx,F,[A|[]]) :- !,write('('),write(F),write(' '),pretty(A),write(')'). /*
 */ pretty_op(fy,F,[A|[]]) :- !,write('('),write(F),write(' '),pretty(A),write(')'). /*
 */ pretty_op(xf,F,[A|[]]) :- !,write('('),pretty(A),write(' '),write(F),write(')'). /*
 */ pretty_op(yf,F,[A|[]]) :- !,write('('),pretty(A),write(' '),write(F),write(')'). /*

Binary operators are written in infix form.

 */ pretty_op(_,F,[X,Y|[]]):- !,write('('),pretty(X),write(' '),write(F),write(' '),pretty(Y),write(')'). /*

Nothing should reach this point.

 */ pretty(X) :- write('Bug: '),write(pretty(X)),nl. /*

End of literate program. */
