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