This file summaries what has been done in each branch of the experiments on HB (available in a fork of the hierarchy-builder repository.

16/04/2024

• proto-coercion:

  • declares the constructor of the class as an elpi coercion, using elaborate-skeleton to fill in the holes
  • declares the sort projection as an elpi coercion when there is no coercion target
  • declares axioms_ as a typeclass (enables inference in the first coercion)

• coercion-tc:

  • see proto-coercion
  • declares a tactic done_tc := trivial || apply _ || done
  • turns a term T into an elpi clause that looks for an instance of a class C by applying T, unifying the type of T with the expected parameters and filling the holes with done_tc
  • declares instances through elpi’s typeclasses instead of coq’s canonical structures
  • declares the “generic” constant as a canonical structure
  • declares axioms_ in Prop whenever every field is in Prop
  • Euh, I do not know what declare-auto-infer-params-abbrev and mk-infer are, but they show up in the diff. They are not used, so they should be ignored and removed. Fun fact, they cause an anomaly when importing structures.

• coercion-tcwp:

  • see coercion-tc
  • clause solve-all-with to repeat solving the main holes of a term until no hole remains
  • enhances instance generation: the subject is not brutally unified, we check first if there is a cs-pattern to direct the resolution against.
  • clause simpl-tc-instance: precompiles an instance (when an argument is a structure, we cut it into sort and class) to give to elpi’s typeclass solver
  • command HB.flush: we want to declare some clauses in the same elpi runtime as the declaration of the predicate, which is not allowed, so we register the clauses and HB.flush accumulates them. N.B. we also postpone the building of the clauses
  • clauses to build a structure on S.sort _ and on anything using information from the context.
  • add our own db for canonical structures: hb-CS-db-for
  • adds clauses for the generic canonical instances for S.sort and S.class in elpi’s canonical structure inference algorithm
  • tactic iter_exact that iterates exact over the proof context

• protowb

  • see coercion-tc
  • enhances instance generate: we use solve-all-with to fill the holes
  • debugging tactics print_goal and print_context

• wbold

  • declares the sort projection as an elpi coercion when there is no coercion target
  • declares an elpi coercion that tries to instantiate a structure using the context
  • declares axioms_ as a typeclass and Axioms_ as an instance in Coq
  • declares axioms_ in Prop whenever every field is in Prop

• tc-any

  • see wbold
  • declares a tactic done_tc := trivial || apply _ || done
  • declares instances as typeclass instances and not as canonical structure instances anymore
  • declare the projections as elpi canonical structures, deferring the instanciation to typeclass search using done_tc

• wb

  • see wbold
  • declares a database of canonical structures
  • adds a clause for elpi’s canonical structure inference that looks up in our database
  • declares all canonical structure instances in our database
  • extend term->cs-patterns to go under the lambdas
  • command HB.canonical_instances: prints the contents of our db of cs instances