Simon Génier pushed to branch macro-expansion-tracing at Stefan / Typer

Commits: d3daf0a3 by Soilih BEN SOILIH at 2022-02-16T10:07:07-05:00 Add a `Proj` constructor to the `lexp` type

We add a projection constructor to the Lexp type in order to be able to offer the completion in a satisfactory manner for the LSP server. When we write MODULE.FIELD, if FIELD doesn't exist, we could not offer the completion because the AST could not be generated at all. So we add this case to be able to have an AST and be able to find the functions of a module, and also select specific functions thanks to the label of a projection.

* src/lexp.ml (lexp): Add `Proj` constructor. (lexp'_hash, lexp_head, lexp_location, push_susp, clean, lexp_unparse) (lexp_str): Adjust accordingly. (mkProj): new function. * src/elab.ml (adjust_subst.loop): Add `Proj` case for the loop substitution. (sform_proj): new special form. (register_special_forms): Register it. * src/opslexp.ml (pos_of_label): new function. (check'', get_type, fv, erase_type): * src/positivity.ml (positive'): Add new case for `Proj`. * src/eval.ml (eval): * src/apply_inv_subst.ml (apply_inv_subst): * src/elexp.ml (elexp, elexp_location, elexp_name, elexp_string): Add new case for `Proj`. * btl/pervasive.typer (__/.__): Delete macro.

- - - - - feda20f6 by Simon Génier at 2022-02-16T19:08:10-05:00 Add a flag to show macros, their arguments and the expanded code.

- - - - -

11 changed files:

- btl/pervasive.typer - src/elab.ml - src/elexp.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/log.ml - src/opslexp.ml - src/positivity.ml - src/unification.ml - typer.ml

Changes:

===================================== btl/pervasive.typer ===================================== @@ -1,6 +1,6 @@ %%% pervasive --- Always available definitions

-%% Copyright (C) 2011-2020 Free Software Foundation, Inc. +%% Copyright (C) 2011-2022 Free Software Foundation, Inc. %% %% Author: Pierre Delaunay pierre.delaunay@hec.ca %% Keywords: languages, lisp, dependent types. @@ -426,32 +426,6 @@ BoolMod = (##datacons Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); pair = datacons Pair pair;

-__.__ = - let mksel o f = - let constructor = Sexp_node (Sexp_symbol "##datacons") - (cons (Sexp_symbol "?") - (cons (Sexp_symbol "cons") - nil)); - pattern = Sexp_node constructor - (cons (Sexp_node (Sexp_symbol "_:=_") - (cons f (cons (Sexp_symbol "v") - nil))) - nil); - branch = Sexp_node (Sexp_symbol "_=>_") - (cons pattern (cons (Sexp_symbol "v") nil)); - in Sexp_node (Sexp_symbol "case_") - (cons (Sexp_node (Sexp_symbol "_|_") - (cons o (cons branch nil))) - nil) - in macro (lambda args - -> IO_return - case args - | cons o tail - => (case tail - | cons f _ => mksel o f - | nil => Sexp_error) - | nil => Sexp_error); - %% Triplet (tuple with 3 values) type Triplet (a : Type) (b : Type) (c : Type) | triplet (x : a) (y : b) (z : c);

===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2021 Free Software Foundation, Inc. + * Copyright (C) 2011-2022 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -97,6 +97,12 @@ let lexp_fatal loc lexp = let value_fatal loc value = fatal ~loc ~print_action:(value_print_details value)

+let macro_tracing_enabled = ref false +let trace_macro location fmt = + if !macro_tracing_enabled + then Log.log_debug ~loc:location ~section:"MACRO" fmt + else Printf.ifprintf () fmt + (** Type info returned by elaboration. *) type sform_type = | Checked (* Checked that the expression has the requested type. *) @@ -429,6 +435,7 @@ let meta_to_var ids (e : lexp) = | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e | Var (n,i) -> if i < o then e else mkVar (n, i + count) + | Proj (l, lxp, lbl) -> mkProj (l, loop o lxp, lbl) | Susp (e, s) -> loop o (push_susp e s) | Let (l, defs, e) -> let len = List.length defs in @@ -919,21 +926,34 @@ and check_case rtype (loc, target, ppatterns) ctx =

mkCase (loc, tlxp, rtype, lpattern, dflt)

-and elab_macro_call ctx func args ot = - let t - = match ot with - | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) - (lexp_location func) - | Some t -> t in - let sxp = match lexp_expand_macro (lexp_location func) - func args ctx (Some t) with +and elab_macro_call + (ctx : elab_context) + (func : lexp) + (args : token list) + (ot : ltype option) + : lexp * sform_type = + + let location = lexp_location func in + let t = + match ot with + | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) location + | Some t -> t + in + + trace_macro location {|expanding: %s|} (lexp_string func); + List.iteri + (fun i arg -> arg |> sexp_string |> trace_macro location {|input %d: %s|} i) + args; + let sxp = + match lexp_expand_macro location func args ctx (Some t) with | Vcommand cmd -> (match cmd () with - | Vsexp (sxp) -> sxp - | v -> value_fatal (lexp_location func) v - "Macros should return a IO Sexp") - | v -> value_fatal (lexp_location func) v - "Macros should return an IO" in + | Vsexp (sxp) -> sxp + | v -> value_fatal location v "Macros should return a IO Sexp") + | v -> value_fatal location v "Macros should return an IO" + in + trace_macro location {|output: %s|} (sexp_string sxp); + elaborate ctx sxp ot

