Subject: Refiner

Keywords: ::Refiner
          ::CODE
          ::proof
          ::API

Title: Command Line Proof manipulation

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

Library: 

<prf_addr> : term 
  - must have an object_id parameter 
  - first subterm must be a !nat_cons list of !nat{n}

prf_tree_size_at_address : term -> int
  - term arg must be <prf_addr>

make_sub_prf : term -> object_id
  - term arg must be <prf_addr>
  - resulting object has kind `PRF`

make_partial_sub_prf : int -> term -> object_id
  - term arg must be <prf_addr>
  - resulting object has kind `PRF`
  - inf_tree of PRF is cut at depth supplied in first arg. 

make_temp_prf : term -> object_id
  - term arg must be <prf_addr>
  - resulting PRF has single unrefined node.

prf_frontier_addresses : object_id{prf} -> term list
  - object_id arg must specify a PRF 
  - terms of result are <prf_addr>s
  view_show (ilist (prf_frontier_addresses <obid>)) 

frontier_size_at_depth : term -> int list
  - term arg must be <prf_addr>
  - returns a list of what the size of frontier (unrefined steps) at each depth would be.

prf_address_append : term -> term -> term
  - first term arg must be <prf_addr>
  - second subterm must be a !nat_cons list of !nat{n}
  - result is <prf_addr>

replace_inf_tree : term -> object_id -> unit
  - term arg is proof address to be replaced
  - obid arg is source of proof_tree replacement
      * generally expect this is a proof created by make_sub_prf. 

refine_proof_tree_copy : bool -> term -> term -> term
  - if bool arg is true then if step is refined
    if false then if copy exactly matches then the subtree is not refined.
  - first term arg is source to copy from
  - second term arg is destination to copy to. 

apply_proof_filter_cli : term -> object_id -> unit
  - term arg is a term to match.
  - object_id is STM or PRF object to search for matchs
  - pops up list of matching proof addresses.

refine_tree_at_addr : term -> term -> unit
  - first term arg is proof address to be refined
  - second arg is proof address to pull tactic tree from
  - then does refinement via refine_queue similar to m-(return) in prf editor.

refine_tree_same_addr : term -> object_id -> unit
  - first term arg is proof address to be refined
  - second arg is STM/PRF to pull tactic tree from using same address as first arg.
  - then does refinement via refine_queue similar to m-(return) in prf editor.
   

Editor:

show_goal_at_prf_addr : term -> unit
  - first term arg must be <prf_addr>
⋅
--------------------------------------------------

Authors: NUPRL:t

Contributors: RICH:t

⋅

Home