Skip to content

Commit

Permalink
Add a more operator atoms and simplify/generalise EL variant syntax (#51
Browse files Browse the repository at this point in the history 
)

* More atoms

* Allow brackets as variant types

* Generalise and simplify variant types
  • Loading branch information
@rossberg
rossberg authored Dec 3, 2023
1 parent ec79d67 commit 63ec997
Show file tree
Hide file tree
Showing 17 changed files with 301 additions and 279 deletions.
2 changes: 1 addition & 1 deletion spectec/doc/Language.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ In addition to type expressions, custom _notation_ types can be defined:
deftyp ::=
nottyp free notation
"{" list(atom typ hint* premise*, ",") "}" record
"..."? "|" list(varid | atom nottyp hint* premise*, "|") "|" "..." variant
"..."? "|" list(varid | nottyp hint* premise*, "|") "|" "..." variant
nottyp ::=
typ plain type
Expand Down
8 changes: 8 additions & 0 deletions spectec/spec/wasm-1.0/0-aux.watsup
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,3 +56,11 @@ syntax testfuse =
| MN nat nat nat hint(show MN_#AB % % %)
| OP nat nat nat hint(show OP_#AB#% % %)
| QR nat nat nat hint(show QR_%#AB % %)


syntax testmixfix = | `{ nat* } | `[ nat* ] | nat -> nat

def $testmixfix(testmixfix) : nat*
def $testmixfix(`{nat*}) = nat*
def $testmixfix(`[nat*]) = nat*
def $testmixfix(nat_1 -> nat_2) = nat_1 nat_2
156 changes: 62 additions & 94 deletions spectec/src/backend-latex/render.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -146,11 +146,6 @@ let strip_nl = function
| xs -> xs


let as_tup_typ t =
match t.it with
| TupT ts -> ts
| _ -> [t]

let as_paren_exp e =
match e.it with
| ParenE (e1, _) -> e1
Expand All @@ -168,27 +163,6 @@ let rec fuse_exp e deep =
| SeqE (e1::es) -> List.fold_left (fun e1 e2 -> FuseE (e1, e2) $ e.at) e1 es
| _ -> e

let rec exp_of_typ t = exp_of_typ' t.it $ t.at
and exp_of_typ' = function
| VarT id -> VarE id
| BoolT -> VarE ("bool" $ no_region)
| NumT NatT -> VarE ("nat" $ no_region)
| NumT IntT -> VarE ("int" $ no_region)
| NumT RatT -> VarE ("rat" $ no_region)
| NumT RealT -> VarE ("real" $ no_region)
| TextT -> VarE ("text" $ no_region)
| ParenT t -> ParenE (exp_of_typ t, false)
| TupT ts -> TupE (List.map exp_of_typ ts)
| IterT (t1, iter) -> IterE (exp_of_typ t1, iter)
| StrT tfs -> StrE (map_nl_list expfield_of_typfield tfs)
| CaseT _ | RangeT _ -> assert false
| AtomT atom -> AtomE atom
| SeqT ts -> SeqE (List.map exp_of_typ ts)
| InfixT (t1, atom, t2) -> InfixE (exp_of_typ t1, atom, exp_of_typ t2)
| BrackT (brack, t1) -> BrackE (brack, exp_of_typ t1)

and expfield_of_typfield (atom, (t, _prems), _) = (atom, exp_of_typ t)


(* Identifiers *)

Expand Down Expand Up @@ -292,16 +266,20 @@ let render_atom env = function
| Atom id -> render_atomid env id
| Infinity -> "\\infty"
| Bot -> "\\bot"
| Top -> "\\top"
| Dot -> "."
| Dot2 -> ".."
| Dot3 -> "\\dots"
| Semicolon -> ";"
| Backslash -> "\\setminus"
| In -> "\\in"
| Arrow -> "\\rightarrow"
| Arrow2 -> "\\Rightarrow"
| Colon -> ":"
| Sub -> "\\leq"
| Sup -> "\\geq"
| Assign -> ":="
| Equiv -> "\\equiv"
| Approx -> "\\approx"
| SqArrow -> "\\hookrightarrow"
| SqArrowStar -> "\\hookrightarrow^\\ast"
Expand All @@ -314,12 +292,16 @@ let render_atom env = function
else
"\\vdash"
| Quest -> "{}^?"
| Plus -> "{}^+"
| Star -> "{}^\\ast"

let render_brack = function
| Paren -> "(", ")"
| Brack -> "[", "]"
| Brace -> "\\{", "\\}"
| Comma -> ","
| Bar -> "\\mid"
| LParen -> "("
| RParen -> ")"
| LBrack -> "["
| RBrack -> "]"
| LBrace -> "\\{"
| RBrace -> "\\}"

let render_unop = function
| NotOp -> "\\neg"
Expand Down Expand Up @@ -410,8 +392,8 @@ and expand_exp' args e' =
let e1' = expand_exp args e1 in
let e2' = expand_exp args e2 in
InfixE (e1', atom, e2')
| BrackE (brack, e) -> BrackE (brack, expand_exp args e)
| CallE (id, e) -> CallE (id, expand_exp args e)
| BrackE (l, e1, r) -> BrackE (l, expand_exp args e1, r)
| CallE (id, e1) -> CallE (id, expand_exp args e1)
| IterE (e1, iter) ->
let e1' = expand_exp args e1 in
let iter' = expand_iter args iter in
Expand Down Expand Up @@ -480,18 +462,29 @@ and render_iter env = function

(* Types *)

and exp_of_typ t = exp_of_typ' t.it $ t.at
and exp_of_typ' = function
| VarT id -> VarE id
| BoolT -> VarE ("bool" $ no_region)
| NumT NatT -> VarE ("nat" $ no_region)
| NumT IntT -> VarE ("int" $ no_region)
| NumT RatT -> VarE ("rat" $ no_region)
| NumT RealT -> VarE ("real" $ no_region)
| TextT -> VarE ("text" $ no_region)
| ParenT t -> ParenE (exp_of_typ t, false)
| TupT ts -> TupE (List.map exp_of_typ ts)
| IterT (t1, iter) -> IterE (exp_of_typ t1, iter)
| StrT tfs -> StrE (map_nl_list expfield_of_typfield tfs)
| CaseT _ | RangeT _ -> assert false
| AtomT atom -> AtomE atom
| SeqT ts -> SeqE (List.map exp_of_typ ts)
| InfixT (t1, atom, t2) -> InfixE (exp_of_typ t1, atom, exp_of_typ t2)
| BrackT (l, t1, r) -> BrackE (l, exp_of_typ t1, r)

and expfield_of_typfield (atom, (t, _prems), _) = (atom, exp_of_typ t)

and render_typ env t =
match t.it with
| VarT id -> render_synid env id
| BoolT -> render_synid env ("bool" $ t.at)
| NumT NatT -> render_synid env ("nat" $ t.at)
| NumT IntT -> render_synid env ("int" $ t.at)
| NumT RatT -> render_synid env ("rat" $ t.at)
| NumT RealT -> render_synid env ("real" $ t.at)
| TextT -> render_synid env ("text" $ t.at)
| ParenT t1 -> "(" ^ render_typ env t1 ^ ")"
| TupT ts -> "(" ^ render_typs ",\\; " env ts ^ ")"
| IterT (t1, iter) -> "{" ^ render_typ env t1 ^ render_iter env iter ^ "}"
| StrT tfs ->
"\\{\\; " ^
"\\begin{array}[t]{@{}l@{}l@{}}\n" ^
Expand All @@ -500,45 +493,20 @@ and render_typ env t =
| CaseT (dots1, ids, tcases, dots2) ->
altern_map_nl " ~|~ " " \\\\ &&|&\n" Fun.id
(render_dots dots1 @ map_nl_list (render_synid env) ids @
map_nl_list (render_typcase env t.at) tcases @ render_dots dots2)
map_nl_list (render_typcase env) tcases @ render_dots dots2)
| RangeT tes ->
altern_map_nl " ~|~ " "\\\\ &&|&\n" (render_typenum env) tes
| AtomT atom -> render_typcase env t.at (atom, ([], []), [])
| SeqT [] -> "\\epsilon"
| SeqT ({it = AtomT atom; at; _}::ts) -> render_typcase env at (atom, (ts, []), [])
| SeqT ts -> render_typs "~" env ts
| InfixT ({it = SeqT []; _}, atom, t2) ->
"{" ^ space (render_atom env) atom ^ "}\\;" ^ render_typ env t2
| InfixT (t1, atom, t2) ->
render_typ env t1 ^ space (render_atom env) atom ^ render_typ env t2
| BrackT (brack, t1) ->
let l, r = render_brack brack in l ^ render_typ env t1 ^ r

and render_typs sep env ts =
concat sep (List.filter ((<>) "") (List.map (render_typ env) ts))
| _ ->
render_exp env (exp_of_typ t)


and render_typfield env (atom, (t, prems), _hints) =
render_fieldname env atom t.at ^ "~" ^ render_typ env t ^
if prems = [] then "" else render_conditions env "&&&&" prems

and render_typcase env at (atom, (ts, prems), _hints) =
let es = List.map exp_of_typ ts in
render_expand env env.show_case (El.Print.string_of_atom atom $ at) es
(fun () ->
match atom, ts with
| Atom id, t1::ts2 when ends_sub id ->
(* Handle subscripting *)
"{" ^ render_atomid env (chop_sub id) ^
"}_{" ^ render_typs "," env (as_tup_typ t1) ^ "}\\," ^
(if ts2 = [] then "" else "\\," ^ render_typs "~" env ts2)
| _ ->
let s1 = render_atom env atom in
let s2 = render_typs "~" env ts in
assert (s1 <> "" || s2 <> "");
if s1 <> "" && s2 <> "" then s1 ^ "~" ^ s2 else s1 ^ s2
) ^
if prems = [] then "" else render_conditions env "&&&&" prems
and render_typcase env (_atom, (t, prems), _hints) =
render_typ env t ^
if prems = [] then "" else render_conditions env "&&&&" prems

and render_typenum env (e, eo) =
render_exp env e ^
Expand All @@ -562,7 +530,6 @@ and render_exp env e =
*)
match e.it with
| VarE id -> render_varid env id
| AtomE atom -> render_expcase env atom [] e.at
| BoolE b -> render_atom env (Atom (string_of_bool b))
| NatE n -> string_of_int n
| HexE n ->
Expand All @@ -586,7 +553,24 @@ and render_exp env e =
| CmpE (e1, op, e2) ->
render_exp env e1 ^ space render_cmpop op ^ render_exp env e2
| EpsE -> "\\epsilon"
| SeqE ({it = AtomE atom; at; _}::es) -> render_expcase env atom es at
| AtomE atom ->
render_expand env env.show_case (El.Print.string_of_atom atom $ e.at) []
(fun () -> render_atom env atom)
| SeqE ({it = AtomE atom; at; _}::es) ->
render_expand env env.show_case (El.Print.string_of_atom atom $ at) es
(fun () ->
match atom, es with
| Atom id, e1::es2 when ends_sub id ->
(* Handle subscripting *)
"{" ^ render_atomid env (chop_sub id) ^ "}_{" ^
render_exps "," env (as_tup_exp e1) ^ "}" ^
(if es2 = [] then "" else "\\," ^ render_exps "~" env es2)
| _ ->
let s1 = render_atom env atom in
let s2 = render_exps "~" env es in
assert (s1 <> "" || s2 <> "");
if s1 <> "" && s2 <> "" then s1 ^ "~" ^ s2 else s1 ^ s2
)
(* Hack for binop_nt *)
| SeqE (e1::e2::es) when chop_sub_exp e1 <> None ->
"{" ^ render_exp env (Option.get (chop_sub_exp e1)) ^ "}_{" ^
Expand Down Expand Up @@ -621,8 +605,8 @@ and render_exp env e =
"{" ^ space (render_atom env) atom ^ "}\\;" ^ render_exp env e2
| InfixE (e1, atom, e2) ->
render_exp env e1 ^ space (render_atom env) atom ^ render_exp env e2
| BrackE (brack, e) ->
let l, r = render_brack brack in l ^ render_exp env e ^ r
| BrackE (l, e1, r) ->
render_atom env l ^ render_exp env e1 ^ render_atom env r
| CallE (id, e1) ->
render_expand env env.show_def id (untup_exp e1)
(fun () ->
Expand Down Expand Up @@ -668,22 +652,6 @@ and render_fieldname env atom at =
render_expand env env.show_field (El.Print.string_of_atom atom $ at) []
(fun () -> render_atom env atom)

and render_expcase env atom es at =
render_expand env env.show_case (El.Print.string_of_atom atom $ at) es
(fun () ->
match atom, es with
| Atom id, e1::es2 when ends_sub id ->
(* Handle subscripting *)
"{" ^ render_atomid env (chop_sub id) ^ "}_{" ^
render_exps "," env (as_tup_exp e1) ^ "}" ^
(if es2 = [] then "" else "\\," ^ render_exps "~" env es2)
| _ ->
let s1 = render_atom env atom in
let s2 = render_exps "~" env es in
assert (s1 <> "" || s2 <> "");
if s1 <> "" && s2 <> "" then s1 ^ "~" ^ s2 else s1 ^ s2
)


(* Premises *)

Expand Down
2 changes: 1 addition & 1 deletion spectec/src/backend-prose/translate.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,7 @@ let rec push right = match right.it with
(Print.string_of_exp n)
(
match cont.it with
| BrackE(_, {it = EpsE; _}) -> "end"
| BrackE(_, {it = EpsE; _}, _) -> "end"
| _ -> "start"
);
printf_step
Expand Down
33 changes: 19 additions & 14 deletions spectec/src/el/ast.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,32 +20,35 @@ type atom =
| Atom of string (* atomid *)
| Infinity (* infinity *)
| Bot (* `_|_` *)
| Top (* `^|^` *)
| Dot (* `.` *)
| Dot2 (* `..` *)
| Dot3 (* `...` *)
| Semicolon (* `;` *)
| Backslash (* `\` *)
| In (* `in` *)
| In (* `<-` *)
| Arrow (* `->` *)
| Arrow2 (* ``=>` *)
| Colon (* `:` *)
| Sub (* `<:` *)
| Sup (* `:>` *)
| Assign (* `:=` *)
| Equiv (* `==` *)
| Approx (* `~~` *)
| SqArrow (* `~>` *)
| SqArrowStar (* `~>*` *)
| Prec (* `<<` *)
| Succ (* `>>` *)
| Turnstile (* `|-` *)
| Tilesturn (* `-|` *)
| Quest (* `?` *)
| Star (* `*` *)

type brack =
| Paren (* ``(` ... `)` *)
| Brack (* ``[` ... `]` *)
| Brace (* ``{` ... `}` *)

type dots = Dots | NoDots
| Quest (* ``?` *)
| Plus (* ``+` *)
| Star (* ``*` *)
| Comma (* ``,` *)
| Bar (* ``|` *)
| LParen | RParen (* ``(` `)` *)
| LBrack | RBrack (* ``[` `]` *)
| LBrace | RBrace (* ``{` `}` *)


(* Iteration *)
Expand All @@ -59,6 +62,8 @@ type iter =

(* Types *)

and dots = Dots | NoDots

and numtyp =
| NatT (* `nat` *)
| IntT (* `int` *)
Expand All @@ -81,10 +86,10 @@ and typ' =
| AtomT of atom (* atom *)
| SeqT of typ list (* `epsilon` / typ typ *)
| InfixT of typ * atom * typ (* typ atom typ *)
| BrackT of brack * typ (* ``` ([{ typ }]) *)
| BrackT of atom * typ * atom (* ``` ([{ typ }]) *)

and typfield = atom * (typ * premise nl_list) * hint list (* atom typ prem* hint* *)
and typcase = atom * (typ list * premise nl_list) * hint list (* atom typ* prem* hint* *)
and typfield = atom * (typ * premise nl_list) * hint list (* atom typ prem* hint* *)
and typcase = atom * (typ * premise nl_list) * hint list (* atom typ* prem* hint* *)
and typenum = exp * exp option (* exp (`|` exp (`|` `...` `|` exp)?)* *)


Expand Down Expand Up @@ -141,7 +146,7 @@ and exp' =
| ParenE of exp * bool (* `(` exp `)` *)
| TupE of exp list (* `(` list2(exp, `,`) `)` *)
| InfixE of exp * atom * exp (* exp atom exp *)
| BrackE of brack * exp (* ``` ([{ exp }]) *)
| BrackE of atom * exp * atom (* ``` ([{ exp }]) *)
| CallE of id * exp (* `$` defid exp? *)
| IterE of exp * iter (* exp iter *)
| HoleE of bool (* `%` or `%%` *)
Expand Down
11 changes: 6 additions & 5 deletions spectec/src/el/eq.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,15 +50,15 @@ and eq_typ t1 t2 =
| SeqT ts1, SeqT ts2 -> eq_list eq_typ ts1 ts2
| InfixT (t11, atom1, t12), InfixT (t21, atom2, t22) ->
eq_typ t11 t21 && atom1 = atom2 && eq_typ t12 t22
| BrackT (brack1, t11), BrackT (brack2, t21) ->
brack1 = brack2 && eq_typ t11 t21
| BrackT (l1, t11, r1), BrackT (l2, t21, r2) ->
l1 = l2 && eq_typ t11 t21 && r1 = r2
| _, _ -> t1.it = t2.it

and eq_typfield (atom1, (t1, prems1), _) (atom2, (t2, prems2), _) =
atom1 = atom2 && eq_typ t1 t2 && eq_nl_list eq_prem prems1 prems2

and eq_typcase (atom1, (ts1, prems1), _) (atom2, (ts2, prems2), _) =
atom1 = atom2 && eq_list eq_typ ts1 ts2 && eq_nl_list eq_prem prems1 prems2
and eq_typcase (atom1, (t1, prems1), _) (atom2, (t2, prems2), _) =
atom1 = atom2 && eq_typ t1 t2 && eq_nl_list eq_prem prems1 prems2

and eq_typenum (e1, eo1) (e2, eo2) =
eq_exp e1 e2 && eq_opt eq_exp eo1 eo2
Expand Down Expand Up @@ -91,7 +91,8 @@ and eq_exp e1 e2 =
| DotE (e11, atom1), DotE (e21, atom2) -> eq_exp e11 e21 && atom1 = atom2
| InfixE (e11, atom1, e12), InfixE (e21, atom2, e22) ->
eq_exp e11 e21 && atom1 = atom2 && eq_exp e12 e22
| BrackE (brack1, e1), BrackE (brack2, e2) -> brack1 = brack2 && eq_exp e1 e2
| BrackE (l1, e1, r1), BrackE (l2, e2, r2) ->
l1 = l2 && eq_exp e1 e2 && r1 = r2
| CallE (id1, e1), CallE (id2, e2) -> id1.it = id2.it && eq_exp e1 e2
| IterE (e11, iter1), IterE (e21, iter2) ->
eq_exp e11 e21 && eq_iter iter1 iter2
Expand Down
Loading

0 comments on commit 63ec997

Please sign in to comment.