Subject: Fragments

Keywords: ::search

Title: Using Fragments to suggest proof completions.

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

When prf updated, ie prf_src_modify_inf_tree called
  - Add: Examine inf_tree for complete subtrees to be added to Fragments
      * avoid duplicates how?
        extract source records for proof (hie lemma) and search for dups.
        keep a cache of recent proof record lists
      * allow for adding parts from broken proof or incomplete proof.
          - add all steps without verifying replay and remove those that fail later.
            do not add incomplete
  - Lookup: Search fragments for completions of proof leaves.

Start with lookup :
Suggestions :
  - run a process loop in editor to show suggestions
      * found Thin/Alpha record.
      * found complete Thin/Alpha tree
      * verified tree completes
  - better maybe to have lib collect unrefined subtrees from refine_queue
    and manage process to find and verify subtrees.
      * send messages to editor to reflect state changes.

  - edd finds leaves by searching open proofs?
  - abort search if proof completes at that address?  

Add:
Have distinct Source/Dekreitz tables since may be somewhat ephemeral.
  - maybe annotate Thin/Alpha

Partially complete some proof but then delete lemma, hie will be unusable for
 finding rank, FTTB just delete or map over theory to find first position where
 refinement works.

Pipeline:
  - Source -> Dekretz -> Thin -> Alpha
      * need to implicitly do TNF and HPF or add steps to pipeline 

⋅
--------------------------------------------------

Authors: 

Contributors: NUPRL:t

⋅

Home