wip

Author: loutr

src/ecHiInductive.ml

@@ -131,21 +131,24 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) =
 
       let tdecl = EcEnv.Ty.by_path_opt tname env0
         |> odfl (EcDecl.abs_tydecl ~params:(`Named tparams) lc) in
-      let tyinst () =
-        fun ty -> ty_instantiate tdecl.tyd_params targs ty in
+      let tyinst = ty_instantiate tdecl.tyd_params targs in
 
       match tdecl.tyd_type with
       | Abstract _ ->
-          List.exists isempty (targs)
+          List.exists isempty targs
 
       | Concrete ty ->
-          isempty_1 [tyinst () ty]
+          isempty_1 [ tyinst ty ]
 
       | Record (_, fields) ->
-          isempty_1 (List.map (tyinst () |- snd) fields)
+          isempty_1 (List.map (tyinst |- snd) fields)
 
       | Datatype dt ->
-          isempty_n (List.map (List.map (tyinst ()) |- snd) dt.tydt_ctors)
+          (* FIXME: Inspecting all constructors recursively causes
+             non-termination in some cases. One can have the same
+             limitation as is done for positivity in order to limit this
+             unfolding to well-behaved cases. *)
+          isempty_n (List.map (List.map tyinst |- snd) dt.tydt_ctors)
 
     in
 

src/ecInductive.ml

@@ -98,7 +98,17 @@ exception NonPositive of nonpositive_description
     - inductive occurences a₁ a₂ .. aₙ p are such that ∀i. p ∉ fv(aᵢ)
 
     Crucially, this has to be checked whenever p occurs in an instance of
-    another type constructor. *)
+    another type constructor.
+
+    FIXME: The current implementation prohibits the use of a type which changes
+    its type arguments like e.g.
+    {v
+      type ('a, 'b) t = [
+        | Elt of 'a
+        | Swap of ('b, 'a) t
+      ].
+    v}
+    to be used as a type constructor  *)
 
 let rec occurs ?(normty = identity) p t =
   match (normty t).ty_node with
@@ -121,7 +131,7 @@ let rec check_positivity_in_decl fct p decl ident =
     | Concrete ty -> [ ty ]
     | Abstract _ ->
         raise (NonPositive (AbstractTypeRestriction p)) 
-    | Datatype { tydt_ctors } -> List.flatten @@ List.map snd tydt_ctors
+    | Datatype { tydt_ctors } -> List.concat_map snd tydt_ctors
     | Record (_, tys) -> List.map snd tys
   in
   List.iter (check_positivity_ident fct p decl.tyd_params ident) tys_to_inspect