Change to normalize more in syntax constructors

Normalizations include

    ...{Bs} -> Bs

    {X = E}.X -> E

    let in E -> E

    let Bs1 in let Bs2 in E -> let Bs1, Bs2 in E

and some more for cases where Bs are all known to be unique compiler generated
variables.

elab.ml

@@ -608,8 +608,9 @@ Trace.debug (lazy ("[RecT] t = " ^ string_of_norm_typ t));
  | EL.AnnotE(e, t) ->
  let exp =
  let open Syntax in
- let x' = var "annot" in
- appE(FunE(x'@@t.at, t, VarE(x'@@t.at)@@t.at, Expl@@t.at)@@span[e.at; t.at], e)@@exp.at in
+ let x' = uniq_var()@@t.at in
+ appE(FunE(x', t, VarE(x')@@t.at, Expl@@t.at)@@span[e.at; t.at], e)@@exp.at
+ in
  elab_exp env exp l
 
 (*

parser.mly

@@ -299,9 +299,9 @@ atdec :
  EqT(annotE(te3, t2)@@span[ati 2; ati 3])@@span[ati 2; ati 3]),
  Pure@@at())@@at())@@at() }
  | ELLIPSIS typ
- { InclD($2)@@at() }
+ { inclD($2)@@at() }
  | LET bind IN typ
