From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 7 Nov 2005 18:46:02 +0000 (+0000)
Subject: Avoid generation of let x = let rec x = ... in x in (x ...).
X-Git-Tag: V_0_7_2_3~113
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8c3e5ceb384228d52f8938569ac3151269071445;p=helm.git

Avoid generation of let x = let rec x = ... in x in (x ...).
---

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index f203e6d79..a245053c6 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -109,6 +109,7 @@ let find_in_context name (context: Cic.name list) =
 
 let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
   assert (uri = None);
+prerr_endline "ciao";
   let rec aux loc (context: Cic.name list) = function
     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
         aux loc context term
@@ -213,14 +214,22 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
           | `Inductive ->
               (fun (var, _, _, _) cic ->
                 incr counter;
-                Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
+                let fix = Cic.Fix (!counter,funs) in
+                 match cic with
+                    Cic.Rel 1 -> fix
+                  | (Cic.Appl (Cic.Rel 1::l)) -> Cic.Appl (fix::l)
+                  | _ -> Cic.LetIn (Cic.Name var, fix, cic))
           | `CoInductive ->
               let funs =
                 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
               in
               (fun (var, _, _, _) cic ->
                 incr counter;
-                Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
+                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))
         in
         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
     | CicNotationPt.Ident _