X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=f5ea66f2f6883e06a840744579277817577fe32f;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=e6cc064a5e928ede7333bd4f776378e1abe03c62;hpb=059c1bb4766e823aa53b39fed7d3dd55b4a06101;p=helm.git

diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
index e6cc064a5..f5ea66f2f 100644
--- a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
@@ -23,51 +23,48 @@
  * http://helm.cs.unibo.it/
  *)
 
-open GrafiteTypes
+(* $Id$ *)
+
+exception BaseUriNotSetYet
 
 let singleton = function
   | [x], _ -> x
   | _ -> assert false
 
   (** @param term not meaningful when context is given *)
-let disambiguate_term ?context status_ref goal term =
-  let status = !status_ref in
-  let context =
-    match context with
-    | Some c -> c
-    | None -> GrafiteTypes.get_proof_context status goal
-  in
+let disambiguate_term lexicon_status_ref context metasenv term =
+  let lexicon_status = !lexicon_status_ref in
   let (diff, metasenv, cic, _) =
     singleton
-      (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
-        ~aliases:status.aliases ~universe:(Some status.multi_aliases)
-        ~context ~metasenv:(GrafiteTypes.get_proof_metasenv status) term)
+      (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
+        ~aliases:lexicon_status.LexiconEngine.aliases
+        ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+        ~context ~metasenv term)
   in
-  let status = GrafiteTypes.set_metasenv metasenv status in
-  let status = MatitaSync.set_proof_aliases status diff in
-  status_ref := status;
-  cic
+  let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+  lexicon_status_ref := lexicon_status;
+  metasenv,cic
   
   (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
    * rationale: lazy_term will be invoked in different context to obtain a term,
    * each invocation will disambiguate the term and can add aliases. Once all
    * disambiguations have been performed, the first returned function can be
    * used to obtain the resulting aliases *)
-let disambiguate_lazy_term status_ref term =
+let disambiguate_lazy_term lexicon_status_ref term =
   (fun context metasenv ugraph ->
-    let status = !status_ref in
+    let lexicon_status = !lexicon_status_ref in
     let (diff, metasenv, cic, ugraph) =
       singleton
-        (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
-          ~initial_ugraph:ugraph ~aliases:status.aliases
-          ~universe:(Some status.multi_aliases) ~context ~metasenv term)
-    in
-    let status = GrafiteTypes.set_metasenv metasenv status in
-    let status = MatitaSync.set_proof_aliases status diff in
-    status_ref := status;
+        (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
+          ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
+          ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+          ~context ~metasenv
+          term) in
+    let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+    lexicon_status_ref := lexicon_status;
     cic, metasenv, ugraph)
 
-let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
+let disambiguate_pattern lexicon_status_ref (wanted, hyp_paths, goal_path) =
   let interp path = Disambiguate.interpretate_path [] 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
@@ -75,179 +72,218 @@ let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
    match wanted with
       None -> None
     | Some wanted ->
-       let wanted = disambiguate_lazy_term status_ref wanted in
+       let wanted = disambiguate_lazy_term lexicon_status_ref wanted in
        Some wanted
   in
   (wanted, hyp_paths, goal_path)
 
-let disambiguate_reduction_kind aliases_ref = function
+let disambiguate_reduction_kind lexicon_status_ref = function
   | `Unfold (Some t) ->
-      let t = disambiguate_lazy_term aliases_ref t in
+      let t = disambiguate_lazy_term lexicon_status_ref t in
       `Unfold (Some t)
+  | `Demodulate
   | `Normalize
   | `Reduce
   | `Simpl
   | `Unfold None
   | `Whd as kind -> kind
   
-let disambiguate_tactic status goal tactic =
-  let status_ref = ref status in
-  let tactic =
-    match tactic with
+let disambiguate_tactic lexicon_status_ref context metasenv tactic =
+  let disambiguate_term = disambiguate_term lexicon_status_ref in
+  let disambiguate_pattern = disambiguate_pattern lexicon_status_ref in
+  let disambiguate_reduction_kind = disambiguate_reduction_kind lexicon_status_ref in
+  let disambiguate_lazy_term = disambiguate_lazy_term lexicon_status_ref in
+   match tactic with
     | GrafiteAst.Absurd (loc, term) -> 
