Simon Génier pushed to branch warning-40-be-gone at Stefan / Typer

Commits: 955c3940 by Simon Génier at 2020-12-12T06:59:37-05:00 Fix a couple of warning 40.

- - - - -

4 changed files:

- src/REPL.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml

Changes:

===================================== src/REPL.ml ===================================== @@ -66,7 +66,7 @@ let print_input_line i = let ieval_error = Log.log_error ~section:"IEVAL"

let print_and_clear_log () = - if (not Log.typer_log_config.print_at_log) then + if (not Log.typer_log_config.Log.print_at_log) then Log.print_and_clear_log ()

let handle_stopped_compilation msg =

===================================== src/lexp.ml ===================================== @@ -40,6 +40,8 @@ type meta_id = int (* Identifier of a meta variable. *)

type label = symbol

+include Pexp.ArgKind + (*************** Elaboration to Lexp *********************)

(* The scoping of `Let` is tricky:

===================================== src/opslexp.ml ===================================== @@ -194,7 +194,10 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = let elevel = match lexp'_whnf (get_type ctx etype) ctx with | Sort (_, Stype l) -> l | _ -> Log.internal_error "" in - mkCall (DB.eq_refl, [Aerasable, elevel; Aerasable, etype; Aerasable, e]) in + mkCall (DB.eq_refl, + [L.Aerasable, elevel; + L.Aerasable, etype; + L.Aerasable, e]) in let reduce it name aargs = let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with | Inductive (_,_,fargs,_) -> fargs @@ -423,10 +426,10 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in let eqty = mkCall (DB.type_eq, - [(Aerasable, tlvl); (* Typelevel *) - (Aerasable, tltp); (* Inductive type *) - (Anormal, hlxp); (* Lexp of the branch head *) - (Anormal, tlxp)]) in (* Target lexp *) + [(L.Aerasable, tlvl); (* Typelevel *) + (L.Aerasable, tltp); (* Inductive type *) + (L.Anormal, hlxp); (* Lexp of the branch head *) + (L.Anormal, tlxp)]) in (* Target lexp *) DB.lexp_ctx_cons ctx (DB.dloc, None) Variable eqty in (* The map module doesn't have a function to compare two maps with the key (which is needed to get the field types @@ -773,12 +776,12 @@ and check'' erased ctx e = let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in let eqty = mkCall (DB.type_eq, - [(Aerasable, tlvl); (* Typelevel *) - (Aerasable, tltp); (* Inductive type *) - (Anormal, hlxp); (* Lexp of the branch head *) - (Anormal, tlxp)]) in (* Target lexp *) + [(L.Aerasable, tlvl); (* Typelevel *) + (L.Aerasable, tltp); (* Inductive type *) + (L.Anormal, hlxp); (* Lexp of the branch head *) + (L.Anormal, tlxp)]) in (* Target lexp *) (* The eq proof is erasable. *) - let nerased = dbset_push Aerasable nerased in + let nerased = dbset_push L.Aerasable nerased in let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in (nerased, nctx) in SMap.iter

===================================== src/pexp.ml ===================================== @@ -29,7 +29,10 @@ let pexp_error loc = Log.log_error ~section:"PEXP" ~loc

(*************** The Pexp Parser *********************)

-type arg_kind = Anormal | Aimplicit | Aerasable (* eraseable ⇒ implicit. *) +module ArgKind = struct + type arg_kind = Anormal | Aimplicit | Aerasable (* eraseable ⇒ implicit. *) +end +include ArgKind

(* This is Dangerously misleading since pvar is NOT pexp but Pvar is *) type pvar = symbol

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/955c39406a9397a0b11922deedcfe4dac3...