added support for multi-aliases in disambiguation environment(s)

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index c33462f8fd90269eedabefac815c2af3f6c1c5c2..919c33eb76526e31035e13721ae25e6caffb7845 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -35,7 +35,9 @@ exception PathNotWellFormed
   (** raised when an environment is not enough informative to decide *)
 exception Try_again
 
-let debug = false
+type aliases = bool * DisambiguateTypes.environment
+
+let debug = true
 let debug_print = if debug then prerr_endline else ignore
 
 (*
@@ -102,7 +104,7 @@ let refine_obj metasenv context uri obj ugraph =
            (CicPp.ppobj obj) msg);
          Ko,ugraph
 
-let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
+let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
   try
     snd (Environment.find item env) env num args
   with Not_found -> 
@@ -339,8 +341,8 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
   | CicNotationPt.AttributedTerm (`Loc loc, term) -> aux loc context term
   | term -> aux dummy_floc context term
 
-let interpretate_path ~context ~env path =
- interpretate_term ~context ~env ~uri:None ~is_path:true path
+let interpretate_path ~context path =
+ interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true path
 
 let interpretate_obj ~context ~env ~uri ~is_path obj =
  assert (context = []);
@@ -367,7 +369,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.env_of_list name_to_uris env in
+     let con_env = DisambiguateTypes.singleton_env_of_list name_to_uris env in
      let undebrujin t =
       snd
        (List.fold_right
@@ -577,8 +579,7 @@ and domain_rev_of_term_option loc context = function
   | None -> []
   | Some t -> domain_rev_of_term ~loc context t
 
-let domain_of_term ~context ast =
- rev_uniq (domain_rev_of_term context ast)
+let domain_of_term ~context ast = rev_uniq (domain_rev_of_term context ast)
 
 let domain_of_obj ~context ast =
  assert (context = []);
@@ -639,26 +640,30 @@ let domain_diff dom1 dom2 =
 module type Disambiguator =
 sig
   val disambiguate_term :
+    ?fresh_instances:bool ->
     dbd:Mysql.dbd ->
     context:Cic.context ->
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
-    aliases:environment ->  (* previous interpretation status *)
+    aliases:aliases ->  (* previous interpretation status *)
     CicNotationPt.term ->
     (environment *                   (* new interpretation status *)
      Cic.metasenv *                  (* new metasenv *)
      Cic.term*
-     CicUniv.universe_graph) list    (* disambiguated term *)
+     CicUniv.universe_graph) list *  (* disambiguated term *)
+    bool
 
   val disambiguate_obj :
+    ?fresh_instances:bool ->
     dbd:Mysql.dbd ->
-    aliases:environment ->           (* previous interpretation status *)
+    aliases:aliases ->           (* previous interpretation status *)
     uri:UriManager.uri option ->     (* required only for inductive types *)
     GrafiteAst.obj ->
     (environment *                   (* new interpretation status *)
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *
-     CicUniv.universe_graph) list    (* disambiguated obj *)
+     CicUniv.universe_graph) list *  (* disambiguated obj *)
+    bool
 end
 
 module Make (C: Callbacks) =
@@ -694,10 +699,15 @@ module Make (C: Callbacks) =
         uris
 
     let disambiguate_thing ~dbd ~context ~metasenv
-      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
+      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases
       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing
     =
-      debug_print "NEW DISAMBIGUATE INPUT";
+      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)
@@ -707,6 +717,8 @@ module Make (C: Callbacks) =
       let thing_dom = domain_of_thing ~context:disambiguate_context thing in
       debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
         (string_of_domain thing_dom));
+      debug_print (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
+        (DisambiguatePp.pp_environment (snd aliases)));
       let current_dom =
         Environment.fold (fun item _ dom -> item :: dom) current_env []
       in
@@ -715,25 +727,26 @@ module Make (C: Callbacks) =
       let lookup_choices =
         let id_choices = Hashtbl.create 1023 in
         fun item ->
-        let choices =
-          match item with
-          | Id id ->
-              (try
-                Hashtbl.find id_choices id
-              with Not_found ->
-                let choices = choices_of_id dbd id in
-                Hashtbl.add id_choices id choices;
-                choices)
-          | Symbol (symb, _) ->
-              List.map DisambiguateChoices.mk_choice
-                (CicNotationRew.lookup_interpretations symb)
-(*               DisambiguateChoices.lookup_symbol_choices symb *)
-          | Num instance -> DisambiguateChoices.lookup_num_choices ()
-        in
-        if choices = [] then raise (No_choices item);
-        choices
+          let choices =
+            let lookup_in_library () =
+              match item with
+              | Id id -> choices_of_id dbd id
+              | Symbol (symb, _) ->
+                  List.map DisambiguateChoices.mk_choice
+                    (CicNotationRew.lookup_interpretations symb)
+              | Num instance ->
+                  DisambiguateChoices.lookup_num_choices ()
+            in
+            match multi_aliases_env with
+            | None -> lookup_in_library ()
+            | Some e ->
+                (try
+                  Environment.find item e
+                with Not_found -> lookup_in_library ())
+          in
+          if choices = [] then raise (No_choices item);
+          choices
       in
-
 (*
       (* <benchmark> *)
       let _ =
@@ -823,14 +836,10 @@ module Make (C: Callbacks) =
          match aux current_env todo_dom base_univ with
          | [] -> raise NoWellTypedInterpretation
          | [ e,me,t,u ] ->
-             debug_print "UNA SOLA SCELTA";
-             (* Experimental: we forget the environment [e] since we are able
-                to recompute it. In this way we are forced to do more work
-                later (since we have less aliases), but we have more freedom
-                (since we have less aliases) in the future disambiguations. *)
-             [ current_env,me,t,u]
+             debug_print "SINGLE INTERPRETATION";
+             [ e,me,t,u ], false
          | l ->
-             debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
+             debug_print (sprintf "MANY INTERPRETATIONS (%d)" (List.length l));
              let choices =
                List.map
                  (fun (env, _, _, _) ->
@@ -844,7 +853,7 @@ module Make (C: Callbacks) =
                  l
              in
              let choosed = C.interactive_interpretation_choice choices in
-             List.map (List.nth l) choosed
+             (List.map (List.nth l) choosed), true
         in
 (*
         (if benchmark then
@@ -856,23 +865,36 @@ module Make (C: Callbacks) =
             !choices_avg
             (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg)));
 *)
-        res
+      let choices, b = res in
+      (List.map
+        (fun (env, metasenv, t, ugraph) ->
+          Environment.fold Environment.cons env (snd aliases),
+          metasenv, t, ugraph)
+        choices),
+      b
      with
       CicEnvironment.CircularDependency s -> 
         failwith "Disambiguate: circular dependency"
 
-    let disambiguate_term ~dbd ~context ~metasenv
+    let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term
     =
-     disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
-      ~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 ~dbd ~aliases ~uri obj =
-     disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri
-      ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj
-      ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
-      obj
+      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
+        ~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 obj =
+        if fresh_instances then CicNotationUtil.freshen_obj obj else obj
+      in
+      disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri
+        ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj
+        ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
+        obj
   end
 
 module Trivial =
@@ -893,8 +915,8 @@ struct
   =
     let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in
     try
-      Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
-        ?initial_ugraph ~aliases
+      fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
+        ?initial_ugraph ~aliases:(false, aliases))
     with Exit -> raise (Ambiguous_term term)
 end
 

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index 6f74c23c0ab674bcf213a60992e4544c0574ff55..10b1c7633dfede3a24ebe3b8d8f51496f334e712 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -29,33 +29,43 @@ exception NoWellTypedInterpretation
 exception PathNotWellFormed
 
 val interpretate_path :
-  context:Cic.name list -> env:DisambiguateTypes.environment ->
-  DisambiguateTypes.term ->
+  context:Cic.name list -> DisambiguateTypes.term ->
     Cic.term
 
+  (** @param multi true if multi aliases are used, false otherwise *)
+type aliases = bool * DisambiguateTypes.environment
+
 module type Disambiguator =
 sig
+  (** @param fresh_instances when set to true fresh instances will be generated
+   * for each number _and_ symbol in the disambiguation domain. Instances of the
+   * input AST will be ignored. Defaults to false. *)
   val disambiguate_term :
+    ?fresh_instances:bool ->
     dbd:Mysql.dbd ->
     context:Cic.context ->
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
-    aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
+    aliases:aliases ->               (* previous interpretation status *)
     DisambiguateTypes.term ->
     (DisambiguateTypes.environment * (* new interpretation status *)
      Cic.metasenv *                  (* new metasenv *)
      Cic.term *
-     CicUniv.universe_graph) list    (* disambiguated term *)
+     CicUniv.universe_graph) list *  (* disambiguated term *)
+    bool  (* has interactive_interpretation_choice been invoked? *)
 
+  (** @param fresh_instances as per disambiguate_term *)
   val disambiguate_obj :
+    ?fresh_instances:bool ->
     dbd:Mysql.dbd ->
-    aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
+    aliases:aliases ->               (* previous interpretation status *)
     uri:UriManager.uri option ->     (* required only for inductive types *)
     GrafiteAst.obj ->
     (DisambiguateTypes.environment * (* new interpretation status *)
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *
-     CicUniv.universe_graph) list    (* disambiguated obj *)
+     CicUniv.universe_graph) list *  (* disambiguated obj *)
+    bool  (* has interactive_interpretation_choice been invoked? *)
 end
 
 module Make (C : DisambiguateTypes.Callbacks) : Disambiguator

diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
index d6a33cfaedf76a1daa38daa1e1279a8d9f024d21..24f9ea37ea1b319f166cc17090fa4ec42564df7c 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
@@ -49,7 +49,7 @@ let parse_environment str =
           Num instance,
           DisambiguateChoices.lookup_num_by_dsc desc
      in
-      environment := Environment.add key value !environment;
+      environment := Environment.cons key value !environment;
     done;
     assert false
   with End_of_file ->
@@ -58,18 +58,21 @@ let parse_environment str =
 let pp_environment env =
   let aliases =
     Environment.fold
-      (fun domain_item (dsc, _) acc ->
-        let s =
-          match domain_item with
-          | Id id ->
-              GrafiteAstPp.pp_alias (GrafiteAst.Ident_alias (id, dsc)) ^ "."
-          | Symbol (symb, i) ->
-              GrafiteAstPp.pp_alias (GrafiteAst.Symbol_alias (symb, i, dsc))
-              ^ "."
-          | Num i ->
-              GrafiteAstPp.pp_alias (GrafiteAst.Number_alias (i, dsc)) ^ "."
-        in
-        s :: acc)
+      (fun domain_item codomain_items acc ->
+        List.fold_left
+          (fun strings (dsc, _) ->
+            let s =
+              match domain_item with
+              | Id id ->
+                  GrafiteAstPp.pp_alias (GrafiteAst.Ident_alias (id, dsc)) ^ "."
+              | Symbol (symb, i) ->
+                  GrafiteAstPp.pp_alias (GrafiteAst.Symbol_alias (symb, i, dsc))
+                  ^ "."
+              | Num i ->
+                  GrafiteAstPp.pp_alias (GrafiteAst.Number_alias (i, dsc)) ^ "."
+            in
+            s :: strings)
+          acc codomain_items)
       env []
   in
   String.concat "\n" (List.sort compare aliases)

diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
index 6c530c2bf4813d16bb06da7eb882d4562f0f04ac..bb513aa6cdbc0cba1141fcdc7cc1f9115a024eca 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml
@@ -45,17 +45,48 @@ module OrderedDomain =
   end
 
 (* module Domain = Set.Make (OrderedDomain) *)
-module Environment = Map.Make (OrderedDomain)
+module Environment =
+struct
+  module Environment' = Map.Make (OrderedDomain)
+
+  include Environment'
+
+  let cons k v env =
+    try
+      let current = find k env in
+      let dsc, _ = v in
+      add k (v :: (List.filter (fun (dsc', _) -> dsc' <> dsc) current)) env
+    with Not_found ->
+      add k [v] env
+
+  let hd list_env =
+    try
+      map List.hd list_env
+    with Failure _ -> assert false
+
+  let fold_flatten f env base =
+    fold
+      (fun k l acc -> List.fold_right (fun v acc -> f k v acc) l acc)
+      env base
+
+end
 
 type codomain_item =
   string *  (* description *)
-  (environment -> string -> Cic.term list -> Cic.term)
+  (singleton_environment -> string -> Cic.term list -> Cic.term)
     (* environment, literal number, arguments as needed *)
 
-and environment = codomain_item Environment.t
+and environment = codomain_item list Environment.t
+
+and singleton_environment = codomain_item Environment.t
 
 (** adds a (name,uri) list l to a disambiguation environment e **)
 let env_of_list l e = 
+  List.fold_left
+   (fun e (name,descr,t) -> Environment.cons (Id name) (descr,fun _ _ _ -> t) e)
+   e l
+
+let singleton_env_of_list l e = 
   List.fold_left
    (fun e (name,descr,t) -> Environment.add (Id name) (descr,fun _ _ _ -> t) e)
    e l

diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
index b6d74a7fd84ff0b4b98668f5dea7a37ad079ff55..1a8dc4ac08bf02e00cc901799f967087d2519160 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli
@@ -29,7 +29,15 @@ type domain_item =
  | Num of int                 (* instance num *)
 
 (* module Domain:      Set.S with type elt = domain_item *)
-module Environment: Map.S with type key = domain_item
+module Environment:
+sig
+  include Map.S with type key = domain_item
+  val cons: domain_item -> ('a * 'b) -> ('a * 'b) list t -> ('a * 'b) list t
+  val hd: 'a list t -> 'a t
+
+    (** last alias cons-ed will be processed first *)
+  val fold_flatten: (domain_item -> 'a -> 'b -> 'b) -> 'a list t -> 'b -> 'b
+end
 
   (** to be raised when a choice is invalid due to some given parameter (e.g.
    * wrong number of Cic.term arguments received) *)
@@ -37,13 +45,21 @@ exception Invalid_choice
 
 type codomain_item =
   string *  (* description *)
-  (environment -> string -> Cic.term list -> Cic.term)
+  (singleton_environment -> string -> Cic.term list -> Cic.term)
     (* environment, literal number, arguments as needed *)
 
-and environment = codomain_item Environment.t
+and environment = codomain_item list Environment.t
+
+and singleton_environment = codomain_item Environment.t
 
 (* a simple case of extension of a disambiguation environment *)
-val env_of_list: (string * string * Cic.term) list -> environment -> environment
+val singleton_env_of_list:
+  (string * string * Cic.term) list -> singleton_environment ->
+    singleton_environment
+
+val env_of_list:
+  (string * string * Cic.term) list -> environment ->
+    environment
 
 module type Callbacks =
   sig