From 8c3e5ceb384228d52f8938569ac3151269071445 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 7 Nov 2005 18:46:02 +0000 Subject: [PATCH] Avoid generation of let x = let rec x = ... in x in (x ...). --- helm/ocaml/cic_disambiguation/disambiguate.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) 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 _ -- 2.39.2