Check-in [afb3b37674]

Not logged in

 ```131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 ... 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 ... 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 ... 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 ... 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 ``` ```% Succeeds if Proof is a structurally-valid proof. We mostly use this for % elaborating partial proofs by replacing a `hole` with a variable and then % asking how it could succeed. proof(trivial). proof(hole). proof(unify(_,_)). proof(ctxmem(_)). proof(induction(_,Proof)) :- proof(Proof). proof(ih(Proof)) :- proof(Proof). proof(generic(Proof)) :- proof(Proof). proof(instan(_,Proof)) :- proof(Proof). proof(product(Proofs)) :- maplist(proof,Proofs). proof(choice(_,Proof)) :- proof(Proof). proof(implies(Proof)) :- proof(Proof). proof(backchain(Proof)) :- proof(Proof). ................................................................................ % subproofs(proof,Subproofs) % Given a proof object, output the list of its subproofs. (children, not % descendants). subproofs(trivial, []). subproofs(hole, []). subproofs(unify(_,_), []). subproofs(ctxmem(_), []). subproofs(induction(_,Proof), [Proof]). subproofs(ih(Proof), [Proof]). subproofs(generic(Proof), [Proof]). subproofs(instan(_,Proof), [Proof]). subproofs(product(Proofs), Proofs). subproofs(choice(_,Proof), [Proof]). subproofs(implies(Proof), [Proof]). subproofs(backchain(Proof), [Proof]). ................................................................................ % subproof itself, uninstantiated, so we now call check to let it fill in % the details. Tree = proof(Goal,_,_,_), check(Program, Goal, NewTree). % If the path is empty, we've reached the node we're looking for, so all the elaborate(Proof,[],What,Data,EProof) :- Proof = proof(Goal,Ctx,Subst,hole), elaborate_node(Goal,Ctx,What,Data,Elaboration), EProof = proof(Goal,Ctx,Subst,Elaboration). elaborate(proof(Goal,Ctx,Subst,Proof), [N|Ns],What,Data, proof(Goal,Ctx,Subst,NewProof)) :- ................................................................................ % proof_complete(Proof) % A proof is complete only if it contains no holes. proof_complete(trivial). proof_complete(ctxmem(_)). proof_complete(unify(_,_)). proof_complete(case(false_left,_,_,[])). proof_complete(induction(_,Proof)) :- proof_complete(Proof). proof_complete(ih(Proof)) :- proof_complete(Proof). proof_complete(generic(Proof)) :- proof_complete(Proof). proof_complete(instan(_,Proof)) :- proof_complete(Proof). proof_complete(product(Proofs)) :- maplist(proof_complete,Proofs). proof_complete(choice(_,Proof)) :- proof_complete(Proof). proof_complete(implies(Proof)) :- proof_complete(Proof). proof_complete(backchain(Proof)) :- proof_complete(Proof). ................................................................................ program:call_goal(Program,V2,Clause,Expansion), % Get variables from the expansion get_vars(Expansion,V3), union(V2,V3,NewVars), % Create the new context append(Expansion,Ctx2,NewCtx), % Recursively check in the new context check(Program, state(NewVars,NewCtx,Goal), VOut,Proof), sub(Proof,Subst). ``` ``` | | | | | ``` ```131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 ... 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 ... 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 ... 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 ... 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 ``` ```% Succeeds if Proof is a structurally-valid proof. We mostly use this for % elaborating partial proofs by replacing a `hole` with a variable and then % asking how it could succeed. proof(trivial). proof(hole). proof(unify(_,_)). proof(ctxmem(_)). proof(induction(_,_,Proof)) :- proof(Proof). proof(ih(Proof)) :- proof(Proof). proof(generic(Proof)) :- proof(Proof). proof(instan(_,Proof)) :- proof(Proof). proof(product(Proofs)) :- maplist(proof,Proofs). proof(choice(_,Proof)) :- proof(Proof). proof(implies(Proof)) :- proof(Proof). proof(backchain(Proof)) :- proof(Proof). ................................................................................ % subproofs(proof,Subproofs) % Given a proof object, output the list of its subproofs. (children, not % descendants). subproofs(trivial, []). subproofs(hole, []). subproofs(unify(_,_), []). subproofs(ctxmem(_), []). subproofs(induction(_,_,Proof), [Proof]). subproofs(ih(Proof), [Proof]). subproofs(generic(Proof), [Proof]). subproofs(instan(_,Proof), [Proof]). subproofs(product(Proofs), Proofs). subproofs(choice(_,Proof), [Proof]). subproofs(implies(Proof), [Proof]). subproofs(backchain(Proof), [Proof]). ................................................................................ % subproof itself, uninstantiated, so we now call check to let it fill in % the details. Tree = proof(Goal,_,_,_), check(Program, Goal, NewTree). % If the path is empty, we've reached the node we're looking for, so all the elaborate(Proof,[],What,Data,EProof) :- Proof = proof(Goal,Ctx,Subst,_), elaborate_node(Goal,Ctx,What,Data,Elaboration), EProof = proof(Goal,Ctx,Subst,Elaboration). elaborate(proof(Goal,Ctx,Subst,Proof), [N|Ns],What,Data, proof(Goal,Ctx,Subst,NewProof)) :- ................................................................................ % proof_complete(Proof) % A proof is complete only if it contains no holes. proof_complete(trivial). proof_complete(ctxmem(_)). proof_complete(unify(_,_)). proof_complete(case(false_left,_,_,[])). proof_complete(induction(_,_,Proof)) :- proof_complete(Proof). proof_complete(ih(Proof)) :- proof_complete(Proof). proof_complete(generic(Proof)) :- proof_complete(Proof). proof_complete(instan(_,Proof)) :- proof_complete(Proof). proof_complete(product(Proofs)) :- maplist(proof_complete,Proofs). proof_complete(choice(_,Proof)) :- proof_complete(Proof). proof_complete(implies(Proof)) :- proof_complete(Proof). proof_complete(backchain(Proof)) :- proof_complete(Proof). ................................................................................ program:call_goal(Program,V2,Clause,Expansion), % Get variables from the expansion get_vars(Expansion,V3), union(V2,V3,NewVars), % Create the new context NewCtx = [Expansion|Ctx2], % Recursively check in the new context check(Program, state(NewVars,NewCtx,Goal), VOut,Proof), sub(Proof,Subst). ```