Subject: Fragments

Keywords: ::API
          ::CODE
          ::ML
          ::implementation
          ::usage

Title: fragment table maintenance functions

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

See also fragment table maintainence recipes.

frag_eval_string

Check state of records and maybe modify some records and 
show some sample of db keys of recores satisfying check.

first bool argument : true means modify db otherwise just show.
token arguments: generally tables

many implicitly use frag_replay_ccobid  

frag_invalidate_hrank_inconsistency : bool -> token -> unit
  - checks for records where a completion has a greater hrank than
    the record. 
  - also invalidates ancestors of inconsistent records. 
  - adds `invalid` main property.

frag_invalidate_grind_failures : bool -> token -> unit
  - checks `grind_fail` cc or main property
    replay failure is grind failure if bad exit of dialog
    replay of source proofs(ie not fragments) may remove replay failures?
    adds `invalid` main property

frag_invalidate_source_orphans : bool -> token -> unit
  - checks if `source` main property is ivoid_term
    adds `invalid` main property.
  - replay will make orphans if source step changes.

frag_invalidate_dekreitz_orphans : bool -> token -> token -> unit
  - first_token is source table, second is dekreitz table
  - collect dekreitz keys of all not invalid source records
    then subtract those from all dek keys 
    and remaining dek keys are orphans

frag_invalidate_dekreitz : bool -> token -> token -> unit 
  - first_token is source table, second is dekreitz table
  - invalidates siblings of invalid deks

frag_invalidate_thins : bool -> token -> token -> unit
  - first_token is dekreitz table, second is thin table
  - union invalid thins with thins of invalid deks
    then union with ancestors

frag_invalidate_alpha : bool -> token -> token -> unit
  - first_token is thin table, second is alpha table
  - union invalid alpha with alphas of invalid thins
    then union with ancestors

frag_clean_source : bool -> token -> unit
  - first token is source table.
  - deletes invalid source records and
    removes orig pointer of relevant dekreitz records

frag_clean_dekreitz : bool -> token -> unit
  - first token is dekreitz table.
  - deletes invalid dekreitz records and
    removes orig pointer of relevant thin records
  this might orphan siblings of dek? 
  without removing orig pointer!
  but likely siblings are invalid too since invalidate touches siblings

frag_clean_thin : bool -> token -> token -> token -> unit
  - index table, thin table, dekreitz table
  - remove invalid thins and dekreitz pointers to those thins.
  - trust that ancestors are invalid. 

frag_clean_alpha : bool -> token -> token -> token -> unit
  - index table, alpha table, thin table 
  - remove invalid alpha and thin pointers to those alphas.
  - trust that ancestors are invalid. 

frag_eval_string "frag_show_replay_failures `Standard_2_9`"


prior functions percolate invalid up
follow push down

frag_invalidate_dekreitz_down : tok -> tok -> tok
  - why -> source table -> dekreitz table
  - invalidates all dekreitz keys of invalid source

frag_invalidate_unreachable : bool -> tok -> tok -> tok -> tok -> unit
 - forreals -> why -> prop name -> up table -> down table  
 - invalidates members of down table not reachable from prop value 
   of not invalid up table records. 
 - computes completion closure to avoid invalidating un-referenced
   members of down table referenced in a completion

frag_fix_orig : bool -> tok -> tok -> tok -> unit
  - prop name -> up table -> down table
  - finds stale `orig` values in valid down table records not referencing 
    valid keys of up table
  - finds valid records of up table which reference records with stale orig
  - modifies orig with list rank valid up table key referencing down record
    if non referencer then orig prop removed.   

frag_verify_index_table : tok -> tok -> unit
  - index table -> table 
  - verifies that all keys in index table refer to extant records.
  - removes stale keys

Presuming have some invalid source :
  - invalidate_dekreitz_down
  - frag_invalidate_unreachable `Thin` <dekreitz> <thin>
  - frag_fix_orig `Thin`  <dekreitz> <thin>  
  - frag_invalidate_unreachable `Alpha` <thin> <alpha>
  - frag_fix_orig `Alpha` <thin> <alpha>  
  - clean source
  - clean dekreitz
  - clean thin
  - clean alpha     



check functions
 - bad pointers -
    orig completion 
    cc Thin Alpha
    source Dekreitz
 - properties
   invalid/bad replay/grind fail  
 ? index tables?

 
  if invalid dekreitz removed prior to calling this then valid thins
  of them would be orphaned.

 In general, being eager with cleaning invalid records will make it more
 likely to produce orphans of the genned records. 
 Orphans are good if grind functions are likely to reproduce exactly
  since they can be adopted rather than reproduced.
 However if grind might produce better records then should want to 
 favor removal over orphaning.
⋅
--------------------------------------------------

Authors: 

Contributors: NUPRL:t
              RICH:t

⋅

Home