X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=9842ffdce7c05a13a9f933f4b6f758367daf0834;hb=aac382f935bc72578119fa7ff9f53c3b649dd0dd;hp=fed62fbb321c4e73b45a4b59b82e0e9c017386f9;hpb=bc36fe01d5465d07ef76c445c83639e341f3eb2a;p=helm.git

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index fed62fbb3..9842ffdce 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -101,18 +101,68 @@ let eval_with_engine status user_goal parsed_text st =
       new_text
   in
     [ new_status, new_text ], parsed_text_length
+
+let disambiguate term status =
+  let module MD = MatitaDisambiguator in
+  let dbd = MatitaDb.instance () in
+  let metasenv = MatitaMisc.get_proof_metasenv status in
+  let context = MatitaMisc.get_proof_context status in
+  let aliases = MatitaMisc.get_proof_aliases status in
+  let interps = MD.disambiguate_term dbd context metasenv aliases term in
+  match interps with 
+  | [_,_,x,_] -> x
+  | _ -> assert false
  
 let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text mac =
   let module TA = TacticAst in
   let module TAPp = TacticAstPp in
   let module MQ = MetadataQuery in
-  let module MD = MatitaDisambiguator in
   let module MDB = MatitaDb in
+  let module CTC = CicTypeChecker in
+  let module CU = CicUniv in
   let parsed_text_length = String.length parsed_text in
+  let dbd = MatitaDb.instance () in
   match mac with
+  (* WHELP's stuff *)
+  | TA.WMatch (loc, term) -> 
+      let term = disambiguate term status in
+      let l =  MQ.match_term ~dbd term in
+      let entry = `Whelp (TAPp.pp_macro_cic (TA.WMatch (loc, term)), l) in
+      mathviewer#show_uri_list ~reuse:true ~entry l;
+      [], parsed_text_length
+  | TA.WInstance (loc, term) ->
+      let term = disambiguate term status in
+      let l = MQ.instance ~dbd term in
+      let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
+      mathviewer#show_uri_list ~reuse:true ~entry l;
+      [], parsed_text_length
+  | TA.WLocate (loc, s) -> 
+      let l = MQ.locate ~dbd s in
+      let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
+      mathviewer#show_uri_list ~reuse:true ~entry l;
+      [], parsed_text_length  
+  | TA.WElim (loc, term) ->
+      let term = disambiguate term status in
+      let uri =
+        match term with
+        | Cic.MutInd (uri,n,_) -> UriManager.string_of_uriref (uri,[n])
+        | _ -> failwith "Not a MutInd"
+      in
+      let l = MQ.elim ~dbd uri in
+      let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
+      mathviewer#show_uri_list ~reuse:true ~entry l;
+      [], parsed_text_length  
+  | TA.WHint (loc, term) ->
+      let term = disambiguate term status in
+      let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
+      let l = List.map fst (MQ.experimental_hint ~dbd s) in
+      let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in
+      mathviewer#show_uri_list ~reuse:true ~entry l;
+      [], parsed_text_length  
+  (* REAL macro *)
   | TA.Hint loc -> 
       let s = MatitaMisc.get_proof_status status in
-      let l = List.map fst (MQ.experimental_hint ~dbd:(MDB.instance ()) s) in
+      let l = List.map fst (MQ.experimental_hint ~dbd s) in
       let selected = urichooser l in
       (match selected with
       | [] -> [], parsed_text_length
@@ -130,62 +180,23 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text
         in
         [ new_status , extra_text ],parsed_text_length
       | _ -> assert false)
-  | TA.Match (_,term) -> 
-      let dbd = MatitaDb.instance () in
+  | TA.Check (_,term) ->
       let metasenv = MatitaMisc.get_proof_metasenv status in
       let context = MatitaMisc.get_proof_context status in
       let aliases = MatitaMisc.get_proof_aliases status in
-      let (_env,_metasenv,term,_graph) = 
-        let interps =
-          MD.disambiguate_term dbd context metasenv aliases term 
-        in
+      let interps = 
+        MatitaDisambiguator.disambiguate_term 
+          dbd context metasenv aliases term 
+      in
+      let _, metasenv , term, ugraph =
         match interps with 
         | [x] -> x
         | _ -> assert false
       in
-      let results =  MetadataQuery.match_term ~dbd:dbd term in
-      mathviewer#show_uri_list ~reuse:true ~entry:(`Whelp ("match", results))
-        results;
-      [], parsed_text_length
-  | TA.Instance (_,term) ->
-      let dbd = MatitaDb.instance () in
-      let metasenv = MatitaMisc.get_proof_metasenv status in
-      let context = MatitaMisc.get_proof_context status in
-      let aliases = MatitaMisc.get_proof_aliases status in
-      let (_env,_metasenv,term,_graph) = 
-        let interps =
-          MD.disambiguate_term dbd context metasenv aliases term 
-        in
-          match interps with 
-            | [x] -> x
-            | _ -> assert false
-      in
-      let results = MetadataQuery.instance ~dbd term in
-        mathviewer#show_uri_list ~reuse:true
-          ~entry:(`Whelp ("instance", results)) results;
-        [], parsed_text_length
-          
-
-  | TA.Check (_,t) ->
-      let metasenv = MatitaMisc.get_proof_metasenv status in
-      let context = MatitaMisc.get_proof_context status in
-      let aliases = MatitaMisc.get_proof_aliases status in
-      let db = MatitaDb.instance () in
-      let (_env,_metasenv,term,_graph) = 
-        let interps = 
-          MD.disambiguate_term db context metasenv aliases t 
-        in
-          match interps with 
-            | [x] -> x
-            | _ -> assert false
-      in
-      let ty,_ = 
-        CicTypeChecker.type_of_aux' metasenv context term
-          CicUniv.empty_ugraph 
-      in
+      let ty,_ = CTC.type_of_aux' metasenv context term ugraph in
       let t_and_ty = Cic.Cast (term,ty) in
-        mathviewer # show_entry (`Cic (t_and_ty,metasenv));
-        [], parsed_text_length
+      mathviewer#show_entry (`Cic (t_and_ty,metasenv));
+      [], parsed_text_length
   | TA.Quit _ ->
       failwith "not implemented quit"
   | _ -> failwith "not implemented"