-        let cic = disambiguate_term status_ref goal term in
-        GrafiteAst.Absurd (loc, cic)
+        let metasenv,cic = disambiguate_term context metasenv term in
+        metasenv,GrafiteAst.Absurd (loc, cic)
     | GrafiteAst.Apply (loc, term) ->
-        let cic = disambiguate_term status_ref goal term in
-        GrafiteAst.Apply (loc, cic)
-    | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc
+        let metasenv,cic = disambiguate_term context metasenv term in
+        metasenv,GrafiteAst.Apply (loc, cic)
+    | GrafiteAst.Assumption loc ->
+        metasenv,GrafiteAst.Assumption loc
     | GrafiteAst.Auto (loc,depth,width,paramodulation,full) ->
-        GrafiteAst.Auto (loc,depth,width,paramodulation,full)
+        metasenv,GrafiteAst.Auto (loc,depth,width,paramodulation,full)
     | GrafiteAst.Change (loc, pattern, with_what) -> 
-        let with_what = disambiguate_lazy_term status_ref with_what in
-        let pattern = disambiguate_pattern status_ref pattern in
-        GrafiteAst.Change (loc, pattern, with_what)
-    | GrafiteAst.Clear (loc,id) -> GrafiteAst.Clear (loc,id)
-    | GrafiteAst.ClearBody (loc,id) -> GrafiteAst.ClearBody (loc,id)
+        let with_what = disambiguate_lazy_term with_what in
+        let pattern = disambiguate_pattern pattern in
+        metasenv,GrafiteAst.Change (loc, pattern, with_what)
+    | GrafiteAst.Clear (loc,id) ->
+        metasenv,GrafiteAst.Clear (loc,id)
+    | GrafiteAst.ClearBody (loc,id) ->
+       metasenv,GrafiteAst.ClearBody (loc,id)
     | GrafiteAst.Compare (loc,term) ->
-        let term = disambiguate_term status_ref goal term in
-        GrafiteAst.Compare (loc,term)
-    | GrafiteAst.Constructor (loc,n) -> GrafiteAst.Constructor (loc,n)
-    | GrafiteAst.Contradiction loc -> GrafiteAst.Contradiction loc
+        let metasenv,term = disambiguate_term context metasenv term in
+        metasenv,GrafiteAst.Compare (loc,term)
+    | GrafiteAst.Constructor (loc,n) ->
+        metasenv,GrafiteAst.Constructor (loc,n)
+    | GrafiteAst.Contradiction loc ->
+        metasenv,GrafiteAst.Contradiction loc
     | GrafiteAst.Cut (loc, ident, term) -> 
-        let cic = disambiguate_term status_ref goal term in
-        GrafiteAst.Cut (loc, ident, cic)
-    | GrafiteAst.DecideEquality loc -> GrafiteAst.DecideEquality loc
+        let metasenv,cic = disambiguate_term context metasenv term in
+        metasenv,GrafiteAst.Cut (loc, ident, cic)
+    | GrafiteAst.DecideEquality loc ->
+        metasenv,GrafiteAst.DecideEquality loc
     | GrafiteAst.Decompose (loc, types, what, names) ->
-        let disambiguate types = function
+        let disambiguate (metasenv,types) = function
            | GrafiteAst.Type _   -> assert false
            | GrafiteAst.Ident id ->
-              (match disambiguate_term status_ref goal
-                (CicNotationPt.Ident (id, None))
-              with
-              | Cic.MutInd (uri, tyno, _) ->
-                  (GrafiteAst.Type (uri, tyno) :: types)
-              | _ -> raise (MatitaDisambiguator.DisambiguationError (0,[[None,lazy "Decompose works only on inductive types"]])))
+              (match
+                disambiguate_term context metasenv
+                 (CicNotationPt.Ident(id, None))
+               with
+                | metasenv,Cic.MutInd (uri, tyno, _) ->
+                    metasenv,(GrafiteAst.Type (uri, tyno) :: types)
+                | _ ->
+                  raise (GrafiteDisambiguator.DisambiguationError
+                   (0,[[None,lazy "Decompose works only on inductive types"]])))
+        in
+        let metasenv,types =
+         List.fold_left disambiguate (metasenv,[]) types
         in
-        let types = List.fold_left disambiguate [] types in
-        GrafiteAst.Decompose (loc, types, what, names)
+         metasenv,GrafiteAst.Decompose (loc, types, what, names)
     | GrafiteAst.Discriminate (loc,term) ->
-        let term = disambiguate_term status_ref goal term in
-        GrafiteAst.Discriminate(loc,term)
+        let metasenv,term = disambiguate_term context metasenv term in
+        metasenv,GrafiteAst.Discriminate(loc,term)
     | GrafiteAst.Exact (loc, term) -> 
-        let cic = disambiguate_term status_ref goal term in
-        GrafiteAst.Exact (loc, cic)
+        let metasenv,cic = disambiguate_term context metasenv term in
+        metasenv,GrafiteAst.Exact (loc, cic)
     | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
-        let what = disambiguate_term status_ref goal what in
-        let using = disambiguate_term status_ref goal using in
-        GrafiteAst.Elim (loc, what, Some using, depth, idents)
+        let metasenv,what = disambiguate_term context metasenv what in
+        let metasenv,using = disambiguate_term context metasenv using in
+        metasenv,GrafiteAst.Elim (loc, what, Some using, depth, idents)
     | GrafiteAst.Elim (loc, what, None, depth, idents) ->
-        let what = disambiguate_term status_ref goal what in
-        GrafiteAst.Elim (loc, what, None, depth, idents)
+        let metasenv,what = disambiguate_term context metasenv what in
+        metasenv,GrafiteAst.Elim (loc, what, None, depth, idents)
     | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
-        let what = disambiguate_term status_ref goal what in
-        let using = disambiguate_term status_ref goal using in
-        GrafiteAst.ElimType (loc, what, Some using, depth, idents)
+        let metasenv,what = disambiguate_term context metasenv what in
+        let metasenv,using = disambiguate_term context metasenv using in
+        metasenv,GrafiteAst.ElimType (loc, what, Some using, depth, idents)
     | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
-        let what = disambiguate_term status_ref goal what in
-        GrafiteAst.ElimType (loc, what, None, depth, idents)
-    | GrafiteAst.Exists loc -> GrafiteAst.Exists loc 
-    | GrafiteAst.Fail loc -> GrafiteAst.Fail loc
+        let metasenv,what = disambiguate_term context metasenv what in
+        metasenv,GrafiteAst.ElimType (loc, what, None, depth, idents)
+    | GrafiteAst.Exists loc ->
+        metasenv,GrafiteAst.Exists loc 
+    | GrafiteAst.Fail loc ->
+        metasenv,GrafiteAst.Fail loc
     | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
-        let pattern = disambiguate_pattern status_ref pattern in
-        let term = disambiguate_lazy_term status_ref term in
-        let red_kind = disambiguate_reduction_kind status_ref red_kind in
-        GrafiteAst.Fold (loc, red_kind, term, pattern)
+        let pattern = disambiguate_pattern pattern in
+        let term = disambiguate_lazy_term term in
+        let red_kind = disambiguate_reduction_kind red_kind in
+        metasenv,GrafiteAst.Fold (loc, red_kind, term, pattern)
     | GrafiteAst.FwdSimpl (loc, hyp, names) ->
-       GrafiteAst.FwdSimpl (loc, hyp, names)  
-    | GrafiteAst.Fourier loc -> GrafiteAst.Fourier loc
+       metasenv,GrafiteAst.FwdSimpl (loc, hyp, names)  
+    | GrafiteAst.Fourier loc ->
+       metasenv,GrafiteAst.Fourier loc
     | GrafiteAst.Generalize (loc,pattern,ident) ->
