Skip to content

Commit e9096be

Browse files
thibautbenjaminthibautbenjamin
committed
implementation of the kolmogorov-style printing
1 parent fbce6f9 commit e9096be

10 files changed

Lines changed: 275 additions & 67 deletions

File tree

‎lib/command.ml‎

Lines changed: 21 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -15,28 +15,14 @@ type cmd =
1515
| Decl of Var.t * (Var.t * tyR) list * tmR * tyR option
1616
| Decl_builtin of Var.t * builtin
1717
| Set of string * string
18+
| Benchmark of (Var.t * tyR) list * tmR
19+
| Benchmark_builtin of builtin
1820

1921
type prog = cmd list
2022

2123
let postprocess_fn : (ctx -> tm -> ctx * tm) ref = ref (fun c e -> (c, e))
2224

2325
let exec_coh v ps ty =
24-
(* let t = Sys.time () in
25-
let _ = Eh.full_eh 6 3 2 in
26-
let t_diff = Sys.time () -. t in
27-
Io.debug "time taken: %f" t_diff;
28-
let t = Sys.time () in
29-
let _ = Eh.full_eh 6 2 3 in
30-
let t_diff = Sys.time () -. t in
31-
Io.debug "time taken: %f" t_diff;
32-
let t = Sys.time () in
33-
let _ = Eh.full_eh_alt 6 3 2 in
34-
let t_diff = Sys.time () -. t in
35-
Io.debug "time taken: %f" t_diff;
36-
let t = Sys.time () in
37-
let _ = Eh.full_eh_alt 6 2 3 in
38-
let t_diff = Sys.time () -. t in
39-
Io.debug "time taken: %f" t_diff; *)
4026
let ps, ty = Elaborate.ty_in_ps ps ty in
4127
Environment.add_coh v ps ty
4228

@@ -127,8 +113,7 @@ let exec_cmd cmd =
127113
Io.info
128114
(lazy
129115
(Printf.sprintf "successfully defined term %s of type %s"
130-
(Printing.print_kolmogorov tm)
131-
(Printing.ty_to_string ty)))
116+
(Printing.tm_to_string tm) (Printing.ty_to_string ty)))
132117
| Set (o, v) -> (
133118
try exec_set o v with
134119
| UnknownOption o -> Error.unknown_option o
@@ -150,6 +135,24 @@ let exec_cmd cmd =
150135
(Printf.sprintf "successfully defined term %s of type %s"
151136
(Environment.value_to_string e)
152137
(Printing.ty_to_string ty)))
138+
| Benchmark (l, e) ->
139+
let e, _ = check l e None in
140+
Io.info
141+
(lazy
142+
(Printf.sprintf "term computes to:\n %s"
143+
(Printing.print_kolmogorov e)))
144+
| Benchmark_builtin b ->
145+
let e, _ = exec_check_builtin b in
146+
let e =
147+
match e with
148+
| Environment.Coh _ ->
149+
Error.fatal "bechmarking a builtin resolving to a coherence"
150+
| Environment.Tm e -> Tm.develop e
151+
in
152+
Io.info
153+
(lazy
154+
(Printf.sprintf "term computes to:\n %s"
155+
(Printing.print_kolmogorov e)))
153156

154157
type next = Abort | KeepGoing | Interactive
155158

‎lib/command.mli‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,8 @@ type cmd =
1010
| Decl of Var.t * (Var.t * tyR) list * tmR * tyR option
1111
| Decl_builtin of Var.t * builtin
1212
| Set of string * string
13+
| Benchmark of (Var.t * tyR) list * tmR
14+
| Benchmark_builtin of builtin
1315

1416
type prog = cmd list
1517

‎lib/equality.ml‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,9 @@ struct
2020
val func_data : TmT.t -> (Var.t * int) list list
2121
val develop : TmT.t -> Unchecked_types(CohT)(TmT).tm
2222
val name : TmT.t -> string
23+
val full_name : TmT.t -> string
2324
val ctx : TmT.t -> ctx
25+
val is_equal : TmT.t -> TmT.t -> bool
2426

2527
val apply :
2628
(Unchecked_types(CohT)(TmT).ctx -> Unchecked_types(CohT)(TmT).ctx) ->
@@ -38,8 +40,10 @@ struct
3840
let rec is_equal_ps ps1 ps2 =
3941
match (ps1, ps2) with
4042
| Br [], Br [] -> true
41-
| Br (ps1 :: l1), Br (ps2 :: l2) ->
42-
is_equal_ps ps1 ps2 && List.for_all2 is_equal_ps l1 l2
43+
| Br (ps1 :: l1), Br (ps2 :: l2) -> (
44+
is_equal_ps ps1 ps2
45+
&&
46+
try List.for_all2 is_equal_ps l1 l2 with Invalid_argument _ -> true)
4347
| Br [], Br (_ :: _) | Br (_ :: _), Br [] -> false
4448

