helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id$ *)
  13
  14 exception DisambiguationError of
  15  int *
  16  ((Stdpp.location list * string * string) list *
  17   (DisambiguateTypes.domain_item * string) list *
  18   (Stdpp.location * string) Lazy.t * bool) list list
  19
  20 open Printf
  21
  22 let debug = false;;
  23 let debug_print s =
  24  if debug then prerr_endline (Lazy.force s);;
  25
  26 module Callbacks =
  27   struct
  28     let interactive_user_uri_choice ~selection_mode ?ok
  29           ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
  30               assert false
  31
  32     let interactive_interpretation_choice interp =
  33             assert false
  34
  35     let input_or_locate_uri ~(title:string) ?id () =
  36             assert false
  37   end
  38
  39 module Disambiguator = NDisambiguate.Make (Callbacks)
  40
  41 let only_one_pass = ref false;;
  42
  43 let disambiguate_thing ~aliases ~universe
  44   ~(f:?fresh_instances:bool ->
  45       aliases:NCic.term DisambiguateTypes.environment ->
  46       universe:NCic.term DisambiguateTypes.multiple_environment option ->
  47       'a -> 'b)
  48   ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b)
  49   ~(drop_aliases_and_clear_diff: 'b -> 'b)
  50   (thing: 'a)
  51 =
  52   assert (universe <> None);
  53   let library = false, DisambiguateTypes.Environment.empty, None in
  54   let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
  55   let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
  56   let passes = (* <fresh_instances?, aliases, coercions?> *)
  57    if !only_one_pass then
  58     [ (true, mono_aliases, false) ]
  59    else
  60     [ (true, mono_aliases, false);
  61       (true, multi_aliases, false);
  62       (true, mono_aliases, true);
  63       (true, multi_aliases, true);
  64       (true, library, false);
  65         (* for demo to reduce the number of interpretations *)
  66       (true, library, true);
  67     ]
  68   in
  69   let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) =
  70     CicRefine.insert_coercions := insert_coercions;
  71     f ~fresh_instances ~aliases ~universe thing
  72   in
  73   let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
  74    if use_mono_aliases then
  75     drop_aliases ~minimize_instances:true res (* one shot aliases *)
  76    else if user_asked then
  77     drop_aliases ~minimize_instances:true res (* one shot aliases *)
  78    else
  79     drop_aliases_and_clear_diff res
  80   in
  81   let rec aux i errors passes =
  82   debug_print (lazy ("Pass: " ^ string_of_int i));
  83    match passes with
  84       [ pass ] ->
  85         (try
  86           set_aliases pass (try_pass pass)
  87          with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
  88           raise (DisambiguationError (offset, errors @ [newerrors])))
  89     | hd :: tl ->
  90         (try
  91           set_aliases hd (try_pass hd)
  92         with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
  93          aux (i+1) (errors @ [newerrors]) tl)
  94     | [] -> assert false
  95   in
  96   let saved_insert_coercions = !CicRefine.insert_coercions in
  97   try
  98     let res = aux 1 [] passes in
  99     CicRefine.insert_coercions := saved_insert_coercions;
 100     res
 101   with exn ->
 102     CicRefine.insert_coercions := saved_insert_coercions;
 103     raise exn
 104
 105 type disambiguator_thing =
 106  { do_it :
 107     'a 'b.
 108     aliases:NCic.term DisambiguateTypes.environment ->
 109     universe:NCic.term DisambiguateTypes.multiple_environment option ->
 110     f:(?fresh_instances:bool ->
 111        aliases:NCic.term DisambiguateTypes.environment ->
 112        universe:NCic.term DisambiguateTypes.multiple_environment option ->
 113        'a -> 'b * bool) ->
 114     drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) ->
 115     drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
 116  }
 117
 118 let disambiguate_thing =
 119  let profiler = HExtlib.profile "disambiguate_thing" in
 120   { do_it =
 121      fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
 122      -> profiler.HExtlib.profile
 123          (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
 124            ~drop_aliases_and_clear_diff) thing
 125   }
 126
 127 let drop_aliases ?(minimize_instances=false) (choices, user_asked) =
 128  let module D = DisambiguateTypes in
 129  let minimize d =
 130   if not minimize_instances then
 131    d
 132   else
 133    let rec aux =
 134     function
 135        [] -> []
 136      | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 ->
 137          if
 138           List.for_all
 139            (function
 140                (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2
 141              | _ -> true
 142            ) d
 143          then
 144           (D.Symbol (s,0),ci)::(aux tl)
 145          else
 146           he::(aux tl)
 147      | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 ->
 148          if
 149           List.for_all
 150            (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d
 151          then
 152           (D.Num 0,ci)::(aux tl)
 153          else
 154           he::(aux tl)
 155       | he::tl -> he::(aux tl)
 156    in
 157     aux d
 158  in
 159   (List.map (fun (d, a, b, c) -> minimize d, a, b, c) choices),
 160   user_asked
 161
 162 let drop_aliases_and_clear_diff (choices, user_asked) =
 163   (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
 164   user_asked
 165
 166 let disambiguate_term ~context ~metasenv ~subst ?goal
 167   ~aliases ~universe term
 168  =
 169   let f =
 170     Disambiguator.disambiguate_term ~context ~metasenv ~subst ?goal
 171      ~lookup_in_library:(fun _ _ -> assert false)
 172   in
 173   disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
 174    ~drop_aliases_and_clear_diff term
 175
 176 let disambiguate_obj ~aliases ~universe ~uri obj =
 177         assert false (*
 178   assert (fresh_instances = None);
 179   let f = Disambiguator.disambiguate_obj ~uri ~lookup_in_library:(fun _ _ -> assert false) in
 180   disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
 181    ~drop_aliases_and_clear_diff obj
 182    *)