1. Bug fixed: compilation of "let corec" to a simple CoFix without a surrounding

   let...in was bugged (because of a missing delifting). Fixed.
2. Localization is no longer lost in the body of a "let rec" or a "let corec"

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index fd8e2a7991e69204ea2a1ec028cea7569460f8ef..1bb8ac9550570c0e1883a86a2dbe753cfe10e5e5 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -127,20 +127,21 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
      ~localization_tbl
 =
   assert (uri = None);
-  let rec aux loc (context: Cic.name list) = function
+  let rec aux ~localize loc (context: Cic.name list) = function
     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
-        let res = aux loc context term in
-         Cic.CicHash.add localization_tbl res loc;
+        let res = aux ~localize loc context term in
+         if localize then Cic.CicHash.add localization_tbl res loc;
          res
-    | CicNotationPt.AttributedTerm (_, term) -> aux loc context term
+    | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
     | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
-        let cic_args = List.map (aux loc context) args in
+        let cic_args = List.map (aux ~localize loc context) args in
         resolve env (Symbol (symb, i)) ~args:cic_args ()
-    | CicNotationPt.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
+    | CicNotationPt.Appl terms ->
+       Cic.Appl (List.map (aux ~localize loc context) terms)
     | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
-        let cic_type = aux_option loc context (Some `Type) typ in
+        let cic_type = aux_option ~localize loc context (Some `Type) typ in
         let cic_name = CicNotationUtil.cic_name_of_name var in
-        let cic_body = aux loc (cic_name :: context) body in
+        let cic_body = aux ~localize loc (cic_name :: context) body in
         (match binder_kind with
         | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
         | `Pi
@@ -149,18 +150,18 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
             resolve env (Symbol ("exists", 0))
               ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
     | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
-        let cic_term = aux loc context term in
-        let cic_outtype = aux_option loc context None outtype in
+        let cic_term = aux ~localize loc context term in
+        let cic_outtype = aux_option ~localize loc context None outtype in
         let do_branch ((head, _, args), term) =
           let rec do_branch' context = function
-            | [] -> aux loc context term
+            | [] -> aux ~localize loc context term
             | (name, typ) :: tl ->
                 let cic_name = CicNotationUtil.cic_name_of_name name in
                 let cic_body = do_branch' (cic_name :: context) tl in
                 let typ =
                   match typ with
                   | None -> Cic.Implicit (Some `Type)
-                  | Some typ -> aux loc context typ
+                  | Some typ -> aux ~localize loc context typ
                 in
                 Cic.Lambda (cic_name, typ, cic_body)
           in
@@ -194,18 +195,18 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
           (List.map do_branch branches))
     | CicNotationPt.Cast (t1, t2) ->
-        let cic_t1 = aux loc context t1 in
-        let cic_t2 = aux loc context t2 in
+        let cic_t1 = aux ~localize loc context t1 in
+        let cic_t2 = aux ~localize loc context t2 in
         Cic.Cast (cic_t1, cic_t2)
     | CicNotationPt.LetIn ((name, typ), def, body) ->
-        let cic_def = aux loc context def in
+        let cic_def = aux ~localize loc context def in
         let cic_name = CicNotationUtil.cic_name_of_name name in
         let cic_def =
           match typ with
           | None -> cic_def
-          | Some t -> Cic.Cast (cic_def, aux loc context t)
+          | Some t -> Cic.Cast (cic_def, aux ~localize loc context t)
         in
-        let cic_body = aux loc (cic_name :: context) body in
+        let cic_body = aux ~localize loc (cic_name :: context) body in
         Cic.LetIn (cic_name, cic_def, cic_body)
     | CicNotationPt.LetRec (kind, defs, body) ->
         let context' =
@@ -214,12 +215,50 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
               CicNotationUtil.cic_name_of_name name :: acc)
             context defs
         in
