• Andrei Paskevich's avatar
    refactor theory.ml: · 1c21c061
    Andrei Paskevich authored
    - split clone code between contexts and theories
    
    - add [Dclone] declarations after cloned decls
    
    - account for the used theories in [ctxt_known]
      (the hash-consed [Duse] declaration is referenced)
    
    - provide use and clone for contexts with a distinct semantics:
    
        Context.use_export ctxt th :
            Copies the contents of [th] and its dependencies
            into [ctxt]. The [Duse] declarations are erased
            from the list of decls, but keeped in [ctxt_known],
            so that theories are not copied twice. Useful to
            build flat contexts.
    
        Context.clone_export ctxt th :
            Clones the contents of [th] into [ctxt]. Dependencies
            of [th] are copied, too. Erases the [Duse] declarations,
            but keeps them in [ctxt_known], so that theories are not
            copied twice. Useful to build flat contexts.
    
        Theory.use_export uc th :
            Marks the dependency on [th]. [Duse th] is added to [uc],
            unless [th] is already used.
    
        Theory.clone_export uc th :
            Clones the contents of [th] into [uc]. The dependencies
            of [th] become dependencies of [uc]. [Duse] declarations
            are added, when a theory is used for the first time.
    
    1c21c061
typing.ml 33.9 KB