(* Identify Call Type and return processed call. *) @@ -1726,6 +1746,18 @@ let sform_letin ctx loc sargs ot = match sargs with | _ -> sexp_error loc "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc

+let sform_proj ctx loc sargs _ = + match sargs with + | [lxp;(Symbol (loca,str))] + -> let (ret,_) = infer lxp ctx in + let e = mkProj (loc,ret,(loca,str)) in + (e, Lazy) + | [_;_] + -> sexp_error loc "Second argument is not a Symbol!"; + sform_dummy_ret ctx loc + | _ -> sexp_error loc "Wrong arg number!"; + sform_dummy_ret ctx loc + let rec infer_level ctx se : lexp = match se with | Symbol (_, "z") -> mkSortLevel SLz @@ -1846,6 +1878,7 @@ let register_special_forms () = ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype); + ("__.__", sform_proj); ("lambda_->_", sform_lambda Anormal); ("lambda_=>_", sform_lambda Aimplicit); ("lambda_≡>_", sform_lambda Aerasable); @@ -1855,7 +1888,7 @@ let register_special_forms () = ("case_", sform_case); ("let_in_", sform_letin); ("Type_", sform_type); - ("load", sform_load); + ("load", sform_load); (* FIXME: We should add here `let_in_`, `case_`, etc... *) (* FIXME: These should be functions! *) ("decltype", sform_decltype);

===================================== src/elexp.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2020 Free Software Foundation, Inc. + * Copyright (C) 2011-2022 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -52,6 +52,8 @@ type elexp = (* A variable reference, using deBruijn indexing. *) | Var of vref

+ | Proj of U.location * elexp * int + (* Recursive `let` binding. *) | Let of U.location * (vname * elexp) list * elexp

@@ -83,6 +85,7 @@ let rec elexp_location e = match e with | Imm s -> sexp_location s | Var ((l,_), _) -> l + | Proj (l,_,_) -> l | Builtin ((l, _)) -> l | Let (l,_,_) -> l | Lambda ((l,_),_) -> l @@ -96,6 +99,7 @@ let elexp_name e = match e with | Imm _ -> "Imm" | Var _ -> "Var" + | Proj _ -> "Proj" | Let _ -> "Let" | Call _ -> "Call" | Cons _ -> "Cons" @@ -136,6 +140,8 @@ and elexp_string lxp = | Imm(s) -> sexp_string s | Builtin((_, s)) -> s | Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]" + | Proj (_,lxp,i) + -> "( __.__ " ^ elexp_string lxp ^ " " ^ (string_of_int i) ^ " )" | Cons (_, (_, s)) -> "datacons(" ^ s ^")"

| Lambda((_, s), b) -> "lambda " ^ L.maybename s ^ " -> " ^ (elexp_string b)

