X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=9effb6ae466b301b5896e783e0f600397cb73f05;hb=3007de3f032ea2349cb2f8fffc76b18d26895f36;hp=d58dc9854bceef447083e2ff628bfe99ef6eee91;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index d58dc9854..9effb6ae4 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -103,8 +103,8 @@ let descr_of_domain_item = function
  | Symbol (s, _) -> s
  | Num i -> string_of_int i
 
-type 'a test_result =
-  | Ok of 'a * Cic.metasenv
+type ('a,'m) test_result =
+  | Ok of 'a * 'm
   | Ko of Stdpp.location option * string Lazy.t
   | Uncertain of Stdpp.location option * string Lazy.t
 
@@ -172,12 +172,12 @@ let find_in_context name context =
   in
   aux 1 context
 
-let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~uri ~is_path ast
+let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
      ~localization_tbl
 =
   (* create_dummy_ids shouldbe used only for interpretating patterns *)
   assert (uri = None);
-  let rec aux ~localize loc (context: Cic.name list) = function
+  let rec aux ~localize loc context = function
     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
         let res = aux ~localize loc context term in
          if localize then Cic.CicHash.add localization_tbl res loc;
@@ -255,7 +255,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                 raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
            ) branches
          else
-         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with
+         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
             Cic.InductiveDefinition (il,_,leftsno,_) ->
              let _,_,_,cl =
               try
@@ -380,6 +380,8 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                 if localize then
                  match body with
                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
+                     (* since we avoid the letin, the context has no
+                      * recfuns in it *)
                      let l' = List.map (aux ~localize loc context) l in
                       `AvoidLetIn (n,l')
                   | _ -> assert false
@@ -484,16 +486,16 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
           (try 
             match cic with
             | Cic.Const (uri, []) ->
-                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
                 let uris = CicUtil.params_of_obj o in
                 Cic.Const (uri, mk_subst uris)
             | Cic.Var (uri, []) ->
-                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
                 let uris = CicUtil.params_of_obj o in
                 Cic.Var (uri, mk_subst uris)
             | Cic.MutInd (uri, i, []) ->
                (try
-                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
                  let uris = CicUtil.params_of_obj o in
                  Cic.MutInd (uri, i, mk_subst uris)
                 with
@@ -506,7 +508,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                   (*here the explicit_named_substituion is assumed to be of length 0 *)
                   Cic.MutInd (uri,i,[]))
             | Cic.MutConstruct (uri, i, j, []) ->
-                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
                 let uris = CicUtil.params_of_obj o in
                 Cic.MutConstruct (uri, i, j, mk_subst uris)
             | Cic.Meta _ | Cic.Implicit _ as t ->
@@ -540,11 +542,11 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
-    | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
+    | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
     | CicNotationPt.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
     | _ -> assert false (* god bless Bologna *)
-  and aux_option ~localize loc (context: Cic.name list) annotation = function
+  and aux_option ~localize loc context annotation = function
     | None -> Cic.Implicit annotation
     | Some term -> aux ~localize loc context term
   in
@@ -659,6 +661,16 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
       | Some bo,_ ->
          let bo' = Some (interpretate_term [] env None false bo) in
           Cic.Constant (name,bo',ty',[],attrs))
+;;
+
+let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
+     ~localization_tbl
+=
+  let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
+interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
+~localization_tbl
+;;
+
           
 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
   | Ast.AttributedTerm (`Loc loc, term) ->
@@ -785,6 +797,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))
+            @ dom
             @ domain_of_term_option ~loc ~context:context' typ
             @ domain_of_term ~loc ~context:context' body
           ) [] defs
@@ -831,6 +844,7 @@ let domain_of_term ~context term =
  uniq_domain (domain_of_term ~context term)
 
 let domain_of_obj ~context ast =
+ let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
  assert (context = []);
   match ast with
    | Ast.Theorem (_,_,ty,bo) ->
