vm.txt (2393B)
1 NEXT STEPS 2 ========== 3 4 - [x] Implement goals for building terms 5 - [x] Implement attitudes 6 - [ ] Implement assumptions 7 - [ ] Implement proofs 8 9 10 NOTES 11 ===== 12 13 GOALS 14 ----- 15 Goals specify a thing to build and a destination. 16 17 - NONE None (JUDGMENT, ASSUMPTION) 18 - JUDG-VAR Give judgment parameter name (SYMBOL) 19 - JUDG-PRE Construct pressuposition term (TERM) 20 - ASMP-VAR Give assumption parameter name (SYMBOL) 21 - ASMP-SUB Construct assumption (ASSUMPTION) 22 - ASMP-JUG Construct judgment term (TERM) 23 - ASMP-PRF Prove judgment (PROOF) 24 - ASMP-ARG Construct proof argument (TERM) 25 26 TACTICS 27 ------- 28 Tactics take arguments and build things for solving goals. 29 30 - JUG (symbol, arity, subsize) Start a judgment form [construct JUDGMENT] 31 - ASM (symbol, arity, subsize) Start an assumption [construct ASSUMPTION] 32 - NAM (symbol) Name a symbol [construct SYMBOL] 33 - ATM (symbol) Construct an atomic term [construct TERM] 34 - APP (symbol, arity) Start a complex term [TERM] 35 - REF (symbol) Reference an assumption [PROOF] 36 37 EFFECTS 38 ------- 39 Each tactic changes the state of the system and possibly creates more 40 goals, but also discharges the current one. 41 42 - JUG (symbol name, int arity, int subsize): 43 - allocate new judgment and set target to point to it 44 - create `arity` symbol goals pointing to its variables 45 - create `subsize` term goals pointing to its pressupositions 46 47 - ASM (symbol name, int arity, int subsize): 48 - allocate new assumption and set target to point to it 49 - create `arity` symbol goals pointing to its variables 50 - create `subsize` assumption goals pointing to its subassumptions 51 - create a term goal pointing to its judgment 52 - create a proof goal pointing to its judgment 53 54 - NAM (symbol): set target's value to givem symbol 55 56 - ATM (symbol): 57 - allocate new term with arity 0 58 - set term's head to given symbol 59 - set target to point to term 60 61 - APP (symbol head, int arity): 62 - allocate new term with arity `arity` 63 - set term's head to `head` 64 - create `arity` symbol goals pointing to the term's subterms 65 66 - REF (symbol): 67 - set target proposition's candidate to given symbol 68 - create one term goal for each variable in assumption refered to by symbol 69 - create one proof goal for each subassumption of the assumption refered to by symbol 70 71 RESOLUTION 72 ---------- 73 When all subgoals of a goal are resolved, extra logic might be needed to verify the resolution of the current goal.