Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

New syntax for pragmas and assertions #276

Open
wants to merge 4 commits into
base: new_dedukti
Choose a base branch
from
Open

New syntax for pragmas and assertions #276

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
494fb52
Add new check to the api
dwarfmaster Jun 8, 2022
5189a13
Implement new pragma syntax without contexts
dwarfmaster Jun 8, 2022
7b5ceea
Update tests
dwarfmaster Jun 8, 2022
223a403
Add support for context in tests
dwarfmaster Jun 13, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 8 additions & 2 deletions api/dep.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -157,8 +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 (_, _, _, 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 (_, _) -> ()
Expand Down
8 changes: 5 additions & 3 deletions api/pp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -323,10 +323,12 @@ 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) ->
fprintf fmt "%s%s %a ::@ %a.@." cmd neg print_term te print_term ty)
| HasType (_, te, 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
Expand Down
30 changes: 22 additions & 8 deletions api/processor.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,20 +54,27 @@ 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 (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 -> ()
| 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
Expand Down Expand Up @@ -171,20 +178,27 @@ 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 (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 -> ()
| 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
Expand Down
12 changes: 8 additions & 4 deletions parsing/entry.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 typed_context * term * term
| HasType of typed_context * term * term
| Typeable of typed_context * term

exception Assert_error of loc

Expand Down Expand Up @@ -65,10 +67,12 @@ 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) ->
fprintf fmt "%s%s %a ::@ %a.@." cmd neg pp_term te pp_term ty)
| HasType (_, te, 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
Expand Down
5 changes: 3 additions & 2 deletions parsing/entry.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 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 *)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not call it infer?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it's because it is an assertion, so we are thinking of a predicate rather than a computation. In particular, the Dedukti command Typeable(c, t) should not print anything. It could be IsTypeable, if you want to stress out the predicate.


exception Assert_error of loc

Expand Down
93 changes: 51 additions & 42 deletions parsing/lexer.mll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand All @@ -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 }
Expand Down
91 changes: 59 additions & 32 deletions parsing/menhir_parser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,14 +57,18 @@ let loc_of_rs = function
%token RIGHTBRA
%token LEFTSQU
%token RIGHTSQU
%token <Kernel.Basic.loc> EVAL
%token <Kernel.Basic.loc> INFER
%token <Kernel.Basic.loc> CHECK
%token <Kernel.Basic.loc> CHECKNOT
%token VDASH
%token QUESTION
%token <Kernel.Basic.loc> PRAGMA_EVAL
%token <Kernel.Basic.loc> PRAGMA_INFER
%token <Kernel.Basic.loc> PRAGMA_CHECK
%token <Kernel.Basic.loc> PRAGMA_CHECKNOT
%token <Kernel.Basic.loc> PRAGMA_ASSERT
%token <Kernel.Basic.loc> PRAGMA_ASSERTNOT
%token <Kernel.Basic.loc> PRAGMA_PRINT
%token <Kernel.Basic.loc> PRAGMA_GDT
%token <Kernel.Basic.loc> PRAGMA_END
%token <Kernel.Basic.loc> ASSERT
%token <Kernel.Basic.loc> ASSERTNOT
%token <Kernel.Basic.loc> PRINT
%token <Kernel.Basic.loc> GDT
%token <Kernel.Basic.loc> UNDERSCORE
%token <Kernel.Basic.loc*Basic.mident> NAME
%token <Kernel.Basic.loc*Basic.mident> REQUIRE
Expand Down Expand Up @@ -142,36 +146,53 @@ line:
| rs=rule+ DOT
{fun md -> Rules(loc_of_rs rs,(List.map (scope_rule md) rs))}

| EVAL te=term DOT
| 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)}
| 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
{fun md -> Check($1, false, false, HasType(scope_term md [] te, scope_term md [] ty))}
| CHECKNOT te=aterm COLON ty=term DOT
{fun md -> Check($1, false, true , HasType(scope_term md [] te, scope_term md [] ty))}
| ASSERT te=aterm COLON ty=term DOT
{fun md -> Check($1, true , false, HasType(scope_term md [] te, scope_term md [] ty))}
| ASSERTNOT te=aterm COLON ty=term DOT
{fun md -> Check($1, true , true , HasType(scope_term md [] te, scope_term md [] ty))}

| CHECK t1=aterm EQUAL t2=term DOT
{fun md -> Check($1, false, false, Convert(scope_term md [] t1, scope_term md [] t2))}
| CHECKNOT t1=aterm EQUAL t2=term DOT
{fun md -> Check($1, false, true , Convert(scope_term md [] t1, scope_term md [] t2))}
| ASSERT t1=aterm EQUAL t2=term DOT
{fun md -> Check($1, true , false, Convert(scope_term md [] t1, scope_term md [] t2))}
| ASSERTNOT t1=aterm EQUAL t2=term DOT
{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_CHECK te=aterm COLON ty=term PRAGMA_END
{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))}
| PRAGMA_ASSERT te=aterm COLON ty=term PRAGMA_END
{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))}

| PRAGMA_CHECK t1=aterm EQUAL t2=term PRAGMA_END
{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))}
| PRAGMA_ASSERT t1=aterm EQUAL t2=term PRAGMA_END
{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))}

| 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}
Expand Down Expand Up @@ -246,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) }
%%
10 changes: 10 additions & 0 deletions parsing/scoping.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions parsing/scoping.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading