From ad9080b8b1953d17f9d1bc36296f2676639e7a1d Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Sun, 2 Aug 2020 13:00:43 +0300 Subject: [PATCH] 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 | 5 ++-- parser.mly | 12 ++++---- syntax.ml | 83 ++++++++++++++++++++++++++++++++++++------------------ 3 files changed, 64 insertions(+), 36 deletions(-) diff --git a/elab.ml b/elab.ml index 15f6fd8..44afaff 100644 --- a/elab.ml +++ b/elab.ml @@ -619,8 +619,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 (* diff --git a/parser.mly b/parser.mly index 500001a..a90b876 100644 --- a/parser.mly +++ b/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() } /* diff --git a/syntax.ml b/syntax.ml index 361e650..28d4cae 100644 --- a/syntax.ml +++ b/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 @@ -109,23 +114,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 @@ -171,14 +197,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 @@ -189,21 +216,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) @@ -248,7 +275,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