types

parent 90bdeb69
......@@ -7,37 +7,36 @@
#:export (use_set_theory sets_to_theory))
(define (sets->theory sets)
(with-fluids ((*current-set-theory* (make-set-theory)))
(let lp ((l sets))
(if (pair? l)
(begin (pk (car l)) (new-set (car l)) (pk (lookup (car l))) (lp (cdr l)))))
(define (sets->theory sets s)
(let lp ((l sets))
(if (pair? l)
(begin
(new-set (car l))
(lp (cdr l)))))
(let lp1 ((l1 sets))
(if (pair? l1)
(begin
(let lp2 ((l2 (cdr l1)))
(if (pair? l2)
(begin
(begin
(cond
((<wrap> subset-scm (car l1) (car l2))
(a->b (car l2) (car l1)))
((<wrap> subset-scm (car l2) (car l1))
(a->b (car l1) (car l2)))
(else #t))
(lp2 (cdr l2))))
(lp1 (cdr l1)))))))
(fluid-ref *current-set-theory*)))
(let lp1 ((l1 sets))
(if (pair? l1)
(begin
(let lp2 ((l2 (cdr l1)))
(if (pair? l2)
(begin
(begin
(cond
((<wrap-s> subset-scm s (car l1) (car l2))
(a->b (car l2) (car l1)))
((<wrap-s> subset-scm s (car l2) (car l1))
(a->b (car l1) (car l2)))
(else #t))
(lp2 (cdr l2))))
(lp1 (cdr l1))))))))
(<define> (use_set_theory theory)
(<code> (fluid-set! *current-set-theory* (<lookup> theory))))
(<define> (sets_to_theory sets theory)
(<define> (sets_to_theory sets)
(let lp ((l sets) (ll '()))
(<match> (#:mode -) (l)
((x . l) (lp l (cons (<lookup> x) ll)))
(()
(<=> theory ,(sets->theory ll))))))
(<code> (sets->theory ll S))))))
......@@ -526,7 +526,7 @@ a natural generational mapping to help in constructing a match tree.
(x (list x)))))
(define (p x)
(pk 'revlockup (map (lambda (x) (reverse-lookup theory x)) x))
(map (lambda (x) (reverse-lookup theory x)) x)
x)
(define setlist (linearize (mktree1 setbits)))
......
......@@ -291,7 +291,7 @@
(instantiation_error))
(#((F . A))
(<cut>
(<recur> lp2 ((F (pk (<lookup> F))))
(<recur> lp2 ((F (<lookup> F)))
(if (not (dynamic? F))
(if (procedure? F)
(if (object-property F 'prolog-symbol)
......@@ -323,7 +323,7 @@
(#((F . A))
(<cut>
(<values> (A Body) (analyze A true))
(<recur> lp ((F (pk (<lookup> F))))
(<recur> lp ((F (<lookup> F)))
(if (not (dynamic? F))
(if (procedure? F)
(if (object-property F 'prolog-symbol)
......
......@@ -835,7 +835,7 @@
n (lp2 pre) n
(lp a) (map lp (gp->scm l s)))
(format #f "~a is ~a(~a~{,~a~}),~a(~a~{,~a~})"
n (pk 1 (lp2 pre))
n (lp2 pre)
(car args) (cdr args)
n (lp a) (map lp (gp->scm l s)))))))
(format #f "~a(~a~{,~a~})"
......
......@@ -10,6 +10,8 @@
#:replace (type)
#:export (type? Type mk-type))
(define-syntax-rule (aif it p a b) (let ((it p)) (if it a b)))
(define cons--
(case-lambda
(() '())
......@@ -28,9 +30,11 @@
((V)
(<=> V "nonvar"))
((Var V YY Write)
((Var V YY Write)
(<=> Write "write")
(<=> YY ,(vector (cons- type Var (<lookup> V)))))
(let ((V (<lookup> V)))
;;(<=> YY ,(vector (cons- type Var (reverse-lookup (car V)) (cdr V))))))
(<=> YY ,(vector (cons- type Var (car V) (cdr V))))))
((me val pred?)
(let ((val (<lookup> val))
......@@ -90,7 +94,6 @@
(<define> (type x f . l)
(let ((x (<lookup> x))
(f (<lookup> f)))
(<pp> (list 'type l))
(<var> (v)
(<if> (<get-attr> x Type v)
(let* ((v (<lookup> v))
......
......@@ -332,7 +332,7 @@
(define sfluid (make-fluid #f))
(define (s) (fluid-ref *cuurent-stack*))
(define (s) (fluid-ref *current-stack*))
(define (xhash x size)
(let lp ((x x))
(umatch (#:mode -) (x)
......
......@@ -2,7 +2,7 @@
(use-modules (logic guile-log))
(use-modules (logic guile-log type))
(use-modules ((logic guile-log inheritance) #:select
(compile-sup-sub print-theory *current-set-theory*
(compile-sup-sub print-theory *current-set-theory* reverse-lookup
order-the-set (lookup . get))))
(use-modules (logic guile-log guile-prolog attribute))
(use-modules (logic guile-log guile-prolog set))
......@@ -36,23 +36,38 @@ f4(A,B) :- mk({1,2},X),(A⊔B)⊂X.
(define bS #f)
(define cS #f)
(<define> (revlookup a b)
(<=> b ,(reverse-lookup (<lookup> a))))
(compile-prolog-string
"
:- dynamic(class).
cls(X,L) :-
tr(X,L) :-
class(X,C),
L = (X : C).
texp(X,X) :- var(X),(\\+attvar(X)),!.
texp(cls(X),L) :-
class(X,C),
L = (X : C).
texp([A|B],[AA|BB]) :- texp(A,AA),texp(B,BB).
texp(A(|B),AA(|BB)) :- texp(A,AA),texp(B,BB).
texp({A},{AA}) :- texp(A,AA).
texp(A,A).
e(X,L) :-
texp(X,XX,true,LL),
(
LL=true ->
L=XX ;
L = (LL,XX)
).
texp(X,X,L,L) :- var(X),(\\+attvar(X)),!.
texp(cls(X),U,L,LL) :- !,
LL = (L,(class(X,C),U=(X : C))).
texp(cls(X,C),U,L,LL) :- !,
get_attr(C,'Type',[A|_]),
revlookup(A,AA),
AA ⊆ X,
LL = (L,(U=(X : C))).
texp([A|B],[AA|BB],L,LL) :- texp(A,AA,L,L1),texp(B,BB,L1,LL).
texp(A(|B),AA(|BB),L,LL) :- texp(A,AA,L,L1),texp(B,BB,L1,LL).
texp({A},{AA},L,LL) :- texp(A,AA,L,LL).
texp(A,A,L,L).
......@@ -60,7 +75,6 @@ f4(A,B) :- mk({1,2},X),(A⊔B)⊂X.
mktype(X,C),
asserta(class(X,C)).
% :- add_goal_expansion(texp).
")
......@@ -71,8 +85,7 @@ f4(A,B) :- mk({1,2},X),(A⊔B)⊂X.
B is {\"b\"},
C is A∪B,
sets_to_theory([A,B,C],Theory),
use_set_theory(Theory),
sets_to_theory([A,B,C]),
do[(set! aS (<lookup> A))],
do[(set! bS (<lookup> B))],
......@@ -98,22 +111,22 @@ f4(A,B) :- mk({1,2},X),(A⊔B)⊂X.
(prolog-run 1 () (tp))
(compile-prolog-string
"
ftheory(X : scm[cT]) :- write(c(X)),fail.
ftheory(X : scm[aT]) :- write(a(X)),fail.
ftheory(X : scm[bT]) :- write(b(X)),fail.
ftheory(X : cT) :- write(c(X)),fail.
ftheory(X : aT) :- write(a(X)),fail.
ftheory(X : bT) :- write(b(X)),fail.
t(X) :- (X -> write(true(X)) ; write(false(X))),nl.
t(X) :- e(X,XX),(XX -> write(true(X)) ; write(false(X))),nl.
test :-
write(start),nl,
cls(aS,A),
cls(bS,B),
cls(cS,C),
t(ftheory(A)),
t(ftheory(B)),
t(ftheory(C)).
nl,write(start),nl,nl,
t(ftheory(cls(aS))),
t(ftheory(cls(bS))),
t(ftheory(cls(cS))),
X is {a-2},t(ftheory(cls(X))),
Y is {a-2,b-4},t(ftheory(cls(Y,aT))).
")
(prolog-run 1 () (test))
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment