From cf4a3f9226194e0f6dc9572dea1090e2bfa55219 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Sep 2009 11:11:22 +0000 Subject: [PATCH] new macro ncheck. fixed term2pres for Inductive and LetIn=Cast --- .../content_pres/termContentPres.ml | 4 + .../software/components/grafite/grafiteAst.ml | 6 +- .../components/grafite/grafiteAstPp.ml | 5 ++ .../grafite_engine/grafiteEngine.ml | 3 + .../grafite_engine/grafiteEngine.mli | 1 + .../grafite_parser/grafiteParser.ml | 6 ++ .../ng_cic_content/nTermCicContent.ml | 73 ++++++++++--------- helm/software/matita/matitaMathView.ml | 10 +++ helm/software/matita/matitaScript.ml | 18 +++++ helm/software/matita/matitaTypes.ml | 2 + helm/software/matita/matitaTypes.mli | 1 + 11 files changed, 92 insertions(+), 37 deletions(-) diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index c115fe018..3fae0f52b 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -543,6 +543,8 @@ let head_names names env = aux ((name, (ty, v)) :: acc) tl | Env.TermType _, Env.TermValue _ -> aux ((name, (ty, v)) :: acc) tl + | Env.OptType _, Env.OptValue _ -> + aux ((name, (ty, v)) :: acc) tl | _ -> assert false) | _ :: tl -> aux acc tl (* base pattern may contain only meta names, thus we trash all others *) @@ -558,6 +560,8 @@ let tail_names names env = aux ((name, (Env.ListType ty, Env.ListValue vtl)) :: acc) tl | Env.TermType _, Env.TermValue _ -> aux ((name, (ty, v)) :: acc) tl + | Env.OptType _, Env.OptValue _ -> + aux ((name, (ty, v)) :: acc) tl | _ -> assert false) | binding :: tl -> aux (binding :: acc) tl | [] -> acc diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 813a08071..c84bf99fa 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -188,9 +188,12 @@ type ('term,'lazy_term) macro = | Inline of loc * string * inline_param list (* URI or base-uri, parameters *) +type nmacro = + | NCheck of loc * CicNotationPt.term + (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 26 +let magic = 27 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) @@ -238,6 +241,7 @@ type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code = | Command of loc * ('term, 'obj) command | NCommand of loc * ncommand | Macro of loc * ('term,'lazy_term) macro + | NMacro of loc * nmacro | NTactic of loc * ntactic list | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option * punctuation_tactical diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 6c7a6638a..89c4e3699 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -295,6 +295,10 @@ let pp_arg ~term_pp arg = else "(" ^ s ^ ")" +let pp_nmacro = function + | NCheck (_, term) -> Printf.sprintf "ncheck %s" (CicNotationPp.pp_term term) +;; + let pp_macro ~term_pp ~lazy_term_pp = let term_pp = pp_arg ~term_pp in let flavour_pp = function @@ -422,6 +426,7 @@ let pp_non_punctuation_tactical = let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = function + | NMacro (_, macro) -> pp_nmacro macro ^ "." | Macro (_, macro) -> pp_macro ~term_pp ~lazy_term_pp macro ^ "." | Tactic (_, Some tac, punct) -> pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp tac diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 597f29e10..d0d58a6fe 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -33,6 +33,7 @@ exception IncludedFileNotCompiled of string * string exception Macro of GrafiteAst.loc * (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) +exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro type 'a disambiguator_input = string * int * 'a @@ -1083,6 +1084,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status eval_ncommand opts status (text,prefix_len,cmd) | GrafiteAst.Macro (loc, macro) -> raise (Macro (loc,disambiguate_macro status (text,prefix_len,macro))) + | GrafiteAst.NMacro (loc, macro) -> + raise (NMacro (loc,macro)) } and eval_from_moo = {efm_go = fun status fname -> let ast_of_cmd cmd = diff --git a/helm/software/components/grafite_engine/grafiteEngine.mli b/helm/software/components/grafite_engine/grafiteEngine.mli index de7fb2790..6993afcb2 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.mli +++ b/helm/software/components/grafite_engine/grafiteEngine.mli @@ -28,6 +28,7 @@ exception IncludedFileNotCompiled of string * string exception Macro of GrafiteAst.loc * (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) +exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro type 'a disambiguator_input = string * int * 'a diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 277482456..c92e3175f 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -652,6 +652,11 @@ EXTEND in (params,name,typ,fields) ] ]; + + nmacro: [ + [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t) + ] + ]; macro: [ [ [ IDENT "check" ]; t = term -> @@ -938,6 +943,7 @@ EXTEND punct = punctuation_tactical -> G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct]) | mac = macro; SYMBOL "." -> G.Macro (loc, mac) + | mac = nmacro; SYMBOL "." -> G.NMacro (loc, mac) ] ]; comment: [ diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index c53a4a31c..56a3f3507 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -103,9 +103,11 @@ let nast_of_cic0 status | NCic.Lambda (n,s,t) -> idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ~context s)), k ~context:((n,NCic.Decl s)::context) t)) + | NCic.LetIn (n,s,ty,NCic.Rel 1) -> + idref (Ast.Cast (k ~context ty, k ~context s)) | NCic.LetIn (n,s,ty,t) -> - idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context ty)), k ~context s, - k ~context:((n,NCic.Decl s)::context) t)) + idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context s)), k ~context + ty, k ~context:((n,NCic.Decl s)::context) t)) | NCic.Appl (NCic.Meta (n,lc) :: args) when List.mem_assoc n subst -> let _,_,t,_ = List.assoc n subst in let hd = NCicSubstitution.subst_meta lc t in @@ -454,6 +456,8 @@ let nmap_sequent status ~metasenv ~subst conjecture = let object_prefix = "obj:";; let declaration_prefix = "decl:";; let definition_prefix = "def:";; +let inductive_prefix = "ind:";; +let joint_prefix = "joint:";; let get_id = function @@ -534,9 +538,39 @@ let nmap_obj status (uri,_,metasenv,subst,kind) = (*CSC: used to be the previous line, that uses seed *) Some (List.map (nmap_sequent0 status ~idref ~metasenv ~subst) metasenv) in +let build_constructors seed l = + List.map + (fun (_,n,ty) -> + let ty = nast_of_cic ~context:[] ty in + { K.dec_name = Some n; + K.dec_id = gen_id declaration_prefix seed; + K.dec_inductive = false; + K.dec_aref = ""; + K.dec_type = ty + }) l +in +let build_inductive b seed = + fun (_,n,ty,cl) -> + let ty = nast_of_cic ~context:[] ty in + `Inductive + { K.inductive_id = gen_id inductive_prefix seed; + K.inductive_name = n; + K.inductive_kind = b; + K.inductive_type = ty; + K.inductive_constructors = build_constructors seed cl + } +in let res = match kind with - NCic.Constant (_,_,Some bo,ty,_) -> + | NCic.Fixpoint (is_rec, ifl, _) -> assert false + | NCic.Inductive (is_ind, lno, itl, _) -> + (gen_id object_prefix seed, [], conjectures, + `Joint + { K.joint_id = gen_id joint_prefix seed; + K.joint_kind = `Inductive lno; + K.joint_defs = List.map (build_inductive is_ind seed) itl + }) + | NCic.Constant (_,_,Some bo,ty,_) -> let ty = nast_of_cic ~context:[] ty in let bo = nast_of_cic ~context:[] bo in (gen_id object_prefix seed, [], conjectures, @@ -548,39 +582,6 @@ let nmap_obj status (uri,_,metasenv,subst,kind) = `Decl (K.Const, (*CSC: ??? get_id ty here used to be the id of the axiom! *) build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty)) -(* - | C.AInductiveDefinition (id,l,params,nparams,_) -> - (gen_id object_prefix seed, params, conjectures, - `Joint - { K.joint_id = gen_id joint_prefix seed; - K.joint_kind = `Inductive nparams; - K.joint_defs = List.map (build_inductive seed) l - }) - -and - build_inductive seed = - let module K = Content in - fun (_,n,b,ty,l) -> - `Inductive - { K.inductive_id = gen_id inductive_prefix seed; - K.inductive_name = n; - K.inductive_kind = b; - K.inductive_type = ty; - K.inductive_constructors = build_constructors seed l - } - -and - build_constructors seed l = - let module K = Content in - List.map - (fun (n,t) -> - { K.dec_name = Some n; - K.dec_id = gen_id declaration_prefix seed; - K.dec_inductive = false; - K.dec_aref = ""; - K.dec_type = t - }) l -*) in res,ids_to_refs ;; diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 7ab9299fb..5f3f413bf 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -944,6 +944,7 @@ let current_proof_uri = BuildTimeConf.current_proof_uri type term_source = [ `Ast of CicNotationPt.term | `Cic of Cic.term * Cic.metasenv + | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution | `String of string ] @@ -1264,6 +1265,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `About `Grammar -> self#grammar () | `Check term -> self#_loadCheck term | `Cic (term, metasenv) -> self#_loadTermCic term metasenv + | `NCic (term, ctx, metasenv, subst) -> + self#_loadTermNCic term metasenv subst ctx | `Dir dir -> self#_loadDir dir | `HBugs `Tutors -> self#_loadHBugsTutors | `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) -> @@ -1447,6 +1450,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) mathView#load_sequent (sequent :: metasenv) dummyno; self#_showMath + method private _loadTermNCic term m s c = + let d = 0 in + let m = (0,(None,c,term))::m in + let status = (MatitaScript.current ())#grafite_status in + mathView#nload_sequent status m s d; + self#_showMath + method private _loadList l = model#list_store#clear (); List.iter (fun (tag, s) -> model#easy_append ~tag s) l; diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index bbe76859f..9874e7184 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -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 diff --git a/helm/software/matita/matitaTypes.ml b/helm/software/matita/matitaTypes.ml index 2584f61f6..4f2d414ee 100644 --- a/helm/software/matita/matitaTypes.ml +++ b/helm/software/matita/matitaTypes.ml @@ -45,6 +45,7 @@ type mathViewer_entry = [ `About of abouts (* current proof *) | `Check of string (* term *) | `Cic of Cic.term * Cic.metasenv + | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution | `Dir of string (* "directory" in cic uris namespace *) | `HBugs of [ `Tutors ] (* list of available HBugs tutors *) | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ] @@ -64,6 +65,7 @@ let string_of_entry = function | `About `Grammar -> "about:grammar" | `Check _ -> "check:" | `Cic (_, _) -> "term:" + | `NCic (_, _, _, _) -> "nterm:" | `Dir uri -> uri | `HBugs `Tutors -> "hbugs:/tutors/" | `Metadata meta -> diff --git a/helm/software/matita/matitaTypes.mli b/helm/software/matita/matitaTypes.mli index 34e98cc1a..ecc78a629 100644 --- a/helm/software/matita/matitaTypes.mli +++ b/helm/software/matita/matitaTypes.mli @@ -32,6 +32,7 @@ type mathViewer_entry = [ `About of abouts | `Check of string | `Cic of Cic.term * Cic.metasenv + | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution | `Dir of string | `HBugs of [ `Tutors ] | `Metadata of [ `Deps of [`Fwd | `Back] * UriManager.uri ] -- 2.39.2