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

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 1bb8ac955..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
@@ -408,7 +411,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
     | None -> Cic.Implicit annotation
     | Some term -> aux ~localize loc context term
   in
-   aux ~localize:true 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
@@ -444,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) ->
@@ -463,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'
@@ -488,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
@@ -505,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) ->
@@ -544,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) ->
@@ -620,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
@@ -687,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
 
@@ -962,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