https://github.com/theoremprover-museum/CLIN
Raw File
Tip revision: e7082fbde3634286f458d64846699ae488fe18f3 authored by Michael Kohlhase on 22 December 2016, 09:28:55 UTC
initial commit, thanks to David Plaisted
Tip revision: e7082fb
Eclipse
%%%
%%% Specific code for Eclipse Prolog.
%%%

%%%
%%% Set compiler for optimized compile.
%%%
:- nodbgcomp.

%%%
%%% Load Quintus Prolog compatibility library.
%%%
:- use_module(library(quintus)).

%%%
%%% Force compile of lists.pl
%%%
:- append([1],[2],_).

%%%
%%% Handle user interrupt signal (SIGINT -- 2).
%%%
user_interrupt_signal :-
   set_interrupt_handler(2,true/0),
   update_sentC,  
   \+ unit_simp_subs_hk_1,
   assert_tryresult('user_interrupt'),
   not(not(summary)),
   reset_by_horn_set,
   not(not(postproc)),
   !,
   halt.
user_interrupt_signal :-
   halt.
:- set_interrupt_handler(2,user_interrupt_signal/0).

%%%
%%% Handle user kill signal (SIGTERM -- 15).
%%%
user_kill_signal :-
   set_interrupt_handler(15,true/0),
   update_sentC,  
   \+ unit_simp_subs_hk_1,
   assert_tryresult('user_kill'),
   not(not(summary)),
   reset_by_horn_set,
   not(not(postproc)),
   !,
   halt.
user_kill_signal :-
   halt.
:- set_interrupt_handler(15,user_kill_signal/0).

%%%
%%% Handle time overflow signal (SIGXCPU -- 24).
%%%
time_overflow_signal :-
   set_interrupt_handler(24,true/0),
   update_sentC,  
   \+ unit_simp_subs_hk_1,
   assert_tryresult('time_overflow'),
   not(not(summary)),
   reset_by_horn_set,
   !,
   not(not(postproc)),
   halt.
time_overflow_signal :-
   halt.
:- set_interrupt_handler(24,time_overflow_signal/0).

%%%
%%% nl/0
%%%
nl :-
  call_explicit(nl,sepia_kernel),
  flush(1).

%%%
%%% Code to allow database references for clauses.  Doesn't handle module
%%% specification, ie. mod:clause.  Also, type checking is not performed.
%%%
abolish([]) :- !.
abolish([Pred|PredList]) :-
        abolish(Pred),
        !,
        abolish(PredList).
abolish(Name/Arity) :-
        call_explicit(abolish(Name/Arity),quintus),
        concat_atom([Name,'_ref$'],Name_ref),
        Arity_ref is Arity+1,
        call_explicit(abolish(Name_ref/Arity_ref),quintus),
        functor(Key,Name,Arity),
        erase_all(Key).
abolish(Name,Arity) :-
        abolish(Name/Arity).
assert(Clause) :- assert(Clause,_).
assert((Head :- Body),Ref) :-
        !,
        'make_db_key$'(Head,Key),
        recorda(Key,(Head :- Body),Ref),
        'assert_clause$'((Head :- Body),Ref).
assert(Fact,Ref) :-
        'make_db_key$'(Fact,Key),
        recorda(Key,(Fact :- true),Ref),
        'assert_clause$'(Fact,Ref).
asserta(Clause) :- asserta(Clause,_).
asserta((Head :- Body),Ref) :-
        !,
        'make_db_key$'(Head,Key),
        recorda(Key,(Head :- Body),Ref),
        'asserta_clause$'((Head :- Body),Ref).
asserta(Fact,Ref) :-
        'make_db_key$'(Fact,Key),
        recorda(Key,(Fact :- true),Ref),
        'asserta_clause$'(Fact,Ref).
assertz(Clause) :- assertz(Clause,_).
assertz((Head :- Body),Ref) :-
        !,
        'make_db_key$'(Head,Key),
        recordz(Key,(Head :- Body),Ref),
        'assert_clause$'((Head :- Body),Ref).
assertz(Fact,Ref) :-
        'make_db_key$'(Fact,Key),
        recordz(Key,(Fact :- true),Ref),
        'assert_clause$'(Fact,Ref).
