Skip to content

Commit 52a209d

Browse files
committed
[spectec] Fix resolution of argument syntax sugar in the case of forward uses
1 parent 63201ed commit 52a209d

3 files changed

Lines changed: 28 additions & 0 deletions

File tree

0 Bytes
Binary file not shown.

spectec/src/el/convert.ml

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,18 @@ let rec typ_of_exp e =
7373
| IterE (e1, iter) -> IterT (typ_of_exp e1, iter)
7474
| StrE efs -> StrT (NoDots, [], map_nl_list typfield_of_expfield efs, NoDots)
7575
| AtomE atom -> AtomT atom
76+
| SeqE [{it = VarE (id, []); at = at1; _}; {it = ParenE e1; at = at2; _}]
77+
when at1.right = at2.left -> (* HACK! *)
78+
VarT (id, [ref (ExpA e1) $ e1.at])
79+
| SeqE [{it = VarE (id, []); at = at1; _}; {it = TupE es; at = at2; _}]
80+
when at1.right = at2.left -> (* HACK! *)
81+
VarT (id, List.map (fun ei -> ref (ExpA ei) $ ei.at) es)
82+
| SeqE [{it = AtomE {it = Xl.Atom.Atom id; at; _}; at = at1; _}; {it = ParenE e1; at = at2; _}]
83+
when at1.right = at2.left -> (* HACK! *)
84+
VarT (id $ at, [ref (ExpA e1) $ e1.at])
85+
| SeqE [{it = AtomE {it = Xl.Atom.Atom id; at; _}; at = at1; _}; {it = TupE es; at = at2; _}]
86+
when at1.right = at2.left -> (* HACK! *)
87+
VarT (id $ at, List.map (fun ei -> ref (ExpA ei) $ ei.at) es)
7688
| SeqE es -> SeqT (List.map typ_of_exp es)
7789
| InfixE (e1, atom, e2) -> InfixT (typ_of_exp e1, atom, typ_of_exp e2)
7890
| BrackE (l, e1, r) -> BrackT (l, typ_of_exp e1, r)
@@ -156,6 +168,18 @@ let rec sym_of_exp e =
156168
| NumE (op, `Nat n) -> NumG (op, n)
157169
| TextE s -> TextG s
158170
| EpsE -> EpsG
171+
| SeqE [{it = VarE (id, []); at = at1; _}; {it = ParenE e1; at = at2; _}]
172+
when at1.right = at2.left -> (* HACK! *)
173+
VarG (id, [ref (ExpA e1) $ e1.at])
174+
| SeqE [{it = VarE (id, []); at = at1; _}; {it = TupE es; at = at2; _}]
175+
when at1.right = at2.left -> (* HACK! *)
176+
VarG (id, List.map (fun ei -> ref (ExpA ei) $ ei.at) es)
177+
| SeqE [{it = AtomE {it = Xl.Atom.Atom id; at; _}; at = at1; _}; {it = ParenE e1; at = at2; _}]
178+
when at1.right = at2.left -> (* HACK! *)
179+
VarG (id $ at, [ref (ExpA e1) $ e1.at])
180+
| SeqE [{it = AtomE {it = Xl.Atom.Atom id; at; _}; at = at1; _}; {it = TupE es; at = at2; _}]
181+
when at1.right = at2.left -> (* HACK! *)
182+
VarG (id $ at, List.map (fun ei -> ref (ExpA ei) $ ei.at) es)
159183
| SeqE es -> SeqG (List.map (fun e -> Elem (sym_of_exp e)) es)
160184
| ParenE e1 -> ParenG (sym_of_exp e1)
161185
| TupE es -> TupG (List.map sym_of_exp es)

spectec/src/frontend/elab.ml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2222,6 +2222,10 @@ and elab_arg in_lhs env (a : arg) (p : Il.param) s : Il.arg list * Il.Subst.subs
22222222
| ExpA {it = CallE (id, []); _}, Il.DefP _ -> a.it := DefA id
22232223
| _, _ -> ()
22242224
);
2225+
Debug.(log_at "el.elab_arg" a.at
2226+
(fun _ -> fmt "%s : %s" (el_arg a) (il_param p))
2227+
(fun (as', _) -> fmt "%s" (list il_arg as'))
2228+
) @@ fun _ ->
22252229
match !(a.it), (Il.Subst.subst_param s p).it with
22262230
| ExpA e, Il.ExpP (x, t) ->
22272231
let e' = checkpoint (elab_exp env e t) in

0 commit comments

Comments
 (0)