• Andrei Paskevich's avatar
    Reworking tags and transformations, stage 2: · 157f4a5c
    Andrei Paskevich authored
    - dependent transformations (ones that depend on cloning history
      and/or metaproperties) have now the same type Trans.trans and
      can be registered via Trans, too.
    - load_driver accumulates appropriate tdecls to be appended to
      tasks before transformation/printing.
    At this moment, we have almost everything in place and are ready
    to remove Register module (subsumed by Trans and Printer in core/)
    and Prover module (its functions will move to Driver), and convert
    all printers and transformations to use the new infrastructure. 
    Not implemented yet:
    - appending driver-imposed tdecls to tasks - when and where?
    - metas-options - what is the best way to implement them?
    - syntax/typing for metas in theories and drivers.
printer.ml 7.7 KB