X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_disambiguation%2FgrafiteDisambiguate.ml;h=3ada62287967ca23c647ef954725047fe38d5767;hb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hp=923ae26125346c4ae63adef3bc68c46ef9297945;hpb=2ab652e8e37ad8459510eeff3741b0b16e00d8fb;p=helm.git

diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
index 923ae2612..3ada62287 100644
--- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -43,7 +43,7 @@ class type g_status =
    method disambiguate_db: db
   end
 
-class status =
+class virtual status =
  object (self)
   inherit Interpretations.status
   val disambiguate_db = initial_status
@@ -57,9 +57,9 @@ class status =
 let eval_with_new_aliases status f =
  let status =
   status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
- let res = f status in
- let new_aliases = status#disambiguate_db.new_aliases in
-  new_aliases,res
+ let new_status = f status in
+ let new_aliases = new_status#disambiguate_db.new_aliases in
+  new_aliases,new_status
 ;;
 
 let dump_aliases out msg status =
@@ -71,11 +71,6 @@ let set_proof_aliases status ~implicit_aliases mode new_aliases =
  if mode = GrafiteAst.WithoutPreferences then
    status
  else
-   (* MATITA 1.0
-   let new_commands =
-     List.map
-      (fun _,alias -> GrafiteAst.Alias (HExtlib.dummy_floc, alias)) new_aliases
-   in *)
    let aliases =
     List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
      status#disambiguate_db.aliases new_aliases in
@@ -127,7 +122,7 @@ let ncic_mk_choice status = function
      let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
       desc, `Num_interp
        (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
-  | GrafiteAst.Ident_alias (name, uri) -> 
+  | GrafiteAst.Ident_alias (_name, uri) -> 
      uri, `Sym_interp 
       (fun l->assert(l = []);
         let nref = NReference.reference_of_string uri in
@@ -144,7 +139,7 @@ let mk_implicit b =
 ;;
 
 let nlookup_in_library 
-  interactive_user_uri_choice input_or_locate_uri item 
+  _interactive_user_uri_choice _input_or_locate_uri item 
 =
   match item with
   | DisambiguateTypes.Id id -> 
@@ -176,26 +171,26 @@ let fix_instance item l =
 ;;
 
 
-let disambiguate_nterm estatus expty context metasenv subst thing
+let disambiguate_nterm status expty context metasenv subst thing
 =
   let diff, metasenv, subst, cic =
     singleton "first"
       (NCicDisambiguate.disambiguate_term
-        ~rdb:estatus
-        ~aliases:estatus#disambiguate_db.aliases
+        status
+        ~aliases:status#disambiguate_db.aliases
         ~expty 
-        ~universe:(Some estatus#disambiguate_db.multi_aliases)
+        ~universe:(Some status#disambiguate_db.multi_aliases)
         ~lookup_in_library:nlookup_in_library
-        ~mk_choice:(ncic_mk_choice estatus)
+        ~mk_choice:(ncic_mk_choice status)
         ~mk_implicit ~fix_instance
         ~description_of_alias:GrafiteAst.description_of_alias
         ~context ~metasenv ~subst thing)
   in
-  let estatus =
-   set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences
+  let status =
+   set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
     diff
   in
-   metasenv, subst, estatus, cic
+   metasenv, subst, status, cic
 ;;
 
 
@@ -203,18 +198,16 @@ type pattern =
   NotationPt.term Disambiguate.disambiguator_input option * 
   (string * NCic.term) list * NCic.term option
 
-let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
-  let interp path = NCicDisambiguate.disambiguate_path path in
+let disambiguate_npattern status (text, prefix_len, (wanted, hyp_paths, goal_path)) =
+  let interp path = NCicDisambiguate.disambiguate_path status path in
   let goal_path = HExtlib.map_option interp goal_path in
   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
-  let wanted = 
-    match wanted with None -> None | Some x -> Some (text,prefix_len,x)
-  in
+  let wanted = HExtlib.map_option (fun x -> text,prefix_len,x) wanted in
    (wanted, hyp_paths, goal_path)
 ;;
 
-let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
-  | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
+let disambiguate_reduction_kind _text _prefix_len = function
+  | `Unfold (Some _t) -> assert false (* MATITA 1.0 *)
   | `Normalize
   | `Simpl
   | `Unfold None
@@ -248,16 +241,18 @@ let disambiguate_just disambiguate_term context metasenv =
        metasenv, `Auto params
 ;;
       
-let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
+let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
   let uri =
    let baseuri = 
      match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
    in
    let name = 
      match obj with
-     | NotationPt.Inductive (_,(name,_,_,_)::_)
-     | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
-     | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
+     | NotationPt.Inductive (_,(name,_,_,_)::_,_)
+     | NotationPt.Record (_,name,_,_,_) -> name ^ ".ind"
+     | NotationPt.Theorem (name,_,_,_) -> name ^ ".con"
+     | NotationPt.LetRec (_,(_,(NotationPt.Ident (name, None),_),_,_)::_,_) -> name ^ ".con"
+     | NotationPt.LetRec _
      | NotationPt.Inductive _ -> assert false
    in
      NUri.uri_of_string (baseuri ^ "/" ^ name)
@@ -265,20 +260,19 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
   let diff, _, _, cic =
    singleton "third"
     (NCicDisambiguate.disambiguate_obj
+      status
       ~lookup_in_library:nlookup_in_library
       ~description_of_alias:GrafiteAst.description_of_alias
-      ~mk_choice:(ncic_mk_choice estatus)
-      ~mk_implicit ~fix_instance
-      ~uri
-      ~rdb:estatus
-      ~aliases:estatus#disambiguate_db.aliases
-      ~universe:(Some estatus#disambiguate_db.multi_aliases) 
+      ~mk_choice:(ncic_mk_choice status)
+      ~mk_implicit ~fix_instance ~uri
+      ~aliases:status#disambiguate_db.aliases
+      ~universe:(Some status#disambiguate_db.multi_aliases) 
       (text,prefix_len,obj)) in
-  let estatus =
-   set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences
+  let status =
+   set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
     diff
   in
-   estatus, cic
+   status, cic
 ;;
 
 let disambiguate_cic_appl_pattern status args =
@@ -315,14 +309,14 @@ let disambiguate_cic_appl_pattern status args =
   disambiguate
 ;;
 
-let aliases_for_objs refs =
+let aliases_for_objs status refs =
  List.concat
   (List.map
     (fun nref ->
       let references = NCicLibrary.aliases_of nref in
        List.map
         (fun u ->
-          let name = NCicPp.r2s true u in
+          let name = NCicPp.r2s status true u in
            DisambiguateTypes.Id name,
             GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
         ) references) refs)