Stefan pushed to branch master at Stefan / Typer

Commits: 02dabd43 by Stefan Monnier at 2016-11-28T10:01:45-05:00 Use ##... for types. Don't use `Macro` for special forms

* btl/unit.typer, btl/list.typer, btl/macro.typer: Remove, unused. * btl/builtins.typer: Rename from types.typer. (Unit): Define as inductive, rather than builtin. (unit): New predefined constant. (Int, Float, String, Sexp, Context, IO, FileHandle, Attribute): Remove built-in types, now declared in OCaml. (new-attribute, get-attribute, has-attribute, add-attribute, decltype) (declexpr): Remove special forms, now declared in OCaml.

* src/builtin.ml (predef_name): Remove "Attribute", unused. (add_builtin_type): New function. Add all builtin sorts and types.

* src/debruijn.ml (sort_level): Rename from type_level. (sort_omega): Rename from type_omega. (type_level): New type.

* src/lparse.ml (macromap): Move. (special_forms): Rename from make_macro_map; make it a ref cell rather than a function of no arguments. (type_special_form): New built-in type. (add_special_form): New function. (get_special_form): Rename from get_macro_impl, rewrite. (infer_call.handle_funcall): Use mkBuiltin. Remove the single-arg form of `Built-in`. (infer_call): Don't use the `Macro` to indicate a special form. (builtin_macro, is_builtin_macro): Remove. (<toplevel>): Register special forms. (default_lctx): Add entries predefined in BI.lmap. before loading types.typer.

