Subject: Fragments

Keywords: ::Data

Title: Fragment record structure

--------------------------------------------------

Fragment records are Terms

<fragment-record> : 
  fragment_record
    { <kind>:t> }
    ( <key>;
      <step>;
      <reference_environment>;
      <properties>;
      <conditional properties>
    )

<kind> : Source - Step from source proof
       | Dekreitz - see dekreitz fragments
       | Thin - see Thin Fragments
       | Alpha - see Alpha generalized fragments
<key>  : fragments are stored in a key value database. 
         the key is stored in the fragment to simplify
         management of the key value pair outside of the database.
<reference_environment> : see Reference Environment
<properties> : (<name> # <value>) ilist
  Some common properties :
    - stats : time, space and number of primitive steps
    - functions : info about tactics and tactics used in step
    - dependencies : lists of definitions, lemmas and rules referenced in step.
        * note that not all content referenced is needed for the step to run.
          some items are referenced on aborted paths.
<conditional-properties> : (object_id # ((token # term) list)) list
    the object_id specifies a context under which the fragment is generalized
    the context might indicate a change in content specified by the reference 
    environment such that the refinement is changed. 
  There is only one object id currently used, intent is try to manage some sort
  of truth maintenance or versioning methods, but this is for future 
  development.    
<step> : fragment_step{}(<goal>; <tactic>; <goal> ilist)
    
⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t

⋅

Home