Small printer fix

This commit is contained in:
Louis Gesbert 2024-07-05 17:04:45 +02:00
parent a5278244ec
commit 961a93ae83
6 changed files with 22 additions and 2 deletions

View File

@ -20,6 +20,13 @@ type ('e, 'elt, 'last) t = ('e, 'elt, 'last) bound_list =
| Last of 'last | Last of 'last
| Cons of 'elt * ('e, ('e, 'elt, 'last) t) binder | Cons of 'elt * ('e, ('e, 'elt, 'last) t) binder
let rec to_seq = function
| Last () -> Seq.empty
| Cons (item, next_bind) ->
fun () ->
let v, next = Bindlib.unbind next_bind in
Seq.Cons ((v, item), to_seq next)
let rec last = function let rec last = function
| Last e -> e | Last e -> e
| Cons (_, bnd) -> | Cons (_, bnd) ->

View File

@ -30,6 +30,7 @@ type ('e, 'elt, 'last) t = ('e, 'elt, 'last) bound_list =
| Last of 'last | Last of 'last
| Cons of 'elt * ('e, ('e, 'elt, 'last) t) binder | Cons of 'elt * ('e, ('e, 'elt, 'last) t) binder
val to_seq : (((_, _) gexpr as 'e), 'elt, unit) t -> ('e Var.t * 'elt) Seq.t
val last : (_, _, 'a) t -> 'a val last : (_, _, 'a) t -> 'a
val iter : f:('e Var.t -> 'elt -> unit) -> ('e, 'elt, 'last) t -> 'last val iter : f:('e Var.t -> 'elt -> unit) -> ('e, 'elt, 'last) t -> 'last
val find : f:('elt -> 'a option) -> (_, 'elt, _) t -> 'a val find : f:('elt -> 'a option) -> (_, 'elt, _) t -> 'a

View File

@ -920,11 +920,15 @@ let code_item ?(debug = false) ?name decl_ctx fmt c =
"=" (expr ~debug ()) e "=" (expr ~debug ()) e
let code_item_list ?(debug = false) decl_ctx fmt c = let code_item_list ?(debug = false) decl_ctx fmt c =
BoundList.iter c ~f:(fun x item -> Format.pp_open_vbox fmt 0;
Format.pp_print_seq
(fun fmt (x, item) ->
code_item ~debug code_item ~debug
~name:(Format.asprintf "%a" var_debug x) ~name:(Format.asprintf "%a" var_debug x)
decl_ctx fmt item; decl_ctx fmt item;
Format.pp_print_newline fmt ()) Format.pp_print_cut fmt ())
fmt (BoundList.to_seq c);
Format.pp_close_box fmt ()
let program ?(debug = false) fmt p = let program ?(debug = false) fmt p =
decl_ctx ~debug p.decl_ctx fmt p.decl_ctx; decl_ctx ~debug p.decl_ctx fmt p.decl_ctx;

View File

@ -33,6 +33,7 @@ type S = { z: integer; }
let topval closure_f1 : (closure_env, integer) → integer = let topval closure_f1 : (closure_env, integer) → integer =
λ (env: closure_env) (y: integer) → λ (env: closure_env) (y: integer) →
if (from_closure_env env).0 then y else - y if (from_closure_env env).0 then y else - y
let scope S (S_in: S_in {x_in: bool}): S {z: integer} = let scope S (S_in: S_in {x_in: bool}): S {z: integer} =
let get x : bool = S_in.x_in in let get x : bool = S_in.x_in in
let set f : ((closure_env, integer) → integer, closure_env) = let set f : ((closure_env, integer) → integer, closure_env) =

View File

@ -31,6 +31,7 @@ type S = { f: ((closure_env, integer) → integer, closure_env); }
let topval closure_f1 : (closure_env, integer) → integer = let topval closure_f1 : (closure_env, integer) → integer =
λ (env: closure_env) (y: integer) → λ (env: closure_env) (y: integer) →
if (from_closure_env env).0 then y else - y if (from_closure_env env).0 then y else - y
let scope S let scope S
(S_in: S_in {x_in: bool}) (S_in: S_in {x_in: bool})
: S {f: ((closure_env, integer) → integer, closure_env)} : S {f: ((closure_env, integer) → integer, closure_env)}

View File

@ -76,6 +76,7 @@ type Foo = { z: integer; }
let topval closure_y1 : (closure_env, integer) → integer = let topval closure_y1 : (closure_env, integer) → integer =
λ (env: closure_env) (z: integer) → λ (env: closure_env) (z: integer) →
(from_closure_env env).0 + z (from_closure_env env).0 + z
let scope SubFoo1 let scope SubFoo1
(SubFoo1_in: SubFoo1_in {x_in: integer}) (SubFoo1_in: SubFoo1_in {x_in: integer})
: SubFoo1 { : SubFoo1 {
@ -88,10 +89,12 @@ let scope SubFoo1
(closure_y1, to_closure_env (x)) (closure_y1, to_closure_env (x))
in in
return { SubFoo1 x = x; y = y; } return { SubFoo1 x = x; y = y; }
let topval closure_y1 : (closure_env, integer) → integer = let topval closure_y1 : (closure_env, integer) → integer =
λ (env: closure_env) (z: integer) → λ (env: closure_env) (z: integer) →
let env1 : (integer, integer) = from_closure_env env in let env1 : (integer, integer) = from_closure_env env in
((env1.1 + env1.0 + z)) ((env1.1 + env1.0 + z))
let scope SubFoo2 let scope SubFoo2
(SubFoo2_in: SubFoo2_in {x1_in: integer; x2_in: integer}) (SubFoo2_in: SubFoo2_in {x1_in: integer; x2_in: integer})
: SubFoo2 { : SubFoo2 {
@ -105,18 +108,21 @@ let scope SubFoo2
(closure_y1, to_closure_env (x2, x1)) (closure_y1, to_closure_env (x2, x1))
in in
return { SubFoo2 x1 = x1; y = y; } return { SubFoo2 x1 = x1; y = y; }
let topval closure_r2 : (closure_env, integer) → integer = let topval closure_r2 : (closure_env, integer) → integer =
λ (env: closure_env) (param0: integer) → λ (env: closure_env) (param0: integer) →
let code_and_env : ((closure_env, integer) → integer, closure_env) = let code_and_env : ((closure_env, integer) → integer, closure_env) =
(from_closure_env env).0.y (from_closure_env env).0.y
in in
code_and_env.0 code_and_env.1 param0 code_and_env.0 code_and_env.1 param0
let topval closure_r1 : (closure_env, integer) → integer = let topval closure_r1 : (closure_env, integer) → integer =
λ (env: closure_env) (param0: integer) → λ (env: closure_env) (param0: integer) →
let code_and_env : ((closure_env, integer) → integer, closure_env) = let code_and_env : ((closure_env, integer) → integer, closure_env) =
(from_closure_env env).0.y (from_closure_env env).0.y
in in
code_and_env.0 code_and_env.1 param0 code_and_env.0 code_and_env.1 param0
let scope Foo let scope Foo
(Foo_in: Foo_in {b_in: ((closure_env, unit) → option bool, closure_env)}) (Foo_in: Foo_in {b_in: ((closure_env, unit) → option bool, closure_env)})
: Foo {z: integer} : Foo {z: integer}