Replace `Symbols.t` by `Var.t` in binders and substitutions #976

Halbaroth · 2023-11-24T09:45:55Z

Alt-Ergo embeds variables into symbols then expressions. It's a good design but at many places in the codebase, we use symboles where variables are clearly sufficient.

For instance, we shouldn't use symbols in substitutions or binders because we always bind a variable to an expression or substitute a variable by an expression.

Let's use the simpler type Var.t as much as possible.

This commit should be safe because the comparison functions of Symbols.t and Var.t agree on variables.

bclement-ocp · 2023-11-24T10:25:16Z

src/lib/structures/var.ml

+let underscore =
+  Random.self_init ();
+  of_string @@ Format.sprintf "_%d" (Random.int 1_000_000)


Wait, I was not aware we were doing that — this does not seem safe at all! We should use a counter instead (there are no guarantees that two consecutive Random.int calls won't return the same value, which would be problematic as forall x, y : int. x + y would become forall _1, _1: int. _1 + _1 which… is not the same at all.

Opened #977

ah ah :) you don't know the best part of our mighty codebase I see :)
This snippet is pure gold. I shared it one year ago on zulip, best joke of my short software developer career.

Ah! But what I said above is not true — underscore is a global variable, not a function. OK, that makes things better — there can "just" be conflicts with a variable named _n for some n that changes each time Alt-Ergo is run. We should just call this "._" instead, no?

Stevendeo · 2023-11-24T10:19:46Z

src/lib/frontend/cnf.ml

@@ -116,12 +116,13 @@ let rec make_term up_qv quant_basename t =

    | TTlet (binders, t2) ->
      let binders =
-        List.rev_map (fun (s, t1) -> s, mk_term t1)
+        List.rev_map (fun (s, t1) ->
+            match s with Sy.Var v -> v, mk_term t1 | _ -> assert false)


Is this invariant really always true? In that case, could we replace the type of binders by a list of Var.ts?

Actually I'm checking it right now. I forgot to do it before publishing the PR. I hope the legacy parser enforce this invariant (the new one does).

Actually, before submitting this PR, I tried to change the type of the binders in the legacy typechecker. This will requires to change many types, mostly because the typechecker aggregates the symbols in a context, so embed variables into symbols makes the design simpler here. I decided to keep the code as before. The only place where we produce a new TTlet term is here:

alt-ergo/src/lib/frontend/typechecker.ml

Lines 913 to 934 in 7363cd0

| PPlet(l, t2) ->

let _ =

List.fold_left (fun z (sy,_) ->

if Util.SS.mem sy z then

Errors.typing_error (DuplicatePattern sy) loc;

Util.SS.add sy z

)Util.SS.empty l

in

let rev_l = List.rev_map (fun (sy, t) -> sy, type_term env t) l in

let env =

List.fold_left

(fun env (sy, te1) ->

let ty1 = Ty.shorten te1.c.tt_ty in

let fvar s = Symbols.var @@ Var.of_string s in

Env.add env [sy] fvar ty1

)env rev_l

in

let te2 = type_term env t2 in

let ty2 = Ty.shorten te2.c.tt_ty in

let l = List.rev_map (fun (sy, t) -> fst (Env.find env sy), t) rev_l in

Options.tool_req 1 (append_type "TR-Typing-Let type" ty2);

TTlet(l, te2), ty2

As you can see line 926, we store new variables in the environment of the typechecker and we retrieve them at the line 932 to produce the list of binders. Thus, the binders are always variables (embedded in symbols).

I suggest you add to the assert false a TODO stating that we could actually simplify but it would require to update some legacy code which was out of the scope of the PR adding this assert false (and a reference to typechecker.ml).

Stevendeo · 2023-11-24T10:33:42Z

src/lib/structures/expr.ml

-          let fresh_sy = Sy.fresh_skolem ~is_var:true "Pur-Ite" in
-          mk_term fresh_sy [] t.ty , add_let fresh_sy t lets
+          let fresh_var =
+            match Sy.fresh_skolem ~is_var:true "Pur-Ite" with


I think it is better to add a Symbols.fresh_skolem_name instead of creating a var and destroying it with an assert false (or simple export the SkolemId from symbols)? I wonder if the current fresh_skolem function is still relevant: is there still cases in your PR where fresh_skolem is called with without creating a var?

I'll check. Good catch.

The function Symbols.fresh_skolem isn't necessary anymore. I create a two functions fresh_skolem_string and fresh_skolem_name. It would be better to extract the module of identifiers from the Symbols module and create a function fresk_skolem in Var but it's a small detail.

Stevendeo · 2023-11-27T12:36:04Z