'assert_clause$'(Clause,Ref) :-
        Clause =.. [Predicate|Args],
        concat_atom([Predicate,'_ref$'],Predicate_ref),
        Clause_ref =.. [Predicate_ref|[Ref|Args]],
        call_explicit(assert(Clause_ref),sepia_kernel),
        functor(Clause,_,Arity),
        functor(Clause1,Predicate,Arity),
        Clause1 =.. [_|Args1],
        Clause2 =.. [Predicate_ref|[_|Args1]],
        'assert_clause$1'(Clause1,Clause2).
'assert_clause$1'(Clause1,Clause2) :-
        call_explicit(clause((Clause1 :- Clause2)),sepia_kernel),
        !.
'assert_clause$1'(Clause1,Clause2) :-
        call_explicit(assert((Clause1 :- Clause2)),sepia_kernel).
'asserta_clause$'(Clause,Ref) :-
        Clause =.. [Predicate|Args],
        concat_atom([Predicate,'_ref$'],Predicate_ref),
        Clause_ref =.. [Predicate_ref|[Ref|Args]],
        call_explicit(asserta(Clause_ref),sepia_kernel),
        functor(Clause,_,Arity),
        functor(Clause1,Predicate,Arity),
        Clause1 =.. [_|Args1],
        Clause2 =.. [Predicate_ref|[_|Args1]],
        'assert_clause$1'(Clause1,Clause2).
clause(Head,Body) :-
        'make_db_key$'(Head,Key),
        recorded(Key,(Head :- Body),_).
clause(Head,Body,Ref) :-
        nonvar(Ref),
        !,
        instance(Ref,(Head :- Body)).
clause(Head,Body,Ref) :-
        nonvar(Head),
        !,
        'make_db_key$'(Head,Key),
        recorded(Key,(Head :- Body),Ref).
clause(_,_,_) :-
        write('clause/3 type error'),
        nl,
        abort.
erase(Ref) :-
        instance(Ref,(Fact :- true)),
        !,
        Fact =.. [Predicate|Args],
        concat_atom([Predicate,'_ref$'],Predicate_ref),
        Fact_ref =.. [Predicate_ref|[Ref|Args]],
        once(call_explicit(retract(Fact_ref),sepia_kernel)),
        call_explicit(erase(Ref),quintus).
erase(Ref) :-
        instance(Ref,Clause),
        Clause =.. [Predicate|Args],
        concat_atom([Predicate,'_ref$'],Predicate_ref),
        Clause_ref =.. [Predicate_ref|[Ref|Args]],
        once(call_explicit(retract(Clause_ref),sepia_kernel)),
        call_explicit(erase(Ref),quintus).
'make_db_key$'(Term,Key) :-
        functor(Term,Name,Arity),
        functor(Key,Name,Arity).
recorded(Key,Term,Ref) :-
        nonvar(Ref),
        !,
        'recorded$1'(Key,Term,Ref).
recorded(Key,Term,Ref) :-
        call_explicit(recorded(Key,Term,Ref),quintus).
'recorded$1'(Key,Term,Ref) :-
        current_record(Key),
        call_explicit(recorded(Key,Term,Ref),quintus),
        !.
retract((Head :- Body)) :-
        !,
        clause(Head,Body,Ref),
        erase(Ref).
retract(Fact) :-
        clause(Fact,true,Ref),
        erase(Ref).
retractall(Head) :-
        clause(Head,_,Ref),
        erase(Ref),
        fail.
retractall(_).
        
%%%
%%% Simply fail unknown predicates.
%%%
:- unknown(_,fail).

%%%
%%% Quintus_banner/0.
%%%
quintus_banner :-
  clin_version(Version),
  nl, tab(15),write('WELCOME TO CLIN '),
  write(Version),nl,
  write('(c) 1990 by Shie-Jue Lee and David Plaisted'),
  nl,nl,nl,
  !.

%%%
%%% load_file/1.
%%%
load_file(X) :-
  no_style_check(single_var),
  compile(X).

%%%
%%% Overide selection operator precedences.
%%%
:- op(900,fy,[not]).
:- op(30,fx,[@]).
:- op(100,xfy,[&]).
:- op(120,xfy,[#]).
:- op(150,xfx,[=>,<=>]).
back to top