Importing prolog predicates

We have just a couple of loose ends to tie up before finishing our program. Since we have used several external functions in our Typol rules (add, sub, mult, and neg), we must herald their origins using the import clause:

import function1(arg1,arg2), function2(arg1),... from program;

When importing a predicate, you must indicate the correct number of arguments, with either an underscore or type name indicating the type of each argument. For our arithmetic predicates, we write:

 
   import add(integer, integer, integer), 
          sub(integer, integer, integer), 
          mult(integer, integer, integer), 
          neg(integer,integer) from expfunc;

where we have chosen expfunc as a package name for functions found in a prolog file named expfunc.sp. Any predicate function imported from package must be named package$predicate and be defined in a file package.sp. The package name must begin with a lower case letter since it is a prolog predicate. Our file expfunc.sp contains the following definitions:

   expfunc$add(N, M, X)  :- X is N + M.
   expfunc$sum(N, M, X)  :- X is N - M.
   expfunc$mult(N, M, X) :- X is N * M.
   expfunc$neg(N, M)     :- M is 0 - N.
   expfunc$diff(N, M)    :- N ~= M.

We have now seen the minimum necessary for building a simple interpreter for Exp. The following program should be stored in the file:

contrib/Exp/semantics/interpreter/eval_exp.ty

program eval_exp is
    use Exp;
    import add(integer, integer, integer), 
           sub(integer, integer, integer), 
           mult(integer, integer, integer), 
           neg(integer,integer) from expfunc ;
 
    export |- EXP : integer N as eval_exp(EXP) = N ;

    judgement |- Exp : INTEGER ;

    
    |- integer N : integer N ;

    |- EXP1 : integer x1  &  
    |- EXP2 : integer x2  &  
    add(x1, x2, x)
    ---------------- 
    |- plus(EXP1, EXP2) : integer x ;

    |- EXP1 : integer x1  &  
    |- EXP2 : integer x2  &  
    sub(x1, x2, x)
    ---------------- 
    |- minus(EXP1, EXP2) : integer x ;

    |- EXP1 : integer x1  &  
    |- EXP2 : integer x2  &  
    mult(x1, x2, x)
    ---------------- 
    |- prod(EXP1, EXP2) : integer x ;

    |- EXP : integer x1  &  
    neg(x1, x)
    ---------------- 
    |- uminus(EXP) : integer x ;

    |- EXP1 : v
    ----------------
    |- exp_s[EXP1] : v ;

    |- EXP1 : v1  &  
    |- EXPS : v 
    ----------------
    |- exp_s[EXP1.EXPS] : v ;

end eval_exp ;