From 494fb52be0d7c70947bab96e733bddc78636f9fe Mon Sep 17 00:00:00 2001 From: DwarfMaster Date: Wed, 8 Jun 2022 15:44:15 +0200 Subject: [PATCH 1/4] Add new check to the api --- api/dep.ml | 1 + api/pp.ml | 4 +++- api/processor.ml | 14 ++++++++++++++ 3 files changed, 18 insertions(+), 1 deletion(-) diff --git a/api/dep.ml b/api/dep.ml index 43c6b7ff..beb0af15 100644 --- a/api/dep.ml +++ b/api/dep.ml @@ -159,6 +159,7 @@ let handle_entry e = | Infer (_, _, te) -> mk_term te | Check (_, _, _, Convert (t1, t2)) -> mk_term t1; mk_term t2 | Check (_, _, _, HasType (te, ty)) -> mk_term te; mk_term ty + | Check (_, _, _, Typeable te) -> mk_term te | DTree (_, _, _) -> () | Print (_, _) -> () | Name (_, _) -> () diff --git a/api/pp.ml b/api/pp.ml index d89384e4..81edf84b 100644 --- a/api/pp.ml +++ b/api/pp.ml @@ -326,7 +326,9 @@ module Make (S : Sig) : Printer = struct | Convert (t1, t2) -> fprintf fmt "%s%s %a ==@ %a.@." cmd neg print_term t1 print_term t2 | HasType (te, ty) -> - fprintf fmt "%s%s %a ::@ %a.@." cmd neg print_term te print_term ty) + fprintf fmt "%s%s %a ::@ %a.@." cmd neg print_term te print_term ty + | Typeable te -> + fprintf fmt "%s%s %a.@." cmd neg pp_term te) | DTree (_, m, v) -> ( match m with | None -> fprintf fmt "#GDT %a.@." print_ident v diff --git a/api/processor.ml b/api/processor.ml index bc704ac2..b3d240e3 100644 --- a/api/processor.ml +++ b/api/processor.ml @@ -68,6 +68,13 @@ module MakeTypeChecker (Env : CustomEnv) : S with type t = unit = struct | true, true -> () | false, false -> Format.printf "NO@." | false, true -> raise @@ Entry.Assert_error lc) + | Check (lc, assrt, neg, Typeable te) -> ( + let succ = try ignore (Env.infer env te); not neg with _ -> neg in + match (succ,assrt) with + | true, false -> Format.printf "YES@." + | true, true -> () + | false, false -> Format.printf "NO@." + | false, true -> raise @@ Entry.Assert_error lc) | DTree (lc, m, v) -> let m = match m with None -> Env.get_name env | Some m -> m in let cst = mk_name m v in @@ -185,6 +192,13 @@ module MakeTopLevel (Env : CustomEnv) : S with type t = unit = struct | true, true -> () | false, false -> Format.printf "NO@." | false, true -> raise @@ Entry.Assert_error lc) + | Check (lc, assrt, neg, Typeable te) -> ( + let succ = try ignore (Env.infer env te); not neg with _ -> neg in + match (succ,assrt) with + | true, false -> Format.printf "YES@." + | true, true -> () + | false, false -> Format.printf "NO@." + | false, true -> raise @@ Entry.Assert_error lc) | DTree (lc, m, v) -> let m = match m with None -> Env.get_name env | Some m -> m in let cst = mk_name m v in From 5189a1352be4c59383beb2793d2a4e1233a5d116 Mon Sep 17 00:00:00 2001 From: DwarfMaster Date: Wed, 8 Jun 2022 15:45:26 +0200 Subject: [PATCH 2/4] Implement new pragma syntax without contexts --- parsing/entry.ml | 8 +++- parsing/entry.mli | 5 ++- parsing/lexer.mll | 93 +++++++++++++++++++++------------------ parsing/menhir_parser.mly | 59 ++++++++++++++++--------- parsing/tokens.ml | 21 ++++++--- 5 files changed, 111 insertions(+), 75 deletions(-) diff --git a/parsing/entry.ml b/parsing/entry.ml index 17a552af..f84f8f5d 100644 --- a/parsing/entry.ml +++ b/parsing/entry.ml @@ -8,7 +8,9 @@ type is_assertion = bool type should_fail = bool -type test = Convert of term * term | HasType of term * term +type test = Convert of term * term + | HasType of term * term + | Typeable of term exception Assert_error of loc @@ -68,7 +70,9 @@ let pp_entry fmt e = | Convert (t1, t2) -> fprintf fmt "%s%s %a ==@ %a.@." cmd neg pp_term t1 pp_term t2 | HasType (te, ty) -> - fprintf fmt "%s%s %a ::@ %a.@." cmd neg pp_term te pp_term ty) + fprintf fmt "%s%s %a ::@ %a.@." cmd neg pp_term te pp_term ty + | Typeable te -> + fprintf fmt "%s%s %a.@." cmd neg pp_term te) | DTree (_, m, v) -> ( match m with | None -> fprintf fmt "#GDT %a.@." pp_ident v diff --git a/parsing/entry.mli b/parsing/entry.mli index d0795cec..df8365b9 100644 --- a/parsing/entry.mli +++ b/parsing/entry.mli @@ -10,8 +10,9 @@ type should_fail = bool (** Possible tests in source files. *) type test = - | Convert of term * term (** Convertibility between the two given terms. *) - | HasType of term * term (** Typability test, given a term and a type. *) + | Convert of term * term (** Convertibility between the two given terms. *) + | HasType of term * term (** Typability test, given a term and a type. *) + | Typeable of term (** Typability test, without the type *) exception Assert_error of loc diff --git a/parsing/lexer.mll b/parsing/lexer.mll index 51a20b6d..3794b6bd 100644 --- a/parsing/lexer.mll +++ b/parsing/lexer.mll @@ -23,53 +23,56 @@ let ident = ['a'-'z' 'A'-'Z' '0'-'9' '_' '!' '?']['a'-'z' 'A'-'Z' '0'-'9' '_' let capital = ['A'-'Z']+ rule token = parse - | space { token lexbuf } - | '\n' { new_line lexbuf ; token lexbuf } - | "(;" { comment 0 lexbuf} - | '.' { DOT } - | ',' { COMMA } - | ':' { COLON } - | "==" { EQUAL } - | '[' { LEFTSQU } - | ']' { RIGHTSQU } - | '{' { LEFTBRA } - | '}' { RIGHTBRA } - | '(' { LEFTPAR } - | ')' { RIGHTPAR } - | "-->" { LONGARROW } - | "->" { ARROW } - | "=>" { FATARROW } - | ":=" { DEF } - | "_" { UNDERSCORE ( get_loc lexbuf ) } - | "Type" { TYPE ( get_loc lexbuf ) } - | "def" { KW_DEF ( get_loc lexbuf ) } - | "defac" { KW_DEFAC ( get_loc lexbuf ) } - | "defacu" { KW_DEFACU ( get_loc lexbuf ) } - | "injective" { KW_INJ ( get_loc lexbuf ) } - | "thm" { KW_THM ( get_loc lexbuf ) } - | "private" { KW_PRV ( get_loc lexbuf ) } - | "#NAME" space+ (mident as md) { NAME (get_loc lexbuf , mk_mident md) } - | "#REQUIRE" space+ (mident as md) { REQUIRE (get_loc lexbuf , mk_mident md) } - | "#EVAL" { EVAL ( get_loc lexbuf ) } - | "#INFER" { INFER ( get_loc lexbuf ) } - | "#CHECK" { CHECK ( get_loc lexbuf ) } - | "#CHECKNOT" { CHECKNOT ( get_loc lexbuf ) } - | "#ASSERT" { ASSERT ( get_loc lexbuf ) } - | "#ASSERTNOT"{ ASSERTNOT ( get_loc lexbuf ) } - | "#PRINT" { PRINT ( get_loc lexbuf ) } - | "#GDT" { GDT ( get_loc lexbuf ) } + | space { token lexbuf } + | '\n' { new_line lexbuf ; token lexbuf } + | "(;# eval" { PRAGMA_EVAL ( get_loc lexbuf ) } + | "(;# infer" { PRAGMA_INFER ( get_loc lexbuf ) } + | "(;# check" { PRAGMA_CHECK ( get_loc lexbuf ) } + | "(;# checknot" { PRAGMA_CHECKNOT ( get_loc lexbuf ) } + | "(;# assert" { PRAGMA_ASSERT ( get_loc lexbuf ) } + | "(;# assertnot" { PRAGMA_ASSERTNOT ( get_loc lexbuf ) } + | "(;# print" { PRAGMA_PRINT ( get_loc lexbuf ) } + | "(;# gdt" { PRAGMA_GDT ( get_loc lexbuf ) } + | "(;#" { generic_pragma lexbuf } + | "#;)" { PRAGMA_END ( get_loc lexbuf ) } + | "(;" { comment 0 lexbuf} + | '.' { DOT } + | ',' { COMMA } + | ':' { COLON } + | "==" { EQUAL } + | '[' { LEFTSQU } + | ']' { RIGHTSQU } + | '{' { LEFTBRA } + | '}' { RIGHTBRA } + | '(' { LEFTPAR } + | ')' { RIGHTPAR } + | "-->" { LONGARROW } + | "->" { ARROW } + | "=>" { FATARROW } + | ":=" { DEF } + | "|-" { VDASH } + | "?" { QUESTION } + | "_" { UNDERSCORE ( get_loc lexbuf ) } + | "Type" { TYPE ( get_loc lexbuf ) } + | "def" { KW_DEF ( get_loc lexbuf ) } + | "defac" { KW_DEFAC ( get_loc lexbuf ) } + | "defacu" { KW_DEFACU ( get_loc lexbuf ) } + | "injective" { KW_INJ ( get_loc lexbuf ) } + | "thm" { KW_THM ( get_loc lexbuf ) } + | "private" { KW_PRV ( get_loc lexbuf ) } + | "assert" { ASSERT ( get_loc lexbuf ) } | mident as md '.' (ident as id) - { QID ( get_loc lexbuf , mk_mident md , mk_ident id ) } + { QID ( get_loc lexbuf , mk_mident md , mk_ident id ) } | ident as id - { ID ( get_loc lexbuf , mk_ident id ) } - | '{' '|' { sident None (Buffer.create 42) lexbuf } + { ID ( get_loc lexbuf , mk_ident id ) } + | '{' '|' { sident None (Buffer.create 42) lexbuf } | mident as md '.' '{' '|' - {sident (Some (mk_mident md)) (Buffer.create 42) lexbuf} - | '"' { string (Buffer.create 42) lexbuf } + {sident (Some (mk_mident md)) (Buffer.create 42) lexbuf} + | '"' { string (Buffer.create 42) lexbuf } | _ as s - { let msg = sprintf "Unexpected characters '%s'." (String.make 1 s) in + { let msg = sprintf "Unexpected characters '%s'." (String.make 1 s) in fail (get_loc lexbuf) msg } - | eof { EOF } + | eof { EOF } and comment i = parse | ";)" { if (i=0) then token lexbuf else comment (i-1) lexbuf } @@ -78,6 +81,12 @@ and comment i = parse | _ { comment i lexbuf } | eof { fail (get_loc lexbuf) "Unexpected end of file." } +and generic_pragma = parse + | "#;)" { token lexbuf } + | "\n" { new_line lexbuf; generic_pragma lexbuf } + | _ { generic_pragma lexbuf } + | eof { fail (get_loc lexbuf) "Unexpected end of file." } + and string buf = parse | '\\' (_ as c) { Buffer.add_char buf '\\'; Buffer.add_char buf c; string buf lexbuf } diff --git a/parsing/menhir_parser.mly b/parsing/menhir_parser.mly index 027ee740..c62ed852 100644 --- a/parsing/menhir_parser.mly +++ b/parsing/menhir_parser.mly @@ -57,14 +57,18 @@ let loc_of_rs = function %token RIGHTBRA %token LEFTSQU %token RIGHTSQU -%token EVAL -%token INFER -%token CHECK -%token CHECKNOT +%token VDASH +%token QUESTION +%token PRAGMA_EVAL +%token PRAGMA_INFER +%token PRAGMA_CHECK +%token PRAGMA_CHECKNOT +%token PRAGMA_ASSERT +%token PRAGMA_ASSERTNOT +%token PRAGMA_PRINT +%token PRAGMA_GDT +%token PRAGMA_END %token ASSERT -%token ASSERTNOT -%token PRINT -%token GDT %token UNDERSCORE %token NAME %token REQUIRE @@ -142,36 +146,47 @@ line: | rs=rule+ DOT {fun md -> Rules(loc_of_rs rs,(List.map (scope_rule md) rs))} - | EVAL te=term DOT + | ASSERT QUESTION te=term DOT + {fun md -> Check($1, true, false, Typeable(scope_term md [] te))} + | ASSERT VDASH t1=aterm EQUAL t2=term DOT + {fun md -> Check($1, true , false, Convert(scope_term md [] t1, scope_term md [] t2))} + | ASSERT VDASH te=aterm COLON ty=term DOT + {fun md -> Check($1, true, false, HasType(scope_term md [] te, scope_term md [] ty))} + + | PRAGMA_EVAL te=term PRAGMA_END {fun md -> Eval($1, default_cfg, scope_term md [] te)} - | EVAL cfg=eval_config te=term DOT + | PRAGMA_EVAL cfg=eval_config te=term PRAGMA_END {fun md -> Eval($1, cfg, scope_term md [] te)} - | INFER te=term DOT + | PRAGMA_INFER te=term PRAGMA_END {fun md -> Infer($1, default_cfg, scope_term md [] te)} - | INFER cfg=eval_config te=term DOT + | PRAGMA_INFER cfg=eval_config te=term PRAGMA_END {fun md -> Infer($1, cfg, scope_term md [] te)} - | CHECK te=aterm COLON ty=term DOT + | PRAGMA_CHECK te=aterm COLON ty=term PRAGMA_END {fun md -> Check($1, false, false, HasType(scope_term md [] te, scope_term md [] ty))} - | CHECKNOT te=aterm COLON ty=term DOT + | PRAGMA_CHECKNOT te=aterm COLON ty=term PRAGMA_END {fun md -> Check($1, false, true , HasType(scope_term md [] te, scope_term md [] ty))} - | ASSERT te=aterm COLON ty=term DOT + | PRAGMA_ASSERT te=aterm COLON ty=term PRAGMA_END {fun md -> Check($1, true , false, HasType(scope_term md [] te, scope_term md [] ty))} - | ASSERTNOT te=aterm COLON ty=term DOT + | PRAGMA_ASSERTNOT te=aterm COLON ty=term PRAGMA_END {fun md -> Check($1, true , true , HasType(scope_term md [] te, scope_term md [] ty))} - | CHECK t1=aterm EQUAL t2=term DOT + | PRAGMA_CHECK t1=aterm EQUAL t2=term PRAGMA_END {fun md -> Check($1, false, false, Convert(scope_term md [] t1, scope_term md [] t2))} - | CHECKNOT t1=aterm EQUAL t2=term DOT + | PRAGMA_CHECKNOT t1=aterm EQUAL t2=term PRAGMA_END {fun md -> Check($1, false, true , Convert(scope_term md [] t1, scope_term md [] t2))} - | ASSERT t1=aterm EQUAL t2=term DOT + | PRAGMA_ASSERT t1=aterm EQUAL t2=term PRAGMA_END {fun md -> Check($1, true , false, Convert(scope_term md [] t1, scope_term md [] t2))} - | ASSERTNOT t1=aterm EQUAL t2=term DOT + | PRAGMA_ASSERTNOT t1=aterm EQUAL t2=term PRAGMA_END {fun md -> Check($1, true , true , Convert(scope_term md [] t1, scope_term md [] t2))} - | PRINT STRING DOT {fun _ -> Print($1, $2)} - | GDT ID DOT {fun _ -> DTree($1, None, snd $2)} - | GDT QID DOT {fun _ -> let (_,m,v) = $2 in DTree($1, Some m, v)} + | PRAGMA_PRINT STRING PRAGMA_END + {fun _ -> Print($1, $2)} + | PRAGMA_GDT ID PRAGMA_END + {fun _ -> DTree($1, None, snd $2)} + | PRAGMA_GDT QID PRAGMA_END + {fun _ -> let (_,m,v) = $2 in DTree($1, Some m, v)} + | n=NAME DOT {fun _ -> Name(fst n, snd n)} | r=REQUIRE DOT {fun _ -> Require(fst r,snd r)} | EOF {raise End_of_file} diff --git a/parsing/tokens.ml b/parsing/tokens.ml index 02638b25..694614e9 100644 --- a/parsing/tokens.ml +++ b/parsing/tokens.ml @@ -3,6 +3,7 @@ open Kernel.Basic type token = | UNDERSCORE of loc | TYPE of loc + (* Update *) | KW_DEF of loc | KW_DEFAC of loc | KW_DEFACU of loc @@ -28,12 +29,18 @@ type token = | COLON | EQUAL | ARROW - | EVAL of loc - | INFER of loc - | CHECK of loc + | QUESTION + (* New pragma system *) + | PRAGMA_END of loc + | PRAGMA_EVAL of loc + | PRAGMA_INFER of loc + | PRAGMA_CHECK of loc + | PRAGMA_CHECKNOT of loc + | PRAGMA_ASSERT of loc + | PRAGMA_ASSERTNOT of loc + | PRAGMA_PRINT of loc + | PRAGMA_GDT of loc | ASSERT of loc - | CHECKNOT of loc - | ASSERTNOT of loc - | PRINT of loc - | GDT of loc + | VDASH + (* End of pragma system *) | STRING of string From 7b5ceeafa5ebfc4c5769ebfc76aa21cd3e1481f5 Mon Sep 17 00:00:00 2001 From: DwarfMaster Date: Wed, 8 Jun 2022 15:46:24 +0200 Subject: [PATCH 3/4] Update tests --- tests/KO/arity.dk | 2 +- tests/KO/arrowCodomainType.dk | 2 +- tests/KO/arrowDomainType.dk | 2 +- tests/KO/arrowDomainType2.dk | 2 +- tests/KO/assert_conv_command.dk | 2 +- tests/KO/assert_not_conv_command.dk | 2 +- tests/KO/assert_not_type_command.dk | 2 +- tests/KO/assert_type_command.dk | 2 +- tests/KO/brackets5.dk | 2 +- tests/KO/convertibility_check_types.dk | 2 +- tests/KO/guard1.dk | 2 +- tests/KO/guard2.dk | 2 +- tests/KO/nsteps1.dk | 2 +- tests/KO/product_expected_6.dk | 2 +- tests/KO/typeArrowType.dk | 2 +- tests/OK/arities.dk | 14 ++--- tests/OK/arities2.dk | 6 +-- tests/OK/assert/conv_command.dk | 6 +-- tests/OK/assert/type_command.dk | 4 +- tests/OK/check/conv_command.dk | 16 +++--- tests/OK/check/type_command.dk | 16 +++--- tests/OK/fixpoints.dk | 34 ++++++------ tests/OK/guard1.dk | 2 +- tests/OK/guard2.dk | 2 +- tests/OK/guard3.dk | 2 +- tests/OK/ho_bug1.dk | 4 +- tests/OK/ho_bug2.dk | 6 +-- tests/OK/ho_match.dk | 10 ++-- tests/OK/ho_nonlinearity.dk | 2 +- .../inferingKindForArrowWithCodomainType.dk | 8 +-- tests/OK/inferingKindForType.dk | 4 +- tests/OK/let_syntax.dk | 10 ++-- tests/OK/miller1.dk | 6 +-- tests/OK/miller2.dk | 6 +-- tests/OK/nested_miller_pattern.dk | 4 +- tests/OK/nsteps1.dk | 32 ++++++------ tests/OK/nsteps2.dk | 16 +++--- tests/OK/nsteps3.dk | 28 +++++----- tests/OK/nsteps4.dk | 52 +++++++++---------- tests/OK/recursive.dk | 2 +- tests/OK/self_dep.dk | 4 +- tests/OK/self_dep2.dk | 4 +- tests/OK/sharing.dk | 20 +++---- tests/OK/special_idents1.dk | 10 ++-- tests/OK/underscore1.dk | 2 +- tests/OK/underscore2.dk | 2 +- tests/OK/underscore3.dk | 4 +- tests/OK/underscore4.dk | 6 +-- tests/OK/underscore5.dk | 4 +- tests/OK/underscore6.dk | 6 +-- tests/OK/underscore7.dk | 6 +-- tests/acu/cc.dk | 8 +-- tests/acu/easy_ac.dk | 18 +++---- tests/acu/extra_rules.dk | 10 ++-- tests/acu/extra_rules2.dk | 20 +++---- tests/acu/extra_rules3.dk | 32 ++++++------ tests/acu/extra_rules4.dk | 26 +++++----- tests/acu/fail_ac.dk | 2 +- tests/acu/min_ac.dk | 4 +- tests/eta/KO/eta_0.dk | 2 +- tests/eta/KO/eta_1b.dk | 2 +- tests/eta/KO/eta_2.dk | 2 +- tests/eta/OK/eta_0.dk | 2 +- tests/eta/OK/eta_0b.dk | 2 +- tests/eta/OK/eta_1.dk | 2 +- tests/eta/OK/eta_2.dk | 2 +- tests/eta/OK/eta_2b.dk | 2 +- 67 files changed, 263 insertions(+), 263 deletions(-) diff --git a/tests/KO/arity.dk b/tests/KO/arity.dk index e8954e5c..89533d36 100644 --- a/tests/KO/arity.dk +++ b/tests/KO/arity.dk @@ -6,4 +6,4 @@ N : Type. def a : (N -> N) -> N -> N. [f] a (x => f x) --> f. -#SNF a (z => z). +(;# snf a (z => z) #;) diff --git a/tests/KO/arrowCodomainType.dk b/tests/KO/arrowCodomainType.dk index b8036608..d4fa58ee 100644 --- a/tests/KO/arrowCodomainType.dk +++ b/tests/KO/arrowCodomainType.dk @@ -1,4 +1,4 @@ (; KO 101 ;) A : Type. -#INFER (A -> Type) -> A. +(;# infer (A -> Type) -> A #;) diff --git a/tests/KO/arrowDomainType.dk b/tests/KO/arrowDomainType.dk index 39f6cea3..add453c0 100644 --- a/tests/KO/arrowDomainType.dk +++ b/tests/KO/arrowDomainType.dk @@ -1,4 +1,4 @@ (; KO 101 ;) A : Type. -#INFER Type -> A. +(;# infer Type -> A #;) diff --git a/tests/KO/arrowDomainType2.dk b/tests/KO/arrowDomainType2.dk index 91cd6805..15b8ff8c 100644 --- a/tests/KO/arrowDomainType2.dk +++ b/tests/KO/arrowDomainType2.dk @@ -1,4 +1,4 @@ (; KO 101 ;) A : Type. -#INFER (Type -> A) -> A. +(;# infer (Type -> A) -> A #;) diff --git a/tests/KO/assert_conv_command.dk b/tests/KO/assert_conv_command.dk index 1c078e77..6b7dd881 100644 --- a/tests/KO/assert_conv_command.dk +++ b/tests/KO/assert_conv_command.dk @@ -3,4 +3,4 @@ A : Type. B : Type. -#ASSERT A == B. +(;# assert A == B #;) diff --git a/tests/KO/assert_not_conv_command.dk b/tests/KO/assert_not_conv_command.dk index d96562ab..05586eaf 100644 --- a/tests/KO/assert_not_conv_command.dk +++ b/tests/KO/assert_not_conv_command.dk @@ -3,4 +3,4 @@ A : Type. def B := A. -#ASSERTNOT B == A. +(;# assertnot B == A #;) diff --git a/tests/KO/assert_not_type_command.dk b/tests/KO/assert_not_type_command.dk index e526a2cc..c8bd5f92 100644 --- a/tests/KO/assert_not_type_command.dk +++ b/tests/KO/assert_not_type_command.dk @@ -3,4 +3,4 @@ A : Type. a : A. -#ASSERTNOT a : A. +(;# assertnot a : A #;) diff --git a/tests/KO/assert_type_command.dk b/tests/KO/assert_type_command.dk index dabb4d88..8f2b463b 100644 --- a/tests/KO/assert_type_command.dk +++ b/tests/KO/assert_type_command.dk @@ -4,4 +4,4 @@ A : Type. B : Type. a : A. -#ASSERT a : B. +(;# assert a : B #;) diff --git a/tests/KO/brackets5.dk b/tests/KO/brackets5.dk index 8b14b2d3..586ae724 100644 --- a/tests/KO/brackets5.dk +++ b/tests/KO/brackets5.dk @@ -18,4 +18,4 @@ def g : x : A -> eta (V a) -> eta (V a) -> eta (V a). [x,N] g x N {N} --> g x N N. -#EVAL[WHNF,1] (g a N C). +(;# eval [WHNF,1] (g a N C) #;) diff --git a/tests/KO/convertibility_check_types.dk b/tests/KO/convertibility_check_types.dk index eb78ddae..8ffd8780 100644 --- a/tests/KO/convertibility_check_types.dk +++ b/tests/KO/convertibility_check_types.dk @@ -1,4 +1,4 @@ (; KO 704 ;) A : Type. B : Type. -#ASSERT (x : A => x) == (x : B => x). +(;# assert (x : A => x) == (x : B => x) #;) diff --git a/tests/KO/guard1.dk b/tests/KO/guard1.dk index d4ab513d..2b23306c 100644 --- a/tests/KO/guard1.dk +++ b/tests/KO/guard1.dk @@ -11,4 +11,4 @@ def ff : A -> (A -> A) -> A. def pr1 : A -> A -> A. [x,y] pr1 x y --> x. -#EVAL[WHNF] (ff a (y => (pr1 a y))). +(;# eval [WHNF] (ff a (y => (pr1 a y))) #;) diff --git a/tests/KO/guard2.dk b/tests/KO/guard2.dk index 68bf592b..b7c0bc0d 100644 --- a/tests/KO/guard2.dk +++ b/tests/KO/guard2.dk @@ -8,4 +8,4 @@ g : A -> A. def ff : A -> (A -> A) -> A. [x] ff x (y => {g x}) --> a. -#CHECK (ff a (y => a)) == a. +(;# check (ff a (y => a)) == a #;) diff --git a/tests/KO/nsteps1.dk b/tests/KO/nsteps1.dk index 0c307801..1146ef67 100644 --- a/tests/KO/nsteps1.dk +++ b/tests/KO/nsteps1.dk @@ -2,4 +2,4 @@ def A : Type. -#EVAL[-1] A. +(;# eval [-1] A #;) diff --git a/tests/KO/product_expected_6.dk b/tests/KO/product_expected_6.dk index 3227c28d..965024c4 100644 --- a/tests/KO/product_expected_6.dk +++ b/tests/KO/product_expected_6.dk @@ -4,4 +4,4 @@ A : Type. f : A. -#INFER (x : A => f x). +(;# infer (x : A => f x) #;) diff --git a/tests/KO/typeArrowType.dk b/tests/KO/typeArrowType.dk index 24082112..048e7bb8 100644 --- a/tests/KO/typeArrowType.dk +++ b/tests/KO/typeArrowType.dk @@ -1,3 +1,3 @@ (; KO 101 ;) -#INFER Type -> Type. +(;# infer Type -> Type #;) diff --git a/tests/OK/arities.dk b/tests/OK/arities.dk index 8ce4c0ff..a2f8be1c 100644 --- a/tests/OK/arities.dk +++ b/tests/OK/arities.dk @@ -16,10 +16,10 @@ def f : A -> A -> A -> A -> A. [] f --> i. -#ASSERT f a a a b == g b. -#ASSERT f c a b == i c a b. -#ASSERT f b a b == h a b. -#ASSERT f b a == h a. -#ASSERT f a a == i a a. -#ASSERT f a == i a. -#ASSERT f == i. +(;# assert f a a a b == g b #;) +(;# assert f c a b == i c a b #;) +(;# assert f b a b == h a b #;) +(;# assert f b a == h a #;) +(;# assert f a a == i a a #;) +(;# assert f a == i a #;) +(;# assert f == i #;) diff --git a/tests/OK/arities2.dk b/tests/OK/arities2.dk index 04356b17..da815cf3 100644 --- a/tests/OK/arities2.dk +++ b/tests/OK/arities2.dk @@ -15,6 +15,6 @@ def g : N -> N. [] g (f (S (S 0)) 0 0) --> S (S 0). -#ASSERT g (f 0 ) == 0. -#ASSERT g (f (S 0) 0 ) == S 0. -#ASSERT g (f (S (S 0)) 0 0) == S (S 0). +(;# assert g (f 0 ) == 0 #;) +(;# assert g (f (S 0) 0 ) == S 0 #;) +(;# assert g (f (S (S 0)) 0 0) == S (S 0) #;) diff --git a/tests/OK/assert/conv_command.dk b/tests/OK/assert/conv_command.dk index 2a98f5ea..ec7197cd 100644 --- a/tests/OK/assert/conv_command.dk +++ b/tests/OK/assert/conv_command.dk @@ -5,6 +5,6 @@ def B := A. def C := A. D : Type. -#ASSERT B == A. -#ASSERT B == C. -#ASSERTNOT A == D. +assert |- B == A. +assert |- B == C. +(;# assertnot A == D #;) diff --git a/tests/OK/assert/type_command.dk b/tests/OK/assert/type_command.dk index ec9397f5..da0b0448 100644 --- a/tests/OK/assert/type_command.dk +++ b/tests/OK/assert/type_command.dk @@ -4,5 +4,5 @@ A : Type. B : Type. a : A. -#ASSERT a : A. -#ASSERTNOT a : B. +assert |- a : A. +(;# assertnot a : B #;) diff --git a/tests/OK/check/conv_command.dk b/tests/OK/check/conv_command.dk index e2d667d5..ce5f3002 100644 --- a/tests/OK/check/conv_command.dk +++ b/tests/OK/check/conv_command.dk @@ -5,14 +5,14 @@ def B := A. def C := A. D : Type. -#CHECK B == A. -#PRINT "YES". +(;# check B == A #;) +(;# print "YES" #;) -#CHECKNOT D == A. -#PRINT "YES". +(;# checknot D == A #;) +(;# print "YES" #;) -#CHECKNOT B == C. -#PRINT "NO". +(;# checknot B == C #;) +(;# print "NO" #;) -#CHECK C == D. -#PRINT "NO". +(;# check C == D #;) +(;# print "NO" #;) diff --git a/tests/OK/check/type_command.dk b/tests/OK/check/type_command.dk index fde536bf..44b0af15 100644 --- a/tests/OK/check/type_command.dk +++ b/tests/OK/check/type_command.dk @@ -4,14 +4,14 @@ A : Type. B : Type. a : A. -#CHECK a : A. -#PRINT "YES". +(;# check a : A #;) +(;# print "YES" #;) -#CHECKNOT a : B. -#PRINT "YES". +(;# checknot a : B #;) +(;# print "YES" #;) -#CHECKNOT a : A. -#PRINT "NO". +(;# checknot a : A #;) +(;# print "NO" #;) -#CHECK a : B. -#PRINT "NO". +(;# check a : B #;) +(;# print "NO" #;) diff --git a/tests/OK/fixpoints.dk b/tests/OK/fixpoints.dk index 543627da..a8afb172 100644 --- a/tests/OK/fixpoints.dk +++ b/tests/OK/fixpoints.dk @@ -999,10 +999,10 @@ def nat__rect__proj := fix_proj (type z) 1 nat__rect__MA nat__rect__FP 0. (; -#PRINT " nat_rect : Nat -> P n ?". -#CHECK nat__rect__proj : ( n : T set nat -> T (type z) (P n) ). +(;# print " nat_rect : Nat -> P n ?" #;) +(;# check nat__rect__proj : ( n : T set nat -> T (type z) (P n) ) #;) ;) -#ASSERT nat__rect__proj : ( n : T set nat -> T (type z) (P n) ). +(;# assert nat__rect__proj : ( n : T set nat -> T (type z) (P n) ) #;) def nat__rect : @@ -1067,10 +1067,10 @@ def plus : 0. (; -#PRINT " 2+3 = 5 ?". -#CHECK plus _2 _3 == _5. +(;# print " 2+3 = 5 ?" #;) +(;# check plus _2 _3 == _5 #;) ;) -#ASSERT plus _2 _3 == _5. +(;# assert plus _2 _3 == _5 #;) def times : @@ -1088,10 +1088,10 @@ def times : 0. (; -#PRINT " 2*3 = 6 ?". -#CHECK times _2 _3 == _6. +(;# print " 2*3 = 6 ?" #;) +(;# check times _2 _3 == _6 #;) ;) -#ASSERT times _2 _3 == _6. +(;# assert times _2 _3 == _6 #;) def _10 := plus _5 _5. @@ -1100,14 +1100,14 @@ def _1000 := times _10 _100. def _10000 := times _10 _1000. (; -#PRINT " 100*10=10*100 ?". -#CHECK times _100 _10 == times _10 _100. +(;# print " 100*10=10*100 ?" #;) +(;# check times _100 _10 == times _10 _100 #;) ;) -#ASSERT times _100 _10 == times _10 _100. +(;# assert times _100 _10 == times _10 _100 #;) (; -#PRINT " 1000*10=10*1000 ?". -#CHECK times _1000 _10 == times _10 _1000. +(;# print " 1000*10=10*1000 ?" #;) +(;# check times _1000 _10 == times _10 _1000 #;) ;) vect : @@ -1291,14 +1291,14 @@ def g := fix_proj set 2 fg_MA fg_FP 1. (; f 0 3 [3,2,1] = 7 ;) (; #PRINT " f 0 3 [3,2,1] = 7 ?". ;) -#ASSERT +assert |- f Z _3 (cons _2 _3 (cons _1 _2 (cons Z _1 nil))) == plus _3 _4. (; #PRINT " f acc (n+1) (cons n a l) = g (acc+a) n l". ;) -#ASSERT +assert |- ( acc:T set nat => n : T set nat => @@ -1334,6 +1334,6 @@ def bug_FP := def bug := fix_proj set 1 bug_MA bug_FP 0. (; This loops ;) -#EVAL[SNF] x : T set nat => bug (Succ x). +(;# eval [SNF] x : T set nat => bug (Succ x) #;) ;) (; Coqine readable = true ;) diff --git a/tests/OK/guard1.dk b/tests/OK/guard1.dk index 6c5c7865..2f3cca07 100644 --- a/tests/OK/guard1.dk +++ b/tests/OK/guard1.dk @@ -11,4 +11,4 @@ def ff : A -> (A -> A) -> A. def pr1 : A -> A -> A. [x,y] pr1 x y --> x. -#ASSERTNOT ff a (y => (pr1 y a)) == a. +(;# assertnot ff a (y => (pr1 y a)) == a #;) diff --git a/tests/OK/guard2.dk b/tests/OK/guard2.dk index 70e71b77..1c69cd56 100644 --- a/tests/OK/guard2.dk +++ b/tests/OK/guard2.dk @@ -8,4 +8,4 @@ g : A -> A. def ff : A -> (A -> A) -> A. [x] ff x (y => {g x}) --> a. -#ASSERTNOT ff a (y => y) == a. +(;# assertnot ff a (y => y) == a #;) diff --git a/tests/OK/guard3.dk b/tests/OK/guard3.dk index 53a09e05..d9e66497 100644 --- a/tests/OK/guard3.dk +++ b/tests/OK/guard3.dk @@ -8,4 +8,4 @@ g : A -> A. def ff : A -> (A -> A) -> A. [x] ff x (y => {g x}) --> a. -#ASSERT ff a (y => (g a)) == a. +(;# assert ff a (y => (g a)) == a #;) diff --git a/tests/OK/ho_bug1.dk b/tests/OK/ho_bug1.dk index 90344903..11fecc4d 100644 --- a/tests/OK/ho_bug1.dk +++ b/tests/OK/ho_bug1.dk @@ -42,5 +42,5 @@ def pr1 (a : A) (c : A) := (; pr2 is the normal form of pr1. ;) def pr2 (__ : A) (c : A) := e1 c b. -#ASSERT pr1 == pr2. -#ASSERT f pr1 == f pr2. +(;# assert pr1 == pr2 #;) +(;# assert f pr1 == f pr2 #;) diff --git a/tests/OK/ho_bug2.dk b/tests/OK/ho_bug2.dk index 2bb28851..96cf9bcb 100644 --- a/tests/OK/ho_bug2.dk +++ b/tests/OK/ho_bug2.dk @@ -10,7 +10,7 @@ a : A. g : A -> A. def test (b : A) := F (x => g x) b. -#PRINT "b:A => a". -#EVAL test. +(;# print "b:A => a" #;) +(;# eval test #;) -#ASSERT test == b : A => a. +(;# assert test == b : A => a #;) diff --git a/tests/OK/ho_match.dk b/tests/OK/ho_match.dk index 0f40a04d..e721bbe2 100644 --- a/tests/OK/ho_match.dk +++ b/tests/OK/ho_match.dk @@ -6,12 +6,12 @@ N : Type. def f : N -> N. [x] f x --> 0. -#ASSERT (y:N => f y) == (y:N => 0). +(;# assert (y:N => f y) == (y:N => 0) #;) def g : (N -> N) -> N. [h] g (x => h x) --> 0. -#ASSERT ( y:N => g (x => 0 ) ) == (y:N => 0). -#ASSERT ( y:N => g (x => x ) ) == (y:N => 0). -#ASSERT ( y:N => g (x => y ) ) == (y:N => 0). -#ASSERT ( y:N => g (x => f y) ) == (y:N => 0). +(;# assert ( y:N => g (x => 0 ) ) == (y:N => 0) #;) +(;# assert ( y:N => g (x => x ) ) == (y:N => 0) #;) +(;# assert ( y:N => g (x => y ) ) == (y:N => 0) #;) +(;# assert ( y:N => g (x => f y) ) == (y:N => 0) #;) diff --git a/tests/OK/ho_nonlinearity.dk b/tests/OK/ho_nonlinearity.dk index cb546977..281e6e47 100644 --- a/tests/OK/ho_nonlinearity.dk +++ b/tests/OK/ho_nonlinearity.dk @@ -9,7 +9,7 @@ c : A -> A -> A. def f : (A -> A -> A -> A -> A) -> (A -> A -> A -> A -> A) -> A. [V] f (y => x => z => V x y z) (x => y => z => V z x y) --> V 1 2 3 4. -#ASSERT +assert |- ( f (y => x => z => u => c (c (c y x) (c u y)) diff --git a/tests/OK/inferingKindForArrowWithCodomainType.dk b/tests/OK/inferingKindForArrowWithCodomainType.dk index 9c30722a..ab04140d 100644 --- a/tests/OK/inferingKindForArrowWithCodomainType.dk +++ b/tests/OK/inferingKindForArrowWithCodomainType.dk @@ -1,8 +1,8 @@ (; OK ;) A : Type. -#INFER A -> Type. -#PRINT "Kind". +(;# infer A -> Type #;) +(;# print "Kind" #;) -#INFER (A -> A) -> A -> Type. -#PRINT "Kind". \ No newline at end of file +(;# infer (A -> A) -> A -> Type #;) +(;# print "Kind" #;) \ No newline at end of file diff --git a/tests/OK/inferingKindForType.dk b/tests/OK/inferingKindForType.dk index e4682dd1..36034006 100644 --- a/tests/OK/inferingKindForType.dk +++ b/tests/OK/inferingKindForType.dk @@ -1,4 +1,4 @@ (; OK ;) -#INFER Type. -#PRINT "Kind". \ No newline at end of file +(;# infer Type #;) +(;# print "Kind" #;) diff --git a/tests/OK/let_syntax.dk b/tests/OK/let_syntax.dk index 3ba812bf..0a56a556 100644 --- a/tests/OK/let_syntax.dk +++ b/tests/OK/let_syntax.dk @@ -10,20 +10,20 @@ def plus : N -> N -> N. [x,y] plus (S x) y --> S (plus x y). -#ASSERT S (S 0) == +assert |- S (S 0) == (x1 : N := 0 ) => (x2 : N := S x1) => (x3 : N := plus x1 x2) => plus x3 x2. -#ASSERT S (S (S 0)) == +assert |- S (S (S 0)) == (x1 : N := 0 ) => (x2 : N := S x1) => (x3 : N := plus x1 x2) => (x4 : N := plus x2 x3) => plus x4 x3. -#ASSERT S (S (S (S (S 0)))) == +assert |- S (S (S (S (S 0)))) == (x1 : N := 0 ) => (x2 : N := S x1) => (x3 : N := plus x1 x2) => @@ -31,14 +31,14 @@ def plus : N -> N -> N. (x5 : N := plus x3 x4) => plus x5 x4. -#ASSERT S (S (S 0)) == +assert |- S (S (S 0)) == (x : N := 0 ) => (x : N := S x) => (x : N := S x) => (x : N := S x) => x. -#ASSERT S (S (S (S 0))) == +assert |- S (S (S (S 0))) == (succ : (N -> N) := S) => (zero : N := 0) => (one : N := succ zero) => diff --git a/tests/OK/miller1.dk b/tests/OK/miller1.dk index cf103647..c4fca9ed 100644 --- a/tests/OK/miller1.dk +++ b/tests/OK/miller1.dk @@ -35,7 +35,7 @@ def flip : (R -> R -> R2) -> (R -> R -> R2). def f : R -> R -> R := x : R => y : R => ch x. -#EVAL grad (trans f). -#EVAL flip (grad f). +(;# eval grad (trans f) #;) +(;# eval flip (grad f) #;) -#ASSERT grad (trans f) == flip (grad f). +(;# assert grad (trans f) == flip (grad f) #;) diff --git a/tests/OK/miller2.dk b/tests/OK/miller2.dk index 3ec85ee2..c063d4e2 100644 --- a/tests/OK/miller2.dk +++ b/tests/OK/miller2.dk @@ -46,7 +46,7 @@ def flip : (R -> R -> R2) -> (R -> R -> R2). def f : R -> R -> R := plus (x : R => y : R => ch x) (x : R => y : R => sh y). -#EVAL flip (grad f). -#EVAL grad (trans f). +(;# eval flip (grad f) #;) +(;# eval grad (trans f) #;) -#ASSERT grad (trans f) == flip (grad f). +(;# assert grad (trans f) == flip (grad f) #;) diff --git a/tests/OK/nested_miller_pattern.dk b/tests/OK/nested_miller_pattern.dk index aba3645b..0ccbdc27 100644 --- a/tests/OK/nested_miller_pattern.dk +++ b/tests/OK/nested_miller_pattern.dk @@ -9,5 +9,5 @@ g : A -> B. def f : (A -> B) -> B. [F] f (x => g F) --> g a. -#EVAL[WHNF] f (x => f (y => g x)). -#EVAL[WHNF] g a. +(;# eval [WHNF] f (x => f (y => g x)) #;) +(;# eval [WHNF] g a #;) diff --git a/tests/OK/nsteps1.dk b/tests/OK/nsteps1.dk index 917119e7..d9bd2a2d 100644 --- a/tests/OK/nsteps1.dk +++ b/tests/OK/nsteps1.dk @@ -3,28 +3,28 @@ def A : Type. [] A --> A -> A. -#EVAL[1,CBV] A. -#EVAL[1,CBN] A. -#EVAL[1,CBSV] A. -#EVAL[0] A -> A. +(;# eval [1,CBV] A #;) +(;# eval [1,CBN] A #;) +(;# eval [1,CBSV] A #;) +(;# eval [0] A -> A #;) -#EVAL[2,CBN] A. -#EVAL[0] A -> A -> A. +(;# eval [2,CBN] A #;) +(;# eval [0] A -> A -> A #;) -#EVAL[3,CBN] A. -#EVAL[0] A -> A -> A -> A. +(;# eval [3,CBN] A #;) +(;# eval [0] A -> A -> A -> A #;) -#EVAL[2,CBV] A. -#EVAL[0] A -> A -> A. +(;# eval [2,CBV] A #;) +(;# eval [0] A -> A -> A #;) -#EVAL[3,CBV] A. -#EVAL[0] A -> A -> A -> A. +(;# eval [3,CBV] A #;) +(;# eval [0] A -> A -> A -> A #;) -#EVAL[2,CBSV] A. -#EVAL[0] (A -> A) -> A. +(;# eval [2,CBSV] A #;) +(;# eval [0] (A -> A) -> A #;) -#EVAL[3,CBSV] A. -#EVAL[0] ((A -> A) -> A) -> A. +(;# eval [3,CBSV] A #;) +(;# eval [0] ((A -> A) -> A) -> A #;) diff --git a/tests/OK/nsteps2.dk b/tests/OK/nsteps2.dk index ecbe2159..c5dd72c8 100644 --- a/tests/OK/nsteps2.dk +++ b/tests/OK/nsteps2.dk @@ -12,15 +12,15 @@ def P : Bool -> Bool. [x] P x --> F. -#EVAL[1,CBV] P b. -#EVAL[0,CBV] P a. +(;# eval [1,CBV] P b #;) +(;# eval [0,CBV] P a #;) -#EVAL[2,CBV] P b. -#EVAL[0,CBV] P T. +(;# eval [2,CBV] P b #;) +(;# eval [0,CBV] P T #;) -#EVAL[3,CBV] P b. -#EVAL[0,CBV] T. +(;# eval [3,CBV] P b #;) +(;# eval [0,CBV] T #;) -#EVAL[1,WHNF] P b. -#EVAL[0] T. +(;# eval [1,WHNF] P b #;) +(;# eval [0] T #;) diff --git a/tests/OK/nsteps3.dk b/tests/OK/nsteps3.dk index a957bfb0..17ca6642 100644 --- a/tests/OK/nsteps3.dk +++ b/tests/OK/nsteps3.dk @@ -16,31 +16,31 @@ def plus : N -> N -> N. def a := plus 2 3. -#EVAL[WHNF,1,CBN] a. +(;# eval [WHNF,1,CBN] a #;) -#EVAL[WHNF,2,CBN] a. +(;# eval [WHNF,2,CBN] a #;) -#EVAL[WHNF,3,CBN] a. +(;# eval [WHNF,3,CBN] a #;) -#EVAL[WHNF,4,CBN] a. +(;# eval [WHNF,4,CBN] a #;) -#EVAL[SNF,6,CBN] a. +(;# eval [SNF,6,CBN] a #;) -#EVAL[1,CBV] a. +(;# eval [1,CBV] a #;) -#EVAL[2,CBV] a. +(;# eval [2,CBV] a #;) -#EVAL[3,CBV] a. +(;# eval [3,CBV] a #;) -#EVAL[4,CBV] a. +(;# eval [4,CBV] a #;) -#EVAL[5,CBV] a. +(;# eval [5,CBV] a #;) -#EVAL[6,CBV] a. +(;# eval [6,CBV] a #;) -#EVAL[7,CBV] a. +(;# eval [7,CBV] a #;) -#EVAL[8,CBV] a. +(;# eval [8,CBV] a #;) -#EVAL[9,CBV] a. +(;# eval [9,CBV] a #;) diff --git a/tests/OK/nsteps4.dk b/tests/OK/nsteps4.dk index a3d2cc90..67cfae84 100644 --- a/tests/OK/nsteps4.dk +++ b/tests/OK/nsteps4.dk @@ -7,45 +7,45 @@ def B := A. a : A. f : A -> A -> A. -#EVAL[CBN ,WHNF] (y:A => f y y) ( (x:B => x) a ). -#EVAL[0] f ((x:B => x) a) ((x:B => x) a). +(;# eval [CBN ,WHNF] (y:A => f y y) ( (x:B => x) a ) #;) +(;# eval [0] f ((x:B => x) a) ((x:B => x) a) #;) -#EVAL[CBN ,SNF] (y:A => f y y) ( (x:B => x) a ). -#EVAL[0] f a a. +(;# eval [CBN ,SNF] (y:A => f y y) ( (x:B => x) a ) #;) +(;# eval [0] f a a #;) -#EVAL[CBV ,WHNF] (y:A => f y y) ( (x:B => x) a ). -#EVAL[0] f a a. +(;# eval [CBV ,WHNF] (y:A => f y y) ( (x:B => x) a ) #;) +(;# eval [0] f a a #;) -#EVAL[CBSV,WHNF] (y:A => f y y) ( (x:B => x) a ). -#EVAL[0] f a a. +(;# eval [CBSV,WHNF] (y:A => f y y) ( (x:B => x) a ) #;) +(;# eval [0] f a a #;) -#EVAL[CBN,1,WHNF] (y:A => f y y) ( (x:B => x) a ). -#EVAL[CBN ,WHNF] (y:A => f y y) ( (x:B => x) a ). +(;# eval [CBN,1,WHNF] (y:A => f y y) ( (x:B => x) a ) #;) +(;# eval [CBN ,WHNF] (y:A => f y y) ( (x:B => x) a ) #;) -#EVAL[CBN,2,SNF] (y:B => f y y) ( (x:B => x) a ). -#EVAL[0] f ((x:B => x) a) a. +(;# eval [CBN,2,SNF] (y:B => f y y) ( (x:B => x) a ) #;) +(;# eval [0] f ((x:B => x) a) a #;) -#EVAL[CBN,3,SNF] (y:B => f y y) ( (x:B => x) a ). -#EVAL[CBN ,SNF] (y:B => f y y) ( (x:B => x) a ). +(;# eval [CBN,3,SNF] (y:B => f y y) ( (x:B => x) a ) #;) +(;# eval [CBN ,SNF] (y:B => f y y) ( (x:B => x) a ) #;) -#EVAL[CBV,1,WHNF] (y:B => f y y) ( (x:B => x) a ). -#EVAL[0] (y:B => f y y) a. +(;# eval [CBV,1,WHNF] (y:B => f y y) ( (x:B => x) a ) #;) +(;# eval [0] (y:B => f y y) a #;) -#EVAL[CBV,2,WHNF] (y:A => f y y) ( (x:B => x) a ). -#EVAL[CBV ,WHNF] (y:B => f y y) ( (x:B => x) a ). +(;# eval [CBV,2,WHNF] (y:A => f y y) ( (x:B => x) a ) #;) +(;# eval [CBV ,WHNF] (y:B => f y y) ( (x:B => x) a ) #;) -#EVAL[CBSV,1,SNF] (y:B => f y y) ( (x:B => x) a ). -#EVAL[0] (y:B => f y y) ((x:A => x) a). +(;# eval [CBSV,1,SNF] (y:B => f y y) ( (x:B => x) a ) #;) +(;# eval [0] (y:B => f y y) ((x:A => x) a) #;) -#EVAL[CBSV,2,SNF] (y:B => f y y) ( (x:B => x) a ). -#EVAL[0] (y:B => f y y) a. +(;# eval [CBSV,2,SNF] (y:B => f y y) ( (x:B => x) a ) #;) +(;# eval [0] (y:B => f y y) a #;) -#EVAL[CBSV,3,SNF] (y:B => f y y) ( (x:B => x) a ). -#EVAL[0] (y:A => f y y) a. +(;# eval [CBSV,3,SNF] (y:B => f y y) ( (x:B => x) a ) #;) +(;# eval [0] (y:A => f y y) a #;) -#EVAL[CBSV,4,SNF] (y:B => f y y) ( (x:B => x) a ). -#EVAL[CBSV ,SNF] (y:B => f y y) ( (x:B => x) a ). +(;# eval [CBSV,4,SNF] (y:B => f y y) ( (x:B => x) a ) #;) +(;# eval [CBSV ,SNF] (y:B => f y y) ( (x:B => x) a ) #;) diff --git a/tests/OK/recursive.dk b/tests/OK/recursive.dk index 4b348b60..8928698f 100644 --- a/tests/OK/recursive.dk +++ b/tests/OK/recursive.dk @@ -12,4 +12,4 @@ def 2pow16 (x:N) := 2pow8 (2pow8 x). def a := 1. -#ASSERT 2pow8 (2pow4 1) == 2pow8 (2pow4 a). +(;# assert 2pow8 (2pow4 1) == 2pow8 (2pow4 a) #;) diff --git a/tests/OK/self_dep.dk b/tests/OK/self_dep.dk index cdfffdc3..c6ed9505 100644 --- a/tests/OK/self_dep.dk +++ b/tests/OK/self_dep.dk @@ -5,5 +5,5 @@ U : A -> Type. a : A. [] A --> U a. -#ASSERT a : U a. -#ASSERT U : U a -> Type. +(;# assert a : U a #;) +(;# assert U : U a -> Type #;) diff --git a/tests/OK/self_dep2.dk b/tests/OK/self_dep2.dk index 49b8b6c5..47a2e244 100644 --- a/tests/OK/self_dep2.dk +++ b/tests/OK/self_dep2.dk @@ -11,5 +11,5 @@ b : B. [] A --> V b. [] B --> U a. -#ASSERT a : V b. -#ASSERT b : U a. +(;# assert a : V b #;) +(;# assert b : U a #;) diff --git a/tests/OK/sharing.dk b/tests/OK/sharing.dk index 4336639d..2e813545 100644 --- a/tests/OK/sharing.dk +++ b/tests/OK/sharing.dk @@ -38,14 +38,14 @@ def test : T -> N. [X] test (c (c X X) (c X X)) --> test X. [X] test (c X X) --> test X. -#EVAL z. -#EVAL test (f 16). +(;# eval z #;) +(;# eval test (f 16) #;) -#EVAL z. -#EVAL test (f 32). +(;# eval z #;) +(;# eval test (f 32) #;) -#EVAL z. -#EVAL test (f 65536). +(;# eval z #;) +(;# eval test (f 65536) #;) def f2 : N -> N -> T. @@ -55,9 +55,9 @@ def f2 : N -> N -> T. def test2 : (N -> T) -> N. [X] test2 (x => X) --> z. -#EVAL z. -#EVAL test2 (x => f2 x 16). +(;# eval z #;) +(;# eval test2 (x => f2 x 16) #;) (; -#EVAL test2 (x => f2 x 32). -#EVAL test2 (x => f2 x 65536). +(;# eval test2 (x => f2 x 32) #;) +(;# eval test2 (x => f2 x 65536) #;) ;) diff --git a/tests/OK/special_idents1.dk b/tests/OK/special_idents1.dk index 11ea3ba1..78b2d684 100644 --- a/tests/OK/special_idents1.dk +++ b/tests/OK/special_idents1.dk @@ -2,17 +2,17 @@ {|∀∃“ç^°}|} : Type. -#EVAL[SNF] {|∀∃“ç^°}|}. -#PRINT "{|∀∃“ç^°}|}". +(;# eval [SNF] {|∀∃“ç^°}|} #;) +(;# print "{|∀∃“ç^°}|}" #;) {|ç^°}|} : Type. def {|\\~~&œe|} : Type. [] {|\\~~&œe|} --> {|ç^°}|}. -#EVAL[SNF] {|\\~~&œe|}. -#PRINT "{|ç^°}|}". +(;# eval [SNF] {|\\~~&œe|} #;) +(;# print "{|ç^°}|}" #;) def {|a|} : Type. def a : Type. -#ASSERTNOT {|a|} == a. +(;# assertnot {|a|} == a #;) diff --git a/tests/OK/underscore1.dk b/tests/OK/underscore1.dk index dfafead9..bdc69881 100644 --- a/tests/OK/underscore1.dk +++ b/tests/OK/underscore1.dk @@ -7,4 +7,4 @@ def B : (A -> A) -> Type. b : B (_ => a). (; This is equivalent to b : B (x => a) ;) -#ASSERT b : B (x => a). +(;# assert b : B (x => a) #;) diff --git a/tests/OK/underscore2.dk b/tests/OK/underscore2.dk index 80399c8f..a41eea94 100644 --- a/tests/OK/underscore2.dk +++ b/tests/OK/underscore2.dk @@ -8,4 +8,4 @@ C : (A -> A) -> Type. [] B (_ => a) --> C (_ => a). (; This is equivalent to B (x => a) --> C (y => a) ;) -#ASSERT B (x => a) == C (y => a). +(;# assert B (x => a) == C (y => a) #;) diff --git a/tests/OK/underscore3.dk b/tests/OK/underscore3.dk index 64c721d8..5e749d3a 100644 --- a/tests/OK/underscore3.dk +++ b/tests/OK/underscore3.dk @@ -7,6 +7,6 @@ def B : A -> Type. (; This is equivalent to B X --> A (with X fresh) ;) a : A. -#ASSERT B a == A. +(;# assert B a == A #;) -#ASSERT (x:A => B x) == (x:A => A). +(;# assert (x:A => B x) == (x:A => A) #;) diff --git a/tests/OK/underscore4.dk b/tests/OK/underscore4.dk index a21a14bc..f4c5b194 100644 --- a/tests/OK/underscore4.dk +++ b/tests/OK/underscore4.dk @@ -7,8 +7,8 @@ def B : (A -> A) -> Type. (; This is equivalent to B (x => X) --> A (with X fresh) ;) a : A. -#ASSERT B (y => a) == A. +(;# assert B (y => a) == A #;) -#ASSERT (z:A => B (y => z)) == (z:A => A). +(;# assert (z:A => B (y => z)) == (z:A => A) #;) -#ASSERTNOT B (y => y) == A. +(;# assertnot B (y => y) == A #;) diff --git a/tests/OK/underscore5.dk b/tests/OK/underscore5.dk index 9ff78cfe..bf960aa0 100644 --- a/tests/OK/underscore5.dk +++ b/tests/OK/underscore5.dk @@ -6,7 +6,7 @@ def B : (A -> A) -> Type. [] B (x => _ x) --> A. (; This is equivalent to B (x => X x) --> A (with X fresh) ;) -#ASSERT B (x => x) == A. +(;# assert B (x => x) == A #;) a : A. -#ASSERT B (x => a) == A. +(;# assert B (x => a) == A #;) diff --git a/tests/OK/underscore6.dk b/tests/OK/underscore6.dk index db3c5da4..b435c84d 100644 --- a/tests/OK/underscore6.dk +++ b/tests/OK/underscore6.dk @@ -7,8 +7,8 @@ def B : (A -> A) -> Type. (; This is equivalent to B (x => X) --> A (with x and X fresh) ;) a : A. -#ASSERT B (y => a) == A. +(;# assert B (y => a) == A #;) -#ASSERT (z:A => B (y => z)) == (z:A => A). +(;# assert (z:A => B (y => z)) == (z:A => A) #;) -#ASSERTNOT B (y => y) == A. +(;# assertnot B (y => y) == A #;) diff --git a/tests/OK/underscore7.dk b/tests/OK/underscore7.dk index e8cfbe7d..3a5c6f3f 100644 --- a/tests/OK/underscore7.dk +++ b/tests/OK/underscore7.dk @@ -7,8 +7,8 @@ def B : (A -> A -> A) -> Type. (; This is equivalent to B (x => y => X x) --> A (with X fresh) ;) a : A. -#ASSERT B (_ => _ => a) == A. +(;# assert B (_ => _ => a) == A #;) -#ASSERT B (u => v => u) == A. +(;# assert B (u => v => u) == A #;) -#ASSERTNOT B (u => v => v) == A. +(;# assertnot B (u => v => v) == A #;) diff --git a/tests/acu/cc.dk b/tests/acu/cc.dk index a6492b65..4af3e881 100644 --- a/tests/acu/cc.dk +++ b/tests/acu/cc.dk @@ -26,7 +26,7 @@ def rule : Sort -> Sort -> Sort. [i,j,k] max (rule i j) (rule i k) --> rule i (max j k). [i,j,k] max (rule j i) (rule k i) --> rule (max j k) i. -#ASSERT ( +assert |- ( u : Sort => v : Sort => w : Sort => @@ -38,7 +38,7 @@ def rule : Sort -> Sort -> Sort. plus (max w v) u ). -#ASSERT ( +assert |- ( x : Sort => y : Sort => rule 0 (rule (plus (plus x 1) (plus y 0)) (plus (plus 0 (plus 0 1)) (plus x y))) @@ -48,7 +48,7 @@ def rule : Sort -> Sort -> Sort. plus (plus y x) 1 ). -#ASSERT ( +assert |- ( x : Sort => y : Sort => rule (rule (plus (plus x 1) (plus y 0)) (plus (plus 0 (plus 0 1)) (plus x y))) 0 @@ -58,7 +58,7 @@ def rule : Sort -> Sort -> Sort. 0 ). -#ASSERT +assert |- ( i : Sort => rule (plus 1 i) 1 ) == ( i : Sort => plus i 1). diff --git a/tests/acu/easy_ac.dk b/tests/acu/easy_ac.dk index 113a9cc3..54bf7e48 100644 --- a/tests/acu/easy_ac.dk +++ b/tests/acu/easy_ac.dk @@ -8,14 +8,14 @@ N : Type. defac mset [N]. -#ASSERT mset 1 0 == mset 0 1. -#ASSERT mset 0 1 == mset 1 0. +(;# assert mset 1 0 == mset 0 1 #;) +(;# assert mset 0 1 == mset 1 0 #;) -#ASSERT mset 0 (mset 1 2) == mset (mset 0 1) 2. -#ASSERT mset 1 (mset 0 2) == mset (mset 0 1) 2. -#ASSERT mset 1 (mset 2 0) == mset (mset 0 1) 2. +(;# assert mset 0 (mset 1 2) == mset (mset 0 1) 2 #;) +(;# assert mset 1 (mset 0 2) == mset (mset 0 1) 2 #;) +(;# assert mset 1 (mset 2 0) == mset (mset 0 1) 2 #;) -#ASSERT +assert |- mset 1 (mset 2 (mset 2 @@ -36,6 +36,6 @@ defac mset [N]. (mset 2 2 ))))))). -#ASSERTNOT mset 1 0 == mset 0 0. -#ASSERTNOT mset 1 0 == mset 1 1. -#ASSERTNOT mset 1 1 == mset 1 0. +(;# assertnot mset 1 0 == mset 0 0 #;) +(;# assertnot mset 1 0 == mset 1 1 #;) +(;# assertnot mset 1 1 == mset 1 0 #;) diff --git a/tests/acu/extra_rules.dk b/tests/acu/extra_rules.dk index 001cd4cb..f0607402 100644 --- a/tests/acu/extra_rules.dk +++ b/tests/acu/extra_rules.dk @@ -11,11 +11,11 @@ defac o [T]. o{t X} --> (x => x) X ;) -#ASSERT o t == y:T => y. -#ASSERT o t t == t. +(;# assert o t == y:T => y #;) +(;# assert o t t == t #;) u : T. -#ASSERT o t u == u. -#ASSERT o u t == u. +(;# assert o t u == u #;) +(;# assert o u t == u #;) -#ASSERT (x:T => o x t) == (z:T => z). +(;# assert (x:T => o x t) == (z:T => z) #;) diff --git a/tests/acu/extra_rules2.dk b/tests/acu/extra_rules2.dk index 63e6fe59..fc0de6c6 100644 --- a/tests/acu/extra_rules2.dk +++ b/tests/acu/extra_rules2.dk @@ -14,16 +14,16 @@ defac o [T]. o{u u X} --> o{t X} ;) -#ASSERT o t t == u. -#ASSERT o u u == t. -#ASSERT o u t == o t u. +(;# assert o t t == u #;) +(;# assert o u u == t #;) +(;# assert o u t == o t u #;) -#ASSERT o (o t u) (o u t) == o u t. -#ASSERT o t (o u (o u t)) == o u t. +(;# assert o (o t u) (o u t) == o u t #;) +(;# assert o t (o u (o u t)) == o u t #;) -#ASSERT o t (o t (o t t)) == t. +(;# assert o t (o t (o t t)) == t #;) -#ASSERT (x:T => o (o t x) t) == (x:T => o u x). -#ASSERT (x:T => o (o x t) t) == (x:T => o u x). -#ASSERT (x:T => o t (o t x)) == (x:T => o x u). -#ASSERT (x:T => o t (o x t)) == (x:T => o x u). +(;# assert (x:T => o (o t x) t) == (x:T => o u x) #;) +(;# assert (x:T => o (o x t) t) == (x:T => o u x) #;) +(;# assert (x:T => o t (o t x)) == (x:T => o x u) #;) +(;# assert (x:T => o t (o x t)) == (x:T => o x u) #;) diff --git a/tests/acu/extra_rules3.dk b/tests/acu/extra_rules3.dk index 7c5cda85..6f659fe3 100644 --- a/tests/acu/extra_rules3.dk +++ b/tests/acu/extra_rules3.dk @@ -13,19 +13,19 @@ defac o [T]. t : T. u : T. -#ASSERT o t t == t. -#ASSERT o u u == u. -#ASSERT o u t == o t u. - -#ASSERT o (o t u) (o u t) == o u t. -#ASSERT o t (o u (o u t)) == o u t. -#ASSERT o t (o t (o t t)) == t. - -#ASSERT o t (o t u) == o u t. -#ASSERT o (o t u) t == o u t. -#ASSERT o (o u t) t == o u t. - -#ASSERT (x:T => o (o t x) t) == (x:T => o t x). -#ASSERT (x:T => o (o x t) t) == (x:T => o t x). -#ASSERT (x:T => o t (o t x)) == (x:T => o x t). -#ASSERT (x:T => o t (o x t)) == (x:T => o x t). +(;# assert o t t == t #;) +(;# assert o u u == u #;) +(;# assert o u t == o t u #;) + +(;# assert o (o t u) (o u t) == o u t #;) +(;# assert o t (o u (o u t)) == o u t #;) +(;# assert o t (o t (o t t)) == t #;) + +(;# assert o t (o t u) == o u t #;) +(;# assert o (o t u) t == o u t #;) +(;# assert o (o u t) t == o u t #;) + +(;# assert (x:T => o (o t x) t) == (x:T => o t x) #;) +(;# assert (x:T => o (o x t) t) == (x:T => o t x) #;) +(;# assert (x:T => o t (o t x)) == (x:T => o x t) #;) +(;# assert (x:T => o t (o x t)) == (x:T => o x t) #;) diff --git a/tests/acu/extra_rules4.dk b/tests/acu/extra_rules4.dk index d23ea95b..bac055b5 100644 --- a/tests/acu/extra_rules4.dk +++ b/tests/acu/extra_rules4.dk @@ -18,21 +18,21 @@ defac o [T]. t : T. u : T. -#ASSERT o t t == f t. -#ASSERT o u u == f u. -#ASSERT o u t == o t u. +(;# assert o t t == f t #;) +(;# assert o u u == f u #;) +(;# assert o u t == o t u #;) -#ASSERT f (o u t) == o (f u) (f t). +(;# assert f (o u t) == o (f u) (f t) #;) -#ASSERT o (o t u) (o u t) == o (f u) (f t). -#ASSERT o t (o u (o u t)) == o (f u) (f t). +(;# assert o (o t u) (o u t) == o (f u) (f t) #;) +(;# assert o t (o u (o u t)) == o (f u) (f t) #;) -#ASSERT o t (o t (o t t)) == f (f t). +(;# assert o t (o t (o t t)) == f (f t) #;) -#ASSERT (x:T => o (o t x) t) == (x:T => o (f t) x). -#ASSERT (x:T => o (o x t) t) == (x:T => o (f t) x). -#ASSERT (x:T => o t (o t x)) == (x:T => o x (f t)). -#ASSERT (x:T => o t (o x t)) == (x:T => o x (f t)). +(;# assert (x:T => o (o t x) t) == (x:T => o (f t) x) #;) +(;# assert (x:T => o (o x t) t) == (x:T => o (f t) x) #;) +(;# assert (x:T => o t (o t x)) == (x:T => o x (f t)) #;) +(;# assert (x:T => o t (o x t)) == (x:T => o x (f t)) #;) -#ASSERT (x:T => o x (o t x)) == (x:T => o t (f x)). -#ASSERT (x:T => o t (o x x)) == (x:T => o t (f x)). +(;# assert (x:T => o x (o t x)) == (x:T => o t (f x)) #;) +(;# assert (x:T => o t (o x x)) == (x:T => o t (f x)) #;) diff --git a/tests/acu/fail_ac.dk b/tests/acu/fail_ac.dk index a85ae353..4b4dfcc5 100644 --- a/tests/acu/fail_ac.dk +++ b/tests/acu/fail_ac.dk @@ -6,5 +6,5 @@ f : N -> N -> N. defac g [N]. [] g --> f. -#EVAL[WHNF] g. +(;# eval [WHNF] g #;) (; This forces impossible computation of g's decision tree ;) diff --git a/tests/acu/min_ac.dk b/tests/acu/min_ac.dk index 0e7422f7..8068c115 100644 --- a/tests/acu/min_ac.dk +++ b/tests/acu/min_ac.dk @@ -14,11 +14,11 @@ defac min [N]. [] min 0 --> (x : N => 0) [x,y] min (S x) (S y) --> S (min x y). -#ASSERT min 3 (min 1 2) == 1. +(;# assert min 3 (min 1 2) == 1 #;) defac max [N]. [] min 0 --> (x : N => x) [x,y] min (S x) (S y) --> S (min x y). -#ASSERT min 3 (min 1 2) == 3. +(;# assert min 3 (min 1 2) == 3 #;) diff --git a/tests/eta/KO/eta_0.dk b/tests/eta/KO/eta_0.dk index d701ffda..74b43dc2 100644 --- a/tests/eta/KO/eta_0.dk +++ b/tests/eta/KO/eta_0.dk @@ -2,4 +2,4 @@ A : Type. x : A -> A. -#ASSERT x == y : A => x y. +(;# assert x == y : A => x y #;) diff --git a/tests/eta/KO/eta_1b.dk b/tests/eta/KO/eta_1b.dk index 10c8ce4d..feba2ab0 100644 --- a/tests/eta/KO/eta_1b.dk +++ b/tests/eta/KO/eta_1b.dk @@ -14,4 +14,4 @@ f1 : B. def f2 := x:A => f1 x. def f3 := x:A => f2 x. -#ASSERT T f2 (c f3) == c f1. +(;# assert T f2 (c f3) == c f1 #;) diff --git a/tests/eta/KO/eta_2.dk b/tests/eta/KO/eta_2.dk index 04e31706..26e0bbe1 100644 --- a/tests/eta/KO/eta_2.dk +++ b/tests/eta/KO/eta_2.dk @@ -14,4 +14,4 @@ def l := (X:type => x:(T X) => g X x) paa foo. def r := (f:(T paa) => g paa (x:T a => f x)) foo. -#ASSERT l == r. +(;# assert l == r #;) diff --git a/tests/eta/OK/eta_0.dk b/tests/eta/OK/eta_0.dk index d701ffda..7c7d6818 100644 --- a/tests/eta/OK/eta_0.dk +++ b/tests/eta/OK/eta_0.dk @@ -2,4 +2,4 @@ A : Type. x : A -> A. -#ASSERT x == y : A => x y. +assert |- x == y : A => x y. diff --git a/tests/eta/OK/eta_0b.dk b/tests/eta/OK/eta_0b.dk index 4641e8a3..c9d8ade3 100644 --- a/tests/eta/OK/eta_0b.dk +++ b/tests/eta/OK/eta_0b.dk @@ -2,4 +2,4 @@ A : Type. x : A -> A. -#ASSERTNOT x == y : A => x y. +(;# assertnot x == y : A => x y #;) diff --git a/tests/eta/OK/eta_1.dk b/tests/eta/OK/eta_1.dk index a81b7d83..fe457560 100644 --- a/tests/eta/OK/eta_1.dk +++ b/tests/eta/OK/eta_1.dk @@ -14,4 +14,4 @@ f1 : B. def f2 := x:A => f1 x. def f3 := x:A => f2 x. -#ASSERT T f2 (c f3) == c f1. +(;# assert T f2 (c f3) == c f1 #;) diff --git a/tests/eta/OK/eta_2.dk b/tests/eta/OK/eta_2.dk index 10ead91d..c8277f8e 100644 --- a/tests/eta/OK/eta_2.dk +++ b/tests/eta/OK/eta_2.dk @@ -14,4 +14,4 @@ def l := (X:type => x:(T X) => g X x) paa foo. def r := (f:(T paa) => g paa (x:T a => f x)) foo. -#ASSERT l == r. +(;# assert l == r #;) diff --git a/tests/eta/OK/eta_2b.dk b/tests/eta/OK/eta_2b.dk index aba8c8dd..5e3d48b0 100644 --- a/tests/eta/OK/eta_2b.dk +++ b/tests/eta/OK/eta_2b.dk @@ -14,4 +14,4 @@ def l := (X:type => x:(T X) => g X x) paa foo. def r := (f:(T paa) => g paa (x:T a => f x)) foo. -#ASSERTNOT l == r. +(;# assertnot l == r #;) From 223a403c93d95c8804788cf4821dc7553a8637cf Mon Sep 17 00:00:00 2001 From: DwarfMaster Date: Mon, 13 Jun 2022 12:54:11 +0200 Subject: [PATCH 4/4] Add support for context in tests --- api/dep.ml | 11 ++++++++--- api/pp.ml | 6 +++--- api/processor.ml | 24 +++++++++++------------ parsing/entry.ml | 12 ++++++------ parsing/entry.mli | 6 +++--- parsing/menhir_parser.mly | 40 +++++++++++++++++++++++++------------- parsing/scoping.ml | 10 ++++++++++ parsing/scoping.mli | 2 ++ tests/OK/assert/context.dk | 7 +++++++ 9 files changed, 77 insertions(+), 41 deletions(-) create mode 100644 tests/OK/assert/context.dk diff --git a/api/dep.ml b/api/dep.ml index beb0af15..ede80c08 100644 --- a/api/dep.ml +++ b/api/dep.ml @@ -121,6 +121,11 @@ let rec mk_term t = | Lam (_, _, Some ty, te) -> mk_term ty; mk_term te | Pi (_, _, a, b) -> mk_term a; mk_term b +let rec mk_typed_context ctx = + match ctx with + | [] -> () + | (_,_,ty) :: tl -> mk_term ty; mk_typed_context tl + let rec mk_pattern p = let open Rule in match p with @@ -157,9 +162,9 @@ let handle_entry e = List.iter mk_rule rs | Eval (_, _, te) -> mk_term te | Infer (_, _, te) -> mk_term te - | Check (_, _, _, Convert (t1, t2)) -> mk_term t1; mk_term t2 - | Check (_, _, _, HasType (te, ty)) -> mk_term te; mk_term ty - | Check (_, _, _, Typeable te) -> mk_term te + | Check (_, _, _, Convert (ctx, t1, t2)) -> mk_typed_context ctx; mk_term t1; mk_term t2 + | Check (_, _, _, HasType (ctx, te, ty)) -> mk_typed_context ctx; mk_term te; mk_term ty + | Check (_, _, _, Typeable (ctx, te)) -> mk_typed_context ctx; mk_term te | DTree (_, _, _) -> () | Print (_, _) -> () | Name (_, _) -> () diff --git a/api/pp.ml b/api/pp.ml index 81edf84b..9dfc64e5 100644 --- a/api/pp.ml +++ b/api/pp.ml @@ -323,11 +323,11 @@ module Make (S : Sig) : Printer = struct let cmd = if assrt then "#ASSERT" else "#CHECK" in let neg = if neg then "NOT" else "" in match test with - | Convert (t1, t2) -> + | Convert (_, t1, t2) -> fprintf fmt "%s%s %a ==@ %a.@." cmd neg print_term t1 print_term t2 - | HasType (te, ty) -> + | HasType (_, te, ty) -> fprintf fmt "%s%s %a ::@ %a.@." cmd neg print_term te print_term ty - | Typeable te -> + | Typeable (_, te) -> fprintf fmt "%s%s %a.@." cmd neg pp_term te) | DTree (_, m, v) -> ( match m with diff --git a/api/processor.ml b/api/processor.ml index b3d240e3..e1836912 100644 --- a/api/processor.ml +++ b/api/processor.ml @@ -54,22 +54,22 @@ module MakeTypeChecker (Env : CustomEnv) : S with type t = unit = struct let ty = Env.infer env te in let rty = Env.reduction env ~red ty in Format.printf "%a@." Pp.print_term rty - | Check (lc, assrt, neg, Convert (t1, t2)) -> ( - let succ = Env.are_convertible env t1 t2 <> neg in + | Check (lc, assrt, neg, Convert (ctx, t1, t2)) -> ( + let succ = Env.are_convertible env ~ctx:ctx t1 t2 <> neg in match (succ, assrt) with | true, false -> Format.printf "YES@." | true, true -> () | false, false -> Format.printf "NO@." | false, true -> raise @@ Entry.Assert_error lc) - | Check (lc, assrt, neg, HasType (te, ty)) -> ( - let succ = try Env.check env te ty; not neg with _ -> neg in + | Check (lc, assrt, neg, HasType (ctx, te, ty)) -> ( + let succ = try Env.check env ~ctx:ctx te ty; not neg with _ -> neg in match (succ, assrt) with | true, false -> Format.printf "YES@." | true, true -> () | false, false -> Format.printf "NO@." | false, true -> raise @@ Entry.Assert_error lc) - | Check (lc, assrt, neg, Typeable te) -> ( - let succ = try ignore (Env.infer env te); not neg with _ -> neg in + | Check (lc, assrt, neg, Typeable (ctx,te)) -> ( + let succ = try ignore (Env.infer env ~ctx:ctx te); not neg with _ -> neg in match (succ,assrt) with | true, false -> Format.printf "YES@." | true, true -> () @@ -178,22 +178,22 @@ module MakeTopLevel (Env : CustomEnv) : S with type t = unit = struct let ty = Env.infer env te in let rty = Env.reduction env ~red ty in Format.printf "%a@." Printer.print_term rty - | Check (lc, assrt, neg, Convert (t1, t2)) -> ( - let succ = Env.are_convertible env t1 t2 <> neg in + | Check (lc, assrt, neg, Convert (ctx, t1, t2)) -> ( + let succ = Env.are_convertible env ~ctx:ctx t1 t2 <> neg in match (succ, assrt) with | true, false -> Format.printf "YES@." | true, true -> () | false, false -> Format.printf "NO@." | false, true -> raise @@ Entry.Assert_error lc) - | Check (lc, assrt, neg, HasType (te, ty)) -> ( - let succ = try Env.check env te ty; not neg with _ -> neg in + | Check (lc, assrt, neg, HasType (ctx, te, ty)) -> ( + let succ = try Env.check env ~ctx:ctx te ty; not neg with _ -> neg in match (succ, assrt) with | true, false -> Format.printf "YES@." | true, true -> () | false, false -> Format.printf "NO@." | false, true -> raise @@ Entry.Assert_error lc) - | Check (lc, assrt, neg, Typeable te) -> ( - let succ = try ignore (Env.infer env te); not neg with _ -> neg in + | Check (lc, assrt, neg, Typeable (ctx,te)) -> ( + let succ = try ignore (Env.infer env ~ctx:ctx te); not neg with _ -> neg in match (succ,assrt) with | true, false -> Format.printf "YES@." | true, true -> () diff --git a/parsing/entry.ml b/parsing/entry.ml index f84f8f5d..44506a8f 100644 --- a/parsing/entry.ml +++ b/parsing/entry.ml @@ -8,9 +8,9 @@ type is_assertion = bool type should_fail = bool -type test = Convert of term * term - | HasType of term * term - | Typeable of term +type test = Convert of typed_context * term * term + | HasType of typed_context * term * term + | Typeable of typed_context * term exception Assert_error of loc @@ -67,11 +67,11 @@ let pp_entry fmt e = let cmd = if assrt then "#ASSERT" else "#CHECK" in let neg = if neg then "NOT" else "" in match test with - | Convert (t1, t2) -> + | Convert (_, t1, t2) -> fprintf fmt "%s%s %a ==@ %a.@." cmd neg pp_term t1 pp_term t2 - | HasType (te, ty) -> + | HasType (_, te, ty) -> fprintf fmt "%s%s %a ::@ %a.@." cmd neg pp_term te pp_term ty - | Typeable te -> + | Typeable (_, te) -> fprintf fmt "%s%s %a.@." cmd neg pp_term te) | DTree (_, m, v) -> ( match m with diff --git a/parsing/entry.mli b/parsing/entry.mli index df8365b9..eba34254 100644 --- a/parsing/entry.mli +++ b/parsing/entry.mli @@ -10,9 +10,9 @@ type should_fail = bool (** Possible tests in source files. *) type test = - | Convert of term * term (** Convertibility between the two given terms. *) - | HasType of term * term (** Typability test, given a term and a type. *) - | Typeable of term (** Typability test, without the type *) + | Convert of typed_context * term * term (** Convertibility between the two given terms. *) + | HasType of typed_context * term * term (** Typability test, given a term and a type. *) + | Typeable of typed_context * term (** Typability test, without the type *) exception Assert_error of loc diff --git a/parsing/menhir_parser.mly b/parsing/menhir_parser.mly index c62ed852..0d728ad4 100644 --- a/parsing/menhir_parser.mly +++ b/parsing/menhir_parser.mly @@ -146,12 +146,18 @@ line: | rs=rule+ DOT {fun md -> Rules(loc_of_rs rs,(List.map (scope_rule md) rs))} - | ASSERT QUESTION te=term DOT - {fun md -> Check($1, true, false, Typeable(scope_term md [] te))} - | ASSERT VDASH t1=aterm EQUAL t2=term DOT - {fun md -> Check($1, true , false, Convert(scope_term md [] t1, scope_term md [] t2))} - | ASSERT VDASH te=aterm COLON ty=term DOT - {fun md -> Check($1, true, false, HasType(scope_term md [] te, scope_term md [] ty))} + | ASSERT ctx=assert_ctx QUESTION te=term DOT + {fun md -> Check($1, true, false, + let ctx = scope_ctx md ctx in + Typeable(ctx, scope_term md ctx te))} + | ASSERT ctx=assert_ctx VDASH t1=aterm EQUAL t2=term DOT + {fun md -> Check($1, true , false, + let ctx = scope_ctx md ctx in + Convert(ctx, scope_term md ctx t1, scope_term md ctx t2))} + | ASSERT ctx=assert_ctx VDASH te=aterm COLON ty=term DOT + {fun md -> Check($1, true, false, + let ctx = scope_ctx md ctx in + HasType(ctx, scope_term md ctx te, scope_term md ctx ty))} | PRAGMA_EVAL te=term PRAGMA_END {fun md -> Eval($1, default_cfg, scope_term md [] te)} @@ -163,22 +169,22 @@ line: {fun md -> Infer($1, cfg, scope_term md [] te)} | PRAGMA_CHECK te=aterm COLON ty=term PRAGMA_END - {fun md -> Check($1, false, false, HasType(scope_term md [] te, scope_term md [] ty))} + {fun md -> Check($1, false, false, HasType([], scope_term md [] te, scope_term md [] ty))} | PRAGMA_CHECKNOT te=aterm COLON ty=term PRAGMA_END - {fun md -> Check($1, false, true , HasType(scope_term md [] te, scope_term md [] ty))} + {fun md -> Check($1, false, true , HasType([], scope_term md [] te, scope_term md [] ty))} | PRAGMA_ASSERT te=aterm COLON ty=term PRAGMA_END - {fun md -> Check($1, true , false, HasType(scope_term md [] te, scope_term md [] ty))} + {fun md -> Check($1, true , false, HasType([], scope_term md [] te, scope_term md [] ty))} | PRAGMA_ASSERTNOT te=aterm COLON ty=term PRAGMA_END - {fun md -> Check($1, true , true , HasType(scope_term md [] te, scope_term md [] ty))} + {fun md -> Check($1, true , true , HasType([], scope_term md [] te, scope_term md [] ty))} | PRAGMA_CHECK t1=aterm EQUAL t2=term PRAGMA_END - {fun md -> Check($1, false, false, Convert(scope_term md [] t1, scope_term md [] t2))} + {fun md -> Check($1, false, false, Convert([], scope_term md [] t1, scope_term md [] t2))} | PRAGMA_CHECKNOT t1=aterm EQUAL t2=term PRAGMA_END - {fun md -> Check($1, false, true , Convert(scope_term md [] t1, scope_term md [] t2))} + {fun md -> Check($1, false, true , Convert([], scope_term md [] t1, scope_term md [] t2))} | PRAGMA_ASSERT t1=aterm EQUAL t2=term PRAGMA_END - {fun md -> Check($1, true , false, Convert(scope_term md [] t1, scope_term md [] t2))} + {fun md -> Check($1, true , false, Convert([], scope_term md [] t1, scope_term md [] t2))} | PRAGMA_ASSERTNOT t1=aterm EQUAL t2=term PRAGMA_END - {fun md -> Check($1, true , true , Convert(scope_term md [] t1, scope_term md [] t2))} + {fun md -> Check($1, true , true , Convert([], scope_term md [] t1, scope_term md [] t2))} | PRAGMA_PRINT STRING PRAGMA_END {fun _ -> Print($1, $2)} @@ -261,4 +267,10 @@ term: {PreLam (fst $1, snd $1, Some $3, $5)} | LEFTPAR pid COLON aterm DEF aterm RIGHTPAR FATARROW term { PreApp (PreLam (fst $2, snd $2, Some $4, $9), $6, []) } + +assert_ctx: separated_list(COMMA, assert_decl) { $1 } + +assert_decl: + | id=ID COLON ty=term + { (fst id, snd id, ty) } %% diff --git a/parsing/scoping.ml b/parsing/scoping.ml index 943b57c3..43673a71 100644 --- a/parsing/scoping.ml +++ b/parsing/scoping.ml @@ -36,6 +36,16 @@ let rec t_of_pt md (ctx : ident list) (pte : preterm) : term = let scope_term md ctx (pte : preterm) : term = t_of_pt md (List.map (fun (_, x, _) -> x) ctx) pte +(* Expects the preterm list in reverse *) +let rec scope_ctx' md : Preterm.preterm context -> typed_context = function + | [] -> [] + | (l,id,ty) :: tl -> + let scp_ctx = scope_ctx' md tl in + let ty = scope_term md scp_ctx ty in + (l, id, ty) :: scp_ctx + +let scope_ctx md ctx = scope_ctx' md (List.rev ctx) + (******************************************************************************) type pre_context = preterm option context diff --git a/parsing/scoping.mli b/parsing/scoping.mli index 5f39a956..16ec8a89 100644 --- a/parsing/scoping.mli +++ b/parsing/scoping.mli @@ -8,4 +8,6 @@ exception Scoping_error of loc * string val scope_term : mident -> typed_context -> Preterm.preterm -> term +val scope_ctx : mident -> Preterm.preterm context -> typed_context + val scope_rule : mident -> Preterm.prule -> Rule.partially_typed_rule diff --git a/tests/OK/assert/context.dk b/tests/OK/assert/context.dk new file mode 100644 index 00000000..15d7e349 --- /dev/null +++ b/tests/OK/assert/context.dk @@ -0,0 +1,7 @@ +(; OK ;) + +assert A : Type ? A. +assert A : Type |- A : Type. +assert A : Type, a : A |- A : Type. +assert A : Type, a : A |- a : A. +assert A : Type, a : A |- a == a.