diff --git a/spectec/.ocamlformat b/spectec/.ocamlformat new file mode 100644 index 0000000000..ee03d858cf --- /dev/null +++ b/spectec/.ocamlformat @@ -0,0 +1,13 @@ +profile = default +break-infix = wrap-or-vertical +break-string-literals = never +cases-exp-indent=2 +dock-collection-brackets = false +exp-grouping = preserve +if-then-else = fit-or-vertical +indicate-multiline-delimiters = closing-on-separate-line +leading-nested-match-parens = true +space-around-arrays = false +space-around-lists = false +space-around-records = false +space-around-variants = false diff --git a/spectec/src/backend-latex/config.ml b/spectec/src/backend-latex/config.ml index 0dc60602fc..9b1644f8e1 100644 --- a/spectec/src/backend-latex/config.ml +++ b/spectec/src/backend-latex/config.ml @@ -1,48 +1,42 @@ type anchor = - { - token : string; (* anchor token *) - prefix : string; (* prefix generated for splice *) - suffix : string; (* suffix generated for splice *) - indent : string; (* inserted after generated newlines *) + { token : string; (* anchor token *) + prefix : string; (* prefix generated for splice *) + suffix : string; (* suffix generated for splice *) + indent : string (* inserted after generated newlines *) } type config = - { - (* Anchor token for splices (default: "@@"/"@@@") *) + { (* Anchor token for splices (default: "@@"/"@@@") *) anchors : anchor list; - (* Generate id's as macro calls `\id` instead of `\mathit{id}` *) macros_for_ids : bool; - (* Generate vdash's as macro calls `\vdashRelid` instead of `\vdash` *) macros_for_vdash : bool; - (* Decorate grammars with l.h.s. description like "(instruction) instr ::= ..." *) - include_grammar_desc : bool; + include_grammar_desc : bool } type t = config - let default = { anchors = []; macros_for_ids = false; macros_for_vdash = false; - include_grammar_desc = false; + include_grammar_desc = false } let latex = { default with - anchors = [ - {token = "@@"; prefix = "$"; suffix ="$"; indent = ""}; - {token = "@@@"; prefix = "$$\n"; suffix = "\n$$"; indent = ""}; - ] + anchors = + [ {token = "@@"; prefix = "$"; suffix = "$"; indent = ""}; + {token = "@@@"; prefix = "$$\n"; suffix = "\n$$"; indent = ""} + ] } let sphinx = { default with - anchors = [ - {token = "$"; prefix = ":math:`"; suffix ="`"; indent = ""}; - {token = "$$"; prefix = ".. math::\n "; suffix = ""; indent = " "}; - ] + anchors = + [ {token = "$"; prefix = ":math:`"; suffix = "`"; indent = ""}; + {token = "$$"; prefix = ".. math::\n "; suffix = ""; indent = " "} + ] } diff --git a/spectec/src/backend-latex/dune b/spectec/src/backend-latex/dune index 41515041b6..4e64e973f3 100644 --- a/spectec/src/backend-latex/dune +++ b/spectec/src/backend-latex/dune @@ -1,5 +1,4 @@ (library - (name backend_latex) - (libraries util el frontend str) - (modules config render gen splice) -) + (name backend_latex) + (libraries util el frontend str) + (modules config render gen splice)) diff --git a/spectec/src/backend-latex/gen.ml b/spectec/src/backend-latex/gen.ml index 15f60b1518..b7b75fee3a 100644 --- a/spectec/src/backend-latex/gen.ml +++ b/spectec/src/backend-latex/gen.ml @@ -1,11 +1,14 @@ let gen_string ?(decorated = true) el = - let env = Render.env Config.latex el + let env = + Render.env Config.latex el |> Render.with_syntax_decoration decorated |> Render.with_rule_decoration decorated - in Render.render_script env el + in + Render.render_script env el let gen_file ?(decorated = true) file el = let latex = gen_string ~decorated el in let oc = Out_channel.open_text file in - Fun.protect (fun () -> Out_channel.output_string oc latex) + Fun.protect + (fun () -> Out_channel.output_string oc latex) ~finally:(fun () -> Out_channel.close oc) diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml index 25cdf317b0..a019a40bb7 100644 --- a/spectec/src/backend-latex/render.ml +++ b/spectec/src/backend-latex/render.ml @@ -3,16 +3,14 @@ open Source open El.Ast open Config - (* Errors *) let error at msg = Source.error at "latex generation" msg - (* Environment *) -module Set = Set.Make(String) -module Map = Map.Make(String) +module Set = Set.Make (String) +module Map = Map.Make (String) type rel_sort = TypingRel | ReductionRel @@ -28,7 +26,7 @@ type env = desc_syn : exp list Map.t ref; deco_syn : bool; deco_rule : bool; - current_rel : string; + current_rel : string } let new_env config = @@ -43,19 +41,22 @@ let new_env config = desc_syn = ref Map.empty; deco_syn = false; deco_rule = false; - current_rel = ""; + current_rel = "" } let with_syntax_decoration b env = {env with deco_syn = b} let with_rule_decoration b env = {env with deco_rule = b} - let env_hints name map id hints = - List.iter (fun {hintid; hintexp} -> - if hintid.it = name then - let exps = match Map.find_opt id !map with Some exps -> exps | None -> [] in - map := Map.add id (hintexp::exps) !map - ) hints + List.iter + (fun {hintid; hintexp} -> + if hintid.it = name then + let exps = + match Map.find_opt id !map with Some exps -> exps | None -> [] + in + map := Map.add id (hintexp :: exps) !map + ) + hints let env_typfield env = function | Elem (Atom id, _, hints) -> env_hints "show" env.show_field id hints @@ -69,7 +70,7 @@ let env_typ env t = match t.it with | StrT tfs -> List.iter (env_typfield env) tfs | CaseT (_, _, tcases, _) -> List.iter (env_typcase env) tcases - | _ -> () (* TODO: this assumes that types structs & variants aren't nested *) + | _ -> () (* TODO: this assumes that types structs & variants aren't nested *) let env_hintdef env hd = match hd.it with @@ -104,61 +105,41 @@ let env config script : env = List.iter (env_def env) script; env - (* Helpers *) let concat = String.concat let suffix s f x = f x ^ s let space f x = " " ^ f x ^ " " - -let rec has_nl = function - | [] -> false - | Nl::_ -> true - | _::xs -> has_nl xs - +let rec has_nl = function [] -> false | Nl :: _ -> true | _ :: xs -> has_nl xs let map_nl_list f xs = List.map (function Nl -> Nl | Elem x -> Elem (f x)) xs let rec concat_map_nl sep br f = function | [] -> "" | [Elem x] -> f x - | (Elem x)::xs -> f x ^ sep ^ concat_map_nl sep br f xs - | Nl::xs -> br ^ concat_map_nl sep br f xs + | Elem x :: xs -> f x ^ sep ^ concat_map_nl sep br f xs + | Nl :: xs -> br ^ concat_map_nl sep br f xs let rec altern_map_nl sep br f = function | [] -> "" | [Elem x] -> f x - | (Elem x)::Nl::xs -> f x ^ br ^ altern_map_nl sep br f xs - | (Elem x)::xs -> f x ^ sep ^ altern_map_nl sep br f xs - | Nl::xs -> br ^ altern_map_nl sep br f xs + | Elem x :: Nl :: xs -> f x ^ br ^ altern_map_nl sep br f xs + | Elem x :: xs -> f x ^ sep ^ altern_map_nl sep br f xs + | Nl :: xs -> br ^ altern_map_nl sep br f xs -let strip_nl = function - | Nl::xs -> xs - | 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 - | _ -> e - -let as_tup_exp e = - match e.it with - | TupE es -> es - | _ -> [e] +let strip_nl = function Nl :: xs -> xs | 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 | _ -> e +let as_tup_exp e = match e.it with TupE es -> es | _ -> [e] let rec fuse_exp e deep = match e.it with | ParenE (e1, b) when deep -> ParenE (fuse_exp e1 false, b) $ e.at | IterE (e1, iter) -> IterE (fuse_exp e1 deep, iter) $ e.at - | SeqE (e1::es) -> List.fold_left (fun e1 e2 -> FuseE (e1, e2) $ e.at) e1 es + | 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) @@ -176,15 +157,12 @@ and exp_of_typ' = function and expfield_of_typfield (atom, t, _) = (atom, exp_of_typ t) - (* Identifiers *) let render_expand_fwd = ref (fun _ -> assert false) - let is_digit c = '0' <= c && c <= '9' let is_upper c = 'A' <= c && c <= 'Z' let lower = String.lowercase_ascii - let ends_sub id = id <> "" && id.[String.length id - 1] = '_' let chop_sub id = String.sub id 0 (String.length id - 1) @@ -194,7 +172,7 @@ let rec chop_sub_exp e = | AtomE (Atom "_") -> Some (SeqE [] $ e.at) | AtomE (Atom id) when ends_sub id -> Some (AtomE (Atom (chop_sub id)) $ e.at) | FuseE (e1, e2) -> - (match chop_sub_exp e2 with + ( match chop_sub_exp e2 with | Some e2' -> Some (FuseE (e1, e2') $ e.at) | None -> None ) @@ -218,13 +196,15 @@ let render_id' env style id = let rec render_id_sub env style show at = function | [] -> "" - | ""::ss -> render_id_sub env style show at ss - | s::ss when style = `Var && is_upper s.[0] && not (Set.mem s !(env.vars)) -> - render_id_sub env `Atom show at (lower s ::ss) (* subscripts may be atoms *) - | s1::""::ss -> render_id_sub env style show at (s1::ss) - | s1::s2::ss when style = `Atom && is_upper s2.[0] -> - render_id_sub env `Atom show at ((s1 ^ "_" ^ lower s2)::ss) - | s::ss -> + | "" :: ss -> render_id_sub env style show at ss + | s :: ss when style = `Var && is_upper s.[0] && not (Set.mem s !(env.vars)) + -> + render_id_sub env `Atom show at (lower s :: ss) + (* subscripts may be atoms *) + | s1 :: "" :: ss -> render_id_sub env style show at (s1 :: ss) + | s1 :: s2 :: ss when style = `Atom && is_upper s2.[0] -> + render_id_sub env `Atom show at ((s1 ^ "_" ^ lower s2) :: ss) + | s :: ss -> let rec find_primes i = if i > 0 && s.[i - 1] = '\'' then find_primes (i - 1) else i in @@ -232,11 +212,19 @@ let rec render_id_sub env style show at = function let i = find_primes n in let s' = String.sub s 0 i in let s'' = - if String.for_all is_digit s' then s' else - !render_expand_fwd env show (s' $ at) [] (fun () -> render_id' env style s') + if String.for_all is_digit s' then + s' + else + !render_expand_fwd env show (s' $ at) [] (fun () -> + render_id' env style s' + ) in - (if i = n then s'' else "{" ^ s'' ^ String.sub s i (n - i) ^ "}") ^ - (if ss = [] then "" else "_{" ^ render_id_sub env `Var env.show_var at ss ^ "}") + (if i = n then s'' else "{" ^ s'' ^ String.sub s i (n - i) ^ "}") + ^ + if ss = [] then + "" + else + "_{" ^ render_id_sub env `Var env.show_var at ss ^ "}" let render_id env style show id = render_id_sub env style show id.at (String.split_on_char '_' id.it) @@ -244,26 +232,24 @@ let render_id env style show id = let render_synid env id = render_id env `Var env.show_syn id let render_varid env id = render_id env `Var env.show_var id let render_defid env id = render_id env `Func (ref Map.empty) id - -let render_atomid env id = - render_id' env `Atom (quote_id (lower id)) +let render_atomid env id = render_id' env `Atom (quote_id (lower id)) let render_ruleid env id1 id2 = let id1' = match Map.find_opt id1.it !(env.show_rel) with | None -> id1.it | Some [] -> assert false - | Some ({it = TextE s; _}::_) -> s - | Some ({at; _}::_) -> - error at "malformed `show` hint for relation" + | Some ({it = TextE s; _} :: _) -> s + | Some ({at; _} :: _) -> error at "malformed `show` hint for relation" in let id2' = if id2.it = "" then "" else "-" ^ id2.it in "\\textsc{\\scriptsize " ^ dash_id (quote_id (id1' ^ id2')) ^ "}" let render_rule_deco env pre id1 id2 post = - if not env.deco_rule then "" else - pre ^ "{[" ^ render_ruleid env id1 id2 ^ "]}" ^ post - + if not env.deco_rule then + "" + else + pre ^ "{[" ^ render_ruleid env id1 id2 ^ "]}" ^ post (* Operators *) @@ -287,14 +273,11 @@ let render_atom env = function "\\vdash" let render_brack = function - | Paren -> "(", ")" - | Brack -> "[", "]" - | Brace -> "\\{", "\\}" + | Paren -> ("(", ")") + | Brack -> ("[", "]") + | Brace -> ("\\{", "\\}") -let render_unop = function - | NotOp -> "\\neg" - | PlusOp -> "+" - | MinusOp -> "-" +let render_unop = function NotOp -> "\\neg" | PlusOp -> "+" | MinusOp -> "-" let render_binop = function | AndOp -> "\\land" @@ -315,10 +298,7 @@ let render_cmpop = function | LeOp -> "\\leq" | GeOp -> "\\geq" -let render_dots = function - | Dots -> [Elem "..."] - | NoDots -> [] - +let render_dots = function Dots -> [Elem "..."] | NoDots -> [] (* Show expansions *) @@ -330,6 +310,7 @@ let rec expand_iter args iter = | ListN e -> ListN (expand_exp args e) and expand_exp args e = expand_exp' args e.it $ e.at + and expand_exp' args e' = match e' with | VarE _ | AtomE _ | BoolE _ | NatE _ | TextE _ | EpsE -> e' @@ -386,19 +367,24 @@ and expand_exp' args e' = let iter' = expand_iter args iter in IterE (e1', iter') | HoleE false -> - (match !args with + ( match !args with | [] -> raise Arity_mismatch - | arg::args' -> args := args'; arg.it + | arg :: args' -> + args := args'; + arg.it ) - | HoleE true -> let es = !args in args := []; SeqE es + | HoleE true -> + let es = !args in + args := []; + SeqE es | FuseE (e1, e2) -> let e1' = expand_exp args e1 in let e2' = expand_exp args e2 in FuseE (e1', e2') and expand_expfield args (atom, e) = (atom, expand_exp args e) - and expand_path args p = expand_path' args p.it $ p.at + and expand_path' args p' = match p' with | RootP -> RootP @@ -413,27 +399,28 @@ and expand_path' args p' = SliceP (p1', e1', e2') | DotP (p1, atom) -> DotP (expand_path args p1, atom) - and render_expand env (show : exp list Map.t ref) id args f = match Map.find_opt id.it !show with | None -> f () | Some showexps -> let rec attempt = function | [] -> f () - | showexp::showexps' -> - try - let rargs = ref args in - let e = expand_exp rargs showexp in - if !rargs <> [] then raise Arity_mismatch; - (* Avoid cyclic expansion *) - show := Map.remove id.it !show; - Fun.protect (fun () -> render_exp env e) - ~finally:(fun () -> show := Map.add id.it showexps !show) - with Arity_mismatch -> attempt showexps' - (* HACK: Ignore arity mismatches, such that overloading notation works, - * e.g., using CONST for both instruction and relation. *) - in attempt showexps - + | showexp :: showexps' -> + ( try + let rargs = ref args in + let e = expand_exp rargs showexp in + if !rargs <> [] then raise Arity_mismatch; + (* Avoid cyclic expansion *) + show := Map.remove id.it !show; + Fun.protect + (fun () -> render_exp env e) + ~finally:(fun () -> show := Map.add id.it showexps !show) + with Arity_mismatch -> attempt showexps' + ) + (* HACK: Ignore arity mismatches, such that overloading notation works, + * e.g., using CONST for both instruction and relation. *) + in + attempt showexps (* Iteration *) @@ -443,7 +430,6 @@ and render_iter env = function | List1 -> "^{+}" | ListN {it = ParenE (e, _); _} | ListN e -> "^{" ^ render_exp env e ^ "}" - (* Types *) and render_typ env t = @@ -456,42 +442,51 @@ and render_typ env t = | TupT ts -> "(" ^ render_typs ",\\; " env ts ^ ")" | IterT (t1, iter) -> "{" ^ render_typ env t1 ^ render_iter env iter ^ "}" | StrT tfs -> - "\\{\\; " ^ - "\\begin{array}[t]{@{}l@{}}\n" ^ - concat_map_nl ",\\; " "\\\\\n " (render_typfield env) tfs ^ " \\;\\}" ^ - "\\end{array}" + "\\{\\; " + ^ "\\begin{array}[t]{@{}l@{}}\n" + ^ concat_map_nl ",\\; " "\\\\\n " (render_typfield env) tfs + ^ " \\;\\}" + ^ "\\end{array}" | 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) + (render_dots dots1 + @ map_nl_list (render_synid env) ids + @ map_nl_list (render_typcase env t.at) tcases + @ render_dots dots2 + ) | AtomT atom -> render_typcase env t.at (atom, [], []) | SeqT [] -> "\\epsilon" - | SeqT ({it = AtomT atom; at; _}::ts) -> render_typcase env at (atom, ts, []) + | 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 + 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)) - + concat sep (List.filter (( <> ) "") (List.map (render_typ env) ts)) and render_typfield env (atom, t, _hints) = render_fieldname env atom t.at ^ "~" ^ render_typ env t and render_typcase env at (atom, ts, _hints) = let es = List.map exp_of_typ ts in - render_expand env env.show_case (El.Print.string_of_atom atom $ at) es + 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 -> + 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) + "{" + ^ 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 @@ -499,14 +494,10 @@ and render_typcase env at (atom, ts, _hints) = if s1 <> "" && s2 <> "" then s1 ^ "~" ^ s2 else s1 ^ s2 ) - (* Expressions *) and untup_exp e = - match e.it with - | TupE es -> es - | ParenE (e1, _) -> [e1] - | _ -> [e] + match e.it with TupE es -> es | ParenE (e1, _) -> [e1] | _ -> [e] and render_exp env e = (* @@ -520,35 +511,51 @@ and render_exp env e = | NatE n -> string_of_int n | TextE t -> "``" ^ t ^ "''" | UnE (op, e2) -> render_unop op ^ render_exp env e2 - | BinE (e1, ExpOp, ({it = ParenE (e2, _); _ } | e2)) -> + | BinE (e1, ExpOp, ({it = ParenE (e2, _); _} | e2)) -> "{" ^ render_exp env e1 ^ "^{" ^ render_exp env e2 ^ "}}" | BinE (e1, op, e2) -> render_exp env e1 ^ space render_binop op ^ render_exp env e2 | 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 + | SeqE ({it = AtomE atom; at; _} :: es) -> render_expcase env atom es at (* Hack for binop_nt *) - | SeqE (e1::e2::es) when chop_sub_exp e1 <> None -> - "{" ^ render_exp env (Option.get (chop_sub_exp e1)) ^ "}_{" ^ - render_exps "," env (as_tup_exp e2) ^ "}" ^ - (if es = [] then "" else "\\," ^ render_exp env (SeqE es $ e.at)) + | SeqE (e1 :: e2 :: es) when chop_sub_exp e1 <> None -> + "{" + ^ render_exp env (Option.get (chop_sub_exp e1)) + ^ "}_{" + ^ render_exps "," env (as_tup_exp e2) + ^ "}" + ^ if es = [] then "" else "\\," ^ render_exp env (SeqE es $ e.at) | SeqE es -> render_exps "~" env es | IdxE (e1, e2) -> render_exp env e1 ^ "[" ^ render_exp env e2 ^ "]" | SliceE (e1, e2, e3) -> - render_exp env e1 ^ - "[" ^ render_exp env e2 ^ " : " ^ render_exp env e3 ^ "]" + render_exp env e1 + ^ "[" + ^ render_exp env e2 + ^ " : " + ^ render_exp env e3 + ^ "]" | UpdE (e1, p, e2) -> - render_exp env e1 ^ - "[" ^ render_path env p ^ " = " ^ render_exp env e2 ^ "]" + render_exp env e1 + ^ "[" + ^ render_path env p + ^ " = " + ^ render_exp env e2 + ^ "]" | ExtE (e1, p, e2) -> - render_exp env e1 ^ - "[" ^ render_path env p ^ " = .." ^ render_exp env e2 ^ "]" + render_exp env e1 + ^ "[" + ^ render_path env p + ^ " = .." + ^ render_exp env e2 + ^ "]" | StrE efs -> - "\\{ " ^ - "\\begin{array}[t]{@{}l@{}}\n" ^ - concat_map_nl ",\\; " "\\\\\n " (render_expfield env) efs ^ " \\}" ^ - "\\end{array}" + "\\{ " + ^ "\\begin{array}[t]{@{}l@{}}\n" + ^ concat_map_nl ",\\; " "\\\\\n " (render_expfield env) efs + ^ " \\}" + ^ "\\end{array}" | DotE (e1, atom) -> render_exp env e1 ^ "." ^ render_fieldname env atom e.at | CommaE (e1, e2) -> render_exp env e1 ^ ", " ^ render_exp env e2 | CompE (e1, e2) -> render_exp env e1 ^ " \\oplus " ^ render_exp env e2 @@ -560,25 +567,29 @@ and render_exp env e = | 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 + let l, r = render_brack brack in + l ^ render_exp env e ^ r | CallE (id, e1) -> - render_expand env env.show_def id (untup_exp e1) - (fun () -> + render_expand env env.show_def id (untup_exp e1) (fun () -> if not (ends_sub id.it) then match e1.it with | TupE [] -> render_defid env id | _ -> render_defid env id ^ render_exp env e1 - else - (* Handle subscripting *) - "{" ^ render_defid env (chop_sub id.it $ id.at) ^ + else (* Handle subscripting *) + "{" + ^ render_defid env (chop_sub id.it $ id.at) + ^ let e1', e2' = match untup_exp e1 with - | [] -> SeqE [] $ e1.at, SeqE [] $ e1.at - | [e1'] -> e1', SeqE [] $ e1.at - | e1'::es -> e1', TupE es $ e1.at + | [] -> (SeqE [] $ e1.at, SeqE [] $ e1.at) + | [e1'] -> (e1', SeqE [] $ e1.at) + | e1' :: es -> (e1', TupE es $ e1.at) in - "}_{" ^ render_exps "," env (as_tup_exp e1') ^ "}" ^ render_exp env e2' - ) + "}_{" + ^ render_exps "," env (as_tup_exp e1') + ^ "}" + ^ render_exp env e2' + ) | IterE (e1, iter) -> "{" ^ render_exp env e1 ^ render_iter env iter ^ "}" | FuseE (e1, e2) -> (* Hack for printing t.LOADn_sx *) @@ -587,7 +598,7 @@ and render_exp env e = | HoleE _ -> assert false and render_exps sep env es = - concat sep (List.filter ((<>) "") (List.map (render_exp env) es)) + concat sep (List.filter (( <> ) "") (List.map (render_exp env) es)) and render_expfield env (atom, e) = render_fieldname env atom e.at ^ "~" ^ render_exp env e @@ -597,24 +608,35 @@ and render_path env p = | RootP -> "" | IdxP (p1, e) -> render_path env p1 ^ "[" ^ render_exp env e ^ "]" | SliceP (p1, e1, e2) -> - render_path env p1 ^ "[" ^ render_exp env e1 ^ " : " ^ render_exp env e2 ^ "]" + render_path env p1 + ^ "[" + ^ render_exp env e1 + ^ " : " + ^ render_exp env e2 + ^ "]" | DotP ({it = RootP; _}, atom) -> render_fieldname env atom p.at - | DotP (p1, atom) -> - render_path env p1 ^ "." ^ render_fieldname env atom p.at + | DotP (p1, atom) -> render_path env p1 ^ "." ^ render_fieldname env atom p.at and render_fieldname env atom at = - render_expand env env.show_field (El.Print.string_of_atom 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 + 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 -> + 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) + "{" + ^ 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 @@ -622,10 +644,8 @@ and render_expcase env atom es at = if s1 <> "" && s2 <> "" then s1 ^ "~" ^ s2 else s1 ^ s2 ) - let () = render_expand_fwd := render_expand - (* Definitions *) let word s = "\\mbox{" ^ s ^ "}" @@ -635,201 +655,203 @@ let rec render_prem env prem = | RulePr (id, e) -> render_exp {env with current_rel = id.it} e | IfPr e -> render_exp env e | ElsePr -> error prem.at "misplaced `otherwise` premise" - | IterPr ({it = IterPr _; _} as prem', iter) -> + | IterPr (({it = IterPr _; _} as prem'), iter) -> "{" ^ render_prem env prem' ^ "}" ^ render_iter env iter | IterPr (prem', iter) -> "(" ^ render_prem env prem' ^ ")" ^ render_iter env iter - let merge_typ t1 t2 = - match t1.it, t2.it with + match (t1.it, t2.it) with | CaseT (dots1, ids1, cases1, _), CaseT (_, ids2, cases2, dots2) -> - CaseT( dots1, ids1 @ strip_nl ids2, cases1 @ strip_nl cases2, dots2) $ t1.at + CaseT (dots1, ids1 @ strip_nl ids2, cases1 @ strip_nl cases2, dots2) $ t1.at | _, _ -> assert false let rec merge_syndefs = function | [] -> [] - | {it = SynD (id1, _, t1, _); at; _}:: - {it = SynD (id2, _, t2, _); _}::ds when id1.it = id2.it -> + | {it = SynD (id1, _, t1, _); at; _} :: {it = SynD (id2, _, t2, _); _} :: ds + when id1.it = id2.it -> let d' = SynD (id1, "" $ no_region, merge_typ t1 t2, []) $ at in - merge_syndefs (d'::ds) - | d::ds -> - d :: merge_syndefs ds + merge_syndefs (d' :: ds) + | d :: ds -> d :: merge_syndefs ds let string_of_desc = function - | Some ({it = TextE s; _}::_) -> Some s - | Some ({at; _}::_) -> error at "malformed description hint" + | Some ({it = TextE s; _} :: _) -> Some s + | Some ({at; _} :: _) -> error at "malformed description hint" | _ -> None let render_syndef env d = match d.it with | SynD (id1, _id2, t, _) -> - (match env.deco_syn, string_of_desc (Map.find_opt id1.it !(env.desc_syn)) with + ( match + (env.deco_syn, string_of_desc (Map.find_opt id1.it !(env.desc_syn))) + with | true, Some s -> "\\mbox{(" ^ s ^ ")} & " | _ -> "& " - ) ^ - render_synid env id1 ^ " &::=& " ^ render_typ env t + ) + ^ render_synid env id1 + ^ " &::=& " + ^ render_typ env t | _ -> assert false let render_ruledef env d = match d.it with | RuleD (id1, id2, e, prems) -> - "\\frac{\n" ^ - (if has_nl prems then "\\begin{array}{@{}c@{}}\n" else "") ^ - altern_map_nl " \\qquad\n" " \\\\\n" (suffix "\n" (render_prem env)) prems ^ - (if has_nl prems then "\\end{array}\n" else "") ^ - "}{\n" ^ - render_exp {env with current_rel = id1.it} e ^ "\n" ^ - "}" ^ - render_rule_deco env " \\, " id1 id2 "" + "\\frac{\n" + ^ (if has_nl prems then "\\begin{array}{@{}c@{}}\n" else "") + ^ altern_map_nl " \\qquad\n" " \\\\\n" (suffix "\n" (render_prem env)) prems + ^ (if has_nl prems then "\\end{array}\n" else "") + ^ "}{\n" + ^ render_exp {env with current_rel = id1.it} e + ^ "\n" + ^ "}" + ^ render_rule_deco env " \\, " id1 id2 "" | _ -> failwith "render_ruledef" let render_conditions env = function | [] -> " & " | [Elem {it = ElsePr; _}] -> " &\\quad\n " ^ word "otherwise" - | (Elem {it = ElsePr; _})::prems -> - " &\\quad\n " ^ word "otherwise, if" ^ "~" ^ - concat_map_nl " \\\\\n &&&&\\quad {\\land}~" "" (render_prem env) prems + | Elem {it = ElsePr; _} :: prems -> + " &\\quad\n " + ^ word "otherwise, if" + ^ "~" + ^ concat_map_nl " \\\\\n &&&&\\quad {\\land}~" "" (render_prem env) prems | prems -> - " &\\quad\n " ^ word "if" ^ "~" ^ - concat_map_nl " \\\\\n &&&&\\quad {\\land}~" "" (render_prem env) prems + " &\\quad\n " + ^ word "if" + ^ "~" + ^ concat_map_nl " \\\\\n &&&&\\quad {\\land}~" "" (render_prem env) prems let render_reddef env d = match d.it with | RuleD (id1, id2, e, prems) -> let e1, e2 = match e.it with - | InfixE (e1, SqArrow, e2) -> e1, e2 + | InfixE (e1, SqArrow, e2) -> (e1, e2) | _ -> error e.at "unrecognized format for reduction rule" in - render_rule_deco env "" id1 id2 " \\quad " ^ "& " ^ - render_exp env e1 ^ " &" ^ render_atom env SqArrow ^ "& " ^ - render_exp env e2 ^ render_conditions env prems + render_rule_deco env "" id1 id2 " \\quad " + ^ "& " + ^ render_exp env e1 + ^ " &" + ^ render_atom env SqArrow + ^ "& " + ^ render_exp env e2 + ^ render_conditions env prems | _ -> failwith "render_reddef" let render_funcdef env d = match d.it with | DefD (id1, e1, e2, prems) -> - render_exp env (CallE (id1, e1) $ d.at) ^ " &=& " ^ - render_exp env e2 ^ render_conditions env prems + render_exp env (CallE (id1, e1) $ d.at) + ^ " &=& " + ^ render_exp env e2 + ^ render_conditions env prems | _ -> failwith "render_funcdef" let rec render_sep_defs ?(sep = " \\\\\n") ?(br = " \\\\[0.8ex]\n") f = function | [] -> "" - | {it = SepD; _}::ds -> "{} \\\\[-2ex]\n" ^ render_sep_defs ~sep ~br f ds - | d::{it = SepD; _}::ds -> f d ^ br ^ render_sep_defs ~sep ~br f ds - | d::ds -> f d ^ sep ^ render_sep_defs ~sep ~br f ds - + | {it = SepD; _} :: ds -> "{} \\\\[-2ex]\n" ^ render_sep_defs ~sep ~br f ds + | d :: {it = SepD; _} :: ds -> f d ^ br ^ render_sep_defs ~sep ~br f ds + | d :: ds -> f d ^ sep ^ render_sep_defs ~sep ~br f ds let rec classify_rel e : rel_sort option = match e.it with | InfixE (_, Turnstile, _) -> Some TypingRel | InfixE (_, SqArrow, _) -> Some ReductionRel | InfixE (e1, _, e2) -> - (match classify_rel e1 with - | None -> classify_rel e2 - | some -> some - ) + (match classify_rel e1 with None -> classify_rel e2 | some -> some) | _ -> None - let rec render_defs env = function | [] -> "" - | d::ds' as ds -> - match d.it with + | d :: ds' as ds -> + ( match d.it with | SynD _ -> let ds' = merge_syndefs ds in let deco = if env.deco_syn then "l" else "l@{}" in - "\\begin{array}{@{}" ^ deco ^ "rrl@{}}\n" ^ - render_sep_defs (render_syndef env) ds' ^ - "\\end{array}" + "\\begin{array}{@{}" + ^ deco + ^ "rrl@{}}\n" + ^ render_sep_defs (render_syndef env) ds' + ^ "\\end{array}" | RelD (id, t, _hints) -> - "\\boxed{" ^ - render_typ {env with current_rel = id.it} t ^ - "}" ^ - (if ds' = [] then "" else " \\; " ^ render_defs env ds') + "\\boxed{" + ^ render_typ {env with current_rel = id.it} t + ^ "}" + ^ if ds' = [] then "" else " \\; " ^ render_defs env ds' | RuleD (_, _, e, _) -> - (match classify_rel e with + ( match classify_rel e with | Some TypingRel -> - "\\begin{array}{@{}c@{}}\\displaystyle\n" ^ - render_sep_defs ~sep:"\n\\qquad\n" ~br:"\n\\\\[3ex]\\displaystyle\n" - (render_ruledef env) ds ^ - "\\end{array}" + "\\begin{array}{@{}c@{}}\\displaystyle\n" + ^ render_sep_defs ~sep:"\n\\qquad\n" ~br:"\n\\\\[3ex]\\displaystyle\n" + (render_ruledef env) ds + ^ "\\end{array}" | Some ReductionRel -> - "\\begin{array}{@{}l@{}lcl@{}l@{}}\n" ^ - render_sep_defs (render_reddef env) ds ^ - "\\end{array}" + "\\begin{array}{@{}l@{}lcl@{}l@{}}\n" + ^ render_sep_defs (render_reddef env) ds + ^ "\\end{array}" | None -> error d.at "unrecognized form of relation" ) | DefD _ -> - "\\begin{array}{@{}lcl@{}l@{}}\n" ^ - render_sep_defs (render_funcdef env) ds ^ - "\\end{array}" - | SepD -> - " \\\\\n" ^ - render_defs env ds' - | VarD _ | DecD _ | HintD _ -> - failwith "render_defs" + "\\begin{array}{@{}lcl@{}l@{}}\n" + ^ render_sep_defs (render_funcdef env) ds + ^ "\\end{array}" + | SepD -> " \\\\\n" ^ render_defs env ds' + | VarD _ | DecD _ | HintD _ -> failwith "render_defs" + ) let render_def env d = render_defs env [d] - (* Scripts *) let rec split_syndefs syndefs = function - | [] -> List.rev syndefs, [] - | d::ds -> - match d.it with - | SynD _ -> split_syndefs (d::syndefs) ds - | _ -> List.rev syndefs, d::ds + | [] -> (List.rev syndefs, []) + | d :: ds -> + ( match d.it with + | SynD _ -> split_syndefs (d :: syndefs) ds + | _ -> (List.rev syndefs, d :: ds) + ) let rec split_reddefs id reddefs = function - | [] -> List.rev reddefs, [] - | d::ds -> - match d.it with + | [] -> (List.rev reddefs, []) + | d :: ds -> + ( match d.it with | RuleD (id1, _, _, _) when id1.it = id -> - split_reddefs id (d::reddefs) ds - | _ -> List.rev reddefs, d::ds + split_reddefs id (d :: reddefs) ds + | _ -> (List.rev reddefs, d :: ds) + ) let rec split_funcdefs id funcdefs = function - | [] -> List.rev funcdefs, [] - | d::ds -> - match d.it with - | DefD (id1, _, _, _) when id1.it = id -> split_funcdefs id (d::funcdefs) ds - | _ -> List.rev funcdefs, d::ds + | [] -> (List.rev funcdefs, []) + | d :: ds -> + ( match d.it with + | DefD (id1, _, _, _) when id1.it = id -> + split_funcdefs id (d :: funcdefs) ds + | _ -> (List.rev funcdefs, d :: ds) + ) let rec render_script env = function | [] -> "" - | d::ds -> - match d.it with + | d :: ds -> + ( match d.it with | SynD _ -> let syndefs, ds' = split_syndefs [d] ds in - "$$\n" ^ render_defs env syndefs ^ "\n$$\n\n" ^ - render_script env ds' - | RelD _ -> - "$" ^ render_def env d ^ "$\n\n" ^ - render_script env ds + "$$\n" ^ render_defs env syndefs ^ "\n$$\n\n" ^ render_script env ds' + | RelD _ -> "$" ^ render_def env d ^ "$\n\n" ^ render_script env ds | RuleD (id1, _, e, _) -> - (match classify_rel e with + ( match classify_rel e with | Some TypingRel -> - "$$\n" ^ render_def env d ^ "\n$$\n\n" ^ - render_script env ds + "$$\n" ^ render_def env d ^ "\n$$\n\n" ^ render_script env ds | Some ReductionRel -> let reddefs, ds' = split_reddefs id1.it [d] ds in - "$$\n" ^ render_defs env reddefs ^ "\n$$\n\n" ^ - render_script env ds' + "$$\n" ^ render_defs env reddefs ^ "\n$$\n\n" ^ render_script env ds' | None -> error d.at "unrecognized form of relation" ) - | VarD _ -> - render_script env ds - | DecD _ -> - render_script env ds + | VarD _ -> render_script env ds + | DecD _ -> render_script env ds | DefD (id, _, _, _) -> let funcdefs, ds' = split_funcdefs id.it [d] ds in - "$$\n" ^ render_defs env funcdefs ^ "\n$$\n\n" ^ - render_script env ds' - | SepD -> - "\\vspace{1ex}\n\n" ^ - render_script env ds - | HintD _ -> - render_script env ds + "$$\n" ^ render_defs env funcdefs ^ "\n$$\n\n" ^ render_script env ds' + | SepD -> "\\vspace{1ex}\n\n" ^ render_script env ds + | HintD _ -> render_script env ds + ) diff --git a/spectec/src/backend-latex/render.mli b/spectec/src/backend-latex/render.mli index cd2c38764b..5149e78a63 100644 --- a/spectec/src/backend-latex/render.mli +++ b/spectec/src/backend-latex/render.mli @@ -1,16 +1,13 @@ open El.Ast - (* Environment *) type env val env : Config.t -> El.Ast.script -> env - val with_syntax_decoration : bool -> env -> env val with_rule_decoration : bool -> env -> env - (* Generators *) val render_atom : env -> atom -> string diff --git a/spectec/src/backend-latex/splice.ml b/spectec/src/backend-latex/splice.ml index c0ff8b9ca2..5dffac55bc 100644 --- a/spectec/src/backend-latex/splice.ml +++ b/spectec/src/backend-latex/splice.ml @@ -3,7 +3,6 @@ open Source open El.Ast open Config - (* Errors *) type source = {file : string; s : string; mutable i : int} @@ -20,7 +19,7 @@ let rec pos' src j (line, column) : Source.pos = Source.{file = src.file; line; column} else pos' src (j + 1) - (if src.s.[j] = '\n' then line + 1, 1 else line, column + 1) + (if src.s.[j] = '\n' then (line + 1, 1) else (line, column + 1)) let pos src = pos' src 0 (1, 1) @@ -28,13 +27,11 @@ let error src msg = let pos = pos src in Source.error {left = pos; right = pos} "splice replacement" msg - (* Environment *) -module Map = Map.Make(String) +module Map = Map.Make (String) type use = int ref - type syntax = {sdef : def; fragments : (string * def * use) list} type relation = {rdef : def; rules : (string * def * use) list} type definition = {fdef : def; clauses : def list; use : use} @@ -44,10 +41,9 @@ type env = render : Render.env; mutable syn : syntax Map.t; mutable rel : relation Map.t; - mutable def : definition Map.t; + mutable def : definition Map.t } - let env_def env def = match def.it with | SynD (id1, id2, _, _) -> @@ -56,8 +52,7 @@ let env_def env def = let syntax = Map.find id1.it env.syn in let fragments = syntax.fragments @ [(id2.it, def, ref 0)] in env.syn <- Map.add id1.it {syntax with fragments} env.syn - | RelD (id, _, _) -> - env.rel <- Map.add id.it {rdef = def; rules = []} env.rel + | RelD (id, _, _) -> env.rel <- Map.add id.it {rdef = def; rules = []} env.rel | RuleD (id1, id2, _, _) -> let relation = Map.find id1.it env.rel in let rules = relation.rules @ [(id2.it, def, ref 0)] in @@ -68,8 +63,7 @@ let env_def env def = let definition = Map.find id.it env.def in let clauses = definition.clauses @ [def] in env.def <- Map.add id.it {definition with clauses} env.def - | VarD _ | SepD | HintD _ -> - () + | VarD _ | SepD | HintD _ -> () let env config script : env = let env = @@ -83,7 +77,6 @@ let env config script : env = List.iter (env_def env) script; env - let warn_use use space id1 id2 = if !use <> 1 then let id = if id2 = "" then id1 else id1 ^ "/" ^ id2 in @@ -91,15 +84,18 @@ let warn_use use space id1 id2 = prerr_endline ("warning: " ^ space ^ " `" ^ id ^ "` was " ^ msg) let warn env = - Map.iter (fun id1 {fragments; _} -> - List.iter (fun (id2, _, use) -> warn_use use "syntax" id1 id2) fragments - ) env.syn; - Map.iter (fun id1 {rules; _} -> - List.iter (fun (id2, _, use) -> warn_use use "rule" id1 id2) rules - ) env.rel; + Map.iter + (fun id1 {fragments; _} -> + List.iter (fun (id2, _, use) -> warn_use use "syntax" id1 id2) fragments + ) + env.syn; + Map.iter + (fun id1 {rules; _} -> + List.iter (fun (id2, _, use) -> warn_use use "rule" id1 id2) rules + ) + env.rel; Map.iter (fun id1 {use; _} -> warn_use use "definition" id1 "") env.def - let find_nosub space src id1 id2 = if id2 <> "" then error src ("unknown " ^ space ^ " identifier `" ^ id1 ^ "/" ^ id2 ^ "`") @@ -108,11 +104,16 @@ let match_full re s = Str.string_match re s 0 && Str.match_end () = String.length s let find_entries space src id1 id2 entries = - let re = Str.(regexp (global_replace (regexp "\\*\\|\\?") (".\\0") id2)) in + let re = Str.(regexp (global_replace (regexp "\\*\\|\\?") ".\\0" id2)) in let defs = List.filter (fun (id, _, _) -> match_full re id) entries in if defs = [] then error src ("unknown " ^ space ^ " identifier `" ^ id1 ^ "/" ^ id2 ^ "`"); - List.map (fun (_, def, use) -> incr use; def) defs + List.map + (fun (_, def, use) -> + incr use; + def + ) + defs let find_syntax env src id1 id2 = match Map.find_opt id1 env.syn with @@ -137,42 +138,53 @@ let find_func env src id1 id2 = | Some definition -> if definition.clauses = [] then error src ("definition `" ^ id1 ^ "` has no clauses"); - incr definition.use; definition.clauses - + incr definition.use; + definition.clauses (* Parsing *) let len = String.length let rec parse_space src = - if not (eos src) && (get src = ' ' || get src = '\t' || get src = '\n') then - (adv src; parse_space src) + if (not (eos src)) && (get src = ' ' || get src = '\t' || get src = '\n') then ( + adv src; + parse_space src + ) let rec try_string' s i s' j : bool = - j = len s' || s.[i] = s'.[j] && try_string' s (i + 1) s' (j + 1) + j = len s' || (s.[i] = s'.[j] && try_string' s (i + 1) s' (j + 1)) let try_string src s : bool = - left src >= len s && try_string' src.s src.i s 0 && (advn src (len s); true) + left src >= len s + && try_string' src.s src.i s 0 + && + ( advn src (len s); + true + ) -let try_anchor_start src anchor : bool = - try_string src (anchor ^ "{") +let try_anchor_start src anchor : bool = try_string src (anchor ^ "{") let rec parse_anchor_end src j depth = if eos src then error {src with i = j} "unclosed anchor" - else if get src = '{' then - (adv src; parse_anchor_end src j (depth + 1)) - else if get src <> '}' then - (adv src; parse_anchor_end src j depth) - else if depth > 0 then - (adv src; parse_anchor_end src j (depth - 1)) + else if get src = '{' then ( + adv src; + parse_anchor_end src j (depth + 1) + ) else if get src <> '}' then ( + adv src; + parse_anchor_end src j depth + ) else if depth > 0 then ( + adv src; + parse_anchor_end src j (depth - 1) + ) let rec parse_id' src = if not (eos src) then - match get src with - | 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' | '\'' | '`' | '-' | '*' -> - (adv src; parse_id' src) - | _ -> () + match get src with + | 'A' .. 'Z' | 'a' .. 'z' | '0' .. '9' | '_' | '\'' | '`' | '-' | '*' -> + adv src; + parse_id' src + | _ -> () let parse_id src space : string = let j = src.i in @@ -186,55 +198,66 @@ let parse_id_id env src space1 space2 find : def list = let id1 = parse_id src space1 in let id2 = if space2 <> "" && try_string src "/" then parse_id src space2 else "" - in find env {src with i = j} id1 id2 + in + find env {src with i = j} id1 id2 let rec parse_id_id_list env src space1 space2 find : def list = parse_space src; - if try_string src "}" then [] else - let defs1 = parse_id_id env src space1 space2 find in - let defs2 = parse_id_id_list env src space1 space2 find in - defs1 @ defs2 + if try_string src "}" then + [] + else + let defs1 = parse_id_id env src space1 space2 find in + let defs2 = parse_id_id_list env src space1 space2 find in + defs1 @ defs2 let rec parse_group_list env src space1 space2 find : def list list = parse_space src; - if try_string src "}" then [] else - let groups = - if try_string src "{" then - [parse_id_id_list env src space1 space2 find] - else - List.map (fun def -> [def]) (parse_id_id env src space1 space2 find) - in - groups @ parse_group_list env src space1 space2 find + if try_string src "}" then + [] + else + let groups = + if try_string src "{" then + [parse_id_id_list env src space1 space2 find] + else + List.map (fun def -> [def]) (parse_id_id env src space1 space2 find) + in + groups @ parse_group_list env src space1 space2 find let try_def_anchor env src r sort space1 space2 find deco : bool = let b = try_string src sort in if b then ( parse_space src; - if not (try_string src ":") then - error src "colon `:` expected"; + if not (try_string src ":") then error src "colon `:` expected"; let groups = parse_group_list env src space1 space2 find in - let defs = List.tl (List.concat_map ((@) [SepD $ no_region]) groups) in - let env' = env.render + let defs = List.tl (List.concat_map (( @ ) [SepD $ no_region]) groups) in + let env' = + env.render |> Render.with_syntax_decoration deco |> Render.with_rule_decoration deco - in r := Render.render_defs env' defs + in + r := Render.render_defs env' defs ); b let try_exp_anchor env src r : bool = let b = try_string src ":" in if b then ( - let j = src.i in + let j = src.i in parse_anchor_end src (j - 4) 0; let s = str src j in adv src; let exp = - try Frontend.Parse.parse_exp s with Source.Error (at, msg) -> + try Frontend.Parse.parse_exp s + with Source.Error (at, msg) -> (* Translate relative positions *) let pos = pos {src with i = j} in let shift {line; column; _} = - { file = src.file; line = line + pos.line - 1; - column = if false(*line = 1*) then column + pos.column - 1 else column} in + { file = src.file; + line = line + pos.line - 1; + column = + (if false (*line = 1*) then column + pos.column - 1 else column) + } + in let at' = {left = shift at.left; right = shift at.right} in raise (Source.Error (at', msg)) in @@ -242,46 +265,49 @@ let try_exp_anchor env src r : bool = ); b - (* Splicing *) let splice_anchor env src anchor buf = parse_space src; Buffer.add_string buf anchor.prefix; let r = ref "" in - ignore ( - try_exp_anchor env src r || - try_def_anchor env src r "syntax+" "syntax" "fragment" find_syntax true || - try_def_anchor env src r "syntax" "syntax" "fragment" find_syntax false || - try_def_anchor env src r "relation" "relation" "" find_relation false || - try_def_anchor env src r "rule+" "relation" "rule" find_rule true || - try_def_anchor env src r "rule" "relation" "rule" find_rule false || - try_def_anchor env src r "definition" "definition" "" find_func false || - error src "unknown definition sort"; - ); + ignore + (try_exp_anchor env src r + || try_def_anchor env src r "syntax+" "syntax" "fragment" find_syntax true + || try_def_anchor env src r "syntax" "syntax" "fragment" find_syntax false + || try_def_anchor env src r "relation" "relation" "" find_relation false + || try_def_anchor env src r "rule+" "relation" "rule" find_rule true + || try_def_anchor env src r "rule" "relation" "rule" find_rule false + || try_def_anchor env src r "definition" "definition" "" find_func false + || error src "unknown definition sort" + ); let s = - if anchor.indent = "" then !r else - Str.(global_replace (regexp "\n") ("\n" ^ anchor.indent) !r) + if anchor.indent = "" then + !r + else + Str.(global_replace (regexp "\n") ("\n" ^ anchor.indent) !r) in Buffer.add_string buf s; Buffer.add_string buf anchor.suffix let rec try_anchors env src buf = function | [] -> false - | anchor::anchors -> - if try_anchor_start src anchor.token then - (splice_anchor env src anchor buf; true) - else + | anchor :: anchors -> + if try_anchor_start src anchor.token then ( + splice_anchor env src anchor buf; + true + ) else try_anchors env src buf anchors let rec splice_all env src buf = if not (eos src) then ( - if not (try_anchors env src buf env.config.anchors) then - (Buffer.add_char buf (get src); adv src); + if not (try_anchors env src buf env.config.anchors) then ( + Buffer.add_char buf (get src); + adv src + ); splice_all env src buf ) - (* Entry points *) let splice_string env file s : string = @@ -292,11 +318,13 @@ let splice_string env file s : string = let splice_file ?(dry = false) env file = let ic = In_channel.open_text file in let s = - Fun.protect (fun () -> In_channel.input_all ic) + Fun.protect + (fun () -> In_channel.input_all ic) ~finally:(fun () -> In_channel.close ic) in let s' = splice_string env file s in if not dry then let oc = Out_channel.open_text file in - Fun.protect (fun () -> Out_channel.output_string oc s') + Fun.protect + (fun () -> Out_channel.output_string oc s') ~finally:(fun () -> Out_channel.close oc) diff --git a/spectec/src/backend-latex/splice.mli b/spectec/src/backend-latex/splice.mli index 3d3cba329a..e3c70b2b3b 100644 --- a/spectec/src/backend-latex/splice.mli +++ b/spectec/src/backend-latex/splice.mli @@ -1,8 +1,6 @@ type env val env : Config.t -> El.Ast.script -> env - val splice_string : env -> string -> string -> string (* raise Source.Error *) val splice_file : ?dry:bool -> env -> string -> unit (* raise Source.Error *) - val warn : env -> unit diff --git a/spectec/src/backend-prose/dune b/spectec/src/backend-prose/dune index 2809e9198c..b06ae2f289 100644 --- a/spectec/src/backend-prose/dune +++ b/spectec/src/backend-prose/dune @@ -1,5 +1,4 @@ (library - (name backend_prose) - (libraries util il el) - (modules translate il2ir print ir) -) + (name backend_prose) + (libraries util il el) + (modules translate il2ir print ir)) diff --git a/spectec/src/backend-prose/il2ir.ml b/spectec/src/backend-prose/il2ir.ml index 87cb7c00fe..74b3f6003e 100644 --- a/spectec/src/backend-prose/il2ir.ml +++ b/spectec/src/backend-prose/il2ir.ml @@ -4,82 +4,81 @@ open Il (** Translate `Ast.exp` **) (* `Ast.exp` -> `Ir.expr` *) -let translate_expr exp = match exp.it with - | _ -> Ir.YetE (Print.string_of_exp exp) +let translate_expr exp = + match exp.it with _ -> Ir.YetE (Print.string_of_exp exp) (* `Ast.exp` -> `Ir.AssertI` *) -let insert_assert exp = match exp.it with - | Ast.CaseE ( - Atom "CONST", - { it = TupE({ it = CaseE (Atom "I32", _); _ } :: _); _ } - ) -> - Ir.AssertI - "Due to validation, a value of value type i32 is on the top of the stack" - | _ -> - Ir.AssertI "Due to validation, a value is on the top of the stack" +let insert_assert exp = + match exp.it with + | Ast.CaseE + (Atom "CONST", {it = TupE ({it = CaseE (Atom "I32", _); _} :: _); _}) -> + Ir.AssertI + "Due to validation, a value of value type i32 is on the top of the stack" + | _ -> Ir.AssertI "Due to validation, a value is on the top of the stack" (* `Ast.exp` -> `Ir.instr list` *) -let rec lhs2pop exp = match exp.it with +let rec lhs2pop exp = + match exp.it with (* TODO: Handle bubble-up semantics *) | Ast.ListE exps -> - let rev = List.rev exps |> List.tl in - List.fold_right - (fun e acc -> insert_assert e :: Ir.PopI (Some (translate_expr e)) :: acc) - rev - [] + let rev = List.rev exps |> List.tl in + List.fold_right + (fun e acc -> insert_assert e :: Ir.PopI (Some (translate_expr e)) :: acc) + rev [] | Ast.CatE (iterexp, listexp) -> - insert_assert iterexp :: - Ir.PopI (Some (translate_expr iterexp)) :: - lhs2pop listexp + insert_assert iterexp + :: Ir.PopI (Some (translate_expr iterexp)) + :: lhs2pop listexp | _ -> failwith "Unreachable" (* `Ast.CaseE | Ast.SubE` -> `Ir.instr list` *) -let casesub2instrs exp = match exp.it with +let casesub2instrs exp = + match exp.it with | Ast.CaseE (Atom "TRAP", _) -> [Ir.TrapI] - | Ast.CaseE (Atom atomid, _) - when atomid = "CONST" || atomid = "REF.FUNC_ADDR" -> - [Ir.PushI (translate_expr exp)] + | Ast.CaseE (Atom atomid, _) when atomid = "CONST" || atomid = "REF.FUNC_ADDR" + -> + [Ir.PushI (translate_expr exp)] | Ast.CaseE (Atom "FRAME_", tupexp) -> - [Ir.LetI (Ir.NameE (Ir.N "F"), Ir.FrameE); Ir.PushI (translate_expr tupexp)] + [Ir.LetI (Ir.NameE (Ir.N "F"), Ir.FrameE); Ir.PushI (translate_expr tupexp)] | Ast.CaseE (Atom "LABEL_", _) -> - (* TODO *) - [ Ir.LetI (Ir.NameE (Ir.N "L"), Ir.YetE ""); Ir.EnterI ("Yet", YetE "") ] + (* TODO *) + [Ir.LetI (Ir.NameE (Ir.N "L"), Ir.YetE ""); Ir.EnterI ("Yet", YetE "")] | Ast.CaseE (Atom atomid, argexp) - when String.starts_with ~prefix: "TABLE." atomid || - String.starts_with ~prefix: "MEMORY." atomid || - atomid = "LOAD" || atomid = "STORE" || - atomid = "BLOCK" || atomid = "BR" || atomid = "CALL_ADDR" || - atomid = "LOCAL.SET" || atomid = "RETURN" -> - (match argexp.it with - | Ast.TupE (exps) -> - let argexprs = List.map translate_expr exps in - [Ir.ExecuteI (atomid, argexprs)] - | _ -> [Ir.ExecuteI (atomid, [translate_expr argexp])]) + when String.starts_with ~prefix:"TABLE." atomid + || String.starts_with ~prefix:"MEMORY." atomid + || atomid = "LOAD" + || atomid = "STORE" + || atomid = "BLOCK" + || atomid = "BR" + || atomid = "CALL_ADDR" + || atomid = "LOCAL.SET" + || atomid = "RETURN" -> + ( match argexp.it with + | Ast.TupE exps -> + let argexprs = List.map translate_expr exps in + [Ir.ExecuteI (atomid, argexprs)] + | _ -> [Ir.ExecuteI (atomid, [translate_expr argexp])] + ) | Ast.SubE (_, _, _) -> [Ir.PushI (YetE (Print.string_of_exp exp))] | _ -> failwith "Unreachable" (* `Ast.exp` -> `Ir.instr list` *) let rec rhs2instrs exp = match exp.it with - | Ast.MixE ( - [[]; [Ast.Semicolon]; [Ast.Star]], - (* z' ; instr'* *) - { it = TupE ([callexp; rhs]); _ } - ) -> - let yet_instr = Ir.YetI ("Perform " ^ Print.string_of_exp callexp) in - let push_instrs = rhs2instrs rhs in - yet_instr :: push_instrs - | Ast.ListE (exps) -> List.map casesub2instrs exps |> List.flatten - | Ast.IterE (_, _) -> [Ir.PushI (YetE (Print.string_of_exp exp))] - | Ast.CatE (exp1, exp2) -> - rhs2instrs exp1 @ rhs2instrs exp2 - | _ -> failwith "Unreachable" - -let check_nop instrs = match instrs with - | [] -> [Ir.NopI] - | _ -> instrs - + | Ast.MixE + ( [[]; [Ast.Semicolon]; [Ast.Star]], + (* z' ; instr'* *) + {it = TupE [callexp; rhs]; _} + ) -> + let yet_instr = Ir.YetI ("Perform " ^ Print.string_of_exp callexp) in + let push_instrs = rhs2instrs rhs in + yet_instr :: push_instrs + | Ast.ListE exps -> List.map casesub2instrs exps |> List.flatten + | Ast.IterE (_, _) -> [Ir.PushI (YetE (Print.string_of_exp exp))] + | Ast.CatE (exp1, exp2) -> rhs2instrs exp1 @ rhs2instrs exp2 + | _ -> failwith "Unreachable" +let check_nop instrs = match instrs with [] -> [Ir.NopI] | _ -> instrs (** Translate `Ast.premise` **) @@ -87,95 +86,94 @@ let check_nop instrs = match instrs with let prem2let prems = List.filter_map (function - | { it = Ast.IfPr { it = Ast.CmpE (Ast.EqOp, exp1, exp2); _ }; _ } -> - Some (Ir.LetI (translate_expr exp1, translate_expr exp2)) - | _ -> None) + | {it = Ast.IfPr {it = Ast.CmpE (Ast.EqOp, exp1, exp2); _}; _} -> + Some (Ir.LetI (translate_expr exp1, translate_expr exp2)) + | _ -> None + ) prems (* `Ast.prem list` -> `Ir.cond` *) -let prem2cond _prems = Ir.YetC ("") - - +let prem2cond _prems = Ir.YetC "" (** Main translation **) (* `reduction_group list` -> `Backend-prose.Ir.Program` *) let reduction_group2program reduction_group acc = - let (reduction_name, lhs, _, _) = List.hd reduction_group in + let reduction_name, lhs, _, _ = List.hd reduction_group in let program_name = String.split_on_char '-' reduction_name |> List.hd in - let pop_instrs = match lhs.it with + let pop_instrs = + match lhs.it with (* z; lhs *) - | Ast.MixE ( - [[]; [Ast.Semicolon]; [Ast.Star]], - {it=Ast.TupE ({it=Ast.VarE {it="z"; _ }; _ } :: exp :: []); _} - ) -> lhs2pop exp - | _ -> lhs2pop lhs in - - let instrs = match reduction_group with + | Ast.MixE + ( [[]; [Ast.Semicolon]; [Ast.Star]], + {it = Ast.TupE [{it = Ast.VarE {it = "z"; _}; _}; exp]; _} + ) -> + lhs2pop exp + | _ -> lhs2pop lhs + in + + let instrs = + match reduction_group with (* one reduction rule: assignment *) | [(_, _, rhs, prems)] -> - let let_instrs = prem2let prems in - let push_instrs = rhs2instrs rhs in - let_instrs @ push_instrs + let let_instrs = prem2let prems in + let push_instrs = rhs2instrs rhs in + let_instrs @ push_instrs (* multiple reduction rules: conditions *) | _ -> - List.map - (fun (_, _, rhs, prems) -> - let cond = prem2cond prems in - let rhs_instrs = rhs2instrs rhs |> check_nop in - Ir.IfI(cond, rhs_instrs, []) - ) - reduction_group in + List.map + (fun (_, _, rhs, prems) -> + let cond = prem2cond prems in + let rhs_instrs = rhs2instrs rhs |> check_nop in + Ir.IfI (cond, rhs_instrs, []) + ) + reduction_group + in - let body = (pop_instrs @ instrs) |> check_nop in + let body = pop_instrs @ instrs |> check_nop in Ir.Program (program_name, body) :: acc - - (** Temporarily convert `Ast.RuleD` into `reduction_group` **) type reduction_group = (string * Ast.exp * Ast.exp * Ast.premise list) list (* extract rules except Step/pure and Step/read *) -let extract_rules def acc = match def.it with - | Ast.RelD (id, _, _, rules) - when String.starts_with ~prefix:"Step" id.it -> - let filter_context = - (fun rule -> - let Ast.RuleD (ruleid, _, _, _, _) = rule.it in - ruleid.it <> "pure" && ruleid.it <> "read") in - (List.filter filter_context rules) :: acc +let extract_rules def acc = + match def.it with + | Ast.RelD (id, _, _, rules) when String.starts_with ~prefix:"Step" id.it -> + let filter_context rule = + let (Ast.RuleD (ruleid, _, _, _, _)) = rule.it in + ruleid.it <> "pure" && ruleid.it <> "read" + in + List.filter filter_context rules :: acc | _ -> acc -let name_of_rule rule = - let Ast.RuleD (id1, _, _, _, _) = rule.it in +let name_of_rule rule = + let (Ast.RuleD (id1, _, _, _, _)) = rule.it in String.split_on_char '-' id1.it |> List.hd let rule2tup rule = - let Ast.RuleD (id, _, _, exp, prems) = rule.it in + let (Ast.RuleD (id, _, _, exp, prems)) = rule.it in match exp.it with - | Ast.TupE (lhs :: rhs :: []) -> (id.it, lhs, rhs, prems) - | _ -> failwith "Unreachable" + | Ast.TupE [lhs; rhs] -> (id.it, lhs, rhs, prems) + | _ -> failwith "Unreachable" (* group reduction rules that have same name *) let rec group = function | [] -> [] | h :: t -> - let (reduction_group, rem) = - List.partition - (fun rule -> name_of_rule h = name_of_rule rule) - t in - List.map rule2tup (h :: reduction_group) :: (group rem) - - + let reduction_group, rem = + List.partition (fun rule -> name_of_rule h = name_of_rule rule) t + in + List.map rule2tup (h :: reduction_group) :: group rem (** Entry **) (* `Ast.script` -> `Ir.Program` *) let translate il = let rules = List.fold_right extract_rules il [] |> List.flatten in - let reduction_groups: reduction_group list = group rules in + let reduction_groups : reduction_group list = group rules in List.fold_right reduction_group2program reduction_groups [] diff --git a/spectec/src/backend-prose/print.ml b/spectec/src/backend-prose/print.ml index bed3c6fa28..1575ca9bd4 100644 --- a/spectec/src/backend-prose/print.ml +++ b/spectec/src/backend-prose/print.ml @@ -8,16 +8,19 @@ let indent = " " let string_of_list stringifier left sep right = function | [] -> left ^ right | h :: t -> - left - ^ List.fold_left - (fun acc elem -> acc ^ sep ^ stringifier elem) - (stringifier h) t - ^ right + left + ^ List.fold_left + (fun acc elem -> acc ^ sep ^ stringifier elem) + (stringifier h) t + ^ right let rec repeat str num = - if num = 0 then "" - else if Int.rem num 2 = 0 then repeat (str ^ str) (num / 2) - else str ^ repeat (str ^ str) (num / 2) + if num = 0 then + "" + else if Int.rem num 2 = 0 then + repeat (str ^ str) (num / 2) + else + str ^ repeat (str ^ str) (num / 2) (* structured stringifier *) @@ -31,105 +34,141 @@ let rec structured_string_of_name = function (* expression *) let rec structured_string_of_expr = function - | ValueE (i) -> "ValueE " ^ string_of_int i + | ValueE i -> "ValueE " ^ string_of_int i | AddE (e1, e2) -> - "AddE (" ^ - structured_string_of_expr e1 ^ ", " ^ - structured_string_of_expr e2 ^ ")" + "AddE (" + ^ structured_string_of_expr e1 + ^ ", " + ^ structured_string_of_expr e2 + ^ ")" | MulE (e1, e2) -> - "MulE (" ^ - structured_string_of_expr e1 ^ ", " ^ - structured_string_of_expr e2 ^ ")" + "MulE (" + ^ structured_string_of_expr e1 + ^ ", " + ^ structured_string_of_expr e2 + ^ ")" | DivE (e1, e2) -> - "DivE (" ^ - structured_string_of_expr e1 ^ ", " ^ - structured_string_of_expr e2 ^ ")" + "DivE (" + ^ structured_string_of_expr e1 + ^ ", " + ^ structured_string_of_expr e2 + ^ ")" | VecE (e1, e2) -> - "VecE (" ^ - structured_string_of_expr e1 ^ ", " ^ - structured_string_of_expr e2 ^ ")" + "VecE (" + ^ structured_string_of_expr e1 + ^ ", " + ^ structured_string_of_expr e2 + ^ ")" | AppE (n, nl) -> - "AppE (" ^ - structured_string_of_name n ^ ", " ^ - string_of_list structured_string_of_expr "[ " ", " " ]" nl ^ ")" + "AppE (" + ^ structured_string_of_name n + ^ ", " + ^ string_of_list structured_string_of_expr "[ " ", " " ]" nl + ^ ")" | NdAppE (n, nl) -> - "NdAppE (" ^ - structured_string_of_name n ^ ", " ^ - string_of_list structured_string_of_expr "[ " ", " " ]" nl ^ ")" + "NdAppE (" + ^ structured_string_of_name n + ^ ", " + ^ string_of_list structured_string_of_expr "[ " ", " " ]" nl + ^ ")" | RangedAppE (n, e1, e2) -> - "RangedAppE (" ^ - structured_string_of_name n ^ ", " ^ - structured_string_of_expr e1 ^ ", " ^ - structured_string_of_expr e2 ^ ")" + "RangedAppE (" + ^ structured_string_of_name n + ^ ", " + ^ structured_string_of_expr e1 + ^ ", " + ^ structured_string_of_expr e2 + ^ ")" | WithAppE (n, e, s) -> - "WithAppE (" ^ - structured_string_of_name n ^ ", " ^ - structured_string_of_expr e ^ ", " ^ - s ^ ")" + "WithAppE (" + ^ structured_string_of_name n + ^ ", " + ^ structured_string_of_expr e + ^ ", " + ^ s + ^ ")" | ConcatE (e1, e2) -> - "ConcatE (" ^ - structured_string_of_expr e1 ^ ", " ^ - structured_string_of_expr e2 ^ ")" + "ConcatE (" + ^ structured_string_of_expr e1 + ^ ", " + ^ structured_string_of_expr e2 + ^ ")" | LengthE e -> "LengthE (" ^ structured_string_of_expr e ^ ")" | ArityE e -> "ArityE (" ^ structured_string_of_expr e ^ ")" | FrameE -> "FrameE" | BitWidthE expr -> "BitWidthE (" ^ structured_string_of_expr expr ^ ")" | PropE (e, s) -> "PropE (" ^ structured_string_of_expr e ^ ", " ^ s ^ ")" | IndexAccessE (e1, e2) -> - "IndexAccessE (" ^ - structured_string_of_expr e1 ^ ", " ^ - structured_string_of_expr e2 ^ ")" + "IndexAccessE (" + ^ structured_string_of_expr e1 + ^ ", " + ^ structured_string_of_expr e2 + ^ ")" | SliceAccessE (e1, e2, e3) -> - "SliceAccessE (" ^ - structured_string_of_expr e1 ^ ", " ^ - structured_string_of_expr e2 ^ ", " ^ - structured_string_of_expr e3 ^ ")" + "SliceAccessE (" + ^ structured_string_of_expr e1 + ^ ", " + ^ structured_string_of_expr e2 + ^ ", " + ^ structured_string_of_expr e3 + ^ ")" | ForWhichE cond -> "ForWhichE (" ^ structured_string_of_cond cond ^ ")" | RecordE l -> - "RecordE (" ^ string_of_list structured_string_of_field "[" ", " "]" l ^ ")" + "RecordE (" ^ string_of_list structured_string_of_field "[" ", " "]" l ^ ")" | PageSizeE -> "PageSizeE" | AfterCallE -> "AfterCallE" | ContE e1 -> "ContE (" ^ structured_string_of_expr e1 ^ ")" | LabelNthE e1 -> "LabelNthE (" ^ structured_string_of_expr e1 ^ ")" | LabelE (e1, e2) -> - "LabelE (" ^ - structured_string_of_expr e1 ^ ", " ^ - structured_string_of_expr e2 ^ ")" + "LabelE (" + ^ structured_string_of_expr e1 + ^ ", " + ^ structured_string_of_expr e2 + ^ ")" | NameE n -> "NameE (" ^ structured_string_of_name n ^ ")" | ConstE (n, e) -> - "ConstE (" ^ - structured_string_of_name n ^ ", " ^ - structured_string_of_expr e ^ ")" + "ConstE (" + ^ structured_string_of_name n + ^ ", " + ^ structured_string_of_expr e + ^ ")" | RefNullE n -> "RefNullE (" ^ structured_string_of_name n ^ ")" | YetE s -> "YetE (" ^ s ^ ")" and structured_string_of_field (n, e) = "(" ^ structured_string_of_name n ^ ", " ^ structured_string_of_expr e ^ ")" - (* condition *) and structured_string_of_cond = function | NotC c -> "NotC (" ^ structured_string_of_cond c ^ ")" | AndC (c1, c2) -> - "AndC (" ^ - structured_string_of_cond c1 ^ ", " ^ - structured_string_of_cond c2 ^ ")" + "AndC (" + ^ structured_string_of_cond c1 + ^ ", " + ^ structured_string_of_cond c2 + ^ ")" | OrC (c1, c2) -> - "OrC (" ^ - structured_string_of_cond c1 ^ ", " ^ - structured_string_of_cond c2 ^ ")" + "OrC (" + ^ structured_string_of_cond c1 + ^ ", " + ^ structured_string_of_cond c2 + ^ ")" | EqC (e1, e2) -> - "EqC (" ^ - structured_string_of_expr e1 ^ ", " ^ - structured_string_of_expr e2 ^ ")" + "EqC (" + ^ structured_string_of_expr e1 + ^ ", " + ^ structured_string_of_expr e2 + ^ ")" | LtC (e1, e2) -> - "LtC (" ^ - structured_string_of_expr e1 ^ ", " ^ - structured_string_of_expr e2 ^ ")" + "LtC (" + ^ structured_string_of_expr e1 + ^ ", " + ^ structured_string_of_expr e2 + ^ ")" | DefinedC e -> "DefinedC (" ^ structured_string_of_expr e ^ ")" | PartOfC el -> - "PartOfC (" ^ string_of_list structured_string_of_expr "[" ", " "]" el ^ ")" + "PartOfC (" ^ string_of_list structured_string_of_expr "[" ", " "]" el ^ ")" | TopC s -> "TopC (" ^ s ^ ")" | YetC s -> "YetC (" ^ s ^ ")" @@ -137,54 +176,82 @@ and structured_string_of_cond = function let rec structured_string_of_instr depth = function | IfI (c, t, e) -> - "IfI (\n" ^ repeat indent (depth + 1) ^ - structured_string_of_cond c ^ "\n" ^ repeat indent depth ^ "then\n" ^ - structured_string_of_instrs (depth + 1) t ^ repeat indent depth ^ "else\n" ^ - structured_string_of_instrs (depth + 1) e ^ repeat indent depth ^ ")" + "IfI (\n" + ^ repeat indent (depth + 1) + ^ structured_string_of_cond c + ^ "\n" + ^ repeat indent depth + ^ "then\n" + ^ structured_string_of_instrs (depth + 1) t + ^ repeat indent depth + ^ "else\n" + ^ structured_string_of_instrs (depth + 1) e + ^ repeat indent depth + ^ ")" | WhileI (c, il) -> - "WhileI (\n" ^ repeat indent (depth + 1) ^ - structured_string_of_cond c ^ ":\n" ^ - structured_string_of_instrs (depth + 1) il ^ repeat indent depth ^ ")" + "WhileI (\n" + ^ repeat indent (depth + 1) + ^ structured_string_of_cond c + ^ ":\n" + ^ structured_string_of_instrs (depth + 1) il + ^ repeat indent depth + ^ ")" | RepeatI (e, il) -> - "RepeatI (\n" ^ - repeat indent (depth + 1) ^ - structured_string_of_expr e ^ ":\n" ^ - structured_string_of_instrs (depth + 1) il ^ - repeat indent depth ^ ")" + "RepeatI (\n" + ^ repeat indent (depth + 1) + ^ structured_string_of_expr e + ^ ":\n" + ^ structured_string_of_instrs (depth + 1) il + ^ repeat indent depth + ^ ")" | EitherI (il1, il2) -> - "EitherI (\n" ^ - structured_string_of_instrs (depth + 1) il1 ^ repeat indent depth ^ "Or\n" ^ - structured_string_of_instrs (depth + 1) il2 ^ repeat indent depth ^ ")" + "EitherI (\n" + ^ structured_string_of_instrs (depth + 1) il1 + ^ repeat indent depth + ^ "Or\n" + ^ structured_string_of_instrs (depth + 1) il2 + ^ repeat indent depth + ^ ")" | AssertI s -> "AssertI (" ^ s ^ ")" | PushI e -> "PushI (" ^ structured_string_of_expr e ^ ")" | PopI None -> "PopI" | PopI (Some e) -> "PopI (" ^ structured_string_of_expr e ^ ")" | LetI (n, e) -> - "LetI (" ^ structured_string_of_expr n ^ ", " ^ structured_string_of_expr e ^ ")" + "LetI (" + ^ structured_string_of_expr n + ^ ", " + ^ structured_string_of_expr e + ^ ")" | TrapI -> "TrapI" | NopI -> "NopI" | ReturnI -> "ReturnI" | InvokeI e -> "InvokeI (" ^ structured_string_of_expr e ^ ")" | EnterI (s, e) -> "EnterI (" ^ s ^ ", " ^ structured_string_of_expr e ^ ")" | ExecuteI (s, el) -> - "ExecuteI (" ^ - s ^ ", " ^ - string_of_list structured_string_of_expr "[" ", " "]" el ^ ")" + "ExecuteI (" + ^ s + ^ ", " + ^ string_of_list structured_string_of_expr "[" ", " "]" el + ^ ")" | ReplaceI (e1, e2) -> - "ReplaceI (" ^ - structured_string_of_expr e1 ^ ", " ^ - structured_string_of_expr e2 ^ ")" + "ReplaceI (" + ^ structured_string_of_expr e1 + ^ ", " + ^ structured_string_of_expr e2 + ^ ")" | JumpI e -> "JumpI (" ^ structured_string_of_expr e ^ ")" | YetI s -> "YetI " ^ s and structured_string_of_instrs depth instrs = List.fold_left (fun acc i -> - acc ^ repeat indent depth ^ structured_string_of_instr depth i ^ "\n") + acc ^ repeat indent depth ^ structured_string_of_instr depth i ^ "\n" + ) "" instrs let structured_string_of_program = function - | Program (name, instrs) -> name ^ ":\n" ^ structured_string_of_instrs 1 instrs + | Program (name, instrs) -> + name ^ ":\n" ^ structured_string_of_instrs 1 instrs (* IR stringifier *) @@ -197,57 +264,53 @@ let rec string_of_name = function let rec string_of_expr = function | ValueE i -> string_of_int i | AddE (e1, e2) -> - sprintf "the integer (%s + %s)" (string_of_expr e1) (string_of_expr e2) + sprintf "the integer (%s + %s)" (string_of_expr e1) (string_of_expr e2) | MulE (e1, e2) -> - sprintf "the integer (%s · %s)" (string_of_expr e1) (string_of_expr e2) + sprintf "the integer (%s · %s)" (string_of_expr e1) (string_of_expr e2) | DivE (e1, e2) -> - sprintf "the integer (%s / %s)" (string_of_expr e1) (string_of_expr e2) + sprintf "the integer (%s / %s)" (string_of_expr e1) (string_of_expr e2) | VecE (e1, e2) -> sprintf "%s^%s" (string_of_expr e1) (string_of_expr e2) | AppE (n, el) -> - sprintf "the result of computing %s(%s)" - (string_of_name n) - (string_of_list string_of_expr "" ", " "" el) + sprintf "the result of computing %s(%s)" (string_of_name n) + (string_of_list string_of_expr "" ", " "" el) | NdAppE (n, el) -> - sprintf "a possible result of computing %s(%s)" - (string_of_name n) - (string_of_list string_of_expr "" ", " "" el) + sprintf "a possible result of computing %s(%s)" (string_of_name n) + (string_of_list string_of_expr "" ", " "" el) | RangedAppE (n, e1, e2) -> - sprintf "the result of computing %s(%s ... %s)" - (string_of_name n) - (string_of_expr e1) - (string_of_expr e2) + sprintf "the result of computing %s(%s ... %s)" (string_of_name n) + (string_of_expr e1) (string_of_expr e2) | WithAppE (n, e, s) -> - sprintf "the result of computing %s(%s with %s)" - (string_of_name n) - (string_of_expr e) - s + sprintf "the result of computing %s(%s with %s)" (string_of_name n) + (string_of_expr e) s | ConcatE (e1, e2) -> - sprintf "the concatenation of the two sequences %s and %s" - (string_of_expr e1) - (string_of_expr e2) + sprintf "the concatenation of the two sequences %s and %s" + (string_of_expr e1) (string_of_expr e2) | LengthE e -> sprintf "the length of %s" (string_of_expr e) | ArityE e -> sprintf "the arity of %s" (string_of_expr e) | FrameE -> "the current frame" | BitWidthE e -> sprintf "the bit width of %s" (string_of_expr e) | PropE (e, s) -> sprintf "%s.%s" (string_of_expr e) s - | IndexAccessE (e1, e2) -> sprintf "%s[%s]" (string_of_expr e1) (string_of_expr e2) + | IndexAccessE (e1, e2) -> + sprintf "%s[%s]" (string_of_expr e1) (string_of_expr e2) | SliceAccessE (e1, e2, e3) -> - sprintf "%s[%s : %s]" (string_of_expr e1) (string_of_expr e2) (string_of_expr e3) + sprintf "%s[%s : %s]" (string_of_expr e1) (string_of_expr e2) + (string_of_expr e3) | ForWhichE c -> sprintf "the constant for which %s" (string_of_cond c) - | RecordE (fl) -> - let string_of_field (n, e) = - sprintf "%s %s" (string_of_name n) (string_of_expr e) in - sprintf "the instance { %s }" - (string_of_list string_of_field "" ", " "" fl) + | RecordE fl -> + let string_of_field (n, e) = + sprintf "%s %s" (string_of_name n) (string_of_expr e) + in + sprintf "the instance { %s }" (string_of_list string_of_field "" ", " "" fl) | PageSizeE -> "the page size" - | AfterCallE -> "the instruction after the original call that pushed the frame" + | AfterCallE -> + "the instruction after the original call that pushed the frame" | ContE e -> sprintf "the continuation of %s" (string_of_expr e) | LabelNthE e -> sprintf "the %s-th label in the stack" (string_of_expr e) | LabelE (e1, e2) -> - sprintf "the label_%s{%s}" (string_of_expr e1) (string_of_expr e2) + sprintf "the label_%s{%s}" (string_of_expr e1) (string_of_expr e2) | NameE n -> string_of_name n | ConstE (n1, n2) -> - sprintf "the value %s.CONST %s" (string_of_name n1) (string_of_expr n2) + sprintf "the value %s.CONST %s" (string_of_name n1) (string_of_expr n2) | RefNullE n -> sprintf "the value ref.null %s" (string_of_name n) | YetE s -> sprintf "YetE (%s)" s @@ -260,97 +323,86 @@ and string_of_cond = function | DefinedC e -> sprintf "%s is defined" (string_of_expr e) | PartOfC [e] -> sprintf "%s is part of the instruction" (string_of_expr e) | PartOfC [e1; e2] -> - sprintf "%s and %s are part of the instruction" - (string_of_expr e1) - (string_of_expr e2) + sprintf "%s and %s are part of the instruction" (string_of_expr e1) + (string_of_expr e2) | PartOfC _ -> failwith "Invalid case" - | TopC s -> sprintf "the top of the stack is %s" s + | TopC s -> sprintf "the top of the stack is %s" s | YetC s -> sprintf "YetC (%s)" s let make_index index depth = index := !index + 1; - if depth = 0 then string_of_int !index ^ "." - else if depth = 1 then Char.escaped (Char.chr (96 + !index)) ^ "." - else if depth = 2 then "i." - else failwith "Invalid case" + if depth = 0 then + string_of_int !index ^ "." + else if depth = 1 then + Char.escaped (Char.chr (96 + !index)) ^ "." + else if depth = 2 then + "i." + else + failwith "Invalid case" let rec string_of_instr index depth = function | IfI (c, il, []) -> - sprintf "%s If %s, then:%s" - (make_index index depth) - (string_of_cond c) - (string_of_instrs (depth + 1) il) + sprintf "%s If %s, then:%s" (make_index index depth) (string_of_cond c) + (string_of_instrs (depth + 1) il) | IfI (c, il1, il2) -> - let if_index = (make_index index depth) in - let else_index = (make_index index depth) in - sprintf "%s If %s, then:%s\n%s Else:%s" - if_index - (string_of_cond c) - (string_of_instrs (depth + 1) il1) - ((repeat indent depth) ^ else_index) - (string_of_instrs (depth + 1) il2) + let if_index = make_index index depth in + let else_index = make_index index depth in + sprintf "%s If %s, then:%s\n%s Else:%s" if_index (string_of_cond c) + (string_of_instrs (depth + 1) il1) + (repeat indent depth ^ else_index) + (string_of_instrs (depth + 1) il2) | WhileI (c, il) -> - sprintf "%s While %s, do:%s" - (make_index index depth) - (string_of_cond c) - (string_of_instrs (depth + 1) il) + sprintf "%s While %s, do:%s" (make_index index depth) (string_of_cond c) + (string_of_instrs (depth + 1) il) | RepeatI (e, il) -> - sprintf "%s Repeat %s times:%s" - (make_index index depth) - (string_of_expr e) - (string_of_instrs (depth + 1) il) + sprintf "%s Repeat %s times:%s" (make_index index depth) (string_of_expr e) + (string_of_instrs (depth + 1) il) | EitherI (il1, il2) -> - let either_index = (make_index index depth) in - let or_index = (make_index index depth) in - sprintf "%s Either:%s\n%s Or:%s" - either_index - (string_of_instrs (depth + 1) il1) - ((repeat indent depth) ^ or_index) - (string_of_instrs (depth + 1) il2) + let either_index = make_index index depth in + let or_index = make_index index depth in + sprintf "%s Either:%s\n%s Or:%s" either_index + (string_of_instrs (depth + 1) il1) + (repeat indent depth ^ or_index) + (string_of_instrs (depth + 1) il2) | AssertI s -> sprintf "%s Assert: %s." (make_index index depth) s | PushI e -> - sprintf "%s Push %s to the stack." (make_index index depth) (string_of_expr e) - | PopI None -> sprintf "%s Pop a value from the stack." (make_index index depth) + sprintf "%s Push %s to the stack." (make_index index depth) + (string_of_expr e) + | PopI None -> + sprintf "%s Pop a value from the stack." (make_index index depth) | PopI (Some e) -> - sprintf "%s Pop %s from the stack." (make_index index depth) (string_of_expr e) + sprintf "%s Pop %s from the stack." (make_index index depth) + (string_of_expr e) | LetI (n, e) -> - sprintf "%s Let %s be %s." - (make_index index depth) - (string_of_expr n) - (string_of_expr e) + sprintf "%s Let %s be %s." (make_index index depth) (string_of_expr n) + (string_of_expr e) | TrapI -> sprintf "%s Trap." (make_index index depth) | NopI -> sprintf "%s Do nothing." (make_index index depth) | ReturnI -> sprintf "%s Return." (make_index index depth) | InvokeI e -> - sprintf "%s Invoke the function instance at address %s." - (make_index index depth) - (string_of_expr e) + sprintf "%s Invoke the function instance at address %s." + (make_index index depth) (string_of_expr e) | EnterI (s, e) -> - sprintf "%s Enter the block %s with label %s." - (make_index index depth) - s - (string_of_expr e) - | ExecuteI (s, []) -> - sprintf "%s Execute (%s)." (make_index index depth) s + sprintf "%s Enter the block %s with label %s." (make_index index depth) s + (string_of_expr e) + | ExecuteI (s, []) -> sprintf "%s Execute (%s)." (make_index index depth) s | ExecuteI (s, el) -> - sprintf "%s Execute (%s %s)." - (make_index index depth) - s - (string_of_list string_of_expr "" " " "" el) + sprintf "%s Execute (%s %s)." (make_index index depth) s + (string_of_list string_of_expr "" " " "" el) | ReplaceI (e1, e2) -> - sprintf "%s Replace %s with %s." - (make_index index depth) - (string_of_expr e1) - (string_of_expr e2) - | JumpI e -> sprintf "%s Jump to %s." (make_index index depth) (string_of_expr e) + sprintf "%s Replace %s with %s." (make_index index depth) + (string_of_expr e1) (string_of_expr e2) + | JumpI e -> + sprintf "%s Jump to %s." (make_index index depth) (string_of_expr e) | YetI s -> sprintf "%s YetI: %s." (make_index index depth) s and string_of_instrs depth instrs = let index = ref 0 in List.fold_left - (fun acc i -> acc ^ "\n" ^ repeat indent depth ^ string_of_instr index depth i) + (fun acc i -> + acc ^ "\n" ^ repeat indent depth ^ string_of_instr index depth i + ) "" instrs let string_of_program = function | Program (name, instrs) -> "" ^ name ^ string_of_instrs 0 instrs ^ "\n" - diff --git a/spectec/src/backend-prose/translate.ml b/spectec/src/backend-prose/translate.ml index 317aae2156..48a100fc88 100644 --- a/spectec/src/backend-prose/translate.ml +++ b/spectec/src/backend-prose/translate.ml @@ -7,35 +7,35 @@ let buf = Buffer.create 4096 (* Helpers *) let _stepIdx = ref 1 + let stepIdx _ = let i = !_stepIdx in - _stepIdx := (i + 1); + _stepIdx := i + 1; i let _subIdx = ref 1 + let subIdx _ = let i = !_subIdx in - _subIdx := (i + 1); + _subIdx := i + 1; i let _indent = ref false + let indent _ = _indent := true; _subIdx := 1 -let unindent _ = - _indent := false + +let unindent _ = _indent := false let printf_step formatted = if !_indent then - Printf.bprintf buf (" %d) " ^^ formatted ^^ "\n") (subIdx()) + Printf.bprintf buf (" %d) " ^^ formatted ^^ "\n") (subIdx ()) else - Printf.bprintf buf ("%d. " ^^ formatted ^^ "\n") (stepIdx()) + Printf.bprintf buf ("%d. " ^^ formatted ^^ "\n") (stepIdx ()) let check_nothing _ = - if - !_indent && !_subIdx = 1 || - not !_indent && !_stepIdx = 1 - then + if (!_indent && !_subIdx = 1) || ((not !_indent) && !_stepIdx = 1) then printf_step "Do nothing." (* 1. Handle lhs of reduction rules *) @@ -45,174 +45,191 @@ let hds l = l |> List.rev |> List.tl let assert_type e = match e.it with (* ({CONST I32 c}) *) - | ParenE({it = SeqE({it = (AtomE (Atom "CONST")); _} :: {it = (AtomE (Atom "I32")); _} :: _); _}, _) -> - printf_step "Assert: Due to validation, a value of value type i32 is on the top of the stack." + | ParenE + ( { it = + SeqE + ({it = AtomE (Atom "CONST"); _} + :: {it = AtomE (Atom "I32"); _} + :: _ + ); + _ + }, + _ + ) -> + printf_step + "Assert: Due to validation, a value of value type i32 is on the top of the stack." | _ -> printf_step "Assert: Due to validation, a value is on the top of the stack." -let pop left = match left.it with - | SeqE(es) -> hds es |> List.iter (fun e -> - assert_type e; - let v = Print.string_of_exp e in - printf_step "Pop the value %s from the stack." v - ) - | ParenE({it = SeqE({it = AtomE(Atom "LABEL_"); _} :: _); _}, _) -> +let pop left = + match left.it with + | SeqE es -> + hds es + |> List.iter (fun e -> + assert_type e; + let v = Print.string_of_exp e in + printf_step "Pop the value %s from the stack." v + ) + | ParenE ({it = SeqE ({it = AtomE (Atom "LABEL_"); _} :: _); _}, _) -> printf_step "YET: Bubble-up semantics." | _ -> () (* 2. Handle premises *) -let calc (prems: premise nl_list) : unit = - prems |> List.iter (fun p -> match p with - | Elem { it = IfPr e; _ } -> printf_step "Let %s." (Print.string_of_exp e) - | _ -> () - ) +let calc (prems : premise nl_list) : unit = + prems + |> List.iter (fun p -> + match p with + | Elem {it = IfPr e; _} -> printf_step "Let %s." (Print.string_of_exp e) + | _ -> () + ) -let cond (prems: premise nl_list) = +let cond (prems : premise nl_list) = prems - |> List.map (fun p -> match p with - | Elem {it = IfPr e; _} -> Print.string_of_exp e - | Elem p -> Print.string_of_prem p - | Nl -> "Nl" - ) + |> List.map (fun p -> + match p with + | Elem {it = IfPr e; _} -> Print.string_of_exp e + | Elem p -> Print.string_of_prem p + | Nl -> "Nl" + ) |> String.concat " and " |> printf_step "If %s, then:" (* 3. Handle rhs of reductino rules *) let _freshId = ref 0 + let fresh _ = let id = !_freshId in - _freshId := (id + 1); + _freshId := id + 1; "tmp" ^ string_of_int id let bind_atomic e = let is_call = match e.it with CallE _ -> true | _ -> false in - let id = fresh() in + let id = fresh () in if is_call then - printf_step "Let %s be the result of computing %s." id (Print.string_of_exp e) + printf_step "Let %s be the result of computing %s." id + (Print.string_of_exp e) else - printf_step "Let %s be %s." id (Print.string_of_exp e) - ; - VarE(id $ e.at) $ e.at - -let rec bind e = match e.it with - | VarE _ - | IterE({it = VarE _; _}, _) - | AtomE _ - | NatE _ -> e - | BinE _ -> ParenE(e, true) $ e.at - | IdxE(base, idx) -> + printf_step "Let %s be %s." id (Print.string_of_exp e); + VarE (id $ e.at) $ e.at + +let rec bind e = + match e.it with + | VarE _ | IterE ({it = VarE _; _}, _) | AtomE _ | NatE _ -> e + | BinE _ -> ParenE (e, true) $ e.at + | IdxE (base, idx) -> let base = bind base in - let idx = bind idx in - bind_atomic (IdxE(base, idx) $ e.at) - | _ -> - bind_atomic e + let idx = bind idx in + bind_atomic (IdxE (base, idx) $ e.at) + | _ -> bind_atomic e let destruct_instr = function - | {it = AtomE(Atom name); _} :: args -> (name, args) - | _ -> raise(Invalid_argument "invalid instr") + | {it = AtomE (Atom name); _} :: args -> (name, args) + | _ -> raise (Invalid_argument "invalid instr") -let mutate state = match state.it with +let mutate state = + match state.it with | CallE _ -> printf_step "Perform %s." (Print.string_of_exp state) | _ -> () -let rec push right = match right.it with - | InfixE(state, Semicolon, stack) -> +let rec push right = + match right.it with + | InfixE (state, Semicolon, stack) -> mutate state; push stack - | SeqE seq -> - List.iter push seq - | AtomE(Atom "TRAP") -> printf_step "Trap." - | ParenE({it = SeqE(instr); _}, _) -> ( - match destruct_instr instr with - | ("LABEL_", n :: cont :: args) -> - printf_step - "Let L be the label whose arity is %s and whose continuation is the %s of this instruction." - (Print.string_of_exp n) - ( - match cont.it with - | BrackE(_, {it = EpsE; _}) -> "end" - | _ -> "start" - ); - printf_step - "Enter the block %s with label L." - (Print.string_of_exps " " args) - | ("FRAME_", n :: frame :: label :: []) -> - printf_step - "Let F be the frame %s." - (Print.string_of_exp frame); - printf_step - "Push the activation of F with the arity %s to the stack." - (Print.string_of_exp n); - push label - | ("CONST" | "REF.NULL" | "REF.FUNC_ADDR" as name, args) -> - let args = List.map bind args in - let str = Print.string_of_exps " " args in - printf_step "Push the value %s %s to the stack." name str - | (name, args) -> - let args = List.map bind args in - let str = Print.string_of_exps " " args in - printf_step "Execute the instruction %s %s." name str + | SeqE seq -> List.iter push seq + | AtomE (Atom "TRAP") -> printf_step "Trap." + | ParenE ({it = SeqE instr; _}, _) -> + ( match destruct_instr instr with + | "LABEL_", n :: cont :: args -> + printf_step + "Let L be the label whose arity is %s and whose continuation is the %s of this instruction." + (Print.string_of_exp n) + (match cont.it with BrackE (_, {it = EpsE; _}) -> "end" | _ -> "start"); + printf_step "Enter the block %s with label L." + (Print.string_of_exps " " args) + | "FRAME_", [n; frame; label] -> + printf_step "Let F be the frame %s." (Print.string_of_exp frame); + printf_step "Push the activation of F with the arity %s to the stack." + (Print.string_of_exp n); + push label + | (("CONST" | "REF.NULL" | "REF.FUNC_ADDR") as name), args -> + let args = List.map bind args in + let str = Print.string_of_exps " " args in + printf_step "Push the value %s %s to the stack." name str + | name, args -> + let args = List.map bind args in + let str = Print.string_of_exps " " args in + printf_step "Execute the instruction %s %s." name str ) - | VarE(id) -> printf_step "Push the value %s to the stack." id.it - | IterE({it = VarE _; _}, _) -> printf_step "Push the values %s to the stack." (Print.string_of_exp right) + | VarE id -> printf_step "Push the value %s to the stack." id.it + | IterE ({it = VarE _; _}, _) -> + printf_step "Push the values %s to the stack." (Print.string_of_exp right) | EpsE -> () | _ -> let e = bind right in - printf_step "Push the value %s to the stack." (Print.string_of_exp e) + printf_step "Push the value %s to the stack." (Print.string_of_exp e) (* if r is a reduction rule, desturct it into triplet of (lhs, rhs, premises) *) -let destruct_as_rule r = match r.it with - | RuleD(name, _, e, prems) -> (match e.it with - | InfixE(left, SqArrow, right) -> +let destruct_as_rule r = + match r.it with + | RuleD (name, _, e, prems) -> + ( match e.it with + | InfixE (left, SqArrow, right) -> if String.starts_with ~prefix:"Step_" name.it then Some (left, right, prems) else None - | _ -> None) + | _ -> None + ) | _ -> None + let string_of_destructed (left, right, prems) = - let filter_nl xs = List.filter_map (function Nl -> None | Elem x -> Some x) xs in + let filter_nl xs = + List.filter_map (function Nl -> None | Elem x -> Some x) xs + in let map_nl_list f xs = List.map f (filter_nl xs) in - Print.string_of_exp left ^ - " ~> " ^ - Print.string_of_exp right ^ - String.concat "" (map_nl_list (fun x -> "\n -- " ^ Print.string_of_prem x) prems) + Print.string_of_exp left + ^ " ~> " + ^ Print.string_of_exp right + ^ String.concat "" + (map_nl_list (fun x -> "\n -- " ^ Print.string_of_prem x) prems) let handle_reduction_group red_group = (* assert: every redunction rule in red_group has same lhs *) - red_group |> List.iter (fun red -> - Buffer.add_string buf (string_of_destructed red); - Buffer.add_char buf '\n' - ); + red_group + |> List.iter (fun red -> + Buffer.add_string buf (string_of_destructed red); + Buffer.add_char buf '\n' + ); _stepIdx := 1; _freshId := 0; - let (left, _, _) = List.hd red_group in - let left = match left.it with - | InfixE(_, Semicolon, left) -> left - | _ -> left + let left, _, _ = List.hd red_group in + let left = + match left.it with InfixE (_, Semicolon, left) -> left | _ -> left in pop left; - ( - match red_group with - (* one rule -> premises are highly likely assignment *) - | [(_, right, prems)] -> - calc prems; - push right; - (* two or more rules -> premises are highly likely conditions *) - | _ -> red_group |> List.iter (fun (_, right, prems) -> - cond prems; - indent(); - push right; - check_nothing(); - unindent(); - ) + ( match red_group with + (* one rule -> premises are highly likely assignment *) + | [(_, right, prems)] -> + calc prems; + push right + (* two or more rules -> premises are highly likely conditions *) + | _ -> + red_group + |> List.iter (fun (_, right, prems) -> + cond prems; + indent (); + push right; + check_nothing (); + unindent () + ) ); - check_nothing(); + check_nothing (); Buffer.add_char buf '\n' @@ -220,18 +237,18 @@ let rec group_by f = function | [] -> [] | [x] -> [[x]] | hd :: tl -> - let pred x = (f hd = f x) in - let (l, r) = List.partition pred tl in - (hd :: l) :: (group_by f r) + let pred x = f hd = f x in + let l, r = List.partition pred tl in + (hd :: l) :: group_by f r let translate el = (* Filter and destruct redctions only *) let reductions = el |> List.filter_map destruct_as_rule in (* Group reductions by lefthand side *) - let reduction_groups = group_by (fun (left, _, _) -> - Print.string_of_exp left - ) reductions in + let reduction_groups = + group_by (fun (left, _, _) -> Print.string_of_exp left) reductions + in (* Handle each redction group *) List.iter handle_reduction_group reduction_groups; diff --git a/spectec/src/dune b/spectec/src/dune index ea13545166..c14e979e7a 100644 --- a/spectec/src/dune +++ b/spectec/src/dune @@ -1,13 +1,11 @@ (library - (name spectec) - (modules) - (libraries - (re_export util) - (re_export el) - (re_export il) - (re_export frontend) - (re_export middlend) - (re_export backend_latex) - (re_export backend_prose) - ) -) + (name spectec) + (modules) + (libraries + (re_export util) + (re_export el) + (re_export il) + (re_export frontend) + (re_export middlend) + (re_export backend_latex) + (re_export backend_prose))) diff --git a/spectec/src/el/ast.ml b/spectec/src/el/ast.ml index e2c082c30a..d73e950252 100644 --- a/spectec/src/el/ast.ml +++ b/spectec/src/el/ast.ml @@ -1,15 +1,10 @@ open Util.Source - (* Lists *) -type 'a nl_elem = - | Nl - | Elem of 'a - +type 'a nl_elem = Nl | Elem of 'a type 'a nl_list = 'a nl_elem list - (* Terminals *) type nat = int @@ -17,76 +12,78 @@ type text = string type id = string phrase type atom = - | Atom of string (* atomid *) - | Bot (* `_|_` *) - | Dot (* `.` *) - | Dot2 (* `..` *) - | Dot3 (* `...` *) - | Semicolon (* `;` *) - | Arrow (* `->` *) - | Colon (* `:` *) - | Sub (* `<:` *) - | SqArrow (* `~>` *) - | Turnstile (* `|-` *) - | Tilesturn (* `-|` *) + | Atom of string (* atomid *) + | Bot (* `_|_` *) + | Dot (* `.` *) + | Dot2 (* `..` *) + | Dot3 (* `...` *) + | Semicolon (* `;` *) + | Arrow (* `->` *) + | Colon (* `:` *) + | Sub (* `<:` *) + | SqArrow (* `~>` *) + | Turnstile (* `|-` *) + | Tilesturn (* `-|` *) type brack = - | Paren (* ``(` ... `)` *) - | Brack (* ``[` ... `]` *) - | Brace (* ``{` ... `}` *) + | Paren (* ``(` ... `)` *) + | Brack (* ``[` ... `]` *) + | Brace (* ``{` ... `}` *) type dots = Dots | NoDots - (* Iteration *) type iter = - | Opt (* `?` *) - | List (* `*` *) - | List1 (* `+` *) - | ListN of exp (* `^` exp *) - + | Opt (* `?` *) + | List (* `*` *) + | List1 (* `+` *) + | ListN of exp (* `^` exp *) (* Types *) - and typ = typ' phrase + and typ' = - | VarT of id (* varid *) - | BoolT (* `bool` *) - | NatT (* `nat` *) - | TextT (* `text` *) - | ParenT of typ (* `(` typ `)` *) - | TupT of typ list (* `(` list2(typ, `,`) `)` *) - | IterT of typ * iter (* typ iter *) + | VarT of id (* varid *) + | BoolT (* `bool` *) + | NatT (* `nat` *) + | TextT (* `text` *) + | ParenT of typ (* `(` typ `)` *) + | TupT of typ list (* `(` list2(typ, `,`) `)` *) + | IterT of typ * iter (* typ iter *) (* The forms below are only allowed in type definitions *) - | StrT of typfield nl_list (* `{` list(typfield,`,`') `}` *) - | CaseT of dots * id nl_list * typcase nl_list * dots (* `|` list(`...`|varid|typcase, `|`) *) - | AtomT of atom (* atom *) - | SeqT of typ list (* `epsilon` / typ typ *) - | InfixT of typ * atom * typ (* typ atom typ *) - | BrackT of brack * typ (* ``` ([{ typ }]) *) - -and typfield = atom * typ * hint list (* atom typ hint* *) -and typcase = atom * typ list * hint list (* atom typ* hint* *) - + | StrT of typfield nl_list (* `{` list(typfield,`,`') `}` *) + | CaseT of + dots + * id nl_list + * typcase nl_list + * dots (* `|` list(`...`|varid|typcase, `|`) *) + | AtomT of atom (* atom *) + | SeqT of typ list (* `epsilon` / typ typ *) + | InfixT of typ * atom * typ (* typ atom typ *) + | BrackT of brack * typ (* ``` ([{ typ }]) *) + +and typfield = atom * typ * hint list (* atom typ hint* *) +and typcase = atom * typ list * hint list (* atom typ* hint* *) (* Expressions *) - and unop = - | NotOp (* `~` *) - | PlusOp (* `+` *) + | NotOp + (* `~` *) + | PlusOp + (* `+` *) | MinusOp (* `-` *) and binop = - | AndOp (* `/\` *) - | OrOp (* `\/` *) + | AndOp (* `/\` *) + | OrOp (* `\/` *) | ImplOp (* `=>` *) | EquivOp (* `<=>` *) - | AddOp (* `+` *) - | SubOp (* `-` *) - | MulOp (* `*` *) - | DivOp (* `/` *) - | ExpOp (* `^` *) + | AddOp (* `+` *) + | SubOp (* `-` *) + | MulOp (* `*` *) + | DivOp (* `/` *) + | ExpOp (* `^` *) and cmpop = | EqOp (* `=` *) @@ -97,66 +94,76 @@ and cmpop = | GeOp (* `>=` *) and exp = exp' phrase -and exp' = - | VarE of id (* varid *) - | AtomE of atom (* atom *) - | BoolE of bool (* bool *) - | NatE of nat (* nat *) - | TextE of text (* text *) - | UnE of unop * exp (* unop exp *) - | BinE of exp * binop * exp (* exp binop exp *) - | CmpE of exp * cmpop * exp (* exp cmpop exp *) - | EpsE (* `epsilon` *) - | SeqE of exp list (* exp exp *) - | IdxE of exp * exp (* exp `[` exp `]` *) - | SliceE of exp * exp * exp (* exp `[` exp `:` exp `]` *) - | UpdE of exp * path * exp (* exp `[` path `=` exp `]` *) - | ExtE of exp * path * exp (* exp `[` path `=..` exp `]` *) - | StrE of expfield nl_list (* `{` list(expfield, `,`) `}` *) - | DotE of exp * atom (* exp `.` atom *) - | CommaE of exp * exp (* exp `,` exp *) - | CompE of exp * exp (* exp `++` exp *) - | LenE of exp (* `|` 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 }]) *) - | CallE of id * exp (* `$` defid exp? *) - | IterE of exp * iter (* exp iter *) - | HoleE of bool (* `%` or `%%` *) - | FuseE of exp * exp (* exp `#` exp *) - -and expfield = atom * exp (* atom exp *) +and exp' = + | VarE of id (* varid *) + | AtomE of atom (* atom *) + | BoolE of bool (* bool *) + | NatE of nat (* nat *) + | TextE of text (* text *) + | UnE of unop * exp (* unop exp *) + | BinE of exp * binop * exp (* exp binop exp *) + | CmpE of exp * cmpop * exp (* exp cmpop exp *) + | EpsE (* `epsilon` *) + | SeqE of exp list (* exp exp *) + | IdxE of exp * exp (* exp `[` exp `]` *) + | SliceE of exp * exp * exp (* exp `[` exp `:` exp `]` *) + | UpdE of exp * path * exp (* exp `[` path `=` exp `]` *) + | ExtE of exp * path * exp (* exp `[` path `=..` exp `]` *) + | StrE of expfield nl_list (* `{` list(expfield, `,`) `}` *) + | DotE of exp * atom (* exp `.` atom *) + | CommaE of exp * exp (* exp `,` exp *) + | CompE of exp * exp (* exp `++` exp *) + | LenE of exp (* `|` 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 }]) *) + | CallE of id * exp (* `$` defid exp? *) + | IterE of exp * iter (* exp iter *) + | HoleE of bool (* `%` or `%%` *) + | FuseE of exp * exp (* exp `#` exp *) + +and expfield = atom * exp (* atom exp *) and path = path' phrase -and path' = - | RootP (* *) - | IdxP of path * exp (* path `[` exp `]` *) - | SliceP of path * exp * exp (* path `[` exp `:` exp `]` *) - | DotP of path * atom (* path `.` atom *) +and path' = + | RootP (* *) + | IdxP of path * exp (* path `[` exp `]` *) + | SliceP of path * exp * exp (* path `[` exp `:` exp `]` *) + | DotP of path * atom (* path `.` atom *) (* Definitions *) - and def = def' phrase + and def' = - | SynD of id * id * typ * hint list (* `syntax` synid hint* `=` typ *) - | RelD of id * typ * hint list (* `relation` relid `:` typ hint* *) - | RuleD of id * id * exp * premise nl_list (* `rule` relid ruleid? `:` exp (`--` premise)* *) - | VarD of id * typ * hint list (* `var` varid `:` typ *) - | DecD of id * exp * typ * hint list (* `def` `$` defid exp? `:` typ hint* *) - | DefD of id * exp * exp * premise nl_list (* `def` `$` defid exp? `=` exp (`--` premise)* *) - | SepD (* separator *) + | SynD of id * id * typ * hint list (* `syntax` synid hint* `=` typ *) + | RelD of id * typ * hint list (* `relation` relid `:` typ hint* *) + | RuleD of + id + * id + * exp + * premise nl_list (* `rule` relid ruleid? `:` exp (`--` premise)* *) + | VarD of id * typ * hint list (* `var` varid `:` typ *) + | DecD of id * exp * typ * hint list (* `def` `$` defid exp? `:` typ hint* *) + | DefD of + id + * exp + * exp + * premise nl_list (* `def` `$` defid exp? `=` exp (`--` premise)* *) + | SepD (* separator *) | HintD of hintdef and premise = premise' phrase + and premise' = - | RulePr of id * exp (* ruleid `:` exp *) - | IfPr of exp (* `if` exp *) - | ElsePr (* `otherwise` *) - | IterPr of premise * iter (* premise iter *) + | RulePr of id * exp (* ruleid `:` exp *) + | IfPr of exp (* `if` exp *) + | ElsePr (* `otherwise` *) + | IterPr of premise * iter (* premise iter *) and hintdef = hintdef' phrase + and hintdef' = | AtomH of id * hint list | SynH of id * id * hint list @@ -164,8 +171,8 @@ and hintdef' = | VarH of id * hint list | DecH of id * hint list -and hint = {hintid : id; hintexp : exp} (* `(` `hint` hintid exp `)` *) - +and hint = {hintid : id; hintexp : exp} +(* `(` `hint` hintid exp `)` *) (* Scripts *) diff --git a/spectec/src/el/dune b/spectec/src/el/dune index 18b957cc91..9f37c39b7f 100644 --- a/spectec/src/el/dune +++ b/spectec/src/el/dune @@ -1,5 +1,4 @@ (library - (name el) - (libraries util) - (modules ast eq free print) -) + (name el) + (libraries util) + (modules ast eq free print)) diff --git a/spectec/src/el/eq.ml b/spectec/src/el/eq.ml index f5cf97f0d0..83e8f15829 100644 --- a/spectec/src/el/eq.ml +++ b/spectec/src/el/eq.ml @@ -1,28 +1,22 @@ open Util.Source open Ast - (* Helpers *) let eq_list eq_x xs1 xs2 = List.length xs1 = List.length xs2 && List.for_all2 eq_x xs1 xs2 let eq_nl_elem eq_x e1 e2 = - match e1, e2 with - | Elem x1, Elem x2 -> eq_x x1 x2 - | _, _ -> false + match (e1, e2) with Elem x1, Elem x2 -> eq_x x1 x2 | _, _ -> false let eq_nl_list eq_x xs1 xs2 = eq_list (eq_nl_elem eq_x) xs1 xs2 - (* Iteration *) let rec eq_iter iter1 iter2 = - iter1 = iter2 || - match iter1, iter2 with - | ListN e1, ListN e2 -> eq_exp e1 e2 - | _, _ -> false - + iter1 = iter2 + || + match (iter1, iter2) with ListN e1, ListN e2 -> eq_exp e1 e2 | _, _ -> false (* Types *) @@ -32,8 +26,9 @@ and eq_typ t1 t2 = (Print.string_of_typ t1) (Print.string_of_typ t2) (t1.it = t2.it); *) - t1.it = t2.it || - match t1.it, t2.it with + t1.it = t2.it + || + match (t1.it, t2.it) with | VarT id1, VarT id2 -> id1.it = id2.it | TupT ts1, TupT ts2 -> eq_list eq_typ ts1 ts2 | IterT (t11, iter1), IterT (t21, iter2) -> @@ -44,15 +39,14 @@ and eq_typ t1 t2 = eq_typ t11 t21 && atom1 = atom2 && eq_typ t12 t22 | BrackT (brack1, t11), BrackT (brack2, t21) -> brack1 = brack2 && eq_typ t11 t21 - | _, _ -> - false - + | _, _ -> false (* Expressions *) and eq_exp e1 e2 = - e1.it = e2.it || - match e1.it, e2.it with + e1.it = e2.it + || + match (e1.it, e2.it) with | VarE id1, VarE id2 -> id1.it = id2.it | UnE (op1, e11), UnE (op2, e21) -> op1 = op2 && eq_exp e11 e21 | BinE (e11, op1, e12), BinE (e21, op2, e22) -> @@ -63,15 +57,15 @@ and eq_exp e1 e2 = | IdxE (e11, e12), IdxE (e21, e22) | CommaE (e11, e12), CommaE (e21, e22) | CompE (e11, e12), CompE (e21, e22) - | FuseE (e11, e12), FuseE (e21, e22) -> eq_exp e11 e21 && eq_exp e12 e22 + | FuseE (e11, e12), FuseE (e21, e22) -> + eq_exp e11 e21 && eq_exp e12 e22 | SliceE (e11, e12, e13), SliceE (e21, e22, e23) -> eq_exp e11 e21 && eq_exp e12 e22 && eq_exp e13 e23 | UpdE (e11, p1, e12), UpdE (e21, p2, e22) | ExtE (e11, p1, e12), ExtE (e21, p2, e22) -> eq_exp e11 e21 && eq_path p1 p2 && eq_exp e12 e22 | ParenE (e11, b1), ParenE (e21, b2) -> eq_exp e11 e21 && b1 = b2 - | SeqE es1, SeqE es2 - | TupE es1, TupE es2 -> eq_list eq_exp es1 es2 + | SeqE es1, SeqE es2 | TupE es1, TupE es2 -> eq_list eq_exp es1 es2 | StrE efs1, StrE efs2 -> eq_nl_list eq_expfield efs1 efs2 | DotE (e11, atom1), DotE (e21, atom2) -> eq_exp e11 e21 && atom1 = atom2 | InfixE (e11, atom1, e12), InfixE (e21, atom2, e22) -> @@ -80,18 +74,15 @@ and eq_exp e1 e2 = | CallE (id1, e1), CallE (id2, e2) -> id1 = id2 && eq_exp e1 e2 | IterE (e11, iter1), IterE (e21, iter2) -> eq_exp e11 e21 && eq_iter iter1 iter2 - | _, _ -> - false + | _, _ -> false -and eq_expfield (atom1, e1) (atom2, e2) = - atom1 = atom2 && eq_exp e1 e2 +and eq_expfield (atom1, e1) (atom2, e2) = atom1 = atom2 && eq_exp e1 e2 and eq_path p1 p2 = - match p1.it, p2.it with + match (p1.it, p2.it) with | RootP, RootP -> true | IdxP (p11, e1), IdxP (p21, e2) -> eq_path p11 p21 && eq_exp e1 e2 | SliceP (p11, e11, e12), SliceP (p21, e21, e22) -> eq_path p11 p21 && eq_exp e11 e21 && eq_exp e12 e22 | DotP (p11, atom1), DotP (p21, atom2) -> eq_path p11 p21 && atom1 = atom2 - | _, _ -> - false + | _, _ -> false diff --git a/spectec/src/el/free.ml b/spectec/src/el/free.ml index 8ca0e1ff15..6a0bd4f621 100644 --- a/spectec/src/el/free.ml +++ b/spectec/src/el/free.ml @@ -1,10 +1,9 @@ open Util.Source open Ast - (* Data Structure *) -module Set = Set.Make(String) +module Set = Set.Make (String) type sets = {synid : Set.t; relid : Set.t; varid : Set.t; defid : Set.t} @@ -15,14 +14,14 @@ let union sets1 sets2 = { synid = Set.union sets1.synid sets2.synid; relid = Set.union sets1.relid sets2.relid; varid = Set.union sets1.varid sets2.varid; - defid = Set.union sets1.defid sets2.defid; + defid = Set.union sets1.defid sets2.defid } let free_list free_x xs = List.(fold_left union empty (map free_x xs)) - let free_nl_elem free_x = function Nl -> empty | Elem x -> free_x x -let free_nl_list free_x xs = List.(fold_left union empty (map (free_nl_elem free_x) xs)) +let free_nl_list free_x xs = + List.(fold_left union empty (map (free_nl_elem free_x) xs)) (* Identifiers *) @@ -31,14 +30,10 @@ let free_relid id = {empty with relid = Set.singleton id.it} let free_varid id = {empty with varid = Set.singleton id.it} let free_defid id = {empty with defid = Set.singleton id.it} - (* Iterations *) let rec free_iter iter = - match iter with - | Opt | List | List1 -> empty - | ListN e -> free_exp e - + match iter with Opt | List | List1 -> empty | ListN e -> free_exp e (* Types *) @@ -60,18 +55,21 @@ and free_typ t = and free_typfield (_, t, _) = free_typ t and free_typcase (_, ts, _) = free_list free_typ ts - (* Expressions *) and free_exp e = match e.it with | VarE id -> free_varid id | AtomE _ | BoolE _ | NatE _ | TextE _ | EpsE | HoleE _ -> empty - | UnE (_, e1) | DotE (e1, _) | LenE e1 - | ParenE (e1, _) | BrackE (_, e1) -> free_exp e1 - | BinE (e1, _, e2) | CmpE (e1, _, e2) - | IdxE (e1, e2) | CommaE (e1, e2) | CompE (e1, e2) - | InfixE (e1, _, e2) | FuseE (e1, e2) -> + | UnE (_, e1) | DotE (e1, _) | LenE e1 | ParenE (e1, _) | BrackE (_, e1) -> + free_exp e1 + | BinE (e1, _, e2) + | CmpE (e1, _, e2) + | IdxE (e1, e2) + | CommaE (e1, e2) + | CompE (e1, e2) + | InfixE (e1, _, e2) + | FuseE (e1, e2) -> free_list free_exp [e1; e2] | SliceE (e1, e2, e3) -> free_list free_exp [e1; e2; e3] | SeqE es | TupE es -> free_list free_exp es @@ -91,7 +89,6 @@ and free_path p = union (free_path p1) (union (free_exp e1) (free_exp e2)) | DotP (p1, _) -> free_path p1 - (* Definitions *) let rec free_prem prem = diff --git a/spectec/src/el/free.mli b/spectec/src/el/free.mli index e95538b604..f16328bbfc 100644 --- a/spectec/src/el/free.mli +++ b/spectec/src/el/free.mli @@ -1,12 +1,10 @@ open Ast - module Set : Set.S with type elt = string type sets = {synid : Set.t; relid : Set.t; varid : Set.t; defid : Set.t} val free_list : ('a -> sets) -> 'a list -> sets val free_nl_list : ('a -> sets) -> 'a nl_list -> sets - val free_iter : iter -> sets val free_typ : typ -> sets val free_exp : exp -> sets diff --git a/spectec/src/el/print.ml b/spectec/src/el/print.ml index 6a4f6683e6..104999267e 100644 --- a/spectec/src/el/print.ml +++ b/spectec/src/el/print.ml @@ -1,18 +1,15 @@ open Util.Source open Ast - (* Helpers *) let concat = String.concat let prefix s f x = s ^ f x let suffix f s x = f x ^ s let space f x = " " ^ f x ^ " " - let filter_nl xs = List.filter_map (function Nl -> None | Elem x -> Some x) xs let map_nl_list f xs = List.map f (filter_nl xs) - (* Operators *) let string_of_atom = function @@ -30,14 +27,11 @@ let string_of_atom = function | Turnstile -> "|-" let string_of_brack = function - | Paren -> "(", ")" - | Brack -> "[", "]" - | Brace -> "{", "}" + | Paren -> ("(", ")") + | Brack -> ("[", "]") + | Brace -> ("{", "}") -let string_of_unop = function - | NotOp -> "~" - | PlusOp -> "+" - | MinusOp -> "-" +let string_of_unop = function NotOp -> "~" | PlusOp -> "+" | MinusOp -> "-" let string_of_binop = function | AndOp -> "/\\" @@ -58,10 +52,7 @@ let string_of_cmpop = function | LeOp -> "<=" | GeOp -> ">=" -let strings_of_dots = function - | Dots -> ["..."] - | NoDots -> [] - +let strings_of_dots = function Dots -> ["..."] | NoDots -> [] (* Iteration *) @@ -72,7 +63,6 @@ let rec string_of_iter iter = | List1 -> "+" | ListN e -> "^" ^ string_of_exp e - (* Types *) and string_of_typ t = @@ -84,12 +74,15 @@ and string_of_typ t = | ParenT t -> "(" ^ string_of_typ t ^ ")" | TupT ts -> "(" ^ string_of_typs ", " ts ^ ")" | IterT (t1, iter) -> string_of_typ t1 ^ string_of_iter iter - | StrT tfs -> - "{" ^ concat ", " (map_nl_list string_of_typfield tfs) ^ "}" + | StrT tfs -> "{" ^ concat ", " (map_nl_list string_of_typfield tfs) ^ "}" | CaseT (dots1, ids, tcases, dots2) -> - "\n | " ^ concat "\n | " - (strings_of_dots dots1 @ map_nl_list it ids @ - map_nl_list string_of_typcase tcases @ strings_of_dots dots2) + "\n | " + ^ concat "\n | " + (strings_of_dots dots1 + @ map_nl_list it ids + @ map_nl_list string_of_typcase tcases + @ strings_of_dots dots2 + ) | AtomT atom -> string_of_atom atom | SeqT ts -> "{" ^ string_of_typs " " ts ^ "}" | InfixT (t1, atom, t2) -> @@ -98,8 +91,7 @@ and string_of_typ t = let l, r = string_of_brack brack in "`" ^ l ^ string_of_typ t1 ^ r -and string_of_typs sep ts = - concat sep (List.map string_of_typ ts) +and string_of_typs sep ts = concat sep (List.map string_of_typ ts) and string_of_typfield (atom, t, _hints) = string_of_atom atom ^ " " ^ string_of_typ t @@ -110,7 +102,6 @@ and string_of_typcase (atom, ts, _hints) = else string_of_atom atom ^ " " ^ string_of_typs " " ts - (* Expressions *) and string_of_exp e = @@ -129,14 +120,11 @@ and string_of_exp e = | SeqE es -> "{" ^ string_of_exps " " es ^ "}" | IdxE (e1, e2) -> string_of_exp e1 ^ "[" ^ string_of_exp e2 ^ "]" | SliceE (e1, e2, e3) -> - string_of_exp e1 ^ - "[" ^ string_of_exp e2 ^ " : " ^ string_of_exp e3 ^ "]" + string_of_exp e1 ^ "[" ^ string_of_exp e2 ^ " : " ^ string_of_exp e3 ^ "]" | UpdE (e1, p, e2) -> - string_of_exp e1 ^ - "[" ^ string_of_path p ^ " = " ^ string_of_exp e2 ^ "]" + string_of_exp e1 ^ "[" ^ string_of_path p ^ " = " ^ string_of_exp e2 ^ "]" | ExtE (e1, p, e2) -> - string_of_exp e1 ^ - "[" ^ string_of_path p ^ " =.. " ^ string_of_exp e2 ^ "]" + string_of_exp e1 ^ "[" ^ string_of_path p ^ " =.. " ^ string_of_exp e2 ^ "]" | StrE efs -> "{" ^ concat ", " (map_nl_list string_of_expfield efs) ^ "}" | DotE (e1, atom) -> string_of_exp e1 ^ "." ^ string_of_atom atom | CommaE (e1, e2) -> string_of_exp e1 ^ ", " ^ string_of_exp e2 @@ -156,11 +144,8 @@ and string_of_exp e = | HoleE true -> "%%" | FuseE (e1, e2) -> string_of_exp e1 ^ "#" ^ string_of_exp e2 -and string_of_exps sep es = - concat sep (List.map string_of_exp es) - -and string_of_expfield (atom, e) = - string_of_atom atom ^ " " ^ string_of_exp e +and string_of_exps sep es = concat sep (List.map string_of_exp es) +and string_of_expfield (atom, e) = string_of_atom atom ^ " " ^ string_of_exp e and string_of_path p = match p.it with @@ -171,7 +156,6 @@ and string_of_path p = | DotP ({it = RootP; _}, atom) -> string_of_atom atom | DotP (p1, atom) -> string_of_path p1 ^ "." ^ string_of_atom atom - (* Definitions *) let rec string_of_prem prem = @@ -179,38 +163,40 @@ let rec string_of_prem prem = | RulePr (id, e) -> id.it ^ ": " ^ string_of_exp e | IfPr e -> "if " ^ string_of_exp e | ElsePr -> "otherwise" - | IterPr ({it = IterPr _; _} as prem', iter) -> + | IterPr (({it = IterPr _; _} as prem'), iter) -> string_of_prem prem' ^ string_of_iter iter | IterPr (prem', iter) -> "(" ^ string_of_prem prem' ^ ")" ^ string_of_iter iter - let string_of_def d = match d.it with | SynD (id1, id2, t, _hints) -> let id2' = if id2.it = "" then "" else "/" ^ id2.it in "syntax " ^ id1.it ^ id2' ^ " = " ^ string_of_typ t - | RelD (id, t, _hints) -> - "relation " ^ id.it ^ ": " ^ string_of_typ t + | RelD (id, t, _hints) -> "relation " ^ id.it ^ ": " ^ string_of_typ t | RuleD (id1, id2, e, prems) -> let id2' = if id2.it = "" then "" else "/" ^ id2.it in - "rule " ^ id1.it ^ id2' ^ ":\n " ^ string_of_exp e ^ - concat "" (map_nl_list (prefix "\n -- " string_of_prem) prems) - | VarD (id, t, _hints) -> - "var " ^ id.it ^ " : " ^ string_of_typ t + "rule " + ^ id1.it + ^ id2' + ^ ":\n " + ^ string_of_exp e + ^ concat "" (map_nl_list (prefix "\n -- " string_of_prem) prems) + | VarD (id, t, _hints) -> "var " ^ id.it ^ " : " ^ string_of_typ t | DecD (id, e1, t2, _hints) -> let s1 = match e1.it with SeqE [] -> "" | _ -> " " ^ string_of_exp e1 in "def " ^ id.it ^ s1 ^ " : " ^ string_of_typ t2 | DefD (id, e1, e2, prems) -> let s1 = match e1.it with SeqE [] -> "" | _ -> " " ^ string_of_exp e1 in - "def " ^ id.it ^ s1 ^ " = " ^ string_of_exp e2 ^ - concat "" (map_nl_list (prefix "\n -- " string_of_prem) prems) - | SepD -> - "\n\n" + "def " + ^ id.it + ^ s1 + ^ " = " + ^ string_of_exp e2 + ^ concat "" (map_nl_list (prefix "\n -- " string_of_prem) prems) + | SepD -> "\n\n" | HintD _ -> "" - (* Scripts *) -let string_of_script ds = - concat "" (List.map (suffix string_of_def "\n") ds) +let string_of_script ds = concat "" (List.map (suffix string_of_def "\n") ds) diff --git a/spectec/src/exe-watsup/dune b/spectec/src/exe-watsup/dune index a9da47797c..908d868ed6 100644 --- a/spectec/src/exe-watsup/dune +++ b/spectec/src/exe-watsup/dune @@ -1,4 +1,3 @@ (executable - (name main) - (libraries spectec) -) + (name main) + (libraries spectec)) diff --git a/spectec/src/exe-watsup/main.ml b/spectec/src/exe-watsup/main.ml index cb6c5bdea7..4f76b25b2f 100644 --- a/spectec/src/exe-watsup/main.ml +++ b/spectec/src/exe-watsup/main.ml @@ -1,79 +1,70 @@ open Util - (* Configuration *) let name = "watsup" let version = "0.3" - (* Flags and parameters *) -type target = - | Check - | Latex of Backend_latex.Config.config - | Prose +type target = Check | Latex of Backend_latex.Config.config | Prose let target = ref (Latex Backend_latex.Config.latex) - -let log = ref false (* log execution steps *) -let dst = ref false (* patch files *) -let dry = ref false (* dry run for patching *) +let log = ref false (* log execution steps *) +let dst = ref false (* patch files *) +let dry = ref false (* dry run for patching *) let warn = ref false (* warn about unused or reused splices *) - -let srcs = ref [] (* src file arguments *) -let dsts = ref [] (* destination file arguments *) -let odst = ref "" (* generation file argument *) - +let srcs = ref [] (* src file arguments *) +let dsts = ref [] (* destination file arguments *) +let odst = ref "" (* generation file argument *) let print_elab_il = ref false let print_final_il = ref false let print_all_il = ref false - let pass_sub = ref false let pass_totalize = ref false let pass_unthe = ref false let pass_sideconditions = ref false - (* Argument parsing *) -let banner () = - print_endline (name ^ " " ^ version ^ " generator") - +let banner () = print_endline (name ^ " " ^ version ^ " generator") let usage = "Usage: " ^ name ^ " [option] [file ...] [-p file ...]" let add_arg source = - let args = if !dst then dsts else srcs in args := !args @ [source] - -let argspec = Arg.align -[ - "-v", Arg.Unit banner, " Show version"; - "-o", Arg.String (fun s -> odst := s), " Generate file"; - "-p", Arg.Set dst, " Patch files"; - "-d", Arg.Set dry, " Dry run (when -p) "; - "-l", Arg.Set log, " Log execution steps"; - "-w", Arg.Set warn, " Warn about unused or multiply used splices"; - - "--check", Arg.Unit (fun () -> target := Check), " Check only"; - "--latex", Arg.Unit (fun () -> target := Latex Backend_latex.Config.latex), - " Generate Latex (default)"; - "--sphinx", Arg.Unit (fun () -> target := Latex Backend_latex.Config.sphinx), - " Generate Latex for Sphinx"; - "--prose", Arg.Unit (fun () -> target := Prose), " Generate prose"; - - "--print-il", Arg.Set print_elab_il, " Print il (after elaboration)"; - "--print-final-il", Arg.Set print_final_il, " Print final il"; - "--print-all-il", Arg.Set print_all_il, " Print il after each step"; - - "--sub", Arg.Set pass_sub, " Synthesize explicit subtype coercions"; - "--totalize", Arg.Set pass_totalize, " Run function totalization"; - "--the-elimination", Arg.Set pass_unthe, " Eliminate the ! operator in relations"; - "--sideconditions", Arg.Set pass_sideconditions, " Infer side conditions"; - - "-help", Arg.Unit ignore, ""; - "--help", Arg.Unit ignore, ""; -] - + let args = if !dst then dsts else srcs in + args := !args @ [source] + +let argspec = + Arg.align + [ ("-v", Arg.Unit banner, " Show version"); + ("-o", Arg.String (fun s -> odst := s), " Generate file"); + ("-p", Arg.Set dst, " Patch files"); + ("-d", Arg.Set dry, " Dry run (when -p) "); + ("-l", Arg.Set log, " Log execution steps"); + ("-w", Arg.Set warn, " Warn about unused or multiply used splices"); + ("--check", Arg.Unit (fun () -> target := Check), " Check only"); + ( "--latex", + Arg.Unit (fun () -> target := Latex Backend_latex.Config.latex), + " Generate Latex (default)" + ); + ( "--sphinx", + Arg.Unit (fun () -> target := Latex Backend_latex.Config.sphinx), + " Generate Latex for Sphinx" + ); + ("--prose", Arg.Unit (fun () -> target := Prose), " Generate prose"); + ("--print-il", Arg.Set print_elab_il, " Print il (after elaboration)"); + ("--print-final-il", Arg.Set print_final_il, " Print final il"); + ("--print-all-il", Arg.Set print_all_il, " Print il after each step"); + ("--sub", Arg.Set pass_sub, " Synthesize explicit subtype coercions"); + ("--totalize", Arg.Set pass_totalize, " Run function totalization"); + ( "--the-elimination", + Arg.Set pass_unthe, + " Eliminate the ! operator in relations" + ); + ("--sideconditions", Arg.Set pass_sideconditions, " Infer side conditions"); + ("-help", Arg.Unit ignore, ""); + ("--help", Arg.Unit ignore, "") + ] (* Main *) @@ -92,18 +83,25 @@ let () = log "IL Validation..."; Il.Validation.valid il; - let il = if not !pass_sub then il else - ( log "Subtype injection..."; + let il = + if not !pass_sub then + il + else ( + log "Subtype injection..."; let il = Middlend.Sub.transform il in - if !print_all_il then Printf.printf "%s\n%!" (Il.Print.string_of_script il); + if !print_all_il then + Printf.printf "%s\n%!" (Il.Print.string_of_script il); log "IL Validation..."; Il.Validation.valid il; il ) in - let il = if not !pass_totalize then il else - ( log "Function totalization..."; + let il = + if not !pass_totalize then + il + else ( + log "Function totalization..."; let il = Middlend.Totalize.transform il in if !print_all_il then Printf.printf "%s\n%!" (Il.Print.string_of_script il); @@ -113,8 +111,11 @@ let () = ) in - let il = if not !pass_unthe then il else - ( log "Option projection eliminiation"; + let il = + if not !pass_unthe then + il + else ( + log "Option projection eliminiation"; let il = Middlend.Unthe.transform il in if !print_all_il then Printf.printf "%s\n%!" (Il.Print.string_of_script il); @@ -124,8 +125,11 @@ let () = ) in - let il = if not !pass_sideconditions then il else - ( log "Side condition inference"; + let il = + if not !pass_sideconditions then + il + else ( + log "Side condition inference"; let il = Middlend.Sideconditions.transform il in if !print_all_il then Printf.printf "%s\n%!" (Il.Print.string_of_script il); @@ -138,19 +142,18 @@ let () = if !print_final_il && not !print_all_il then Printf.printf "%s\n%!" (Il.Print.string_of_script il); - (match !target with + ( match !target with | Check -> () | Latex config -> log "Latex Generation..."; if !odst = "" && !dsts = [] then print_endline (Backend_latex.Gen.gen_string el); - if !odst <> "" then - Backend_latex.Gen.gen_file !odst el; + if !odst <> "" then Backend_latex.Gen.gen_file !odst el; if !dsts <> [] then ( let env = Backend_latex.Splice.(env config el) in List.iter (Backend_latex.Splice.splice_file ~dry:!dry env) !dsts; - if !warn then Backend_latex.Splice.warn env; - ); + if !warn then Backend_latex.Splice.warn env + ) | Prose -> log "Prose Generation..."; let ir = true in @@ -158,10 +161,9 @@ let () = let program = Backend_prose.Il2ir.translate il in List.map Backend_prose.Print.string_of_program program |> List.iter print_endline - else ( + else let prose = Backend_prose.Translate.translate el in print_endline prose - ) ); log "Complete." with diff --git a/spectec/src/frontend/dune b/spectec/src/frontend/dune index d006656b98..d12f8e0dde 100644 --- a/spectec/src/frontend/dune +++ b/spectec/src/frontend/dune @@ -1,13 +1,10 @@ (library - (name frontend) - (libraries util el il) - (modules lexer parser parse multiplicity elab) -) + (name frontend) + (libraries util el il) + (modules lexer parser parse multiplicity elab)) (ocamllex - (modules lexer) -) + (modules lexer)) (menhir - (modules parser) -) + (modules parser)) diff --git a/spectec/src/frontend/elab.ml b/spectec/src/frontend/elab.ml index 22f268d3d6..60593c1da6 100644 --- a/spectec/src/frontend/elab.ml +++ b/spectec/src/frontend/elab.ml @@ -4,31 +4,37 @@ open El open Ast open Print -module Il = struct include Il include Ast end +module Il = struct + include Il + include Ast +end module Set = Free.Set -module Map = Map.Make(String) +module Map = Map.Make (String) let filter_nl xs = List.filter_map (function Nl -> None | Elem x -> Some x) xs let map_nl_list f xs = List.map f (filter_nl xs) - (* Errors *) let error at msg = Source.error at "type" msg - -let error_atom at atom msg = - error at (msg ^ " `" ^ string_of_atom atom ^ "`") - -let error_id id msg = - error id.at (msg ^ " `" ^ id.it ^ "`") +let error_atom at atom msg = error at (msg ^ " `" ^ string_of_atom atom ^ "`") +let error_id id msg = error id.at (msg ^ " `" ^ id.it ^ "`") let error_typ at phrase t = error at (phrase ^ " does not match expected type `" ^ string_of_typ t ^ "`") let error_typ2 at phrase t1 t2 reason = - error at (phrase ^ "'s type `" ^ string_of_typ t1 ^ "`" ^ - " does not match expected type `" ^ string_of_typ t2 ^ "`" ^ reason) + error at + (phrase + ^ "'s type `" + ^ string_of_typ t1 + ^ "`" + ^ " does not match expected type `" + ^ string_of_typ t2 + ^ "`" + ^ reason + ) type direction = Infer | Check @@ -36,48 +42,35 @@ let error_dir_typ at phrase dir t expected = match dir with | Check -> error_typ at phrase t | Infer -> - error at (phrase ^ "'s type `" ^ string_of_typ t ^ "`" ^ - " does not match expected type " ^ expected) - + error at + (phrase + ^ "'s type `" + ^ string_of_typ t + ^ "`" + ^ " does not match expected type " + ^ expected + ) (* Helpers *) -let unparen_exp e = - match e.it with - | ParenE (e1, _) -> e1 - | _ -> e - -let unseq_exp e = - match e.it with - | EpsE -> [] - | SeqE es -> es - | _ -> [e] - -let tup_typ' ts' at = - match ts' with - | [t'] -> t' - | _ -> Il.TupT ts' $ at +let unparen_exp e = match e.it with ParenE (e1, _) -> e1 | _ -> e +let unseq_exp e = match e.it with EpsE -> [] | SeqE es -> es | _ -> [e] +let tup_typ' ts' at = match ts' with [t'] -> t' | _ -> Il.TupT ts' $ at let tup_exp' es' at = match es' with | [e'] -> e' | _ -> Il.TupE es' $$ (at, Il.TupT (List.map note es') $ at) -let lift_exp' e' iter' = - if iter' = Opt then - Il.OptE (Some e') - else - Il.ListE [e'] +let lift_exp' e' iter' = if iter' = Opt then Il.OptE (Some e') else Il.ListE [e'] let cat_exp' e1' e2' = - match e1'.it, e2'.it with + match (e1'.it, e2'.it) with | _, Il.ListE [] -> e1'.it | Il.ListE [], _ -> e2'.it | Il.ListE es1, Il.ListE es2 -> Il.ListE (es1 @ es2) | _ -> Il.CatE (e1', e2') - - (* Environment *) type fwd_typ = Bad | Ok @@ -90,17 +83,18 @@ type env = { mutable vars : var_typ Map.t; mutable typs : syn_typ Map.t; mutable rels : rel_typ Map.t; - mutable defs : def_typ Map.t; + mutable defs : def_typ Map.t } let new_env () = - { vars = Map.empty + { vars = + Map.empty |> Map.add "bool" (BoolT $ no_region) |> Map.add "nat" (NatT $ no_region) |> Map.add "text" (TextT $ no_region); typs = Map.empty; rels = Map.empty; - defs = Map.empty; + defs = Map.empty } let bound env' id = Map.mem id.it env' @@ -130,27 +124,25 @@ let find_case cases atom at = | Some (_, x, _) -> x | None -> error_atom at atom "unknown case" - let rec prefix_id id = prefix_id' id.it $ id.at + and prefix_id' id = - match String.index_opt id '_', String.index_opt id '\'' with + match (String.index_opt id '_', String.index_opt id '\'') with | None, None -> id | None, Some n | Some n, None -> String.sub id 0 n | Some n1, Some n2 -> String.sub id 0 (min n1 n2) - (* Type Accessors *) let as_defined_typid' env id at : typ' * [`Alias | `NoAlias] = match find "syntax type" env.typs id with - | Either.Right (t, {it = Il.AliasT _t'; _}) -> t.it, `Alias - | Either.Right (t, _deftyp') -> t.it, `NoAlias - | Either.Left _ -> - error_id (id.it $ at) "invalid forward use of syntax type" + | Either.Right (t, {it = Il.AliasT _t'; _}) -> (t.it, `Alias) + | Either.Right (t, _deftyp') -> (t.it, `NoAlias) + | Either.Left _ -> error_id (id.it $ at) "invalid forward use of syntax type" let rec expand' env = function | VarT id as t' -> - (match as_defined_typid' env id id.at with + ( match as_defined_typid' env id id.at with | t1, `Alias -> expand' env t1 | _ -> t' ) @@ -164,10 +156,9 @@ let expand_singular' env t' = | IterT (t1, (Opt | List | List1)) -> expand env t1 | t' -> t' - let as_iter_typ phrase env dir t at : typ * iter = match expand' env t.it with - | IterT (t1, iter) -> t1, iter + | IterT (t1, iter) -> (t1, iter) | _ -> error_dir_typ at phrase dir t "(_)*" let as_list_typ phrase env dir t at : typ = @@ -180,10 +171,9 @@ let as_tup_typ phrase env dir t at : typ list = | TupT ts -> ts | _ -> error_dir_typ at phrase dir t "(_,...,_)" - let as_notation_typid' phrase env id at : typ = match as_defined_typid' env id at with - | (AtomT _ | SeqT _ | InfixT _ | BrackT _) as t, _ -> t $ at + | ((AtomT _ | SeqT _ | InfixT _ | BrackT _) as t), _ -> t $ at | _ -> error_dir_typ at phrase Infer (VarT id $ id.at) "_ ... _" let as_notation_typ phrase env dir t at : typ = @@ -205,7 +195,7 @@ let rec as_variant_typid' phrase env id at : typcase list * dots = match as_defined_typid' env id at with | CaseT (_dots1, ids, cases, dots2), _ -> let casess = map_nl_list (as_variant_typid "" env) ids in - List.concat (filter_nl cases :: List.map fst casess), dots2 + (List.concat (filter_nl cases :: List.map fst casess), dots2) | _ -> error_dir_typ id.at phrase Infer (VarT id $ id.at) "| ..." and as_variant_typid phrase env id : typcase list * dots = @@ -220,16 +210,16 @@ let case_has_args env t atom at : bool = let cases, _ = as_variant_typ "" env Check t at in find_case cases atom at <> [] - let is_x_typ as_x_typ env t = - try ignore (as_x_typ "" env Check t no_region); true + try + ignore (as_x_typ "" env Check t no_region); + true with Error _ -> false let is_iter_typ = is_x_typ as_iter_typ let is_notation_typ = is_x_typ as_notation_typ let is_variant_typ = is_x_typ as_variant_typ - (* Type Equivalence *) let equiv_list equiv_x xs1 xs2 = @@ -241,15 +231,15 @@ let rec equiv_typ env t1 t2 = (Print.string_of_typ t1) (Print.string_of_typ t2) (t1.it = t2.it); *) - t1.it = t2.it || - match expand env t1, expand env t2 with + t1.it = t2.it + || + match (expand env t1, expand env t2) with | VarT id1, VarT id2 -> id1.it = id2.it | TupT ts1, TupT ts2 -> equiv_list (equiv_typ env) ts1 ts2 | IterT (t11, iter1), IterT (t21, iter2) -> equiv_typ env t11 t21 && Eq.eq_iter iter1 iter2 | t1', t2' -> Eq.eq_typ (t1' $ t1.at) (t2' $ t2.at) - (* Hints *) let elab_hint {hintid; hintexp} : Il.hint = @@ -262,7 +252,6 @@ let elab_hint {hintid; hintexp} : Il.hint = let elab_hints = List.map elab_hint - (* Atoms and Operators *) let elab_atom = function @@ -280,9 +269,9 @@ let elab_atom = function | Tilesturn -> Il.Tilesturn let elab_brack = function - | Paren -> Il.LParen, Il.RParen - | Brack -> Il.LBrack, Il.RBrack - | Brace -> Il.LBrace, Il.RBrace + | Paren -> (Il.LParen, Il.RParen) + | Brack -> (Il.LBrack, Il.RBrack) + | Brace -> (Il.LBrace, Il.RBrace) let elab_unop = function | NotOp -> Il.NotOp @@ -309,25 +298,31 @@ let elab_cmpop = function | GeOp -> Il.GeOp let merge_mixop mixop1 mixop2 = - match mixop1, mixop2 with + match (mixop1, mixop2) with | _, [] -> mixop1 | [], _ -> mixop2 - | mixop1, atoms2::mixop2' -> + | mixop1, atoms2 :: mixop2' -> let mixop1', atoms1 = Lib.List.split_last mixop1 in mixop1' @ [atoms1 @ atoms2] @ mixop2' - let check_atoms phrase item list at = let _, dups = - List.fold_right (fun (atom, _, _) (set, dups) -> - let s = Print.string_of_atom atom in - if Set.mem s set then (set, s::dups) else (Set.add s set, dups) - ) list (Set.empty, []) + List.fold_right + (fun (atom, _, _) (set, dups) -> + let s = Print.string_of_atom atom in + if Set.mem s set then (set, s :: dups) else (Set.add s set, dups) + ) + list (Set.empty, []) in if dups <> [] then - error at (phrase ^ " contains duplicate " ^ item ^ "(s) `" ^ - String.concat "`, `" dups ^ "`") - + error at + (phrase + ^ " contains duplicate " + ^ item + ^ "(s) `" + ^ String.concat "`, `" dups + ^ "`" + ) (* Iteration *) @@ -338,13 +333,12 @@ let rec elab_iter env iter : Il.iter = | List1 -> Il.List1 | ListN e -> Il.ListN (elab_exp env e (NatT $ e.at)) - (* Types *) and elab_typ env t : Il.typ = match t.it with | VarT id -> - (match find "syntax type" env.typs id with + ( match find "syntax type" env.typs id with | Either.Left Bad -> error_id id "invalid forward reference to syntax type" | _ -> Il.VarT id $ t.at ) @@ -354,33 +348,37 @@ and elab_typ env t : Il.typ = | ParenT t1 -> elab_typ env t1 | TupT ts -> Il.TupT (List.map (elab_typ env) ts) $ t.at | IterT (t1, iter) -> - (match iter with + ( match iter with | List1 | ListN _ -> error t.at "illegal iterator in syntax type" | _ -> Il.IterT (elab_typ env t1, elab_iter env iter) $ t.at ) | StrT _ | CaseT _ | AtomT _ | SeqT _ | InfixT _ | BrackT _ -> - failwith(*error t.at*) "this type is only allowed in type definitions" + failwith (*error t.at*) "this type is only allowed in type definitions" and elab_typ_definition env id t : Il.deftyp = - (match t.it with + ( match t.it with | StrT tfs -> let tfs' = filter_nl tfs in check_atoms "record" "field" tfs' t.at; Il.StructT (map_nl_list (elab_typfield env) tfs) | CaseT (dots1, ids, cases, _dots2) -> let cases0 = - if dots1 = Dots then fst (as_variant_typid "own type" env id) else [] in + if dots1 = Dots then fst (as_variant_typid "own type" env id) else [] + in let casess = map_nl_list (as_variant_typid "parent type" env) ids in let cases' = - List.flatten (cases0 :: List.map fst casess @ [filter_nl cases]) in + List.flatten ((cases0 :: List.map fst casess) @ [filter_nl cases]) + in let tcs' = List.map (elab_typcase env t.at) cases' in check_atoms "variant" "case" cases' t.at; Il.VariantT tcs' | _ -> - match elab_typ_notation env t with + ( match elab_typ_notation env t with | false, _mixop, ts' -> Il.AliasT (tup_typ' ts' t.at) | true, mixop, ts' -> Il.NotationT (mixop, tup_typ' ts' t.at) - ) $ t.at + ) + ) + $ t.at and elab_typ_notation env t : bool * Il.mixop * Il.typ list = (* @@ -388,38 +386,37 @@ and elab_typ_notation env t : bool * Il.mixop * Il.typ list = (string_of_region t.at) (string_of_typ t); *) match t.it with - | AtomT atom -> - true, [[elab_atom atom]], [] - | SeqT [] -> - true, [[]], [] - | SeqT (t1::ts2) -> + | AtomT atom -> (true, [[elab_atom atom]], []) + | SeqT [] -> (true, [[]], []) + | SeqT (t1 :: ts2) -> let _b1, mixop1, ts1' = elab_typ_notation env t1 in let _b2, mixop2, ts2' = elab_typ_notation env (SeqT ts2 $ t.at) in - true, merge_mixop mixop1 mixop2, ts1' @ ts2' + (true, merge_mixop mixop1 mixop2, ts1' @ ts2') | InfixT (t1, atom, t2) -> let _b1, mixop1, ts1' = elab_typ_notation env t1 in let _b2, mixop2, ts2' = elab_typ_notation env t2 in - true, merge_mixop (merge_mixop mixop1 [[elab_atom atom]]) mixop2, ts1' @ ts2' + ( true, + merge_mixop (merge_mixop mixop1 [[elab_atom atom]]) mixop2, + ts1' @ ts2' + ) | BrackT (brack, t1) -> let l, r = elab_brack brack in let _b1, mixop1, ts' = elab_typ_notation env t1 in - true, merge_mixop (merge_mixop [[l]] mixop1) [[r]], ts' + (true, merge_mixop (merge_mixop [[l]] mixop1) [[r]], ts') | ParenT t1 -> let b1, mixop1, ts1' = elab_typ_notation env t1 in - b1, merge_mixop (merge_mixop [[Il.LParen]] mixop1) [[Il.RParen]], ts1' + (b1, merge_mixop (merge_mixop [[Il.LParen]] mixop1) [[Il.RParen]], ts1') | IterT (t1, iter) -> - (match iter with + ( match iter with | List1 | ListN _ -> error t.at "illegal iterator in notation type" | _ -> let b1, mixop1, ts' = elab_typ_notation env t1 in let iter' = elab_iter env iter in let t' = Il.IterT (tup_typ' ts' t1.at, iter') $ t.at in let op = match iter with Opt -> Il.Quest | _ -> Il.Star in - b1, [List.flatten mixop1] @ [[op]], [t'] + (b1, [List.flatten mixop1] @ [[op]], [t']) ) - | _ -> - false, [[]; []], [elab_typ env t] - + | _ -> (false, [[]; []], [elab_typ env t]) and elab_typfield env (atom, t, hints) : Il.typfield = let _, _, ts' = elab_typ_notation env t in @@ -427,19 +424,19 @@ and elab_typfield env (atom, t, hints) : Il.typfield = and elab_typcase env at (atom, ts, hints) : Il.typcase = let tss' = - List.map (fun (_, _, ts) -> ts) (List.map (elab_typ_notation env) ts) in + List.map (fun (_, _, ts) -> ts) (List.map (elab_typ_notation env) ts) + in (elab_atom atom, tup_typ' (List.concat tss') at, elab_hints hints) +and ( !! ) env t = elab_typ env t -and (!!) env t = elab_typ env t -and (!!!) env t = let _, _, ts' = elab_typ_notation env t in tup_typ' ts' t.at - +and ( !!! ) env t = + let _, _, ts' = elab_typ_notation env t in + tup_typ' ts' t.at (* Expressions *) -and infer_unop = function - | NotOp -> BoolT - | PlusOp | MinusOp -> NatT +and infer_unop = function NotOp -> BoolT | PlusOp | MinusOp -> NatT and infer_binop = function | AndOp | OrOp | ImplOp | EquivOp -> BoolT @@ -465,7 +462,8 @@ and infer_exp env e : typ = | UpdE (e1, _, _) | ExtE (e1, _, _) | CommaE (e1, _) - | CompE (e1, _) -> infer_exp env e1 + | CompE (e1, _) -> + infer_exp env e1 | StrE _ -> error e.at "cannot infer type of record" | DotE (e1, atom) -> let t1 = infer_exp env e1 in @@ -475,7 +473,9 @@ and infer_exp env e : typ = | SeqE _ -> error e.at "cannot infer type of expression sequence" | TupE es -> TupT (List.map (infer_exp env) es) $ e.at | ParenE (e1, _) -> ParenT (infer_exp env e1) $ e.at - | CallE (id, _) -> let _, t2, _ = find "function" env.defs id in t2 + | CallE (id, _) -> + let _, t2, _ = find "function" env.defs id in + t2 | InfixE _ -> error e.at "cannot infer type of infix expression" | BrackE _ -> error e.at "cannot infer type of bracket expression" | IterE (e1, iter) -> @@ -484,7 +484,6 @@ and infer_exp env e : typ = | HoleE _ -> error e.at "misplaced hole" | FuseE _ -> error e.at "misplaced token concatenation" - and elab_exp env e t : Il.exp = (* Printf.printf "[elab %s] %s : %s\n%!" @@ -527,8 +526,9 @@ and elab_exp env e t : Il.exp = | CmpE (e21, _, _) -> let e21' = elab_exp env e21 t1' in let e2' = elab_exp env e2 (BoolT $ e2.at) in - Il.BinE (Il.AndOp, - Il.CmpE (elab_cmpop op, e1', e21') $$ e1.at % !!env t' , e2') $$ e.at % !!env t' + Il.BinE + (Il.AndOp, Il.CmpE (elab_cmpop op, e1', e21') $$ e1.at % !!env t', e2') + $$ e.at % !!env t' | _ -> let e2' = elab_exp env e2 t1' in Il.CmpE (elab_cmpop op, e1', e2') $$ e.at % !!env t' @@ -573,7 +573,7 @@ and elab_exp env e t : Il.exp = let e1' = elab_exp env e1 t in let tfs = as_struct_typ "expression" env Check t e1.at in (* TODO: this is a bit of a hack *) - (match e2.it with + ( match e2.it with | SeqE ({it = AtomE atom; at; _} :: es2) -> let _t2 = find_field tfs atom at in let e2 = match es2 with [e2] -> e2 | _ -> SeqE es2 $ e2.at in @@ -597,8 +597,7 @@ and elab_exp env e t : Il.exp = let t1, _iter = as_iter_typ "expression" env Check t e.at in let e1' = elab_exp env e1 t1 in cast_exp "expression" env e1' t1 t - | ParenE (e1, _) -> - elab_exp env e1 t + | ParenE (e1, _) -> elab_exp env e1 t | TupE es -> let ts = as_tup_typ "tuple" env Check t e.at in let es' = elab_exps env es ts e.at in @@ -608,16 +607,12 @@ and elab_exp env e t : Il.exp = let e2' = elab_exp env e2 t2 in let e' = Il.CallE (id, e2') $$ e.at % !!env t' in cast_exp "expression" env e' t' t - | SeqE [_] -> assert false (* sequences cannot be singleton *) - | EpsE | SeqE _ when is_iter_typ env t -> + | SeqE [_] -> assert false (* sequences cannot be singleton *) + | (EpsE | SeqE _) when is_iter_typ env t -> let e1 = unseq_exp e in elab_exp_iter env e1 (as_iter_typ "" env Check t e.at) t e.at - | EpsE -> - error_typ e.at "empty expression" t - | AtomE _ - | InfixE _ - | BrackE _ - | SeqE _ -> + | EpsE -> error_typ e.at "empty expression" t + | AtomE _ | InfixE _ | BrackE _ | SeqE _ -> (* All these expression forms can only be used when checking against * either a defined notation/variant type or (for SeqE) an iteration type; * the latter case is already captured above *) @@ -625,15 +620,15 @@ and elab_exp env e t : Il.exp = elab_exp_notation env e (as_notation_typ "" env Check t e.at) t else if is_variant_typ env t then elab_exp_variant env (unseq_exp e) - (fst (as_variant_typ "" env Check t e.at)) t e.at + (fst (as_variant_typ "" env Check t e.at)) + t e.at else error_typ e.at "expression" t | IterE (e1, iter2) -> (* An iteration expression must match the expected type directly, * significant parentheses have to be used otherwise *) let t1, iter = as_iter_typ "iteration" env Check t e.at in - if (iter = Opt) <> (iter2 = Opt) then - error_typ e.at "iteration expression" t; + if iter = Opt <> (iter2 = Opt) then error_typ e.at "iteration expression" t; let e1' = elab_exp env e1 t1 in let iter2' = elab_iterexp env iter2 in Il.IterE (e1', iter2') $$ e.at % !!env t @@ -646,20 +641,20 @@ and elab_exps env es ts at : Il.exp list = List.map2 (elab_exp env) es ts and elab_expfields env efs tfs at : Il.expfield list = - match efs, tfs with + match (efs, tfs) with | [], [] -> [] - | (atom1, e)::efs2, (atom2, t, _)::tfs2 when atom1 = atom2 -> + | (atom1, e) :: efs2, (atom2, t, _) :: tfs2 when atom1 = atom2 -> let es' = elab_exp_notation' env e t in let efs2' = elab_expfields env efs2 tfs2 at in (elab_atom atom1, tup_exp' es' e.at) :: efs2' - | _, (atom, t, _)::tfs2 -> + | _, (atom, t, _) :: tfs2 -> let atom' = string_of_atom atom in let e' = - cast_empty ("omitted record field `" ^ atom' ^ "`") env t at (!!env t) in + cast_empty ("omitted record field `" ^ atom' ^ "`") env t at (!!env t) + in let efs2' = elab_expfields env efs tfs2 at in (elab_atom atom, e') :: efs2' - | (atom, e)::_, [] -> - error_atom e.at atom "unexpected record field" + | (atom, e) :: _, [] -> error_atom e.at atom "unexpected record field" and elab_exp_iter env es (t1, iter) t at : Il.exp = (* @@ -668,28 +663,23 @@ and elab_exp_iter env es (t1, iter) t at : Il.exp = (String.concat " " (List.map string_of_exp es)) (string_of_typ t) (string_of_typ t1) (string_of_iter iter); *) - match es, iter with + match (es, iter) with (* If the sequence actually starts with a non-nullary constructor, * then assume this is a singleton iteration and fallback to variant *) - | {it = AtomE atom; at = at1; _}::_, _ when is_variant_typ env t1 && - case_has_args env t1 atom at1 -> + | {it = AtomE atom; at = at1; _} :: _, _ + when is_variant_typ env t1 && case_has_args env t1 atom at1 -> let cases, _dots = as_variant_typ "" env Check t1 at in lift_exp' (elab_exp_variant env es cases t1 at) iter $$ at % !!env t - (* An empty sequence represents the None case for options *) - | [], Opt -> - Il.OptE None $$ at % !!env t + | [], Opt -> Il.OptE None $$ at % !!env t (* An empty sequence represents the Nil case for lists *) - | [], List -> - Il.ListE [] $$ at % !!env t + | [], List -> Il.ListE [] $$ at % !!env t (* All other elements are either splices or (by cast injection) elements *) - | e1::es2, List -> + | e1 :: es2, List -> let e1' = elab_exp env e1 t in let e2' = elab_exp_iter env es2 (t1, iter) t at in cat_exp' e1' e2' $$ at % !!env t - - | _, _ -> - error_typ at "expression" t + | _, _ -> error_typ at "expression" t and elab_exp_notation env e nt t : Il.exp = (* @@ -707,7 +697,7 @@ and elab_exp_notation' env e t : Il.exp list = Printf.printf "[notation %s] %s : %s\n%!" (string_of_region e.at) (string_of_exp e) (string_of_typ t); *) - match e.it, t.it with + match (e.it, t.it) with | AtomE atom, AtomT atom' -> if atom <> atom' then error_typ e.at "atom" t; [] @@ -719,51 +709,45 @@ and elab_exp_notation' env e t : Il.exp list = | BrackE (brack, e1), BrackT (brack', t1) -> if brack <> brack' then error_typ e.at "bracket expression" t; elab_exp_notation' env e1 t1 - - | SeqE [], SeqT [] -> - [] + | SeqE [], SeqT [] -> [] (* Iterations at the end of a sequence may be inlined *) - | _, SeqT [{it = IterT _; _} as t1] -> - elab_exp_notation' env e t1 + | _, SeqT [({it = IterT _; _} as t1)] -> elab_exp_notation' env e t1 (* Optional iterations may always be inlined, use backtracking *) - | SeqE (e1::es2), SeqT (({it = IterT (_, Opt); _} as t1)::ts2) -> - (try - let es1' = [cast_empty "omitted sequence tail" env t1 e.at (!!!env t1)] in - let es2' = elab_exp_notation' env e (SeqT ts2 $ t.at) in - es1' @ es2' - with Source.Error _ -> - (* + | SeqE (e1 :: es2), SeqT (({it = IterT (_, Opt); _} as t1) :: ts2) -> + ( try + let es1' = + [cast_empty "omitted sequence tail" env t1 e.at (!!!env t1)] + in + let es2' = elab_exp_notation' env e (SeqT ts2 $ t.at) in + es1' @ es2' + with Source.Error _ -> + (* Printf.printf "[backtrack %s] %s : %s\n%!" (string_of_region e.at) (string_of_exp e) (string_of_typ t); *) - let es1' = elab_exp_notation' env e1 t1 in - let es2' = elab_exp_notation' env (SeqE es2 $ e.at) (SeqT ts2 $ t.at) in - es1' @ es2' + let es1' = elab_exp_notation' env e1 t1 in + let es2' = elab_exp_notation' env (SeqE es2 $ e.at) (SeqT ts2 $ t.at) in + es1' @ es2' ) - | SeqE (e1::es2), SeqT (t1::ts2) -> + | SeqE (e1 :: es2), SeqT (t1 :: ts2) -> let es1' = elab_exp_notation' env (unparen_exp e1) t1 in let es2' = elab_exp_notation' env (SeqE es2 $ e.at) (SeqT ts2 $ t.at) in es1' @ es2' (* Trailing elements can be omitted if they can be epsilon *) - | SeqE [], SeqT (t1::ts2) -> + | SeqE [], SeqT (t1 :: ts2) -> let e1' = cast_empty "omitted sequence tail" env t1 e.at (!!!env t1) in - let es2' = - elab_exp_notation' env (SeqE [] $ e.at) (SeqT ts2 $ t.at) in + let es2' = elab_exp_notation' env (SeqE [] $ e.at) (SeqT ts2 $ t.at) in [e1'] @ es2' - | SeqE (e1::_), SeqT [] -> + | SeqE (e1 :: _), SeqT [] -> error e1.at "superfluous expression does not match expected empty notation type" (* Since trailing elements can be omitted, a singleton may match a sequence *) - | _, SeqT _ -> - elab_exp_notation' env (SeqE [e] $ e.at) t - - | SeqE [e1], IterT _ -> - [elab_exp env e1 t] + | _, SeqT _ -> elab_exp_notation' env (SeqE [e] $ e.at) t + | SeqE [e1], IterT _ -> [elab_exp env e1 t] | (EpsE | SeqE _), IterT (t1, iter) -> [elab_exp_notation_iter env (unseq_exp e) (t1, iter) t e.at] | IterE (e1, iter1), IterT (t1, iter) -> - if (iter = Opt) <> (iter1 = Opt) then - error_typ e.at "iteration expression" t; + if iter = Opt <> (iter1 = Opt) then error_typ e.at "iteration expression" t; let es1' = elab_exp_notation' env e1 t1 in let iter1' = elab_iter env iter1 in [Il.IterE (tup_exp' es1' e1.at, (iter1', [])) $$ e.at % !!!env t] @@ -779,14 +763,9 @@ and elab_exp_notation' env e t : Il.exp list = | _, IterT (t1, iter) -> let es' = elab_exp_notation' env e t1 in [lift_exp' (tup_exp' es' e.at) iter $$ e.at % !!!env t] - - | ParenE (e1, _), _ -> - elab_exp_notation' env e1 t - | _, ParenT t1 -> - elab_exp_notation' env e t1 - - | _, _ -> - [elab_exp env e t] + | ParenE (e1, _), _ -> elab_exp_notation' env e1 t + | _, ParenT t1 -> elab_exp_notation' env e t1 + | _, _ -> [elab_exp env e t] and elab_exp_notation_iter env es (t1, iter) t at : Il.exp = (* @@ -795,29 +774,24 @@ and elab_exp_notation_iter env es (t1, iter) t at : Il.exp = (String.concat " " (List.map string_of_exp es)) (string_of_typ t); *) - match es, iter with + match (es, iter) with (* If the sequence actually starts with a non-nullary constructor, * then assume this is a singleton iteration and fallback to variant *) - | {it = AtomE atom; at = at1; _}::_, iter when is_variant_typ env t1 && - case_has_args env t1 atom at1 -> + | {it = AtomE atom; at = at1; _} :: _, iter + when is_variant_typ env t1 && case_has_args env t1 atom at1 -> let cases, _ = as_variant_typ "expression" env Check t1 at in lift_exp' (elab_exp_variant env es cases t1 at) iter $$ at % !!!env t - (* An empty sequence represents the None case for options *) - | [], Opt -> - Il.OptE None $$ at % !!!env t + | [], Opt -> Il.OptE None $$ at % !!!env t (* An empty sequence represents the Nil case for lists *) - | [], List -> - Il.ListE [] $$ at % !!!env t + | [], List -> Il.ListE [] $$ at % !!!env t (* All other elements are either splices or (by cast injection) elements; * nested expressions must be lifted into a tuple *) - | e1::es2, List -> + | e1 :: es2, List -> let es1' = elab_exp_notation' env e1 t in let e2' = elab_exp_notation_iter env es2 (t1, iter) t at in cat_exp' (tup_exp' es1' e1.at) e2' $$ at % !!!env t - - | _, _ -> - error_typ at "expression" t + | _, _ -> error_typ at "expression" t and elab_exp_variant env es cases t at : Il.exp = (* @@ -835,39 +809,36 @@ and elab_exp_variant env es cases t at : Il.exp = *) *) match es with - | {it = AtomE atom; _}::es -> + | {it = AtomE atom; _} :: es -> let ts = find_case cases atom at in (* TODO: this is a bit hacky *) let e2 = SeqE es $ at in let es' = elab_exp_notation' env e2 (SeqT ts $ t.at) in let t2 = expand_singular' env t.it $ at in cast_exp "variant case" env - (Il.CaseE (elab_atom atom, tup_exp' es' at) $$ at % !!env t2) t2 t - | _ -> - error_typ at "expression" t - + (Il.CaseE (elab_atom atom, tup_exp' es' at) $$ at % !!env t2) + t2 t + | _ -> error_typ at "expression" t and elab_path env p t : Il.path * typ = match p.it with - | RootP -> - Il.RootP $$ p.at % !!env t, t + | RootP -> (Il.RootP $$ p.at % !!env t, t) | IdxP (p1, e1) -> let p1', t1 = elab_path env p1 t in let e1' = elab_exp env e1 (NatT $ e1.at) in let t' = as_list_typ "path" env Check t1 p1.at in - Il.IdxP (p1', e1') $$ p.at % !!env t', t' + (Il.IdxP (p1', e1') $$ p.at % !!env t', t') | SliceP (p1, e1, e2) -> let p1', t1 = elab_path env p1 t in let e1' = elab_exp env e1 (NatT $ e1.at) in let e2' = elab_exp env e2 (NatT $ e2.at) in let _ = as_list_typ "path" env Check t1 p1.at in - Il.SliceP (p1', e1', e2') $$ p.at % !!env t1, t1 + (Il.SliceP (p1', e1', e2') $$ p.at % !!env t1, t1) | DotP (p1, atom) -> let p1', t1 = elab_path env p1 t in let tfs = as_struct_typ "path" env Check t1 p1.at in let t' = find_field tfs atom p1.at in - Il.DotP (p1', elab_atom atom) $$ p.at % !!env t', t' - + (Il.DotP (p1', elab_atom atom) $$ p.at % !!env t', t') and cast_empty phrase env t at t' : Il.exp = match expand env t with @@ -884,51 +855,55 @@ and cast_exp phrase env e' t1 t2 : Il.exp = (string_of_typ (expand env t2 $ t2.at)) (equiv_typ env t1 t2); *) - if equiv_typ env t1 t2 then e' else - match expand env t2 with - | IterT (t21, Opt) -> - Il.OptE (Some (cast_exp_variant phrase env e' t1 t21)) $$ e'.at % !!env t2 - | IterT (t21, (List | List1)) -> - Il.ListE [cast_exp_variant phrase env e' t1 t21] $$ e'.at % !!env t2 - | _ -> - cast_exp_variant phrase env e' t1 t2 + if equiv_typ env t1 t2 then + e' + else + match expand env t2 with + | IterT (t21, Opt) -> + Il.OptE (Some (cast_exp_variant phrase env e' t1 t21)) $$ e'.at % !!env t2 + | IterT (t21, (List | List1)) -> + Il.ListE [cast_exp_variant phrase env e' t1 t21] $$ e'.at % !!env t2 + | _ -> cast_exp_variant phrase env e' t1 t2 and cast_exp_variant phrase env e' t1 t2 : Il.exp = - if equiv_typ env t1 t2 then e' else - if is_variant_typ env t1 && is_variant_typ env t2 then + if equiv_typ env t1 t2 then + e' + else if is_variant_typ env t1 && is_variant_typ env t2 then ( let cases1, dots1 = as_variant_typ "" env Check t1 e'.at in let cases2, _dots2 = as_variant_typ "" env Check t2 e'.at in if dots1 = Dots then error e'.at "used variant type is only partially defined at this point"; - (try - List.iter (fun (atom, ts1, _) -> - let ts2 = find_case cases2 atom t1.at in - (* Shallow subtyping on variants *) - if List.length ts1 <> List.length ts2 - || not (List.for_all2 Eq.eq_typ ts1 ts2) then - error_atom e'.at atom "type mismatch for case" - ) cases1 - with Error (_, msg) -> error_typ2 e'.at phrase t1 t2 (", " ^ msg) + ( try + List.iter + (fun (atom, ts1, _) -> + let ts2 = find_case cases2 atom t1.at in + (* Shallow subtyping on variants *) + if + List.length ts1 <> List.length ts2 + || not (List.for_all2 Eq.eq_typ ts1 ts2) + then + error_atom e'.at atom "type mismatch for case" + ) + cases1 + with Error (_, msg) -> error_typ2 e'.at phrase t1 t2 (", " ^ msg) ); Il.SubE (e', elab_typ env t1, elab_typ env t2) $$ e'.at % !!env t2 - else + ) else error_typ2 e'.at phrase t1 t2 "" - -and elab_iterexp env iter = - (elab_iter env iter, []) - +and elab_iterexp env iter = (elab_iter env iter, []) (* Definitions *) let make_binds env free dims at : Il.binds = - List.map (fun id' -> - let id = id' $ at in - let t = elab_typ env (find "variable" env.vars (prefix_id id)) in - let ctx = List.map (elab_iter env) (Multiplicity.Env.find id.it dims) in - (id, t, ctx) - ) (Set.elements free) - + List.map + (fun id' -> + let id = id' $ at in + let t = elab_typ env (find "variable" env.vars (prefix_id id)) in + let ctx = List.map (elab_iter env) (Multiplicity.Env.find id.it dims) in + (id, t, ctx) + ) + (Set.elements free) let rec elab_prem env prem : Il.premise = match prem.it with @@ -940,62 +915,62 @@ let rec elab_prem env prem : Il.premise = | IfPr e -> let e' = elab_exp env e (BoolT $ e.at) in Il.IfPr e' $ prem.at - | ElsePr -> - Il.ElsePr $ prem.at + | ElsePr -> Il.ElsePr $ prem.at | IterPr (prem1, iter) -> let prem1' = elab_prem env prem1 in let iter' = elab_iterexp env iter in Il.IterPr (prem1', iter') $ prem.at - let infer_typ_definition _env t : syn_typ = - match t.it with - | StrT _ | CaseT _ -> Either.Left Ok - | _ -> Either.Left Bad + match t.it with StrT _ | CaseT _ -> Either.Left Ok | _ -> Either.Left Bad let infer_def env d = match d.it with | SynD (id1, _id2, t, _hints) -> if not (bound env.typs id1) then ( env.typs <- bind "syntax type" env.typs id1 (infer_typ_definition env t); - env.vars <- bind "variable" env.vars id1 (VarT id1 $ id1.at); + env.vars <- bind "variable" env.vars id1 (VarT id1 $ id1.at) ) | _ -> () let elab_hintdef _env hd : Il.def list = match hd.it with | SynH (id1, _id2, hints) -> - if hints = [] then [] else - [Il.HintD (Il.SynH (id1, elab_hints hints) $ hd.at) $ hd.at] + if hints = [] then + [] + else + [Il.HintD (Il.SynH (id1, elab_hints hints) $ hd.at) $ hd.at] | RelH (id, hints) -> - if hints = [] then [] else - [Il.HintD (Il.RelH (id, elab_hints hints) $ hd.at) $ hd.at] + if hints = [] then + [] + else + [Il.HintD (Il.RelH (id, elab_hints hints) $ hd.at) $ hd.at] | DecH (id, hints) -> - if hints = [] then [] else - [Il.HintD (Il.DecH (id, elab_hints hints) $ hd.at) $ hd.at] - | AtomH _ | VarH _ -> - [] + if hints = [] then + [] + else + [Il.HintD (Il.DecH (id, elab_hints hints) $ hd.at) $ hd.at] + | AtomH _ | VarH _ -> [] let elab_def env d : Il.def list = match d.it with | SynD (id1, id2, t, hints) -> let dt' = elab_typ_definition env id1 t in let t1, closed = - match find "syntax type" env.typs id1, t.it with + match (find "syntax type" env.typs id1, t.it) with | Either.Left _, CaseT (Dots, _, _, _) -> error_id id1 "extension of not yet defined syntax type" - | Either.Left _, CaseT (NoDots, _, _, dots2) -> - t, dots2 = NoDots - | Either.Left _, _ -> - t, true - | Either.Right ({it = CaseT (dots1, ids1, tcs1, Dots); at; _}, _), - CaseT (Dots, ids2, tcs2, dots2) -> - CaseT (dots1, ids1 @ ids2, tcs1 @ tcs2, dots2) $ over_region [at; t.at], + | Either.Left _, CaseT (NoDots, _, _, dots2) -> (t, dots2 = NoDots) + | Either.Left _, _ -> (t, true) + | ( Either.Right ({it = CaseT (dots1, ids1, tcs1, Dots); at; _}, _), + CaseT (Dots, ids2, tcs2, dots2) ) -> + ( CaseT (dots1, ids1 @ ids2, tcs1 @ tcs2, dots2) $ over_region [at; t.at], dots2 = NoDots + ) | Either.Right _, CaseT (Dots, _, _, _) -> error_id id1 "extension of non-extensible syntax type" | Either.Right _, _ -> - error_id id1 "duplicate declaration for syntax type"; + error_id id1 "duplicate declaration for syntax type" in (* Printf.printf "[def %s] %s ~> %s\n%!" id1.it @@ -1003,24 +978,31 @@ let elab_def env d : Il.def list = *) env.typs <- rebind "syntax type" env.typs id1 (Either.Right (t1, dt')); (if not closed then [] else [Il.SynD (id1, dt') $ d.at]) - @ elab_hintdef env (SynH (id1, id2, hints) $ d.at) + @ elab_hintdef env (SynH (id1, id2, hints) $ d.at) | RelD (id, t, hints) -> let _, mixop, ts' = elab_typ_notation env t in env.rels <- bind "relation" env.rels id (t, []); [Il.RelD (id, mixop, tup_typ' ts' t.at, []) $ d.at] - @ elab_hintdef env (RelH (id, hints) $ d.at) + @ elab_hintdef env (RelH (id, hints) $ d.at) | RuleD (id1, id2, e, prems) -> let dims = Multiplicity.check_def d in let dims' = Multiplicity.Env.map (List.map (elab_iter env)) dims in let t, rules' = find "relation" env.rels id1 in let _, mixop, _ = elab_typ_notation env t in - let es' = List.map (Multiplicity.annot_exp dims') (elab_exp_notation' env e t) in - let prems' = List.map (Multiplicity.annot_prem dims') - (map_nl_list (elab_prem env) prems) in + let es' = + List.map (Multiplicity.annot_exp dims') (elab_exp_notation' env e t) + in + let prems' = + List.map + (Multiplicity.annot_prem dims') + (map_nl_list (elab_prem env) prems) + in let free = (Free.free_def d).Free.varid in let binds' = make_binds env free dims d.at in - let rule' = Il.RuleD (id2, binds', mixop, tup_exp' es' e.at, prems') $ d.at in - env.rels <- rebind "relation" env.rels id1 (t, rule'::rules'); + let rule' = + Il.RuleD (id2, binds', mixop, tup_exp' es' e.at, prems') $ d.at + in + env.rels <- rebind "relation" env.rels id1 (t, rule' :: rules'); [] | VarD (id, t, _hints) -> let _t' = elab_typ env t in @@ -1033,30 +1015,34 @@ let elab_def env d : Il.def list = let t2' = elab_typ env t2 in env.defs <- bind "function" env.defs id (t1, t2, []); [Il.DecD (id, t1', t2', []) $ d.at] - @ elab_hintdef env (DecH (id, hints) $ d.at) + @ elab_hintdef env (DecH (id, hints) $ d.at) | DefD (id, e1, e2, prems) -> let dims = Multiplicity.check_def d in let dims' = Multiplicity.Env.map (List.map (elab_iter env)) dims in let t1, t2, clauses' = find "function" env.defs id in let e1' = Multiplicity.annot_exp dims' (elab_exp env e1 t1) in let e2' = Multiplicity.annot_exp dims' (elab_exp env e2 t2) in - let prems' = List.map (Multiplicity.annot_prem dims') - (map_nl_list (elab_prem env) prems) in + let prems' = + List.map + (Multiplicity.annot_prem dims') + (map_nl_list (elab_prem env) prems) + in let free_rh = Free.(Set.diff (free_exp e2).varid (free_exp e1).varid) in if free_rh <> Free.Set.empty then - error d.at ("definition contains unbound variable(s) `" ^ - String.concat "`, `" (Free.Set.elements free_rh) ^ "`"); - let free = Free.(Set.union - (free_exp e1).varid (free_nl_list free_prem prems).varid) in + error d.at + ("definition contains unbound variable(s) `" + ^ String.concat "`, `" (Free.Set.elements free_rh) + ^ "`" + ); + let free = + Free.(Set.union (free_exp e1).varid (free_nl_list free_prem prems).varid) + in let binds' = make_binds env free dims d.at in let clause' = Il.DefD (binds', e1', e2', prems') $ d.at in - env.defs <- rebind "definition" env.defs id (t1, t2, clause'::clauses'); - [] - | SepD -> + env.defs <- rebind "definition" env.defs id (t1, t2, clause' :: clauses'); [] - | HintD hd -> - elab_hintdef env hd - + | SepD -> [] + | HintD hd -> elab_hintdef env hd let populate_def env d' : Il.def = match d'.it with @@ -1067,9 +1053,7 @@ let populate_def env d' : Il.def = | Il.DecD (id, t1', t2', []) -> let _, _, clauses' = find "function" env.defs id in Il.DecD (id, t1', t2', List.rev clauses') $ d'.at - | _ -> - assert false - + | _ -> assert false (* Scripts *) @@ -1077,25 +1061,34 @@ let origins i (map : int Map.t ref) (set : Il.Free.Set.t) = Il.Free.Set.iter (fun id -> map := Map.add id i !map) set let deps (map : int Map.t) (set : Il.Free.Set.t) : int array = - Array.map (fun id -> -try - Map.find id map -with Not_found as e -> Printf.printf "[%s]\n%!" id; raise e - ) (Array.of_seq (Il.Free.Set.to_seq set)) - + Array.map + (fun id -> + try Map.find id map + with Not_found as e -> + Printf.printf "[%s]\n%!" id; + raise e + ) + (Array.of_seq (Il.Free.Set.to_seq set)) let check_recursion ds' = - List.iter (fun d' -> - match d'.it, (List.hd ds').it with - | Il.HintD _, _ | _, Il.HintD _ - | Il.SynD _, Il.SynD _ - | Il.RelD _, Il.RelD _ - | Il.DecD _, Il.DecD _ -> () - | _, _ -> - error (List.hd ds').at (" " ^ string_of_region d'.at ^ - ": invalid recursion between definitions of different sort") - ) ds' - (* TODO: check that notations are non-recursive and defs are inductive? *) + List.iter + (fun d' -> + match (d'.it, (List.hd ds').it) with + | Il.HintD _, _ + | _, Il.HintD _ + | Il.SynD _, Il.SynD _ + | Il.RelD _, Il.RelD _ + | Il.DecD _, Il.DecD _ -> + () + | _, _ -> + error (List.hd ds').at + (" " + ^ string_of_region d'.at + ^ ": invalid recursion between definitions of different sort" + ) + ) + ds' +(* TODO: check that notations are non-recursive and defs are inductive? *) let recursify_defs ds' : Il.def list = let open Il.Free in @@ -1105,29 +1098,35 @@ let recursify_defs ds' : Il.def list = let map_defid = ref Map.empty in let frees = Array.map Il.Free.free_def da in let bounds = Array.map Il.Free.bound_def da in - Array.iteri (fun i bound -> - origins i map_synid bound.synid; - origins i map_relid bound.relid; - origins i map_defid bound.defid; - ) bounds; + Array.iteri + (fun i bound -> + origins i map_synid bound.synid; + origins i map_relid bound.relid; + origins i map_defid bound.defid + ) + bounds; let graph = - Array.map (fun free -> - Array.concat - [ deps !map_synid free.synid; - deps !map_relid free.relid; - deps !map_defid free.defid; - ]; - ) frees + Array.map + (fun free -> + Array.concat + [ deps !map_synid free.synid; + deps !map_relid free.relid; + deps !map_defid free.defid + ] + ) + frees in let sccs = Scc.sccs graph in - List.map (fun set -> - let ds'' = List.map (fun i -> da.(i)) (Scc.Set.elements set) in - check_recursion ds''; - let i = Scc.Set.choose set in - match ds'' with - | [d'] when Il.Free.disjoint bounds.(i) frees.(i) -> d' - | ds'' -> Il.RecD ds'' $ Source.over_region (List.map at ds'') - ) sccs + List.map + (fun set -> + let ds'' = List.map (fun i -> da.(i)) (Scc.Set.elements set) in + check_recursion ds''; + let i = Scc.Set.choose set in + match ds'' with + | [d'] when Il.Free.disjoint bounds.(i) frees.(i) -> d' + | ds'' -> Il.RecD ds'' $ Source.over_region (List.map at ds'') + ) + sccs let elab ds : Il.script = let env = new_env () in diff --git a/spectec/src/frontend/lexer.mli b/spectec/src/frontend/lexer.mli index e54a8234df..e06dbb3dcc 100644 --- a/spectec/src/frontend/lexer.mli +++ b/spectec/src/frontend/lexer.mli @@ -1,2 +1,2 @@ val region : Lexing.lexbuf -> Util.Source.region -val token : Lexing.lexbuf -> Parser.token (* raises Source.Error *) +val token : Lexing.lexbuf -> Parser.token (* raises Source.Error *) diff --git a/spectec/src/frontend/multiplicity.ml b/spectec/src/frontend/multiplicity.ml index ac879463b3..517e4178ee 100644 --- a/spectec/src/frontend/multiplicity.ml +++ b/spectec/src/frontend/multiplicity.ml @@ -3,20 +3,17 @@ open Source open El open Ast - (* Errors *) let error at msg = Source.error at "multiplicity" msg - (* Environment *) -module Env = Map.Make(String) +module Env = Map.Make (String) type ctx = iter list type env = ctx Env.t -type renv = ((region * ctx) list) Env.t - +type renv = (region * ctx) list Env.t (* Solving constraints *) @@ -24,68 +21,64 @@ let string_of_ctx id ctx = id ^ String.concat "" (List.map Print.string_of_iter ctx) let rec is_prefix ctx1 ctx2 = - match ctx1, ctx2 with + match (ctx1, ctx2) with | [], _ -> true | _, [] -> false - | iter1::ctx1', iter2::ctx2' -> + | iter1 :: ctx1', iter2 :: ctx2' -> Eq.eq_iter iter1 iter2 && is_prefix ctx1' ctx2' - let rec check_ctx id (at0, ctx0) = function | [] -> () - | (at, ctx)::ctxs -> + | (at, ctx) :: ctxs -> if not (is_prefix ctx0 ctx) then - error at ("inconsistent variable context, " ^ - string_of_ctx id ctx0 ^ " vs " ^ string_of_ctx id ctx ^ - " (" ^ string_of_region at0 ^ ")"); + error at + ("inconsistent variable context, " + ^ string_of_ctx id ctx0 + ^ " vs " + ^ string_of_ctx id ctx + ^ " (" + ^ string_of_region at0 + ^ ")" + ); check_ctx id (at0, ctx0) ctxs - let check_ctxs id ctxs : ctx = - let sorted = List.stable_sort - (fun (_, ctx1) (_, ctx2) -> compare (List.length ctx1) (List.length ctx2)) - ctxs + let sorted = + List.stable_sort + (fun (_, ctx1) (_, ctx2) -> compare (List.length ctx1) (List.length ctx2)) + ctxs in check_ctx id (List.hd sorted) (List.tl sorted); snd (List.hd sorted) -let check_env (env : renv ref) : env = - Env.mapi check_ctxs !env - +let check_env (env : renv ref) : env = Env.mapi check_ctxs !env (* Collecting constraints *) let check_id env ctx id = let ctxs = match Env.find_opt id.it !env with - | None -> [id.at, ctx] - | Some ctxs -> (id.at, ctx)::ctxs - in env := Env.add id.it ctxs !env - + | None -> [(id.at, ctx)] + | Some ctxs -> (id.at, ctx) :: ctxs + in + env := Env.add id.it ctxs !env let iter_nl_list f xs = List.iter (function Nl -> () | Elem x -> f x) xs let rec check_iter env ctx iter = - match iter with - | Opt | List | List1 -> () - | ListN e -> check_exp env ctx e + match iter with Opt | List | List1 -> () | ListN e -> check_exp env ctx e and check_exp env ctx e = match e.it with | VarE id -> check_id env ctx id - | AtomE _ - | BoolE _ - | NatE _ - | TextE _ - | EpsE - | HoleE _ - | FuseE _ -> () + | AtomE _ | BoolE _ | NatE _ | TextE _ | EpsE | HoleE _ | FuseE _ -> () | UnE (_, e1) | DotE (e1, _) | LenE e1 | ParenE (e1, _) | BrackE (_, e1) - | CallE (_, e1) -> check_exp env ctx e1 + | CallE (_, e1) -> + check_exp env ctx e1 | BinE (e1, _, e2) | CmpE (e1, _, e2) | IdxE (e1, e2) @@ -98,17 +91,15 @@ and check_exp env ctx e = check_exp env ctx e1; check_exp env ctx e2; check_exp env ctx e3 - | UpdE (e1, p, e2) - | ExtE (e1, p, e2) -> + | UpdE (e1, p, e2) | ExtE (e1, p, e2) -> check_exp env ctx e1; check_path env ctx p; check_exp env ctx e2 - | SeqE es - | TupE es -> List.iter (check_exp env ctx) es + | SeqE es | TupE es -> List.iter (check_exp env ctx) es | StrE efs -> iter_nl_list (fun ef -> check_exp env ctx (snd ef)) efs | IterE (e1, iter) -> check_iter env ctx iter; - check_exp env (iter::ctx) e1 + check_exp env (iter :: ctx) e1 and check_path env ctx p = match p.it with @@ -120,8 +111,7 @@ and check_path env ctx p = check_path env ctx p1; check_exp env ctx e1; check_exp env ctx e2 - | DotP (p1, _) -> - check_path env ctx p1 + | DotP (p1, _) -> check_path env ctx p1 let rec check_prem env ctx prem = match prem.it with @@ -130,7 +120,7 @@ let rec check_prem env ctx prem = | ElsePr -> () | IterPr (prem', iter) -> check_iter env ctx iter; - check_prem env (iter::ctx) prem' + check_prem env (iter :: ctx) prem' let check_def d : env = match d.it with @@ -147,7 +137,6 @@ let check_def d : env = iter_nl_list (check_prem env []) prems; check_env env - (* Annotating iterations *) open Il.Ast @@ -155,154 +144,159 @@ open Il.Ast type env' = iter list Env.t type occur = Il.Ast.iter list Env.t -let union = Env.union (fun _ ctx1 ctx2 -> assert (ctx1 = ctx2); Some ctx1) - +let union = + Env.union (fun _ ctx1 ctx2 -> + assert (ctx1 = ctx2); + Some ctx1 + ) let rec annot_iter env iter : Il.Ast.iter * occur = match iter with - | Opt | List | List1 -> iter, Env.empty + | Opt | List | List1 -> (iter, Env.empty) | ListN e -> let e', occur = annot_exp env e in - ListN e', occur + (ListN e', occur) and annot_exp env e : Il.Ast.exp * occur = let it, occur = match e.it with - | VarE id -> - VarE id, Env.singleton id.it (Env.find id.it env) - | BoolE _ | NatE _ | TextE _ -> - e.it, Env.empty + | VarE id -> (VarE id, Env.singleton id.it (Env.find id.it env)) + | BoolE _ | NatE _ | TextE _ -> (e.it, Env.empty) | UnE (op, e1) -> let e1', occur1 = annot_exp env e1 in - UnE (op, e1'), occur1 + (UnE (op, e1'), occur1) | BinE (op, e1, e2) -> let e1', occur1 = annot_exp env e1 in let e2', occur2 = annot_exp env e2 in - BinE (op, e1', e2'), union occur1 occur2 + (BinE (op, e1', e2'), union occur1 occur2) | CmpE (op, e1, e2) -> let e1', occur1 = annot_exp env e1 in let e2', occur2 = annot_exp env e2 in - CmpE (op, e1', e2'), union occur1 occur2 + (CmpE (op, e1', e2'), union occur1 occur2) | IdxE (e1, e2) -> let e1', occur1 = annot_exp env e1 in let e2', occur2 = annot_exp env e2 in - IdxE (e1', e2'), union occur1 occur2 + (IdxE (e1', e2'), union occur1 occur2) | SliceE (e1, e2, e3) -> let e1', occur1 = annot_exp env e1 in let e2', occur2 = annot_exp env e2 in let e3', occur3 = annot_exp env e3 in - SliceE (e1', e2', e3'), union (union occur1 occur2) occur3 + (SliceE (e1', e2', e3'), union (union occur1 occur2) occur3) | UpdE (e1, p, e2) -> let e1', occur1 = annot_exp env e1 in let p', occur2 = annot_path env p in let e2', occur3 = annot_exp env e2 in - UpdE (e1', p', e2'), union (union occur1 occur2) occur3 + (UpdE (e1', p', e2'), union (union occur1 occur2) occur3) | ExtE (e1, p, e2) -> let e1', occur1 = annot_exp env e1 in let p', occur2 = annot_path env p in let e2', occur3 = annot_exp env e2 in - ExtE (e1', p', e2'), union (union occur1 occur2) occur3 + (ExtE (e1', p', e2'), union (union occur1 occur2) occur3) | StrE efs -> let efs', occurs = List.split (List.map (annot_expfield env) efs) in - StrE efs', List.fold_left union Env.empty occurs + (StrE efs', List.fold_left union Env.empty occurs) | DotE (e1, atom) -> let e1', occur1 = annot_exp env e1 in - DotE (e1', atom), occur1 + (DotE (e1', atom), occur1) | CompE (e1, e2) -> let e1', occur1 = annot_exp env e1 in let e2', occur2 = annot_exp env e2 in - CompE (e1', e2'), union occur1 occur2 + (CompE (e1', e2'), union occur1 occur2) | LenE e1 -> let e1', occur1 = annot_exp env e1 in - LenE e1', occur1 + (LenE e1', occur1) | TupE es -> let es', occurs = List.split (List.map (annot_exp env) es) in - TupE es', List.fold_left union Env.empty occurs + (TupE es', List.fold_left union Env.empty occurs) | MixE (op, e1) -> let e1', occur1 = annot_exp env e1 in - MixE (op, e1'), occur1 + (MixE (op, e1'), occur1) | CallE (id, e1) -> let e1', occur1 = annot_exp env e1 in - CallE (id, e1'), occur1 + (CallE (id, e1'), occur1) | IterE (e1, iter) -> let e1', occur1 = annot_exp env e1 in let iter', occur' = annot_iterexp env occur1 iter e.at in - IterE (e1', iter'), occur' - | OptE None -> - OptE None, Env.empty + (IterE (e1', iter'), occur') + | OptE None -> (OptE None, Env.empty) | OptE (Some e1) -> let e1', occur1 = annot_exp env e1 in - OptE (Some e1'), occur1 + (OptE (Some e1'), occur1) | TheE e1 -> let e1', occur1 = annot_exp env e1 in - TheE e1', occur1 + (TheE e1', occur1) | ListE es -> let es', occurs = List.split (List.map (annot_exp env) es) in - ListE es', List.fold_left union Env.empty occurs + (ListE es', List.fold_left union Env.empty occurs) | CatE (e1, e2) -> let e1', occur1 = annot_exp env e1 in let e2', occur2 = annot_exp env e2 in - CatE (e1', e2'), union occur1 occur2 + (CatE (e1', e2'), union occur1 occur2) | CaseE (atom, e1) -> let e1', occur1 = annot_exp env e1 in - CaseE (atom, e1'), occur1 + (CaseE (atom, e1'), occur1) | SubE (e1, t1, t2) -> let e1', occur1 = annot_exp env e1 in - SubE (e1', t1, t2), occur1 - in {e with it}, occur + (SubE (e1', t1, t2), occur1) + in + ({e with it}, occur) and annot_expfield env (atom, e) : Il.Ast.expfield * occur = let e', occur = annot_exp env e in - (atom, e'), occur + ((atom, e'), occur) and annot_path env p : Il.Ast.path * occur = let it, occur = match p.it with - | RootP -> RootP, Env.empty + | RootP -> (RootP, Env.empty) | IdxP (p1, e) -> let p1', occur1 = annot_path env p1 in let e', occur2 = annot_exp env e in - IdxP (p1', e'), union occur1 occur2 + (IdxP (p1', e'), union occur1 occur2) | SliceP (p1, e1, e2) -> let p1', occur1 = annot_path env p1 in let e1', occur2 = annot_exp env e1 in let e2', occur3 = annot_exp env e2 in - SliceP (p1', e1', e2'), union occur1 (union occur2 occur3) + (SliceP (p1', e1', e2'), union occur1 (union occur2 occur3)) | DotP (p1, atom) -> let p1', occur1 = annot_path env p1 in - DotP (p1', atom), occur1 - in {p with it}, occur + (DotP (p1', atom), occur1) + in + ({p with it}, occur) and annot_iterexp env occur1 (iter, ids) at : Il.Ast.iterexp * occur = assert (ids = []); let iter', occur2 = annot_iter env iter in let occur1' = - Env.filter_map (fun _ iters -> - match iters with - | [] -> None - | iter1::iters' -> assert (Il.Eq.eq_iter iter iter1); Some iters' - ) occur1 + Env.filter_map + (fun _ iters -> + match iters with + | [] -> None + | iter1 :: iters' -> + assert (Il.Eq.eq_iter iter iter1); + Some iters' + ) + occur1 in let ids' = List.map (fun (x, _) -> x $ at) (Env.bindings occur1') in - (iter', ids'), union occur1' occur2 - + ((iter', ids'), union occur1' occur2) and annot_prem env prem : Il.Ast.premise * occur = let it, occur = match prem.it with | RulePr (id, op, e) -> let e', occur = annot_exp env e in - RulePr (id, op, e'), occur + (RulePr (id, op, e'), occur) | IfPr e -> let e', occur = annot_exp env e in - IfPr e', occur - | ElsePr -> - ElsePr, Env.empty + (IfPr e', occur) + | ElsePr -> (ElsePr, Env.empty) | IterPr (prem1, iter) -> let prem1', occur1 = annot_prem env prem1 in let iter', occur' = annot_iterexp env occur1 iter prem.at in - IterPr (prem1', iter'), occur' - in {prem with it}, occur + (IterPr (prem1', iter'), occur') + in + ({prem with it}, occur) let annot_exp env e = let e', occurs = annot_exp env e in diff --git a/spectec/src/frontend/multiplicity.mli b/spectec/src/frontend/multiplicity.mli index b73e8765bf..ab99b08b91 100644 --- a/spectec/src/frontend/multiplicity.mli +++ b/spectec/src/frontend/multiplicity.mli @@ -4,6 +4,5 @@ type env = El.Ast.iter list Env.t type env' = Il.Ast.iter list Env.t val check_def : El.Ast.def -> env (* raises Source.Error *) - val annot_exp : env' -> Il.Ast.exp -> Il.Ast.exp val annot_prem : env' -> Il.Ast.premise -> Il.Ast.premise diff --git a/spectec/src/frontend/parse.ml b/spectec/src/frontend/parse.ml index 57b0eb4a5c..c5b5263192 100644 --- a/spectec/src/frontend/parse.ml +++ b/spectec/src/frontend/parse.ml @@ -3,8 +3,7 @@ open Util let with_lexbuf name lexbuf start = let open Lexing in lexbuf.lex_curr_p <- {lexbuf.lex_curr_p with pos_fname = name}; - try - start Lexer.token lexbuf + try start Lexer.token lexbuf with Parser.Error -> raise (Source.Error (Lexer.region lexbuf, "unexpected token")) diff --git a/spectec/src/il/ast.ml b/spectec/src/il/ast.ml index 8b89af59f4..ad3724784d 100644 --- a/spectec/src/il/ast.ml +++ b/spectec/src/il/ast.ml @@ -1,9 +1,7 @@ open Util.Source - (* TODO: annotate types on nodes *) - (* Terminals *) type nat = int @@ -11,78 +9,77 @@ type text = string type id = string phrase type atom = - | Atom of string (* atomid *) - | Bot (* `_|_` *) - | Dot (* `.` *) - | Dot2 (* `..` *) - | Dot3 (* `...` *) - | Semicolon (* `;` *) - | Arrow (* `->` *) - | Colon (* `:` *) - | Sub (* `<:` *) - | SqArrow (* `~>` *) - | Turnstile (* `|-` *) - | Tilesturn (* `-|` *) - | LParen (* `(` *) - | LBrack (* `[` *) - | LBrace (* `{` *) - | RParen (* `)` *) - | RBrack (* `]` *) - | RBrace (* `}` *) - | Quest (* `?` *) - | Star (* `*` *) - -type mixop = atom list list (* mixfix name *) - + | Atom of string (* atomid *) + | Bot (* `_|_` *) + | Dot (* `.` *) + | Dot2 (* `..` *) + | Dot3 (* `...` *) + | Semicolon (* `;` *) + | Arrow (* `->` *) + | Colon (* `:` *) + | Sub (* `<:` *) + | SqArrow (* `~>` *) + | Turnstile (* `|-` *) + | Tilesturn (* `-|` *) + | LParen (* `(` *) + | LBrack (* `[` *) + | LBrace (* `{` *) + | RParen (* `)` *) + | RBrack (* `]` *) + | RBrace (* `}` *) + | Quest (* `?` *) + | Star (* `*` *) + +type mixop = atom list list (* mixfix name *) (* Iteration *) type iter = - | Opt (* `?` *) - | List (* `*` *) - | List1 (* `+` *) - | ListN of exp (* `^` exp *) - + | Opt (* `?` *) + | List (* `*` *) + | List1 (* `+` *) + | ListN of exp (* `^` exp *) (* Types *) - and typ = typ' phrase + and typ' = - | VarT of id (* varid *) - | BoolT (* `bool` *) - | NatT (* `nat` *) - | TextT (* `text` *) - | TupT of typ list (* typ * ... * typ *) - | IterT of typ * iter (* typ iter *) + | VarT of id (* varid *) + | BoolT (* `bool` *) + | NatT (* `nat` *) + | TextT (* `text` *) + | TupT of typ list (* typ * ... * typ *) + | IterT of typ * iter (* typ iter *) and deftyp = deftyp' phrase -and deftyp' = - | AliasT of typ (* type alias *) - | NotationT of mixop * typ (* notation type *) - | StructT of typfield list (* record type *) - | VariantT of typcase list (* variant type *) -and typfield = atom * typ * hint list (* record field *) -and typcase = atom * typ * hint list (* variant case *) +and deftyp' = + | AliasT of typ (* type alias *) + | NotationT of mixop * typ (* notation type *) + | StructT of typfield list (* record type *) + | VariantT of typcase list (* variant type *) +and typfield = atom * typ * hint list (* record field *) +and typcase = atom * typ * hint list (* variant case *) (* Expressions *) - and unop = - | NotOp (* `~` *) - | PlusOp (* `+` *) + | NotOp + (* `~` *) + | PlusOp + (* `+` *) | MinusOp (* `-` *) and binop = - | AndOp (* `/\` *) - | OrOp (* `\/` *) + | AndOp (* `/\` *) + | OrOp (* `\/` *) | ImplOp (* `=>` *) | EquivOp (* `<=>` *) - | AddOp (* `+` *) - | SubOp (* `-` *) - | MulOp (* `*` *) - | DivOp (* `/` *) - | ExpOp (* `^` *) + | AddOp (* `+` *) + | SubOp (* `-` *) + | MulOp (* `*` *) + | DivOp (* `/` *) + | ExpOp (* `^` *) and cmpop = | EqOp (* `=` *) @@ -93,80 +90,80 @@ and cmpop = | GeOp (* `>=` *) and exp = (exp', typ) note_phrase -and exp' = - | VarE of id (* varid *) - | BoolE of bool (* bool *) - | NatE of nat (* nat *) - | TextE of text (* text *) - | UnE of unop * exp (* unop exp *) - | BinE of binop * exp * exp (* exp binop exp *) - | CmpE of cmpop * exp * exp (* exp cmpop exp *) - | IdxE of exp * exp (* exp `[` exp `]` *) - | SliceE of exp * exp * exp (* exp `[` exp `:` exp `]` *) - | UpdE of exp * path * exp (* exp `[` path `=` exp `]` *) - | ExtE of exp * path * exp (* exp `[` path `=..` exp `]` *) - | StrE of expfield list (* `{` list(expfield, `,`) `}` *) - | DotE of exp * atom (* exp `.` atom *) - | CompE of exp * exp (* exp `@` exp *) - | LenE of exp (* `|` exp `|` *) - | TupE of exp list (* `(` list2(exp, `,`) `)` *) - | MixE of mixop * exp (* exp atom exp *) - | CallE of id * exp (* defid exp? *) - | IterE of exp * iterexp (* exp iter *) - | OptE of exp option (* exp? *) - | TheE of exp (* THE exp *) - | ListE of exp list (* [exp ... exp] *) - | CatE of exp * exp (* exp :: exp *) - | CaseE of atom * exp (* atom exp *) - | SubE of exp * typ * typ (* exp : typ1 <: typ2 *) - -and expfield = atom * exp (* atom exp *) +and exp' = + | VarE of id (* varid *) + | BoolE of bool (* bool *) + | NatE of nat (* nat *) + | TextE of text (* text *) + | UnE of unop * exp (* unop exp *) + | BinE of binop * exp * exp (* exp binop exp *) + | CmpE of cmpop * exp * exp (* exp cmpop exp *) + | IdxE of exp * exp (* exp `[` exp `]` *) + | SliceE of exp * exp * exp (* exp `[` exp `:` exp `]` *) + | UpdE of exp * path * exp (* exp `[` path `=` exp `]` *) + | ExtE of exp * path * exp (* exp `[` path `=..` exp `]` *) + | StrE of expfield list (* `{` list(expfield, `,`) `}` *) + | DotE of exp * atom (* exp `.` atom *) + | CompE of exp * exp (* exp `@` exp *) + | LenE of exp (* `|` exp `|` *) + | TupE of exp list (* `(` list2(exp, `,`) `)` *) + | MixE of mixop * exp (* exp atom exp *) + | CallE of id * exp (* defid exp? *) + | IterE of exp * iterexp (* exp iter *) + | OptE of exp option (* exp? *) + | TheE of exp (* THE exp *) + | ListE of exp list (* [exp ... exp] *) + | CatE of exp * exp (* exp :: exp *) + | CaseE of atom * exp (* atom exp *) + | SubE of exp * typ * typ (* exp : typ1 <: typ2 *) + +and expfield = atom * exp (* atom exp *) and path = (path', typ) note_phrase + and path' = - | RootP (* *) - | IdxP of path * exp (* path `[` exp `]` *) - | SliceP of path * exp * exp (* path `[` exp `:` exp `]` *) - | DotP of path * atom (* path `.` atom *) + | RootP (* *) + | IdxP of path * exp (* path `[` exp `]` *) + | SliceP of path * exp * exp (* path `[` exp `:` exp `]` *) + | DotP of path * atom (* path `.` atom *) and iterexp = iter * id list - (* Definitions *) - and binds = (id * typ * iter list) list - and def = def' phrase + and def' = - | SynD of id * deftyp (* syntax type *) - | RelD of id * mixop * typ * rule list (* relation *) - | DecD of id * typ * typ * clause list (* definition *) - | RecD of def list (* recursive *) + | SynD of id * deftyp (* syntax type *) + | RelD of id * mixop * typ * rule list (* relation *) + | DecD of id * typ * typ * clause list (* definition *) + | RecD of def list (* recursive *) | HintD of hintdef and rule = rule' phrase + and rule' = - | RuleD of id * binds * mixop * exp * premise list (* relation rule *) + | RuleD of id * binds * mixop * exp * premise list (* relation rule *) and clause = clause' phrase -and clause' = - | DefD of binds * exp * exp * premise list (* definition clause *) - +and clause' = DefD of binds * exp * exp * premise list (* definition clause *) and premise = premise' phrase + and premise' = - | RulePr of id * mixop * exp (* premise *) - | IfPr of exp (* side condition *) - | ElsePr (* otherwise *) - | IterPr of premise * iterexp (* iteration *) + | RulePr of id * mixop * exp (* premise *) + | IfPr of exp (* side condition *) + | ElsePr (* otherwise *) + | IterPr of premise * iterexp (* iteration *) and hintdef = hintdef' phrase + and hintdef' = | SynH of id * hint list | RelH of id * hint list | DecH of id * hint list -and hint = {hintid : id; hintexp : string list} (* hint *) - +and hint = {hintid : id; hintexp : string list} +(* hint *) (* Scripts *) diff --git a/spectec/src/il/dune b/spectec/src/il/dune index 38b4366dee..9cc20a259e 100644 --- a/spectec/src/il/dune +++ b/spectec/src/il/dune @@ -1,5 +1,4 @@ (library - (name il) - (libraries util) - (modules ast eq free print validation) -) + (name il) + (libraries util) + (modules ast eq free print validation)) diff --git a/spectec/src/il/eq.ml b/spectec/src/il/eq.ml index 61fb22f964..cf3de512f9 100644 --- a/spectec/src/il/eq.ml +++ b/spectec/src/il/eq.ml @@ -1,32 +1,24 @@ open Util.Source open Ast - (* Helpers *) let eq_opt eq_x xo1 xo2 = - match xo1, xo2 with - | Some x1, Some x2 -> eq_x x1 x2 - | _, _ -> xo1 = xo2 + match (xo1, xo2) with Some x1, Some x2 -> eq_x x1 x2 | _, _ -> xo1 = xo2 let eq_list eq_x xs1 xs2 = List.length xs1 = List.length xs2 && List.for_all2 eq_x xs1 xs2 - (* Ids *) -let eq_id i1 i2 = - i1.it = i2.it - +let eq_id i1 i2 = i1.it = i2.it (* Iteration *) let rec eq_iter iter1 iter2 = - iter1 = iter2 || - match iter1, iter2 with - | ListN e1, ListN e2 -> eq_exp e1 e2 - | _, _ -> false - + iter1 = iter2 + || + match (iter1, iter2) with ListN e1, ListN e2 -> eq_exp e1 e2 | _, _ -> false (* Types *) @@ -36,21 +28,21 @@ and eq_typ t1 t2 = (Print.string_of_typ t1) (Print.string_of_typ t2) (t1.it = t2.it); *) - t1.it = t2.it || - match t1.it, t2.it with + t1.it = t2.it + || + match (t1.it, t2.it) with | VarT id1, VarT id2 -> eq_id id1 id2 | TupT ts1, TupT ts2 -> eq_list eq_typ ts1 ts2 | IterT (t11, iter1), IterT (t21, iter2) -> eq_typ t11 t21 && eq_iter iter1 iter2 - | _, _ -> - false - + | _, _ -> false (* Expressions *) and eq_exp e1 e2 = - e1.it = e2.it || - match e1.it, e2.it with + e1.it = e2.it + || + match (e1.it, e2.it) with | VarE id1, VarE id2 -> eq_id id1 id2 | UnE (op1, e11), UnE (op2, e21) -> op1 = op2 && eq_exp e11 e21 | BinE (op1, e11, e12), BinE (op2, e21, e22) -> @@ -60,14 +52,14 @@ and eq_exp e1 e2 = | LenE e11, LenE e21 -> eq_exp e11 e21 | IdxE (e11, e12), IdxE (e21, e22) | CompE (e11, e12), CompE (e21, e22) - | CatE (e11, e12), CatE (e21, e22) -> eq_exp e11 e21 && eq_exp e12 e22 + | CatE (e11, e12), CatE (e21, e22) -> + eq_exp e11 e21 && eq_exp e12 e22 | SliceE (e11, e12, e13), SliceE (e21, e22, e23) -> eq_exp e11 e21 && eq_exp e12 e22 && eq_exp e13 e23 | UpdE (e11, p1, e12), UpdE (e21, p2, e22) | ExtE (e11, p1, e12), ExtE (e21, p2, e22) -> eq_exp e11 e21 && eq_path p1 p2 && eq_exp e12 e22 - | TupE es1, TupE es2 - | ListE es1, ListE es2 -> eq_list eq_exp es1 es2 + | TupE es1, TupE es2 | ListE es1, ListE es2 -> eq_list eq_exp es1 es2 | StrE efs1, StrE efs2 -> eq_list eq_expfield efs1 efs2 | DotE (e11, atom1), DotE (e21, atom2) -> eq_exp e11 e21 && atom1 = atom2 | MixE (op1, e1), MixE (op2, e2) -> op1 = op2 && eq_exp e1 e2 @@ -81,11 +73,10 @@ and eq_exp e1 e2 = eq_exp e1 e2 && eq_typ t11 t21 && eq_typ t12 t22 | _, _ -> false -and eq_expfield (atom1, e1) (atom2, e2) = - atom1 = atom2 && eq_exp e1 e2 +and eq_expfield (atom1, e1) (atom2, e2) = atom1 = atom2 && eq_exp e1 e2 and eq_path p1 p2 = - match p1.it, p2.it with + match (p1.it, p2.it) with | RootP, RootP -> true | IdxP (p11, e1), IdxP (p21, e2) -> eq_path p11 p21 && eq_exp e1 e2 | SliceP (p11, e11, e12), SliceP (p21, e21, e22) -> @@ -97,8 +88,9 @@ and eq_iterexp (iter1, ids1) (iter2, ids2) = eq_iter iter1 iter2 && eq_list eq_id ids1 ids2 let rec eq_prem prem1 prem2 = - prem1.it = prem2.it || - match prem1.it, prem2.it with + prem1.it = prem2.it + || + match (prem1.it, prem2.it) with | RulePr (id1, op1, e1), RulePr (id2, op2, e2) -> eq_id id1 id2 && op1 = op2 && eq_exp e1 e2 | IfPr e1, IfPr e2 -> eq_exp e1 e2 diff --git a/spectec/src/il/free.ml b/spectec/src/il/free.ml index 9f25887426..54d81696f7 100644 --- a/spectec/src/il/free.ml +++ b/spectec/src/il/free.ml @@ -1,10 +1,9 @@ open Util.Source open Ast - (* Data Structure *) -module Set = Set.Make(String) +module Set = Set.Make (String) type sets = {synid : Set.t; relid : Set.t; varid : Set.t; defid : Set.t} @@ -15,33 +14,31 @@ let union sets1 sets2 = { synid = Set.union sets1.synid sets2.synid; relid = Set.union sets1.relid sets2.relid; varid = Set.union sets1.varid sets2.varid; - defid = Set.union sets1.defid sets2.defid; + defid = Set.union sets1.defid sets2.defid } let diff sets1 sets2 = { synid = Set.diff sets1.synid sets2.synid; relid = Set.diff sets1.relid sets2.relid; varid = Set.diff sets1.varid sets2.varid; - defid = Set.diff sets1.defid sets2.defid; + defid = Set.diff sets1.defid sets2.defid } let subset sets1 sets2 = - Set.subset sets1.synid sets2.synid && - Set.subset sets1.relid sets2.relid && - Set.subset sets1.varid sets2.varid && - Set.subset sets1.defid sets2.defid + Set.subset sets1.synid sets2.synid + && Set.subset sets1.relid sets2.relid + && Set.subset sets1.varid sets2.varid + && Set.subset sets1.defid sets2.defid let disjoint sets1 sets2 = - Set.disjoint sets1.synid sets2.synid && - Set.disjoint sets1.relid sets2.relid && - Set.disjoint sets1.varid sets2.varid && - Set.disjoint sets1.defid sets2.defid - + Set.disjoint sets1.synid sets2.synid + && Set.disjoint sets1.relid sets2.relid + && Set.disjoint sets1.varid sets2.varid + && Set.disjoint sets1.defid sets2.defid let free_opt free_x xo = Option.(value (map free_x xo) ~default:empty) let free_list free_x xs = List.(fold_left union empty (map free_x xs)) - (* Identifiers *) let free_synid id = {empty with synid = Set.singleton id.it} @@ -49,14 +46,10 @@ let free_relid id = {empty with relid = Set.singleton id.it} let free_varid id = {empty with varid = Set.singleton id.it} let free_defid id = {empty with defid = Set.singleton id.it} - (* Iterations *) let rec free_iter iter = - match iter with - | Opt | List | List1 -> empty - | ListN e -> free_exp e - + match iter with Opt | List | List1 -> empty | ListN e -> free_exp e (* Types *) @@ -76,18 +69,20 @@ and free_deftyp dt = and free_typfield (_, t, _) = free_typ t and free_typcase (_, t, _) = free_typ t - (* Expressions *) and free_exp e = match e.it with | VarE id -> free_varid id | BoolE _ | NatE _ | TextE _ -> empty - | UnE (_, e1) | LenE e1 | TheE e1 | MixE (_, e1) - | DotE (e1, _) | CaseE (_, e1) -> + | UnE (_, e1) | LenE e1 | TheE e1 | MixE (_, e1) | DotE (e1, _) | CaseE (_, e1) + -> free_exp e1 - | BinE (_, e1, e2) | CmpE (_, e1, e2) - | IdxE (e1, e2) | CompE (e1, e2) | CatE (e1, e2) -> + | BinE (_, e1, e2) + | CmpE (_, e1, e2) + | IdxE (e1, e2) + | CompE (e1, e2) + | CatE (e1, e2) -> free_list free_exp [e1; e2] | SliceE (e1, e2, e3) -> free_list free_exp [e1; e2; e3] | OptE eo -> free_opt free_exp eo @@ -109,15 +104,12 @@ and free_path p = union (free_path p1) (union (free_exp e1) (free_exp e2)) | DotP (p1, _atom) -> free_path p1 -and free_iterexp (iter, ids) = - union (free_iter iter) (free_list free_varid ids) - +and free_iterexp (iter, ids) = union (free_iter iter) (free_list free_varid ids) (* Definitions *) let bound_bind (id, _typ, _dim) = free_varid id let bound_binds binds = free_list bound_bind binds - let free_bind (_id, t, _dim) = free_typ t let free_binds binds = free_list free_bind binds @@ -132,18 +124,15 @@ let free_rule rule = match rule.it with | RuleD (_id, binds, _op, e, prems) -> union (free_binds binds) - (diff - (union (free_exp e) (free_list free_prem prems)) - (bound_binds binds) - ) + (diff (union (free_exp e) (free_list free_prem prems)) (bound_binds binds)) let free_clause clause = match clause.it with | DefD (binds, e1, e2, prems) -> union (free_binds binds) (diff - (union (free_list free_exp [e1; e2]) (free_list free_prem prems)) - (bound_binds binds) + (union (free_list free_exp [e1; e2]) (free_list free_prem prems)) + (bound_binds binds) ) let free_hintdef hd = @@ -162,7 +151,6 @@ let rec free_def d = | RecD ds -> free_list free_def ds | HintD hd -> free_hintdef hd - let rec bound_def d = match d.it with | SynD (id, _) -> free_synid id diff --git a/spectec/src/il/free.mli b/spectec/src/il/free.mli index af1fef34c3..9186532a1c 100644 --- a/spectec/src/il/free.mli +++ b/spectec/src/il/free.mli @@ -1,5 +1,4 @@ open Ast - module Set : Set.S with type elt = string type sets = {synid : Set.t; relid : Set.t; varid : Set.t; defid : Set.t} @@ -8,10 +7,8 @@ val subset : sets -> sets -> bool val disjoint : sets -> sets -> bool val union : sets -> sets -> sets val diff : sets -> sets -> sets - val free_opt : ('a -> sets) -> 'a option -> sets val free_list : ('a -> sets) -> 'a list -> sets - val free_iter : iter -> sets val free_typ : typ -> sets val free_exp : exp -> sets @@ -19,5 +16,4 @@ val free_path : path -> sets val free_prem : premise -> sets val free_def : def -> sets val free_deftyp : deftyp -> sets - val bound_def : def -> sets diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml index cc3ac3a37a..97db1fd943 100644 --- a/spectec/src/il/print.ml +++ b/spectec/src/il/print.ml @@ -2,14 +2,12 @@ open Util open Source open Ast - (* Helpers *) let concat = String.concat let prefix s f x = s ^ f x let space f x = " " ^ f x ^ " " - (* Operators *) let string_of_atom = function @@ -34,10 +32,7 @@ let string_of_atom = function | Quest -> "?" | Star -> "*" -let string_of_unop = function - | NotOp -> "~" - | PlusOp -> "+" - | MinusOp -> "-" +let string_of_unop = function NotOp -> "~" | PlusOp -> "+" | MinusOp -> "-" let string_of_binop = function | AndOp -> "/\\" @@ -59,16 +54,17 @@ let string_of_cmpop = function | GeOp -> ">=" let string_of_mixop = function - | [Atom a]::tail when List.for_all ((=) []) tail -> a + | [Atom a] :: tail when List.for_all (( = ) []) tail -> a | mixop -> let s = - String.concat "%" (List.map ( - fun atoms -> String.concat "" (List.map string_of_atom atoms)) mixop - ) + String.concat "%" + (List.map + (fun atoms -> String.concat "" (List.map string_of_atom atoms)) + mixop + ) in "`" ^ s ^ "`" - (* Types *) let rec string_of_iter iter = @@ -93,8 +89,7 @@ and string_of_typ_args t = | TupT _ -> string_of_typ t | _ -> "(" ^ string_of_typ t ^ ")" -and string_of_typs sep ts = - concat sep (List.map string_of_typ ts) +and string_of_typs sep ts = concat sep (List.map string_of_typ ts) and string_of_deftyp dt = match dt.it with @@ -104,8 +99,10 @@ and string_of_deftyp dt = | VariantT tcs -> "\n | " ^ concat "\n | " (List.map string_of_typcase tcs) and string_of_typ_mix mixop t = - if mixop = [[]; []] then string_of_typ t else - string_of_mixop mixop ^ string_of_typ_args t + if mixop = [[]; []] then + string_of_typ t + else + string_of_mixop mixop ^ string_of_typ_args t and string_of_typfield (atom, t, _hints) = string_of_atom atom ^ " " ^ string_of_typ t @@ -113,7 +110,6 @@ and string_of_typfield (atom, t, _hints) = and string_of_typcase (atom, t, _hints) = string_of_atom atom ^ string_of_typ_args t - (* Expressions *) and string_of_exp e = @@ -129,14 +125,11 @@ and string_of_exp e = "(" ^ string_of_exp e1 ^ space string_of_cmpop op ^ string_of_exp e2 ^ ")" | IdxE (e1, e2) -> string_of_exp e1 ^ "[" ^ string_of_exp e2 ^ "]" | SliceE (e1, e2, e3) -> - string_of_exp e1 ^ - "[" ^ string_of_exp e2 ^ " : " ^ string_of_exp e3 ^ "]" + string_of_exp e1 ^ "[" ^ string_of_exp e2 ^ " : " ^ string_of_exp e3 ^ "]" | UpdE (e1, p, e2) -> - string_of_exp e1 ^ - "[" ^ string_of_path p ^ " = " ^ string_of_exp e2 ^ "]" + string_of_exp e1 ^ "[" ^ string_of_path p ^ " = " ^ string_of_exp e2 ^ "]" | ExtE (e1, p, e2) -> - string_of_exp e1 ^ - "[" ^ string_of_path p ^ " =.. " ^ string_of_exp e2 ^ "]" + string_of_exp e1 ^ "[" ^ string_of_path p ^ " =.. " ^ string_of_exp e2 ^ "]" | StrE efs -> "{" ^ concat ", " (List.map string_of_expfield efs) ^ "}" | DotE (e1, atom) -> string_of_exp e1 ^ "." ^ string_of_atom atom ^ "_" ^ string_of_typ e1.note @@ -161,17 +154,13 @@ and string_of_exp_args e = | TupE _ | SubE _ | BinE _ | CmpE _ -> string_of_exp e | _ -> "(" ^ string_of_exp e ^ ")" -and string_of_exps sep es = - concat sep (List.map string_of_exp es) - -and string_of_expfield (atom, e) = - string_of_atom atom ^ " " ^ string_of_exp e +and string_of_exps sep es = concat sep (List.map string_of_exp es) +and string_of_expfield (atom, e) = string_of_atom atom ^ " " ^ string_of_exp e and string_of_path p = match p.it with | RootP -> "" - | IdxP (p1, e) -> - string_of_path p1 ^ "[" ^ string_of_exp e ^ "]" + | IdxP (p1, e) -> string_of_path p1 ^ "[" ^ string_of_exp e ^ "]" | SliceP (p1, e1, e2) -> string_of_path p1 ^ "[" ^ string_of_exp e1 ^ " : " ^ string_of_exp e2 ^ "]" | DotP ({it = RootP; note; _}, atom) -> @@ -182,7 +171,6 @@ and string_of_path p = and string_of_iterexp (iter, ids) = string_of_iter iter ^ "{" ^ String.concat " " (List.map Source.it ids) ^ "}" - (* Definitions *) let string_of_bind (id, t, iters) = @@ -193,37 +181,45 @@ let string_of_binds = function | [] -> "" | binds -> " {" ^ concat ", " (List.map string_of_bind binds) ^ "}" - let rec string_of_prem prem = match prem.it with | RulePr (id, op, e) -> id.it ^ ": " ^ string_of_exp {e with it = MixE (op, e)} | IfPr e -> "if " ^ string_of_exp e | ElsePr -> "otherwise" - | IterPr ({it = IterPr _; _} as prem', iter) -> + | IterPr (({it = IterPr _; _} as prem'), iter) -> string_of_prem prem' ^ string_of_iterexp iter | IterPr (prem', iter) -> "(" ^ string_of_prem prem' ^ ")" ^ string_of_iterexp iter let region_comment indent at = - if at = no_region then "" else - indent ^ ";; " ^ string_of_region at ^ "\n" + if at = no_region then "" else indent ^ ";; " ^ string_of_region at ^ "\n" let string_of_rule rule = match rule.it with | RuleD (id, binds, mixop, e, prems) -> let id' = if id.it = "" then "_" else id.it in - "\n" ^ region_comment " " rule.at ^ - " rule " ^ id' ^ string_of_binds binds ^ ":\n " ^ - string_of_exp {e with it = MixE (mixop, e)} ^ - concat "" (List.map (prefix "\n -- " string_of_prem) prems) + "\n" + ^ region_comment " " rule.at + ^ " rule " + ^ id' + ^ string_of_binds binds + ^ ":\n " + ^ string_of_exp {e with it = MixE (mixop, e)} + ^ concat "" (List.map (prefix "\n -- " string_of_prem) prems) let string_of_clause id clause = match clause.it with | DefD (binds, e1, e2, prems) -> - "\n" ^ region_comment " " clause.at ^ - " def" ^ string_of_binds binds ^ " " ^ id.it ^ string_of_exp_args e1 ^ " = " ^ - string_of_exp e2 ^ - concat "" (List.map (prefix "\n -- " string_of_prem) prems) + "\n" + ^ region_comment " " clause.at + ^ " def" + ^ string_of_binds binds + ^ " " + ^ id.it + ^ string_of_exp_args e1 + ^ " = " + ^ string_of_exp e2 + ^ concat "" (List.map (prefix "\n -- " string_of_prem) prems) let rec string_of_def d = let pre = "\n" ^ region_comment "" d.at in @@ -231,23 +227,29 @@ let rec string_of_def d = | SynD (id, dt) -> pre ^ "syntax " ^ id.it ^ " = " ^ string_of_deftyp dt ^ "\n" | RelD (id, mixop, t, rules) -> - pre ^ "relation " ^ id.it ^ ": " ^ string_of_typ_mix mixop t ^ - concat "\n" (List.map string_of_rule rules) ^ "\n" + pre + ^ "relation " + ^ id.it + ^ ": " + ^ string_of_typ_mix mixop t + ^ concat "\n" (List.map string_of_rule rules) + ^ "\n" | DecD (id, t1, t2, clauses) -> let s1 = - match t1.it with - | TupT [] -> "" - | _ -> string_of_typ t1 ^ " -> " + match t1.it with TupT [] -> "" | _ -> string_of_typ t1 ^ " -> " in - pre ^ "def " ^ id.it ^ " : " ^ s1 ^ string_of_typ t2 ^ - concat "" (List.map (string_of_clause id) clauses) ^ "\n" + pre + ^ "def " + ^ id.it + ^ " : " + ^ s1 + ^ string_of_typ t2 + ^ concat "" (List.map (string_of_clause id) clauses) + ^ "\n" | RecD ds -> pre ^ "rec {\n" ^ concat "" (List.map string_of_def ds) ^ "}" ^ "\n" - | HintD _ -> - "" - + | HintD _ -> "" (* Scripts *) -let string_of_script ds = - concat "" (List.map string_of_def ds) +let string_of_script ds = concat "" (List.map string_of_def ds) diff --git a/spectec/src/il/validation.ml b/spectec/src/il/validation.ml index a63fb5507c..24d8e449bb 100644 --- a/spectec/src/il/validation.ml +++ b/spectec/src/il/validation.ml @@ -3,15 +3,13 @@ open Source open Ast open Print - (* Errors *) let error at msg = Source.error at "validation" msg - (* Environment *) -module Env = Map.Make(String) +module Env = Map.Make (String) type var_typ = typ * iter list type syn_typ = deftyp @@ -22,15 +20,11 @@ type env = { mutable vars : var_typ Env.t; mutable typs : syn_typ Env.t; mutable rels : rel_typ Env.t; - mutable defs : def_typ Env.t; + mutable defs : def_typ Env.t } let new_env () = - { vars = Env.empty; - typs = Env.empty; - rels = Env.empty; - defs = Env.empty; - } + {vars = Env.empty; typs = Env.empty; rels = Env.empty; defs = Env.empty} let fwd_deftyp id = NotationT ([[]; []], VarT (id $ no_region) $ no_region) let fwd_deftyp_bad = fwd_deftyp "(undefined)" $ no_region @@ -61,12 +55,11 @@ let find_case cases atom at = | Some (_, x, _) -> x | None -> error at ("unknown case `" ^ string_of_atom atom ^ "`") - (* Type Accessors *) let rec expand' env = function | VarT id as t' -> - (match (find "syntax type" env.typs id).it with + ( match (find "syntax type" env.typs id).it with | AliasT t1 -> expand' env t1.it | _ -> t' ) @@ -74,24 +67,24 @@ let rec expand' env = function let expand env t = expand' env t.it - type direction = Infer | Check let as_error at phrase dir t expected = match dir with | Infer -> - error at ( - phrase ^ "'s type `" ^ string_of_typ t ^ - "` does not match expected type `" ^ expected ^ "`" - ) + error at + (phrase + ^ "'s type `" + ^ string_of_typ t + ^ "` does not match expected type `" + ^ expected + ^ "`" + ) | Check -> - error at ( - phrase ^ "'s type does not match expected type `" ^ - string_of_typ t ^ "`" - ) + error at + (phrase ^ "'s type does not match expected type `" ^ string_of_typ t ^ "`") -let match_iter iter1 iter2 = - iter2 = List || Eq.eq_iter iter1 iter2 +let match_iter iter1 iter2 = iter2 = List || Eq.eq_iter iter1 iter2 let as_iter_typ iter phrase env dir t at : typ = match expand' env t.it with @@ -108,16 +101,15 @@ let as_tup_typ phrase env dir t at : typ list = | TupT ts -> ts | _ -> as_error at phrase dir t "(_,...,_)" - let as_mix_typid phrase env id at : mixop * typ = match (find "syntax type" env.typs id).it with - | NotationT (mixop, t) -> mixop, t + | NotationT (mixop, t) -> (mixop, t) | _ -> as_error at phrase Infer (VarT id $ id.at) "`mixin-op`(...)" let as_mix_typ phrase env dir t at : mixop * typ = match expand' env t.it with | VarT id -> as_mix_typid phrase env id at - | _ -> as_error at phrase dir t ("`mixin-op`(...)") + | _ -> as_error at phrase dir t "`mixin-op`(...)" let as_struct_typid phrase env id at : typfield list = match (find "syntax type" env.typs id).it with @@ -139,7 +131,6 @@ let as_variant_typ phrase env dir t at : typcase list = | VarT id -> as_variant_typid phrase env id at | _ -> as_error at phrase dir t "| ..." - (* Type Equivalence *) let equiv_list equiv_x xs1 xs2 = @@ -151,21 +142,25 @@ let rec equiv_typ' env t1 t2 = (Print.string_of_typ t1) (Print.string_of_typ t2) (t1.it = t2.it); *) - t1.it = t2.it || - match expand env t1, expand env t2 with + t1.it = t2.it + || + match (expand env t1, expand env t2) with | VarT id1, VarT id2 -> id1.it = id2.it - | TupT ts1, TupT ts2 -> - equiv_list (equiv_typ' env) ts1 ts2 + | TupT ts1, TupT ts2 -> equiv_list (equiv_typ' env) ts1 ts2 | IterT (t11, iter1), IterT (t21, iter2) -> equiv_typ' env t11 t21 && Eq.eq_iter iter1 iter2 - | t1', t2' -> - Eq.eq_typ (t1' $ t1.at) (t2' $ t2.at) + | t1', t2' -> Eq.eq_typ (t1' $ t1.at) (t2' $ t2.at) let equiv_typ env t1 t2 at = if not (equiv_typ' env t1 t2) then - error at ("expression's type `" ^ string_of_typ t1 ^ "` " ^ - "does not match expected type `" ^ string_of_typ t2 ^ "`") - + error at + ("expression's type `" + ^ string_of_typ t1 + ^ "` " + ^ "does not match expected type `" + ^ string_of_typ t2 + ^ "`" + ) (* Subtyping *) @@ -175,36 +170,47 @@ let sub_typ' env t1 t2 = (Print.string_of_typ t1) (Print.string_of_typ t2) (t1.it = t2.it); *) - equiv_typ' env t1 t2 || - match expand env t1, expand env t2 with + equiv_typ' env t1 t2 + || + match (expand env t1, expand env t2) with | VarT id1, VarT id2 -> - (match (find "" env.typs id1).it, (find "" env.typs id2).it with + ( match ((find "" env.typs id1).it, (find "" env.typs id2).it) with | StructT tfs1, StructT tfs2 -> - List.for_all (fun (atom, t2, _) -> - try let t1 = find_field tfs1 atom t2.at in Eq.eq_typ t1 t2 - with Error _ -> false - ) tfs2 + List.for_all + (fun (atom, t2, _) -> + try + let t1 = find_field tfs1 atom t2.at in + Eq.eq_typ t1 t2 + with Error _ -> false + ) + tfs2 | VariantT tcs1, VariantT tcs2 -> - List.for_all (fun (atom, t1, _) -> - try let t2 = find_case tcs2 atom t1.at in Eq.eq_typ t1 t2 - with Error _ -> false - ) tcs1 + List.for_all + (fun (atom, t1, _) -> + try + let t2 = find_case tcs2 atom t1.at in + Eq.eq_typ t1 t2 + with Error _ -> false + ) + tcs1 | _, _ -> false ) - | _, _ -> - false + | _, _ -> false let sub_typ env t1 t2 at = if not (sub_typ' env t1 t2) then - error at ("expression's type `" ^ string_of_typ t1 ^ "` " ^ - "does not match expected supertype `" ^ string_of_typ t2 ^ "`") - + error at + ("expression's type `" + ^ string_of_typ t1 + ^ "` " + ^ "does not match expected supertype `" + ^ string_of_typ t2 + ^ "`" + ) (* Operators *) -let infer_unop = function - | NotOp -> BoolT - | PlusOp | MinusOp -> NatT +let infer_unop = function NotOp -> BoolT | PlusOp | MinusOp -> NatT let infer_binop = function | AndOp | OrOp | ImplOp | EquivOp -> BoolT @@ -214,36 +220,44 @@ let infer_cmpop = function | EqOp | NeOp -> None | LtOp | GtOp | LeOp | GeOp -> Some NatT - (* Atom Bindings *) let check_atoms phrase item list at = let _, dups = - List.fold_right (fun (atom, _, _) (set, dups) -> - let s = Print.string_of_atom atom in - Free.Set.(if mem s set then (set, s::dups) else (add s set, dups)) - ) list (Free.Set.empty, []) + List.fold_right + (fun (atom, _, _) (set, dups) -> + let s = Print.string_of_atom atom in + Free.Set.(if mem s set then (set, s :: dups) else (add s set, dups)) + ) + list (Free.Set.empty, []) in if dups <> [] then - error at (phrase ^ " contains duplicate " ^ item ^ "(s) `" ^ - String.concat "`, `" dups ^ "`") - + error at + (phrase + ^ " contains duplicate " + ^ item + ^ "(s) `" + ^ String.concat "`, `" dups + ^ "`" + ) (* Iteration *) let valid_list valid_x_y env xs ys at = if List.length xs <> List.length ys then - error at ("arity mismatch for expression list, expected " ^ - string_of_int (List.length ys) ^ ", got " ^ string_of_int (List.length xs)); + error at + ("arity mismatch for expression list, expected " + ^ string_of_int (List.length ys) + ^ ", got " + ^ string_of_int (List.length xs) + ); List.iter2 (valid_x_y env) xs ys - let rec valid_iter env iter = match iter with | Opt | List | List1 -> () | ListN e -> valid_exp env e (NatT $ e.at) - (* Types *) and valid_typ env t = @@ -251,23 +265,20 @@ and valid_typ env t = | VarT id -> if find "syntax type" env.typs id = fwd_deftyp_bad then error t.at ("invalid forward reference to syntax type `" ^ id.it ^ "`") - | BoolT - | NatT - | TextT -> - () - | TupT ts -> - List.iter (valid_typ env) ts + | BoolT | NatT | TextT -> () + | TupT ts -> List.iter (valid_typ env) ts | IterT (t1, iter) -> - match iter with + ( match iter with | ListN e -> error e.at "definite iterator not allowed in type" - | _ -> valid_typ env t1; valid_iter env iter + | _ -> + valid_typ env t1; + valid_iter env iter + ) and valid_deftyp env dt = match dt.it with - | AliasT t -> - valid_typ env t - | NotationT (mixop, t) -> - valid_typ_mix env mixop t dt.at + | AliasT t -> valid_typ env t + | NotationT (mixop, t) -> valid_typ_mix env mixop t dt.at | StructT tfs -> check_atoms "record" "field" tfs dt.at; List.iter (valid_typfield env) tfs @@ -276,20 +287,19 @@ and valid_deftyp env dt = List.iter (valid_typcase env) tcs and valid_typ_mix env mixop t at = - let arity = - match t.it with - | TupT ts -> List.length ts - | _ -> 1 - in + let arity = match t.it with TupT ts -> List.length ts | _ -> 1 in if List.length mixop <> arity + 1 then - error at ("inconsistent arity in mixin notation, `" ^ string_of_mixop mixop ^ - "` applied to " ^ string_of_typ t); + error at + ("inconsistent arity in mixin notation, `" + ^ string_of_mixop mixop + ^ "` applied to " + ^ string_of_typ t + ); valid_typ env t and valid_typfield env (_atom, t, _hints) = valid_typ env t and valid_typcase env (_atom, t, _hints) = valid_typ env t - (* Expressions *) and infer_exp env e : typ = @@ -302,10 +312,8 @@ and infer_exp env e : typ = | BinE (op, _, _) -> infer_binop op $ e.at | CmpE _ -> BoolT $ e.at | IdxE (e1, _) -> as_list_typ "expression" env Infer (infer_exp env e1) e1.at - | SliceE (e1, _, _) - | UpdE (e1, _, _) - | ExtE (e1, _, _) - | CompE (e1, _) -> infer_exp env e1 + | SliceE (e1, _, _) | UpdE (e1, _, _) | ExtE (e1, _, _) | CompE (e1, _) -> + infer_exp env e1 | StrE _ -> error e.at "cannot infer type of record" | DotE (e1, atom) -> let tfs = as_struct_typ "expression" env Infer (infer_exp env e1) e1.at in @@ -323,7 +331,6 @@ and infer_exp env e : typ = | CaseE _ -> error e.at "cannot infer type of case constructor" | SubE _ -> error e.at "cannot infer type of subsumption" - and valid_exp env e t = (* Printf.printf "[valid %s] %s : %s == %s\n%!" @@ -335,9 +342,12 @@ and valid_exp env e t = let t', dim = find "variable" env.vars id in equiv_typ env t' t e.at; if dim <> [] then - error e.at ("use of iterated variable `" ^ - id.it ^ String.concat "" (List.map string_of_iter dim) ^ - "` outside suitable iteraton context") + error e.at + ("use of iterated variable `" + ^ id.it + ^ String.concat "" (List.map string_of_iter dim) + ^ "` outside suitable iteraton context" + ) | BoolE _ | NatE _ | TextE _ -> let t' = infer_exp env e in equiv_typ env t' t e.at @@ -414,8 +424,7 @@ and valid_exp env e t = | OptE eo -> let t1 = as_iter_typ Opt "option" env Check t e.at in Option.iter (fun e1 -> valid_exp env e1 t1) eo - | TheE e1 -> - valid_exp env e1 (IterT (t, Opt) $ e1.at) + | TheE e1 -> valid_exp env e1 (IterT (t, Opt) $ e1.at) | ListE es -> let t1 = as_iter_typ List "list" env Check t e.at in List.iter (fun eI -> valid_exp env eI t1) es @@ -436,10 +445,13 @@ and valid_exp env e t = and valid_expmix env mixop e (mixop', t) at = if mixop <> mixop' then - error at ( - "mixin notation `" ^ string_of_mixop mixop ^ - "` does not match expected notation `" ^ string_of_mixop mixop' ^ "`" - ); + error at + ("mixin notation `" + ^ string_of_mixop mixop + ^ "` does not match expected notation `" + ^ string_of_mixop mixop' + ^ "`" + ); valid_exp env e t and valid_expfield env (atom1, e) (atom2, t, _) = @@ -470,41 +482,51 @@ and valid_path env p t : typ = and valid_iterexp env (iter, ids) : env = valid_iter env iter; - List.fold_left (fun env id -> - match find "variable" env.vars id with - | t, iter1::iters - when Eq.eq_iter (snd (Lib.List.split_last (iter1::iters))) iter -> - {env with vars = - Env.add id.it (t, fst (Lib.List.split_last (iter1::iters))) env.vars} - | _, iters -> - error id.at ("iteration variable `" ^ id.it ^ - "` has incompatible dimension `" ^ id.it ^ - String.concat "" (List.map string_of_iter iters) ^ - "` in iteration `_" ^ string_of_iter iter ^ "`") - ) env ids - + List.fold_left + (fun env id -> + match find "variable" env.vars id with + | t, iter1 :: iters + when Eq.eq_iter (snd (Lib.List.split_last (iter1 :: iters))) iter -> + { env with + vars = + Env.add id.it + (t, fst (Lib.List.split_last (iter1 :: iters))) + env.vars + } + | _, iters -> + error id.at + ("iteration variable `" + ^ id.it + ^ "` has incompatible dimension `" + ^ id.it + ^ String.concat "" (List.map string_of_iter iters) + ^ "` in iteration `_" + ^ string_of_iter iter + ^ "`" + ) + ) + env ids (* Definitions *) let valid_binds env binds = - List.iter (fun (id, t, dim) -> - valid_typ env t; - env.vars <- bind "variable" env.vars id (t, dim) - ) binds + List.iter + (fun (id, t, dim) -> + valid_typ env t; + env.vars <- bind "variable" env.vars id (t, dim) + ) + binds let rec valid_prem env prem = match prem.it with | RulePr (id, mixop, e) -> valid_expmix env mixop e (find "relation" env.rels id) e.at - | IfPr e -> - valid_exp env e (BoolT $ e.at) - | ElsePr -> - () + | IfPr e -> valid_exp env e (BoolT $ e.at) + | ElsePr -> () | IterPr (prem', iter) -> let env' = valid_iterexp env iter in valid_prem env' prem' - let valid_rule env mixop t rule = match rule.it with | RuleD (_id, binds, mixop', e, prems) -> @@ -523,15 +545,18 @@ let valid_clause env t1 t2 clause = env.vars <- Env.empty; let free_rh = Free.(Set.diff (free_exp e2).varid (free_exp e1).varid) in if free_rh <> Free.Set.empty then - error clause.at ("definition contains unbound variable(s) `" ^ - String.concat "`, `" (Free.Set.elements free_rh) ^ "`") - + error clause.at + ("definition contains unbound variable(s) `" + ^ String.concat "`, `" (Free.Set.elements free_rh) + ^ "`" + ) let infer_def env d = match d.it with | SynD (id, dt) -> let fwd_deftyp = - match dt.it with NotationT _ -> fwd_deftyp_bad | _ -> fwd_deftyp_ok in + match dt.it with NotationT _ -> fwd_deftyp_bad | _ -> fwd_deftyp_ok + in env.typs <- bind "syntax" env.typs id fwd_deftyp | RelD (id, mixop, t, _rules) -> valid_typ_mix env mixop t d.at; @@ -542,14 +567,13 @@ let infer_def env d = env.defs <- bind "function" env.defs id (t1, t2) | _ -> () - type bind = {bind : 'a. string -> 'a Env.t -> id -> 'a -> 'a Env.t} let rec valid_def {bind} env d = match d.it with | SynD (id, dt) -> valid_deftyp env dt; - env.typs <- bind "syntax" env.typs id dt; + env.typs <- bind "syntax" env.typs id dt | RelD (id, mixop, t, rules) -> valid_typ_mix env mixop t d.at; List.iter (valid_rule env mixop t) rules; @@ -562,19 +586,24 @@ let rec valid_def {bind} env d = | RecD ds -> List.iter (infer_def env) ds; List.iter (valid_def {bind = rebind} env) ds; - List.iter (fun d -> - match (List.hd ds).it, d.it with - | HintD _, _ | _, HintD _ - | SynD _, SynD _ - | RelD _, RelD _ - | DecD _, DecD _ -> () - | _, _ -> - error (List.hd ds).at (" " ^ string_of_region d.at ^ - ": invalid recursion between definitions of different sort") - ) ds - | HintD _ -> - () - + List.iter + (fun d -> + match ((List.hd ds).it, d.it) with + | HintD _, _ + | _, HintD _ + | SynD _, SynD _ + | RelD _, RelD _ + | DecD _, DecD _ -> + () + | _, _ -> + error (List.hd ds).at + (" " + ^ string_of_region d.at + ^ ": invalid recursion between definitions of different sort" + ) + ) + ds + | HintD _ -> () (* Scripts *) diff --git a/spectec/src/middlend/dune b/spectec/src/middlend/dune index 6564b4b657..d9ef93fb68 100644 --- a/spectec/src/middlend/dune +++ b/spectec/src/middlend/dune @@ -1,5 +1,4 @@ (library - (name middlend) - (libraries util il) - (modules sub totalize unthe sideconditions) -) + (name middlend) + (libraries util il) + (modules sub totalize unthe sideconditions)) diff --git a/spectec/src/middlend/sideconditions.ml b/spectec/src/middlend/sideconditions.ml index 8b592aa480..6323fa8d94 100644 --- a/spectec/src/middlend/sideconditions.ml +++ b/spectec/src/middlend/sideconditions.ml @@ -8,7 +8,7 @@ of terms in premises and conclusions: (The option projection would probably be nicer by rewriting !(e) to a fresh variable x and require e=?x. Maybe later.) -*) + *) open Util open Source @@ -18,39 +18,75 @@ open Il.Ast let _error at msg = Source.error at "sideconditions" msg -module Env = Map.Make(String) +module Env = Map.Make (String) -let is_null e = CmpE (EqOp, e, OptE None $$ no_region % e.note) $$ no_region % (BoolT $ e.at) -let iffE e1 e2 = IfPr (BinE (EquivOp, e1, e2) $$ no_region % (BoolT $ no_region)) $ no_region -let same_len e1 e2 = IfPr (CmpE (EqOp, LenE e1 $$ no_region % (NatT $ e1.at), LenE e2 $$ no_region % (NatT $ e2.at)) $$ no_region % (BoolT $ no_region)) $ no_region -let has_len ne e = IfPr (CmpE (EqOp, LenE e $$ no_region % (NatT $ e.at), ne) $$ no_region % (BoolT $ no_region)) $ no_region +let is_null e = + CmpE (EqOp, e, OptE None $$ no_region % e.note) $$ no_region % (BoolT $ e.at) + +let iffE e1 e2 = + IfPr (BinE (EquivOp, e1, e2) $$ no_region % (BoolT $ no_region)) $ no_region + +let same_len e1 e2 = + IfPr + (CmpE + ( EqOp, + LenE e1 $$ no_region % (NatT $ e1.at), + LenE e2 $$ no_region % (NatT $ e2.at) + ) + $$ no_region % (BoolT $ no_region) + ) + $ no_region + +let has_len ne e = + IfPr + (CmpE (EqOp, LenE e $$ no_region % (NatT $ e.at), ne) + $$ no_region % (BoolT $ no_region) + ) + $ no_region let iter_side_conditions env ((iter, vs) : iterexp) : premise list = let iter' = if iter = Opt then Opt else List in - let ves = List.map (fun v -> - let t = Env.find v.it env in - IterE (VarE v $$ no_region % t, (iter, [v])) $$ no_region % (IterT (t, iter') $ no_region)) vs in - match iter, ves with + let ves = + List.map + (fun v -> + let t = Env.find v.it env in + IterE (VarE v $$ no_region % t, (iter, [v])) + $$ no_region % (IterT (t, iter') $ no_region) + ) + vs + in + match (iter, ves) with | _, [] -> [] - | Opt, (e::es) -> List.map (fun e' -> iffE (is_null e) (is_null e')) es - | (List|List1), (e::es) -> List.map (same_len e) es + | Opt, e :: es -> List.map (fun e' -> iffE (is_null e) (is_null e')) es + | (List | List1), e :: es -> List.map (same_len e) es | ListN ne, es -> List.map (has_len ne) es (* Expr traversal *) let rec t_exp env e : premise list = (* First the conditions to be generated here *) - begin match e.it with - | IdxE (exp1, exp2) -> - [IfPr (CmpE (LtOp, exp2, LenE exp1 $$ no_region % exp2.note) $$ no_region % (BoolT $ no_region)) $ no_region] - | TheE exp -> - [IfPr (CmpE (NeOp, exp, OptE None $$ no_region % exp.note) $$ no_region % (BoolT $ no_region)) $ no_region] - | IterE (_exp, iterexp) -> iter_side_conditions env iterexp - | _ -> [] - end @ + begin + match e.it with + | IdxE (exp1, exp2) -> + [ IfPr + (CmpE (LtOp, exp2, LenE exp1 $$ no_region % exp2.note) + $$ no_region % (BoolT $ no_region) + ) + $ no_region + ] + | TheE exp -> + [ IfPr + (CmpE (NeOp, exp, OptE None $$ no_region % exp.note) + $$ no_region % (BoolT $ no_region) + ) + $ no_region + ] + | IterE (_exp, iterexp) -> iter_side_conditions env iterexp + | _ -> [] + end + @ (* And now descend *) match e.it with - | VarE _ | BoolE _ | NatE _ | TextE _ | OptE None - -> [] + | VarE _ | BoolE _ | NatE _ | TextE _ | OptE None -> [] | UnE (_, exp) | DotE (exp, _) | LenE exp @@ -59,75 +95,69 @@ let rec t_exp env e : premise list = | OptE (Some exp) | TheE exp | CaseE (_, exp) - | SubE (exp, _, _) - -> t_exp env exp + | SubE (exp, _, _) -> + t_exp env exp | BinE (_, exp1, exp2) | CmpE (_, exp1, exp2) | IdxE (exp1, exp2) | CompE (exp1, exp2) - | CatE (exp1, exp2) - -> t_exp env exp1 @ t_exp env exp2 - | SliceE (exp1, exp2, exp3) - -> t_exp env exp1 @ t_exp env exp2 @ t_exp env exp3 - | UpdE (exp1, path, exp2) - | ExtE (exp1, path, exp2) - -> t_exp env exp1 @ t_path env path @ t_exp env exp2 - | StrE fields - -> List.concat_map (fun (_, e) -> t_exp env e) fields - | TupE es | ListE es - -> List.concat_map (t_exp env) es - | IterE (e, iterexp) - -> List.map (fun pr -> IterPr (pr, iterexp) $ no_region) (t_exp env e) @ t_iterexp env iterexp + | CatE (exp1, exp2) -> + t_exp env exp1 @ t_exp env exp2 + | SliceE (exp1, exp2, exp3) -> + t_exp env exp1 @ t_exp env exp2 @ t_exp env exp3 + | UpdE (exp1, path, exp2) | ExtE (exp1, path, exp2) -> + t_exp env exp1 @ t_path env path @ t_exp env exp2 + | StrE fields -> List.concat_map (fun (_, e) -> t_exp env e) fields + | TupE es | ListE es -> List.concat_map (t_exp env) es + | IterE (e, iterexp) -> + List.map (fun pr -> IterPr (pr, iterexp) $ no_region) (t_exp env e) + @ t_iterexp env iterexp and t_iterexp env (iter, _) = t_iter env iter +and t_iter env = function ListN e -> t_exp env e | _ -> [] -and t_iter env = function - | ListN e -> t_exp env e - | _ -> [] - -and t_path env path = match path.it with +and t_path env path = + match path.it with | RootP -> [] | IdxP (path, e) -> t_path env path @ t_exp env e | SliceP (path, e1, e2) -> t_path env path @ t_exp env e1 @ t_exp env e2 | DotP (path, _) -> t_path env path - -let rec t_prem env prem = match prem.it with +let rec t_prem env prem = + match prem.it with | RulePr (_, _, exp) -> t_exp env exp | IfPr e -> t_exp env e | ElsePr -> [] - | IterPr (prem, iterexp) - -> iter_side_conditions env iterexp @ - List.map (fun pr -> IterPr (pr, iterexp) $ no_region) (t_prem env prem) @ t_iterexp env iterexp + | IterPr (prem, iterexp) -> + iter_side_conditions env iterexp + @ List.map (fun pr -> IterPr (pr, iterexp) $ no_region) (t_prem env prem) + @ t_iterexp env iterexp let t_prems env = List.concat_map (t_prem env) (* Does prem1 obviously imply prem2? *) -let rec implies prem1 prem2 = Il.Eq.eq_prem prem1 prem2 || - match prem2.it with - | IterPr (prem2', _) -> implies prem1 prem2' - | _ -> false - +let rec implies prem1 prem2 = + Il.Eq.eq_prem prem1 prem2 + || + match prem2.it with IterPr (prem2', _) -> implies prem1 prem2' | _ -> false let t_rule' = function | RuleD (id, binds, mixop, exp, prems) -> - let env = List.fold_left (fun env (v, t, _) -> Env.add v.it t env) Env.empty binds in + let env = + List.fold_left (fun env (v, t, _) -> Env.add v.it t env) Env.empty binds + in let extra_prems = t_prems env prems @ t_exp env exp in let prems' = Util.Lib.List.nub implies (extra_prems @ prems) in RuleD (id, binds, mixop, exp, prems') -let t_rule x = { x with it = t_rule' x.it } - +let t_rule x = {x with it = t_rule' x.it} let t_rules = List.map t_rule let rec t_def' = function | RecD defs -> RecD (List.map t_def defs) - | RelD (id, mixop, typ, rules) -> - RelD (id, mixop, typ, t_rules rules) + | RelD (id, mixop, typ, rules) -> RelD (id, mixop, typ, t_rules rules) | def -> def -and t_def x = { x with it = t_def' x.it } - -let transform (defs : script) = - List.map t_def defs +and t_def x = {x with it = t_def' x.it} +let transform (defs : script) = List.map t_def defs diff --git a/spectec/src/middlend/sub.ml b/spectec/src/middlend/sub.ml index ceda4ad2e2..8d0b3732ab 100644 --- a/spectec/src/middlend/sub.ml +++ b/spectec/src/middlend/sub.ml @@ -32,9 +32,11 @@ let error at msg = Source.error at "subtype elimination" msg (* Environment *) -module M = Map.Make(String) -module S = Set.Make(struct +module M = Map.Make (String) + +module S = Set.Make (struct type t = id * id + let compare (t1, t2) (t3, t4) = compare (t1.it, t2.it) (t3.it, t4.it) end) @@ -43,15 +45,9 @@ The environment consist of: * Which constructors the type has (and their non-aliased concrete type) * Which SubE type pairs have been observed, but not yet generated *) -type env = - { mutable typ : (id * typcase list) M.t; - mutable pairs : S.t - } +type env = {mutable typ : (id * typcase list) M.t; mutable pairs : S.t} -let new_env () : env = - { typ = M.empty; - pairs = S.empty; - } +let new_env () : env = {typ = M.empty; pairs = S.empty} let lookup (env : env) (id : id) : id * typcase list = match M.find_opt id.it env.typ with @@ -66,15 +62,19 @@ let register_variant (env : env) (id : id) (cases : typcase list) = let register_alias (env : env) (id : id) (id2 : id) = match M.find_opt id2.it env.typ with - | Some type_info -> - env.typ <- M.add id.it type_info env.typ + | Some type_info -> env.typ <- M.add id.it type_info env.typ | None -> () (* Not an alias of a variant type *) let injection_name (sub : id) (sup : id) = sup.it ^ "_" ^ sub.it $ no_region -let var_of_typ typ = match typ.it with +let var_of_typ typ = + match typ.it with | VarT id -> id - | _ -> error typ.at ("Non-variable type expression not supported:\n" ^ Il.Print.string_of_typ typ) + | _ -> + error typ.at + ("Non-variable type expression not supported:\n" + ^ Il.Print.string_of_typ typ + ) (* Step 1 and 4: Collect SubE occurrences, and replace with function *) @@ -86,12 +86,12 @@ let rec t_exp env exp = let sub = var_of_typ sub_ty in let sup = var_of_typ sup_ty in env.pairs <- S.add (sub, sup) env.pairs; - { exp' with it = CallE (injection_name sub sup, e)} + {exp' with it = CallE (injection_name sub sup, e)} | _ -> exp' (* Traversal boilerplate *) -and t_exp2 env x = { x with it = t_exp' env x.it } +and t_exp2 env x = {x with it = t_exp' env x.it} and t_exp' env = function | (VarE _ | BoolE _ | NatE _ | TextE _) as e -> e @@ -99,10 +99,13 @@ and t_exp' env = function | BinE (binop, exp1, exp2) -> BinE (binop, t_exp env exp1, t_exp env exp2) | CmpE (cmpop, exp1, exp2) -> CmpE (cmpop, t_exp env exp1, t_exp env exp2) | IdxE (exp1, exp2) -> IdxE (t_exp env exp1, t_exp env exp2) - | SliceE (exp1, exp2, exp3) -> SliceE (t_exp env exp1, t_exp env exp2, t_exp env exp3) - | UpdE (exp1, path, exp2) -> UpdE (t_exp env exp1, t_path env path, t_exp env exp2) - | ExtE (exp1, path, exp2) -> ExtE (t_exp env exp1, t_path env path, t_exp env exp2) - | StrE fields -> StrE (List.map (fun (a, e) -> a, t_exp env e) fields) + | SliceE (exp1, exp2, exp3) -> + SliceE (t_exp env exp1, t_exp env exp2, t_exp env exp3) + | UpdE (exp1, path, exp2) -> + UpdE (t_exp env exp1, t_path env path, t_exp env exp2) + | ExtE (exp1, path, exp2) -> + ExtE (t_exp env exp1, t_path env path, t_exp env exp2) + | StrE fields -> StrE (List.map (fun (a, e) -> (a, t_exp env e)) fields) | DotE (e, a) -> DotE (t_exp env e, a) | CompE (exp1, exp2) -> CompE (t_exp env exp1, t_exp env exp2) | LenE exp -> LenE exp @@ -118,10 +121,7 @@ and t_exp' env = function | CaseE (a, e) -> CaseE (a, t_exp env e) | SubE (e, t1, t2) -> SubE (e, t1, t2) -and t_iter env = function - | ListN e -> ListN (t_exp env e) - | i -> i - +and t_iter env = function ListN e -> ListN (t_exp env e) | i -> i and t_iterexp env (iter, vs) = (t_iter env iter, vs) and t_path' env = function @@ -130,7 +130,7 @@ and t_path' env = function | SliceP (path, e1, e2) -> SliceP (t_path env path, t_exp env e1, t_exp env e2) | DotP (path, a) -> DotP (t_path env path, a) -and t_path env x = { x with it = t_path' env x.it } +and t_path env x = {x with it = t_path' env x.it} let rec t_prem' env = function | RulePr (id, mixop, exp) -> RulePr (id, mixop, t_exp env exp) @@ -138,23 +138,22 @@ let rec t_prem' env = function | ElsePr -> ElsePr | IterPr (prem, iterexp) -> IterPr (t_prem env prem, t_iterexp env iterexp) -and t_prem env x = { x with it = t_prem' env x.it } +and t_prem env x = {x with it = t_prem' env x.it} let t_prems env = List.map (t_prem env) let t_clause' env = function - | DefD (binds, lhs, rhs, prems) -> - DefD (binds, t_exp env lhs, t_exp env rhs, t_prems env prems) - -let t_clause env (clause : clause) = { clause with it = t_clause' env clause.it } + | DefD (binds, lhs, rhs, prems) -> + DefD (binds, t_exp env lhs, t_exp env rhs, t_prems env prems) +let t_clause env (clause : clause) = {clause with it = t_clause' env clause.it} let t_clauses env = List.map (t_clause env) let t_rule' env = function | RuleD (id, binds, mixop, exp, prems) -> RuleD (id, binds, mixop, t_exp env exp, t_prems env prems) -let t_rule env x = { x with it = t_rule' env x.it } +let t_rule env x = {x with it = t_rule' env x.it} let rec t_def' env = function | RecD defs -> RecD (List.map (t_def env) defs) @@ -164,62 +163,88 @@ let rec t_def' env = function RelD (id, mixop, typ, List.map (t_rule env) rules) | def -> def -and t_def env (def : def) = { def with it = t_def' env def.it } +and t_def env (def : def) = {def with it = t_def' env def.it} (* Step 2 and 3: Traverse definitions, collect type information, insert as soon as possible *) -let rec add_type_info env (def : def) = match def.it with +let rec add_type_info env (def : def) = + match def.it with | RecD defs -> List.iter (add_type_info env) defs - | SynD (id, deftyp) -> - begin match deftyp.it with + | SynD (id, deftyp) -> begin + match deftyp.it with | VariantT cases -> register_variant env id cases | AliasT {it = VarT id2; _} -> register_alias env id id2 | _ -> () - end - | _ ->() + end + | _ -> () let is_ready env (t1, t2) = M.mem t1.it env.typ && M.mem t2.it env.typ (* Returns type pairs that are defined now, and removes them from the env *) let ready_pairs (env : env) = - let (ready, todo) = S.partition (is_ready env) env.pairs in + let ready, todo = S.partition (is_ready env) env.pairs in env.pairs <- todo; S.elements ready - let insert_injections env (def : def) : def list = add_type_info env def; let pairs = ready_pairs env in - [ def ] @ - List.map (fun (sub, sup) -> - let name = injection_name sub sup in - let sub_ty = VarT sub $ no_region in - let sup_ty = VarT sup $ no_region in - let (real_id, cases) = lookup env sub in - let clauses = List.map (fun (a, arg_typ, _hints) -> - match arg_typ.it with - | TupT ts -> - let binds = List.mapi (fun i arg_typ_i -> ("x" ^ string_of_int i $ no_region, arg_typ_i, [])) ts in - let xes = List.map (fun (x, arg_typ_i, _) -> VarE x $$ no_region % arg_typ_i) binds in - let xe = TupE xes $$ no_region % arg_typ in - DefD (binds, - CaseE (a, xe) $$ no_region % (VarT real_id $ no_region), - CaseE (a, xe) $$ no_region % sup_ty, []) $ no_region - | _ -> - let x = "x" $ no_region in - let xe = VarE x $$ no_region % arg_typ in - DefD ([(x, arg_typ, [])], - CaseE (a, xe) $$ no_region % (VarT real_id $ no_region), - CaseE (a, xe) $$ no_region % sup_ty, []) $ no_region - ) cases in - DecD (name, sub_ty, sup_ty, clauses) $ no_region - ) pairs - + [def] + @ List.map + (fun (sub, sup) -> + let name = injection_name sub sup in + let sub_ty = VarT sub $ no_region in + let sup_ty = VarT sup $ no_region in + let real_id, cases = lookup env sub in + let clauses = + List.map + (fun (a, arg_typ, _hints) -> + match arg_typ.it with + | TupT ts -> + let binds = + List.mapi + (fun i arg_typ_i -> + ("x" ^ string_of_int i $ no_region, arg_typ_i, []) + ) + ts + in + let xes = + List.map + (fun (x, arg_typ_i, _) -> VarE x $$ no_region % arg_typ_i) + binds + in + let xe = TupE xes $$ no_region % arg_typ in + DefD + ( binds, + CaseE (a, xe) $$ no_region % (VarT real_id $ no_region), + CaseE (a, xe) $$ no_region % sup_ty, + [] + ) + $ no_region + | _ -> + let x = "x" $ no_region in + let xe = VarE x $$ no_region % arg_typ in + DefD + ( [(x, arg_typ, [])], + CaseE (a, xe) $$ no_region % (VarT real_id $ no_region), + CaseE (a, xe) $$ no_region % sup_ty, + [] + ) + $ no_region + ) + cases + in + DecD (name, sub_ty, sup_ty, clauses) $ no_region + ) + pairs let transform (defs : script) = let env = new_env () in let defs' = List.map (t_def env) defs in let defs'' = List.concat_map (insert_injections env) defs' in - S.iter (fun (sub, sup) -> error sub.at ("left-over subtype coercion " ^ sub.it ^ " <: " ^ sup.it)) env.pairs; + S.iter + (fun (sub, sup) -> + error sub.at ("left-over subtype coercion " ^ sub.it ^ " <: " ^ sup.it) + ) + env.pairs; defs'' - diff --git a/spectec/src/middlend/totalize.ml b/spectec/src/middlend/totalize.ml index 7f3c9ed9e7..8b481baafb 100644 --- a/spectec/src/middlend/totalize.ml +++ b/spectec/src/middlend/totalize.ml @@ -12,7 +12,7 @@ The declarations are changed: All calls to such functions are wrapped in option projection `THE e`. -*) + *) open Util open Source @@ -24,19 +24,14 @@ let _error at msg = Source.error at "totalize" msg (* Environment *) -module S = Set.Make(String) +module S = Set.Make (String) -type env = - { mutable partial_funs : S.t; - } - -let new_env () : env = - { partial_funs = S.empty; - } +type env = {mutable partial_funs : S.t} +let new_env () : env = {partial_funs = S.empty} let is_partial (env : env) (id : id) = S.mem id.it env.partial_funs -let register_partial (env : env) (id :id) = +let register_partial (env : env) (id : id) = env.partial_funs <- S.add id.it env.partial_funs (* Transformation *) @@ -49,7 +44,7 @@ let rec t_exp env exp = {exp' with it = TheE {exp' with note = IterT (exp'.note, Opt) $ exp'.at}} | _ -> exp' -and t_exp2 env x = { x with it = t_exp' env x.it } +and t_exp2 env x = {x with it = t_exp' env x.it} (* Expr traversal *) and t_exp' env = function @@ -58,10 +53,13 @@ and t_exp' env = function | BinE (binop, exp1, exp2) -> BinE (binop, t_exp env exp1, t_exp env exp2) | CmpE (cmpop, exp1, exp2) -> CmpE (cmpop, t_exp env exp1, t_exp env exp2) | IdxE (exp1, exp2) -> IdxE (t_exp env exp1, t_exp env exp2) - | SliceE (exp1, exp2, exp3) -> SliceE (t_exp env exp1, t_exp env exp2, t_exp env exp3) - | UpdE (exp1, path, exp2) -> UpdE (t_exp env exp1, t_path env path, t_exp env exp2) - | ExtE (exp1, path, exp2) -> ExtE (t_exp env exp1, t_path env path, t_exp env exp2) - | StrE fields -> StrE (List.map (fun (a, e) -> a, t_exp env e) fields) + | SliceE (exp1, exp2, exp3) -> + SliceE (t_exp env exp1, t_exp env exp2, t_exp env exp3) + | UpdE (exp1, path, exp2) -> + UpdE (t_exp env exp1, t_path env path, t_exp env exp2) + | ExtE (exp1, path, exp2) -> + ExtE (t_exp env exp1, t_path env path, t_exp env exp2) + | StrE fields -> StrE (List.map (fun (a, e) -> (a, t_exp env e)) fields) | DotE (e, a) -> DotE (t_exp env e, a) | CompE (exp1, exp2) -> CompE (t_exp env exp1, t_exp env exp2) | LenE exp -> LenE exp @@ -77,10 +75,7 @@ and t_exp' env = function | CaseE (a, e) -> CaseE (a, t_exp env e) | SubE (e, t1, t2) -> SubE (e, t1, t2) -and t_iter env = function - | ListN e -> ListN (t_exp env e) - | i -> i - +and t_iter env = function ListN e -> ListN (t_exp env e) | i -> i and t_iterexp env (iter, vs) = (t_iter env iter, vs) and t_path' env = function @@ -89,7 +84,7 @@ and t_path' env = function | SliceP (path, e1, e2) -> SliceP (t_path env path, t_exp env e1, t_exp env e2) | DotP (path, a) -> DotP (t_path env path, a) -and t_path env x = { x with it = t_path' env x.it } +and t_path env x = {x with it = t_path' env x.it} let rec t_prem' env = function | RulePr (id, mixop, exp) -> RulePr (id, mixop, t_exp env exp) @@ -97,46 +92,58 @@ let rec t_prem' env = function | ElsePr -> ElsePr | IterPr (prem, iterexp) -> IterPr (t_prem env prem, t_iterexp env iterexp) -and t_prem env x = { x with it = t_prem' env x.it } +and t_prem env x = {x with it = t_prem' env x.it} let t_prems env = List.map (t_prem env) let t_clause' env = function - | DefD (binds, lhs, rhs, prems) -> - DefD (binds, t_exp env lhs, t_exp env rhs, t_prems env prems) + | DefD (binds, lhs, rhs, prems) -> + DefD (binds, t_exp env lhs, t_exp env rhs, t_prems env prems) -let t_clause env (clause : clause) = { clause with it = t_clause' env clause.it } +let t_clause env (clause : clause) = {clause with it = t_clause' env clause.it} let t_rule' env = function | RuleD (id, binds, mixop, exp, prems) -> RuleD (id, binds, mixop, t_exp env exp, t_prems env prems) -let t_rule env x = { x with it = t_rule' env x.it } +let t_rule env x = {x with it = t_rule' env x.it} let rec t_def' env = function | RecD defs -> RecD (List.map (t_def env) defs) | DecD (id, typ1, typ2, clauses) -> let clauses' = List.map (t_clause env) clauses in - if is_partial env id - then + if is_partial env id then let typ2' = IterT (typ2, Opt) $ no_region in - let clauses'' = List.map (fun clause -> match clause.it with - DefD (binds, lhs, rhs, prems) -> - { clause with - it = DefD (binds, lhs, OptE (Some rhs) $$ no_region % typ2', prems) } - ) clauses' in + let clauses'' = + List.map + (fun clause -> + match clause.it with + | DefD (binds, lhs, rhs, prems) -> + { clause with + it = + DefD (binds, lhs, OptE (Some rhs) $$ no_region % typ2', prems) + } + ) + clauses' + in let x = "x" $ no_region in - let catch_all = DefD ([(x, typ1, [])], VarE x $$ no_region % typ1, - OptE None $$ no_region % typ2', []) $ no_region in - DecD (id, typ1, typ2', clauses'' @ [ catch_all ]) + let catch_all = + DefD + ( [(x, typ1, [])], + VarE x $$ no_region % typ1, + OptE None $$ no_region % typ2', + [] + ) + $ no_region + in + DecD (id, typ1, typ2', clauses'' @ [catch_all]) else DecD (id, typ1, typ2, clauses') | RelD (id, mixop, typ, rules) -> RelD (id, mixop, typ, List.map (t_rule env) rules) | (SynD _ | HintD _) as def -> def -and t_def env x = { x with it = t_def' env x.it } - +and t_def env x = {x with it = t_def' env x.it} let is_partial_hint hint = hint.hintid.it = "partial" @@ -150,4 +157,3 @@ let transform (defs : script) = let env = new_env () in List.iter (register_hints env) defs; List.map (t_def env) defs - diff --git a/spectec/src/middlend/unthe.ml b/spectec/src/middlend/unthe.ml index 47eb9ccab0..f6709883e3 100644 --- a/spectec/src/middlend/unthe.ml +++ b/spectec/src/middlend/unthe.ml @@ -19,8 +19,8 @@ let error at msg = Source.error at "sideconditions" msg (* We pull out fresh variables and equating side conditions. *) -type bind = (id * typ * iter list) -type eqn = (bind * premise) +type bind = id * typ * iter list +type eqn = bind * premise type eqns = eqn list (* Fresh name generation *) @@ -29,11 +29,11 @@ let name i = "o" ^ string_of_int i (* no clash avoidance *) let fresh_id (n : int ref) : id = let i = !n in - n := !n+1; + n := !n + 1; name i $ no_region (* If the expression (or premise) under iteration changes, we may be able to -drop some variables from the iterexp *) + drop some variables from the iterexp *) let update_iterexp_vars (sets : Il.Free.sets) ((iter, vs) : iterexp) : iterexp = (iter, List.filter (fun v -> Il.Free.Set.mem v.it sets.varid) vs) @@ -41,46 +41,54 @@ let update_iterexp_vars (sets : Il.Free.sets) ((iter, vs) : iterexp) : iterexp = (* If a bind and premise is generated under an iteration, wrap them accordingly *) let under_iterexp (iter, vs) eqns : iterexp * eqns = - let new_vs = List.map (fun ((v, _, _), _) -> v) eqns in - let iterexp' = (iter, vs @ new_vs) in - let eqns' = List.map (fun ((v, t, is), pr) -> - let pr_iterexp = update_iterexp_vars (Il.Free.free_prem pr) (iter, vs @ new_vs) in - let pr' = IterPr (pr, pr_iterexp) $ no_region in - ((v, t, is@[iter]), pr') - ) eqns in - iterexp', eqns' - + let new_vs = List.map (fun ((v, _, _), _) -> v) eqns in + let iterexp' = (iter, vs @ new_vs) in + let eqns' = + List.map + (fun ((v, t, is), pr) -> + let pr_iterexp = + update_iterexp_vars (Il.Free.free_prem pr) (iter, vs @ new_vs) + in + let pr' = IterPr (pr, pr_iterexp) $ no_region in + ((v, t, is @ [iter]), pr') + ) + eqns + in + (iterexp', eqns') (* Generic traversal helpers *) type 'a traversal = int ref -> 'a -> eqns * 'a type ('a, 'b) traversal_k = int ref -> 'a -> ('a -> 'b) -> eqns * 'b -let phrase (t : 'a traversal) : ('a, 'b) note_phrase traversal - = fun n x -> let eqns, x' = t n x.it in eqns, x' $$ x.at % x.note +let phrase (t : 'a traversal) : ('a, 'b) note_phrase traversal = + fun n x -> + let eqns, x' = t n x.it in + (eqns, x' $$ x.at % x.note) -let t_list (t : 'a traversal) : ('a list, 'b) traversal_k - = fun n xs k -> - let eqnss, xs' = List.split (List.map (t n) xs) in - List.concat eqnss, k xs' +let t_list (t : 'a traversal) : ('a list, 'b) traversal_k = + fun n xs k -> + let eqnss, xs' = List.split (List.map (t n) xs) in + (List.concat eqnss, k xs') let unary (t : 'a traversal) : ('a, 'b) traversal_k = - fun n x k -> + fun n x k -> let eqns, exp' = t n x in - eqns, k exp' + (eqns, k exp') let binary (t1 : 'a traversal) (t2 : 'b traversal) : ('a * 'b, 'c) traversal_k = - fun n (x1, x2) k -> + fun n (x1, x2) k -> let eqns1, x1' = t1 n x1 in let eqns2, x2' = t2 n x2 in - eqns1 @ eqns2, k (x1', x2') + (eqns1 @ eqns2, k (x1', x2')) -let ternary (t1 : 'a traversal) (t2 : 'b traversal) (t3 : 'c traversal) : ('a * 'b * 'c, 'd) traversal_k = - fun n (x1, x2, x3) k -> +let ternary (t1 : 'a traversal) (t2 : 'b traversal) (t3 : 'c traversal) : + ('a * 'b * 'c, 'd) traversal_k = + fun n (x1, x2, x3) k -> let eqns1, x1' = t1 n x1 in let eqns2, x2' = t2 n x2 in let eqns3, x3' = t3 n x3 in - eqns1 @ eqns2 @ eqns3, k (x1', x2', x3') + (eqns1 @ eqns2 @ eqns3, k (x1', x2', x3')) (* Expr traversal *) @@ -88,25 +96,29 @@ let rec t_exp n e : eqns * exp = (* Descend first using t_exp2, and then see if we have to pull out the current expression *) let eqns, e' = t_exp2 n e in match e.it with - | TheE exp -> + | TheE exp -> let ot = exp.note in - let t = match ot.it with + let t = + match ot.it with | IterT (t, Opt) -> t | _ -> error exp.at "Expected option type in TheE" in let x = fresh_id n in let xe = VarE x $$ no_region % t in let bind = (x, t, []) in - let prem = IfPr ( - CmpE (EqOp, exp, OptE (Some xe) $$ no_region % ot) $$ no_region % (BoolT $ no_region) - ) $ no_region in - eqns @ [(bind, prem)], xe - | _ -> eqns, e' + let prem = + IfPr + (CmpE (EqOp, exp, OptE (Some xe) $$ no_region % ot) + $$ no_region % (BoolT $ no_region) + ) + $ no_region + in + (eqns @ [(bind, prem)], xe) + | _ -> (eqns, e') (* Traversal helpers *) and t_exp2 n = phrase t_exp' n - and t_e n x k = unary t_exp n x k and t_ee n x k = binary t_exp t_exp n x k and t_eee n x k = ternary t_exp t_exp t_exp n x k @@ -114,96 +126,95 @@ and t_epe n x k = ternary t_exp t_path t_exp n x k and t_exp' n e : eqns * exp' = match e with - | VarE _ | BoolE _ | NatE _ | TextE _ | OptE None -> [], e - + | VarE _ | BoolE _ | NatE _ | TextE _ | OptE None -> ([], e) | UnE (uo, exp) -> t_e n exp (fun exp' -> UnE (uo, exp')) | DotE (exp, a) -> t_e n exp (fun exp' -> DotE (exp', a)) | LenE exp -> t_e n exp (fun exp' -> LenE exp') | MixE (mo, exp) -> t_e n exp (fun exp' -> MixE (mo, exp')) - | CallE (f, exp) ->t_e n exp (fun exp' -> CallE (f, exp')) - | OptE (Some exp) ->t_e n exp (fun exp' -> OptE (Some exp')) - | TheE exp ->t_e n exp (fun exp' -> TheE exp') - | CaseE (a, exp) ->t_e n exp (fun exp' -> CaseE (a, exp')) + | CallE (f, exp) -> t_e n exp (fun exp' -> CallE (f, exp')) + | OptE (Some exp) -> t_e n exp (fun exp' -> OptE (Some exp')) + | TheE exp -> t_e n exp (fun exp' -> TheE exp') + | CaseE (a, exp) -> t_e n exp (fun exp' -> CaseE (a, exp')) | SubE (exp, a, b) -> t_e n exp (fun exp' -> SubE (exp', a, b)) - - | BinE (bo, exp1, exp2) -> t_ee n (exp1, exp2) (fun (e1', e2') -> BinE (bo, e1', e2')) - | CmpE (co, exp1, exp2) -> t_ee n (exp1, exp2) (fun (e1', e2') -> CmpE (co, e1', e2')) + | BinE (bo, exp1, exp2) -> + t_ee n (exp1, exp2) (fun (e1', e2') -> BinE (bo, e1', e2')) + | CmpE (co, exp1, exp2) -> + t_ee n (exp1, exp2) (fun (e1', e2') -> CmpE (co, e1', e2')) | IdxE (exp1, exp2) -> t_ee n (exp1, exp2) (fun (e1', e2') -> IdxE (e1', e2')) - | CompE (exp1, exp2) -> t_ee n (exp1, exp2) (fun (e1', e2') -> CompE (e1', e2')) + | CompE (exp1, exp2) -> + t_ee n (exp1, exp2) (fun (e1', e2') -> CompE (e1', e2')) | CatE (exp1, exp2) -> t_ee n (exp1, exp2) (fun (e1', e2') -> CatE (e1', e2')) - - | SliceE (exp1, exp2, exp3) -> t_eee n (exp1, exp2, exp3) (fun (e1', e2', e3') -> SliceE (e1', e2', e3')) - - | UpdE (exp1, path, exp2) -> t_epe n (exp1, path, exp2) (fun (e1', p', e2') -> UpdE (e1', p', e2')) - | ExtE (exp1, path, exp2) -> t_epe n (exp1, path, exp2) (fun (e1', p', e2') -> ExtE (e1', p', e2')) - + | SliceE (exp1, exp2, exp3) -> + t_eee n (exp1, exp2, exp3) (fun (e1', e2', e3') -> SliceE (e1', e2', e3')) + | UpdE (exp1, path, exp2) -> + t_epe n (exp1, path, exp2) (fun (e1', p', e2') -> UpdE (e1', p', e2')) + | ExtE (exp1, path, exp2) -> + t_epe n (exp1, path, exp2) (fun (e1', p', e2') -> ExtE (e1', p', e2')) | StrE fields -> t_list t_field n fields (fun fields' -> StrE fields') - | TupE es -> t_list t_exp n es (fun es' -> TupE es') | ListE es -> t_list t_exp n es (fun es' -> ListE es') - | IterE (e, iterexp) -> let eqns1, e' = t_exp n e in let iterexp', eqns1' = under_iterexp iterexp eqns1 in let eqns2, iterexp'' = t_iterexp n iterexp' in let iterexp''' = update_iterexp_vars (Il.Free.free_exp e') iterexp'' in - eqns1' @ eqns2, IterE (e', iterexp''') - -and t_field n ((a, e) : expfield) = - unary t_exp n e (fun e' -> (a, e')) + (eqns1' @ eqns2, IterE (e', iterexp''')) -and t_iterexp n (iter, vs) = - unary t_iter n iter (fun iter' -> (iter', vs)) +and t_field n ((a, e) : expfield) = unary t_exp n e (fun e' -> (a, e')) +and t_iterexp n (iter, vs) = unary t_iter n iter (fun iter' -> (iter', vs)) -and t_iter n iter = match iter with +and t_iter n iter = + match iter with | ListN e -> unary t_exp n e (fun e' -> ListN e') - | _ -> [], iter + | _ -> ([], iter) and t_path n = phrase t_path' n -and t_path' n path = match path with - | RootP -> [], path - | IdxP (path, e) -> binary t_path t_exp n (path, e) (fun (path', e') -> IdxP (path', e')) - | SliceP (path, e1, e2) -> ternary t_path t_exp t_exp n (path, e1, e2) (fun (path', e1', e2') -> SliceP (path', e1', e2')) +and t_path' n path = + match path with + | RootP -> ([], path) + | IdxP (path, e) -> + binary t_path t_exp n (path, e) (fun (path', e') -> IdxP (path', e')) + | SliceP (path, e1, e2) -> + ternary t_path t_exp t_exp n (path, e1, e2) (fun (path', e1', e2') -> + SliceP (path', e1', e2') + ) | DotP (path, a) -> unary t_path n path (fun path' -> DotP (path', a)) let rec t_prem n : premise -> eqns * premise = phrase t_prem' n and t_prem' n prem : eqns * premise' = match prem with - | RulePr (a, b, exp) -> - unary t_exp n exp (fun exp' -> RulePr (a, b, exp')) + | RulePr (a, b, exp) -> unary t_exp n exp (fun exp' -> RulePr (a, b, exp')) | IfPr e -> unary t_exp n e (fun e' -> IfPr e') - | ElsePr -> [], prem + | ElsePr -> ([], prem) | IterPr (prem, iterexp) -> let eqns1, prem' = t_prem n prem in let iterexp', eqns1' = under_iterexp iterexp eqns1 in let eqns2, iterexp'' = t_iterexp n iterexp' in let iterexp''' = update_iterexp_vars (Il.Free.free_prem prem') iterexp'' in - eqns1' @ eqns2, IterPr (prem', iterexp''') + (eqns1' @ eqns2, IterPr (prem', iterexp''')) -let t_prems n k = t_list t_prem n k (fun x -> x) +let t_prems n k = t_list t_prem n k (fun x -> x) let t_rule' = function | RuleD (id, binds, mixop, exp, prems) -> (* Counter for fresh variables *) let n = ref 0 in - let eqns, (exp', prems') = binary t_exp t_prems n (exp, prems) (fun x -> x) in + let eqns, (exp', prems') = + binary t_exp t_prems n (exp, prems) (fun x -> x) + in let extra_binds, extra_prems = List.split eqns in RuleD (id, binds @ extra_binds, mixop, exp', extra_prems @ prems') -let t_rule x = { x with it = t_rule' x.it } - +let t_rule x = {x with it = t_rule' x.it} let t_rules = List.map t_rule let rec t_def' = function | RecD defs -> RecD (List.map t_def defs) - | RelD (id, mixop, typ, rules) -> - RelD (id, mixop, typ, t_rules rules) + | RelD (id, mixop, typ, rules) -> RelD (id, mixop, typ, t_rules rules) | def -> def -and t_def x = { x with it = t_def' x.it } - -let transform (defs : script) = - List.map t_def defs +and t_def x = {x with it = t_def' x.it} +let transform (defs : script) = List.map t_def defs diff --git a/spectec/src/util/dune b/spectec/src/util/dune index 835dff1b25..c4af67bf4e 100644 --- a/spectec/src/util/dune +++ b/spectec/src/util/dune @@ -1,4 +1,3 @@ (library - (name util) - (modules lib utf8 scc source) -) + (name util) + (modules lib utf8 scc source)) diff --git a/spectec/src/util/lib.ml b/spectec/src/util/lib.ml index e681b2beef..b143a24bf4 100644 --- a/spectec/src/util/lib.ml +++ b/spectec/src/util/lib.ml @@ -1,23 +1,21 @@ -module List = -struct +module List = struct include List - let split_hd = function - | x::xs -> x, xs - | _ -> failwith "split_hd" + let split_hd = function x :: xs -> (x, xs) | _ -> failwith "split_hd" let rec split_last = function - | x::[] -> [], x - | x::xs -> let ys, y = split_last xs in x::ys, y + | x :: [] -> ([], x) + | x :: xs -> + let ys, y = split_last xs in + (x :: ys, y) | [] -> failwith "split_last" let rec nub pred = function | [] -> [] - | x::xs -> x :: nub pred (List.filter (fun y -> not (pred x y)) xs) + | x :: xs -> x :: nub pred (List.filter (fun y -> not (pred x y)) xs) end -module String = -struct +module String = struct include String let implode cs = @@ -27,6 +25,8 @@ struct let explode s = let cs = ref [] in - for i = String.length s - 1 downto 0 do cs := s.[i] :: !cs done; + for i = String.length s - 1 downto 0 do + cs := s.[i] :: !cs + done; !cs end diff --git a/spectec/src/util/lib.mli b/spectec/src/util/lib.mli index 873e2e9f3c..6e8c76dced 100644 --- a/spectec/src/util/lib.mli +++ b/spectec/src/util/lib.mli @@ -1,14 +1,12 @@ (* Things that should be in the OCaml library... *) -module List : -sig +module List : sig val split_hd : 'a list -> 'a * 'a list (* raises Failure *) val split_last : 'a list -> 'a list * 'a (* raises Failure *) val nub : ('a -> 'a -> bool) -> 'a list -> 'a list end -module String : -sig +module String : sig val implode : char list -> string val explode : string -> char list end diff --git a/spectec/src/util/scc.ml b/spectec/src/util/scc.ml index 9b02969370..0a5c4e8e7f 100644 --- a/spectec/src/util/scc.ml +++ b/spectec/src/util/scc.ml @@ -9,59 +9,55 @@ type vert = int array type graph = vert array -module Set = Set.Make(Int) - +module Set = Set.Make (Int) (* SCC *) -type vert_info = - { mutable index : int; - mutable low : int; - mutable onstack : bool; - } +type vert_info = {mutable index : int; mutable low : int; mutable onstack : bool} let sccs (graph : graph) : Set.t list = let len = Array.length graph in - if len = 0 then [] else - - let info = Array.init len (fun _ -> {index = -1; low = -1; onstack = false}) in - let stack = Array.make len (-1) in - let stack_top = ref 0 in - let index = ref 0 in - let sccs = ref [] in - - let rec connect x = - stack.(!stack_top) <- x; - incr stack_top; - let v = info.(x) in - v.onstack <- true; - v.index <- !index; - v.low <- !index; - incr index; - visit v graph.(x); - if v.low = v.index then sccs := scc x Set.empty :: !sccs - - and scc x ys = - decr stack_top; - let y = stack.(!stack_top) in - info.(y).onstack <- false; - let ys' = Set.add y ys in - if x = y then ys' else scc x ys' - - and visit v vert = - let succs = vert in - for i = 0 to Array.length succs - 1 do - let x = succs.(i) in - let w = info.(x) in - if w.index = -1 then begin - connect x; - v.low <- min v.low w.low - end else if w.onstack then - v.low <- min v.low w.index - done - in - - for x = 0 to len - 1 do - if info.(x).index = -1 then connect x - done; - List.rev !sccs + if len = 0 then + [] + else + let info = + Array.init len (fun _ -> {index = -1; low = -1; onstack = false}) + in + let stack = Array.make len (-1) in + let stack_top = ref 0 in + let index = ref 0 in + let sccs = ref [] in + + let rec connect x = + stack.(!stack_top) <- x; + incr stack_top; + let v = info.(x) in + v.onstack <- true; + v.index <- !index; + v.low <- !index; + incr index; + visit v graph.(x); + if v.low = v.index then sccs := scc x Set.empty :: !sccs + and scc x ys = + decr stack_top; + let y = stack.(!stack_top) in + info.(y).onstack <- false; + let ys' = Set.add y ys in + if x = y then ys' else scc x ys' + and visit v vert = + let succs = vert in + for i = 0 to Array.length succs - 1 do + let x = succs.(i) in + let w = info.(x) in + if w.index = -1 then begin + connect x; + v.low <- min v.low w.low + end else if w.onstack then + v.low <- min v.low w.index + done + in + + for x = 0 to len - 1 do + if info.(x).index = -1 then connect x + done; + List.rev !sccs diff --git a/spectec/src/util/source.ml b/spectec/src/util/source.ml index 8bdd8fcdc2..0d85df62ad 100644 --- a/spectec/src/util/source.ml +++ b/spectec/src/util/source.ml @@ -5,17 +5,15 @@ type region = {left : pos; right : pos} let no_pos = {file = ""; line = 0; column = 0} let no_region = {left = no_pos; right = no_pos} - let pos_of_file file = {no_pos with file} let region_of_file file = {left = pos_of_file file; right = pos_of_file file} let over_region = function | [] -> raise (Invalid_argument "Source.over") - | r::rs -> - List.fold_left (fun r1 r2 -> - {left = min r1.left r2.left; right = max r1.right r2.right} - ) r rs - + | r :: rs -> + List.fold_left + (fun r1 r2 -> {left = min r1.left r2.left; right = max r1.right r2.right}) + r rs let string_of_pos pos = if pos.line = -1 then @@ -27,24 +25,23 @@ let string_of_region r = if r = region_of_file r.left.file then r.left.file else - r.left.file ^ ":" ^ string_of_pos r.left ^ - (if r.left = r.right then "" else "-" ^ string_of_pos r.right) - + r.left.file + ^ ":" + ^ string_of_pos r.left + ^ if r.left = r.right then "" else "-" ^ string_of_pos r.right (* Phrases *) type ('a, 'b) note_phrase = {at : region; it : 'a; note : 'b} type 'a phrase = ('a, unit) note_phrase -let ($) it at = {it; at; note = ()} -let ($$) it (at, note) = {it; at; note} -let (%) at note = (at, note) - +let ( $ ) it at = {it; at; note = ()} +let ( $$ ) it (at, note) = {it; at; note} +let ( % ) at note = (at, note) let it {it; _} = it let at {at; _} = at let note {note; _} = note - (* Errors *) exception Error of region * string diff --git a/spectec/src/util/source.mli b/spectec/src/util/source.mli index 33d8205d5c..404488483b 100644 --- a/spectec/src/util/source.mli +++ b/spectec/src/util/source.mli @@ -6,22 +6,18 @@ type region = {left : pos; right : pos} val no_pos : pos val no_region : region val region_of_file : string -> region - val over_region : region list -> region - val string_of_pos : pos -> string val string_of_region : region -> string - (* Phrases *) type ('a, 'b) note_phrase = {at : region; it : 'a; note : 'b} type 'a phrase = ('a, unit) note_phrase -val ($) : 'a -> region -> 'a phrase -val ($$) : 'a -> region * 'b -> ('a, 'b) note_phrase -val (%) : region -> 'b -> region * 'b - +val ( $ ) : 'a -> region -> 'a phrase +val ( $$ ) : 'a -> region * 'b -> ('a, 'b) note_phrase +val ( % ) : region -> 'b -> region * 'b val it : ('a, 'b) note_phrase -> 'a val at : ('a, 'b) note_phrase -> region val note : ('a, 'b) note_phrase -> 'b diff --git a/spectec/src/util/utf8.ml b/spectec/src/util/utf8.ml index 4a2260b90c..f971c5cf5d 100644 --- a/spectec/src/util/utf8.ml +++ b/spectec/src/util/utf8.ml @@ -6,40 +6,42 @@ exception Utf8 let con n = 0x80 lor (n land 0x3f) let rec encode ns = Lib.String.implode (List.map Char.chr (encode' ns)) + and encode' = function | [] -> [] - | n::_ns when n < 0 -> - raise Utf8 - | n::ns when n < 0x80 -> - n :: encode' ns - | n::ns when n < 0x800 -> - 0xc0 lor (n lsr 6) :: con n :: encode' ns - | n::ns when n < 0x10000 -> - 0xe0 lor (n lsr 12) :: con (n lsr 6) :: con n :: encode' ns - | n::ns when n < 0x110000 -> - 0xf0 lor (n lsr 18) :: con (n lsr 12) :: con (n lsr 6) :: con n + | n :: _ns when n < 0 -> raise Utf8 + | n :: ns when n < 0x80 -> n :: encode' ns + | n :: ns when n < 0x800 -> (0xc0 lor (n lsr 6)) :: con n :: encode' ns + | n :: ns when n < 0x10000 -> + (0xe0 lor (n lsr 12)) :: con (n lsr 6) :: con n :: encode' ns + | n :: ns when n < 0x110000 -> + (0xf0 lor (n lsr 18)) + :: con (n lsr 12) + :: con (n lsr 6) + :: con n :: encode' ns - | _ -> - raise Utf8 + | _ -> raise Utf8 let con b = if b land 0xc0 = 0x80 then b land 0x3f else raise Utf8 + let code min n = - if n < min || (0xd800 <= n && n < 0xe000) || n >= 0x110000 then raise Utf8 - else n + if n < min || (0xd800 <= n && n < 0xe000) || n >= 0x110000 then + raise Utf8 + else + n let rec decode s = decode' (List.map Char.code (Lib.String.explode s)) + and decode' = function | [] -> [] - | b1::bs when b1 < 0x80 -> - code 0x0 b1 :: decode' bs - | b1::_bs when b1 < 0xc0 -> - raise Utf8 - | b1::b2::bs when b1 < 0xe0 -> - code 0x80 ((b1 land 0x1f) lsl 6 + con b2) :: decode' bs - | b1::b2::b3::bs when b1 < 0xf0 -> - code 0x800 ((b1 land 0x0f) lsl 12 + con b2 lsl 6 + con b3) :: decode' bs - | b1::b2::b3::b4::bs when b1 < 0xf8 -> - code 0x10000 ((b1 land 0x07) lsl 18 + con b2 lsl 12 + con b3 lsl 6 + con b4) + | b1 :: bs when b1 < 0x80 -> code 0x0 b1 :: decode' bs + | b1 :: _bs when b1 < 0xc0 -> raise Utf8 + | b1 :: b2 :: bs when b1 < 0xe0 -> + code 0x80 (((b1 land 0x1f) lsl 6) + con b2) :: decode' bs + | b1 :: b2 :: b3 :: bs when b1 < 0xf0 -> + code 0x800 (((b1 land 0x0f) lsl 12) + (con b2 lsl 6) + con b3) :: decode' bs + | b1 :: b2 :: b3 :: b4 :: bs when b1 < 0xf8 -> + code 0x10000 + (((b1 land 0x07) lsl 18) + (con b2 lsl 12) + (con b3 lsl 6) + con b4) :: decode' bs - | _ -> - raise Utf8 + | _ -> raise Utf8 diff --git a/spectec/test-frontend/dune b/spectec/test-frontend/dune index 47035d055b..301f210f82 100644 --- a/spectec/test-frontend/dune +++ b/spectec/test-frontend/dune @@ -1,8 +1,6 @@ (mdx - (libraries spectec) - (deps - (file ../src/exe-watsup/main.exe) - (glob_files ../spec/*.watsup) - ) - (files TEST.md) -) + (libraries spectec) + (deps + (file ../src/exe-watsup/main.exe) + (glob_files ../spec/*.watsup)) + (files TEST.md)) diff --git a/spectec/test-latex/dune b/spectec/test-latex/dune index a0c9411b6a..c94cb5b8ba 100644 --- a/spectec/test-latex/dune +++ b/spectec/test-latex/dune @@ -1,9 +1,7 @@ (mdx - (libraries spectec) - (deps - (file ../src/exe-watsup/main.exe) - (glob_files ../spec/*.watsup) - (file spec-splice-in.tex) - ) - (files TEST.md) -) + (libraries spectec) + (deps + (file ../src/exe-watsup/main.exe) + (glob_files ../spec/*.watsup) + (file spec-splice-in.tex)) + (files TEST.md)) diff --git a/spectec/test-middlend/dune b/spectec/test-middlend/dune index 47035d055b..301f210f82 100644 --- a/spectec/test-middlend/dune +++ b/spectec/test-middlend/dune @@ -1,8 +1,6 @@ (mdx - (libraries spectec) - (deps - (file ../src/exe-watsup/main.exe) - (glob_files ../spec/*.watsup) - ) - (files TEST.md) -) + (libraries spectec) + (deps + (file ../src/exe-watsup/main.exe) + (glob_files ../spec/*.watsup)) + (files TEST.md)) diff --git a/spectec/test-prose/dune b/spectec/test-prose/dune index 47035d055b..301f210f82 100644 --- a/spectec/test-prose/dune +++ b/spectec/test-prose/dune @@ -1,8 +1,6 @@ (mdx - (libraries spectec) - (deps - (file ../src/exe-watsup/main.exe) - (glob_files ../spec/*.watsup) - ) - (files TEST.md) -) + (libraries spectec) + (deps + (file ../src/exe-watsup/main.exe) + (glob_files ../spec/*.watsup)) + (files TEST.md))