Merge pull request #169 from clarus/add-dune-2.8

Upgrade to Merlin 3.4.2

CHANGELOG.md

@@ -1,10 +1,11 @@
-## [Unreleased]
+## 2.4.1 (March 15, 2021)
 * Add basic translation of `try ... with` with extensible types (cannot run in Coq but may be extracted to OCaml).
 * Add basic support for matching on extensible types.
 * Add the attribute `@coq_type_annotation` to generate the type annotation of an expression.
 * Show nicer error messages for errors in the configuration file.
 * Remove existential types from the modules (except for the first-class modules).
 * Upgrade OCaml to the version 4.10.
+* Upgrade Dune to the version 2.8.
 
 ## 2.4.0 (January 11, 2021)
 * Install the Coq proofs in `CoqOfOCaml` rather than `OCaml` for clarity.

README.md

@@ -77,11 +77,6 @@ Read the `coq-of-ocaml.opam` file at the root of the project to know the depende
 coq-of-ocaml file.ml
 ```
 
-If this does not work as expected, you may specify the path to a `.merlin` file:
-```
-coq-of-ocaml -merlin src/.merlin path/file.ml
-```
-
 You can start to experiment with the test files in `tests/` or look at our [online examples](https://clarus.github.io/coq-of-ocaml/examples/).
 
 ## License

coq-of-ocaml.opam

@@ -18,7 +18,8 @@ install: [
 ]
 depends: [
   "conf-ruby" {with-test}
-  "dune" {>= "2.0" & < "2.8"}
+  "csexp"
+  "dune" {>= "2.8"}
   "ocaml" {>= "4.10" & < "4.11"}
   "ocamlfind" {>= "1.5.2"}
   "smart-print"

doc/docs/run.md

@@ -50,7 +50,6 @@ coq-of-ocaml [options] file.ml
 ```
 
 The options are:
-* `-merlin file`: specify the configuration file of Merlin (by default `.merlin` if this file exists in the current folder)
 * `-output file`: specify the name of the Coq `.v` file to output (by default the capitalized OCaml file name with a `.v` extension)
 * `-json-mode`: produce the list of error messages in JSON format; useful for post-processing
 

merlin/analysis/completion.ml

@@ -537,9 +537,12 @@ let complete_prefix ?get_doc ?target_type ?(kinds=[]) ~prefix ~is_label
           (kinds : kind list :> kinds)
       in
       let add_completions acc kind =
-        get_candidates ?get_doc ?target_type ?prefix_path ~prefix kind ~validate env branch @ acc
+        get_candidates
+          ?get_doc ?target_type ?prefix_path ~prefix kind ~validate env branch
+        :: acc
       in
       List.fold_left ~f:add_completions order ~init:[]
+      |> List.concat
     else base_completion
   in
   try
@@ -660,7 +663,7 @@ let expand_prefix ~global_modules ?(kinds=[]) env prefix =
   let process_prefix_path prefix_path =
     let candidates =
       let aux compl kind =
-        get_candidates ?prefix_path ~prefix:"" kind ~validate env [] @ compl in
+        get_candidates ?prefix_path ~prefix:"" kind ~validate env [] :: compl in
       List.fold_left ~f:aux kinds ~init:[]
     in
     match prefix_path with
