From 91d21783f8ef99251f1868ea286c395d7f653ac5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 18 Nov 2011 15:48:16 +0000 Subject: [PATCH] short notation for "coercion" --- matita/components/grafite/grafiteAst.ml | 3 +- .../grafite_engine/grafiteEngine.ml | 28 ++++++++++++++++++- .../grafite_parser/grafiteParser.ml | 6 ++-- 3 files changed, 32 insertions(+), 5 deletions(-) diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index e96cf1bbc..2d55e8634 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -104,7 +104,8 @@ type command = | NInverter of loc * string * nterm * bool list option * nterm option | NUnivConstraint of loc * NUri.uri * NUri.uri | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list - | NCoercion of loc * string * bool * nterm * nterm * (string * nterm) * nterm + | NCoercion of loc * string * bool * + (nterm * nterm * (string * nterm) * nterm) option | NQed of loc * bool (* ex lexicon commands *) | Alias of loc * alias_spec diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 59821ac09..d3da51af0 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -485,7 +485,33 @@ 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, compose, t, ty, source, target) -> + | GrafiteAst.NCoercion (loc, name, compose, None) -> + let status, t, ty, source, target = + let o_t = NotationPt.Ident (name,None) 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 compose 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, compose, Some (t, ty, source, target)) -> let status, composites = NCicCoercDeclaration.eval_ncoercion status name compose t ty source target in diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 5f1b212bc..c1b059991 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -545,12 +545,12 @@ EXTEND G.UnificationHint (loc, t, n) | IDENT "coercion"; name = IDENT; compose = OPT [ IDENT "nocomposites" -> () ]; - SYMBOL ":"; ty = term; + spec = OPT [ SYMBOL ":"; ty = term; SYMBOL <:unicode>; t = term; "on"; id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term; - "to"; target = term -> + "to"; target = term -> t,ty,(id,source),target ] -> let compose = compose = None in - G.NCoercion(loc,name,compose,t,ty,(id,source),target) + G.NCoercion(loc,name,compose,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"; -- 2.39.2