End of patch for computation of LetIn types. Now types of mutually (co)recursive

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 2fe6b9aaee80949f0130b972cc8bae673ace256f..dfaf5b42426816f6f3dcfed8c333dc4c5565726a 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -36,16 +36,20 @@ type lazy_tactic =
   (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) 
     GrafiteAst.tactic
 
-let singleton = function
+let singleton msg = function
   | [x], _ -> x
-  | _ -> assert false
-;;
+  | l, _   ->
+      let debug = 
+         Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
+        msg (List.length l)
+      in
+      HLog.debug debug; assert false
 
   (** @param term not meaningful when context is given *)
 let disambiguate_term text prefix_len lexicon_status_ref context metasenv term =
   let lexicon_status = !lexicon_status_ref in
   let (diff, metasenv, cic, _) =
-    singleton
+    singleton "first"
       (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
         ~aliases:lexicon_status.LexiconEngine.aliases
         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
@@ -65,7 +69,7 @@ let disambiguate_lazy_term text prefix_len lexicon_status_ref term =
   (fun context metasenv ugraph ->
     let lexicon_status = !lexicon_status_ref in
     let (diff, metasenv, cic, ugraph) =
-      singleton
+      singleton "second"
         (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
           ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
           ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
@@ -99,7 +103,6 @@ let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
       let t = disambiguate_lazy_term text prefix_len lexicon_status_ref t in
       `Unfold (Some t)
   | `Normalize
-  | `Reduce
   | `Simpl
   | `Unfold None
   | `Whd as kind -> kind
@@ -216,9 +219,13 @@ let rec disambiguate_tactic
          metasenv,GrafiteAst.Decompose (loc, names)
     | GrafiteAst.Demodulate loc ->
         metasenv,GrafiteAst.Demodulate loc
-    | GrafiteAst.Destruct (loc, Some term) ->
-        let metasenv,term = disambiguate_term context metasenv term in
-        metasenv,GrafiteAst.Destruct(loc, Some term)
+    | GrafiteAst.Destruct (loc, Some terms) ->
+        let map term (metasenv, terms) =
+           let metasenv, term = disambiguate_term context metasenv term in
+           metasenv, term :: terms
+        in
+        let metasenv, terms = List.fold_right map terms (metasenv, []) in 
+       metasenv, GrafiteAst.Destruct(loc, Some terms)
     | GrafiteAst.Destruct (loc, None) ->
         metasenv,GrafiteAst.Destruct(loc,None)
     | GrafiteAst.Exact (loc, term) -> 
@@ -264,12 +271,12 @@ let rec disambiguate_tactic
        let metasenv,term = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Inversion (loc, term)
     | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
-       let f term to_what =
-          let metasenv,term = disambiguate_term context metasenv term in
-          term :: to_what
+       let f term (metasenv, to_what) =
+          let metasenv, term = disambiguate_term context metasenv term in
+          metasenv, term :: to_what
        in
-       let to_what = List.fold_right f to_what [] in 
-       let metasenv,what = disambiguate_term context metasenv what in
+       let metasenv, to_what = List.fold_right f to_what (metasenv, []) in 
+       let metasenv, what = disambiguate_term context metasenv what in
        metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
     | GrafiteAst.Left loc ->
        metasenv,GrafiteAst.Left loc
@@ -402,7 +409,7 @@ let rec disambiguate_tactic
        metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)   
 
 
-let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =
+let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
   let uri =
    match obj with
     | CicNotationPt.Inductive (_,(name,_,_,_)::_)
@@ -414,7 +421,7 @@ let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =
     | CicNotationPt.Inductive _ -> assert false
     | CicNotationPt.Theorem _ -> None in
   let (diff, metasenv, cic, _) =
-    singleton
+    singleton "third"
       (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
         ~aliases:lexicon_status.LexiconEngine.aliases
         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri 
@@ -422,7 +429,7 @@ let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =
   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
   lexicon_status, metasenv, cic
   
-let disambiguate_command lexicon_status ~baseuri metasenv (text,prefix_len,cmd)=
+let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
   match cmd with
    | GrafiteAst.Index(loc,key,uri) ->
        let lexicon_status_ref = ref lexicon_status in 
@@ -447,7 +454,7 @@ let disambiguate_command lexicon_status ~baseuri metasenv (text,prefix_len,cmd)=
        lexicon_status,metasenv,cmd
    | GrafiteAst.Obj (loc,obj) ->
        let lexicon_status,metasenv,obj =
-        disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj)in
+        disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj)in
        lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
    | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
       let lexicon_status_ref = ref lexicon_status in