Check-in [afb3b37674]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Fixed a bug in case analysis of atomic goals.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:afb3b37674cd0a42c8c74b85e62c9d71d8651bb2
User & Date: andy 2015-04-15 19:42:19
Context
2015-04-15
19:43
Fixed a couple bugs in the handling of non-string atoms (coerce to string). check-in: 808229ea10 user: andy tags: trunk
19:42
Fixed a bug in case analysis of atomic goals. check-in: afb3b37674 user: andy tags: trunk
14:32
Fixed module declarations/imports for the new argument pattern for `elaborate`. check-in: 207908bad1 user: andy tags: trunk
Changes
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

Changes to plsrc/checker.pl.

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