- { InclD(letT($2, $4)@@at())@@at() }
+ { inclD(letT($2, $4)@@at())@@at() }
 /*
  | LPAR dec RPAR
  { $2 }
@@ -322,7 +322,7 @@ dotpathexp :
  | atpathexp
  { $1 }
  | dotpathexp DOT label
- { DotE($1, $3)@@at() }
+ { dotE($1, $3)@@at() }
 ;
 atpathexp :
  | pname
@@ -357,7 +357,7 @@ dotexp :
  | atexp
  { $1 }
  | dotexp DOT label
- { DotE($1, $3)@@at() }
+ { dotE($1, $3)@@at() }
 ;
 atexp :
  | atpathexp
@@ -495,13 +495,13 @@ atbind :
  | typpat bindanns_opt typdef
  { VarB(fst $1, funE(snd $1, $2($3))@@at())@@at() }
  | ELLIPSIS exp
- { InclB($2)@@at() }
+ { inclB($2)@@at() }
  | DO exp
  { doB($2)@@at() }
  | TYPE_ERROR exp
  { TypeErrorB($2)@@at() }
  | LET bind IN exp
- { InclB(letE($2, $4)@@at())@@at() }
+ { inclB(letE($2, $4)@@at())@@at() }
  | IMPORT TEXT
  { InclB(ImportE($2@@ati 2)@@at())@@at() }
 /*

syntax.ml

@@ -64,11 +64,16 @@ and bind' =
  | TypeErrorB of exp
 
 
-let var_counts = ref []
-let var s =
- let count = try List.assoc s !var_counts with Not_found ->
- let count = ref 0 in var_counts := (s, count) :: !var_counts; count
- in incr count; s ^ "$" ^ string_of_int !count
+let uniq_count = ref 0
+let uniq_var () = incr uniq_count; "%_" ^ string_of_int !uniq_count
+let is_uniq n = Lib.String.is_prefix "%_" n.it
+let rec every_var pr b =
+ match b.it with
+ | EmptyB -> true
+ | SeqB(b1, b2) -> every_var pr b1 && every_var pr b2
+ | VarB(v, _) -> pr v
+ | InclB(_) -> false
+ | TypeErrorB(_) -> true
 
 let index n = "_" ^ string_of_int n
 
@@ -119,23 +124,44 @@ let pathT(e) =
  | TypE(t) -> t.it
  | _ -> PathT(e)
 
-(* Sugar *)
+let inclD(t) =
+ match t.it with
+ | StrT(d) -> d.it
+ | _ -> InclD(t)
+
+let inclB(e) =
+ match e.it with
+ | StrE(b) -> b.it
+ | _ -> InclB(e)
 
-let letE(b, e) =
- let x' = var "let" in
- let b2 = VarB(x'@@e.at, e)@@e.at in
- DotE(strE(seqB(b, b2)@@span[b.at; e.at])@@span[b.at; e.at], x'@@e.at)
+let dotE(e, l) =
+ match e.it with
+ | StrE({it = VarB(x, e)}) when x.it = l.it -> e.it
+ | _ -> DotE(e, l)
+
+(* Sugar *)
 
-let asVarE(e, n, k) =
+let asVarB(e, pr) =
  match e.it with
- | VarE(x) -> (k x).it
+ | VarE(x) -> EmptyB@@e.at, x
+ | DotE({it=StrE(b)}, l) when pr b ->
+ b, l
  | _ ->
- let x = var n@@e.at in
- letE(VarB(x, e)@@e.at, k x)
+ let x = uniq_var()@@e.at in
+ VarB(x, e)@@e.at, x
+
+let letE(b1, e) =
+ let b2, x = asVarB(e, fun _ -> true) in
+ let r = span[b1.at; b2.at] in
+ dotE(strE(seqB(b1, b2)@@r)@@r, x)
+
+let asVarE(e, k) =
+ let b, x = asVarB(e, every_var is_uniq) in
+ letE(b, k x)
 
-let letT(b, t) = PathT(letE(b, typE(t)@@t.at)@@span[b.at; t.at])
-let letD(b, d) = InclD(letT(b, StrT(d)@@d.at)@@span[b.at; d.at])
-let letB(b, b') = InclB(letE(b, strE(b')@@b'.at)@@span[b.at; b'.at])
+let letT(b, t) = pathT(letE(b, typE(t)@@t.at)@@span[b.at; t.at])
+let letD(b, d) = inclD(letT(b, strT(d)@@d.at)@@span[b.at; d.at])
+let letB(b, b') = inclB(letE(b, strE(b')@@b'.at)@@span[b.at; b'.at])
 
 let rec tupT(ts) = strT(tupT' 1 ts)
 and tupT' n = function
@@ -181,14 +207,15 @@ and funE'(ps, e) =
  | _ -> "$"@@p.at, letE(b, e')@@span[p.at; e.at]
  in FunE(x, t, e'', i)@@span[p.at; e.at]
 
-let doB(e) = letB(VarB("_"@@e.at, e)@@e.at, EmptyB@@e.at)
+let doB(e) =
+ let b, _ = asVarB(e, fun _ -> true) in
+ letB(b, EmptyB@@e.at)
 
-let seqE(l, r) =
- letE(VarB("_"@@l.at, l)@@l.at, r)
+let seqE(l, r) = asVarE(l, fun _ -> r)
 
 let ifE(e1, e2, e3) =
  let at = span[e1.at; e3.at] in
- let ifE = asVarE(e1, "if", fun x -> IfE(x, e2, e3)@@at) in
+ let ifE = asVarE(e1, fun x -> IfE(x, e2, e3)@@at) in
  match e3.it with
  | AnnotE(_, t) -> AnnotE(ifE@@at, t)
  | _ -> ifE
@@ -199,21 +226,21 @@ let andE(e1, e2) =
  ifE(e1, e2, PrimE(Prim.BoolV(false))@@e1.at)
 
 let appE(e1, e2) =
- asVarE(e1, "app1", fun x1 ->
- asVarE(e2, "app2", fun x2 ->
+ asVarE(e1, fun x1 ->
+ asVarE(e2, fun x2 ->
  AppE(x1, x2)@@span[e1.at; e2.at])@@span[e1.at; e2.at])
 
 let wrapE(e, t) =
- asVarE(e, "wrap", fun x -> WrapE(x, t)@@span[e.at; t.at])
+ asVarE(e, fun x -> WrapE(x, t)@@span[e.at; t.at])
 
 let unwrapE(e, t) =
- asVarE(e, "unwrap", fun x -> UnwrapE(x, t)@@span[e.at; t.at])
+ asVarE(e, fun x -> UnwrapE(x, t)@@span[e.at; t.at])
 
 let rollE(e, t) =
- asVarE(e, "roll", fun x -> RollE(x, t)@@span[e.at; t.at])
+ asVarE(e, fun x -> RollE(x, t)@@span[e.at; t.at])
 
 let unrollE(e, t) =
- asVarE(e, "unroll", fun x -> UnrollE(x, t)@@span[e.at; t.at])
+ asVarE(e, fun x -> UnrollE(x, t)@@span[e.at; t.at])
 
 let annotE(e, t) = AnnotE(e, t)
 
@@ -258,7 +285,7 @@ let patB(p, e) =
  match p.it.infer with
  | None -> b
  | Some t ->
- letB(VarB("_"@@p.at, annotE(e, t)@@span[e.at; t.at])@@p.at, b@@p.at)
+ letB(VarB(uniq_var()@@p.at, annotE(e, t)@@span[e.at; t.at])@@p.at, b@@p.at)
 
 let asTopt(to1, to2) =
  match to1, to2 with