equal
deleted
inserted
replaced
779 } |
779 } |
780 } |
780 } |
781 |
781 |
782 // fun pAKC_aux :: "arexp list ⇒ arexp ⇒ rexp ⇒ arexp" |
782 // fun pAKC_aux :: "arexp list ⇒ arexp ⇒ rexp ⇒ arexp" |
783 // where |
783 // where |
784 // "pAKC_aux rsa r ctx = (if (regConcat (SEQ (erase r) ( ctx) )) ⊆ (regConcat (erase (AALTs [] rsa))) then AZERO else |
784 // "pAKC_aux rsa r ctx = (if (seqFold (SEQ (erase r) ( ctx) )) ⊆ (seqFold (erase (AALTs [] rsa))) then AZERO else |
785 // case r of (ASEQ bs r1 r2) ⇒ |
785 // case r of (ASEQ bs r1 r2) ⇒ |
786 // bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ (erase r2) ( ctx) )) r2 | |
786 // bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ (erase r2) ( ctx) )) r2 | |
787 // (AALTs bs rs) ⇒ |
787 // (AALTs bs rs) ⇒ |
788 // bsimp_AALTs bs (flts (map (λr. pAKC_aux rsa r ( ctx) ) rs) ) | |
788 // bsimp_AALTs bs (flts (map (λr. pAKC_aux rsa r ( ctx) ) rs) ) | |
789 // r ⇒ r |
789 // r ⇒ r |
794 // case r1::r2::Nil => SEQ(SEQ(r1, r2), acc) |
794 // case r1::r2::Nil => SEQ(SEQ(r1, r2), acc) |
795 // } |
795 // } |
796 |
796 |
797 |
797 |
798 //the "fake" Language interpretation: just concatenates! |
798 //the "fake" Language interpretation: just concatenates! |
799 def regConcat(acc: Rexp, rs: List[Rexp]) : Rexp = rs match { |
799 def seqFold(acc: Rexp, rs: List[Rexp]) : Rexp = rs match { |
800 case Nil => acc |
800 case Nil => acc |
801 case r :: rs1 => |
801 case r :: rs1 => |
802 // if(acc == ONE) |
802 // if(acc == ONE) |
803 // regConcat(r, rs1) |
803 // seqFold(r, rs1) |
804 // else |
804 // else |
805 regConcat(SEQ(acc, r), rs1) |
805 seqFold(SEQ(acc, r), rs1) |
806 } |
806 } |
807 |
807 |
808 def rprint(r: Rexp) : Unit = println(shortRexpOutput(r)) |
808 def rprint(r: Rexp) : Unit = println(shortRexpOutput(r)) |
809 def rsprint(rs: Iterable[Rexp]) = rs.foreach(r => println(shortRexpOutput(r))) |
809 def rsprint(rs: Iterable[Rexp]) = rs.foreach(r => println(shortRexpOutput(r))) |
810 |
810 |
817 // println("acc") |
817 // println("acc") |
818 // rsprint(acc) |
818 // rsprint(acc) |
819 // println("ctx---------") |
819 // println("ctx---------") |
820 // rsprint(ctx) |
820 // rsprint(ctx) |
821 // println("ctx---------end") |
821 // println("ctx---------end") |
822 // rsprint(breakIntoTerms(regConcat(erase(r), ctx)).map(oneSimp)) |
822 // rsprint(breakIntoTerms(seqFold(erase(r), ctx)).map(oneSimp)) |
823 |
823 |
824 if (breakIntoTerms(regConcat(erase(r), ctx)).map(oneSimp).forall(acc.contains)) {//acc.flatMap(breakIntoTerms |
824 if (breakIntoTerms(seqFold(erase(r), ctx)).map(oneSimp).forall(acc.contains)) {//acc.flatMap(breakIntoTerms |
825 AZERO |
825 AZERO |
826 } |
826 } |
827 else{ |
827 else{ |
828 r match { |
828 r match { |
829 case ASEQ(bs, r1, r2) => |
829 case ASEQ(bs, r1, r2) => |
926 else |
926 else |
927 SEQ(r11, r2) :: Nil |
927 SEQ(r11, r2) :: Nil |
928 } |
928 } |
929 |
929 |
930 def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = { |
930 def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = { |
931 turnIntoTerms((regConcat(erase(r), ctx))) |
931 turnIntoTerms((seqFold(erase(r), ctx))) |
932 .toSet |
932 .toSet |
933 } |
933 } |
934 |
934 |
935 def attachCtxcc(r: Rexp, ctx: List[Rexp]) : Set[Rexp] = |
935 def attachCtxcc(r: Rexp, ctx: List[Rexp]) : Set[Rexp] = |
936 turnIntoTerms(regConcat(r, ctx)).toSet |
936 turnIntoTerms(seqFold(r, ctx)).toSet |
937 |
937 |
938 def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, |
938 def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, |
939 subseteqPred: (C, C) => Boolean) : Boolean = { |
939 subseteqPred: (C, C) => Boolean) : Boolean = { |
940 subseteqPred(f(a, b), c) |
940 subseteqPred(f(a, b), c) |
941 } |
941 } |