Several bugs fixed:

[helm.git] / components / cic_disambiguation / disambiguate.ml

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 1d4a6a61ef9ecd8a1cbf8613035014c768fc568c..5c198cb5962bf06bef7850892ba384ffe2c35618 100644 (file)
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -86,7 +86,7 @@ let uniq_domain dom =
  in
   snd (aux [] dom)
 
-let debug = false
+let debug = true
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (*
@@ -267,14 +267,14 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
         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) ->
+            Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
+          | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->
              (try
                let l' =
                 List.map
                  (function t ->
                    let t',subst,metasenv =
-                    CicMetaSubst.delift_rels [] [] 1 t
+                    CicMetaSubst.delift_rels [] [] (List.length defs) t
                    in
                     assert (subst=[]);
                     assert (metasenv=[]);
@@ -286,10 +286,10 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
                  match body with
                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
                      let l' = List.map (aux ~localize loc context) l in
-                      `AvoidLetIn l'
+                      `AvoidLetIn (n,l')
                   | _ -> assert false
                 else
-                 `AvoidLetIn l'
+                 `AvoidLetIn (n,l')
               with
                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
                 if localize then
@@ -324,42 +324,32 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
               (name, decr_idx, cic_type, cic_body))
             defs
         in
-        let counter = ref ~-1 in
-        let build_term funs =
-          (* this is the body of the fold_right function below. Rationale: Fix
-           * and CoFix cases differs only in an additional index in the
-           * inductiveFun list, see Cic.term *)
-          match kind with
-          | `Inductive ->
-              (fun (var, _, _, _) cic ->
-                incr counter;
-                let fix = Cic.Fix (!counter,funs) in
-                 match cic with
-                    `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)))
+        let fix_or_cofix n =
+         match kind with
+            `Inductive -> Cic.Fix (n,inductiveFuns)
           | `CoInductive ->
-              let funs =
-                List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
+              let coinductiveFuns =
+                List.map
+                 (fun (name, _, typ, body) -> name, typ, body)
+                 inductiveFuns
               in
-              (fun (var, _, _, _) cic ->
-                incr counter;
-                let cofix = Cic.CoFix (!counter,funs) in
-                 match cic with
-                    `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)))
+               Cic.CoFix (n,coinductiveFuns)
         in
-         (match
-           List.fold_right (build_term inductiveFuns) inductiveFuns
-            (`Recipe cic_body)
-          with
-             `Recipe _ -> assert false
-           | `Term t -> t)
+         let counter = ref ~-1 in
+         let build_term funs (var,_,_,_) t =
+          incr counter;
+          Cic.LetIn (Cic.Name var, fix_or_cofix !counter, t)
+         in
+          (match cic_body with
+              `AvoidLetInNoAppl n ->
+                let n' = List.length inductiveFuns - n in
+                 fix_or_cofix n'
+            | `AvoidLetIn (n,l) ->
+                let n' = List.length inductiveFuns - n in
+                 Cic.Appl (fix_or_cofix n'::l)
+            | `AddLetIn cic_body ->         
+                List.fold_right (build_term inductiveFuns) inductiveFuns
+                 cic_body)
     | CicNotationPt.Ident _
     | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
     | CicNotationPt.Ident (name, subst)