• Andrei Paskevich's avatar
    reworking tags and transformations, stage 1: · 18a0e0b0
    Andrei Paskevich authored
    - introduce a new Theory.tdecl "Meta" to be used for tags
    - simplify cloning procedure, get rid of the th_clone field
    - when a goal proposition is discarded during cloning, 
      it's still keeped in the theory as a "skip proposition",
      this is needed to preserve/clone every local identifier.
      Skip propositions are eliminated during task formation.
    - get rid of a separate Task.tdecl type
    - reorganize the Task.task_hd record:
      * use/clone history is cached in a theory-keyed map;
      * meta-properties are cached in a tagname-keyed map.
      This is done to simplify the fine-grained configuration
      of transformations.
    18a0e0b0
driver.ml 12.8 KB