===================================== src/eval.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018, 2020, 2021 Free Software Foundation, Inc. + * Copyright (C) 2011-2018, 2020, 2021, 2022 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -462,7 +462,12 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) -> eval_call (elexp_location f) f trace (eval f ctx trace) (List.map (fun e -> eval e ctx trace) args) - + (* Proj *) + | Proj (loc, e, i) + -> (match eval' e ctx with + | Vcons (_, vtl) -> List.nth vtl i + | _ -> error loc "Proj on a non-datatype constructor: %s \n" + (elexp_string e)) (* Case *) | Case (loc, target, pat, dflt) -> (eval_case ctx trace loc target pat dflt)

===================================== src/inverse_subst.ml ===================================== @@ -1,6 +1,6 @@ (* inverse_subst.ml --- Computing the inverse of a substitution

-Copyright (C) 2016-2020 Free Software Foundation, Inc. +Copyright (C) 2016-2022 Free Software Foundation, Inc.

Author: Vincent Bonnevalle tiv.crb@gmail.com

@@ -264,6 +264,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = | Sort (_l, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) + | Proj (l,lxp,lbl) -> mkProj (l, apply_inv_subst lxp s, lbl) | Susp (e, s') -> apply_inv_subst (push_susp e s') s | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in

===================================== src/lexp.ml ===================================== @@ -1,6 +1,6 @@ (* lexp.ml --- Lambda-expressions: the core language.

-Copyright (C) 2011-2021 Free Software Foundation, Inc. +Copyright (C) 2011-2022 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -66,6 +66,7 @@ type ltype = lexp | Sort of U.location * sort | Builtin of symbol * ltype | Var of vref + | Proj of U.location * lexp * label | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vname * lexp * ltype) list * lexp @@ -245,6 +246,10 @@ let lexp'_hash (lp : lexp') = args))) | Susp (lp, subst) -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (Hashtbl.hash subst)) + | Proj (l,lxp,lbl) + -> U.combine_hash 15 (U.combine_hash (Hashtbl.hash l) + (U.combine_hash (Hashtbl.hash lxp) + (Hashtbl.hash lbl)))

(* Equality function for hash table * using physical equality for "sub-lexp" and compare for `subst`. *) @@ -307,8 +312,9 @@ let hc (l : lexp') : lexp = let mkImm s = hc (Imm s) let mkSortLevel l = hc (SortLevel l) let mkSort (l, s) = hc (Sort (l, s)) -let mkBuiltin (v, t) = hc (Builtin (v, t)) +let mkBuiltin (v, t) = hc (Builtin (v, t)) let mkVar v = hc (Var v) +let mkProj (l,lxp,lbl) = hc (Proj (l,lxp,lbl)) let mkLet (l, ds, e) = hc (Let (l, ds, e)) let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) @@ -329,6 +335,7 @@ let lexp_head e = | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s | Var _ -> "Var" + | Proj _ -> "Proj" | Let _ -> "let" | Arrow _ -> "Arrow" | Lambda _ -> "lambda" @@ -524,6 +531,7 @@ let rec lexp_location e = | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e *) | Metavar (_,_,(l,_)) -> l + | Proj (l,_,_) -> l

(********* Normalizing a term *********) @@ -590,6 +598,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) * in many other cases than just when we bump into a Susp. *) | Susp (e,s') -> push_susp e (scompose s' s) | (Var _ | Metavar _) -> nosusp (mkSusp e s) + | Proj (l,lxp,lbl) -> mkProj (l, mkSusp lxp s, lbl)

and nosusp e = (* Return `e` with no outermost `Susp`. *) match lexp_lexp' e with @@ -653,6 +662,7 @@ let clean e = | Susp (e, s') -> clean (scompose s' s) e | Var _ -> if S.identity_p s then e else clean S.identity (mkSusp e s) + | Proj (l, lxp, lbl) -> mkProj (l, clean s lxp, lbl) | Metavar (idx, s', name) -> let s = scompose s' s in match metavar_lookup idx with @@ -671,6 +681,9 @@ let rec lexp_unparse lxp = | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) | Var ((loc, name), _) -> Symbol (loc, maybename name) + | Proj (l,lxp,(loc,str) ) + -> Node (Symbol (l, "__.__"), + [(lexp_unparse lxp);(Symbol (loc,str))]) | Cons (t, (l, name)) -> Node (sdatacons, [lexp_unparse t; Symbol (l, name)]) @@ -973,6 +986,9 @@ and lexp_str ctx (exp : lexp) : string =

| Var ((_loc, name), idx) -> maybename name ^ (index idx) ;

+ | Proj (_, lxp, (_, str)) + -> "( __.__ " ^ lexp_str' lxp ^ " " ^ str ^ " )" + | Metavar (idx, subst, (_loc, name)) (* print metavar result if any *) -> (match metavar_lookup idx with

===================================== src/log.ml ===================================== @@ -114,15 +114,15 @@ let maybe_color_string color_opt str = | None -> str

