------------------------------------------ 3. Renaming / Contextual constraints check Source: dynamicprog.safe Date: Di 27. Jan 15:03:10 CET 2009 ------------------------------------------ data ListaT a @ r = | [] @ r | : a REC @ r data Maybe a @ rho = | Nothing @ rho | Just a @ rho data Table k v @ rho1 rho2 rho3 = | TBL [TuplaTT k v @ rho1] @ rho2 @ rho3 {* :: Int -> Int -> Int} * 0 0= 0 {()} {+ :: Int -> Int -> Int} + 0 0= 0 {()} {- :: Int -> Int -> Int} - 0 0= 0 {()} {/ :: Int -> Int -> Int} / 0 0= 0 {()} {% :: Int -> Int -> Int} % 0 0= 0 {()} {< :: Int -> Int -> Bool} < 0 0= True {()} {> :: Int -> Int -> Bool} > 0 0= True {()} {== :: a -> a -> Bool} == 1_x {()} 2_y {()}= True {()} {<= :: Int -> Int -> Bool} <= 0 0= True {()} {>= :: Int -> Int -> Bool} >= 0 0= False {()} {&& :: Bool -> Bool -> Bool} && 3_x {()} 4_y {()}= False {()} fst (TuplaT 5_xs1 {()} 6_xs2 {()}) {()}= 5_xs1 {()} snd (TuplaT 7_xs1 {()} 8_xs2 {()}) {()}= 8_xs2 {()} fstD (TuplaT 9_xs1 {()} 10_xs2 {()}) {()} != 9_xs1 {()} sndD (TuplaT 11_xs1 {()} 12_xs2 {()}) {()} != 12_xs2 {()} emptyTbl _ {()}= TBL [] @ _r_ {()} @ _r_ {()} insertTblN (TBL 13_t {()}) {()} 14_k {()} 15_v {()}= TBL : TuplaT 14_k {()} 15_v {()} @ _r_ {()} 13_t {()} @ _r_ {()} @ _r_ {()} insertTblD (TBL 16_t {()}) {()} ! 17_k {()} 18_v {()}= TBL : TuplaT 17_k {()} 18_v {()} @ _r_ {()} 16_t {()} @ _r_ {()} @ _r_ {()} searchTbl (TBL [] {()}) {()} 19_k {()}= Nothing @ _r_ {()} searchTbl (TBL (: (TuplaT 20_k' {()} 21_v' {()}) {()} 22_t {()}) {()}) {()} 23_k {()}= | == 23_k {()} 20_k' {()} {()} = Just 21_v' {()} @ _r_ {()} | True {()} = searchTbl TBL 22_t {()} @ _r_ {()} 23_k {()} {()} concat [] {()} 24_ys {()}= 24_ys {()} concat (: 25_x {()} 26_xs {()}) {()} 27_ys {()}= : 25_x {()} concat 26_xs {()} 27_ys {()} {()} @ _r_ {()} length [] {()}= 0 {()} length (: _ {()} 28_xs {()}) {()}= + 1 {()} length 28_xs {()} {()} {()} putBefore 29_k {()} [] {()}= [] @ _r_ {()} putBefore 30_k {()} (: 31_x {()} 32_xs {()}) {()}= : TuplaT 30_k {()} 31_x {()} @ _r_ {()} putBefore 30_k {()} 32_xs {()} {()} @ _r_ {()} enumFromTo 33_i {()} 34_j {()}= | > 33_i {()} 34_j {()} {()} = [] @ _r_ {()} | True {()} = : 33_i {()} enumFromTo + 33_i {()} 1 {()} {()} 34_j {()} {()} @ _r_ {()} enumPairsFromTo' 35_i {()} 36_i' {()} 37_j' {()}= | > 35_i {()} 37_j' {()} {()} = [] @ _r_ {()} | True {()} = concat putBefore 35_i {()} enumFromTo 36_i' {()} 37_j' {()} {()} {()} enumPairsFromTo' + 35_i {()} 1 {()} {()} 36_i' {()} 37_j' {()} {()} {()} enumPairsFromTo 38_i {()} 39_j {()}= enumPairsFromTo' 38_i {()} 38_i {()} 39_j {()} {()} minimum' 40_min {()} [] {()}= 40_min {()} minimum' 41_min {()} (: 42_x {()} 43_xs {()}) {()}= | < 42_x {()} 41_min {()} {()} = minimum' 42_x {()} 43_xs {()} {()} | True {()} = minimum' 41_min {()} 43_xs {()} {()} minimum (: 44_x {()} 45_xs {()}) {()}= minimum' 44_x {()} 45_xs {()} {()} !! (: 46_x {()} 47_xs {()}) {()} 0= 46_x {()} !! (: 48_x {()} 49_xs {()}) {()} 50_n {()}= !! 49_xs {()} - 50_n {()} 1 {()} {()} {()} createList' 51_k {()} 52_i {()} 53_j {()} 54_d {()} 55_t {()}= | == 51_k {()} 53_j {()} {()} = [] @ _r_ {()} | True {()} = : + 56_c1 {()} + 57_c2 {()} 58_p {()} {()} {()} createList' + 51_k {()} 1 {()} {()} 52_i {()} 53_j {()} 54_d {()} 55_t {()} {()} @ _r_ {()} where (Just 56_c1 {()}) {()}= searchTbl 55_t {()} TuplaT 52_i {()} 51_k {()} @ _r_ {()} {()} (Just 57_c2 {()}) {()}= searchTbl 55_t {()} TuplaT + 51_k {()} 1 {()} {()} 53_j {()} @ _r_ {()} {()} 58_p = * !! 54_d {()} - 52_i {()} 1 {()} {()} {()} * !! 54_d {()} 51_k {()} {()} !! 54_d {()} 53_j {()} {()} {()} {()} createList 59_i {()} 60_j {()} 61_d {()} 62_t {()}= createList' 59_i {()} 59_i {()} 60_j {()} 61_d {()} 62_t {()} {()} calculateCoord (TuplaT 63_i {()} 64_j {()}) {()} 65_d {()} 66_t {()}= | >= 63_i {()} 64_j {()} {()} = 0 {()} | True {()} = minimum createList 63_i {()} 64_j {()} 65_d {()} 66_t {()} {()} {()} calculateTable 67_d {()} 68_t {()} [] {()}= 68_t! {()} calculateTable 69_d {()} 70_t {()} (: 71_x {()} 72_xs {()}) {()}= calculateTable 69_d {()} insertTblD 70_t {()} 71_x {()} calculateCoord 71_x {()} 69_d {()} 70_t {()} {()} {()} 72_xs {()} {()} chainedMatrix 73_d {()}= searchTbl calculateTable 73_d {()} 75_t {()} enumPairsFromTo 0 {()} 74_n {()} {()} {()} TuplaT 1 {()} 74_n {()} @ _r_ {()} {()} where 74_n = length 73_d {()} {()} 75_t = emptyTbl 0 {()} {()} listaEj _ {()}= : 30 {()} : 1 {()} : 40 {()} : 10 {()} : 25 {()} [] @ _r_ {()} @ _r_ {()} @ _r_ {()} @ _r_ {()} @ _r_ {()} @ _r_ {()} chainedMatrix listaEj 0 {()} {()} {()}