From 7b9cd608108481cff16282d7447b52f56ab8394a Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Thu, 13 Dec 2012 15:49:11 +0100
Subject: [PATCH] Removed legacy Isabelle pretty-printer.
(This was a semester project by Octavian-Eugen Ganea, first half of
2011.)
---
src/main/scala/leon/isabelle/Main.scala | 825 ------------------
src/main/scala/leon/isabelle/README | 56 --
.../isabelle/StrongConnectedComponents.scala | 167 ----
3 files changed, 1048 deletions(-)
delete mode 100644 src/main/scala/leon/isabelle/Main.scala
delete mode 100644 src/main/scala/leon/isabelle/README
delete mode 100644 src/main/scala/leon/isabelle/StrongConnectedComponents.scala
diff --git a/src/main/scala/leon/isabelle/Main.scala b/src/main/scala/leon/isabelle/Main.scala
deleted file mode 100644
index abd1f5576..000000000
--- a/src/main/scala/leon/isabelle/Main.scala
+++ /dev/null
@@ -1,825 +0,0 @@
-package leon
-package isabelle
-
-import leon.Reporter
-import leon.Settings._
-
-import leon.purescala.Common.Identifier
-import leon.purescala.Definitions._
-import leon.purescala.PrettyPrinter
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.Extractors._
-import leon.purescala.TypeTrees._
-
-import java.lang.StringBuffer
-import java.io._
-import scala.collection.mutable.ListMap
-
-// TODO FIXME If this class is to be resurrected, make it a proper phase
-@deprecated("Unused, Untested, Unmaintained.", "")
-class Main(context : LeonContext) {
- val description = "Generates Isabelle source"
- val shortDescription = "isabelle"
-
- private val reporter = context.reporter
-
- var mapParentTypes = new ListMap[String, String]
-
- //map for each function keeps the functions that it calls inside it
- var functionDependsOn = new ListMap[String, List[String]]
- var currentFunction = ""
- //current #res:
- var current_res = ""
-
- //list of binders : for expressions like x match { case binder@expr => E[binder] }
- var bindersMap = new ListMap[MatchCase, (Identifier, String)]
-
- //function that takes a variable name and returns a valid Isabelle fresh name:
- private def freshName(s : String) : String = {
- if((s.length <= 2 || s.length >= 5) && Character.isLetter(s.charAt(s.length - 1)) && Character.isLetter(s.charAt(0)))
- return s
- if(Character.isLetter(s.charAt(s.length - 1)))
- return "var_" + s
- if(Character.isLetter(s.charAt(0)))
- return s + "_var"
- return "var_" + s + "_var"
-
- }
-
- //function that transforms an expression if it is a match with guards (if on branches) in one without matches:
- private def transformGuardedMatchExpression(tree: Expr): Expr = tree match {
- case mex @ MatchExpr(s, csc) => {
- var rez = tree
- csc.foreach(cs => {
- cs.theGuard.foreach(g => {
- rez = matchToIfThenElse(tree)
- })
- })
- rez
- }
- case _ => tree
- }
-
- def apply(tree: Expr): String = {
- val retSB = pp(tree, new StringBuffer, 0)
- retSB.toString
- }
-
- def apply(tpe: TypeTree): String = {
- val retSB = pp(tpe, new StringBuffer, 0)
- retSB.toString
- }
-
- def apply(defn: Definition): String = {
- val retSB = pp(defn, new StringBuffer, 0)
- retSB.toString
- }
-
- private def ind(sb: StringBuffer, lvl: Int): StringBuffer = {
- sb.append(" " * lvl)
- sb
- }
-
- // EXPRESSIONS
- // all expressions are printed in-line
- private def ppUnary(sb: StringBuffer, expr: Expr, op1: String, op2: String, lvl: Int): StringBuffer = {
- var nsb: StringBuffer = sb
- nsb.append(op1)
- nsb = pp(expr, nsb, lvl)
- nsb.append(op2)
- nsb
- }
-
- private def ppBinary(sb: StringBuffer, left: Expr, right: Expr, op: String, lvl: Int): StringBuffer = {
- var nsb: StringBuffer = sb
- nsb.append("(")
- nsb = pp(left, nsb, lvl)
- nsb.append(op)
- nsb = pp(right, nsb, lvl)
- nsb.append(")")
- nsb
- }
-
- private def ppNary(sb: StringBuffer, exprs: Seq[Expr], pre: String, op: String, post: String, lvl: Int): StringBuffer = {
- var nsb = sb
- nsb.append(pre)
- val sz = exprs.size
- var c = 0
-
- exprs.foreach(ex => {
- nsb = pp(ex, nsb, lvl); c += 1; if (c < sz) nsb.append(op)
- })
-
- nsb.append(post)
- nsb
- }
-
- private def pp(tree: Expr, sb: StringBuffer, lvl: Int): StringBuffer = transformGuardedMatchExpression(tree) match {
- case Variable(id) => {
- //we need to replace binders by their actual expressions
- var found = false
- bindersMap.foreach(t =>
- if (t._2._1.toString.compareTo(id.toString) == 0) {
- found = true
- sb.append(t._2._2)
- })
- if (!found)
- sb.append(freshName(id.toString)) //add this to avoid isabelle reserved names like "min"
- sb
- }
- case Let(b, d, e) => {
- var nsb = pp(d, sb.append("(let " + freshName(b.toString) + " = "), lvl).append(" in \n")
- ind(nsb, lvl + 2)
- pp(e, nsb, lvl + 2).append(")")
- }
- case And(exprs) => ppNary(sb, exprs, "(", " \\<and> ", ")", lvl)
- case Or(exprs) => ppNary(sb, exprs, "(", " \\<or> ", ")", lvl)
- case Not(Equals(l, r)) => ppBinary(sb, l, r, " \\<noteq> ", lvl)
- case Iff(l, r) => ppBinary(sb, l, r, " \\<Leftrightarrow> ", lvl)
- case Implies(l, r) => ppBinary(sb, l, r, " \\<longrightarrow> ", lvl)
- case UMinus(expr) => ppUnary(sb, expr, "-(", ")", lvl)
- case Equals(l, r) => ppBinary(sb, l, r, " = ", lvl)
- case IntLiteral(v) => sb.append(v)
- case BooleanLiteral(v) => v match {
- case true => sb.append("True")
- case false => sb.append("False")
- }
- case StringLiteral(s) => sb.append("\"" + s + "\"")
- case CaseClass(cd, args) => {
- var nsb = sb
- nsb.append("(" + cd.id)
- nsb = ppNary(nsb, args, " ", " ", ")", lvl)
- nsb
- }
- case CaseClassInstanceOf(cd, e) => {
- var nsb = sb
- nsb.append("(case ")
- nsb = pp(e, nsb, lvl)
- nsb.append(" of (" + cd.id)
- cd.fields.foreach(vd => {
- nsb.append(" _")
- })
- nsb.append(") \\<Rightarrow> True")
- //nsb.append("| _ \\<Rightarrow> False")
- nsb.append(") ")
-
- nsb
- }
- case CaseClassSelector(ccdef, cc, id) => {
- sb.append("(" + ccdef.id + "__" + id + " ")
- pp(cc, sb, 0)
- sb.append(")")
- }
-
- //does it calls a previous defined function or not ?
- case FunctionInvocation(fd, args) => {
- var nsb = sb
- if (currentFunction.compareTo("") != 0 && currentFunction.compareTo(fd.id.toString + "" + fd.args.size) != 0) {
- var list = Nil: List[String]
- functionDependsOn.get(currentFunction) match {
- case None => reporter.error("function not defined: " + currentFunction)
- case Some(l) => list = l
- }
- list = (fd.id.toString + "" + fd.args.size) :: list
- functionDependsOn.update(currentFunction, list.distinct)
- }
- nsb.append("(" + fd.id.toString + "" + fd.args.size)
- nsb = ppNary(nsb, args, " ", " ", " ", lvl)
- nsb.append(")")
- nsb
- }
- case Plus(l, r) => ppBinary(sb, l, r, " + ", lvl)
- case Minus(l, r) => ppBinary(sb, l, r, " - ", lvl)
- case Times(l, r) => ppBinary(sb, l, r, " * ", lvl)
- case Division(l, r) => ppBinary(sb, l, r, " / ", lvl)
- case LessThan(l, r) => ppBinary(sb, l, r, " < ", lvl)
- case GreaterThan(l, r) => ppBinary(sb, l, r, " > ", lvl)
- case LessEquals(l, r) => ppBinary(sb, l, r, " \\<le> ", lvl) // \leq
- case GreaterEquals(l, r) => ppBinary(sb, l, r, " \\<ge> ", lvl) // \geq
- case FiniteSet(rs) => ppNary(sb, rs, "{", ", ", "}", lvl)
- case FiniteMultiset(rs) => {
- reporter.error("[not handled ] FinitMultiset")
- ppNary(sb, rs, "{|", ", ", "|}", lvl) //TODO
- }
- case EmptySet(_) => sb.append("{}") // Ø
- case EmptyMultiset(_) => sb.append("{}") // Ø
- case Not(ElementOfSet(s, e)) => ppBinary(sb, s, e, " \\<notin> ", lvl) // \notin
- case ElementOfSet(s, e) => ppBinary(sb, s, e, " \\<in> ", lvl) // \in
- case SubsetOf(l, r) => ppBinary(sb, l, r, " \\<subseteq> ", lvl) // \subseteq
- case Not(SubsetOf(l, r)) => ppBinary(sb, l, r, " \\<not> \\<subseteq> ", lvl) // \notsubseteq
- case SetMin(s) => {
- reporter.error("[not handled ] SetMin")
- pp(s, sb, lvl).append(".min") //TODO
- }
- case SetMax(s) => {
- reporter.error("[not handled ] SetMax")
- pp(s, sb, lvl).append(".max") //TODO
- }
- case SetUnion(l, r) => ppBinary(sb, l, r, " \\<union> ", lvl) // \cup
- case MultisetUnion(l, r) => ppBinary(sb, l, r, " \\<union> ", lvl) // \cup
- case SetDifference(l, r) => ppBinary(sb, l, r, " - ", lvl)
- case MultisetDifference(l, r) => ppBinary(sb, l, r, " - ", lvl)
- case SetIntersection(l, r) => ppBinary(sb, l, r, " \\<inter> ", lvl) // \cap
- case MultisetIntersection(l, r) => ppBinary(sb, l, r, " \\<inter> ", lvl) // \cap
- case SetCardinality(t) => ppUnary(sb, t, "(card ", ")", lvl)
- case MultisetCardinality(t) => ppUnary(sb, t, "(card ", ")", lvl)
- case MultisetPlus(l, r) => {
- reporter.error("[not handled ] MultiSetPlus")
- ppBinary(sb, l, r, " \u228E ", lvl) // TODO
- }
- case MultisetToSet(e) => {
- reporter.error("[not handled ] MultisetToSet")
- pp(e, sb, lvl).append(".toSet") //TODO
- }
- case IfExpr(c, t, e) => {
- var nsb = sb
- nsb.append("(if (")
- nsb = pp(c, nsb, lvl)
- nsb.append(") then (\n")
- ind(nsb, lvl + 1)
- nsb = pp(t, nsb, lvl + 1)
- nsb.append("\n")
- ind(nsb, lvl + 1)
- nsb.append(") else (\n")
- ind(nsb, lvl + 1)
- nsb = pp(e, nsb, lvl + 1)
- nsb.append("\n")
- ind(nsb, lvl)
- nsb.append("))")
- nsb
- }
-
- case mex @ MatchExpr(s, csc) => {
- def ppc(sb: StringBuffer, p: Pattern, matchcase: MatchCase): StringBuffer = p match {
-
- case CaseClassPattern(bndr, ccd, subps) => {
- var buf = new StringBuffer
- buf.append("(").append(ccd.id).append(" ")
- var c = 0
- val sz = subps.size
- subps.foreach(sp => {
- buf = ppc(buf, sp, matchcase)
- if (c < sz - 1)
- buf.append(" ")
- c = c + 1
- })
- buf.append(")")
-
- bndr.foreach(b => bindersMap.update(matchcase, (b, buf.toString)))
-
- sb.append(buf.toString)
- }
- case WildcardPattern(None) => sb.append("_")
- case WildcardPattern(Some(id)) => {
- sb.append(freshName(id.toString))
- }
- case _ => sb.append("Pattern?")
- }
-
- var nsb = sb
- nsb.append("(case ")
- nsb == pp(s, nsb, lvl)
- nsb.append(" of\n")
-
- var len1 = csc.size
- var c1 = 0
-
- csc.foreach(cs => {
- ind(nsb, lvl + 2)
- nsb = ppc(nsb, cs.pattern, cs)
-
- nsb.append(" \\<Rightarrow> \n")
- ind(nsb, lvl + 4)
-
- cs.theGuard.foreach(g => {
- reporter.error("!!!!! match case has IF condition - BUG of translation if it enters here!")
- })
-
- nsb = pp(cs.rhs, nsb, lvl + 4)
- if (c1 < len1 - 1)
- nsb.append(" |")
- nsb.append("\n")
- c1 = c1 + 1
-
- bindersMap = bindersMap - cs
- })
- ind(nsb, lvl).append(" )\n")
- nsb
- }
-
- //#res
- case ResultVariable() => sb.append(current_res)
- case Not(expr) => ppUnary(sb, expr, "\\<not>(", ")", lvl)
-
- case e @ Error(desc) => {
- var nsb = sb
- nsb.append("error(\"" + desc + "\")[")
- nsb = pp(e.getType, nsb, lvl)
- nsb.append("]")
- nsb
- }
-
- case _ => sb.append("Expr?")
- }
-
- // TYPE TREES
- // all type trees are printed in-line
- private def pp(tpe: TypeTree, sb: StringBuffer, lvl: Int): StringBuffer = tpe match {
- case Untyped => sb.append("???")
- case Int32Type => sb.append("int")
- case BooleanType => sb.append("bool")
- case SetType(bt) => pp(bt, sb.append("("), lvl).append(" set)")
- case MultisetType(bt) => {
- println("[not handled] multisettype")
- pp(bt, sb.append("Multiset["), lvl).append("]")
- }
- case c: ClassType => sb.append(mapParentTypes.get(c.classDef.id.toString) match {
- case None => c.classDef.id
- case Some(l) => l
- })
- case _ => sb.append("Type?")
- }
-
- // DEFINITIONS
- // all definitions are printed with an end-of-line
- private def pp(defn: Definition, sb: StringBuffer, lvl: Int): StringBuffer = {
-
- defn match {
- case Program(id, mainObj) => {
- assert(lvl == 0)
- pp(mainObj, sb, lvl)
- sb.append("end\n")
- }
-
- case ObjectDef(id, defs, invs) => {
- var nsb = sb
- sb.append("theory " + id + "\n")
- sb.append("imports Datatype Main\n")
- sb.append("begin\n\n")
-
- val definedFunctions: Seq[FunDef] = defs.filter(_.isInstanceOf[FunDef]).map(_.asInstanceOf[FunDef])
- val definedClasses: Seq[ClassTypeDef] = defs.filter(_.isInstanceOf[ClassTypeDef]).map(_.asInstanceOf[ClassTypeDef])
-
- /*interpret datatype definitions:
- case class Binary(exp1 : Expr, op : BinOp, exp2 : Expr) extends Expr ==>
- datatype Expr = ...
- | Binary Expr BinOp Expr
- */
- var map = new ListMap[String, List[List[String]]]
-
- definedClasses.foreach(dc => {
- dc match {
- case AbstractClassDef(id2, parent) => {
- parent match {
- case None =>
- case _ => reporter.error("[not analyzed] sealed class " + id2 + " should not have a parent")
- }
- }
- //suppose parent is not a typed class (e.g "List int")
- case CaseClassDef(id2, parent, varDecls) => {
- var datatype: Option[List[List[String]]] = None
- var nsb = sb
- parent match {
- case None => reporter.error("case class without parent")
- case Some(AbstractClassDef(idparent, ll)) => {
- datatype = map.get(idparent.toString)
- //list = list of current subtypes of this datatype
- var list: List[List[String]] = List()
- datatype match {
- case None =>
- case Some(l) => list = l
- }
-
- /*list of the subtype (e.g case Value(v:int) extends Expr ----> List(Value, int) ) */
- var subtype_list = Nil: List[String]
- subtype_list = subtype_list :+ id2.toString
-
- varDecls.foreach(vd => {
- var subtype = new StringBuffer
- pp(vd.tpe, subtype, 0) // type of parameters
- subtype_list = subtype_list :+ subtype.toString
- })
- list = list :+ subtype_list
- map.update(idparent.toString, list)
- }
- }
- }
- }
- })
-
- /*map that keeps every case class in map with its parent */
- /*case class Value (v : Int) extends Whatever ---> Value will have as parent type Whatever */
- map foreach ((t1) =>
- for (t2 <- t1._2)
- mapParentTypes.update(t2.head, t1._1))
-
- /* if a case class appears in one definition, then replace it by it parent class */
- map foreach ((one_type) => {
- var l = Nil: List[List[String]]
- for (subtype_list <- one_type._2) {
- var ll = List(subtype_list.head)
- for (dependent_type <- subtype_list.tail) {
- var x = mapParentTypes.get(dependent_type)
- x match {
- case Some(s) => ll = ll :+ s
- case None => ll = ll :+ dependent_type
- }
- }
- l = l :+ ll
- }
- map.update(one_type._1, l)
- })
-/// ============================== SORT DATATYPES BY THE CORRECT ORDER ===========================================
- // def contains(t: (String, List[List[String]]) ,l : List[(String, List[List[String]])]) : Boolean ={
- def contains(t: (String, Any), l: List[(String, Any)]): Boolean = {
- for (el <- l)
- if (t._1.compareTo(el._1) == 0)
- return true
- false
- }
-
- //graph of datatypes dependencies
- var graphDatatypes = new ListMap[String, List[String]]
- map foreach ((t1) => graphDatatypes.update(t1._1, Nil : List[String]))
-
- map foreach ((t1) =>
- map foreach ((t2) =>
- if(t2._1.compareTo(t1._1) != 0)
- for (el <- t2._2)
- for (str <- el)
- if (str.compareTo(t1._1) == 0){
- var o = graphDatatypes.get(t1._1)
- var list = Nil : List[String]
- o match {
- case None => list = Nil: List[String]
- case Some(l) => list = l
- }
- graphDatatypes.update(t1._1, list ::: List(t2._1))
- }
- ))
-
- var components = StrongConnectedComponents.stronglyOrderedConnectedComponents(graphDatatypes)
-
- def preetyPrint(l: List[String], nsb: StringBuffer): Unit = {
- for (el <- l)
- nsb.append(el + " ")
- }
-
- components.foreach(comp => {
- var type_decl = "datatype "
- comp.foreach(parenttype => {
- var numberTabs = (type_decl + parenttype + " ").size
- nsb.append(type_decl + parenttype + " = ")
- type_decl = " and "
-
- var o = map.get(parenttype)
- var list = Nil : List[List[String]]
- o match {
- case None => list = Nil: List[List[String]]
- case Some(l) => list = l
- }
-
- preetyPrint(list.head, nsb)
- nsb.append("\n")
- for (el <- list.tail) {
- nsb.append(" " * numberTabs)
- nsb.append("| ")
- preetyPrint(el, nsb)
- nsb.append("\n")
- }
- })
- nsb.append("\n")
- })
-
- nsb.append("\n")
-
- //================================= FUNCTIONS FOR FIELD ACCESS: ==========================================
- /* case class Acc(checking : Int, savings : Int) extends AccLike ---->
- fun Acc__checking :: "AccLike \<Rightarrow> Int" where
- "Acc__checking var =
- (case var of (Acc checking savings) \Rightarrow checking)"
-*/
- definedClasses.foreach(dc => {
- dc match {
- case AbstractClassDef(id2, parent) =>
- //suppose parent is not a typed class (e.g "List int")
- case CaseClassDef(id2, parent, varDecls) => {
- parent match {
- case None => reporter.error("case class without parent")
- case Some(AbstractClassDef(idparent, ll)) => {
- varDecls.foreach(vd => {
- var subtype = new StringBuffer
- pp(vd.tpe, subtype, 0) // type of parameter
-
- ind(nsb, lvl)
- nsb.append("primrec " + id2 + "__" + vd.id + " :: \"" + idparent + " \\<Rightarrow> " + subtype.toString + "\"")
- nsb.append(" where\n")
- ind(nsb, lvl + 2)
- nsb.append("\"" + id2 + "__" + vd.id)
- nsb.append(" (" + id2)
- for (j <- varDecls)
- nsb.append(" " + freshName(j.id.toString))
- nsb.append(") = " + freshName(vd.id.toString) + "\"\n\n")
-
- })
- }
- case Some(_) => reporter.error("case class has parent another case class - n/a")
- }
- }
- }
- })
-
- //=========================== FUNCTIONS ORDER ================
- //the following sets the right order of functions according to dependencies
- //interpret functions
- var functionCode = new ListMap[String, StringBuffer]
-
- definedFunctions.foreach(df => {
- var sbaux = new StringBuffer
- //get function code recursively
- sbaux = pp(df, sbaux, lvl)
- sbaux.append("\n\n")
- if(functionCode.get(df.id + "" + df.args.size).isDefined)
- reporter.error("unexpected duplicate of function definitions")
- else
- functionCode.update(df.id + "" + df.args.size, sbaux)
- })
-
- def functionBody (f : String) : String = {
- functionCode.get(f) match {
- case Some(buf) => buf.toString
- case None => "fatal error in functions translation"
- }
- }
-
- var sortedFunctionList = StrongConnectedComponents.stronglyOrderedConnectedComponents(functionDependsOn)
-
- //reverse the list because transpose graph of functionDependsOn should be used
- sortedFunctionList.reverse.foreach(comp => {
- var fun_decl = "fun "
- comp.foreach(fun => {
- var body = functionBody(fun)
- var indexOfFunDeclaration = body.indexOf("fun ")
- var offsetOfFunDeclaration = indexOfFunDeclaration + 4
- if(body.indexOf("primrec ") >=0){
- indexOfFunDeclaration = body.indexOf("primrec ")
- offsetOfFunDeclaration = indexOfFunDeclaration + 8
- fun_decl = "primrec "
- }
- if(indexOfFunDeclaration >=0)
- nsb.append("\n" + fun_decl + body.substring(offsetOfFunDeclaration,body.indexOf("where")))
- else{
- fun_decl = "definition "
- assert(body.indexOf("definition ") >=0)
- nsb.append("\n" + fun_decl + body.substring(body.indexOf("definition ") + 11,body.indexOf("where")))
- }
-
- fun_decl = "and "
- })
- nsb.append("where")
- var first = true
- comp.foreach(fun => {
- if(!first)
- nsb.append(" |")
- var body = functionBody(fun)
- if(body.indexOf("lemma ") >=0 )
- nsb.append(body.substring(body.indexOf("where") + 6,body.indexOf("lemma ")))
- else
- nsb.append(body.substring(body.indexOf("where") + 6,body.length - 1))
- first = false
- })
-
- comp.foreach(fun => {
- var body = functionBody(fun)
- if(body.indexOf("lemma ") >=0 )
- nsb.append(body.substring(body.indexOf("lemma "),body.length - 1)+ "\n")
- })
- })
-
- nsb
- }
-
- //========================================== FUNCTIONS =====================================================
- /*
- def evalOp(v1 : Value, op : BinOp, v2 : Value) : Value = .....
- fun evalOp :: "Value \<Rightarrow> BinOp \<Rightarrow> Value \<Rightarrow> Value" where
- "evalOp v1 op v2 = ( ..... )"
- */
-
- //functions :
- case fd @ FunDef(id, rt, args, body, pre, post) => {
- var nsb = sb
- var functionName = id + "" + args.size
- functionDependsOn.update(functionName, List())
- currentFunction = functionName
-
- for (a <- fd.annotations) {
- ind(nsb, lvl)
- nsb.append("(* @" + a + " *)\n")
- }
-
- pre.foreach(prec => {
- ind(nsb, lvl)
- nsb.append("(* @pre : ")
- nsb = pp(prec, nsb, lvl)
- nsb.append(" *)\n")
- })
-
- ind(nsb, lvl)
- if (args.size > 0){
- transformGuardedMatchExpression(body.get) match {
- case SimplePatternMatching(e, ct, patterns) => nsb.append("primrec ")
- case _ => nsb.append("fun ")
- }
- }
- else
- nsb.append("definition ")
- nsb.append(functionName)
- nsb.append(" :: \"")
-
- val sz = args.size
- var c = 0
-
- args.foreach(arg => {
- nsb = pp(arg.tpe, nsb, lvl)
-
- if (c < sz - 1) {
- nsb.append(" \\<Rightarrow> ")
- }
- c = c + 1
- })
-
- if (args.size > 0)
- nsb.append(" \\<Rightarrow> ")
- nsb = pp(rt, nsb, lvl)
- nsb.append("\" where \n")
-
- ind(nsb, lvl)
-
- /// here starts the body of the function =========================
- if (body.isDefined) {
-
- def isArgument(ss : String) : Boolean = {
- args.foreach(arg => {
- if(arg.id.toString.compareTo(ss) == 0)
- return true
- })
- return false
- }
-
- //we look if the outermost match refers to a parameter of the function
- //and if so we split the definition of the function
- transformGuardedMatchExpression(body.get) match {
- case mex @ MatchExpr(s, csc) if(isArgument(s.toString)) => {
- def ppc(sb: StringBuffer, p: Pattern, matchcase: MatchCase): StringBuffer = p match {
- case CaseClassPattern(bndr, ccd, subps) => {
- var buf = new StringBuffer
- buf.append("(").append(ccd.id).append(" ")
- var c = 0
- val sz = subps.size
- subps.foreach(sp => {
- buf = ppc(buf, sp, matchcase)
- if (c < sz - 1)
- buf.append(" ")
- c = c + 1
- })
- buf.append(")")
-
- bndr.foreach(b => bindersMap.update(matchcase, (b, buf.toString)))
-
- sb.append(buf.toString)
- }
- case WildcardPattern(None) => sb.append("_")
- case WildcardPattern(Some(id2)) => {
- sb.append(freshName(id2.toString))
- }
- case _ => sb.append("Pattern?")
- }
-
- var nsb = sb
- var len1 = csc.size
- var c1 = 0
-
- csc.foreach(cs => {
- nsb.append(" \"")
- nsb.append(functionName + " ")
-
- var buff = new StringBuffer
-
- args.foreach(arg => {
- if(arg.id.toString.compareTo(s.toString) == 0){
- buff = ppc(buff, cs.pattern, cs)
- }
- else
- buff.append(freshName(arg.id.toString))
- buff.append(" ")
- })
-
- if(buff.toString.charAt(0) != '_')
- nsb.append(buff.toString)
- else
- nsb.append(freshName(s.toString))
-
- nsb.append(" = ")
-
- cs.theGuard.foreach(g => {
- reporter.error("!!!!! match case has IF condition - BUG of translation if it enters here!")
- })
-
- nsb = pp(cs.rhs, nsb, lvl + 4)
-
- nsb.append("\"")
- if (c1 < len1 - 1)
- nsb.append("|")
- nsb.append("\n")
- c1 = c1 + 1
-
- bindersMap = bindersMap - cs
- })
- ind(nsb, lvl).append("\n")
- nsb
- }
- case _ => {
- nsb.append(" \"")
- nsb.append(functionName + " ")
-
- args.foreach(arg => {
- nsb.append(freshName(arg.id.toString))
- nsb.append(" ")
- })
-
- nsb.append("= \n")
- ind(nsb, lvl + 2)
- nsb.append(" ")
- pp(body.get, nsb, lvl + 2)
- ind(nsb, lvl)
- nsb.append(" \"\n")
- }
- }
- } else
- reporter.error("[unknown function implementation] " + fd)
- /// here ends the body of the function ============================
-
- //@postconditions viewed as lemmas; preconditions are integrated in the lemma statement
- //annotations should help to prove the lemma
- //// TODO : add quantifiers to lemma statement
- post.foreach(postc => {
- nsb.append("\n")
- ind(nsb, lvl)
- nsb.append("lemma " + functionName + "_postcondition [simp]: shows \"")
-
- if (pre.size > 0) {
- var l11 = pre.size
- var c2 = 0
- nsb.append("(")
- pre.foreach(prec => {
- nsb = pp(prec, nsb, lvl)
- if (c2 < l11 - 1)
- nsb.append(" \\<and> ")
- c2 = c2 + 1
- })
- nsb.append(") \\<longrightarrow> ")
- }
-
- current_res = "(" + functionName + " "
- args.foreach(arg => {
- current_res = current_res + freshName(arg.id.toString) + " "
- })
- current_res = current_res + ")"
-
- nsb = pp(postc, nsb, lvl)
- nsb.append("\"\n")
- ind(nsb, lvl)
-
- if (args.size > 0) {
- nsb.append("apply(induct_tac " + freshName(args.head.id.toString) + ")\n")
- ind(nsb, lvl)
- }
-
- nsb.append("apply(auto)\n")
- ind(nsb, lvl)
- nsb.append("done\n")
- ind(nsb, lvl)
-
- })
- currentFunction = ""
- nsb
- }
-
- case _ => sb.append("Defn?")
- }
- }
-
- //generates an isabelle file corresponding to the scala input program
- def analyse(program: Program): Unit = {
- println("here")
- val file = new FileOutputStream("isabelle_examples/translation/" + program.mainObject.id + ".thy")
- val out = new PrintStream(file)
-
- out.println(apply(program))
- reporter.info(apply(program))
- out.close()
- }
-
-}
diff --git a/src/main/scala/leon/isabelle/README b/src/main/scala/leon/isabelle/README
deleted file mode 100644
index e19286da7..000000000
--- a/src/main/scala/leon/isabelle/README
+++ /dev/null
@@ -1,56 +0,0 @@
---------------------------------------------------
-
-Ganea Octavian
-
-- translation from LEON to Isabelle
-
-
-15.05.2011:
-TODO:
-- process functions definition where wildcard '_' apears in rhs (now generates an error)
-- problems : MutuallyRecursive.scala - proof of the postcondition does not finish at apply(auto)
-- proofs at VerySimple.scala (and other files) are not working
-
-
-- do NOT work:
-
- 1) proofs of the lemmas : it just tries induction on the first argument (if it has one) and then auto
- 2) some obscure operations on sets: multisets, min , max
- 3) if on a case branch of a match: for example BSTSimple.scala:
- TriplePair(isBST0(l), isBST0(r)) match {
- case TriplePair(Triple(None(),t1,None()),Triple(None(),t2,None())) if(t1 && t2) => Triple(Some(v),true,Some(v))
- case _ => true
- }
- - translation done well, but isabelle refuses to cooperate
-
-- what works : everything else :
- 1) keywords of the variables names
- 2) mutually recursive datatypes
- 3) binders in match cases
- 4) field selector
- 5) constant functions (arrity 0)
- 6) preconditions and postconditions translated as lemmas
- 7) usage of sets and other predefined datatypes
- 8) mutally recursive functions sorted topological by their strongly connected components
- 9) duplicate function names
- 10)instanceOf
-
-
- - add primrec to SimplePatternMatching bodies - CHECKED
- - use matchToIfThenElse to handle pattern-matching with guards - CHECKED but with unexpected behaviour :
- -- match to If not working for
- size of BSTSimpler.scala (lexicographic termination order not found)
- isBST - scripting does not finish at processing function definition;
- if I add | _ => False to translation of instanceOf then it gives an error : _ => False is redundant
-
- - use SimplePatternMatching extractor to handle "simple" pattern-matching to
- avoid case expressions when it's at the top-level - CHECKED
- - compute strongly-connected components for function graphs and recursive
- data-types - CHECKED using Kosaraju's algorithm for strongly connected components
- - topological sorting on Connected components - CHECKED
- - try to run Nitpick on lemmas with bugs. - tried but nothing useful deduced
- - deal with functions with duplicate names - CHECKED (each function has its number of arguments attached)
- - add 2 test files : testcases/MutuallyRecursive.scala and testcases/ConnectedTest.scala
-
-
-
\ No newline at end of file
diff --git a/src/main/scala/leon/isabelle/StrongConnectedComponents.scala b/src/main/scala/leon/isabelle/StrongConnectedComponents.scala
deleted file mode 100644
index 497e16884..000000000
--- a/src/main/scala/leon/isabelle/StrongConnectedComponents.scala
+++ /dev/null
@@ -1,167 +0,0 @@
-package leon.isabelle
-
-import leon.Reporter
-import leon.Settings._
-
-import leon.purescala.Common.Identifier
-import leon.purescala.Definitions._
-import leon.purescala.PrettyPrinter
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
-
-import java.lang.StringBuffer
-import java.io._
-import java.util.Vector
-import scala.collection.mutable.ListMap
-
-//class to determine strongly connected components
-object StrongConnectedComponents {
- def contains(v : Vector[String] , elem : String) : Boolean = {
- for (i <- 0 until v.size)
- if(v.elementAt(i).compareTo(elem) == 0)
- return true
- return false
- }
-
-
- //returns the strongly connected components of a graph in a list - each components is a list of vertices, or a list of Strings
- /*ALGORITHM (Kosaraju):
- * # Let G be a directed graph and S be an empty stack.
- # While S does not contain all vertices:
- * Choose an arbitrary vertex v not in S. Perform a depth-first search starting at v. Each time that depth-first search
- * finishes expanding a vertex u, push u onto S.
-
- # Reverse the directions of all arcs to obtain the transpose graph.
- # While S is nonempty
- * Pop the top vertex v from S. Perform a depth-first search starting at v. The set of visited vertices will give
- * the strongly connected component containing v; record this and remove all these vertices from the graph G and
- * the stack S.
- */
-
- def dfs_firstphase(current: String, graph: ListMap[String, List[String]], stack: Vector[String], visited: Vector[String]): Unit = {
- var o = graph.get(current)
- var list = Nil: List[String]
- o match {
- case None => list = Nil: List[String]
- case Some(l) => list = l
- }
-
- visited.add(current)
-
- for(s <- list)
- if(!contains(stack, s) && !contains(visited, s))
- dfs_firstphase(s,graph,stack, visited)
-
- stack.add(current)
- }
-
- def dfs_secondphase(current: String, graph: ListMap[String, List[String]], visited: Vector[String]): Unit = {
- var o = graph.get(current)
- var list = Nil: List[String]
- o match {
- case None => list = Nil: List[String]
- case Some(l) => list = l
- }
-
- visited.add(current)
-
- for (s <- list)
- if (!contains(visited, s))
- dfs_secondphase(s, graph,visited)
- }
-
- def connectedComponents(graph : ListMap[String, List[String]]) : List[List[String]] = {
- var result = Nil : List[List[String]]
- var stack = new Vector[String]
-
- while(stack.size < graph.size){
- for(t <- graph)
- if(!contains(stack, t._1))
- dfs_firstphase(t._1, graph, stack, new Vector[String])
- }
-
- var transposeGraph = new ListMap[String, List[String]]
- graph foreach( (t) =>{
- t._2.foreach( p => {
- var o = transposeGraph.get(p)
- var list = Nil: List[String]
- o match {
- case None => list = Nil: List[String]
- case Some(l) => list = l
- }
- transposeGraph.update(p, list ::: List(t._1))
- })
- })
-
- while(stack.size > 0){
- var top = stack.remove(stack.size - 1)
- var visited = new Vector[String]
- dfs_secondphase(top, transposeGraph, visited)
- var component = Nil : List[String]
- for(i <- 0 until visited.size)
- component = component ::: List(visited.elementAt(i))
- result = result ::: List(component)
- for(el <- component){
- var index = -1
- for(i <- 0 until stack.size)
- if(stack.elementAt(i).compareTo(el) == 0)
- index = i
- if(index > -1)
- stack.remove(index)
- transposeGraph = transposeGraph - el
- transposeGraph foreach( (t) =>{
- transposeGraph.update(t._1, t._2.filter(_ != el))
- })
- }
- }
-
- topologicalSort(graph, result)
- result
- }
-
- def contains(v : List[List[String]], elem : List[String]) : Boolean = {
- for (el <- v)
- if(el.head.compareTo(elem.head) == 0 && el.size == elem.size)
- return true
- return false
- }
-
- //tests if component v1 has an edge to component v2
- def edgeTo(graph: ListMap[String, List[String]], v1 : List[String] , v2 : List[String]) : Boolean = {
- for(str1 <- v1){
- var o = graph.get(str1)
- var list = Nil: List[String]
- o match {
- case None => list = Nil: List[String]
- case Some(l) => list = l
- }
- if(list.intersect(v2).size > 0)
- return true
- }
- return false
- }
-
- //sorts the connected components in a topological sort
- def topologicalSort(graph: ListMap[String, List[String]], components: List[List[String]]): List[List[String]] = {
-
- var sortedList = Nil: List[List[String]]
- while (sortedList.size < components.size)
- for(current <- components)
- if (!contains(sortedList, current)) {
- var b = true
- for(t <- components)
- if (!contains(sortedList, t) && t != current)
- if(edgeTo(graph, t, current)){
- b = false
- }
- if (b)
- sortedList = sortedList ::: List(current)
- }
- sortedList
- }
-
- //returns the strongly connected components of the graph sorted in topological order using Kosaraju's algorithm
- def stronglyOrderedConnectedComponents(graph : ListMap[String, List[String]]) : List[List[String]] = {
- topologicalSort(graph, connectedComponents(graph))
- }
-}
--
GitLab