programming-language-foundations/TypecheckingTest.v at main · isergeyam/programming-language-foundations · GitHub

1
2
3
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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
Set Warnings "-notation-overridden,-parsing".
From Coq Require Export String.
From PLF Require Import Typechecking.

Parameter MISSING: Type.

Module Check.

Ltac check_type A B :=
    match type of A with
    | context[MISSING] => idtac "Missing:" A
    | ?T => first [unify T B; idtac "Type: ok" | idtac "Type: wrong - should be (" B ")"]
    end.

Ltac print_manual_grade A :=
    match eval compute in A with
    | Some (_ ?S ?C) =>
        idtac "Score:"  S;
        match eval compute in C with
          | ""%string => idtac "Comment: None"
          | _ => idtac "Comment:" C
        end
    | None =>
        idtac "Score: Ungraded";
        idtac "Comment: None"
    end.

End Check.

From PLF Require Import Typechecking.
Import Check.

Goal True.

idtac "-------------------  typechecker_extensions  --------------------".
idtac " ".

idtac "#> Manually graded: TypecheckerExtensions.type_checking_sound".
idtac "Possible points: 4".
print_manual_grade TypecheckerExtensions.manual_grade_for_type_checking_sound.
idtac " ".

idtac "#> Manually graded: TypecheckerExtensions.type_checking_complete".
idtac "Possible points: 6".
print_manual_grade TypecheckerExtensions.manual_grade_for_type_checking_complete.
idtac " ".

idtac " ".

idtac "Max points - standard: 10".
idtac "Max points - advanced: 10".
idtac "".
idtac "Allowed Axioms:".
idtac "functional_extensionality".
idtac "FunctionalExtensionality.functional_extensionality_dep".
idtac "".
idtac "".
idtac "********** Summary **********".
idtac "".
idtac "Below is a summary of the automatically graded exercises that are incomplete.".
idtac "".
idtac "The output for each exercise can be any of the following:".
idtac "  - 'Closed under the global context', if it is complete".
idtac "  - 'MANUAL', if it is manually graded".
idtac "  - A list of pending axioms, containing unproven assumptions. In this case".
idtac "    the exercise is considered complete, if the axioms are all allowed.".
idtac "".
idtac "********** Standard **********".
idtac "---------- type_checking_sound ---------".
idtac "MANUAL".
idtac "---------- type_checking_complete ---------".
idtac "MANUAL".
idtac "".
idtac "********** Advanced **********".
Abort.

(* 2020-09-09 21:09 *)