let string_of_log_entry {level; kind; section; loc; msg; _} = - let color = if typer_log_config.color then (level_color level) else None in + let color = if typer_log_config.color then level_color level else None in + let kind_string = Option.value ~default:(string_of_level level) kind in let parens s = "(" ^ s ^ ")" in - (Option.value ~default:"" (Option.map Source.Location.to_string loc) - ^ maybe_color_string - color - (Option.value ~default:(string_of_level level) kind) - ^ ":" - ^ Option.value ~default:"" (Option.map parens section) ^ " " - ^ msg) + sprintf + "%s %s:%s %s" + (Option.value ~default:"" (Option.map Source.Location.to_string loc)) + (maybe_color_string color kind_string) + (Option.value ~default:"" (Option.map parens section)) + msg

let print_entry entry = print_endline (string_of_log_entry entry);

===================================== src/opslexp.ml ===================================== @@ -1,6 +1,6 @@ (* opslexp.ml --- Operations on Lexps

-Copyright (C) 2011-2021 Free Software Foundation, Inc. +Copyright (C) 2011-2022 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -747,6 +747,51 @@ and check'' erased ctx e = args) in let tct = arg_loop ctx erased args in tct + | Proj (l, e, (loc, label)) + -> ( let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let etype = lexp_whnf (check erased ctx e) ctx in + let it, aargs = call_split etype in + match lexp'_whnf it ctx, aargs with + | Inductive (_, _, fargs, constructors), aargs + when SMap.cardinal constructors = 1 + -> let rec mksubst s fargs aargs = + match fargs, aargs with + | [], [] -> s + | _farg::fargs, (_ak, aarg)::aargs + -> mksubst (S.cons aarg s) fargs aargs + | _,_ -> (log_tc_error ~loc:l + "Wrong arg number to inductive type!"; s) in + let s = mksubst S.identity fargs aargs in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in + let rec getfieldtype s (fieldtypes + : (arg_kind * vname * ltype) list) = + match fieldtypes with + | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; + etype + | (ak, (_, Some fn), ftype)::_ when fn = label + (* We found our field! *) + -> if not (ak = Aerasable) + then mkSusp ftype s (* Yay! We found our field! *) + else (log_tc_error ~loc:l "Can't Proj an erasable field: %s" + label; + Lexp.impossible) + | (_, vdef, _)::fieldtypes + -> let fvdef vdef e loc lbl = + match vdef with + |(_, Some _) -> mkProj (loc, e, lbl) + |_ -> Lexp.impossible in + let fieldref = fvdef vdef e l (loc, label) in + getfieldtype (S.cons fieldref s) fieldtypes in + getfieldtype s fieldtypes + | Inductive _, _ + -> Log.log_error ~loc:l + "Proj on an inductive type that's not a tuple!"; + etype + | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; etype) + | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = @@ -926,6 +971,7 @@ and fv (e : lexp) : (DB.set * mv_set) = | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty | Builtin _ -> fv_empty | Var (_, i) -> (DB.set_singleton i, mv_set_empty) + | Proj (_, lxp, _) -> fv lxp | Susp (e, s) -> fv (push_susp e s) | Let (_, defs, e) -> let len = List.length defs in @@ -1014,6 +1060,54 @@ and get_type ctx e = | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, _name), _idx) as v) -> lookup_type ctx v + | Proj (l, e, (loc, label)) + -> ( + + let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let etype = lexp_whnf (get_type ctx e) ctx in + let it, aargs = call_split etype in + match lexp'_whnf it ctx, aargs with + | Inductive (_, _, fargs, constructors), aargs + when SMap.cardinal constructors = 1 + -> let rec mksubst s fargs aargs = + match fargs, aargs with + | [], [] -> s + | _farg::fargs, (_ak, aarg)::aargs + -> mksubst (S.cons aarg s) fargs aargs + | _,_ -> (log_tc_error ~loc:l + "Wrong arg number to inductive type!"; s) in + let s = mksubst S.identity fargs aargs in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in + let rec getfieldtype s (fieldtypes + : (arg_kind * vname * ltype) list) = + match fieldtypes with + | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" + label; + etype + | (ak, (_, Some fn), ftype)::_ when fn = label + (* We found our field! *) + -> if not (ak = Aerasable) + then mkSusp ftype s (* Yay! We found our field! *) + else (log_tc_error ~loc:l + "Can't Proj an erasable field: %s" label; + Lexp.impossible) + | (_, vdef, _)::fieldtypes + -> let fvdef vdef e loc lbl = + match vdef with + |(_, Some _) -> mkProj (loc, e, lbl) + |_ -> Lexp.impossible in + let fieldref = fvdef vdef e l (loc, label) in + getfieldtype (S.cons fieldref s) fieldtypes in + getfieldtype s fieldtypes + | Inductive _, _ + -> Log.log_error ~loc:l + "Proj on an inductive type that's not a tuple!"; + etype + | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; + etype) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in @@ -1140,11 +1234,53 @@ let arity_of_cons ^^ {|because it is not an inductive type: %s|}) name (lexp_string ty)

+ +let pos_of_label lctx label e : int = + let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + + let it, aargs = call_split (lexp_whnf e lctx) in + match lexp'_whnf it lctx, aargs with + | Inductive (_, _, _, constructors), _ + when SMap.cardinal constructors = 1 + -> let (_, st) = label in + (match SMap.bindings constructors with + | [(_,l)] -> let rec find_index + label + (l : (arg_kind * vname * ltype) list) + (c: int) : int = + match l with + | [] + -> let (loc,st) = label in + Log.log_error ~loc:loc "Label Not Found: %s" st; + 0 + | (_, (_, Some vn), _ )::_ when (String.equal vn st) + -> c + | _::tl -> find_index label tl (c + 1) + in + find_index label l 0 + | _ -> let (loc, _) = label in + Log.log_fatal ~loc:loc "Wrong arg number to inductive type!") + | Inductive _, _ + -> let (loc,_) = label in + Log.log_error ~loc:loc "Proj on an inductive type that's not a tuple!"; + 0 + | _,_ -> let (loc,_) = label in + Log.log_error ~loc:loc "Proj on a non-inductive type: %s" + (Lexp.lexp_string it); + 0 + + let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = match lexp_lexp' lxp with | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) | L.Var (v) -> E.Var (v) + | L.Proj (l, exp, label) + -> let t = get_type lctx exp in + E.Proj (l, erase_type lctx exp, pos_of_label lctx label t) | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s)

| L.Lambda (P.Aerasable, _, _, body)

===================================== src/positivity.ml ===================================== @@ -1,4 +1,4 @@ -(* Copyright (C) 2021 Free Software Foundation, Inc. +(* Copyright (C) 2021, 2022 Free Software Foundation, Inc. * * Author: Simon Génier simon.genier@umontreal.ca * Keywords: languages, lisp, dependent types. @@ -116,6 +116,7 @@ and positive' index lexp = * as the Call applies as a degenerate case with no arguments. *) -> true + | Lexp.Proj _ -> false

| Lexp.Case _ | Lexp.Cons _ | Lexp.Let _ | Lexp.Sort _ | Lexp.SortLevel _ (* There are no rules that have these synctactic forms as a conclusion. *)

===================================== src/unification.ml ===================================== @@ -1,6 +1,6 @@ (* unification.ml --- Unification of Lexp terms

-Copyright (C) 2016-2021 Free Software Foundation, Inc. +Copyright (C) 2016-2022 Free Software Foundation, Inc.

Author: Vincent Bonnevalle tiv.crb@gmail.com

@@ -69,6 +69,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Sort (_, (StypeOmega | StypeLevel)) -> false | Builtin _ -> false | Var (_, _i) -> false + | Proj (_,lxp, _) -> oi lxp | Susp (_e, _s) -> Log.internal_error "`e` should be "clean" here!?" (* ; oi (push_susp e s) *) | Let (_, defs, e)

===================================== typer.ml ===================================== @@ -40,12 +40,22 @@ let arg_defs =

("-Vfull-lctx", Arg.Set Debruijn.log_full_lctx, - "Print the full lexp context on error."); + "Print the full lexp context on error"); + + ("-Vmacro-expansion", + Arg.Set Elab.macro_tracing_enabled, + "Trace macro expansion"); ]

+let parse_args argv usage = + try Arg.parse_argv argv arg_defs add_input_file usage with + | Arg.Help (message) -> + print_string message; + exit 0 + let compile_main argv = let usage = Sys.executable_name ^ " compile [options] <file> …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage;

let ectx = Elab.default_ectx in let backend = new Gambit.gambit_compiler (ectx_to_lctx ectx) stdout in @@ -57,7 +67,7 @@ let compile_main argv =

let repl_main argv = let usage = Sys.executable_name ^ " repl [options] [<file>] …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage;

print_string (Fmt.make_title " TYPER REPL "); print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2021"; @@ -80,7 +90,7 @@ let repl_main argv =

let run_main argv = let usage = Sys.executable_name ^ " run [options] <file> …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage;

let ectx = Elab.default_ectx in let backend = new Eval.ast_interpreter (ectx_to_lctx ectx) in

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/aab4123773bc2a397fcb6a0fc2fe66045...