Subject: Fragments

Keywords: ::replay
          ::Property
          ::proof

Title: Replay from fragments.

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

view_fragment_proof to build and view new proof mace form fragments

Replay by rebuilding proofs from main goal and fragment database.

Collect properties of found proof.

Generate reports about fragment usage from collected properties.

Per proof :
  num_nons : num fragments used in proof that were not derived from STM of proof,
    each occurence counted
  num_dups : sum of dup occurrences of fragments in proof.
    only counts extra occurences, ie occurs twice means 1 dup
    may be more than one fragment duped, sums all 
  reuse : list of size of duplicate subtrees occuring in proof.
  size: total num fragments used in proof, each occurrence counted even if dups.
  failure: num of attemped fragment instantiations that failed to refine.
  incomplete : num incomplete subgoals
Per fragment :
  - non-origin number of occurrences not in origin proof
     
  - count : number of occurences, may be multiple per proof
Sums :
  - Incomplete: 
      * when multiple choices for a goal then search must fail back to try other
        choices if subtree rooted at that goal can not be completed.
          - when multiple but none complete then incomplete if no multiple ancestor  
          - plausible to find largest subtree when no choice completes
      * when no choice and no ancestor has mulitple choices then leave node incomplete
  - Failure
  - Multiple use in a proof
      sum of num_dups for all proofs
  - Multiple occurrences
      sum of all extra (ie doesn't count first) fragment counts > 1
  - Non-Origin by definition also a Multiple occurence  
there is a connection between non-origin and multiple occurences since
any non-origin fragment is like to be multiple occurrence as
is also likely to be used in origin proof


proof_bydb_search_aux_aux can't fail, all stepfailures are caught by search and 
 become incomplete or make another choice.
collapse_bydb_tree_to_tactic_tree can't fail
apply_proof_bydb can fail if refine fails 
  but refine shouldn't fail unless collapsed tree acts differently then plan tree.
  - incomplete when no tac at tree node
search shouldn't fail, refine fails will result in incomplete?     


Replay theory group with following property,
 first tok = `replay` is key, but make sure other args sensible:
DB:                 FragmentReplay
UpdateEvent:        T:b
⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t
              NUPRL:t

⋅

Home