-        let cic_body = aux loc context' body in
+        let cic_body =
+         let unlocalized_body = aux ~localize:false loc context' body in
+         match unlocalized_body with
+            Cic.Rel 1 -> `AvoidLetInNoAppl
+          | Cic.Appl (Cic.Rel 1::l) ->
+             (try
+               let l' =
+                List.map
+                 (function t ->
+                   let t',subst,metasenv =
+                    CicMetaSubst.delift_rels [] [] 1 t
+                   in
+                    assert (subst=[]);
+                    assert (metasenv=[]);
+                    t') l
+               in
+                (* We can avoid the LetIn. But maybe we need to recompute l'
+                   so that it is localized *)
+                if localize then
+                 match body with
+                    CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
+                     let l' = List.map (aux ~localize loc context) l in
+                      `AvoidLetIn l'
+                  | _ -> assert false
+                else
+                 `AvoidLetIn l'
+              with
+               CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+                if localize then
+                 `AddLetIn (aux ~localize loc context' body)
+                else
+                 `AddLetIn unlocalized_body)
+          | _ ->
+             if localize then
+              `AddLetIn (aux ~localize loc context' body)
+             else
+              `AddLetIn unlocalized_body
+        in
         let inductiveFuns =
           List.map
             (fun ((name, typ), body, decr_idx) ->
-              let cic_body = aux loc context' body in
-              let cic_type = aux_option loc context (Some `Type) typ in
+              let cic_body = aux ~localize loc context' body in
+              let cic_type =
+               aux_option ~localize loc context (Some `Type) typ in
               let name =
                 match CicNotationUtil.cic_name_of_name name with
                 | Cic.Anonymous ->
@@ -241,24 +280,11 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
                 incr counter;
                 let fix = Cic.Fix (!counter,funs) in
                  match cic with
-                    Cic.Rel 1 -> fix
-                  | (Cic.Appl (Cic.Rel 1::l)) ->
-                     (try
-                       let l' =
-                        List.map
-                         (function t ->
-                           let t',subst,metasenv =
-                            CicMetaSubst.delift_rels [] [] 1 t
-                           in
-                            assert (subst=[]);
-                            assert (metasenv=[]);
-                            t') l
-                       in
-                        Cic.Appl (fix::l')
-                      with
-                       CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
-                        Cic.LetIn (Cic.Name var, fix, cic))
-                  | _ -> Cic.LetIn (Cic.Name var, fix, cic))
+                    `Recipe (`AddLetIn cic) ->
+                      `Term (Cic.LetIn (Cic.Name var, fix, cic))
+                  | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (fix::l))
+                  | `Recipe `AvoidLetInNoAppl -> `Term fix
+                  | `Term t -> `Term (Cic.LetIn (Cic.Name var, fix, t)))
           | `CoInductive ->
               let funs =
                 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
@@ -267,11 +293,18 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
                 incr counter;
                 let cofix = Cic.CoFix (!counter,funs) in
                  match cic with
-                    Cic.Rel 1 -> cofix
-                  | (Cic.Appl (Cic.Rel 1::l)) -> Cic.Appl (cofix::l)
-                  | _ -> Cic.LetIn (Cic.Name var, cofix, cic))
+                    `Recipe (`AddLetIn cic) ->
+                      `Term (Cic.LetIn (Cic.Name var, cofix, cic))
+                  | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (cofix::l))
+                  | `Recipe `AvoidLetInNoAppl -> `Term cofix
+                  | `Term t -> `Term (Cic.LetIn (Cic.Name var, cofix, t)))
         in
-        List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
+         (match
+           List.fold_right (build_term inductiveFuns) inductiveFuns
+            (`Recipe cic_body)
+          with
+             `Recipe _ -> assert false
+           | `Term t -> t)
     | CicNotationPt.Ident _
     | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
     | CicNotationPt.Ident (name, subst)
@@ -302,7 +335,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
                 List.map
                   (fun (s, term) ->
                     (try
-                      List.assoc s ids_to_uris, aux loc context term
+                      List.assoc s ids_to_uris, aux ~localize loc context term
                      with Not_found ->
                        raise (Invalid_choice (lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
                   subst
@@ -358,7 +391,9 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
     | CicNotationPt.Meta (index, subst) ->
         let cic_subst =
           List.map
-            (function None -> None | Some term -> Some (aux loc context term))
+            (function
+                None -> None
+              | Some term -> Some (aux ~localize loc context term))
             subst
         in
         Cic.Meta (index, cic_subst)
@@ -369,11 +404,11 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
     | CicNotationPt.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
     | _ -> assert false (* god bless Bologna *)
-  and aux_option loc (context: Cic.name list) annotation = function
+  and aux_option ~localize loc (context: Cic.name list) annotation = function
     | None -> Cic.Implicit annotation
-    | Some term -> aux loc context term
+    | Some term -> aux ~localize loc context term
   in
-   aux dummy_floc context ast
+   aux ~localize:true dummy_floc context ast
 
 let interpretate_path ~context path =
  let localization_tbl = Cic.CicHash.create 23 in