Check-in [207908bad1]

Not logged in

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

Overview
Comment:Fixed module declarations/imports for the new argument pattern for `elaborate`.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:207908bad1763ed37f1e312778f47553cf106cf6
User & Date: andy 2015-04-15 14:32:34
Context
2015-04-15
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
14:31
Fixed a small logical mistake in a footnote. check-in: 556662b818 user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to apps/passist/passist.pl.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
%%%
%%% passist.pl
%%% Proof assistant/checker application for Pengines
%%%

:- module(passist, [
    check/2,
    elaborate/4,
    complete/1,
    get_spec/1
]).

:- use_module(library(term_to_json)).

% Load the interpreter and the Nat specification







|







1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
%%%
%%% passist.pl
%%% Proof assistant/checker application for Pengines
%%%

:- module(passist, [
    check/2,
    elaborate/5,
    complete/1,
    get_spec/1
]).

:- use_module(library(term_to_json)).

% Load the interpreter and the Nat specification

Changes to plsrc/checker.pl.

4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
..
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36

37
38
39
40
41
42
43
%%% This only exists to make sure we have the logic right, before implementing
%%% everything in Arend.
%%%

:- module(checker, [
    check/3,
    proof/1,
    elaborate/5,
    proof_complete/1
]).

:- use_module(['program', 'subst', 'util']).

% TODO: (for proof checker)
% * `induction` and `generic` tactics should never be attempted when *generating*
................................................................................
%   a proof (i.e., during resolution). This is already the case for `hole` 
%   tactics (which represent an incomplete proof).
% * An exists(X,Goal(X)) is currently equivalent to Goal(X), except that a 
%   proof of the latter will not contain `instan` nodes. We should pre-check
%   statements (for proofs) to ensure that all existential variables are 
%   explicitly bound by exists() goals. The main purpose of the instan tactic
%   is to explicitly indicate what is being unified with what. 
% * Extend conjuntion to being n-ary. Possibly disjunction as well.
% * Consider making the "canonical" form of proof statements (but not general
%   goals) into 
%
%     forall <conjunction>: exists <disjunction>
%
%   If I'm understanding correctly, this is the form enforced by Twelf.
% * Consider using explicit substitutions (i.e., another argument to check()).
%   A substitution is a list [Var = value,...]. When would we "apply" a 
%   a substitution? How do we check a substitution to canonicalize it, and
%   make sure it's consistent (e.g., not [X = 1, X = 2])?


:- use_module(library(apply)).
:- use_module(library(gensym)).
:- use_module(library(lists)).

:- discontiguous check/4.
:- discontiguous check_case/5.







|







 







<






<
<
<
<
>







4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
..
19
20
21
22
23
24
25

26
27
28
29
30
31




32
33
34
35
36
37
38
39
%%% This only exists to make sure we have the logic right, before implementing
%%% everything in Arend.
%%%

:- module(checker, [
    check/3,
    proof/1,
    elaborate/6,
    proof_complete/1
]).

:- use_module(['program', 'subst', 'util']).

% TODO: (for proof checker)
% * `induction` and `generic` tactics should never be attempted when *generating*
................................................................................
%   a proof (i.e., during resolution). This is already the case for `hole` 
%   tactics (which represent an incomplete proof).
% * An exists(X,Goal(X)) is currently equivalent to Goal(X), except that a 
%   proof of the latter will not contain `instan` nodes. We should pre-check
%   statements (for proofs) to ensure that all existential variables are 
%   explicitly bound by exists() goals. The main purpose of the instan tactic
%   is to explicitly indicate what is being unified with what. 

% * Consider making the "canonical" form of proof statements (but not general
%   goals) into 
%
%     forall <conjunction>: exists <disjunction>
%
%   If I'm understanding correctly, this is the form enforced by Twelf.






:- use_module(library(apply)).
:- use_module(library(gensym)).
:- use_module(library(lists)).

:- discontiguous check/4.
:- discontiguous check_case/5.