Procedural: 2 bug fix in eta expansion + 1 bug fix in pattern generation

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

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 9dc19c7c6a3b281056d4c0c9c640b41d58217a43..1a318362500e115107a1312cdf46bcd0294aeb30 100644 (file)
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -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)
@@ -694,7 +684,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
                   CicNotationUtil.cic_name_of_name var :: context,
                   domain_of_term_option ~loc ~context ty @ res)
                 (add_defs context,[]) params))
-            @ domain_of_term_option ~loc ~context typ
+            @ domain_of_term_option ~loc ~context:context' typ
             @ domain_of_term ~loc ~context:context' body
           ) [] defs
       in
@@ -838,7 +828,7 @@ sig
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
-    CicNotationPt.obj disambiguator_input ->
+    CicNotationPt.term CicNotationPt.obj disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *
@@ -1204,7 +1194,7 @@ in refine_profiler.HExtlib.profile foo ()
         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
       in
       disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
-        ~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj
+        ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
         (text,prefix_len,obj)
   end