@@ -669,11 +672,13 @@ let expand_prefix ~global_modules ?(kinds=[]) env prefix =
         if not (validate' name) then None else
           Some (item_for_global_module name)
       in
-      candidates @ List.filter_map global_modules ~f
+      candidates @ [List.filter_map global_modules ~f]
+      |> List.flatten
     | Some lident ->
       let lident = Longident.flatten lident in
       let lident = String.concat ~sep:"." lident ^ "." in
-      List.map candidates ~f:(fun c -> { c with name = lident ^ parenthesize_name c.name })
+      List.concat_map candidates ~f:(List.map ~f:(fun c ->
+          { c with name = lident ^ parenthesize_name c.name }))
   in
   List.concat_map ~f:process_prefix_path lidents
 

merlin/analysis/destruct.mli

@@ -73,6 +73,7 @@
 exception Not_allowed of string
 exception Useless_refine
 exception Nothing_to_do
+exception Wrong_parent of string
 
 val node :
   Mconfig.t -> Msource.t -> Browse_raw.node ->

merlin/analysis/destruct.ml.new → merlin/analysis/destruct.new.ml

@@ -32,6 +32,7 @@ open Browse_raw
 exception Not_allowed of string
 exception Useless_refine
 exception Nothing_to_do
+exception Wrong_parent of string
 
 let {Logger. log} = Logger.for_section "destruct"
 
@@ -195,6 +196,37 @@ let rec needs_parentheses = function
       end
     | _ -> needs_parentheses ts
 
+let rec get_match = function
+| [] -> assert false
+| parent :: parents ->
+  match parent with
+  | Case _
+  | Pattern _ ->
+    (* We are still in the same branch, going up. *)
+    get_match parents
+  | Expression m ->
+    (match m.Typedtree.exp_desc with
+    | Typedtree.Texp_match (e, _, _) -> m, e.exp_type
+    | Typedtree.Texp_function _ ->
+      let typ = Ctype.repr m.exp_type in
+        (* Function must have arrow type. This arrow type
+           might be hidden behind type constructors *)
+        m, (match typ.desc with
+        | Tarrow (_, te, _, _) -> te
+        | Tconstr _ ->
+          (match (Ctype.full_expand m.exp_env typ |> Ctype.repr).desc with
+          | Tarrow (_, te, _, _) -> te
+          | _ -> assert false)
+        | _ -> assert false)
+    | _ ->
+      (* We were not in a match *)
+      let s = Mbrowse.print_node () parent in
+      raise  (Not_allowed s))
+  | _ ->
+    (* We were not in a match *)
+    let s = Mbrowse.print_node () parent in
+    raise  (Not_allowed s)
+
 let rec get_every_pattern = function
   | [] -> assert false
   | parent :: parents ->
@@ -236,8 +268,9 @@ let rec get_every_pattern = function
       in
       loc, patterns
     | _ ->
-      let s = Json.to_string (Browse_misc.dump_browse parent) in
-      invalid_arg (sprintf "get_every_pattern: %s" s)(* Something went wrong. *)
+      (* We were not in a match *)
+      let s = Mbrowse.print_node () parent in
+      raise  (Not_allowed s)
 
 let rec destructible patt =
   let open Typedtree in
@@ -325,22 +358,53 @@ let rec rm_sub patt sub =
   | Tpat_lazy p ->
     { patt with pat_desc = Tpat_lazy (f p) }
 
-let rec qualify_constructors f pat =
+let rec qualify_constructors ~unmangling_tables f pat  =
   let open Typedtree in
+  let qualify_constructors = qualify_constructors ~unmangling_tables in
   let pat_desc =
     match pat.pat_desc with
     | Tpat_alias (p, id, loc) -> Tpat_alias (qualify_constructors f p, id, loc)
     | Tpat_tuple ps -> Tpat_tuple (List.map ps ~f:(qualify_constructors f))
     | Tpat_record (labels, closed) ->
       let labels =
+        let open Longident in
         List.map labels
-          ~f:(fun (lid, descr, pat) -> lid, descr, qualify_constructors f pat)
+          ~f:(fun ((Location.{ txt ; _ } as lid), lbl_des, pat) ->
+            let lid_name = flatten txt |> String.concat ~sep:"." in
+            let pat = qualify_constructors f pat in
+            (* Un-mangle *)
+            match unmangling_tables with
+            | Some (_, labels) ->
+              (match Hashtbl.find_opt labels lid_name with
+              | Some lbl_des -> (
+                  { lid with txt = Lident lbl_des.Types.lbl_name },
+                  lbl_des,
+                  pat
+                )
+              | None -> (lid, lbl_des, pat))
+            | None -> (lid, lbl_des, pat))
+      in
+      let closed =
+        if List.length labels > 0 then
+          let _, lbl_des, _ = List.hd labels in
+          if List.length labels = Array.length lbl_des.Types.lbl_all then
+            Asttypes.Closed
+          else Asttypes.Open
+        else closed
       in
       Tpat_record (labels, closed)
     | Tpat_construct (lid, cstr_desc, ps) ->
       let lid =
         match lid.Asttypes.txt with
         | Longident.Lident name ->
+          (* Un-mangle *)
+          let name = match unmangling_tables with
+            | Some (constrs, _) ->
+              (match  Hashtbl.find_opt constrs name with
+              | Some cstr_des -> cstr_des.Types.cstr_name
+              | None -> name)
+            | None -> name
+          in
           begin match (Btype.repr pat.pat_type).Types.desc with
           | Types.Tconstr (path, _, _) ->
             let path = f pat.pat_env path in
@@ -425,80 +489,94 @@ let node config source node parents =
     let str = if needs_parentheses then "(" ^ str ^ ")" else str in
     loc, str
   | Pattern patt ->
-    begin match Typedtree.classify_pattern patt with
-    | Computation -> raise (Not_allowed ("computation pattern"));
-    | Value ->
-      let _patt : Typedtree.value Typedtree.general_pattern = patt in
-      let last_case_loc, patterns = get_every_pattern parents in
+    begin let last_case_loc, patterns = get_every_pattern parents in
       (* Printf.eprintf "tot %d o%!"(List.length patterns); *)
       List.iter patterns ~f:(fun p ->
         let p = filter_pat_attr (Untypeast.untype_pattern p) in
         log ~title:"EXISTING" "%t"
           (fun () -> Mreader.print_pretty config source (Pretty_pattern p))
       ) ;
       let pss = List.map patterns ~f:(fun x -> [ x ]) in
-      begin match Parmatch.complete_partial pss with
-      | Some pat ->
-        let pat  = qualify_constructors Printtyp.shorten_type_path pat in
+      let m, e_typ = get_match parents in
+      let pred = Typecore.partial_pred
+        ~lev:Btype.generic_level
+        m.Typedtree.exp_env
+        e_typ
+      in
+      begin match Parmatch.complete_partial ~pred pss with
+      | Some pat, unmangling_tables ->
+        (* Unmangling and prefixing *)
+        let pat =
+          qualify_constructors ~unmangling_tables Printtyp.shorten_type_path pat
+        in
+
+        (* Untyping and casing *)
         let ppat = filter_pat_attr (Untypeast.untype_pattern pat) in
         let case = Ast_helper.Exp.case ppat placeholder in
         let loc =
           let open Location in
           { last_case_loc with loc_start = last_case_loc.loc_end }
         in
+
+        (* Pretty printing *)
         let str = Mreader.print_pretty
             config source (Pretty_case_list [ case ]) in
         loc, str
-      | None ->
-       if not (destructible patt) then raise Nothing_to_do else
-        let ty = patt.Typedtree.pat_type in
-        begin match gen_patterns patt.Typedtree.pat_env ty with
-        | [] -> assert false (* we raise Not_allowed, but never return [] *)
-        | [ more_precise ] ->
-          (* If only one pattern is generated, then we're only refining the
-            current pattern, not generating new branches. *)
-          let ppat = filter_pat_attr (Untypeast.untype_pattern more_precise) in
-          let str = Mreader.print_pretty
-              config source (Pretty_pattern ppat) in
-          patt.Typedtree.pat_loc, str
-        | sub_patterns ->
-          let rev_before, after, top_patt =
-            find_branch patterns patt
-          in
-          let new_branches =
-            List.map sub_patterns ~f:(fun by ->
-              subst_patt patt ~by top_patt
-            )
-          in
-          let patterns =
-            List.rev_append rev_before
-              (List.append new_branches after)
-          in
-          let unused = Parmatch.return_unused patterns in
-          let new_branches =
-            List.fold_left unused ~init:new_branches ~f:(fun branches u ->
-              match u with
-              | `Unused p -> List.remove ~phys:true p branches
-              | `Unused_subs (p, lst) ->
-                List.map branches ~f:(fun branch ->
-                  if branch != p then branch else
-                  List.fold_left lst ~init:branch ~f:rm_sub
+      | None, _ ->
+        begin match Typedtree.classify_pattern patt with
+        | Computation -> raise (Not_allowed ("computation pattern"));
+        | Value ->
+          let _patt : Typedtree.value Typedtree.general_pattern = patt in
+          if not (destructible patt) then raise Nothing_to_do else
+            let ty = patt.Typedtree.pat_type in
+            begin match gen_patterns patt.Typedtree.pat_env ty with
+            | [] -> assert false (* we raise Not_allowed, but never return [] *)
+            | [ more_precise ] ->
+              (* If only one pattern is generated, then we're only refining the
+                current pattern, not generating new branches. *)
+              let ppat = filter_pat_attr (Untypeast.untype_pattern more_precise) in
+              let str = Mreader.print_pretty
+                  config source (Pretty_pattern ppat) in
+              patt.Typedtree.pat_loc, str
+            | sub_patterns ->
+              let rev_before, after, top_patt =
+                find_branch patterns patt
+              in
+              let new_branches =
+                List.map sub_patterns ~f:(fun by ->
+                  subst_patt patt ~by top_patt
                 )
-            )
-          in
-          match new_branches with
-          | [] -> raise Useless_refine
-          | p :: ps ->
-            let p =
-              List.fold_left ps ~init:p ~f:(fun acc p ->
-                Tast_helper.Pat.pat_or top_patt.Typedtree.pat_env
-                  top_patt.Typedtree.pat_type acc p
-              )
-            in
-            let ppat = filter_pat_attr (Untypeast.untype_pattern p) in
-            let str = Mreader.print_pretty
-                config source (Pretty_pattern ppat) in
-            top_patt.Typedtree.pat_loc, str
+              in
+              let patterns =
+                List.rev_append rev_before
+                  (List.append new_branches after)
+              in
+              let unused = Parmatch.return_unused patterns in
+              let new_branches =
+                List.fold_left unused ~init:new_branches ~f:(fun branches u ->
+                  match u with
+                  | `Unused p -> List.remove ~phys:true p branches
+                  | `Unused_subs (p, lst) ->
+                    List.map branches ~f:(fun branch ->
+                      if branch != p then branch else
+                      List.fold_left lst ~init:branch ~f:rm_sub
+                    )
+                )
+              in
+              match new_branches with
+              | [] -> raise Useless_refine
+              | p :: ps ->
+                let p =
+                  List.fold_left ps ~init:p ~f:(fun acc p ->
+                    Tast_helper.Pat.pat_or top_patt.Typedtree.pat_env
+                      top_patt.Typedtree.pat_type acc p
+                  )
+                in
+                let ppat = filter_pat_attr (Untypeast.untype_pattern p) in
+                let str = Mreader.print_pretty
+                    config source (Pretty_pattern ppat) in
+                top_patt.Typedtree.pat_loc, str
+            end
         end
       end
     end