new macro ncheck. fixed term2pres for Inductive and LetIn=Cast

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 2055bb9cdbe3c2a99c7ef25e4722bafbee87dd6e..9874e71840179f20ebe4dec9020ebe105a718a04 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -210,7 +210,7 @@ let cic2grafite context menv t =
       | Cic.Const _ as t -> 
           PT.Ident (pp_t c t, None)
       | Cic.Appl l -> PT.Appl (List.map (aux c) l)
-      | Cic.Implicit _ -> PT.Implicit
+      | Cic.Implicit _ -> PT.Implicit `JustOne
       | Cic.Lambda (Cic.Name n, s, t) ->
           PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
             aux (Some (Cic.Name n, Cic.Decl s)::c) t)
@@ -220,7 +220,7 @@ let cic2grafite context menv t =
       | Cic.LetIn (Cic.Name n, s, ty, t) ->
           PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
             aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
-      | Cic.Meta _ -> PT.Implicit
+      | Cic.Meta _ -> PT.Implicit `JustOne
       | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
       | Cic.Sort Cic.Set -> PT.Sort `Set
       | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
@@ -365,6 +365,20 @@ let cic2grafite context menv t =
   prerr_endline script;
   stupid_indenter script
 ;;
+let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
+  let parsed_text_length = String.length parsed_text in
+  match mac with
+  | TA.NCheck (_,t) ->
+      let status = script#grafite_status in
+      let ctx = [] in
+      let m, s, status, t = 
+        GrafiteDisambiguate.disambiguate_nterm 
+          None status [] [] ctx (parsed_text,parsed_text_length,
+            CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne))  
+          (* XXX use the metasenv, if possible *)
+      in
+      guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
+      [], "", parsed_text_length
 
 let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
   let module MQ = MetadataQuery in
@@ -593,6 +607,10 @@ script ex loc
       let grafite_status,macro = lazy_macro context in
        eval_macro include_paths buffer guistuff grafite_status
         user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
+   | GrafiteEngine.NMacro (_loc,macro) ->
+       eval_nmacro include_paths buffer guistuff grafite_status
+        user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
+
 
 and eval_statement include_paths (buffer : GText.buffer) guistuff 
  grafite_status user_goal script statement