-        let pattern = disambiguate_pattern status_ref pattern in
-        GrafiteAst.Generalize (loc,pattern,ident)
-    | GrafiteAst.Goal (loc, g) -> GrafiteAst.Goal (loc, g)
-    | GrafiteAst.IdTac loc -> GrafiteAst.IdTac loc
+        let pattern = disambiguate_pattern pattern in
+        metasenv,GrafiteAst.Generalize (loc,pattern,ident)
+    | GrafiteAst.Goal (loc, g) ->
+        metasenv,GrafiteAst.Goal (loc, g)
+    | GrafiteAst.IdTac loc ->
+        metasenv,GrafiteAst.IdTac loc
     | GrafiteAst.Injection (loc, term) ->
-        let term = disambiguate_term status_ref goal term in
-        GrafiteAst.Injection (loc,term)
-    | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names)
+        let metasenv,term = disambiguate_term context metasenv term in
+        metasenv,GrafiteAst.Injection (loc,term)
+    | GrafiteAst.Intros (loc, num, names) ->
+        metasenv,GrafiteAst.Intros (loc, num, names)
     | GrafiteAst.Inversion (loc, term) ->
-       let term = disambiguate_term status_ref goal term in
-        GrafiteAst.Inversion (loc, term)
+       let metasenv,term = disambiguate_term context metasenv term in
+        metasenv,GrafiteAst.Inversion (loc, term)
     | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
        let f term to_what =
-          let term = disambiguate_term status_ref goal term in
+          let metasenv,term = disambiguate_term context metasenv term in
           term :: to_what
        in
        let to_what = List.fold_right f to_what [] in 
-       let what = disambiguate_term status_ref goal what in
-       GrafiteAst.LApply (loc, depth, to_what, what, ident)
-    | GrafiteAst.Left loc -> GrafiteAst.Left loc
+       let metasenv,what = disambiguate_term context metasenv what in
+       metasenv,GrafiteAst.LApply (loc, depth, to_what, what, ident)
+    | GrafiteAst.Left loc ->
+       metasenv,GrafiteAst.Left loc
     | GrafiteAst.LetIn (loc, term, name) ->
-        let term = disambiguate_term status_ref goal term in
-        GrafiteAst.LetIn (loc,term,name)
+        let metasenv,term = disambiguate_term context metasenv term in
+        metasenv,GrafiteAst.LetIn (loc,term,name)
     | GrafiteAst.Reduce (loc, red_kind, pattern) ->
-        let pattern = disambiguate_pattern status_ref pattern in
-        let red_kind = disambiguate_reduction_kind status_ref red_kind in
-        GrafiteAst.Reduce(loc, red_kind, pattern)
-    | GrafiteAst.Reflexivity loc -> GrafiteAst.Reflexivity loc
+        let pattern = disambiguate_pattern pattern in
+        let red_kind = disambiguate_reduction_kind red_kind in
+        metasenv,GrafiteAst.Reduce(loc, red_kind, pattern)
+    | GrafiteAst.Reflexivity loc ->
+        metasenv,GrafiteAst.Reflexivity loc
     | GrafiteAst.Replace (loc, pattern, with_what) -> 
-        let pattern = disambiguate_pattern status_ref pattern in
-        let with_what = disambiguate_lazy_term status_ref with_what in
-        GrafiteAst.Replace (loc, pattern, with_what)
+        let pattern = disambiguate_pattern pattern in
+        let with_what = disambiguate_lazy_term with_what in
+        metasenv,GrafiteAst.Replace (loc, pattern, with_what)
     | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
