A.34 SOFTWARE-EVOLUTION-LIBRARY/SOFTWARE/COQ

Class: coq [sel/sw/coq]

Class precedence list: coq, sexp, simple, software, oid-object, file-w-attributes, file, standard-object, slot-object, t

Slots:

• project-file — initarg: :project-file; reader: software-evolution-library/software/coq:project-file

  Path to _CoqProject file, if it exists.

• file-source — initarg: :file-source; reader: software-evolution-library/software/coq:file-source; writer: (setf software-evolution-library/software/coq:file-source)

  Name of source file.

• imports — initarg: :imports; reader: software-evolution-library/software/coq:imports; writer: (setf software-evolution-library/software/coq:imports)

  ASTs for imports, not part of genome.

• coq-modules — initarg: :modules; reader: software-evolution-library/software/coq:coq-modules; writer: (setf software-evolution-library/software/coq:coq-modules)

  List of Modules defined by this object.

• coq-sections — initarg: :sections; reader: software-evolution-library/software/coq:coq-sections; writer: (setf software-evolution-library/software/coq:coq-sections)

  List of Sections defined by this object.

• coq-assumptions — initarg: :assumptions; reader: software-evolution-library/software/coq:coq-assumptions; writer: (setf software-evolution-library/software/coq:coq-assumptions)

  List of Parameters, Variables, etc. defined by this object.

• coq-definitions — initarg: :definitions; reader: software-evolution-library/software/coq:coq-definitions; writer: (setf software-evolution-library/software/coq:coq-definitions)

  List of values defined in this object. Includes Definition, Inductive, Fixpoint, etc.

Coq software object.

Generic Function: coq-type-checks [sel/sw/coq] coq

Return the fraction of ASTs in coq software object that typecheck.

Method: coq-type-checks [sel/sw/coq] (obj coq)

Return the fraction of ASTs in Coq software obj that typecheck. Return nil if source strings cannot be looked up.

Class: type-safe-swap [sel/sw/coq]

Class precedence list: type-safe-swap, sexp-swap, mutation, oid-object, standard-object, slot-object, t

Slots:

• targeter — initarg: :targeter; reader: software-evolution-library/software-evolution-library:targeter

  A function from software -> targets.

• picker — initarg: :picker; reader: software-evolution-library/software-evolution-library:picker

  A function from software -> random target.

Swap two Coq ASTs tagged with the same type.

Variable: *coq-mutation-types* [sel/sw/coq]

Cumulative distribution fo normalized probabilities of weighted mutations.

Function: find-nearest-type [sel/sw/coq] coq index

For object coq, find the nearest tag for the subtree at index in the genome. Search by checking the first element of subtrees, moving forward from index if needed. If the end of the genome is reached, search backward instead.

Function: load-coq-object [sel/sw/coq] coq &key include-imports num-asts

Load the first num-asts ASTs of the coq genome. If num-asts is nil, load all ASTs. include-imports (default T) specifies that imports should be loaded first.

Generic Function: lookup-source-strings [sel/sw/coq] software &key include-imports

Return a list of source strings for the ASTs in software. Set include-imports to t to include import statements in the result.

Method: lookup-source-strings [sel/sw/coq] (obj coq) &key include-imports

Return a list of source strings for the ASTs in coq. Set include-imports to t to include import statements in the result.

Function: pick-subtree-matching-type [sel/sw/coq] coq type ignore-index

For object coq, randomly select the index of a subtree tagged as type. Ensure that the selected index is not equal to ignore-index.

• coq - a Coq software object.
• type - a symbol indicating the type tag to be matched.
• ignore-index - the index of a subtree tagged as type which is not to be

selected.

Generic Function: reset-and-load-imports [sel/sw/coq] coq &key imports

Reset the SerAPI process and load imports for coq software object.

Method: reset-and-load-imports [sel/sw/coq] (project coq-project) &key imports

Reset the SerAPI process and load imports for each Coq object in project. If imports is nil, it defaults to the list of ‘imports’ for each Coq object in project.

Method: reset-and-load-imports [sel/sw/coq] (obj coq) &key (imports (imports obj))

Reset the SerAPI process and load imports for coq software object. imports defaults to the list of ‘imports’ in coq.

Function: synthesize-typed-coq-expression [sel/sw/coq] type scopes depth

Synthesize an expression of type type using in-scope values scopes. Return a list of strings representing Coq expressions of type type. type is a string denoting a Coq type (e.g., "nat -> bool"). scopes is a list of variables with tokenized types (e.g., as generated by ‘search-coq-type’). depth is a number limiting the search depth. Functions will be applied to no more than depth parameters.

Function: tag-loc-info [sel/sw/coq] sexpr

Return sexpr with Coq location info replaced by ‘(:loc NIL)’. See also ‘is-loc-info’ and ‘untag-loc-info’.

Function: untag-loc-info [sel/sw/coq] sexpr

Return sexpr with occurrences of ‘(:loc NIL)’ replaced by nil. See also ‘tag-loc-info’.