From e1d4ad82b1557a8cf808e0374ece9c39ed349ea2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jul 2017 23:33:42 +0200
Subject: Cleaning up the implementation of module subtyping in the kernel.

We export a function in UGraph to check that a polymorphic instance is
a subtype of another, instead of rolling up our own in module code.

We also add a few tests for module subtyping in presence of polymorphic
constants.
---
 kernel/uGraph.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'kernel/uGraph.ml')

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 487257a776..9793dd881d 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -830,6 +830,18 @@ let sort_universes g =
   in
   normalize_universes g
 
+(** Subtyping of polymorphic contexts *)
+
+let check_subtype univs ctxT ctx =
+  if AUContext.size ctx == AUContext.size ctx then
+    let (inst, cst) = UContext.dest (AUContext.repr ctx) in
+    let cstT = UContext.constraints (AUContext.repr ctxT) in
+    let push accu v = add_universe v false accu in
+    let univs = Array.fold_left push univs (Instance.to_array inst) in
+    let univs = merge_constraints cstT univs in
+    check_constraints cst univs
+  else false
+
 (** Instances *)
 
 let check_eq_instances g t1 t2 =
-- 
cgit v1.2.3