* src/opslexp.ml (conv_p) <Inductive>: Fix scoping of fields. (sort_level_max): Hash-cons return value. (check'): Check the type provided to `Builtin`. Hash cons the sorts as well. (erase_type): Silence compiler warning.

- - - - -

9 changed files:

- btl/types.typer → btl/builtins.typer - − btl/list.typer - − btl/macro.typer - − btl/unit.typer - src/builtin.ml - src/debruijn.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml

Changes:

===================================== btl/types.typer → btl/builtins.typer ===================================== --- a/btl/types.typer +++ b/btl/builtins.typer @@ -35,13 +35,8 @@ % Base Types % -----------------------------------------------------

-Int = Built-in "Int"; -Float = Built-in "Float"; -String = Built-in "String"; -Sexp = Built-in "Sexp"; - -Unit = Built-in "Unit"; % Nothing -Context = Built-in "Context"; % Lexp Context +Unit = inductive_ Unit unit; +unit = inductive-cons Unit unit;

% Basic operators _+_ = Built-in "_+_" (Int -> Int -> Int); @@ -145,8 +140,6 @@ sexp_dispatch_ = Built-in "sexp_dispatch_" ( % Monads % -----------------------------------------------------

-IO = Built-in "IO" (Type -> Type); - % Builtin bind bind = Built-in "bind" ( (a : Type) ≡> @@ -157,9 +150,6 @@ bind = Built-in "bind" (

% File monad

-% define a dummy type that supposed to represent a file -FileHandle = Built-in "FileHandle"; - %% `runIO` should have type IO Unit -> b -> b %% or IO a -> b -> b, which means "run the IO, throw away the result, %% and then return the second argument unchanged". The "dummy" b argument @@ -172,29 +162,3 @@ run-io = Built-in "run-io" ((a : Type) ≡> IO Unit -> a -> a); open = Built-in "open" (String -> String -> IO FileHandle); write = Built-in "write" (FileHandle -> String -> IO Unit); read = Built-in "read" (FileHandle -> Int -> IO String); - -% ----------------------------------------------------- -% Attributes -% ----------------------------------------------------- - -% Despite being typed as macro those actually returns lexp. -% not that it matters for the end user -Attribute = Built-in "Attribute"; -new-attribute = Built-in "new-attribute" Macro; -get-attribute = Built-in "get-attribute" Macro; -has-attribute = Built-in "has-attribute" Macro; -add-attribute = Built-in "add-attribute" Macro; - -% attribute = Macro_ add-attribute; - -% ----------------------------------------------------- -% Context Accessors -% ----------------------------------------------------- - -%% FIXME: These should be functions! -decltype = Built-in "decltype" Macro; -declexpr = Built-in "declexpr" Macro; - - - -

===================================== btl/list.typer deleted ===================================== --- a/btl/list.typer +++ /dev/null @@ -1,26 +0,0 @@ -List : Type -> Type; -List = inductive_ (dList (a : Type)) (nil) (cons a (List a)); - -nil = inductive-cons List nil; -cons = inductive-cons List cons; - -length : (a : Type) => List a -> Int; -length = lambda a => - lambda xs -> - case xs - | nil => 0 - | cons hd tl => (1 + length tl); - -head : (a : Type) => List a -> a; -head = lambda a => - lambda xs -> - case xs - | nil => nil - | cons hd tl => hd; - -tail : (a : Type) => List a -> List a; -tail = lambda a => - lambda xs -> - case xs - | nil => nil - | cons hd tl => tl;

===================================== btl/macro.typer deleted ===================================== --- a/btl/macro.typer +++ /dev/null @@ -1,36 +0,0 @@ - - -block_ : (List Sexp) -> Sexp; -block_ = Built-in block_; - -symbol_ : String -> Sexp; -symbol_ = Built-in symbol_; - -string_ : String -> Sexp; -string_ = Built-in string_; - -node_ : (List Sexp) -> Sexp; -node_ = Built-in node_; - -integer_ : Int -> Sexp; -integer_ = Built-in integer_; - -Macro : Type; -Macro = inductive_ (dMacro) (Macro_ Type); -Macro_ = inductive-cons Macro Macro_; - - -%% Basic usage -% -% sqr = (Macro_ -% (node_ (symbol_ "lambda_->_") (symbol "x") -% (node_ "_*_" (symbol "x") (symbol "x")))); -% -% (sqr 4); % <=> 4 * 4 -% -% -%% Using Quasi Quote ` -% -% sqr = (Macro_ (qq (lambda x -> ,x * ,x))); -% -% (sqr 4); % <=> 4 * 4

===================================== btl/unit.typer deleted ===================================== --- a/btl/unit.typer +++ /dev/null @@ -1,5 +0,0 @@ - -% Declare a dummy Type -Unit : Type; -Unit = inductive_ (Unit) (unit); -unit = inductive-cons Unit unit;

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -79,7 +79,6 @@ let predef_name = [ "Macro"; "expand_macro_"; "expand_dmacro_"; - "Attribute"; ]

let default_predef_map : predef_table = @@ -201,3 +200,22 @@ let add_builtin_cst (name : string) (e : lexp) assert (not (SMap.mem name map)); let t = OL.check VMap.empty Myers.nil e in lmap := SMap.add name (e, t) map + +let new_builtin_type name kind = + let t = mkBuiltin ((dloc, name), kind, None) in + add_builtin_cst name t; + t + +let builtins = + add_builtin_cst "TypeLevel" DB.type_level; + add_builtin_cst "TypeLevel.z" DB.level0; + add_builtin_cst "Type" DB.type0; + add_builtin_cst "Type1" DB.type1; + add_builtin_cst "Int" DB.type_int; + add_builtin_cst "Float" DB.type_float; + add_builtin_cst "String" DB.type_string + +let _ = new_builtin_type "Sexp" DB.type0 +let _ = new_builtin_type + "IO" (Arrow (Aexplicit, None, DB.type0, dloc, DB.type0)) +let _ = new_builtin_type "FileHandle" DB.type0

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -79,14 +79,15 @@ let warning = msg_warning "DEBRUIJN" * ---------------------------------- *)

let dloc = dummy_location +let sort_level = mkSort (dloc, StypeLevel) +let sort_omega = mkSort (dloc, StypeOmega) +let type_level = mkBuiltin ((dloc, "TypeLevel"), sort_level, None) let level0 = mkSortLevel SLz let level1 = mkSortLevel (SLsucc level0) let level2 = mkSortLevel (SLsucc level1) let type0 = mkSort (dloc, Stype level0) let type1 = mkSort (dloc, Stype level1) let type2 = mkSort (dloc, Stype level2) -let type_level = mkSort (dloc, StypeLevel) -let type_omega = mkSort (dloc, StypeOmega) let type_int = mkBuiltin ((dloc, "Int"), type0, None) let type_float = mkBuiltin ((dloc, "Float"), type0, None) let type_string = mkBuiltin ((dloc, "String"), type0, None) @@ -291,7 +292,8 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = ret) with Not_found -> error loc ("DeBruijn index " - ^ string_of_int dbi ^ " out of bounds!") + ^ string_of_int dbi ^ " of `" ^ ename + ^ "` out of bounds!")

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -658,9 +658,9 @@ and _lexp_to_str ctx exp =

| Sort (_, Stype (SortLevel SLz)) -> "##Type" | Sort (_, Stype (SortLevel (SLsucc (SortLevel SLz)))) -> "##Type1" - | Sort (_, StypeLevel) -> "##TypeLevel" + | Sort (_, StypeLevel) -> "##Type_ℓ" | Sort (_, Stype _) -> "##Type_?" (* FIXME! *) - | Sort (_, StypeOmega) -> "##Type_ω" (* FIXME: Should never happen! *) + | Sort (_, StypeOmega) -> "##Type_ω"

| SortLevel (SLz) -> "##TypeLevel.z" | SortLevel (SLsucc e) -> "##TypeLevel.succ"

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -89,6 +89,22 @@ let value_fatal = debug_message fatal value_name value_string (* :-( *) let global_substitution = ref (empty_meta_subst, [])

+(** Builtin Macros i.e, special forms. *) +type macromap = + (location -> lexp list -> elab_context -> lexp -> lexp) SMap.t + +let special_forms : macromap ref = ref SMap.empty +let type_special_form = BI.new_builtin_type "Special-Form" type0 + +let add_special_form (name, func) = + BI.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form, None)); + special_forms := SMap.add name func (!special_forms) + +let get_special_form loc name = + try SMap.find name (!special_forms) + with Not_found -> fatal loc ("Special form `" ^ name ^ "` not found!") + + (* The prefix `elab_check_` is used for functions which do internal checking * (i.e. errors signalled here correspond to internal errors rather than * to errors in the user's code). *) @@ -112,10 +128,6 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = ("Type of `" ^ name ^ "` is not a proper type: " ^ typestr)

-(* Builtin Macro i.e, special forms *) -type macromap = - (location -> lexp list -> elab_context -> lexp -> lexp) SMap.t - let elab_check_proper_type (ctx : elab_context) ltp var = let meta_ctx, _ = !global_substitution in try elab_check_sort ctx (OL.check meta_ctx (ectx_to_lctx ctx) ltp) var ltp @@ -778,17 +790,14 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = (* Here we use lexp_whnf on actual code, but it's OK * because we only use the result when it's a "predefined constant". *) match OL.lexp_whnf body (ectx_to_lctx ctx) meta_ctx with - | Builtin((_, "Built-in"), _, _) + | Builtin((_, "Built-in"), _, _) (* FIXME: Should be a Special-Form! *) -> ( (* ------ SPECIAL ------ *) match !_parsing_internals, sargs with - | true, [String (_, str)] -> - Builtin((loc, str), ltp, None), ltp - | true, [String (_, str); stp] -> let ptp = pexp_parse stp in let ltp, _ = infer ptp ctx in - Builtin((loc, str), ltp, None), ltp + mkBuiltin((loc, str), ltp, None), ltp

| true, _ -> error loc "Wrong Usage of `Built-in`"; dlxp, dltype @@ -815,31 +824,32 @@ and infer_call (func: pexp) (sargs: sexp list) ctx = infer pxp ctx in

(* This is the builtin Macro type *) - let macro_type, macro_disp = match BI.get_predef_option "Macro" ctx with - | Some lxp -> OL.lexp_whnf lxp (ectx_to_lctx ctx) meta_ctx, true + let macro_type = match BI.get_predef_option "Macro" ctx with + | Some lxp -> OL.lexp_whnf lxp (ectx_to_lctx ctx) meta_ctx (* When type.typer is being parsed and the predef is not yet available *) - | None -> dltype, false in + | None -> impossible in

(* determine function type *) - match func, ltp with - | macro, _ when (macro_disp - && OL.conv_p meta_ctx (ectx_to_lctx ctx) - ltp macro_type) -> ( - match macro with - | Pvar(l, name) when is_builtin_macro name -> - let pargs = List.map pexp_parse sargs in - let largs = lexp_parse_all pargs ctx in - let e = (get_macro_impl loc name) loc largs ctx ltp in - let meta_ctx, _ = !global_substitution in - (* FIXME: We don't actually need to typecheck `e`, we just need - * to find its type. *) - (e, OL.check meta_ctx (ectx_to_lctx ctx) e) - - (* true macro *) - | _ -> handle_macro_call ()) - - (* FIXME: Handle special-forms here as well! *) - | _ -> handle_funcall () + if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ltp type_special_form) then + match OL.lexp_whnf body (ectx_to_lctx ctx) meta_ctx with + | Builtin ((_, name), _, _) -> + (* Special form. *) + let pargs = List.map pexp_parse sargs in + let largs = lexp_parse_all pargs ctx in + let e = (get_special_form loc name) loc largs ctx ltp in + let meta_ctx, _ = !global_substitution in + (* FIXME: We don't actually need to typecheck `e`, we just need + * to find its type. *) + (e, OL.check meta_ctx (ectx_to_lctx ctx) e) + + | _ -> lexp_error loc body ("Unknown special-form: " + ^ lexp_string body); + let t = newMetatype () in + (newMetavar loc "<dummy>" t, t) + else if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ltp macro_type) then + handle_macro_call () + else + handle_funcall ()

(* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx = @@ -890,22 +900,10 @@ and lexp_expand_macro_ macro_funct sargs ctx expand_fun : value_type = vxp

and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = - try (* Lookup macro declaration *) - let idx = senv_lookup mname ctx in - (* FIXME: We should only check that `ltp` is Macro, and not look - * at `lxp` here (just like we do for expression macros). *) - let ltp = env_lookup_type ctx ((loc, mname), idx) in - let lxp = env_lookup_expr ctx ((loc, mname), idx) in - - (* lxp has the form (Call (Var(_, "Macro_"), [(_, function)])) - * We need the function so we can call it later *) - let body, mfun = match lxp with - | Some (Call(_, [(_, lxp)]) as e) -> e, lxp - | Some lxp -> lxp, lxp - | None -> fatal loc "expression does not exist" in - - (* Special Form *) - let ret = lexp_expand_dmacro body sargs ctx in + try let lxp, ltp = infer (Pvar (loc, mname)) ctx in + + (* FIXME: Check that (conv_p ltp Macro)! *) + let ret = lexp_expand_dmacro lxp sargs ctx in

(* convert typer list to ocaml *) let decls = BI.tlist2olist [] ret in @@ -1017,39 +1015,13 @@ and lexp_p_decls pdecls ctx: ((vdef * lexp * ltype) list list * elab_context) =

and lexp_parse_all (p: pexp list) (ctx: elab_context) : lexp list =

- let rec loop (plst: pexp list) ctx (acc: lexp list) = - match plst with - | [] -> (List.rev acc) - | pe :: plst -> let lxp, _ = infer pe ctx in + let rec loop (plst: pexp list) ctx (acc: lexp list) = + match plst with + | [] -> (List.rev acc) + | pe :: plst -> let lxp, _ = infer pe ctx in (loop plst ctx (lxp::acc)) in - - (loop p ctx []) - -(* -------------------------------------------------------------------------- - * Built-in Macro: i.e special forms - * -------------------------------------------------------------------------- *) -and builtin_macro = [ - (* FIXME: These should be functions! *) - ("decltype", BI.decltype_impl); - ("declexpr", BI.declexpr_impl); - (* FIXME: These are not macros but `special-forms`. - * We should add here `let_in_`, `case_`, etc... *) - ("get-attribute", get_attribute_impl); - ("new-attribute", new_attribute_impl); - ("has-attribute", has_attribute_impl); - ("add-attribute", add_attribute_impl); -] - -and make_macro_map unit : macromap = - List.fold_left (fun map (name, funct) -> - SMap.add name funct map) SMap.empty builtin_macro - -and get_macro_impl loc name = - try SMap.find name (make_macro_map ()) - with Not_found -> fatal loc ("Builtin macro" ^ name ^ " not found") - -and is_builtin_macro name = - SMap.mem name (make_macro_map ()) + + (loop p ctx [])

(* -------------------------------------------------------------------------- * Special form implementation @@ -1124,22 +1096,37 @@ and lexp_print_var_info ctx = print_string "\n") done

+(* Register special forms. *) +let _ = List.iter add_special_form + [ + (* FIXME: We should add here `let_in_`, `case_`, etc... *) + ("get-attribute", get_attribute_impl); + ("new-attribute", new_attribute_impl); + ("has-attribute", has_attribute_impl); + ("add-attribute", add_attribute_impl); + (* FIXME: These should be functions! *) + ("decltype", BI.decltype_impl); + ("declexpr", BI.declexpr_impl); + ] + (* Default context with builtin types * --------------------------------------------------------- *)

(* Make lxp context with built-in types *) -let default_lctx, default_rctx = +let default_lctx =

(* Empty context *) let lctx = make_elab_context in - let lctx = ctx_define lctx (dloc, "Type1") DB.type1 DB.type2 in - let lctx = ctx_define lctx (dloc, "Type") DB.type0 DB.type1 in + let lctx = SMap.fold (fun key (e, t) ctx + -> if String.get key 0 = '-' then ctx + else ctx_define ctx (dloc, key) e t) + (!BI.lmap) lctx in (* FIXME: Add builtins directly here. *) - let lxp = Builtin((dloc, "Built-in"), DB.type0, None) in + let lxp = mkBuiltin((dloc, "Built-in"), DB.type0, None) in let lctx = ctx_define lctx (dloc, "Built-in") lxp DB.type0 in

(* Read BTL files *) - let pres = prelex_file (!btl_folder ^ "types.typer") in + let pres = prelex_file (!btl_folder ^ "builtins.typer") in let sxps = lex default_stt pres in let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in let pxps = pexp_decls_all nods in @@ -1167,7 +1154,9 @@ let default_lctx, default_rctx = with e -> warning dloc "Predef not found"; lctx in - lctx, from_lctx lctx + lctx + +let default_rctx = from_lctx default_lctx

(* String Parsing * --------------------------------------------------------- *)

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -207,16 +207,7 @@ let rec conv_p' meta_ctx (ctx : DB.lexp_context) (vs : set_lexp) e1 e2 : bool = true args1 args2 in conv_p f1 f2 && conv_arglist_p args1 args2 | (Inductive (_, l1, args1, cases1), Inductive (_, l2, args2, cases2)) - -> let rec conv_args ctx vs args1 args2 = - match args1, args2 with - | ([], []) -> true - | ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2) - -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_args (DB.lexp_ctx_cons ctx 0 (Some l1) Variable t1) - (set_shift vs) - args1 args2 - | _,_ -> false in - let rec conv_fields ctx vs fields1 fields2 = + -> let rec conv_fields ctx vs fields1 fields2 = match fields1, fields2 with | ([], []) -> true | ((ak1,vd1,t1)::fields1, (ak2,vd2,t2)::fields2) @@ -225,8 +216,19 @@ let rec conv_p' meta_ctx (ctx : DB.lexp_context) (vs : set_lexp) e1 e2 : bool = (set_shift vs) fields1 fields2 | _,_ -> false in + let rec conv_args ctx vs args1 args2 = + match args1, args2 with + | ([], []) -> + (* Args checked alright, now go on with the fields, + * using the new context. *) + SMap.equal (conv_fields ctx vs) cases1 cases2 + | ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2) + -> ak1 == ak2 && conv_p' ctx vs t1 t2 + && conv_args (DB.lexp_ctx_cons ctx 0 (Some l1) Variable t1) + (set_shift vs) + args1 args2 + | _,_ -> false in l1 == l2 && conv_args ctx vs' args1 args2 - && SMap.equal (conv_fields ctx vs') cases1 cases2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 (* FIXME: Various missing cases, such as Case. *) | (_, _) -> false @@ -237,18 +239,17 @@ let conv_p meta_ctx (ctx : DB.lexp_context) e1 e2

(********* Testing if a lexp is properly typed *********)

- let rec sort_level_max l1 l2 = match nosusp l1, nosusp l2 with | SortLevel SLz, l2 -> l2 | l1, SortLevel SLz -> l1 | SortLevel (SLsucc l1), SortLevel (SLsucc l2) - -> SortLevel (SLsucc (sort_level_max l1 l2)) + -> mkSortLevel (SLsucc (sort_level_max l1 l2)) | _, _ (* FIXME: This requires s.th. like `SLmax of lexp * lexp`! *) -> U.msg_error "TC" (lexp_location l1) ("Can't compute the max of levels `" ^ lexp_string l1 ^ "` and `" ^ lexp_string l2 ^ "`"); - SortLevel SLz + mkSortLevel SLz

let sort_compose l s1 s2 = match s1, s2 with @@ -295,25 +296,25 @@ let rec check' meta_ctx erased ctx e = | SortLevel (SLsucc e) -> let t = check erased ctx e in assert_type ctx e t DB.type_level; - (* FIXME: typelevel vs typelevelsort !? *) DB.type_level | Sort (l, Stype e) -> let t = check erased ctx e in assert_type ctx e t DB.type_level; Sort (l, Stype (SortLevel (SLsucc e))) - | Sort (_, StypeLevel) -> DB.type_omega + | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) - -> (U.msg_error "TC" (lexp_location e) "Reached Unreachable sort!"; - U.internal_error "Reached Unreachable sort!"; - DB.type_omega) - | Builtin (_, t, _) -> t + -> (U.msg_error "TC" (lexp_location e) "Reached unreachable sort!"; + (* U.internal_error "Reached unreachable sort!"; *) + DB.sort_omega) + | Builtin (_, t, _) + -> check_type DB.set_empty ctx t; (* FIXME: Use an empty ctx? *) + t (* FIXME: Check recursive references. *) | Var (((_, name), idx) as v) -> if DB.set_mem idx erased then U.msg_error "TC" (lexp_location e) ("Var `" ^ name ^ "`" - ^ " can't be used here, because it's `erasable`") - else if name = "erased" then U.internal_error "WOWO!"; + ^ " can't be used here, because it's `erasable`"); lookup_type ctx v | Susp (e, s) -> check erased ctx (push_susp e s) | Let (l, defs, e) @@ -411,7 +412,7 @@ let rec check' meta_ctx erased ctx e = (level, ctx) case in level) - cases (SortLevel SLz) in + cases (mkSortLevel SLz) in Sort (l, Stype level) | (ak, v, t)::args -> Arrow (ak, Some v, t, lexp_location t, @@ -477,7 +478,7 @@ let rec check' meta_ctx erased ctx e = ret | Cons (t, (_, name)) -> (match lexp_whnf t ctx meta_ctx with - | Inductive (l, _, fargs, constructors) as it + | Inductive (l, _, fargs, constructors) -> let fieldtypes = SMap.find name constructors in let rec indtype fargs start_index = match fargs with @@ -541,6 +542,7 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Sort _ -> E.Type (* Still useful to some extent. *) | L.Inductive(l, label, _, _) -> E.Inductive(l, label) + | L.Metavar _ -> U.internal_error "Metavar in erase_type"

and filter_arg_list lst = let rec filter_arg_list lst acc =

View it on GitLab: https://gitlab.com/monnier/typer/commit/02dabd43b7f858775ac587cfdca1d71298fd...