pkg/kernel/lib/transformations/coq.dart - sdk.git - Git at Google

 // Copyright (c) 2017, the Dart project authors.  Please see the AUTHORS file
 // for details. All rights reserved. Use of this source code is governed by a
 // BSD-style license that can be found in the LICENSE file.
 //
 // This transformations outputs a Coq definitions to resemble the Dart syntax
 // tree.
 //
 // Classes that are supposed to be converted are marked with the `@coq`
 // annotation. Some fields within these classes will be converted according to
 // the following rules:
 //
 // 1. A field labeled `@nocoq` will not be converted.
 //
 // 2. A field labeled `@coq` or `@coqopt` will be converted unless it's type is
 // unuspported, in which case an exception will be raised.
 //
 // 3. An unannotated field will be converted if it has type `T` or `List<T>`,
 // where `T` is a class marked for conversion.
 //
 // Classes marked `@coqref` are referenced by natural numbered IDs wherever
 // fields of their type appear, and we have a finite map resolving these IDs.
 // This breaks cycles in the AST graph and provides a way to identify nodes for
 // substitution.
 //
 // All classes with data members are given an induction type definition with a
 // single constructor, holding the data members of that class. Classes with
 // subclasses are also given an inductive definition enumerating all (converted)
 // subclasses. Their data-member type definition will appear inline in the data
 // member definitions for their leaf subclasses. Due to this representation,
 // converted classes with subclasses must be abstract.
 //
 // Since the whole syntax tree is mutually recursive, all the types are dumped
 // into one big "Inductive ... with ... with ... " definition.

 library kernel.transformations.coq;

 import 'dart:io';
 import '../ast.dart';
 import '../coq_annot.dart' as coq_annot;
 import '../core_types.dart' show CoreTypes;

 enum RefStyle { direct, identified }

 enum FieldStyle { list, optional, normal }

 class CoqFieldInfo {
   // Only one of these two may be non-null.
   final CoqClassInfo type;
   final String primitiveCoqType;

   final String dartName;
   final FieldStyle style;
   bool definitional = false;

   String get innerRefType => type == null ? primitiveCoqType : type.refType;

   String get refType {
     if (type != null) {
       var rt = definitional ? type.coqType : type.refType;
       if (style == FieldStyle.list) {
         return "list $rt";
       } else if (style == FieldStyle.optional) {
         return "option $rt";
       } else {
         return rt;
       }
     } else {
       if (style == FieldStyle.list) {
         return "list " + primitiveCoqType;
       } else if (style == FieldStyle.optional) {
         return "option " + primitiveCoqType;
       } else {
         return primitiveCoqType;
       }
     }
   }

   CoqFieldInfo(this.dartName, this.type, this.primitiveCoqType, this.style);
 }

 class CoqClassInfo {
   final Class cls;
   final RefStyle refStyle;

   List<CoqClassInfo> subs = <CoqClassInfo>[];
   List<CoqFieldInfo> fields = <CoqFieldInfo>[];

   bool needsOption = false;
   bool needsList = false;

   String get coqType => coqifyName(cls.name);
   String get coqTypeCaps => coqifyName(cls.name, capitalize: true);
   String get abbrevName => abbrev(cls.name);
   String get abbrevNameCaps => abbrev(cls.name, capitalize: true);
   String get refType => refStyle == RefStyle.direct ? coqType : "nat";

   CoqClassInfo(this.cls, this.refStyle);

   Iterable<CoqClassInfo> supersWithData(CoqLibInfo info) sync* {
     for (Supertype st = cls.supertype;
         st != null;
         st = st.classNode.supertype) {
       Class spr = st.classNode;
       var sprInfo = info.classes[spr];
       if (sprInfo == null) break;
       if (sprInfo.fields.length == 0) continue;
       yield sprInfo;
     }
   }
 }

 class CoqLibInfo {
   final Map<Class, CoqClassInfo> classes = <Class, CoqClassInfo>{};
   CoqLibInfo();
 }

 // Get the number associated with the annotation from `coq_annot.dart` on a
 // [Field] or [Class] if one exists, and 0 otherwise. Throws an exception if
 // invalid or multiple annotations are discoverted.
 int getCoqAnnot(NamedNode N, List<Expression> annotations) {
   if (coq_annot.coqEnums.contains("$N")) {
     return coq_annot.coq;
   }

   int annot = 0;
   for (var A in annotations) {
     if (A is StaticGet) {
       var target = A.targetReference.node;
       var parent = target.parent;
       if (parent is Library) {
         if (parent is NamedNode && parent.name == "kernel.coq_annot") {
           if (target is Field) {
             if (annot != 0) {
               throw new Exception("ERROR: Multiple Coq annotations on ${N}!");
             }
             switch ("${target.name}") {
               case "coq":
                 annot = coq_annot.coq;
                 break;
               case "coqref":
                 annot = coq_annot.coqref;
                 break;
               case "nocoq":
                 annot = coq_annot.nocoq;
                 break;
               case "coqopt":
                 annot = coq_annot.coqopt;
                 break;
               case "coqsingle":
                 annot = coq_annot.coqsingle;
                 break;
               case "coqdef":
                 annot = coq_annot.coqdef;
                 break;
               case "coqsingledef":
                 annot = coq_annot.coqsingledef;
                 break;
               default:
                 throw new Exception("ERROR: Invalid Coq annotation on ${N}!");
             }
           } else {
             throw new Exception("ERROR: Invalid Coq annotation on ${N}!");
           }
         }
       }
     }
   }
   return annot;
 }

 // Determine which classes we're going to convert.
 class CoqPass1 extends RecursiveVisitor {
   CoqLibInfo info;
   CoqPass1(this.info);

   visitClass(Class C) {
     int annot = getCoqAnnot(C, C.annotations);
     if (annot == 0) return;

     if (annot != coq_annot.coq && annot != coq_annot.coqref) {
       throw new Exception("ERROR: Invalid Coq annotation on ${C.name}!");
     }

     info.classes[C] = new CoqClassInfo(
         C, annot == coq_annot.coq ? RefStyle.direct : RefStyle.identified);
   }
 }

 // Determine which fields we're going to convert and which classes have
 // converted subclasses.
 class CoqPass2 extends RecursiveVisitor {
   CoqLibInfo info;
   CoreTypes coreTypes;
   CoqPass2(this.info, this.coreTypes);

   CoqClassInfo currentClass = null;

   String getCoqPrimitiveType(Class cls) {
     if (cls == coreTypes.stringClass) {
       return "string";
     } else if (cls == coreTypes.boolClass) {
       return "bool";
     } else if (cls == coreTypes.intClass) {
       return "nat";
     } else {
       return null;
     }
   }

   visitClass(Class C) {
     var classInfo = info.classes[C];
     if (classInfo == null) return;

     if (C.supertype != null) {
       Class spr = C.supertype.classNode;
       var sprInfo = info.classes[spr];
       if (sprInfo != null) {
         sprInfo.subs.add(classInfo);
       }
     }

     currentClass = classInfo;
     C.visitChildren(this);
     currentClass = null;
   }

   visitField(Field F) {
     if (currentClass == null) return;

     int annot = getCoqAnnot(F, F.annotations);
     if (annot == coq_annot.nocoq) return;

     var type = F.type;
     if (type is! InterfaceType) return;

     var interfaceType = type as InterfaceType;

     var cls = null;
     bool isList = false;

     if (interfaceType.classNode == coreTypes.listClass) {
       isList = annot != coq_annot.coqsingle && annot != coq_annot.coqsingledef;
       if (interfaceType.typeArguments.length != 1) return;
       var elemType = interfaceType.typeArguments[0];
       if (elemType is InterfaceType) {
         cls = elemType.classNode;
       } else if (annot == coq_annot.coqopt) {
         throw new Exception("ERROR: Field $F may not be optional.");
       }
     } else {
       cls = interfaceType.classNode;
     }

     FieldStyle style = isList
         ? FieldStyle.list
         : (annot == coq_annot.coqopt ? FieldStyle.optional : FieldStyle.normal);

     CoqFieldInfo fieldInfo = null;
     var primitive = getCoqPrimitiveType(cls);
     var fieldName = F.name.name;

     if (primitive != null) {
       if (annot == 0) return;
       fieldInfo = new CoqFieldInfo(fieldName, null, primitive, style);
     } else {
       var fieldClassInfo = info.classes[cls];
       if (fieldClassInfo == null) {
         return;
       }
       fieldInfo = new CoqFieldInfo(fieldName, fieldClassInfo, null, style);

       if (style == FieldStyle.optional) {
         fieldClassInfo.needsOption = true;
       } else if (style == FieldStyle.list) {
         fieldClassInfo.needsList = true;
       }

       if (annot == coq_annot.coqdef || annot == coq_annot.coqsingledef) {
         fieldInfo.definitional = true;
       }
     }

     currentClass.fields.add(fieldInfo);
   }
 }

 // Conventional Coq code uses underscores instead of camelCase as Dart code
 // does. This function converts the Dart convention to the Coq convention.
 final coqReserved = <String>["let"];
 String coqifyName(String S, {bool capitalize: false}) {
   List<int> codes = <int>[];
   bool skipUnderscore = false;
   for (int i = 0; i < S.length; ++i) {
     var c = S.codeUnitAt(i);
     if (c >= "A".codeUnits[0] && c <= "Z".codeUnits[0]) {
       if (i > 0 && !skipUnderscore) {
         codes.add("_".codeUnitAt(0));
       }
       if (!capitalize) c += ("a".codeUnits[0] - "A".codeUnits[0]);
       codes.add(c);
     } else {
       codes.add(c);
     }
     skipUnderscore = c == "_".codeUnits[0];
   }
   var name = new String.fromCharCodes(codes);
   if (coqReserved.contains(name)) {
     name = "dart_" + name;
   }
   return name;
 }

 // Give an abbreviation of a identifying by combining the capital letters of the
 // identifier. For example, "ProcedureKind" becomes "pk" or "PK".
 String abbrev(String S, {bool capitalize: false}) {
   List<int> codes = <int>[];
   for (var c in S.codeUnits)
     if (c >= 65 && c <= 90) codes.add(capitalize ? c : c + 32);
   return new String.fromCharCodes(codes);
 }

 void outputCoqImports() {
   print("""
 Require Import Common.
 """);
 }

 void outputCoqSyntax(CoqLibInfo info) {
   int defN = 0;
   defkw() => defN++ > 0 ? "with" : "Inductive";
   for (var classInfo in info.classes.values) {
     bool isAbstract = classInfo.subs.length > 0;

     Class cls = classInfo.cls;
     var coqName = classInfo.coqType;

     if (classInfo.cls.isEnum) {
       var enums = [];
       for (var fld in classInfo.fields) {
         if (fld.dartName == "values") continue;
         enums.add(coqifyName(fld.dartName, capitalize: true));
       }
       print("${defkw()} $coqName : Set := ${enums.join(" | ")}\n");
       continue;
     }

     if (!isAbstract || classInfo.fields.length > 0) {
       var suffix = isAbstract ? "_data" : "";
       var dataTypeName = coqName + suffix;
       var dataCtorName = coqifyName(cls.name, capitalize: true);

       print("${defkw()} ${dataTypeName} : Set :=");
       print("  | ${dataCtorName} : ");

       // Insert fields for superclasses.
       int arw = 0;
       arrow() => arw++ == 0 ? "" : "-> ";

       if (classInfo.refStyle == RefStyle.identified) {
         print("      ${arrow()}nat");
       }

       for (var sprInfo in classInfo.supersWithData(info)) {
         print("      ${arrow()}${sprInfo.coqType}_data");
       }

       for (CoqFieldInfo fld in classInfo.fields) {
         print("      ${arrow()}${fld.refType} (* ${fld.dartName} *)");
       }

       print("      ${arrow()}$dataTypeName\n");
     }

     if (classInfo.subs.length > 0) {
       print("${defkw()} $coqName : Set :=");

       var abbrevName = abbrev(cls.name, capitalize: true);
       for (var sub in classInfo.subs) {
         var subTypeName = coqifyName(sub.cls.name);
         var ctorName = coqifyName(sub.cls.name, capitalize: true);
         print("  | ${abbrevName}_${ctorName} : ${subTypeName} -> $coqName");
       }

       print("\n");
     }
   }
   print(".\n");
 }

 void outputCoqStore(info) {
   print("Record ast_store : Type := Ast_Store {");
   for (var classInfo in info.classes.values) {
     if (classInfo.refStyle != RefStyle.identified) continue;
     print("  ${classInfo.abbrevName}_refs : NatMap.t ${classInfo.coqType};");
   }
   print("}.\n");
 }

 void outputCoqSyntaxValidity(CoqLibInfo info) {
   int defN = 0;
   defkw() => defN++ > 0 ? "with" : "Fixpoint";

   validityPredicate(CoqClassInfo CI) {
     if (CI.refStyle == RefStyle.identified) {
       var mapName = "${CI.abbrevName}_refs";
       return (X) => "NatMap.In $X ($mapName ast)";
     } else {
       return (X) => "${CI.coqType}_validity ast $X";
     }
   }

   for (var CI in info.classes.values) {
     stdout.write(
         "${defkw()} ${CI.coqType}_validity (ast : ast_store) (T : ${CI.coqType}) {struct T} : Prop :=");
     if (CI.cls.isEnum) {
       stdout.write(" True\n");
       continue;
     } else {
       stdout.write("\n");
     }

     print("  match T with");
     for (var sub in CI.subs) {
       print(
           "    | ${CI.abbrevNameCaps}_${sub.coqTypeCaps} ST => ${sub.coqType}_validity ast ST");
     }

     if (CI.subs.length > 0) {
       print("end");
       if (CI.fields.length == 0) continue;
       print(
           "${defkw()} ${CI.coqType}_data_validity (ast : ast_store) (T : ${CI.coqType}_data) {struct T}: Prop :=");
       print("  match T with");
     }

     int i = 0;
     var fieldNames = [];
     var validityClauses = [];

     for (var SI in CI.supersWithData(info)) {
       var f = "f${i++}";
       fieldNames.add(f);
       validityClauses.add("${SI.coqType}_data_validity ast $f");
     }

     for (var fld in CI.fields) {
       if (fld.type == null) {
         fieldNames.add("_");
         continue;
       }

       var f = "f${i++}";
       fieldNames.add(f);

       var pred;
       if (fld.style == FieldStyle.normal) {
         pred = validityPredicate(fld.type)(f);
       } else if (fld.style == FieldStyle.list) {
         pred = "${fld.type.coqType}_list_validity ast $f";
       } else if (fld.style == FieldStyle.optional) {
         pred = "${fld.type.coqType}_option_validity ast $f";
       }

       validityClauses.add(pred);
     }

     var clause = "True";
     if (validityClauses.length > 0) {
       clause = validityClauses.join(" /\\\n        ");
     }

     print(
         "    | ${CI.coqTypeCaps} ${fieldNames.join(" ")} =>\n        $clause");
     print("  end");
   }

   for (var CI in info.classes.values) {
     var pred = validityPredicate(CI)("X");
     if (CI.needsList) {
       var def = """
 with ${CI.coqType}_list_validity (ast : ast_store) (L : ${CI.coqType}_list) {struct L} : Prop :=
   match L with
     | ${CI.coqType}_nil => True
     | ${CI.coqType}_cons X XS => $pred /\\ ${CI.coqType}_list_validity ast XS
   end""";
       print(def);
     }
     if (CI.needsOption) {
       var def = """
 with ${CI.coqType}_option_validity (ast : ast_store) (O : ${CI.coqType}_option) {struct O} : Prop :=
   match O with
     | ${CI.coqType}_none => True
     | ${CI.coqType}_some X => $pred
   end""";
       print(def);
     }
   }

   print(".\n");
 }

 void outputCoqStoreValidity(CoqLibInfo info) {
   var clauses = [];
   for (var CI in info.classes.values) {
     if (CI.refStyle != RefStyle.identified) continue;
     var mapName = "${CI.abbrevName}_refs";
     clauses.add(
         "  forall (n : nat), forall (X : ${CI.coqType}), NatMap.MapsTo n X ($mapName ast) -> ${CI.coqType}_validity ast X");
   }
   var clause = clauses.join(" /\\\n");
   print(
       "Definition ast_store_validity (ast : ast_store) : Prop := \n$clause\n.");
 }

 Component transformComponent(CoreTypes coreTypes, Component component) {
   for (Library lib in component.libraries) {
     // TODO(30610): Ideally we'd output to the file in the coq annotation on the
     // library name, but currently fasta throws away annotations on libraries.
     // Instead, we just special case "kernel.ast" and output to stdout.
     if ("$lib" != "kernel.ast") continue;
     var info = new CoqLibInfo();
     (new CoqPass1(info)).visitLibrary(lib);
     (new CoqPass2(info, coreTypes)).visitLibrary(lib);
     outputCoqImports();
     outputCoqSyntax(info);
   }
   return component;
 }
	// Copyright (c) 2017, the Dart project authors. Please see the AUTHORS file
	// for details. All rights reserved. Use of this source code is governed by a
	// BSD-style license that can be found in the LICENSE file.
	//
	// This transformations outputs a Coq definitions to resemble the Dart syntax
	// tree.
	//
	// Classes that are supposed to be converted are marked with the `@coq`
	// annotation. Some fields within these classes will be converted according to
	// the following rules:
	//
	// 1. A field labeled `@nocoq` will not be converted.
	//
	// 2. A field labeled `@coq` or `@coqopt` will be converted unless it's type is
	// unuspported, in which case an exception will be raised.
	//
	// 3. An unannotated field will be converted if it has type `T` or `List<T>`,
	// where `T` is a class marked for conversion.
	//
	// Classes marked `@coqref` are referenced by natural numbered IDs wherever
	// fields of their type appear, and we have a finite map resolving these IDs.
	// This breaks cycles in the AST graph and provides a way to identify nodes for
	// substitution.
	//
	// All classes with data members are given an induction type definition with a
	// single constructor, holding the data members of that class. Classes with
	// subclasses are also given an inductive definition enumerating all (converted)
	// subclasses. Their data-member type definition will appear inline in the data
	// member definitions for their leaf subclasses. Due to this representation,
	// converted classes with subclasses must be abstract.
	//
	// Since the whole syntax tree is mutually recursive, all the types are dumped
	// into one big "Inductive ... with ... with ... " definition.

	library kernel.transformations.coq;

	import 'dart:io';
	import '../ast.dart';
	import '../coq_annot.dart' as coq_annot;
	import '../core_types.dart' show CoreTypes;

	enum RefStyle { direct, identified }

	enum FieldStyle { list, optional, normal }

	class CoqFieldInfo {
	// Only one of these two may be non-null.
	final CoqClassInfo type;
	final String primitiveCoqType;

	final String dartName;
	final FieldStyle style;
	bool definitional = false;

	String get innerRefType => type == null ? primitiveCoqType : type.refType;

	String get refType {
	if (type != null) {
	var rt = definitional ? type.coqType : type.refType;
	if (style == FieldStyle.list) {
	return "list $rt";
	} else if (style == FieldStyle.optional) {
	return "option $rt";
	} else {
	return rt;
	}
	} else {
	if (style == FieldStyle.list) {
	return "list " + primitiveCoqType;
	} else if (style == FieldStyle.optional) {
	return "option " + primitiveCoqType;
	} else {
	return primitiveCoqType;
	}
	}
	}

	CoqFieldInfo(this.dartName, this.type, this.primitiveCoqType, this.style);
	}

	class CoqClassInfo {
	final Class cls;
	final RefStyle refStyle;

	List<CoqClassInfo> subs = <CoqClassInfo>[];
	List<CoqFieldInfo> fields = <CoqFieldInfo>[];

	bool needsOption = false;
	bool needsList = false;

	String get coqType => coqifyName(cls.name);
	String get coqTypeCaps => coqifyName(cls.name, capitalize: true);
	String get abbrevName => abbrev(cls.name);
	String get abbrevNameCaps => abbrev(cls.name, capitalize: true);
	String get refType => refStyle == RefStyle.direct ? coqType : "nat";

	CoqClassInfo(this.cls, this.refStyle);

	Iterable<CoqClassInfo> supersWithData(CoqLibInfo info) sync* {
	for (Supertype st = cls.supertype;
	st != null;
	st = st.classNode.supertype) {
	Class spr = st.classNode;
	var sprInfo = info.classes[spr];
	if (sprInfo == null) break;
	if (sprInfo.fields.length == 0) continue;
	yield sprInfo;
	}
	}
	}

	class CoqLibInfo {
	final Map<Class, CoqClassInfo> classes = <Class, CoqClassInfo>{};
	CoqLibInfo();
	}

	// Get the number associated with the annotation from `coq_annot.dart` on a
	// [Field] or [Class] if one exists, and 0 otherwise. Throws an exception if
	// invalid or multiple annotations are discoverted.
	int getCoqAnnot(NamedNode N, List<Expression> annotations) {
	if (coq_annot.coqEnums.contains("$N")) {
	return coq_annot.coq;
	}

	int annot = 0;
	for (var A in annotations) {
	if (A is StaticGet) {
	var target = A.targetReference.node;
	var parent = target.parent;
	if (parent is Library) {
	if (parent is NamedNode && parent.name == "kernel.coq_annot") {
	if (target is Field) {
	if (annot != 0) {
	throw new Exception("ERROR: Multiple Coq annotations on ${N}!");
	}
	switch ("${target.name}") {
	case "coq":
	annot = coq_annot.coq;
	break;
	case "coqref":
	annot = coq_annot.coqref;
	break;
	case "nocoq":
	annot = coq_annot.nocoq;
	break;
	case "coqopt":
	annot = coq_annot.coqopt;
	break;
	case "coqsingle":
	annot = coq_annot.coqsingle;
	break;
	case "coqdef":
	annot = coq_annot.coqdef;
	break;
	case "coqsingledef":
	annot = coq_annot.coqsingledef;
	break;
	default:
	throw new Exception("ERROR: Invalid Coq annotation on ${N}!");
	}
	} else {
	throw new Exception("ERROR: Invalid Coq annotation on ${N}!");
	}
	}
	}
	}
	}
	return annot;
	}

	// Determine which classes we're going to convert.
	class CoqPass1 extends RecursiveVisitor {
	CoqLibInfo info;
	CoqPass1(this.info);

	visitClass(Class C) {
	int annot = getCoqAnnot(C, C.annotations);
	if (annot == 0) return;

	if (annot != coq_annot.coq && annot != coq_annot.coqref) {
	throw new Exception("ERROR: Invalid Coq annotation on ${C.name}!");
	}

	info.classes[C] = new CoqClassInfo(
	C, annot == coq_annot.coq ? RefStyle.direct : RefStyle.identified);
	}
	}

	// Determine which fields we're going to convert and which classes have
	// converted subclasses.
	class CoqPass2 extends RecursiveVisitor {
	CoqLibInfo info;
	CoreTypes coreTypes;
	CoqPass2(this.info, this.coreTypes);

	CoqClassInfo currentClass = null;

	String getCoqPrimitiveType(Class cls) {
	if (cls == coreTypes.stringClass) {
	return "string";
	} else if (cls == coreTypes.boolClass) {
	return "bool";
	} else if (cls == coreTypes.intClass) {
	return "nat";
	} else {
	return null;
	}
	}

	visitClass(Class C) {
	var classInfo = info.classes[C];
	if (classInfo == null) return;

	if (C.supertype != null) {
	Class spr = C.supertype.classNode;
	var sprInfo = info.classes[spr];
	if (sprInfo != null) {
	sprInfo.subs.add(classInfo);
	}
	}

	currentClass = classInfo;
	C.visitChildren(this);
	currentClass = null;
	}

	visitField(Field F) {
	if (currentClass == null) return;

	int annot = getCoqAnnot(F, F.annotations);
	if (annot == coq_annot.nocoq) return;

	var type = F.type;
	if (type is! InterfaceType) return;

	var interfaceType = type as InterfaceType;

	var cls = null;
	bool isList = false;

	if (interfaceType.classNode == coreTypes.listClass) {
	isList = annot != coq_annot.coqsingle && annot != coq_annot.coqsingledef;
	if (interfaceType.typeArguments.length != 1) return;
	var elemType = interfaceType.typeArguments[0];
	if (elemType is InterfaceType) {
	cls = elemType.classNode;
	} else if (annot == coq_annot.coqopt) {
	throw new Exception("ERROR: Field $F may not be optional.");
	}
	} else {
	cls = interfaceType.classNode;
	}

	FieldStyle style = isList
	? FieldStyle.list
	: (annot == coq_annot.coqopt ? FieldStyle.optional : FieldStyle.normal);

	CoqFieldInfo fieldInfo = null;
	var primitive = getCoqPrimitiveType(cls);
	var fieldName = F.name.name;

	if (primitive != null) {
	if (annot == 0) return;
	fieldInfo = new CoqFieldInfo(fieldName, null, primitive, style);
	} else {
	var fieldClassInfo = info.classes[cls];
	if (fieldClassInfo == null) {
	return;
	}
	fieldInfo = new CoqFieldInfo(fieldName, fieldClassInfo, null, style);

	if (style == FieldStyle.optional) {
	fieldClassInfo.needsOption = true;
	} else if (style == FieldStyle.list) {
	fieldClassInfo.needsList = true;
	}

	if (annot == coq_annot.coqdef \|\| annot == coq_annot.coqsingledef) {
	fieldInfo.definitional = true;
	}
	}

	currentClass.fields.add(fieldInfo);
	}
	}

	// Conventional Coq code uses underscores instead of camelCase as Dart code
	// does. This function converts the Dart convention to the Coq convention.
	final coqReserved = <String>["let"];
	String coqifyName(String S, {bool capitalize: false}) {
	List<int> codes = <int>[];
	bool skipUnderscore = false;
	for (int i = 0; i < S.length; ++i) {
	var c = S.codeUnitAt(i);
	if (c >= "A".codeUnits[0] && c <= "Z".codeUnits[0]) {
	if (i > 0 && !skipUnderscore) {
	codes.add("_".codeUnitAt(0));
	}
	if (!capitalize) c += ("a".codeUnits[0] - "A".codeUnits[0]);
	codes.add(c);
	} else {
	codes.add(c);
	}
	skipUnderscore = c == "_".codeUnits[0];
	}
	var name = new String.fromCharCodes(codes);
	if (coqReserved.contains(name)) {
	name = "dart_" + name;
	}
	return name;
	}

	// Give an abbreviation of a identifying by combining the capital letters of the
	// identifier. For example, "ProcedureKind" becomes "pk" or "PK".
	String abbrev(String S, {bool capitalize: false}) {
	List<int> codes = <int>[];
	for (var c in S.codeUnits)
	if (c >= 65 && c <= 90) codes.add(capitalize ? c : c + 32);
	return new String.fromCharCodes(codes);
	}

	void outputCoqImports() {
	print("""
	Require Import Common.
	""");
	}

	void outputCoqSyntax(CoqLibInfo info) {
	int defN = 0;
	defkw() => defN++ > 0 ? "with" : "Inductive";
	for (var classInfo in info.classes.values) {
	bool isAbstract = classInfo.subs.length > 0;

	Class cls = classInfo.cls;
	var coqName = classInfo.coqType;

	if (classInfo.cls.isEnum) {
	var enums = [];
	for (var fld in classInfo.fields) {
	if (fld.dartName == "values") continue;
	enums.add(coqifyName(fld.dartName, capitalize: true));
	}
	print("${defkw()} $coqName : Set := ${enums.join(" \| ")}\n");
	continue;
	}

	if (!isAbstract \|\| classInfo.fields.length > 0) {
	var suffix = isAbstract ? "_data" : "";
	var dataTypeName = coqName + suffix;
	var dataCtorName = coqifyName(cls.name, capitalize: true);

	print("${defkw()} ${dataTypeName} : Set :=");
	print(" \| ${dataCtorName} : ");

	// Insert fields for superclasses.
	int arw = 0;
	arrow() => arw++ == 0 ? "" : "-> ";

	if (classInfo.refStyle == RefStyle.identified) {
	print(" ${arrow()}nat");
	}

	for (var sprInfo in classInfo.supersWithData(info)) {
	print(" ${arrow()}${sprInfo.coqType}_data");
	}

	for (CoqFieldInfo fld in classInfo.fields) {
	print(" ${arrow()}${fld.refType} (* ${fld.dartName} *)");
	}

	print(" ${arrow()}$dataTypeName\n");
	}

	if (classInfo.subs.length > 0) {
	print("${defkw()} $coqName : Set :=");

	var abbrevName = abbrev(cls.name, capitalize: true);
	for (var sub in classInfo.subs) {
	var subTypeName = coqifyName(sub.cls.name);
	var ctorName = coqifyName(sub.cls.name, capitalize: true);
	print(" \| ${abbrevName}_${ctorName} : ${subTypeName} -> $coqName");
	}

	print("\n");
	}
	}
	print(".\n");
	}

	void outputCoqStore(info) {
	print("Record ast_store : Type := Ast_Store {");
	for (var classInfo in info.classes.values) {
	if (classInfo.refStyle != RefStyle.identified) continue;
	print(" ${classInfo.abbrevName}_refs : NatMap.t ${classInfo.coqType};");
	}
	print("}.\n");
	}

	void outputCoqSyntaxValidity(CoqLibInfo info) {
	int defN = 0;
	defkw() => defN++ > 0 ? "with" : "Fixpoint";

	validityPredicate(CoqClassInfo CI) {
	if (CI.refStyle == RefStyle.identified) {
	var mapName = "${CI.abbrevName}_refs";
	return (X) => "NatMap.In $X ($mapName ast)";
	} else {
	return (X) => "${CI.coqType}_validity ast $X";
	}
	}

	for (var CI in info.classes.values) {
	stdout.write(
	"${defkw()} ${CI.coqType}_validity (ast : ast_store) (T : ${CI.coqType}) {struct T} : Prop :=");
	if (CI.cls.isEnum) {
	stdout.write(" True\n");
	continue;
	} else {
	stdout.write("\n");
	}

	print(" match T with");
	for (var sub in CI.subs) {
	print(
	" \| ${CI.abbrevNameCaps}_${sub.coqTypeCaps} ST => ${sub.coqType}_validity ast ST");
	}

	if (CI.subs.length > 0) {
	print("end");
	if (CI.fields.length == 0) continue;
	print(
	"${defkw()} ${CI.coqType}_data_validity (ast : ast_store) (T : ${CI.coqType}_data) {struct T}: Prop :=");
	print(" match T with");
	}

	int i = 0;
	var fieldNames = [];
	var validityClauses = [];

	for (var SI in CI.supersWithData(info)) {
	var f = "f${i++}";
	fieldNames.add(f);
	validityClauses.add("${SI.coqType}_data_validity ast $f");
	}

	for (var fld in CI.fields) {
	if (fld.type == null) {
	fieldNames.add("_");
	continue;
	}

	var f = "f${i++}";
	fieldNames.add(f);

	var pred;
	if (fld.style == FieldStyle.normal) {
	pred = validityPredicate(fld.type)(f);
	} else if (fld.style == FieldStyle.list) {
	pred = "${fld.type.coqType}_list_validity ast $f";
	} else if (fld.style == FieldStyle.optional) {
	pred = "${fld.type.coqType}_option_validity ast $f";
	}

	validityClauses.add(pred);
	}

	var clause = "True";
	if (validityClauses.length > 0) {
	clause = validityClauses.join(" /\\\n ");
	}

	print(
	" \| ${CI.coqTypeCaps} ${fieldNames.join(" ")} =>\n $clause");
	print(" end");
	}

	for (var CI in info.classes.values) {
	var pred = validityPredicate(CI)("X");
	if (CI.needsList) {
	var def = """
	with ${CI.coqType}_list_validity (ast : ast_store) (L : ${CI.coqType}_list) {struct L} : Prop :=
	match L with
	\| ${CI.coqType}_nil => True
	\| ${CI.coqType}_cons X XS => $pred /\\ ${CI.coqType}_list_validity ast XS
	end""";
	print(def);
	}
	if (CI.needsOption) {
	var def = """
	with ${CI.coqType}_option_validity (ast : ast_store) (O : ${CI.coqType}_option) {struct O} : Prop :=
	match O with
	\| ${CI.coqType}_none => True
	\| ${CI.coqType}_some X => $pred
	end""";
	print(def);
	}
	}

	print(".\n");
	}

	void outputCoqStoreValidity(CoqLibInfo info) {
	var clauses = [];
	for (var CI in info.classes.values) {
	if (CI.refStyle != RefStyle.identified) continue;
	var mapName = "${CI.abbrevName}_refs";
	clauses.add(
	" forall (n : nat), forall (X : ${CI.coqType}), NatMap.MapsTo n X ($mapName ast) -> ${CI.coqType}_validity ast X");
	}
	var clause = clauses.join(" /\\\n");
	print(
	"Definition ast_store_validity (ast : ast_store) : Prop := \n$clause\n.");
	}

	Component transformComponent(CoreTypes coreTypes, Component component) {
	for (Library lib in component.libraries) {
	// TODO(30610): Ideally we'd output to the file in the coq annotation on the
	// library name, but currently fasta throws away annotations on libraries.
	// Instead, we just special case "kernel.ast" and output to stdout.
	if ("$lib" != "kernel.ast") continue;
	var info = new CoqLibInfo();
	(new CoqPass1(info)).visitLibrary(lib);
	(new CoqPass2(info, coreTypes)).visitLibrary(lib);
	outputCoqImports();
	outputCoqSyntax(info);
	}
	return component;
	}