X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_disambiguation%2Fdisambiguate.ml;h=f3600b7cbc34602ba9e8a433ae853aaf66f4d3b8;hb=70c533b5592b0bb91f544fec275213b866bf33ea;hp=fb4c338a447ee040ac8c4ecb63dfad86c149b31d;hpb=59c85666e58d43d1dce56a2456db5f1ec223c1c3;p=helm.git

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index fb4c338a4..f3600b7cb 100644
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -32,7 +32,10 @@ open UriManager
 
 (* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
- int * (Token.flocation option * string Lazy.t) list
+ int *
+ ((Token.flocation list * string * string) list *
+  (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+  Token.flocation option * string Lazy.t) list
 exception PathNotWellFormed
 
   (** raised when an environment is not enough informative to decide *)
@@ -215,7 +218,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
     | CicNotationPt.LetRec (kind, defs, body) ->
         let context' =
           List.fold_left
-            (fun acc ((name, _), _, _) ->
+            (fun acc (_, (name, _), _, _) ->
               CicNotationUtil.cic_name_of_name name :: acc)
             context defs
         in
@@ -259,10 +262,16 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
         in
         let inductiveFuns =
           List.map
-            (fun ((name, typ), body, decr_idx) ->
-              let cic_body = aux ~localize loc context' body in
+            (fun (params, (name, typ), body, decr_idx) ->
+              let add_binders kind t =
+               List.fold_right
+                (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
+              in
+              let cic_body =
+               aux ~localize loc context' (add_binders `Lambda body) in
               let cic_type =
-               aux_option ~localize loc context (Some `Type) typ in
+               aux_option ~localize loc context (Some `Type)
+                (HExtlib.map_option (add_binders `Pi) typ) in
               let name =
                 match CicNotationUtil.cic_name_of_name name with
                 | Cic.Anonymous ->
@@ -432,14 +441,17 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
       let context,res =
        List.fold_left
         (fun (context,res) (name,t) ->
-          Cic.Name name :: context,
-          (name, interpretate_term context env None false t)::res
+          let t =
+           match t with
+              None -> CicNotationPt.Implicit
+            | Some t -> t in
+          let name = CicNotationUtil.cic_name_of_name name in
+           name::context,(name, interpretate_term context env None false t)::res
         ) ([],[]) params
       in
        context,List.rev res in
      let add_params =
-      List.fold_right
-       (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
+      List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
      let name_to_uris =
       snd (
        List.fold_left
@@ -471,14 +483,18 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
       let context,res =
        List.fold_left
         (fun (context,res) (name,t) ->
-          (Cic.Name name :: context),
-          (name, interpretate_term context env None false t)::res
+          let t =
+           match t with
+              None -> CicNotationPt.Implicit
+            | Some t -> t in
+          let name = CicNotationUtil.cic_name_of_name name in
+           name::context,(name, interpretate_term context env None false t)::res
         ) ([],[]) params
       in
        context,List.rev res in
      let add_params =
       List.fold_right
-       (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
+       (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
      let ty' = add_params (interpretate_term context env None false ty) in
      let fields' =
       snd (
@@ -562,7 +578,7 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
         | `Exists -> [ loc, Symbol ("exists", 0) ]
         | _ -> []
       in
-      let type_dom = domain_rev_of_term_option loc context typ in
+      let type_dom = domain_rev_of_term_option ~loc context typ in
       let body_dom =
         domain_rev_of_term ~loc
           (CicNotationUtil.cic_name_of_name var :: context) body
@@ -607,19 +623,31 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
       in
       where_dom @ type_dom @ body_dom
   | CicNotationPt.LetRec (kind, defs, where) ->
-      let context' =
+      let add_defs context =
         List.fold_left
-          (fun acc ((var, typ), _, _) ->
-            CicNotationUtil.cic_name_of_name var :: acc)
-          context defs
-      in
-      let where_dom = domain_rev_of_term ~loc context' where in
+          (fun acc (_, (var, _), _, _) ->
+            CicNotationUtil.cic_name_of_name var :: acc
+          ) context defs in
+      let where_dom = domain_rev_of_term ~loc (add_defs context) where in
       let defs_dom =
         List.fold_left
-          (fun dom ((_, typ), body, _) ->
+          (fun dom (params, (_, typ), body, _) ->
+            let context' =
+             add_defs
+              (List.fold_left
+                (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc)
+                context params)
+            in
             domain_rev_of_term ~loc context' body @
-            domain_rev_of_term_option loc context typ)
-          [] defs
+            domain_rev_of_term_option ~loc context typ @
+            List.rev
+             (snd
+               (List.fold_left
+                (fun (context,res) (var,ty) ->
+                  CicNotationUtil.cic_name_of_name var :: context,
+                  res @ domain_rev_of_term_option ~loc context ty)
+                (add_defs context,[]) params))
+          ) [] defs
       in
       where_dom @ defs_dom
   | CicNotationPt.Ident (name, subst) ->
@@ -654,7 +682,7 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
   | CicNotationPt.Magic _
   | CicNotationPt.Variable _ -> assert false
 
-and domain_rev_of_term_option loc context = function
+and domain_rev_of_term_option ~loc context = function
   | None -> []
   | Some t -> domain_rev_of_term ~loc context t
 
@@ -681,12 +709,17 @@ let domain_of_obj ~context ast =
       let dom = 
        List.fold_left
         (fun dom (_,ty) ->
-          domain_rev_of_term [] ty @ dom
+          match ty with
+             None -> dom
+           | Some ty -> domain_rev_of_term [] ty @ dom
         ) dom params
       in
        List.filter
         (fun (_,name) ->
-          not (  List.exists (fun (name',_) -> name = Id name') params
+          not (  List.exists (fun (name',_) ->
+                  match CicNotationUtil.cic_name_of_name name' with
+                     Cic.Anonymous -> false
+                   | Cic.Name name' -> name = Id name') params
               || List.exists (fun (name',_,_,_) -> name = Id name') tyl)
         ) dom
    | CicNotationPt.Record (params,_,ty,fields) ->
@@ -694,14 +727,19 @@ let domain_of_obj ~context ast =
        List.flatten
         (List.rev_map (fun (_,ty,_,_) -> domain_rev_of_term [] ty) fields) in
       let dom =
-       List.fold_left
-        (fun dom (_,ty) ->
-          domain_rev_of_term [] ty @ dom
-        ) (dom @ domain_rev_of_term [] ty) params
+       List.fold_right
+        (fun (_,ty) dom ->
+          match ty with
+             None -> dom
+           | Some ty -> dom @ domain_rev_of_term [] ty
+        ) params (dom @ domain_rev_of_term [] ty)
       in
        List.filter
         (fun (_,name) ->
-          not (  List.exists (fun (name',_) -> name = Id name') params
+          not (  List.exists (fun (name',_) ->
+                  match CicNotationUtil.cic_name_of_name name' with
+                     Cic.Anonymous -> false
+                   | Cic.Name name' -> name = Id name') params
               || List.exists (fun (name',_,_,_) -> name = Id name') fields)
         ) dom
  in
@@ -828,8 +866,11 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
               match item with
               | Id id -> choices_of_id dbd id
               | Symbol (symb, _) ->
-                  List.map DisambiguateChoices.mk_choice
+                 (try
+                   List.map DisambiguateChoices.mk_choice
                     (TermAcicContent.lookup_interpretations symb)
+                  with
+                   TermAcicContent.Interpretation_not_found -> [])
               | Num instance ->
                   DisambiguateChoices.lookup_num_choices ()
             in
@@ -910,7 +951,8 @@ in refine_profiler.HExtlib.profile foo ()
             (match test_env aliases [] base_univ with
             | Ok (thing, metasenv),new_univ -> 
                [ aliases, diff, metasenv, thing, new_univ ], []
-            | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg])
+            | Ko (loc,msg),_
+            | Uncertain (loc,msg),_ -> [],[aliases,diff,loc,msg])
         | (locs,item) :: remaining_dom ->
             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
              (string_of_domain_item item)));
@@ -920,7 +962,8 @@ in refine_profiler.HExtlib.profile foo ()
               | Some choices -> choices in
             match choices with
                [] ->
-                [], [Some (List.hd locs),
+                [], [aliases, diff,
+                     Some (List.hd locs),
                      lazy ("No choices for " ^ string_of_domain_item item)]
              | [codomain_item] ->
                  (* just one choice. We perform a one-step look-up and
@@ -950,11 +993,11 @@ in refine_profiler.HExtlib.profile foo ()
                             remaining_dom new_univ)
                     | Uncertain (loc,msg),new_univ ->
                         (match remaining_dom with
-                        | [] -> [], [loc,msg]
+                        | [] -> [], [new_env,new_diff,loc,msg]
                         | _ ->
                            aux new_env new_diff lookup_in_todo_dom
                             remaining_dom new_univ)
-                    | Ko (loc,msg),_ -> [], [loc,msg])
+                    | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg])
              | _::_ ->
                let rec filter univ = function 
                 | [] -> [],[]
@@ -965,25 +1008,50 @@ in refine_profiler.HExtlib.profile foo ()
                     (match test_env new_env remaining_dom univ with
                     | Ok (thing, metasenv),new_univ ->
                         (match remaining_dom with
-                        | [] -> [ new_env, new_diff, metasenv, thing, new_univ ], []
+                        | [] -> [new_env,new_diff,metasenv,thing,new_univ], []
                         | _ -> aux new_env new_diff None remaining_dom new_univ
                         ) @@ 
                           filter univ tl
                     | Uncertain (loc,msg),new_univ ->
                         (match remaining_dom with
-                        | [] -> [],[loc,msg]
+                        | [] -> [],[new_env,new_diff,loc,msg]
                         | _ -> aux new_env new_diff None remaining_dom new_univ
                         ) @@ 
                           filter univ tl
-                    | Ko (loc,msg),_ -> ([],[loc,msg]) @@ filter univ tl)
+                    | Ko (loc,msg),_ -> ([],[new_env,new_diff,loc,msg]) @@ filter univ tl)
                in
                 filter base_univ choices
       in
+      let aux' aliases diff lookup_in_todo_dom todo_dom base_univ =
+       match test_env aliases todo_dom base_univ with
+        | Ok _,_
+        | Uncertain _,_ ->
+           aux aliases diff lookup_in_todo_dom todo_dom base_univ
+        | Ko (loc,msg),_ -> ([],[aliases,diff,loc,msg]) in
       let base_univ = initial_ugraph in
       try
         let res =
-         match aux aliases [] None todo_dom base_univ with
-         | [],errors -> raise (NoWellTypedInterpretation (0,errors))
+         match aux' aliases [] None todo_dom base_univ with
+         | [],errors ->
+            let errors =
+             List.map
+              (fun (env,diff,loc,msg) ->
+                let env' =
+                 HExtlib.filter_map
+                   (fun (locs,domain_item) ->
+                     try
+                      let description =
+                       fst (Environment.find domain_item env)
+                      in
+                       Some (locs,descr_of_domain_item domain_item,description)
+                     with
+                      Not_found -> None)
+                   thing_dom
+                in
+                 env',diff,loc,msg
+              ) errors
+            in
+             raise (NoWellTypedInterpretation (0,errors))
          | [_,diff,metasenv,t,ugraph],_ ->
              debug_print (lazy "SINGLE INTERPRETATION");
              [diff,metasenv,t,ugraph], false