-        let term = disambiguate_term status_ref goal t in
-        let pattern = disambiguate_pattern status_ref pattern in
-        GrafiteAst.Rewrite (loc, dir, term, pattern)
-    | GrafiteAst.Right loc -> GrafiteAst.Right loc
-    | GrafiteAst.Ring loc -> GrafiteAst.Ring loc
-    | GrafiteAst.Split loc -> GrafiteAst.Split loc
-    | GrafiteAst.Symmetry loc -> GrafiteAst.Symmetry loc
+        let metasenv,term = disambiguate_term context metasenv t in
+        let pattern = disambiguate_pattern pattern in
+        metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern)
+    | GrafiteAst.Right loc ->
+        metasenv,GrafiteAst.Right loc
+    | GrafiteAst.Ring loc ->
+        metasenv,GrafiteAst.Ring loc
+    | GrafiteAst.Split loc ->
+        metasenv,GrafiteAst.Split loc
+    | GrafiteAst.Symmetry loc ->
+        metasenv,GrafiteAst.Symmetry loc
     | GrafiteAst.Transitivity (loc, term) -> 
-        let cic = disambiguate_term status_ref goal term in
-        GrafiteAst.Transitivity (loc, cic)
-  in
-  status_ref, tactic
+        let metasenv,cic = disambiguate_term context metasenv term in
+        metasenv,GrafiteAst.Transitivity (loc, cic)
 
-let disambiguate_obj status obj =
+let disambiguate_obj lexicon_status ~baseuri metasenv obj =
   let uri =
    match obj with
     | CicNotationPt.Inductive (_,(name,_,_,_)::_)
     | CicNotationPt.Record (_,name,_,_) ->
-       Some (UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ".ind"))
+       (match baseuri with
+         | Some baseuri ->
+            Some (UriManager.uri_of_string (baseuri ^ "/" ^ name ^ ".ind"))
+         | None -> raise BaseUriNotSetYet)
     | CicNotationPt.Inductive _ -> assert false
     | CicNotationPt.Theorem _ -> None in
   let (diff, metasenv, cic, _) =
     singleton
-      (MatitaDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
-        ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj)
-  in
-  let proof_status =
-    match status.proof_status with
-    | No_proof -> Intermediate metasenv
-    | Incomplete_proof _
-    | Proof _ ->
-       raise (GrafiteTypes.Command_error "imbricated proofs not allowed")
-    | Intermediate _ -> assert false
-  in
-  let status = { status with proof_status = proof_status } in
-  let status = MatitaSync.set_proof_aliases status diff in
-  status, cic
+      (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
+        ~aliases:lexicon_status.LexiconEngine.aliases
+        ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri obj) in
+  let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+  lexicon_status, metasenv, cic
   
-let disambiguate_command status =
-  function
-  | GrafiteAst.Alias _
+let disambiguate_command lexicon_status ~baseuri metasenv =
+ function
   | GrafiteAst.Coercion _
   | GrafiteAst.Default _
   | GrafiteAst.Drop _
-  | GrafiteAst.Dump _
   | GrafiteAst.Include _
-  | GrafiteAst.Interpretation _
-  | GrafiteAst.Notation _
   | GrafiteAst.Qed _
-  | GrafiteAst.Render _
   | GrafiteAst.Set _ as cmd ->
-      status,cmd
+      lexicon_status,metasenv,cmd
   | GrafiteAst.Obj (loc,obj) ->
-      let status,obj = disambiguate_obj status obj in
-      status, GrafiteAst.Obj (loc,obj)
+      let lexicon_status,metasenv,obj =
+       disambiguate_obj lexicon_status ~baseuri metasenv obj in
+      lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
 
+let disambiguate_macro lexicon_status_ref metasenv context macro =
+ let disambiguate_term = disambiguate_term lexicon_status_ref in
+  match macro with
+   | GrafiteAst.WMatch (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.WMatch (loc,term)
+   | GrafiteAst.WInstance (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.WInstance (loc,term)
+   | GrafiteAst.WElim (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.WElim (loc,term)
+   | GrafiteAst.WHint (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.WHint (loc,term)
+   | GrafiteAst.Check (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.Check (loc,term)
+   | GrafiteAst.Hint _
+   | GrafiteAst.WLocate _ as macro ->
+      metasenv,macro
+   | GrafiteAst.Quit _
+   | GrafiteAst.Print _
+   | GrafiteAst.Search_pat _
+   | GrafiteAst.Search_term _ -> assert false