src/lib/frontend/cnf.ml

@@ -116,12 +116,13 @@ let rec make_term up_qv quant_basename t =

    | TTlet (binders, t2) ->
      let binders =
-        List.rev_map (fun (s, t1) -> s, mk_term t1)
+        List.rev_map (fun (s, t1) ->
+            match s with Sy.Var v -> v, mk_term t1 | _ -> assert false)


I suggest you add to the assert false a TODO stating that we could actually simplify but it would require to update some legacy code which was out of the scope of the PR adding this assert false (and a reference to typechecker.ml).

Alt-Ergo embeds variables into symbols then expressions. It's a good design but at many places in the codebase, we use symboles where variables are clearly sufficient. For instance, we shouldn't use symbols in substitutions or binders because we always bind a variable to an expression or substitute a variable by an expression. Let's use the simpler type `Var.t` as much as possible. This commit should be safe because the comparison functions of `Symbols.t` and `Var.t` agree on variables.

We need to create fresh variables without embed them in symbols as we now store binders in variable maps.

Halbaroth added the clean-up label Nov 24, 2023

Halbaroth force-pushed the binder-are-vars branch from f595c29 to b406d45 Compare November 24, 2023 09:47

Halbaroth requested review from bclement-ocp and Stevendeo November 24, 2023 10:11

bclement-ocp approved these changes Nov 24, 2023

View reviewed changes

bclement-ocp mentioned this pull request Nov 24, 2023

Do not use random names for variables #977

Closed

Stevendeo reviewed Nov 24, 2023

View reviewed changes

Halbaroth requested a review from Stevendeo November 27, 2023 10:53

Halbaroth force-pushed the binder-are-vars branch from af95041 to ec4d4d2 Compare November 27, 2023 10:53

Stevendeo approved these changes Nov 27, 2023

View reviewed changes

Halbaroth enabled auto-merge (squash) November 27, 2023 12:46

Halbaroth disabled auto-merge November 27, 2023 13:22

Halbaroth force-pushed the binder-are-vars branch from a9f4dce to dda574b Compare November 27, 2023 13:47

Halbaroth added 5 commits November 27, 2023 14:48

linter

2860de4

Don't destroy fresh symbols that are variables

b8915dc

We need to create fresh variables without embed them in symbols as we now store binders in variable maps.

linter

4b4e9f0

Add an explanation for a new assertion in cnf module

dda574b

Halbaroth merged commit 4b89c12 into OCamlPro:next Nov 27, 2023
14 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Replace `Symbols.t` by `Var.t` in binders and substitutions #976

Replace `Symbols.t` by `Var.t` in binders and substitutions #976

Halbaroth commented Nov 24, 2023

bclement-ocp Nov 24, 2023

bclement-ocp Nov 24, 2023

Halbaroth Nov 24, 2023 •

edited

Loading

bclement-ocp Nov 24, 2023

Stevendeo Nov 24, 2023

Halbaroth Nov 24, 2023

Halbaroth Nov 27, 2023 •

edited

Loading

Stevendeo Nov 27, 2023

Stevendeo Nov 24, 2023

Halbaroth Nov 24, 2023

Halbaroth Nov 27, 2023

Stevendeo Nov 27, 2023

	\| PPlet(l, t2) ->
	let _ =
	List.fold_left (fun z (sy,_) ->
	if Util.SS.mem sy z then
	Errors.typing_error (DuplicatePattern sy) loc;
	Util.SS.add sy z
	)Util.SS.empty l
	in
	let rev_l = List.rev_map (fun (sy, t) -> sy, type_term env t) l in
	let env =
	List.fold_left
	(fun env (sy, te1) ->
	let ty1 = Ty.shorten te1.c.tt_ty in
	let fvar s = Symbols.var @@ Var.of_string s in
	Env.add env [sy] fvar ty1
	)env rev_l
	in
	let te2 = type_term env t2 in
	let ty2 = Ty.shorten te2.c.tt_ty in
	let l = List.rev_map (fun (sy, t) -> fst (Env.find env sy), t) rev_l in
	Options.tool_req 1 (append_type "TR-Typing-Let type" ty2);
	TTlet(l, te2), ty2

Replace Symbols.t by Var.t in binders and substitutions #976

Replace Symbols.t by Var.t in binders and substitutions #976

Conversation

Halbaroth commented Nov 24, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth Nov 24, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth Nov 27, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Replace `Symbols.t` by `Var.t` in binders and substitutions #976

Replace `Symbols.t` by `Var.t` in binders and substitutions #976

Halbaroth Nov 24, 2023 •

edited

Loading

Halbaroth Nov 27, 2023 •

edited

Loading