linear.maude 3.46 KB
Newer Older
Joy Mitra's avatar
Joy Mitra committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
***(

    This file is part of the Maude 2 interpreter.

    Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA.

    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
    (at your option) 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., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.

)

***
***	Maude Diophantine solver.
***	Version 2.3.
***

fmod VECTOR{X :: DEFAULT} is
  protecting (ARRAY * (sort Entry{X,Y} to Entry{Y},
                       sort Array{X,Y} to Vector{Y})
             ){Nat, X} .
endfm

fmod INDEX-PAIR is
  protecting NAT .
  sort IndexPair .
  op _,_ : Nat Nat -> IndexPair [ctor] .
endfm

view IndexPair from TRIV to INDEX-PAIR is
  sort Elt to IndexPair .
endv

fmod MATRIX{X :: DEFAULT} is
  protecting (ARRAY * (sort Entry{X,Y} to Entry{Y},
                       sort Array{X,Y} to Matrix{Y})
             ){IndexPair, X} .
endfm

fmod INT-VECTOR is
  protecting VECTOR{Int0} * (sort Entry{Int0} to IntVectorEntry,
                             sort Vector{Int0} to IntVector,
                             op empty to zeroVector) .
endfm

view IntVector from TRIV to INT-VECTOR is
  sort Elt to IntVector .
endv

fmod INT-MATRIX is
  protecting MATRIX{Int0} * (sort Entry{Int0} to IntMatrixEntry,
                             sort Matrix{Int0} to IntMatrix,
		              op empty to zeroMatrix) .
endfm

fmod DIOPHANTINE is
  protecting STRING .
  protecting INT-MATRIX .
  protecting SET{IntVector} * (sort NeSet{IntVector} to NeIntVectorSet,
                               sort Set{IntVector} to IntVectorSet,
		               op _,_ : Set{IntVector} Set{IntVector} -> Set{IntVector} to
                               (_,_) [prec 121 format (d d ni d)]) .

  sort IntVectorSetPair .
  op [_|_] : IntVectorSet IntVectorSet -> IntVectorSetPair [format (d n++i n ni n-- d)] .

  op natSystemSolve : IntMatrix IntVector String -> IntVectorSetPair
     [special (
        id-hook MatrixOpSymbol		(natSystemSolve)
        op-hook succSymbol		(s_ : Nat ~> NzNat)
        op-hook minusSymbol		(-_ : NzNat ~> Int)
        op-hook stringSymbol		(<Strings> : ~> Char)

        op-hook emptyVectorSymbol	(zeroVector : ~> IntVector)
        op-hook vectorEntrySymbol	(_|->_ : Nat Int ~> IntVectorEntry)
        op-hook vectorSymbol		(_;_ : IntVector IntVector ~> IntVector)

        op-hook emptyMatrixSymbol	(zeroMatrix : ~> IntMatrix)
        op-hook matrixEntrySymbol	(_|->_ : IndexPair Int ~> IntMatrixEntry)
        op-hook matrixSymbol		(_;_ : IntMatrix IntMatrix ~> IntMatrix)
        op-hook indexPairSymbol		(_,_ : Nat Nat ~> IndexPair)

        op-hook emptyVectorSetSymbol	(empty : ~> IntVectorSet)
        op-hook vectorSetSymbol		(_,_ : IntVectorSet IntVectorSet ~> IntVectorSet)
        op-hook vectorSetPairSymbol	([_|_] : IntVectorSet IntVectorSet ~> IntVectorSetPair))] .

  op natSystemSolve : IntMatrix IntVector -> IntVectorSetPair .
  eq natSystemSolve(M:IntMatrix, V:IntVector) = natSystemSolve(M:IntMatrix, V:IntVector, "") .
endfm