From: Andrea Asperti Date: Thu, 20 Oct 2011 16:16:24 +0000 (+0000) Subject: 1. ported to camlp5 X-Git-Tag: make_still_working~2163 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dab25d81b789fb8430ef76f2dd77970c2c410048;p=helm.git 1. ported to camlp5 2. added a boolean to qed to governe indexing the syntax for disabling indexing is "qed-" --- diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index e34b690d3..4894218e8 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -321,9 +321,9 @@ let extract_term_production status pattern = | Ast.List0 (_, None) -> Gramext.Slist0 s | Ast.List1 (_, None) -> Gramext.Slist1 s | Ast.List0 (_, Some l) -> - Gramext.Slist0sep (s, gram_of_literal status l, true) + Gramext.Slist0sep (s, gram_of_literal status l) | Ast.List1 (_, Some l) -> - Gramext.Slist1sep (s, gram_of_literal status l, true) + Gramext.Slist1sep (s, gram_of_literal status l) | _ -> assert false in [ Env (List.map Env.list_declaration p_names), diff --git a/matitaB/components/grafite/grafiteAst.ml b/matitaB/components/grafite/grafiteAst.ml index 0db31e94d..bb496f2c0 100644 --- a/matitaB/components/grafite/grafiteAst.ml +++ b/matitaB/components/grafite/grafiteAst.ml @@ -105,7 +105,7 @@ type command = | NCoercion of loc * string * (NotationPt.term * NotationPt.term * (string * NotationPt.term) * NotationPt.term) option - | NQed of loc + | NQed of loc * bool (* ex lexicon commands *) | Alias of loc * alias_spec (** parameters, name, type, fields *) diff --git a/matitaB/components/grafite/grafiteAstPp.ml b/matitaB/components/grafite/grafiteAstPp.ml index c49937127..78bb51971 100644 --- a/matitaB/components/grafite/grafiteAstPp.ml +++ b/matitaB/components/grafite/grafiteAstPp.ml @@ -167,7 +167,7 @@ let pp_ncommand status = function | NUnivConstraint (_) -> "not supported" | NCoercion (_) -> "not supported" | NObj (_,obj) -> NotationPp.pp_obj (NotationPp.pp_term status) obj - | NQed (_) -> "nqed" + | NQed (_,_) -> "nqed" | NCopy (_,name,uri,map) -> "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ String.concat " and " diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml index c0d9baee7..1aa234211 100644 --- a/matitaB/components/grafite_engine/grafiteEngine.ml +++ b/matitaB/components/grafite_engine/grafiteEngine.ml @@ -524,7 +524,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *) let aliases = GrafiteDisambiguate.aliases_for_objs status composites in eval_alias status (mode,aliases) - | GrafiteAst.NQed loc -> + | GrafiteAst.NQed (loc,index) -> if status#ng_mode <> `ProofMode then raise (GrafiteTypes.Command_error "Not in proof mode") else @@ -559,7 +559,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let obj = uri,height,[],[],obj_kind in let old_status = status in let status = NCicLibrary.add_obj status obj in - let index_obj = + let index_obj = index && match obj_kind with NCic.Constant (_,_,_,_,(_,`Example,_)) | NCic.Fixpoint (_,_,(_,`Example,_)) -> false @@ -625,7 +625,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let _,_,menv,_,_ = invobj in (match menv with [] -> eval_ncommand ~include_paths opts status - ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false)) | _ -> status)) (* XXX *) with _ -> (*HLog.warn "error in generating inversion principle"; *) @@ -699,7 +699,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let status = status#set_stack ninitial_stack in let status = subst_metasenv_and_fix_names status in let status = status#set_ng_mode `ProofMode in - eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false)) | GrafiteAst.NObj (loc,obj) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") @@ -715,7 +715,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let status = status#set_ng_mode `ProofMode in (match nmenv with [] -> - eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,true)) | _ -> status) | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) -> if status#ng_mode <> `CommandMode then @@ -776,7 +776,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (match menv with [] -> eval_ncommand ~include_paths opts status - ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false)) | _ -> assert false) | GrafiteAst.NUnivConstraint (loc,u1,u2) -> eval_add_constraint status [`Type,u1] [`Type,u2] diff --git a/matitaB/components/grafite_parser/grafiteParser.ml b/matitaB/components/grafite_parser/grafiteParser.ml index 3e77258e0..1010e2c83 100644 --- a/matitaB/components/grafite_parser/grafiteParser.ml +++ b/matitaB/components/grafite_parser/grafiteParser.ml @@ -536,7 +536,8 @@ EXTEND ]]; grafite_ncommand: [ [ - IDENT "qed" -> G.NQed loc + IDENT "qed" ; b = OPT SYMBOL "-" -> + let b = match b with None -> true | Some _ -> false in G.NQed (loc,b) | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular)) diff --git a/matitaB/components/grafite_parser/print_grammar.ml b/matitaB/components/grafite_parser/print_grammar.ml index 6bcc14687..5bc87f247 100644 --- a/matitaB/components/grafite_parser/print_grammar.ml +++ b/matitaB/components/grafite_parser/print_grammar.ml @@ -87,7 +87,7 @@ and is_symbol_dummy = function | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt | Snterm e | Snterml (e, _) -> is_entry_dummy e | Slist1 x | Slist0 x -> is_symbol_dummy x - | Slist1sep (x,y,_) | Slist0sep (x,y,_) -> is_symbol_dummy x && is_symbol_dummy y + | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y | Sopt x -> is_symbol_dummy x | Sself | Snext -> false | Stree t -> is_tree_dummy t @@ -186,7 +186,7 @@ let visit_description desc fmt self = let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]} @ "; todo - | Slist0sep (symbol,sep,_) -> + | Slist0sep (symbol,sep) -> Format.fprintf fmt "[@[ "; let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "{@[ "; @@ -200,7 +200,7 @@ let visit_description desc fmt self = let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "@]}+ @ "; todo - | Slist1sep (symbol,sep,_) -> + | Slist1sep (symbol,sep) -> let todo = visit_symbol symbol todo is_son in Format.fprintf fmt "{@[ "; let todo = visit_symbol sep todo is_son in