X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=667c50770536bb7187df52a2cc460991b32cf20f;hb=f1dc70ca55058b2983cd23b829d856df3b41b9a7;hp=fd8e2a7991e69204ea2a1ec028cea7569460f8ef;hpb=afa05d30f20de12e031c3e5c3e5c33c19c42a7d8;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index fd8e2a799..667c50770 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -23,13 +23,16 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 open DisambiguateTypes
 open UriManager
 
+(* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
- (Token.flocation option * string Lazy.t) list
+ int * (Token.flocation option * string Lazy.t) list
 exception PathNotWellFormed
 
   (** raised when an environment is not enough informative to decide *)
@@ -115,7 +118,7 @@ let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?
       (DisambiguateTypes.string_of_domain_item item))
 
   (* TODO move it to Cic *)
-let find_in_context name (context: Cic.name list) =
+let find_in_context name context =
   let rec aux acc = function
     | [] -> raise Not_found
     | Cic.Name hd :: tl when hd = name -> acc
@@ -127,20 +130,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 +153,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 +198,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 +218,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 +283,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 +296,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 +338,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 +394,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 +407,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 HExtlib.dummy_floc context ast
 
 let interpretate_path ~context path =
  let localization_tbl = Cic.CicHash.create 23 in
@@ -409,15 +447,6 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
           i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
         ) (0,[]) tyl) in
      let con_env = DisambiguateTypes.env_of_list name_to_uris env in
-     let undebrujin t =
-      snd
-       (List.fold_right
-         (fun (name,_,_,_) (i,t) ->
-           (*here the explicit_named_substituion is assumed to be of length 0 *)
-           let t' = Cic.MutInd (uri,i,[])  in
-           let t = CicSubstitution.subst t' t in
-            i - 1,t
-         ) tyl (List.length tyl - 1,t)) in
      let tyl =
       List.map
        (fun (name,b,ty,cl) ->
@@ -428,7 +457,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
              let ty' =
               add_params (interpretate_term context con_env None false ty)
              in
-              name,undebrujin ty'
+              name,ty'
            ) cl
          in
           name,b,ty',cl'
@@ -453,7 +482,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
      let fields' =
       snd (
        List.fold_left
-        (fun (context,res) (name,ty) ->
+        (fun (context,res) (name,ty,_coercion) ->
           let context' = Cic.Name name :: context in
            context',(name,interpretate_term context env None false ty)::res
         ) (context,[]) fields) in
@@ -470,7 +499,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
        concl fields' in
      let con' = add_params con in
      let tyl = [name,true,ty',["mk_" ^ name,con']] in
-     let field_names = List.map fst fields in
+     let field_names = List.map (fun (x,_,y) -> x,y) fields in
       Cic.InductiveDefinition
        (tyl,[],List.length params,[`Class (`Record field_names)])
   | CicNotationPt.Theorem (flavour, name, ty, bo) ->
@@ -509,7 +538,7 @@ let rev_uniq =
 (* "aux" keeps domain in reverse order and doesn't care about duplicates.
  * Domain item more in deep in the list will be processed first.
  *)
-let rec domain_rev_of_term ?(loc = dummy_floc) context = function
+let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
   | CicNotationPt.AttributedTerm (`Loc loc, term) ->
      domain_rev_of_term ~loc context term
   | CicNotationPt.AttributedTerm (_, term) ->
@@ -585,7 +614,8 @@ let rec domain_rev_of_term ?(loc = dummy_floc) context = function
       where_dom @ defs_dom
   | CicNotationPt.Ident (name, subst) ->
       (try
-        let index = find_in_context name context in
+        (* the next line can raise Not_found *)
+        ignore(find_in_context name context);
         if subst <> None then
           CicNotationPt.fail loc "Explicit substitutions not allowed here"
         else
@@ -652,18 +682,18 @@ let domain_of_obj ~context ast =
    | CicNotationPt.Record (params,_,ty,fields) ->
       let dom =
        List.flatten
-        (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
+        (List.rev_map (fun (_,ty,_) -> domain_rev_of_term [] ty) fields) in
       let dom =
-       List.filter
-        (fun name->
-          not (  List.exists (fun (name',_) -> name = Id name') params
-              || List.exists (fun (name',_) -> name = Id name') fields)
-        ) dom
-      in
        List.fold_left
         (fun dom (_,ty) ->
           domain_rev_of_term [] ty @ dom
         ) (dom @ domain_rev_of_term [] ty) params
+      in
+       List.filter
+        (fun name->
+          not (  List.exists (fun (name',_) -> name = Id name') params
+              || List.exists (fun (name',_,_) -> name = Id name') fields)
+        ) dom
  in
   rev_uniq domain_rev
 
@@ -927,7 +957,7 @@ in refine_profiler.HExtlib.profile foo ()
       try
         let res =
          match aux aliases [] None todo_dom base_univ with
-         | [],errors -> raise (NoWellTypedInterpretation errors)
+         | [],errors -> raise (NoWellTypedInterpretation (0,errors))
          | [_,diff,metasenv,t,ugraph],_ ->
              debug_print (lazy "SINGLE INTERPRETATION");
              [diff,metasenv,t,ugraph], false