Yet another implementation of the single aliases / multi aliases idea.

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

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 5096789d964eccc1560d05fe46ce68d92c4846c7..b9aa8f844fe76a10754a088c2cc2810f3e1d7bd8 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -359,7 +359,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj =
         (fun (i,res) (name,_,_,_) ->
           i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
         ) (0,[]) tyl) in
-     let con_env = DisambiguateTypes.singleton_env_of_list name_to_uris env in
+     let con_env = DisambiguateTypes.env_of_list name_to_uris env in
      let undebrujin t =
       snd
        (List.fold_right
@@ -635,7 +635,8 @@ sig
     context:Cic.context ->
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
-    aliases:aliases ->  (* previous interpretation status *)
+    aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
+    universe:DisambiguateTypes.multiple_environment option ->
     CicNotationPt.term ->
     (environment *                   (* new interpretation status *)
      Cic.metasenv *                  (* new metasenv *)
@@ -646,7 +647,8 @@ sig
   val disambiguate_obj :
     ?fresh_instances:bool ->
     dbd:Mysql.dbd ->
-    aliases:aliases ->           (* previous interpretation status *)
+    aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
+    universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
     GrafiteAst.obj ->
     (environment *                   (* new interpretation status *)
@@ -689,15 +691,10 @@ module Make (C: Callbacks) =
         uris
 
     let disambiguate_thing ~dbd ~context ~metasenv
-      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases
+      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing
     =
       debug_print "DISAMBIGUATE INPUT";
-      let current_env, multi_aliases_env =
-        match aliases with
-        | false, e -> Environment.hd e, None
-        | true, e -> Environment.empty, Some e
-      in
       let disambiguate_context =  (* cic context -> disambiguate context *)
         List.map
           (function None -> Cic.Anonymous | Some (name, _) -> name)
@@ -708,9 +705,11 @@ module Make (C: Callbacks) =
       debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
         (string_of_domain thing_dom));
       debug_print (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
-        (DisambiguatePp.pp_environment (snd aliases)));
+        (DisambiguatePp.pp_environment aliases));
+      debug_print (sprintf "DISAMBIGUATION UNIVERSE: %s"
+        (match universe with None -> "None" | Some _ -> "Some _"));
       let current_dom =
-        Environment.fold (fun item _ dom -> item :: dom) current_env []
+        Environment.fold (fun item _ dom -> item :: dom) aliases []
       in
       let todo_dom = domain_diff thing_dom current_dom in
       (* (2) lookup function for any item (Id/Symbol/Num) *)
@@ -727,7 +726,7 @@ module Make (C: Callbacks) =
               | Num instance ->
                   DisambiguateChoices.lookup_num_choices ()
             in
-            match multi_aliases_env with
+            match universe with
             | None -> lookup_in_library ()
             | Some e ->
                 (try
@@ -764,7 +763,7 @@ module Make (C: Callbacks) =
 
       (* (3) test an interpretation filling with meta uninterpreted identifiers
        *)
-      let test_env current_env todo_dom ugraph = 
+      let test_env aliases todo_dom ugraph = 
         let filled_env =
           List.fold_left
             (fun env item ->
@@ -773,7 +772,7 @@ module Make (C: Callbacks) =
                  (match item with
                     | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
                     | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
-            current_env todo_dom 
+            aliases todo_dom 
         in
         try
           let cic_thing =
@@ -787,12 +786,12 @@ module Make (C: Callbacks) =
         | Invalid_choice -> Ko, ugraph
       in
       (* (4) build all possible interpretations *)
-      let rec aux current_env todo_dom base_univ =
+      let rec aux aliases todo_dom base_univ =
         match todo_dom with
         | [] ->
-            (match test_env current_env [] base_univ with
+            (match test_env aliases [] base_univ with
             | Ok (thing, metasenv),new_univ -> 
-               [ current_env, metasenv, thing, new_univ ]
+               [ aliases, metasenv, thing, new_univ ]
             | Ko,_ | Uncertain,_ -> [])
         | item :: remaining_dom ->
             debug_print (sprintf "CHOOSED ITEM: %s"
@@ -803,7 +802,7 @@ module Make (C: Callbacks) =
               | codomain_item :: tl ->
                   debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
                   let new_env =
-                    Environment.add item codomain_item current_env
+                    Environment.add item codomain_item aliases
                   in
                   (match test_env new_env remaining_dom univ with
                   | Ok (thing, metasenv),new_univ ->
@@ -823,7 +822,7 @@ module Make (C: Callbacks) =
       let base_univ = initial_ugraph in
       try
         let res =
-         match aux current_env todo_dom base_univ with
+         match aux aliases todo_dom base_univ with
          | [] -> raise NoWellTypedInterpretation
          | [ e,me,t,u ] ->
              debug_print "SINGLE INTERPRETATION";
@@ -858,7 +857,7 @@ module Make (C: Callbacks) =
       let choices, b = res in
       (List.map
         (fun (env, metasenv, t, ugraph) ->
-          Environment.fold Environment.cons env (snd aliases),
+          Environment.fold Environment.add env aliases,
           metasenv, t, ugraph)
         choices),
       b
@@ -867,21 +866,23 @@ module Make (C: Callbacks) =
         failwith "Disambiguate: circular dependency"
 
     let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
-      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term
+      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe term
     =
       let term =
         if fresh_instances then CicNotationUtil.freshen_term term else term
       in
       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
-        ~uri:None ~pp_thing:CicNotationPp.pp_term
+        ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
         ~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term
         ~refine_thing:refine_term term
 
-    let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~uri obj =
+    let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
+     obj
+    =
       let obj =
         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
       in
-      disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri
+      disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
         ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj
         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
         obj
@@ -906,7 +907,7 @@ struct
     let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in
     try
       fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
-        ?initial_ugraph ~aliases:(false, aliases))
+        ?initial_ugraph ~aliases ~universe:None)
     with Exit -> raise (Ambiguous_term term)
 end