Pure pattern-matching

[ppolesiuk]

This pull-request aims to resolve #149. This will be done in the following steps

• Add flag about strictly positive recursion to definitions of ADT in Unif
• Add flag about strictly positive recursion in ADT environment (TypeInference.Module.adt_info)
• Recognition of strictly positive recursive types in TypeInference
• Use information about strictly positive recursion in the effect of pattern-matching (TypeInference.Pattern)
• Update translation to Core
• Add flag about strictly positive recursion to definitions of ADT in Core
• Add effect of pattern-matching to TData type in Core
• Adjust internal type-checker for Core

[ppolesiuk]

This implementation has some slight problem with generated accessors for recursive records. For instance, when we write the following code

data rec  T = { x : T }
let f (t : T) = t.x

the f function is impure. This problem comes from the desugaring of recursive records. The above definition is a syntactic sugar for

rec
  data T = T of { x : T }
  method x { self = T { x } : T } = x
end

Notice, that the method is in recursive block, and therefore is impure, even if the pattern-matching on self is pure.

[Foxinio]

All the changes look good to me, however I did look at the problem mention above and there seems to exist simple (partial) fix. It will make record accessors non recursive when record is marked rec and when it is in rec block with only other records, data definitions and labels. It won't always make accessors pure, like in this piece of code:

rec
  let foo (x : T) (n : Int) =
    if n == 0 then x
    else foo (x.x n) (n - 1)

  data T = { x : Int -> T }
end

If we ever decide to make non-termination detection more precise, for example like the one that's present in coq, my change will become redundant as whole problem will be solved. Until then it will help with the not obscure code.

[Foxinio]

changes mentioned:

diff --git a/src/DblParser/Desugar.ml b/src/DblParser/Desugar.ml
index 27d4fe2..ed8bcae 100644
--- a/src/DblParser/Desugar.ml
+++ b/src/DblParser/Desugar.ml
@@ -42,6 +42,19 @@ let tr_ctor_name' (cname : Raw.ctor_name) =
 
 let with_nowhere data = { pos = Position.nowhere; data = data}
 
+let rec node_is_rec_data (def : Raw.def) =
+  match def.data with
+  | DRecord _ -> true
+  | DData   _ -> true
+  | DLabel  _ -> true
+  | _ -> false
+
+let node_is_data_def (def : def) =
+  match def.data with
+  | DData  _ -> true
+  | DLabel _ -> true
+  | _ -> false
+
 let annot_tp e tp =
   { pos = e.pos;
     data = Raw.EAnnot(e, with_nowhere tp)
@@ -751,6 +764,11 @@ and tr_def ?(public=false) (def : Raw.def) =
   | DOpen(pub, path) -> 
     let public = public || pub in
     [ make (DOpen(public, path)) ]
+  | DRec(pub, defs) when List.for_all node_is_rec_data defs ->
+    let public = public || pub in
+    let dds, accessors = tr_defs ~public defs
+      |> List.partition node_is_data_def in
+    make (DRec dds) :: accessors
   | DRec(pub, defs) ->
     let public = public || pub in
     [ make (DRec (tr_defs ~public defs)) ]

[forell]

I haven't spotted anything suspicious, so I'm in favor of merging. However, as (I think) @ilikeheaps pointed out, we should make sure existing tests still make sense after the change. I remember you identified ok0079_impureMethod.fram as outdated, which tests the fix for an old bug reported in #14. We should force impurity in that test by some other means.

[ppolesiuk]

@Foxinio These changes looks reasonable, but I think we should merge them in a separate pull-request. This PR propose basic solution to the problem of pure pattern-matching that has some limitations, but has no edge cases. Your fix improves the solution, but is not perfect, and in a long run will be probably replaced by something better. Having separate commits for them would make history cleaner, and it would be easier to revert your changes in order to provide the final solution.