4549
let rec is_equal_ty ty1 ty2 =
@@ -62,7 +66,6 @@ struct
6266
| Meta_tm i, Meta_tm j -> i = j
6367
| Coh (coh1, s1), Coh (coh2, s2) ->
6468
Coh.is_equal coh1 coh2 && is_equal_sub_ps s1 s2
65-
(* Define check_equal_sub and Tm.develop *)
6669
| App (t1, s1), App (t2, s2) when t1 == t2 -> is_equal_sub s1 s2
6770
| App (t, s), ((Coh _ | App _ | Var _) as tm2)
6871
| ((Coh _ | Var _) as tm2), App (t, s) ->

‎lib/equality.mli‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
open Common
2+
open Unchecked_types
3+
4+
module Equality (Coh : sig
5+
type t
6+
end) (Tm : sig
7+
type t
8+
end) : sig
9+
open Unchecked_types(Coh)(Tm)
10+
11+
module Make (_ : sig
12+
val forget : Coh.t -> ps * Unchecked_types(Coh)(Tm).ty * pp_data
13+
val to_string : ?unroll:bool -> Coh.t -> string
14+
val func_data : Coh.t -> (Var.t * int) list list
15+
val is_equal : Coh.t -> Coh.t -> bool
16+
val check : ps -> ty -> pp_data -> Coh.t
17+
end) (_ : sig
18+
val func_data : Tm.t -> (Var.t * int) list list
19+
val develop : Tm.t -> Unchecked_types(Coh)(Tm).tm
20+
val name : Tm.t -> string
21+
val full_name : Tm.t -> string
22+
val ctx : Tm.t -> ctx
23+
val is_equal : Tm.t -> Tm.t -> bool
24+
25+
val apply :
26+
(Unchecked_types(Coh)(Tm).ctx -> Unchecked_types(Coh)(Tm).ctx) ->
27+
(Unchecked_types(Coh)(Tm).tm -> Unchecked_types(Coh)(Tm).tm) ->
28+
(pp_data -> pp_data) ->
29+
Tm.t ->
30+
Tm.t * Unchecked_types(Coh)(Tm).sub
31+
end) : sig
32+
val check_equal_ctx : ctx -> ctx -> unit
33+
val check_equal_ps : ps -> ps -> unit
34+
val check_equal_ty : ty -> ty -> unit
35+
val check_equal_tm : tm -> tm -> unit
36+
val check_equal_sub_ps : sub_ps -> sub_ps -> unit
37+
val is_equal_ctx : ctx -> ctx -> bool
38+
val is_equal_ps : ps -> ps -> bool
39+
val is_equal_ty : ty -> ty -> bool
40+
val is_equal_tm : tm -> tm -> bool
41+
val is_equal_sub : sub -> sub -> bool
42+
end
43+
end

‎lib/kernel.ml‎

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ open Common
33
open Unchecked_types
44
open Unchecked
55
open Printing
6+
open Equality
67

78
exception IsObj
89
exception IsCoh
@@ -106,7 +107,7 @@ end = struct
106107
module Unchecked = U.Make (Coh) (Tm)
107108
module P = Printing (Coh) (Tm)
108109
module Printing = P.Make (Coh) (Tm)
109-
module E = Equality.Equality (Coh) (Tm)
110+
module E = Equality (Coh) (Tm)
110111
module Equality = E.Make (Coh) (Tm)
111112

112113
let tbl : (ctx, Ctx.t) Hashtbl.t = Hashtbl.create 7829
@@ -185,7 +186,7 @@ end = struct
185186
module Unchecked = U.Make (Coh) (Tm)
186187
module P = Printing (Coh) (Tm)
187188
module Printing = P.Make (Coh) (Tm)
188-
module E = Equality.Equality (Coh) (Tm)
189+
module E = Equality (Coh) (Tm)
189190
module Equality = E.Make (Coh) (Tm)
190191

191192
(** A pasting scheme. *)
@@ -346,7 +347,7 @@ end = struct
346347
module Unchecked = U.Make (Coh) (Tm)
347348
module P = Printing (Coh) (Tm)
348349
module Printing = P.Make (Coh) (Tm)
349-
module E = Equality.Equality (Coh) (Tm)
350+
module E = Equality (Coh) (Tm)
350351
module Equality = E.Make (Coh) (Tm)
351352

352353
(** A type exepression. *)
@@ -440,12 +441,15 @@ and UnnamedTm : sig
440441
val apply_sub : t -> Sub.t -> t
441442
val preimage : t -> Sub.t -> t
442443
val develop : t -> Unchecked_types(Coh)(Tm).tm
444+
val is_equal : t -> t -> bool
443445
end = struct
444-
open Unchecked (Coh) (Tm)
445-
module Unchecked = Make (Coh) (Tm)
446+
module U = Unchecked (Coh) (Tm)
447+
module Unchecked = U.Make (Coh) (Tm)
446448
module Types = Unchecked_types (Coh) (Tm)
447-
open Printing (Coh) (Tm)
448-
module Printing = Make (Coh) (Tm)
449+
module P = Printing (Coh) (Tm)
450+
module Printing = P.Make (Coh) (Tm)
451+
module E = Equality (Coh) (Tm)
452+
module Equality = E.Make (Coh) (Tm)
449453

