From 8aa44cb352041dd314011996b4b1a1ff8990a000 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 26 May 2011 09:27:38 +0000 Subject: [PATCH] Added "nocomposites" to coercions. --- matita/components/grafite/grafiteAst.ml | 6 ++---- .../grafite_engine/grafiteEngine.ml | 7 ++++--- .../grafite_engine/nCicCoercDeclaration.ml | 21 ++++++++++--------- .../grafite_engine/nCicCoercDeclaration.mli | 5 +++-- .../grafite_parser/grafiteParser.ml | 5 +++-- .../components/ng_paramodulation/nCicProof.ml | 2 +- .../components/ng_refiner/nCicUnification.ml | 2 ++ matita/components/syntax_extensions/.depend | 10 ++++----- 8 files changed, 31 insertions(+), 27 deletions(-) diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index ff26c00d6..6b5344f58 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -84,7 +84,7 @@ type nmacro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 35 +let magic = 36 (* composed magic: term + command magics. No need to change this value *) let magic = magic + 10000 * NotationPt.magic @@ -104,9 +104,7 @@ 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 * - nterm * nterm * - (string * nterm) * nterm + | NCoercion of loc * string * bool * nterm * nterm * (string * nterm) * nterm | NQed of loc (* 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 2f37a4e92..f286cf6b8 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -485,9 +485,10 @@ 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, compose, t, ty, source, target) -> let status, composites = - NCicCoercDeclaration.eval_ncoercion status name t ty source target in + 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) @@ -622,7 +623,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let status, nuris = NCicCoercDeclaration. basic_eval_and_record_ncoercion_from_t_cpos_arity - status (name,t,cpos,arity) in + status (name,true,t,cpos,arity) in let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in eval_alias status (mode,aliases) with MultiPassDisambiguator.DisambiguationError _-> diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml index f1b051d46..929d11235 100644 --- a/matita/components/grafite_engine/nCicCoercDeclaration.ml +++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml @@ -259,11 +259,11 @@ let close_graph name t s d to_s from_d p a status = ;; (* idempotent *) -let basic_index_ncoercion (name,t,s,d,position,arity) status = +let basic_index_ncoercion (name,_compose,t,s,d,position,arity) status = NCicCoercion.index_coercion status name t s d arity position ;; -let basic_eval_ncoercion (name,t,s,d,p,a) status = +let basic_eval_ncoercion (name,compose,t,s,d,p,a) status = let to_s = NCicCoercion.look_for_coercion status [] [] [] skel_dummy s in @@ -271,10 +271,11 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status = NCicCoercion.look_for_coercion status [] [] [] d skel_dummy in let status = NCicCoercion.index_coercion status name t s d a p in - let composites = close_graph name t s d to_s from_d p a status in + let composites = + if compose then close_graph name t s d to_s from_d p a status else [] in List.fold_left (fun (uris,infos,st) ((uri,_,_,_,_ as obj),name,t,s,d,p,a) -> - let info = name,t,s,d,p,a in + let info = name,compose,t,s,d,p,a in let st = NCicLibrary.add_obj st obj in let st = basic_index_ncoercion info st in uri::uris, info::infos, st) @@ -282,11 +283,11 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status = ;; let record_ncoercion = - let aux (name,t,s,d,p,a) ~refresh_uri_in_term = + let aux (name,compose,t,s,d,p,a) ~refresh_uri_in_term = let t = refresh_uri_in_term t in let s = refresh_uri_in_term s in let d = refresh_uri_in_term d in - basic_index_ncoercion (name,t,s,d,p,a) + basic_index_ncoercion (name,compose,t,s,d,p,a) in let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status @@ -305,17 +306,17 @@ let basic_eval_and_record_ncoercion infos status = ;; let basic_eval_and_record_ncoercion_from_t_cpos_arity - status (name,t,cpos,arity) + status (name,compose,t,cpos,arity) = let ty = NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] [] t in let src,tgt = src_tgt_of_ty_cpos_arity status ty cpos arity in let status, uris = - basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status + basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status in status,uris ;; -let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt = +let eval_ncoercion (status: #GrafiteTypes.status) name compose t ty (id,src) tgt = let metasenv,subst,status,ty = GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in assert (metasenv=[]); @@ -327,7 +328,7 @@ let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt = let status, src, tgt, cpos, arity = src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in let status, uris = - basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status + basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status in status,uris ;; diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.mli b/matita/components/grafite_engine/nCicCoercDeclaration.mli index 9bca1143d..66e3a561b 100644 --- a/matita/components/grafite_engine/nCicCoercDeclaration.mli +++ b/matita/components/grafite_engine/nCicCoercDeclaration.mli @@ -10,10 +10,11 @@ V_______________________________________________________________ *) -(* evals a coercion declaration statement: name t ty (id,src) tgt *) +(* evals a coercion declaration statement: name compose t ty (id,src) tgt *) val eval_ncoercion: #GrafiteTypes.status as 'status -> string -> + bool -> NotationPt.term -> NotationPt.term -> string * NotationPt.term -> @@ -24,5 +25,5 @@ val eval_ncoercion: * the arity in the `:arity>` syntax *) val basic_eval_and_record_ncoercion_from_t_cpos_arity: #GrafiteTypes.status as 'status -> - string * NCic.term * int * int -> 'status * NUri.uri list + string * bool * NCic.term * int * int -> 'status * NUri.uri list diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index aeb0080c4..762da10f5 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -579,8 +579,9 @@ EXTEND | IDENT "coercion"; name = IDENT; 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; compose = OPT [ IDENT "nocomposites" -> () ] -> + let compose = compose = None in + G.NCoercion(loc,name,compose,t,ty,(id,source),target) | 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/matita/components/ng_paramodulation/nCicProof.ml b/matita/components/ng_paramodulation/nCicProof.ml index cabca8259..3f30a85c3 100644 --- a/matita/components/ng_paramodulation/nCicProof.ml +++ b/matita/components/ng_paramodulation/nCicProof.ml @@ -181,7 +181,7 @@ let debug c _ = c;; List.fold_left (fun (i,acc) t -> i+1, - let f = extract status amount vl f in + let f = extract status amount vl f in if i = n then let imp = NCic.Implicit `Term in NCic.Appl (dag::imp::imp::imp(* f *)::imp::imp:: diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml index 1e37ff797..c8f67f176 100644 --- a/matita/components/ng_refiner/nCicUnification.ml +++ b/matita/components/ng_refiner/nCicUnification.ml @@ -99,6 +99,8 @@ let outside exc_opt = match !times with time1::tl -> times := tl; time1 | [] -> assert false in prerr_endline ("}}} " ^ !indent ^ " " ^ string_of_float (time2 -. time1)); (match exc_opt with + | Some (UnificationFailure msg) -> prerr_endline ("exception raised: NCicUnification.UnificationFailure:" ^ Lazy.force msg) + | Some (Uncertain msg) -> prerr_endline ("exception raised: NCicUnification.Uncertain:" ^ Lazy.force msg) | Some e -> prerr_endline ("exception raised: " ^ Printexc.to_string e) | None -> ()); try diff --git a/matita/components/syntax_extensions/.depend b/matita/components/syntax_extensions/.depend index 25e67131f..119f13093 100644 --- a/matita/components/syntax_extensions/.depend +++ b/matita/components/syntax_extensions/.depend @@ -1,5 +1,5 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: -utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi -utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: +utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi +utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi -- 2.39.2