@@ -881,6 +895,14 @@ let domain_of_obj ~context ast =
 let domain_of_obj ~context obj = 
  uniq_domain (domain_of_obj ~context obj)
 
+let domain_of_ast_term = domain_of_term;;
+
+let domain_of_term ~context term = 
+ let context = 
+   List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context 
+ in
+ domain_of_term ~context term
+
   (* dom1 \ dom2 *)
 let domain_diff dom1 dom2 =
 (* let domain_diff = Domain.diff *)
@@ -908,6 +930,33 @@ let domain_diff dom1 dom2 =
 
 module type Disambiguator =
 sig
+  val disambiguate_thing:
+    dbd:HSql.dbd ->
+    context:'context ->
+    metasenv:'metasenv ->
+    initial_ugraph:'ugraph ->
+    aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
+    universe:DisambiguateTypes.codomain_item list
+             DisambiguateTypes.Environment.t option ->
+    uri:'uri ->
+    pp_thing:('ast_thing -> string) ->
+    domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
+    interpretate_thing:(context:'context ->
+                        env:DisambiguateTypes.codomain_item
+                            DisambiguateTypes.Environment.t ->
+                        uri:'uri ->
+                        is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
+    refine_thing:('metasenv ->
+                  'context ->
+                  'uri ->
+                  'raw_thing ->
+                  'ugraph -> localization_tbl:'cichash -> ('refined_thing,
+                  'metasenv) test_result * 'ugraph) ->
+    localization_tbl:'cichash ->
+    string * int * 'ast_thing ->
+    ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
+     list * 'metasenv * 'refined_thing * 'ugraph)
+    list * bool
   val disambiguate_term :
     ?fresh_instances:bool ->
     dbd:HSql.dbd ->
@@ -976,18 +1025,14 @@ module Make (C: Callbacks) =
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
     let disambiguate_thing ~dbd ~context ~metasenv
-      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
+      ~initial_ugraph ~aliases ~universe
       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
+      ~localization_tbl
       (thing_txt,thing_txt_prefix_len,thing)
     =
       debug_print (lazy "DISAMBIGUATE INPUT");
-      let disambiguate_context =  (* cic context -> disambiguate context *)
-        List.map
-          (function None -> Cic.Anonymous | Some (name, _) -> name)
-          context
-      in
       debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
-      let thing_dom = domain_of_thing ~context:disambiguate_context thing in
+      let thing_dom = domain_of_thing ~context thing in
       debug_print
        (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
 (*
@@ -1073,9 +1118,8 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
               aux (aux env l) tl in
         let filled_env = aux aliases todo_dom in
         try
-          let localization_tbl = Cic.CicHash.create 503 in
           let cic_thing =
-            interpretate_thing ~context:disambiguate_context ~env:filled_env
+            interpretate_thing ~context ~env:filled_env
              ~uri ~is_path:false thing ~localization_tbl
           in
 let foo () =
@@ -1276,17 +1320,19 @@ in refine_profiler.HExtlib.profile foo ()
         failwith "Disambiguate: circular dependency"
 
     let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
-      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe 
+      ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe 
       (text,prefix_len,term)
     =
       let term =
         if fresh_instances then CicNotationUtil.freshen_term term else term
       in
+      let localization_tbl = Cic.CicHash.create 503 in
       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
         ~domain_of_thing:domain_of_term
         ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
         ~refine_thing:refine_term (text,prefix_len,term)
+        ~localization_tbl
 
     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
      (text,prefix_len,obj)
@@ -1294,9 +1340,14 @@ in refine_profiler.HExtlib.profile foo ()
       let obj =
         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
       in
+      let localization_tbl = Cic.CicHash.create 503 in
       disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
         ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
+        ~initial_ugraph:CicUniv.empty_ugraph
         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
+        ~localization_tbl
         (text,prefix_len,obj)
+
   end
 
+