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 *)
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
| 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 *)
| 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
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
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
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
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 =
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
in
(params,name,typ,fields)
] ];
+
+ nmacro: [
+ [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t)
+ ]
+ ];
macro: [
[ [ IDENT "check" ]; t = term ->
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: [
| 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
let object_prefix = "obj:";;
let declaration_prefix = "decl:";;
let definition_prefix = "def:";;
+let inductive_prefix = "ind:";;
+let joint_prefix = "joint:";;
let get_id =
function
(*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,
`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
;;
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
]
| `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)) ->
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;
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
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
[ `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 ]
| `About `Grammar -> "about:grammar"
| `Check _ -> "check:"
| `Cic (_, _) -> "term:"
+ | `NCic (_, _, _, _) -> "nterm:"
| `Dir uri -> uri
| `HBugs `Tutors -> "hbugs:/tutors/"
| `Metadata meta ->
[ `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 ]
projects / helm.git / commitdiff