From 4ba1b9e4165cda40e06fca3b563b7561a6cffc70 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 13 Sep 2021 14:33:06 +0200 Subject: Handle the new warnings of OCaml 4.13 Warning 69 "mutable record field is never mutated": 3 occurrences in backend/IRC.ml removed the "mutable" qualifier on these fields Warning 70 "cannot find interface file" many .ml files have no .mli no strong motivation to add the .mli files turned off the warning in Makefile.extr --- backend/IRC.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backend') diff --git a/backend/IRC.ml b/backend/IRC.ml index ed5ae186..6f4bbe29 100644 --- a/backend/IRC.ml +++ b/backend/IRC.ml @@ -33,8 +33,8 @@ type node = { ident: int; (*r unique identifier *) typ: typ; (*r its type *) var: var; (*r the XTL variable it comes from *) - mutable regclass: int; (*r identifier of register class *) - mutable accesses: int; (*r number of defs and uses *) + regclass: int; (*r identifier of register class *) + accesses: int; (*r number of defs and uses *) mutable spillcost: float; (*r estimated cost of spilling *) mutable adjlist: node list; (*r all nodes it interferes with *) mutable degree: int; (*r number of adjacent nodes *) @@ -206,7 +206,7 @@ type graph = { varTable: (var, node) Hashtbl.t; mutable nextIdent: int; (* The adjacency set *) - mutable adjSet: unit IntPairs.t; + adjSet: unit IntPairs.t; (* Low-degree, non-move-related nodes *) simplifyWorklist: DLinkNode.t; (* Low-degree, move-related nodes *) -- cgit From c9fad7cd7bdc4e79fb06a1d39abfa0d5471623e5 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 15 Sep 2021 14:00:41 +0200 Subject: Avoid `Global Set Asymmetric Patterns` (#408) Instead, add `Set Asymmetric Patterns` to the files that need it, or use `Arguments` to make inductive types work better with symmetric patterns. Closes: #403 --- backend/Inlining.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'backend') diff --git a/backend/Inlining.v b/backend/Inlining.v index 7eb0f0fa..d66d2586 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -293,10 +293,13 @@ Inductive inline_decision (ros: reg + ident) : Type := | Cannot_inline | Can_inline (id: ident) (f: function) (P: ros = inr reg id) (Q: fenv!id = Some f). +Arguments Cannot_inline {ros}. +Arguments Can_inline {ros}. + Program Definition can_inline (ros: reg + ident): inline_decision ros := match ros with - | inl r => Cannot_inline _ - | inr id => match fenv!id with Some f => Can_inline _ id f _ _ | None => Cannot_inline _ end + | inl r => Cannot_inline + | inr id => match fenv!id with Some f => Can_inline id f _ _ | None => Cannot_inline end end. (** Inlining of a call to function [f]. An appropriate context is -- cgit