From: Enrico Tassi Date: Mon, 17 Oct 2011 13:24:47 +0000 (+0000) Subject: compact coercion command: "coercion foo." X-Git-Tag: make_still_working~2178 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=237f4bfbb6d79b38e9417b776495b068b54aff6a;p=helm.git compact coercion command: "coercion foo." --- diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index 4894218e8..e34b690d3 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) + Gramext.Slist0sep (s, gram_of_literal status l, true) | Ast.List1 (_, Some l) -> - Gramext.Slist1sep (s, gram_of_literal status l) + Gramext.Slist1sep (s, gram_of_literal status l, true) | _ -> 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 9d4d3490a..0db31e94d 100644 --- a/matitaB/components/grafite/grafiteAst.ml +++ b/matitaB/components/grafite/grafiteAst.ml @@ -103,8 +103,8 @@ type command = | NUnivConstraint of loc * NUri.uri * NUri.uri | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list | NCoercion of loc * string * - NotationPt.term * NotationPt.term * - (string * NotationPt.term) * NotationPt.term + (NotationPt.term * NotationPt.term * + (string * NotationPt.term) * NotationPt.term) option | NQed of loc (* ex lexicon commands *) | Alias of loc * alias_spec diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml index cbaa4d93a..c0d9baee7 100644 --- a/matitaB/components/grafite_engine/grafiteEngine.ml +++ b/matitaB/components/grafite_engine/grafiteEngine.ml @@ -493,7 +493,32 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = GrafiteTypes.Serializer.require ~alias_only ~baseuri ~fname:fullpath status | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n - | GrafiteAst.NCoercion (loc, name, t, ty, source, target) -> + | GrafiteAst.NCoercion (loc, name, None) -> + let status, t, ty, source, target = + let o_t = NotationPt.Ident (name,`Ambiguous) in + let metasenv,subst, status,t = + GrafiteDisambiguate.disambiguate_nterm + status None [] [] [] ("",0,o_t) in + assert( metasenv = [] && subst = []); + let ty = NCicTypeChecker.typeof status [] [] [] t in + let source, target = + let clean = function + | NCic.Appl (NCic.Const _ as r :: l) -> + NotationPt.Appl (NotationPt.NCic r :: + List.map (fun _ -> NotationPt.Implicit `JustOne)l) + | NCic.Const _ as r -> NotationPt.NCic r + | _ -> assert false in + let rec aux = function + | NCic.Prod (_,_, (NCic.Prod _ as rest)) -> aux rest + | NCic.Prod (name, src, tgt) -> (name, clean src), clean tgt + | _ -> assert false in aux ty in + status, o_t, NotationPt.NCic ty, source, target in + let status, composites = + NCicCoercDeclaration.eval_ncoercion status name t ty source target in + let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *) + let aliases = GrafiteDisambiguate.aliases_for_objs status composites in + eval_alias status (mode,aliases) + | GrafiteAst.NCoercion (loc, name, Some (t, ty, source, target)) -> let status, composites = NCicCoercDeclaration.eval_ncoercion status name t ty source target in let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *) diff --git a/matitaB/components/grafite_parser/grafiteParser.ml b/matitaB/components/grafite_parser/grafiteParser.ml index 30a97a3e3..3e77258e0 100644 --- a/matitaB/components/grafite_parser/grafiteParser.ml +++ b/matitaB/components/grafite_parser/grafiteParser.ml @@ -221,7 +221,7 @@ EXTEND G.NMacro(loc, G.NAutoInteractive (loc, (None,["depth",depth]@params)))) | IDENT "intros" -> G.NMacro (loc, G.NIntroGuess loc) - | IDENT "check"; t = term -> G.NMacro(loc,G.NCheck (loc,t)) + | IDENT "check"; t = tactic_term -> G.NMacro(loc,G.NCheck (loc,t)) | IDENT "screenshot"; fname = QSTRING -> G.NMacro(loc,G.Screenshot (loc, fname)) | IDENT "cases"; what = tactic_term ; where = pattern_spec -> @@ -576,11 +576,11 @@ EXTEND G.NUnivConstraint (loc,u1,u2) | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term -> G.UnificationHint (loc, t, n) - | IDENT "coercion"; name = IDENT; SYMBOL ":"; ty = term; + | IDENT "coercion"; name = IDENT; spec = OPT [ SYMBOL ":"; ty = term; SYMBOL <:unicode>; t = term; "on"; id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term; - "to"; target = term -> - G.NCoercion(loc,name,t,ty,(id,source),target) + "to"; target = term -> t,ty,(id,source),target ] -> + G.NCoercion(loc,name,spec) | IDENT "record" ; (params,name,ty,fields) = record_spec -> G.NObj (loc, N.Record (params,name,ty,fields)) | IDENT "copy" ; s = IDENT; IDENT "from"; u = URI; "with"; diff --git a/matitaB/components/grafite_parser/print_grammar.ml b/matitaB/components/grafite_parser/print_grammar.ml index 5bc87f247..6bcc14687 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