#!/usr/bin/perl
# FormulaDB.pm - A db of formulas and there properties
# (c) Copyright 1998 Hakan Ardo <hakan@debian.org>
#
# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# any later version.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program; if not, write to the Free Software
# Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
=head1 NAME
Math::Expr::FormulaDB - A db of formulas and there properties
=head1 SYNOPSIS
require Math::Expr::FormulaDB;
$db=new Math::Expr::FormulaDB($file);
=cut
package Math::Expr::FormulaDB;
use strict;
use Math::Expr;
require Math::Expr::Rule;
sub new {
my $self = bless {}, shift;
$self->Load(shift);
my $db;
my ($vl, $hl);
foreach ($self->Keys) {
$db=$self->Get($_);
$vl=Parse($db->{'vl'}); $vl=$vl->Simplify;
$hl=Parse($db->{'hl'}); $hl=$hl->Simplify;
$db->{'for'}= new Math::Expr::Rule($vl, $hl);
$db->{'back'}= new Math::Expr::Rule($hl, $vl);
}
$self;
}
sub Load {
my ($self, $file) = @_;
if (-f $file) {$self->LoadFile($file);}
if (-d $file) {$self->LoadDir($file);}
}
sub LoadFile {
my ($self, $file) = @_;
my %t;
open (F, "<$file");
while (<F>) {
if (/^([^:]+)\s*:\s*(.*)$/) {
my $a=lc($1);
if (defined $t{$a}) {$t{$a}.="\n$2";} else {$t{$a}=$2;}
}
if (/^\s*$/ || eof F) {
if ($t{'name'}) {
my $t=$t{'name'};
delete $t{'name'};
foreach (keys %t) {
$self->{'opps'}{$t}{$_}=$t{$_};
delete $t{$_};
}
}
}
}
}
sub LoadDir {
my ($self, $dir) = @_;
foreach (split(/\n/s, `find $dir -type f`)) {
next if (/~$/);
$self->LoadFile($_);
}
}
sub Keys {
my $self = shift;
keys %{$self->{'opps'}};
}
sub Get {
my ($self, $a) = @_;
$self->{'opps'}{$a};
}
sub Find {
my ($self, $e, $t) = @_;
my $db;
my ($n, $d, $i);
my (@res, $id);
my $r;
if (!defined $t) {$t=0;}
foreach $n ($self->Keys) {
$db=$self->Get($n);
foreach $d ("for", "back") {
if (!$t || !$db->{'triv'.$d}) {
@res=$db->{$d}->Apply($e);
$id=$db->{$d}->GetId;
for ($i=0; $i<=$#res; $i++) {
$r->{"$n-$d-".$id->[$i]}=$res[$i];
}
}
}
}
$r;
}
sub ApplyProof {
my ($self, $key) = @_;
my %vars;
my $db=$self->Get($key);
my $res="";
my $prev="";
if (defined $db->{'b'}) {
$vars{'vl'}=Parse($db->{'vl'});
$vars{'hl'}=Parse($db->{'hl'});
$res.=$vars{'hl'}->toText;
$vars{'hl'}->Simplify;
$res.=" <=> ".$vars{'hl'}->toText."\n";
$res.=$vars{'vl'}->toText;
$vars{'vl'}->Simplify;
$res.=" <=> " . $vars{'vl'}->toText;
$prev="vl";
foreach (split(/\n/s, $db->{'b'})) {
if (/^\s*\$([^\s=]+)\s*=\s*([^\'\s]*)\s*(\'[^\']+\')?$/) {
my $var=$1; my $rule=$2; my $pre=$3;
if (defined $pre && $pre=~/^\s*\'\s*([^=\s]+)\s*=\s*([^\']+)\'\s*$/) {
my $a=$1; my $b=$2;
print "Pre: $a<=>$b\n";
$pre=new Math::Expr::VarSet;
$pre->Set($a, Parse($b));
} else {
$pre=undef;
}
if ($prev ne $var) {$res.="\n".$vars{$var}->toText;}
$vars{$var}=$self->ApplyAt($vars{$var},$rule,$pre);
$res.=" <=> " . $vars{$var}->toText;
$prev=$var;
}
}
$res."\n";
}
}
sub ApplyAt {
my ($self, $e, $r,$pre) = @_;
my ($rule, $dir, $pos) = split (/-/, $r);
$self->Get($rule)->{$dir}->ApplyAt($e,$pos,$pre);
}
1;