450454
type expr = Var of Var.t | Coh of Coh.t * Sub.t | App of Tm.t * Sub.t
451455

@@ -531,6 +535,10 @@ end = struct
531535
let c = Sub.tgt sub in
532536
let t = Unchecked.tm_sub_preimage (forget t) (Sub.forget sub) in
533537
check c t
538+
539+
let is_equal t1 t2 =
540+
Ctx.is_equal (Ty.ctx t1.ty) (Ty.ctx t2.ty)
541+
&& Equality.is_equal_tm t1.unchecked t2.unchecked
534542
end
535543

536544
(** Operations on terms. *)
@@ -547,6 +555,7 @@ and Tm : sig
547555
val func_data : t -> (Var.t * int) list list
548556
val pp_data : t -> pp_data
549557
val develop : t -> Unchecked_types(Coh)(Tm).tm
558+
val is_equal : t -> t -> bool
550559

551560
val apply :
552561
(Unchecked_types(Coh)(Tm).ctx -> Unchecked_types(Coh)(Tm).ctx) ->
@@ -595,6 +604,8 @@ end = struct
595604
let pp_data = fun_pp_data pp_data in
596605
let tm = Unchecked.tm_apply_sub (fun_tm (UnnamedTm.forget tm)) db_sub in
597606
(check c pp_data tm, db_sub)
607+
608+
let is_equal (t1, _) (t2, _) = UnnamedTm.is_equal t1 t2
598609
end
599610

600611
(** A coherence. *)
@@ -807,7 +818,7 @@ module U = Unchecked (Coh) (Tm)
807818
module Unchecked = U.Make (Coh) (Tm)
808819
module P = Printing (Coh) (Tm)
809820
module Printing = P.Make (Coh) (Tm)
810-
module E = Equality.Equality (Coh) (Tm)
821+
module E = Equality (Coh) (Tm)
811822
module Equality = E.Make (Coh) (Tm)
812823

813824
let check check_fn name =

‎lib/lexer.mll‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,8 +33,9 @@ rule token = parse
3333
let n = int_of_string n in
3434
let k = int_of_string k in
3535
let l = int_of_string l in
36-
EH_HALF(n,k,l) }
36+
EH_HALF(n,k,l) }
3737
| "declare" { DECLARE }
38+
| "benchmark" { BENCHMARK }
3839
| "I" { INV }
3940
| "U" { UNIT }
4041
| "(" { LPAR }

‎lib/parser.mly‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,12 +9,12 @@
99
let add_suspension = function
1010
| Sub (x,s,None,b) -> Sub (x,s,Some 1,b)
1111
| Sub (x,s,Some n,b) -> Sub (x,s,Some (n+1),b)
12-
| Letin_tm _ | VarR _ |Op _ | Meta | Inverse _ | Unit _ | BuiltinR _
12+
| Letin_tm _ | VarR _ |Op _ | Meta | Inverse _ | Unit _ | BuiltinR _
1313
-> Error.fatal "trying to generate an invalid suspension"
1414

1515
let mark_explicit = function
1616
| Sub(x,s,i,_) -> Sub(x,s,i,true)
17-
| Letin_tm _ | VarR _ |Op _ | Meta | Inverse _ | Unit _ | BuiltinR _
17+
| Letin_tm _ | VarR _ |Op _ | Meta | Inverse _ | Unit _ | BuiltinR _
1818
-> Error.fatal "only substitution can be marked explicit"
1919

2020
let context_of_annotated_ps ps =
@@ -42,7 +42,7 @@
4242
%token <int> CYLSTACK
4343
%token <string> IDENT
4444
%token <string> INT
45-
%token CHECK EQUAL LET IN SET INV UNIT DECLARE
45+
%token CHECK EQUAL LET IN SET INV UNIT DECLARE BENCHMARK
4646
%token EOF
4747

4848
%start prog
@@ -77,6 +77,8 @@ cmd:
7777
| SET IDENT EQUAL IDENT { Set ($2,$4) }
7878
| SET IDENT EQUAL INT { Set ($2,$4) }
7979
| DECLARE IDENT EQUAL builtin { Decl_builtin (Var.make_var $2,$4) }
80+
| BENCHMARK args_or_ps EQUAL tmexpr { Benchmark ($2,$4) }
81+
| BENCHMARK builtin { Benchmark_builtin ($2) }
8082

8183
args_of_same_ty :
8284
| IDENT COL tyexpr { [Var.make_var $1, $3], $3 }

0 commit comments

Comments
 (0)