From f7da48c844105a52a705872dfa0d4104de010c82 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 1 Feb 2013 13:47:25 +0000 Subject: [PATCH] - ng_refiner: now the expected type is `XTNone (was None), `XTSome (was Some, also was `Term), `XTSort (any sort, was `Sort), `XTInd (any (co)inductive type). `XTProd (was `Prod) is used in "try_coercions" - we replaced some instances of None with `XTSort or `XTInd through the code. lib, lambda, and lambdadelta compile, in case of errors like "the term ... is not a sort" or "the term ... is not a (co)inductive type", revert to `XTNone in the corresponding check. - Now generated objects have the `Generated attribute properly set - lambda: many "?" removed because of the improvement in the refiner other instances of "?" removed for other reasons --- matita/components/content/notationPp.ml | 2 +- matita/components/content/notationPt.ml | 4 +- matita/components/content/notationUtil.ml | 4 +- .../components/disambiguation/disambiguate.ml | 2 +- .../disambiguation/disambiguate.mli | 5 +- .../disambiguation/disambiguateTypes.ml | 6 + .../disambiguation/disambiguateTypes.mli | 6 + .../disambiguation/multiPassDisambiguator.mli | 4 +- .../grafite_engine/grafiteEngine.ml | 20 +- .../grafite_engine/nCicCoercDeclaration.ml | 8 +- .../grafite_parser/grafiteParser.ml | 12 +- .../ng_cic_content/interpretations.ml | 4 +- .../ng_disambiguation/grafiteDisambiguate.ml | 2 +- .../ng_disambiguation/grafiteDisambiguate.mli | 2 +- .../ng_disambiguation/nCicDisambiguate.ml | 39 +- .../ng_disambiguation/nCicDisambiguate.mli | 2 +- matita/components/ng_refiner/nCicRefiner.ml | 361 +++++++++++------- matita/components/ng_refiner/nCicRefiner.mli | 7 +- .../components/ng_refiner/nCicUnification.ml | 25 ++ .../components/ng_refiner/nCicUnification.mli | 4 + matita/components/ng_tactics/nCicElim.ml | 7 +- matita/components/ng_tactics/nDestructTac.ml | 6 +- matita/components/ng_tactics/nInversion.ml | 6 +- matita/components/ng_tactics/nTacStatus.ml | 22 +- matita/components/ng_tactics/nTacStatus.mli | 4 +- matita/components/ng_tactics/nTactics.ml | 13 +- matita/components/ng_tactics/nnAuto.ml | 13 +- .../contribs/lambda/background/preamble.ma | 2 +- .../contribs/lambda/paths/dst_computation.ma | 28 +- .../paths/labeled_sequential_reduction.ma | 8 +- .../lambda/paths/labeled_st_computation.ma | 48 +-- .../lambda/paths/labeled_st_reduction.ma | 20 +- matita/matita/contribs/lambda/paths/path.ma | 2 +- .../contribs/lambda/paths/standard_order.ma | 6 +- .../contribs/lambda/paths/standard_trace.ma | 8 +- matita/matita/contribs/lambda/paths/trace.ma | 2 +- .../subterms/relocating_substitution.ma | 4 +- .../contribs/lambda/subterms/relocation.ma | 4 +- .../terms/labeled_sequential_computation.ma | 2 +- .../lambda/terms/parallel_reduction.ma | 10 +- .../lambda/terms/relocating_substitution.ma | 2 +- .../contribs/lambda/terms/relocation.ma | 4 +- .../lambda/terms/sequential_computation.ma | 2 +- matita/matita/matitaScript.ml | 2 +- 44 files changed, 432 insertions(+), 312 deletions(-) diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml index 8828a0321..d9ba51db0 100644 --- a/matita/components/content/notationPp.ml +++ b/matita/components/content/notationPp.ml @@ -317,7 +317,7 @@ let pp_obj pp_term = function (pp_term typ) (pp_constructors constructors) in fst_typ_pp ^ String.concat "" (List.map pp_type tl)) - | Ast.Theorem (flavour, name, typ, body,_) -> + | Ast.Theorem (name, typ, body,(_,flavour,_)) -> sprintf "%s %s:\n %s\n%s" (NCicPp.string_of_flavour flavour) name diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml index cead5e7ae..087a43dde 100644 --- a/matita/components/content/notationPt.ml +++ b/matita/components/content/notationPt.ml @@ -177,8 +177,8 @@ type 'term inductive_type = string * bool * 'term * (string * 'term) list type 'term obj = | Inductive of 'term capture_variable list * 'term inductive_type list (** parameters, list of loc * mutual inductive types *) - | Theorem of NCic.def_flavour * string * 'term * 'term option * NCic.def_pragma - (** flavour, name, type, body + | Theorem of string * 'term * 'term option * NCic.c_attr + (** name, type, body, attributes * - name is absent when an unnamed theorem is being proved, tipically in * interactive usage * - body is present when its given along with the command, otherwise it diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml index 3d80e8fd5..3683c0c0e 100644 --- a/matita/components/content/notationUtil.ml +++ b/matita/components/content/notationUtil.ml @@ -386,11 +386,11 @@ let freshen_obj obj = indtypes in NotationPt.Inductive (freshen_capture_variables params, indtypes) - | NotationPt.Theorem (flav, n, t, ty_opt,p) -> + | NotationPt.Theorem (n, t, ty_opt, attrs) -> let ty_opt = match ty_opt with None -> None | Some ty -> Some (freshen_term ty) in - NotationPt.Theorem (flav, n, freshen_term t, ty_opt,p) + NotationPt.Theorem (n, freshen_term t, ty_opt, attrs) | NotationPt.Record (params, n, ty, fields) -> NotationPt.Record (freshen_capture_variables params, n, freshen_term ty, freshen_name_ty_b fields) diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml index 4476d562a..95d6082d0 100644 --- a/matita/components/disambiguation/disambiguate.ml +++ b/matita/components/disambiguation/disambiguate.ml @@ -334,7 +334,7 @@ let domain_of_term ~context term = let domain_of_obj ~context ast = assert (context = []); match ast with - | Ast.Theorem (_,_,ty,bo,_) -> + | Ast.Theorem (_,ty,bo,_) -> domain_of_term [] ty @ (match bo with None -> [] diff --git a/matita/components/disambiguation/disambiguate.mli b/matita/components/disambiguation/disambiguate.mli index 167de714b..e0464a1d5 100644 --- a/matita/components/disambiguation/disambiguate.mli +++ b/matita/components/disambiguation/disambiguate.mli @@ -93,7 +93,7 @@ val disambiguate_thing: use_coercions:bool -> string_context_of_context:('context -> string option list) -> initial_ugraph:'ugraph -> - expty: 'refined_thing option -> + expty: 'refined_thing DisambiguateTypes.expected_type -> mk_implicit:(bool -> 'alias) -> description_of_alias:('alias -> string) -> fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> @@ -117,10 +117,11 @@ val disambiguate_thing: 'raw_thing) -> refine_thing:( 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool -> - 'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash -> + 'raw_thing -> 'refined_thing DisambiguateTypes.expected_type -> 'ugraph -> localization_tbl:'cichash -> ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> mk_localization_tbl:(int -> 'cichash) -> 'ast_thing disambiguator_input -> ((DisambiguateTypes.Environment.key * 'alias) list * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool + diff --git a/matita/components/disambiguation/disambiguateTypes.ml b/matita/components/disambiguation/disambiguateTypes.ml index f6e03d098..50d1d59da 100644 --- a/matita/components/disambiguation/disambiguateTypes.ml +++ b/matita/components/disambiguation/disambiguateTypes.ml @@ -25,6 +25,12 @@ (* $Id$ *) +type 'a expected_type = [ `XTNone (* unknown *) + | `XTSome of 'a (* the given term *) + | `XTSort (* any sort *) + | `XTInd (* any (co)inductive type *) + ] + type domain_item = | Id of string (* literal *) | Symbol of string * int (* literal, instance num *) diff --git a/matita/components/disambiguation/disambiguateTypes.mli b/matita/components/disambiguation/disambiguateTypes.mli index 1e99fd404..ef24e2ce8 100644 --- a/matita/components/disambiguation/disambiguateTypes.mli +++ b/matita/components/disambiguation/disambiguateTypes.mli @@ -23,6 +23,12 @@ * http://helm.cs.unibo.it/ *) +type 'a expected_type = [ `XTNone (* unknown *) + | `XTSome of 'a (* the given term *) + | `XTSort (* any sort *) + | `XTInd (* any (co)inductive type *) + ] + type domain_item = | Id of string (* literal *) | Symbol of string * int (* literal, instance num *) diff --git a/matita/components/disambiguation/multiPassDisambiguator.mli b/matita/components/disambiguation/multiPassDisambiguator.mli index 41b79c9b0..6bdfdaae2 100644 --- a/matita/components/disambiguation/multiPassDisambiguator.mli +++ b/matita/components/disambiguation/multiPassDisambiguator.mli @@ -47,7 +47,7 @@ val disambiguate_thing: subst:'subst -> string_context_of_context:('context -> string option list) -> initial_ugraph:'ugraph -> - expty: 'refined_thing option -> + expty: 'refined_thing DisambiguateTypes.expected_type -> mk_implicit:(bool -> 'alias) -> description_of_alias:('alias -> string) -> fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> @@ -73,7 +73,7 @@ val disambiguate_thing: 'raw_thing) -> refine_thing:( 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool -> - 'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash -> + 'raw_thing -> 'refined_thing DisambiguateTypes.expected_type -> 'ugraph -> localization_tbl:'cichash -> ('refined_thing, 'metasenv,'subst,'ugraph) Disambiguate.test_result) -> mk_localization_tbl:(int -> 'cichash) -> string * int * 'ast_thing -> diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 15e20277f..9fbcd9472 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -55,7 +55,7 @@ let inject_unification_hint = let eval_unification_hint status t n = let metasenv,subst,status,t = - GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in + GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] ("",0,t) in assert (metasenv=[]); let t = NCicUntrusted.apply_subst status subst [] t in let status = basic_eval_unification_hint (t,n) status in @@ -540,7 +540,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let o_t = NotationPt.Ident (name,None) in let metasenv,subst, status,t = GrafiteDisambiguate.disambiguate_nterm - status None [] [] [] ("",0,o_t) in + status `XTNone [] [] [] ("",0,o_t) in assert( metasenv = [] && subst = []); let ty = NCicTypeChecker.typeof status [] [] [] t in let source, target = @@ -637,7 +637,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (*prerr_endline (status#ppobj obj);*) let boxml = NCicElim.mk_elims status obj in let boxml = boxml @ NCicElim.mk_projections status obj in - let status = status#set_ng_mode `CommandMode in + let status = status#set_ng_mode `CommandMode in let xxaliases = GrafiteDisambiguate.aliases_for_objs status [uri] in let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *) let status = eval_alias status (mode,xxaliases) in @@ -658,9 +658,11 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = else nstatus with - | MultiPassDisambiguator.DisambiguationError _ + | MultiPassDisambiguator.DisambiguationError _ as e -> + HLog.warn "error in disambiguating projection/eliminator"; + status | NCicTypeChecker.TypeCheckerFailure _ -> - (*HLog.warn "error in generating projection/eliminator";*) + HLog.warn "error in typechecking projection/eliminator"; status ) status boxml in let _,_,_,_,nobj = obj in @@ -768,7 +770,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (fun status (name,cpos,arity) -> try let metasenv,subst,status,t = - GrafiteDisambiguate.disambiguate_nterm status None [] [] [] + GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] [] ("",0,NotationPt.Ident (name,None)) in assert (metasenv = [] && subst = []); let status, nuris = @@ -849,7 +851,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = else let status = status#set_ng_mode `ProofMode in let metasenv,subst,status,indty = - GrafiteDisambiguate.disambiguate_nterm status None [] [] [] (text,prefix_len,indty) in + GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] (text,prefix_len,indty) in let indtyno, (_,_,tys,_,_),leftno = match indty with NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) -> indtyno, NCicEnvironment.get_checked_indtys status r, leftno @@ -870,7 +872,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let metasenv,subst,status,sort = match sort with | None -> [],[],status,NCic.Sort NCic.Prop | Some s -> - GrafiteDisambiguate.disambiguate_nterm status None [] [] [] + GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] (text,prefix_len,s) in assert (metasenv = []); @@ -884,7 +886,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (status#ppterm ~metasenv ~subst ~context:[] sort))) in let status = status#set_ng_mode `ProofMode in let metasenv,subst,status,indty = - GrafiteDisambiguate.disambiguate_nterm status None [] [] subst + GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] subst (text,prefix_len,indty) in let indtyno,(_,leftno,tys,_,_) = match indty with diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml index 1c6c63ebc..74a7eb6a4 100644 --- a/matita/components/grafite_engine/nCicCoercDeclaration.ml +++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml @@ -133,7 +133,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt = (try let metasenv,subst,status,src = GrafiteDisambiguate.disambiguate_nterm - status None ctx [] [] ("",0,src) in + status `XTSort ctx [] [] ("",0,src) in let src = NCicUntrusted.apply_subst status subst [] src in (* CHECK that the declared pattern matches the abstraction *) let _ = NCicUnification.unify status metasenv subst ctx ty src in @@ -154,7 +154,7 @@ disambiguation error"))) let status, tgt, arity = let metasenv,subst,status,tgt = GrafiteDisambiguate.disambiguate_nterm - status None [] [] [] ("",0,tgt) in + status `XTSort [] [] [] ("",0,tgt) in let tgt = NCicUntrusted.apply_subst status subst [] tgt in (* CHECK che sia unificabile mancante *) let rec count_prod = function @@ -321,11 +321,11 @@ let basic_eval_and_record_ncoercion_from_t_cpos_arity 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 + GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] ("",0,ty) in assert (metasenv=[]); let ty = NCicUntrusted.apply_subst status subst [] ty in let metasenv,subst,status,t = - GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in + GrafiteDisambiguate.disambiguate_nterm status (`XTSome ty) [] [] [] ("",0,t) in assert (metasenv=[]); let t = NCicUntrusted.apply_subst status subst [] t in let status, src, tgt, cpos, arity = diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 4e5c709f7..0a2103c9a 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -72,7 +72,8 @@ let mk_rec_corec ind_kind defs loc = | _ -> assert false in let body = N.Ident (name,None) in - (loc, N.Theorem(`Definition, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular)) + let attrs = `Provided, `Definition, `Regular in + (loc, N.Theorem(name, ty, Some (N.LetRec (ind_kind, defs, body)), attrs)) let nmk_rec_corec ind_kind defs loc index = let loc,t = mk_rec_corec ind_kind defs loc in @@ -508,14 +509,17 @@ EXTEND IDENT "qed" ; i = index -> G.NQed (loc,i) | 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),true) + let attrs = `Provided, nflavour, `Regular in + G.NObj (loc, N.Theorem (name, typ, body, attrs),true) | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); body = term -> + let attrs = `Provided, nflavour, `Regular in G.NObj (loc, - N.Theorem(nflavour, name, N.Implicit `JustOne, Some body,`Regular), + N.Theorem(name, N.Implicit `JustOne, Some body, attrs), true) | IDENT "axiom"; i = index; name = IDENT; SYMBOL ":"; typ = term -> - G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular),i) + let attrs = `Provided, `Axiom, `Regular in + G.NObj (loc, N.Theorem (name, typ, None, attrs),i) | IDENT "discriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty) | IDENT "inverter"; name = IDENT; IDENT "for" ; indty = tactic_term ; paramspec = OPT inverter_param_list ; diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml index 741cfa640..e2c8c76d0 100644 --- a/matita/components/ng_cic_content/interpretations.ml +++ b/matita/components/ng_cic_content/interpretations.ml @@ -639,13 +639,13 @@ let nmap_obj0 status ~idref (_, _, metasenv, subst, kind) = n, is_ind, ty, List.map (build_constractor lno context) cl in match kind with - | NCic.Constant (_, n, xbo, ty, (_, flavour, pragma)) -> + | NCic.Constant (_, n, xbo, ty, attrs) -> let ty = nast_of_cic ~context:[] ty in let xbo = match xbo with | Some bo -> Some (nast_of_cic ~context:[] bo) | None -> None in - N.Theorem (flavour, n, ty, xbo, pragma) + N.Theorem (n, ty, xbo, attrs) | NCic.Inductive (is_ind, lno, itl, (_, `Regular)) -> let captures, context = build_captures lno itl in N.Inductive (captures, List.map (build_inductive is_ind lno context) itl) diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml index dbdd21313..3601f4c44 100644 --- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml @@ -250,7 +250,7 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) = match obj with | NotationPt.Inductive (_,(name,_,_,_)::_) | NotationPt.Record (_,name,_,_) -> name ^ ".ind" - | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con" + | NotationPt.Theorem (name,_,_,_) -> name ^ ".con" | NotationPt.Inductive _ -> assert false in NUri.uri_of_string (baseuri ^ "/" ^ name) diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.mli b/matita/components/ng_disambiguation/grafiteDisambiguate.mli index 1f5553e91..c462af36f 100644 --- a/matita/components/ng_disambiguation/grafiteDisambiguate.mli +++ b/matita/components/ng_disambiguation/grafiteDisambiguate.mli @@ -60,7 +60,7 @@ exception BaseUriNotSetYet val disambiguate_nterm : #status as 'status -> - NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution -> + NCic.term NCicRefiner.expected_type -> NCic.context -> NCic.metasenv -> NCic.substitution -> NotationPt.term Disambiguate.disambiguator_input -> NCic.metasenv * NCic.substitution * 'status * NCic.term diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml index 8e3f26777..62d05509c 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml @@ -11,10 +11,8 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -open Printf - -open DisambiguateTypes - +module P = Printf +module DT = DisambiguateTypes module Ast = NotationPt module NRef = NReference @@ -36,7 +34,7 @@ let refine_term (status: #NCicCoercion.status) metasenv subst context uri ~use_c ~localization_tbl = assert (uri=None); - debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" + debug_print (lazy (P.sprintf "TEST_INTERPRETATION: %s" (status#ppterm ~metasenv ~subst ~context term))); try let localise t = @@ -58,7 +56,7 @@ let refine_term (status: #NCicCoercion.status) metasenv subst context uri ~use_c status#ppterm ~metasenv ~subst ~context term)) ; Disambiguate.Uncertain loc_msg | NCicRefiner.RefineFailure loc_msg -> - debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s" + debug_print (lazy (P.sprintf "PRUNED:\nterm%s\nmessage:%s" (status#ppterm ~metasenv ~subst ~context term) (snd(Lazy.force loc_msg)))); Disambiguate.Ko loc_msg ;; @@ -66,7 +64,7 @@ let refine_term (status: #NCicCoercion.status) metasenv subst context uri ~use_c let refine_obj status metasenv subst _context _uri ~use_coercions obj _ _ugraph ~localization_tbl = - (*prerr_endline ((sprintf "TEST_INTERPRETATION: %s" (status#ppobj obj)));*) + (*prerr_endline ((P.sprintf "TEST_INTERPRETATION: %s" (status#ppobj obj)));*) assert (metasenv=[]); assert (subst=[]); let localise t = @@ -89,7 +87,7 @@ let refine_obj status metasenv subst _context _uri ~use_coercions obj _ _ugraph status#ppobj obj)) ; Disambiguate.Uncertain loc_msg | NCicRefiner.RefineFailure loc_msg -> - debug_print (lazy (sprintf "PRUNED:\nobj: %s\nmessage: %s" + debug_print (lazy (P.sprintf "PRUNED:\nobj: %s\nmessage: %s" (status#ppobj obj) (snd(Lazy.force loc_msg)))); Disambiguate.Ko loc_msg ;; @@ -126,7 +124,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) aux ~localize loc context (NotationPt.Appl (inner @ args)) | NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) -> let cic_args = List.map (aux ~localize loc context) args in - Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args) + Disambiguate.resolve ~mk_choice ~env (DT.Symbol (symb, i)) (`Args cic_args) | NotationPt.Appl terms -> NCic.Appl (List.map (aux ~localize loc context) terms) | NotationPt.Binder (binder_kind, (var, typ), body) -> @@ -138,7 +136,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) | `Pi | `Forall -> NCic.Prod (cic_name, cic_type, cic_body) | `Exists -> - Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", 0)) + Disambiguate.resolve ~env ~mk_choice (DT.Symbol ("exists", 0)) (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ])) | NotationPt.Case (term, indty_ident, outtype, branches) -> let cic_term = aux ~localize loc context term in @@ -178,7 +176,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) match indty_ident with | Some (indty_ident, _) -> (match Disambiguate.resolve ~env ~mk_choice - (Id indty_ident) (`Args []) with + (DT.Id indty_ident) (`Args []) with | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r | NCic.Implicit _ -> raise (Disambiguate.Try_again @@ -193,7 +191,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) function (Ast.Pattern (head, _, _), _) :: _ -> head | (Ast.Wildcard, _) :: tl -> fst_constructor tl - | [] -> raise (Invalid_choice (lazy (loc,"The type "^ + | [] -> raise (DT.Invalid_choice (lazy (loc,"The type "^ "of the term to be matched cannot be determined "^ "because it is an inductive type without constructors "^ "or because all patterns use wildcards"))) @@ -206,7 +204,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) description_of_alias v)) env; *) (match Disambiguate.resolve ~env ~mk_choice - (Id (fst_constructor branches)) (`Args []) with + (DT.Id (fst_constructor branches)) (`Args []) with | NCic.Const (NReference.Ref (_,NReference.Con _) as r) -> let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in NReference.mk_indty b r @@ -321,7 +319,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) with Not_found -> try NCic.Const (List.assoc name obj_context) with Not_found -> - Disambiguate.resolve ~env ~mk_choice (Id name) (`Args [])) + Disambiguate.resolve ~env ~mk_choice (DT.Id name) (`Args [])) | NotationPt.Uri (uri, subst) -> assert (subst = None); (try @@ -335,7 +333,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) | NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s) | NotationPt.UserInput -> NCic.Implicit `Hole | NotationPt.Num (num, i) -> - Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num) + Disambiguate.resolve ~env ~mk_choice (DT.Num i) (`Num_arg num) | NotationPt.Meta (index, subst) -> let cic_subst = List.map @@ -352,7 +350,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) [`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")]) | NotationPt.Symbol (symbol, instance) -> Disambiguate.resolve ~env ~mk_choice - (Symbol (symbol, instance)) (`Args []) + (DT.Symbol (symbol, instance)) (`Args []) | NotationPt.Variable _ | NotationPt.Magic _ | NotationPt.Layout _ @@ -422,7 +420,8 @@ let interpretate_obj status interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in let uri = match uri with | None -> assert false | Some u -> u in match obj with - | NotationPt.Theorem (flavour, name, ty, bo, pragma) -> + | NotationPt.Theorem (name, ty, bo, attrs) -> + let _, flavour, _ = attrs in let ty' = interpretate_term status ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty @@ -431,11 +430,9 @@ let interpretate_obj status uri, height, [], [], (match bo,flavour with | None,`Axiom -> - let attrs = `Provided, flavour, pragma in NCic.Constant ([],name,None,ty',attrs) | Some _,`Axiom -> assert false | None,_ -> - let attrs = `Provided, flavour, pragma in NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs) | Some bo,_ -> (match bo with @@ -472,14 +469,12 @@ let interpretate_obj status ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body)) defs in - let attrs = `Provided, flavour, pragma in NCic.Fixpoint (inductive,inductiveFuns,attrs) | bo -> let bo = interpretate_term status ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo in - let attrs = `Provided, flavour, pragma in NCic.Constant ([],name,Some bo,ty',attrs))) | NotationPt.Inductive (params,tyl) -> let context,params = @@ -633,7 +628,7 @@ let disambiguate_obj (status: #NCicCoercion.status) ~interpretate_thing:(interpretate_obj status ~mk_choice) ~refine_thing:(refine_obj status) (text,prefix_len,obj) - ~mk_localization_tbl ~expty:None + ~mk_localization_tbl ~expty:`XTNone in List.map (function (a,b,c,d,_) -> a,b,c,d) res, b ;; diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.mli b/matita/components/ng_disambiguation/nCicDisambiguate.mli index 87bdd348a..5942909c2 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.mli +++ b/matita/components/ng_disambiguation/nCicDisambiguate.mli @@ -18,7 +18,7 @@ val disambiguate_term : context:NCic.context -> metasenv:NCic.metasenv -> subst:NCic.substitution -> - expty:NCic.term option -> + expty:NCic.term NCicRefiner.expected_type -> mk_implicit: (bool -> 'alias) -> description_of_alias:('alias -> string) -> fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml index 550c75e93..af8e1d87a 100644 --- a/matita/components/ng_refiner/nCicRefiner.ml +++ b/matita/components/ng_refiner/nCicRefiner.ml @@ -18,6 +18,12 @@ exception AssertFailure of string Lazy.t;; module C = NCic module Ref = NReference +type 'a expected_type = [ `XTNone (* unknown *) + | `XTSome of 'a (* the given term *) + | `XTSort (* any sort *) + | `XTInd (* any (co)inductive type *) + ] + let debug = ref false;; let indent = ref "";; let times = ref [];; @@ -62,15 +68,17 @@ let exp_implicit status ~localise metasenv subst context with_type t = | `Closed -> let metasenv,subst,expty = match with_type with - None -> metasenv,subst,None - | Some typ -> + `XTSort + | `XTInd + | `XTNone -> metasenv,subst,None + | `XTSome typ -> let (metasenv,subst),typ = try NCicMetaSubst.delift status ~unify:(fun m s c t1 t2 -> try Some (NCicUnification.unify status m s c t1 t2) with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None) - metasenv subst context (-1) (0,NCic.Irl 0) typ + metasenv subst context (-1) (0,C.Irl 0) typ with NCicMetaSubst.MetaSubstFailure _ | NCicMetaSubst.Uncertain _ -> @@ -80,9 +88,14 @@ let exp_implicit status ~localise metasenv subst context with_type t = metasenv,subst,Some typ in NCicMetaSubst.mk_meta metasenv [] ?with_type:expty `IsTerm,subst - | `Type -> NCicMetaSubst.mk_meta metasenv context ?with_type `IsType,subst - | `Term -> NCicMetaSubst.mk_meta metasenv context ?with_type `IsTerm,subst + | `Type -> + let with_type = match with_type with `XTSome t -> Some t | _ -> None in + NCicMetaSubst.mk_meta metasenv context ?with_type `IsType,subst + | `Term -> + let with_type = match with_type with `XTSome t -> Some t | _ -> None in + NCicMetaSubst.mk_meta metasenv context ?with_type `IsTerm,subst | `Tagged s -> + let with_type = match with_type with `XTSome t -> Some t | _ -> None in NCicMetaSubst.mk_meta ~attrs:[`Name s] metasenv context ?with_type `IsTerm,subst | `Vector -> @@ -172,7 +185,7 @@ let rec typeof (status:#NCicCoercion.status) let force_ty skip_lambda skip_appl metasenv subst context orig t infty expty = (*D*)inside 'F'; try let rc = match expty with - | Some expty -> + | `XTSome expty -> (match t with | C.Implicit _ -> assert false | C.Lambda _ when skip_lambda -> metasenv, subst, t, expty @@ -192,15 +205,30 @@ let rec typeof (status:#NCicCoercion.status) | NCicUnification.Uncertain _ | NCicUnification.UnificationFailure _ as exc -> try_coercions status ~localise - metasenv subst context t orig infty (`Type expty) exc) - | None -> metasenv, subst, t, infty + metasenv subst context t orig infty (`XTSome expty) exc) + | `XTNone -> metasenv, subst, t, infty + | `XTSort -> + (match t with + | C.Implicit _ -> assert false + | _ -> + pp (lazy ("forcing infty=any sort: "^ + (status#ppterm ~metasenv ~subst ~context infty) ^ " === any sort")); + force_to_sort status metasenv subst context t orig localise infty) + | `XTInd -> + (match t with + | C.Implicit _ -> assert false + | _ -> + pp (lazy ("forcing infty=any (co)inductive type: "^ + (status#ppterm ~metasenv ~subst ~context infty) ^ " === any (co)inductive type")); + force_to_inductive status metasenv subst context t orig localise infty) (*D*)in outside true; rc with exc -> outside false; raise exc in let rec typeof_aux metasenv subst context expty = fun t as orig -> (*D*)inside 'R'; try let rc = pp (lazy (status#ppterm ~metasenv ~subst ~context t ^ " ::exp:: " ^ - match expty with None -> "None" | Some e -> + match expty with `XTSort -> "Any sort" | `XTInd -> "Any (co)inductive type" + | `XTNone -> "None" | `XTSome e -> status#ppterm ~metasenv ~subst ~context e)); let metasenv, subst, t, infty = match t with @@ -224,10 +252,9 @@ let rec typeof (status:#NCicCoercion.status) let (metasenv,_,t,ty),subst = exp_implicit status ~localise metasenv subst context expty t infos in - if expty = None then - typeof_aux metasenv subst context None t - else - metasenv, subst, t, ty + (match expty with + | `XTSome _ -> metasenv, subst, t, ty + | _ -> typeof_aux metasenv subst context expty t) | C.Meta (n,l) as t -> let metasenv, ty = try @@ -239,12 +266,12 @@ let rec typeof (status:#NCicCoercion.status) | C.Const _ -> metasenv, subst, t, NCicTypeChecker.typeof status ~subst ~metasenv context t | C.Prod (name,(s as orig_s),(t as orig_t)) -> - let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in + let metasenv, subst, s, s1 = typeof_aux metasenv subst context `XTSort s in let metasenv, subst, s, s1 = force_to_sort status metasenv subst context s orig_s localise s1 in let context1 = (name,(C.Decl s))::context in - let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in + let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 `XTSort t in let metasenv, subst, t, s2 = force_to_sort status metasenv subst context1 t orig_t localise s2 in @@ -252,19 +279,21 @@ let rec typeof (status:#NCicCoercion.status) sort_of_prod status localise metasenv subst context orig_s orig_t (name,s) t (s1,s2) in - metasenv, subst, NCic.Prod(name,s,t), ty + metasenv, subst, C.Prod(name,s,t), ty | C.Lambda (n,(s as orig_s),t) as orig -> let exp_s, exp_ty_t, force_after = match expty with - | None -> None, None, false - | Some expty -> + | `XTSort + | `XTInd + | `XTNone -> `XTNone, `XTNone, false + | `XTSome expty -> match NCicReduction.whd status ~subst context expty with - | C.Prod (_,s,t) -> Some s, Some t, false - | _ -> None, None, true + | C.Prod (_,s,t) -> `XTSome s, `XTSome t, false + | _ -> `XTNone, `XTNone, true in let (metasenv,subst), s = match exp_s with - | Some exp_s -> + | `XTSome exp_s -> (* optimized case: implicit and implicitly typed meta * the optimization prevents proliferation of metas *) (match s with @@ -281,12 +310,14 @@ let rec typeof (status:#NCicCoercion.status) (try pp(lazy("Force source to: "^status#ppterm ~metasenv ~subst ~context exp_s)); - NCicUnification.unify ~test_eq_only:true status metasenv subst context s exp_s,s + NCicUnification.unify ~test_eq_only:true status metasenv subst context s exp_s, s with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf "Source type %s was expected to be %s" (status#ppterm ~metasenv ~subst ~context s) (status#ppterm ~metasenv ~subst ~context exp_s))) exc))) - | None -> + | `XTNone + | `XTSort + | `XTInd -> let metasenv, subst, s = check_type status ~localise metasenv subst context s in (metasenv, subst), s @@ -304,18 +335,18 @@ let rec typeof (status:#NCicCoercion.status) let metasenv, subst, ty = check_type status ~localise metasenv subst context ty in let metasenv, subst, t, _ = - typeof_aux metasenv subst context (Some ty) t in + typeof_aux metasenv subst context (`XTSome ty) t in let context1 = (n, C.Def (t,ty)) :: context in let metasenv, subst, expty1 = match expty with - | None -> metasenv, subst, None - | Some x -> + | `XTSome x -> let m, s, x = NCicUnification.delift_type_wrt_terms status metasenv subst context1 (NCicSubstitution.lift status 1 x) [NCicSubstitution.lift status 1 t] in - m, s, Some x + m, s, `XTSome x + | _ -> metasenv, subst, expty in let metasenv, subst, bo, bo_ty = typeof_aux metasenv subst context1 expty1 bo @@ -329,13 +360,13 @@ let rec typeof (status:#NCicCoercion.status) in let refine_appl metasenv subst args = let metasenv, subst, he, ty_he = - typeof_aux metasenv subst context None he in + typeof_aux metasenv subst context `XTNone he in let metasenv, subst, t, ty = eat_prods status ~localise force_ty metasenv subst context expty t orig_he he ty_he args in metasenv, subst, hbr t, ty in - if args = [C.Implicit `Vector] && expty <> None then + if args = [C.Implicit `Vector] && expty <> `XTNone then (* we try here to expand the vector a 0 implicits, but we use * the expected type *) try @@ -347,10 +378,10 @@ let rec typeof (status:#NCicCoercion.status) (* CSC: whd can be useful on he too... *) (match he with C.Const (Ref.Ref (uri1,Ref.Con _)) -> ( - match - HExtlib.map_option (NCicReduction.whd status ~subst context) expty - with - Some (C.Appl(C.Const(Ref.Ref (uri2,Ref.Ind _) as ref)::expargs)) + match expty with + | `XTSome expty -> ( + match NCicReduction.whd status ~subst context expty with + C.Appl (C.Const (Ref.Ref (uri2,Ref.Ind _) as ref)::expargs) when NUri.eq uri1 uri2 -> (try let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys status ref in @@ -375,7 +406,7 @@ let rec typeof (status:#NCicCoercion.status) (C.Implicit `Term :: allargs) allexpargs) | arg::args -> let metasenv,subst,arg,_ = - typeof_aux metasenv subst context None arg in + typeof_aux metasenv subst context `XTNone arg in let metasenv,subst = NCicUnification.unify status metasenv subst context arg exparg @@ -387,7 +418,10 @@ let rec typeof (status:#NCicCoercion.status) | Sys.Break as exn -> raise exn | _ -> refine_appl metasenv subst args (* to try coercions *)) - | _ -> refine_appl metasenv subst args) + | _ -> refine_appl metasenv subst args) + | `XTNone + | `XTSort + | `XTInd -> refine_appl metasenv subst args) | _ -> refine_appl metasenv subst args) | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2")) | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r, @@ -399,20 +433,20 @@ let rec typeof (status:#NCicCoercion.status) NCicMetaSubst.saturate status metasenv subst context arity 0 in let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in let metasenv, subst, term, _ = - typeof_aux metasenv subst context (Some ind) term in + typeof_aux metasenv subst context (`XTSome ind) term in let parameters, arguments = HExtlib.split_nth leftno args in let outtype = match outtype with | C.Implicit _ as ot -> let rec aux = function - | [] -> NCic.Lambda ("_",NCic.Implicit `Type,ot) - | _::tl -> NCic.Lambda ("_",NCic.Implicit `Type,aux tl) + | [] -> C.Lambda ("_",C.Implicit `Type,ot) + | _::tl -> C.Lambda ("_",C.Implicit `Type,aux tl) in aux arguments | _ -> outtype in let metasenv, subst, outtype, outsort = - typeof_aux metasenv subst context None outtype in + typeof_aux metasenv subst context `XTNone outtype in (* this cannot be `XTSort *) (* next lines are to do a subst-expansion of the outtype, so that when it becomes a beta-abstraction, the beta-redex is @@ -429,7 +463,7 @@ let rec typeof (status:#NCicCoercion.status) if parameters = [] then C.Const r else C.Appl ((C.Const r)::parameters) in let metasenv, subst, ind, ind_ty = - typeof_aux metasenv subst context None ind in + typeof_aux metasenv subst context `XTNone ind in (* FG: this cannot be `XTSort *) let metasenv, subst = check_allowed_sort_elimination status localise r orig_term metasenv subst context ind ind_ty outsort @@ -455,7 +489,7 @@ let rec typeof (status:#NCicCoercion.status) else C.Appl (C.Const cons::parameters) in let metasenv, subst, cons, ty_cons = - typeof_aux metasenv subst context None cons in + typeof_aux metasenv subst context `XTNone cons in (* FG: this cannot be `XTInd *) let ty_branch = NCicTypeChecker.type_of_branch status ~subst context leftno outtype cons ty_cons in @@ -463,7 +497,7 @@ let rec typeof (status:#NCicCoercion.status) status#ppterm ~metasenv ~subst ~context p ^ " ::inf:: " ^ status#ppterm ~metasenv ~subst ~context ty_branch )); let metasenv, subst, p, _ = - typeof_aux metasenv subst context (Some ty_branch) p in + typeof_aux metasenv subst context (`XTSome ty_branch) p in j-1, metasenv, subst, p :: branches) pl (List.length pl, metasenv, subst, []) in @@ -481,7 +515,7 @@ let rec typeof (status:#NCicCoercion.status) and check_type status ~localise metasenv subst context (ty as orig_ty) = let metasenv, subst, ty, sort = - typeof status ~localise metasenv subst context ty None + typeof status ~localise metasenv subst context ty `XTSort in let metasenv, subst, ty, _ = force_to_sort status metasenv subst context ty orig_ty localise sort @@ -494,25 +528,26 @@ and try_coercions status let cs_subst = NCicSubstitution.subst status ~avoid_beta_redexes:true in try (match expty with - `Type expty -> + `XTSome expty -> pp (lazy "WWW: trying coercions -- preliminary unification"); let metasenv, subst = NCicUnification.unify status metasenv subst context infty expty in metasenv, subst, t, expty - | _ -> raise (Failure "Special case Prod or Sort")) + | _ -> raise (Failure "Special case XTProd, XTSort or XTInd")) with | exn -> (* we try with a coercion *) let rec first exc = function | [] -> - pp (lazy "WWW: no more coercions!"); + pp (lazy "WWW: no more coercions!"); raise (wrap_exc (lazy let expty = match expty with - `Type expty -> status#ppterm ~metasenv ~subst ~context expty - | `Sort -> "[[sort]]" - | `Prod -> "[[prod]]" in - (localise orig_t, Printf.sprintf + `XTSome expty -> status#ppterm ~metasenv ~subst ~context expty + | `XTSort -> "[[sort]]" + | `XTProd -> "[[prod]]" + | `XTInd -> "[[ind]]" in + (localise orig_t, Printf.sprintf "The term\n%s\nhas type\n%s\nbut is here used with type\n%s" (status#ppterm ~metasenv ~subst ~context t) (status#ppterm ~metasenv ~subst ~context infty) @@ -530,7 +565,7 @@ and try_coercions status let metasenv, subst = NCicUnification.unify status metasenv subst context t meta in match expty with - `Type expty -> + `XTSome expty -> pp (lazy ( "UNIFICATION in CTX:\n"^ status#ppcontext ~metasenv ~subst context ^ "\nMENV: " ^ @@ -542,13 +577,17 @@ and try_coercions status NCicUnification.unify status metasenv subst context newtype expty in metasenv, subst, newterm, newtype - | `Sort -> + | `XTSort -> + (match NCicReduction.whd status ~subst context newtype with + C.Sort _ -> metasenv,subst,newterm,newtype + | _ -> first exc tl) + | `XTInd -> (match NCicReduction.whd status ~subst context newtype with - NCic.Sort _ -> metasenv,subst,newterm,newtype + C.Const (Ref.Ref (_, Ref.Ind _)) -> metasenv,subst,newterm,newtype | _ -> first exc tl) - | `Prod -> + | `XTProd -> (match NCicReduction.whd status ~subst context newtype with - NCic.Prod _ -> metasenv,subst,newterm,newtype + C.Prod _ -> metasenv,subst,newterm,newtype | _ -> first exc tl) with | NCicUnification.UnificationFailure _ -> first exc tl @@ -558,8 +597,8 @@ and try_coercions status try pp (lazy "WWW: trying coercions -- inner check"); match infty, expty, t with - (* `Sort|`Prod + Match not implemented *) - | _,`Type expty, NCic.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) -> + (* `XTSort|`XTProd|`XTInd + Match not implemented *) + | _,`XTSome expty, C.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) -> (*{{{*) pp (lazy "CASE"); (* {{{ helper functions *) let get_cl_and_left_p refit outty = @@ -571,8 +610,8 @@ and try_coercions status let count_pis t = let rec aux ctx t = match NCicReduction.whd status ~subst ~delta:max_int ctx t with - | NCic.Prod (name,src,tgt) -> - let ctx = (name, (NCic.Decl src)) :: ctx in + | C.Prod (name,src,tgt) -> + let ctx = (name, (C.Decl src)) :: ctx in 1 + aux ctx tgt | _ -> 0 in @@ -581,17 +620,17 @@ and try_coercions status let rec skip_lambda_delifting t n = match t,n with | _,0 -> t - | NCic.Lambda (_,_,t),n -> + | C.Lambda (_,_,t),n -> pp (lazy ("WWW: failing term? "^ status#ppterm ~subst:[] ~metasenv:[] ~context:[] t)); skip_lambda_delifting (* substitute dangling indices with a dummy *) - (NCicSubstitution.subst status (NCic.Sort NCic.Prop) t) (n - 1) + (NCicSubstitution.subst status (C.Sort C.Prop) t) (n - 1) | _ -> assert false in let get_l_r_p n = function - | NCic.Lambda (_,NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))),_) -> [],[] - | NCic.Lambda (_,NCic.Appl - (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))) :: args),_) -> + | C.Lambda (_,C.Const (Ref.Ref (_,Ref.Ind (_,_,_))),_) -> [],[] + | C.Lambda (_,C.Appl + (C.Const (Ref.Ref (_,Ref.Ind (_,_,_))) :: args),_) -> HExtlib.split_nth n args | _ -> assert false in @@ -604,7 +643,7 @@ and try_coercions status (fun ty -> List.fold_left (fun t p -> match t with - | NCic.Prod (_,_,t) -> + | C.Prod (_,_,t) -> cs_subst p t | _-> assert false) ty left_p) @@ -619,7 +658,7 @@ and try_coercions status match t,n with | _,0 -> let rec mkr n = function - | [] -> [] | _::tl -> NCic.Rel n :: mkr (n+1) tl + | [] -> [] | _::tl -> C.Rel n :: mkr (n+1) tl in pp (lazy ("input replace: " ^ status#ppterm ~context:ctx ~metasenv:[] ~subst:[] bo)); let bo = @@ -627,37 +666,37 @@ and try_coercions status ~equality:(fun _ -> NCicRefineUtil.alpha_equivalence status) ~context:ctx ~what:(matched::right_p) - ~with_what:(NCic.Rel 1::List.rev (mkr 2 right_p)) + ~with_what:(C.Rel 1::List.rev (mkr 2 right_p)) ~where:bo in pp (lazy ("output replace: " ^ status#ppterm ~context:ctx ~metasenv:[] ~subst:[] bo)); bo - | NCic.Lambda (name, src, tgt),_ -> - NCic.Lambda (name, src, + | C.Lambda (name, src, tgt),_ -> + C.Lambda (name, src, keep_lambdas_and_put_expty - ((name, NCic.Decl src)::ctx) tgt (NCicSubstitution.lift status 1 bo) + ((name, C.Decl src)::ctx) tgt (NCicSubstitution.lift status 1 bo) (List.map (NCicSubstitution.lift status 1) right_p) (NCicSubstitution.lift status 1 matched) (n-1)) | _ -> assert false in - (*let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in - let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*) - let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.ind(1,0,2)")) in - let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.con(0,1,2)")) in + (*let eq = C.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in + let eq_refl = C.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*) + let eq = C.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.ind(1,0,2)")) in + let eq_refl = C.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.con(0,1,2)")) in let add_params metasenv subst context cty outty mty m i = let rec aux context outty par j mty m = function - | NCic.Prod (name, src, tgt) -> + | C.Prod (name, src, tgt) -> let t,k = aux - ((name, NCic.Decl src) :: context) - (NCicSubstitution.lift status 1 outty) (NCic.Rel j::par) (j+1) + ((name, C.Decl src) :: context) + (NCicSubstitution.lift status 1 outty) (C.Rel j::par) (j+1) (NCicSubstitution.lift status 1 mty) (NCicSubstitution.lift status 1 m) tgt in - NCic.Prod (name, src, t), k - | NCic.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r) -> + C.Prod (name, src, t), k + | C.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r) -> let k = - let k = NCic.Const(Ref.mk_constructor i r) in + let k = C.Const(Ref.mk_constructor i r) in NCicUntrusted.mk_appl k par in (* the type has no parameters, so kty = mty @@ -665,30 +704,30 @@ and try_coercions status try NCicTypechecker.typeof ~subst ~metasenv context k with NCicTypeChecker.TypeCheckerFailure _ -> assert false in *) - NCic.Prod ("p", - NCic.Appl [eq; mty; m; mty; k], + C.Prod ("p", + C.Appl [eq; mty; m; mty; k], (NCicSubstitution.lift status 1 (NCicReduction.head_beta_reduce status ~delta:max_int (NCicUntrusted.mk_appl outty [k])))),[mty,m,mty,k] - | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r)::pl) -> + | C.Appl (C.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r)::pl) -> let left_p,right_p = HExtlib.split_nth leftno pl in let has_rights = right_p <> [] in let k = - let k = NCic.Const(Ref.mk_constructor i r) in + let k = C.Const(Ref.mk_constructor i r) in NCicUntrusted.mk_appl k (left_p@par) in let right_p = try match NCicTypeChecker.typeof status ~subst ~metasenv context k with - | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) -> + | C.Appl (C.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) -> snd (HExtlib.split_nth leftno args) | _ -> assert false with NCicTypeChecker.TypeCheckerFailure _-> assert false in let orig_right_p = match mty with - | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) -> + | C.Appl (C.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) -> snd (HExtlib.split_nth leftno args) | _ -> assert false in @@ -702,7 +741,7 @@ and try_coercions status try NCicTypeChecker.typeof status ~subst ~metasenv context y with NCicTypeChecker.TypeCheckerFailure _ -> assert false in - NCic.Prod ("_", NCic.Appl [eq;xty;x;yty;y], + C.Prod ("_", C.Appl [eq;xty;x;yty;y], NCicSubstitution.lift status 1 tacc), (xty,x,yty,y)::pacc) (orig_right_p @ [m]) (right_p @ [k]) (NCicReduction.head_beta_reduce status ~delta:max_int @@ -710,13 +749,13 @@ and try_coercions status (* if has_rights then NCicReduction.head_beta_reduce status ~delta:max_int - (NCic.Appl (outty ::right_p @ [k])),k + (C.Appl (outty ::right_p @ [k])),k else - NCic.Prod ("p", - NCic.Appl [eq; mty; m; k], + C.Prod ("p", + C.Appl [eq; mty; m; k], (NCicSubstitution.lift status 1 (NCicReduction.head_beta_reduce status ~delta:max_int - (NCic.Appl (outty ::right_p @ [k]))))),k*) + (C.Appl (outty ::right_p @ [k]))))),k*) | _ -> assert false in aux context outty [] 1 mty m cty @@ -725,32 +764,32 @@ and try_coercions status (* k lives in the right context *) (* if rno <> 0 then pbo else *) let rec aux = function - | NCic.Lambda (name,src,bo), NCic.Prod (_,_,ty) -> - NCic.Lambda (name,src, + | C.Lambda (name,src,bo), C.Prod (_,_,ty) -> + C.Lambda (name,src, (aux (bo,ty))) | t,_ -> snd (List.fold_right - (fun (xty,x,yty,y) (n,acc) -> n+1, NCic.Lambda ("p" ^ string_of_int n, - NCic.Appl [eq; xty; x; yty; y], + (fun (xty,x,yty,y) (n,acc) -> n+1, C.Lambda ("p" ^ string_of_int n, + C.Appl [eq; xty; x; yty; y], NCicSubstitution.lift status 1 acc)) eqs (1,t)) - (*NCic.Lambda ("p", - NCic.Appl [eq; mty; m; k],NCicSubstitution.lift status 1 t)*) + (*C.Lambda ("p", + C.Appl [eq; mty; m; k],NCicSubstitution.lift status 1 t)*) in aux (pbo,cty) in let add_pi_for_refl_m context new_outty mty m lno rno = (*if rno <> 0 then new_outty else*) let rec aux context mty m = function - | NCic.Lambda (name, src, tgt) -> - let context = (name, NCic.Decl src)::context in - NCic.Lambda (name, src, aux context (NCicSubstitution.lift status 1 mty) (NCicSubstitution.lift status 1 m) tgt) + | C.Lambda (name, src, tgt) -> + let context = (name, C.Decl src)::context in + C.Lambda (name, src, aux context (NCicSubstitution.lift status 1 mty) (NCicSubstitution.lift status 1 m) tgt) | t -> let lhs = match mty with - | NCic.Appl (_::params) -> (snd (HExtlib.split_nth lno params))@[m] + | C.Appl (_::params) -> (snd (HExtlib.split_nth lno params))@[m] | _ -> [m] in let rhs = - List.map (fun x -> NCic.Rel x) + List.map (fun x -> C.Rel x) (List.rev (HExtlib.list_seq 1 (rno+2))) in List.fold_right2 (fun x y acc -> @@ -762,12 +801,12 @@ and try_coercions status try NCicTypeChecker.typeof status ~subst ~metasenv context y with NCicTypeChecker.TypeCheckerFailure _ -> assert false in - NCic.Prod - ("_", NCic.Appl [eq;xty;x;yty;y], + C.Prod + ("_", C.Appl [eq;xty;x;yty;y], (NCicSubstitution.lift status 1 acc))) lhs rhs t - (* NCic.Prod - ("_", NCic.Appl [eq;mty;m;NCic.Rel 1], + (* C.Prod + ("_", C.Appl [eq;mty;m;C.Rel 1], NCicSubstitution.lift status 1 t)*) in aux context mty m new_outty @@ -782,8 +821,8 @@ and try_coercions status match NCicTypeChecker.typeof status ~subst ~metasenv context m with - | (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))) | NCic.Meta _) as mty -> [], mty - | NCic.Appl ((NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))|NCic.Meta _)::args) as mty -> + | (C.Const (Ref.Ref (_,Ref.Ind (_,_,_))) | C.Meta _) as mty -> [], mty + | C.Appl ((C.Const (Ref.Ref (_,Ref.Ind (_,_,_)))|C.Meta _)::args) as mty -> snd (HExtlib.split_nth leftno args), mty | _ -> assert false with NCicTypeChecker.TypeCheckerFailure _ -> @@ -820,7 +859,7 @@ and try_coercions status ~context ~metasenv ~subst pbo)); let metasenv, subst, pbo, _ = try_coercions status ~localise menv s context pbo - orig_t (*??*) infty_pbo (`Type expty_pbo) exc + orig_t (*??*) infty_pbo (`XTSome expty_pbo) exc in pp (lazy ("CASE: pbo2: " ^ status#ppterm @@ -840,61 +879,61 @@ and try_coercions status List.map (fun t -> NCicTypeChecker.typeof status ~subst ~metasenv context t) right_p in let eqs = - List.map2 (fun x y -> NCic.Appl[eq_refl;x;y]) (right_tys@[mty]) + List.map2 (fun x y -> C.Appl[eq_refl;x;y]) (right_tys@[mty]) (right_p@[m]) in - let t = NCic.Appl (NCic.Match(r,new_outty,m,pl) :: eqs) + let t = C.Appl (C.Match(r,new_outty,m,pl) :: eqs) in metasenv, subst, t, expty (*}}}*) - | _,`Type expty,NCic.LetIn(name,ty,t,bo) -> + | _,`XTSome expty,C.LetIn(name,ty,t,bo) -> pp (lazy "LETIN"); let name' = mk_fresh_name context name in - let context_bo = (name', NCic.Def (t,ty)) :: context in + let context_bo = (name', C.Def (t,ty)) :: context in let metasenv, subst, bo2, _ = try_coercions status ~localise metasenv subst context_bo bo orig_t (NCicSubstitution.lift status 1 infty) - (`Type (NCicSubstitution.lift status 1 expty)) exc + (`XTSome (NCicSubstitution.lift status 1 expty)) exc in - let coerced = NCic.LetIn (name',ty,t,bo2) in + let coerced = C.LetIn (name',ty,t,bo2) in pp (lazy ("LETIN: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced)); metasenv, subst, coerced, expty - | NCic.Prod (nameprod, src, ty),`Type (NCic.Prod (_, src2, ty2) as expty), _ -> + | C.Prod (nameprod, src, ty),`XTSome (C.Prod (_, src2, ty2) as expty), _ -> (*{{{*) pp (lazy "LAM"); pp (lazy ("LAM: t = " ^ status#ppterm ~metasenv ~subst ~context t)); - let namename = match t with NCic.Lambda (n,_,_) -> n | _ -> nameprod in + let namename = match t with C.Lambda (n,_,_) -> n | _ -> nameprod in let name_con = mk_fresh_name context namename in - let context_src2 = ((name_con, NCic.Decl src2) :: context) in + let context_src2 = ((name_con, C.Decl src2) :: context) in (* contravariant part: the argument of f:src->ty *) let metasenv, subst, rel1, _ = try_coercions status ~localise metasenv subst context_src2 - (NCic.Rel 1) orig_t (NCicSubstitution.lift status 1 src2) - (`Type (NCicSubstitution.lift status 1 src)) exc + (C.Rel 1) orig_t (NCicSubstitution.lift status 1 src2) + (`XTSome (NCicSubstitution.lift status 1 src)) exc in (* covariant part: the result of f(c x); x:src2; (c x):src *) let name_t, bo = match t with - | NCic.Lambda (n,_,bo) -> n, cs_subst rel1 (NCicSubstitution.lift_from status 2 1 bo) + | C.Lambda (n,_,bo) -> n, cs_subst rel1 (NCicSubstitution.lift_from status 2 1 bo) | _ -> name_con, NCicUntrusted.mk_appl (NCicSubstitution.lift status 1 t) [rel1] in (* we fix the possible dependency problem in the source ty *) let ty = cs_subst rel1 (NCicSubstitution.lift_from status 2 1 ty) in let metasenv, subst, bo, _ = try_coercions status ~localise metasenv subst context_src2 - bo orig_t ty (`Type ty2) exc + bo orig_t ty (`XTSome ty2) exc in - let coerced = NCic.Lambda (name_t,src2, bo) in + let coerced = C.Lambda (name_t,src2, bo) in pp (lazy ("LAM: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced)); metasenv, subst, coerced, expty (*}}}*) | _ -> raise exc with exc2 -> let expty = match expty with - `Type expty -> expty - | `Sort -> - NCic.Sort (NCic.Type + `XTSome expty -> expty + | `XTSort -> + C.Sort (C.Type (match NCicEnvironment.get_universes () with | x::_ -> x | _ -> assert false)) - | `Prod -> NCic.Prod ("_",NCic.Implicit `Type,NCic.Implicit `Type) + | `XTProd -> C.Prod ("_",C.Implicit `Type,C.Implicit `Type) in pp(lazy("try_coercion " ^ status#ppterm ~metasenv ~subst ~context infty ^ " |---> " ^ @@ -922,7 +961,32 @@ and force_to_sort status metasenv subst context t orig_t localise ty = RefineFailure msg in try_coercions status ~localise metasenv subst context - t orig_t ty `Sort exn + t orig_t ty `XTSort exn + +and force_to_inductive status metasenv subst context t orig_t localise ty = + try + let metasenv, subst, ty = + NCicUnification.indfy status (Failure "indfy") metasenv subst context ty in + metasenv, subst, t, ty + with + Failure _ -> + let msg = + (lazy (localise orig_t, + "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^ + " is not a (co)inductive type: " ^ status#ppterm ~metasenv ~subst ~context ty)) in + let ty = NCicReduction.whd status ~subst context ty in +(* prerr_endline ("#### " ^ status#ppterm ~metasenv ~subst ~context ty); *) + let exn = + if NCicUnification.could_reduce status ~subst context ty then + Uncertain msg + else + RefineFailure msg + in + raise exn +(* FG: this should be as follows but the case `XTInd is not imp;emented yet + try_coercions status ~localise metasenv subst context + t orig_t ty `XTInd exn +*) and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s) t (t1, t2) @@ -970,15 +1034,16 @@ and eat_prods status ~localise force_ty metasenv subst context expty orig_t orig pp(lazy("FORCE FINAL APPL: " ^ status#ppterm ~metasenv ~subst ~context res ^ " of type " ^ status#ppterm ~metasenv ~subst ~context ty_he - ^ " to type " ^ match expty with None -> "None" | Some x -> + ^ " to type " ^ match expty with `XTSort -> "Any sort" | `XTInd -> "Any (co)inductive type" + | `XTNone -> "None" | `XTSome x -> status#ppterm ~metasenv ~subst ~context x)); (* whatever the term is, we force the type. in case of ((Lambda..) ?...) * the application may also be a lambda! *) force_ty false false metasenv subst context orig_t res ty_he expty - | NCic.Implicit `Vector::tl -> + | C.Implicit `Vector::tl -> let has_some_more_pis x = match NCicReduction.whd status ~subst context x with - | NCic.Meta _ | NCic.Appl (NCic.Meta _::_) -> false + | C.Meta _ | C.Appl (C.Meta _::_) -> false | _ -> true in (try @@ -988,7 +1053,7 @@ and eat_prods status ~localise force_ty metasenv subst context expty orig_t orig | RefineFailure _ as exc when has_some_more_pis ty_he -> (try aux metasenv subst args_so_far he ty_he - (NCic.Implicit `Term :: NCic.Implicit `Vector :: tl) + (C.Implicit `Term :: C.Implicit `Vector :: tl) with Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc)) | RefineFailure msg when not (has_some_more_pis ty_he) -> @@ -998,13 +1063,13 @@ and eat_prods status ~localise force_ty metasenv subst context expty orig_t orig match NCicReduction.whd status ~subst context ty_he with | C.Prod (_,s,t) -> let metasenv, subst, arg, _ = - typeof status ~localise metasenv subst context arg (Some s) in + typeof status ~localise metasenv subst context arg (`XTSome s) in let t = NCicSubstitution.subst status ~avoid_beta_redexes:true arg t in aux metasenv subst (arg :: args_so_far) he t tl | C.Meta _ | C.Appl (C.Meta _ :: _) as t -> let metasenv, subst, arg, ty_arg = - typeof status ~localise metasenv subst context arg None in + typeof status ~localise metasenv subst context arg `XTNone in let name = guess_name status subst context ty_arg in let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv @@ -1013,7 +1078,7 @@ and eat_prods status ~localise force_ty metasenv subst context expty orig_t orig let flex_prod = C.Prod (name, ty_arg, meta) in (* next line grants that ty_args is a type *) let metasenv,subst, flex_prod, _ = - typeof status ~localise metasenv subst context flex_prod None in + typeof status ~localise metasenv subst context flex_prod `XTSort in (* pp (lazy ( "UNIFICATION in CTX:\n"^ status#ppcontext ~metasenv ~subst context @@ -1049,7 +1114,7 @@ and eat_prods status ~localise force_ty metasenv subst context expty orig_t orig let metasenv, subst, newhead, newheadty = try_coercions status ~localise metasenv subst context (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty - `Prod + `XTProd (RefineFailure (lazy (localise orig_he, Printf.sprintf ("The term %s is here applied to %d arguments but expects " ^^ "only %d arguments") (status#ppterm ~metasenv ~subst ~context he) @@ -1104,7 +1169,7 @@ let undebruijnate status inductive ref t rev_fl = (HExtlib.list_mapi (fun (_,_,rno,_,_,_) i -> let i = len - i - 1 in - NCic.Const + C.Const (if inductive then NReference.mk_fix i rno ref else NReference.mk_cofix i ref)) rev_fl) @@ -1123,7 +1188,7 @@ let typeof_obj match bo with | Some bo -> let metasenv, subst, bo, ty = - typeof status ~localise metasenv subst [] bo (Some ty) in + typeof status ~localise metasenv subst [] bo (`XTSome ty) in let height = (* XXX recalculate *) height in metasenv, subst, Some bo, ty, height | None -> metasenv, subst, None, ty, 0 @@ -1147,7 +1212,7 @@ let typeof_obj List.fold_left (fun (metasenv,subst,fl) (relevance,name,k,ty,dbo,localise) -> let metasenv, subst, dbo, ty = - typeof status ~localise metasenv subst types dbo (Some ty) + typeof status ~localise metasenv subst types dbo (`XTSome ty) in metasenv, subst, (relevance,name,k,ty,dbo)::fl) (metasenv, subst, []) rev_fl @@ -1174,7 +1239,7 @@ let typeof_obj (fun (metasenv,subst,res,ctx) (relevance,n,ty,cl) -> let metasenv, subst, ty = check_type status ~localise metasenv subst [] ty in - metasenv,subst,(relevance,n,ty,cl)::res,(n,NCic.Decl ty)::ctx + metasenv,subst,(relevance,n,ty,cl)::res,(n,C.Decl ty)::ctx ) (metasenv,subst,[],[]) itl in let metasenv,subst,itl,_ = List.fold_left @@ -1238,9 +1303,9 @@ let typeof_obj with Invalid_argument "List.fold_left2" -> assert false in let metasenv, subst = let rec aux context (metasenv,subst) = function - | NCic.Meta _ -> metasenv, subst - | NCic.Implicit _ -> metasenv, subst - | NCic.Appl (NCic.Rel i :: args) as t + | C.Meta _ -> metasenv, subst + | C.Implicit _ -> metasenv, subst + | C.Appl (C.Rel i :: args) as t when i > List.length context - len -> let lefts, _ = HExtlib.split_nth leftno args in let ctxlen = List.length context in @@ -1249,7 +1314,7 @@ let typeof_obj (fun ((metasenv, subst),l) arg -> NCicUnification.unify status ~test_eq_only:true metasenv subst context arg - (NCic.Rel (ctxlen - len - l)), l+1 + (C.Rel (ctxlen - len - l)), l+1 ) ((metasenv, subst), 0) lefts in @@ -1297,9 +1362,9 @@ let typeof_obj NCicSubstitution.psubst status (fun i -> if i <= leftno then - NCic.Rel i + C.Rel i else - NCic.Const (NReference.reference_of_spec uri + C.Const (NReference.reference_of_spec uri (NReference.Ind (ind,relsno - i,leftno)))) (HExtlib.list_seq 1 (relsno+1)) te in @@ -1307,8 +1372,8 @@ let typeof_obj List.fold_right (fun (name,decl) te -> match decl with - NCic.Decl ty -> NCic.Prod (name,ty,te) - | NCic.Def (bo,ty) -> NCic.LetIn (name,ty,bo,te) + C.Decl ty -> C.Prod (name,ty,te) + | C.Def (bo,ty) -> C.LetIn (name,ty,bo,te) ) sx_context_te_rev te in metasenv,subst,(k_relev,n,te)::res diff --git a/matita/components/ng_refiner/nCicRefiner.mli b/matita/components/ng_refiner/nCicRefiner.mli index 6ec18e365..7da885e7e 100644 --- a/matita/components/ng_refiner/nCicRefiner.mli +++ b/matita/components/ng_refiner/nCicRefiner.mli @@ -15,11 +15,16 @@ exception RefineFailure of (Stdpp.location * string) Lazy.t;; exception Uncertain of (Stdpp.location * string) Lazy.t;; exception AssertFailure of string Lazy.t;; +type 'a expected_type = [ `XTNone (* unknown *) + | `XTSome of 'a (* the given term *) + | `XTSort (* any sort *) + | `XTInd (* any (co)inductive type *) + ] val typeof : #NCicCoercion.status -> ?localise:(NCic.term -> Stdpp.location) -> NCic.metasenv -> NCic.substitution -> NCic.context -> - NCic.term -> NCic.term option -> (* term, expected type *) + NCic.term -> NCic.term expected_type -> (* term, expected type *) NCic.metasenv * NCic.substitution * NCic.term * NCic.term (* menv, subst,refined term, type *) diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml index 325ced5c4..7d8a45d0e 100644 --- a/matita/components/ng_refiner/nCicUnification.ml +++ b/matita/components/ng_refiner/nCicUnification.ml @@ -233,6 +233,31 @@ let rec sortfy status exc metasenv subst context t = in metasenv,subst,t +let indfy status exc metasenv subst context t = + let t = NCicReduction.whd status ~subst context t in + let metasenv,subst = + match t with + | NCic.Const (Ref.Ref (_, Ref.Ind _)) + | NCic.Appl (NCic.Const (Ref.Ref (_, Ref.Ind _))::_) -> metasenv, subst +(* + | NCic.Meta (n,_) -> + let attrs, context, ty = NCicUtils.lookup_meta n metasenv in + let kind = NCicUntrusted.kind_of_meta attrs in + if kind = `IsSort then + metasenv,subst + else + (match ty with + | NCic.Implicit (`Typeof _) -> + metasenv_to_subst n (`IsSort,[],ty) metasenv subst + | ty -> + let metasenv,subst,ty = sortfy status exc metasenv subst context ty in + metasenv_to_subst n (`IsSort,[],ty) metasenv subst) +*) + | NCic.Implicit _ -> assert false + | _ -> raise exc + in + metasenv,subst,t + let tipify status exc metasenv subst context t ty = let is_type attrs = match NCicUntrusted.kind_of_meta attrs with diff --git a/matita/components/ng_refiner/nCicUnification.mli b/matita/components/ng_refiner/nCicUnification.mli index c7d44e8ab..1cba19183 100644 --- a/matita/components/ng_refiner/nCicUnification.mli +++ b/matita/components/ng_refiner/nCicUnification.mli @@ -46,4 +46,8 @@ val sortfy :# NCic.status -> exn -> NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.metasenv * NCic.substitution * NCic.term +val indfy :# + NCic.status -> exn -> NCic.metasenv -> NCic.substitution -> NCic.context -> + NCic.term -> NCic.metasenv * NCic.substitution * NCic.term + val debug : bool ref diff --git a/matita/components/ng_tactics/nCicElim.ml b/matita/components/ng_tactics/nCicElim.ml index 95b8f783d..5a264c403 100644 --- a/matita/components/ng_tactics/nCicElim.ml +++ b/matita/components/ng_tactics/nCicElim.ml @@ -166,9 +166,9 @@ let mk_elim status uri leftno it (outsort,suffix) pragma = (function x::_ -> x | _ -> assert false) 80 (NotationPres.mpres_of_box boxml))); *) + let attrs = `Generated, `Definition, pragma in NotationPt.Theorem - (`Definition,srec_name, - NotationPt.Implicit `JustOne,Some res,pragma) + (srec_name, NotationPt.Implicit `JustOne, Some res, attrs) ;; let ast_of_sort s = @@ -308,8 +308,9 @@ let mk_projection status leftno tyname consname consty (projname,_,_) i = (function x::_ -> x | _ -> assert false) 80 (NotationPres.render (fun _ -> None) (TermContentPres.pp_ast res)));*) + let attrs = `Generated, `Definition, `Projection in NotationPt.Theorem - (`Definition,projname,NotationPt.Implicit `JustOne,Some res,`Projection) + (projname, NotationPt.Implicit `JustOne, Some res, attrs) ;; let mk_projections status (_,_,_,_,obj) = diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml index fdee9e127..f03baa656 100644 --- a/matita/components/ng_tactics/nDestructTac.ml +++ b/matita/components/ng_tactics/nDestructTac.ml @@ -321,11 +321,11 @@ let mk_discriminator ~use_jmeq ?(force=false) name it leftno status baseuri = (* PHASE 2: create the object for the proof of the principle: we'll name it * "theorem" *) let status, theorem = - GrafiteDisambiguate.disambiguate_nobj status ~baseuri + let attrs = `Generated, `Theorem, `DiscriminationPrinciple in + GrafiteDisambiguate.disambiguate_nobj status ~baseuri (baseuri ^ name ^ ".def",0, NotationPt.Theorem - (`Theorem,name,principle, - Some (NotationPt.Implicit (`Tagged "inv")),`DiscriminationPrinciple)) + (name, principle, Some (NotationPt.Implicit (`Tagged "inv")), attrs)) in let uri,height,nmenv,nsubst,nobj = theorem in let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in diff --git a/matita/components/ng_tactics/nInversion.ml b/matita/components/ng_tactics/nInversion.ml index 12e14be46..8267fd877 100644 --- a/matita/components/ng_tactics/nInversion.ml +++ b/matita/components/ng_tactics/nInversion.ml @@ -150,11 +150,11 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st mk_prods hyplist (mk_appl (mk_id "P"::id_rs)))))) in let status, theorem = - GrafiteDisambiguate.disambiguate_nobj status ~baseuri + let attrs = `Generated, `Theorem, `InversionPrinciple in + GrafiteDisambiguate.disambiguate_nobj status ~baseuri (baseuri ^ name ^ ".def",0, NotationPt.Theorem - (`Theorem,name,theorem, - Some (NotationPt.Implicit (`Tagged "inv")),`InversionPrinciple)) + (name,theorem, Some (NotationPt.Implicit (`Tagged "inv")), attrs)) in let uri,height,nmenv,nsubst,nobj = theorem in let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml index 271f9a040..2fa02c307 100644 --- a/matita/components/ng_tactics/nTacStatus.ml +++ b/matita/components/ng_tactics/nTacStatus.ml @@ -187,9 +187,11 @@ let term_of_cic_term s t c = let disambiguate status context t ty = let status, expty = match ty with - | None -> status, None - | Some ty -> - let status, (_,x) = relocate status context ty in status, Some x + | `XTSome ty -> + let status, (_,x) = relocate status context ty in status, `XTSome x + | `XTNone -> status, `XTNone + | `XTSort -> status, `XTSort + | `XTInd -> status, `XTInd in let uri,height,metasenv,subst,obj = status#obj in let metasenv, subst, status, t = @@ -254,9 +256,11 @@ let refine status ctx term expty = let status, (_,term) = relocate status ctx term in let status, expty = match expty with - None -> status, None - | Some e -> - let status, (_, e) = relocate status ctx e in status, Some e + | `XTSome e -> + let status, (_, e) = relocate status ctx e in status, `XTSome e + | `XTNone -> status, `XTNone + | `XTSort -> status, `XTSort + | `XTInd -> status, `XTInd in let name,height,metasenv,subst,obj = status#obj in let metasenv,subst,t,ty = @@ -289,7 +293,7 @@ let instantiate status ?refine:(dorefine=true) i t = let _,_,metasenv,_,_ = status#obj in let gname, context, gty = List.assoc i metasenv in if dorefine then - let status, (_,t), (_,ty) = refine status context t (Some (context,gty)) in + let status, (_,t), (_,ty) = refine status context t (`XTSome (context,gty)) in to_subst status i (gname,context,t,ty) else let status,(_,ty) = typeof status context t in @@ -300,7 +304,7 @@ let instantiate_with_ast status i t = let _,_,metasenv,_,_ = status#obj in let gname, context, gty = List.assoc i metasenv in let ggty = mk_cic_term context gty in - let status, (_,t) = disambiguate status context t (Some ggty) in + let status, (_,t) = disambiguate status context t (`XTSome ggty) in to_subst status i (gname,context,t,gty) ;; @@ -424,7 +428,7 @@ let select_term | NCic.Implicit `Hole, t -> (match wanted with | Some wanted -> - let status', wanted = disambiguate status ctx wanted None in + let status', wanted = disambiguate status ctx wanted `XTNone in pp(lazy("wanted: "^ppterm status' wanted)); let (status',found), t' = match_term status' ctx wanted t in if found then status',t' else status,t diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli index 35e74debf..da50ea2ac 100644 --- a/matita/components/ng_tactics/nTacStatus.mli +++ b/matita/components/ng_tactics/nTacStatus.mli @@ -70,7 +70,7 @@ val term_of_cic_term : val mk_cic_term : NCic.context -> NCic.term -> cic_term val disambiguate: - #pstatus as 'status -> NCic.context -> tactic_term -> cic_term option -> + #pstatus as 'status -> NCic.context -> tactic_term -> cic_term NCicRefiner.expected_type -> 'status * cic_term (* * cic_term XXX *) val analyse_indty: @@ -90,7 +90,7 @@ val typeof: val unify: #pstatus as 'status -> NCic.context -> cic_term -> cic_term -> 'status val refine: - #pstatus as 'status -> NCic.context -> cic_term -> cic_term option -> + #pstatus as 'status -> NCic.context -> cic_term -> cic_term NCicRefiner.expected_type -> 'status * cic_term * cic_term (* status, term, type *) val apply_subst: #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index 6870dab57..6241a3ea6 100644 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@ -424,7 +424,7 @@ let generalize_tac ~where = _,_,(None,_,_) -> fail (lazy "No term to generalize") | txt,txtlen,(Some what,_,_) -> let status, what = - disambiguate status (ctx_of goalty) (txt,txtlen,what) None + disambiguate status (ctx_of goalty) (txt,txtlen,what) `XTNone in status,what,[] ) @@ -466,7 +466,8 @@ let reduce_tac ~reduction ~where = let change_tac ~where ~with_what = let change status t = - let status, ww = disambiguate status (ctx_of t) with_what None in +(* FG: `XTSort could be used when we change the whole goal *) + let status, ww = disambiguate status (ctx_of t) with_what `XTNone in let status = unify status (ctx_of t) t ww in status, ww in @@ -499,7 +500,7 @@ let ref_of_indtyinfo iti = iti.reference;; let analyze_indty_tac ~what indtyref = distribute_tac (fun (status as orig_status) goal -> let goalty = get_goalty status goal in - let status, what = disambiguate status (ctx_of goalty) what None in + let status, what = disambiguate status (ctx_of goalty) what `XTInd in let status, ty_what = typeof status (ctx_of what) what in let status, (r,consno,lefts,rights) = analyse_indty status ty_what in let leftno = List.length lefts in @@ -592,14 +593,14 @@ let intros_tac ?names_ref names s = let cases ~what status goal = let gty = get_goalty status goal in - let status, what = disambiguate status (ctx_of gty) what None in + let status, what = disambiguate status (ctx_of gty) what `XTInd in let status, ty = typeof status (ctx_of what) what in let status, (ref, consno, _, _) = analyse_indty status ty in let status, what = term_of_cic_term status what (ctx_of gty) in let t = NCic.Match (ref,NCic.Implicit `Term, what, HExtlib.mk_list (NCic.Implicit `Term) consno) - in + in instantiate status goal (mk_cic_term (ctx_of gty) t) ;; @@ -639,7 +640,7 @@ let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal -> let assert0_tac (hyps,concl) = distribute_tac (fun status goal -> let gty = get_goalty status goal in let eq status ctx t1 t2 = - let status,t1 = disambiguate status ctx t1 None in + let status,t1 = disambiguate status ctx t1 `XTSort in let status,t1 = apply_subst status ctx t1 in let status,t1 = term_of_cic_term status t1 ctx in let t2 = mk_cic_term ctx t2 in diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index 1b1132dee..25274de81 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -145,7 +145,7 @@ let is_a_fact_obj s uri = let is_a_fact_ast status subst metasenv ctx cand = noprint ~depth:0 (lazy ("checking facts " ^ NotationPp.pp_term status cand)); - let status, t = disambiguate status ctx ("",0,cand) None in + let status, t = disambiguate status ctx ("",0,cand) `XTNone in let status,t = term_of_cic_term status t ctx in let ty = NCicTypeChecker.typeof status subst metasenv ctx t in is_a_fact status (mk_cic_term ctx ty) @@ -247,7 +247,7 @@ let solve f status eq_cache goal = NCicUnification.unify status metasenv subst ctx gty pty *) NCicRefiner.typeof (status#set_coerc_db NCicCoercion.empty_db) - metasenv subst ctx pt (Some gty) + metasenv subst ctx pt (`XTSome gty) in noprint (lazy (Printf.sprintf "Refined in %fs" (Unix.gettimeofday() -. stamp))); @@ -331,7 +331,7 @@ let index_local_equations2 eq_cache status open_goal lemmas nohyps = let status,lemmas = List.fold_left (fun (status,lemmas) l -> - let status,l = NTacStatus.disambiguate status ctx l None in + let status,l = NTacStatus.disambiguate status ctx l `XTNone in let status,l = NTacStatus.term_of_cic_term status l ctx in status,l::lemmas) (status,[]) lemmas in @@ -590,7 +590,7 @@ let smart_apply t unit_eq status g = let n,h,metasenv,subst,o = status#obj in let gname, ctx, gty = List.assoc g metasenv in (* let ggty = mk_cic_term context gty in *) - let status, t = disambiguate status ctx t None in + let status, t = disambiguate status ctx t `XTNone in let status,t = term_of_cic_term status t ctx in let _,_,metasenv,subst,_ = status#obj in let ty = NCicTypeChecker.typeof status subst metasenv ctx t in @@ -974,7 +974,7 @@ let openg_no status = List.length (head_goals status#stack) let sort_candidates status ctx candidates = let _,_,metasenv,subst,_ = status#obj in let branch cand = - let status,ct = disambiguate status ctx ("",0,cand) None in + let status,ct = disambiguate status ctx ("",0,cand) `XTNone in let status,t = term_of_cic_term status ct ctx in let ty = NCicTypeChecker.typeof status subst metasenv ctx t in let res = branch status (mk_cic_term ctx ty) in @@ -1811,7 +1811,8 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = | None -> None | Some l -> let to_Ast t = - let status, res = disambiguate status [] t None in +(* FG: `XTSort here? *) + let status, res = disambiguate status [] t `XTNone in let _,res = term_of_cic_term status res (ctx_of res) in Ast.NCic res in Some (List.map to_Ast l) diff --git a/matita/matita/contribs/lambda/background/preamble.ma b/matita/matita/contribs/lambda/background/preamble.ma index 769ffa5a3..6455bfcf4 100644 --- a/matita/matita/contribs/lambda/background/preamble.ma +++ b/matita/matita/contribs/lambda/background/preamble.ma @@ -122,7 +122,7 @@ qed. (* Note: this cannot be in lib because of the missing xoa quantifier *) lemma lstar_inv_pos: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → 0 < |l| → ∃∃a,ll,b. a::ll = l & R a b1 b & lstar A B R ll b b2. -#A #B #R #l #b1 #b2 #H @(lstar_ind_l ????????? H) -b1 +#A #B #R #l #b1 #b2 #H @(lstar_ind_l … l b1 H) -l -b1 [ #H elim (lt_refl_false … H) | #a #ll #b1 #b #Hb1 #Hb2 #_ #_ /2 width=6/ (**) (* auto fail if we do not remove the inductive premise *) ] diff --git a/matita/matita/contribs/lambda/paths/dst_computation.ma b/matita/matita/contribs/lambda/paths/dst_computation.ma index f7740daf7..a532e7b15 100644 --- a/matita/matita/contribs/lambda/paths/dst_computation.ma +++ b/matita/matita/contribs/lambda/paths/dst_computation.ma @@ -96,13 +96,13 @@ lemma dst_inv_lift: deliftable_sn dst. | #s #N1 #C1 #C2 #Hs #HN1 #_ #IHC12 #d #M1 #HMN1 elim (pl_sreds_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2 elim (lift_inv_abst … HM2) -HM2 #A1 #HAC1 #HM2 destruct - elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *) + elim (IHC12 …) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *) @(ex2_intro … (𝛌.A2)) // /2 width=5/ | #s #N1 #D1 #D2 #C1 #C2 #Hs #HN1 #_ #_ #IHD12 #IHC12 #d #M1 #HMN1 elim (pl_sreds_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2 elim (lift_inv_appl … HM2) -HM2 #B1 #A1 #HBD1 #HAC1 #HM2 destruct - elim (IHD12 ???) -IHD12 [4: // |2,3: skip ] #B2 #HB12 #HBD2 destruct (**) (* simplify line *) - elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *) + elim (IHD12 …) -IHD12 [4: // |2,3: skip ] #B2 #HB12 #HBD2 destruct (**) (* simplify line *) + elim (IHC12 …) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *) @(ex2_intro … (@B2.A2)) // /2 width=7/ ] qed-. @@ -127,22 +127,22 @@ qed. lemma dst_step_dx: ∀p,M,M2. M ↦[p] M2 → ∀M1. M1 ⓢ↦* M → M1 ⓢ↦* M2. #p #M #M2 #H elim H -p -M -M2 [ #B #A #M1 #H - elim (dst_inv_appl … H ???) -H [4: // |2,3: skip ] #s #B1 #M #Hs #HM1 #HB1 #H (**) (* simplify line *) - elim (dst_inv_abst … H ??) -H [3: // |2: skip ] #r #A1 #Hr #HM #HA1 (**) (* simplify line *) + elim (dst_inv_appl … H …) -H [4: // |2,3: skip ] #s #B1 #M #Hs #HM1 #HB1 #H (**) (* simplify line *) + elim (dst_inv_abst … H …) -H [3: // |2: skip ] #r #A1 #Hr #HM #HA1 (**) (* simplify line *) lapply (pl_sreds_trans … HM1 … (dx:::r) (@B1.𝛌.A1) ?) /2 width=1/ -M #HM1 lapply (pl_sreds_step_dx … HM1 (◊) ([↙B1]A1) ?) -HM1 // #HM1 @(dst_step_sn … HM1) /2 width=1/ /4 width=1/ | #p #A #A2 #_ #IHA2 #M1 #H - elim (dst_inv_abst … H ??) -H [3: // |2: skip ] /3 width=5/ (**) (* simplify line *) + elim (dst_inv_abst … H …) -H [3: // |2: skip ] /3 width=5/ (**) (* simplify line *) | #p #B #B2 #A #_ #IHB2 #M1 #H - elim (dst_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *) + elim (dst_inv_appl … H …) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *) | #p #B #A #A2 #_ #IHA2 #M1 #H - elim (dst_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *) + elim (dst_inv_appl … H …) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *) ] qed-. lemma pl_sreds_dst: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⓢ↦* M2. -#s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 // /2 width=4 by dst_step_dx/ +#s #M1 #M2 #H @(lstar_ind_r … s M2 H) -s -M2 // /2 width=4 by dst_step_dx/ qed. lemma dst_inv_pl_sreds_is_standard: ∀M,N. M ⓢ↦* N → @@ -179,23 +179,23 @@ lemma dst_in_whd_swap: ∀p. in_whd p → ∀N1,N2. N1 ↦[p] N2 → ∀M1. M1 ∃∃q,M2. in_whd q & M1 ↦[q] M2 & M2 ⓢ↦* N2. #p #H @(in_whd_ind … H) -p [ #N1 #N2 #H1 #M1 #H2 - elim (pl_sred_inv_nil … H1 ?) -H1 // #D #C #HN1 #HN2 + elim (pl_sred_inv_nil … H1 …) -H1 // #D #C #HN1 #HN2 elim (dst_inv_appl … H2 … HN1) -N1 #s1 #D1 #N #Hs1 #HM1 #HD1 #H - elim (dst_inv_abst … H ??) -H [3: // |2: skip ] #s2 #C1 #Hs2 #HN #HC1 (**) (* simplify line *) + elim (dst_inv_abst … H …) -H [3: // |2: skip ] #s2 #C1 #Hs2 #HN #HC1 (**) (* simplify line *) lapply (pl_sreds_trans … HM1 … (dx:::s2) (@D1.𝛌.C1) ?) /2 width=1/ -N #HM1 lapply (pl_sreds_step_dx … HM1 (◊) ([↙D1]C1) ?) -HM1 // #HM1 - elim (pl_sreds_inv_pos … HM1 ?) -HM1 + elim (pl_sreds_inv_pos … HM1 …) -HM1 [2: >length_append normalize in ⊢ (??(??%)); // ] #q #r #M #Hq #HM1 #HM lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr @(ex3_2_intro … HM1) -M1 // -q @(dst_step_sn … HM) /2 width=1/ | #p #_ #IHp #N1 #N2 #H1 #M1 #H2 - elim (pl_sred_inv_dx … H1 ??) -H1 [3: // |2: skip ] #D #C1 #C2 #HC12 #HN1 #HN2 (**) (* simplify line *) + elim (pl_sred_inv_dx … H1 …) -H1 [3: // |2: skip ] #D #C1 #C2 #HC12 #HN1 #HN2 (**) (* simplify line *) elim (dst_inv_appl … H2 … HN1) -N1 #s #B #A1 #Hs #HM1 #HBD #HAC1 elim (IHp … HC12 … HAC1) -p -C1 #p #C1 #Hp #HAC1 #HC12 lapply (pl_sreds_step_dx … HM1 (dx::p) (@B.C1) ?) -HM1 /2 width=1/ -A1 #HM1 - elim (pl_sreds_inv_pos … HM1 ?) -HM1 + elim (pl_sreds_inv_pos … HM1 …) -HM1 [2: >length_append normalize in ⊢ (??(??%)); // ] #q #r #M #Hq #HM1 #HM lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -p -s * #Hq #Hr diff --git a/matita/matita/contribs/lambda/paths/labeled_sequential_reduction.ma b/matita/matita/contribs/lambda/paths/labeled_sequential_reduction.ma index 891af919e..8864a708e 100644 --- a/matita/matita/contribs/lambda/paths/labeled_sequential_reduction.ma +++ b/matita/matita/contribs/lambda/paths/labeled_sequential_reduction.ma @@ -116,13 +116,13 @@ qed. theorem pl_sred_mono: ∀p. singlevalued … (pl_sred p). #p #M #N1 #H elim H -p -M -N1 -[ #B #A #N2 #H elim (pl_sred_inv_nil … H ?) -H // +[ #B #A #N2 #H elim (pl_sred_inv_nil … H …) -H // #D #C #H #HN2 destruct // -| #p #A1 #A2 #_ #IHA12 #N2 #H elim (pl_sred_inv_rc … H ??) -H [3: // |2: skip ] (**) (* simplify line *) +| #p #A1 #A2 #_ #IHA12 #N2 #H elim (pl_sred_inv_rc … H …) -H [3: // |2: skip ] (**) (* simplify line *) #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ -| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (pl_sred_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *) +| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (pl_sred_inv_sn … H …) -H [3: // |2: skip ] (**) (* simplify line *) #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/ -| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (pl_sred_inv_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *) +| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (pl_sred_inv_dx … H …) -H [3: // |2: skip ] (**) (* simplify line *) #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ ] qed-. diff --git a/matita/matita/contribs/lambda/paths/labeled_st_computation.ma b/matita/matita/contribs/lambda/paths/labeled_st_computation.ma index eb5e5dc64..29dd72769 100644 --- a/matita/matita/contribs/lambda/paths/labeled_st_computation.ma +++ b/matita/matita/contribs/lambda/paths/labeled_st_computation.ma @@ -90,7 +90,7 @@ lemma pl_sts_inv_rc_abst_dx: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 → ∀r. | #p #s #F1 #F #HF1 #_ #IHF2 #r #H -b2 elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr elim (pl_st_inv_rc … HF1 … Hp) -HF1 -p #b1 #T1 #T #HT1 #HF1 #HF destruct - elim (IHF2 ??) -IHF2 [3: // |2: skip ] (**) (* simplify line *) + elim (IHF2 …) -IHF2 [3: // |2: skip ] (**) (* simplify line *) #b0 #T0 #HT02 #H destruct lapply (pl_sts_step_sn … HT1 … HT02) -T /2 width=4/ ] @@ -103,7 +103,7 @@ lemma pl_sts_inv_sn_appl_dx: ∀b2,s,F1,V2,T2. F1 Ⓡ↦*[s] {b2}@V2.T2 → ∀r | #p #s #F1 #F #HF1 #_ #IHF2 #r #H -b2 elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr elim (pl_st_inv_sn … HF1 … Hp) -HF1 -p #b1 #V1 #V #T1 #HV1 #HF1 #HF destruct - elim (IHF2 ??) -IHF2 [3: // |2: skip ] (**) (* simplify line *) + elim (IHF2 …) -IHF2 [3: // |2: skip ] (**) (* simplify line *) #b0 #V0 #T0 #HV02 #H destruct lapply (pl_sts_step_sn … HV1 … HV02) -V /2 width=5/ ] @@ -116,7 +116,7 @@ lemma pl_sts_inv_dx_appl_dx: ∀b,s,F1,V,T2. F1 Ⓡ↦*[s] {b}@V.T2 → ∀r. dx | #p #s #F1 #F #HF1 #_ #IHF2 #r #H elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr elim (pl_st_inv_dx … HF1 … Hp) -HF1 -p #b0 #V0 #T1 #T #HT1 #HF1 #HF destruct - elim (IHF2 ??) -IHF2 [3: // |2: skip ] (**) (* simplify line *) + elim (IHF2 …) -IHF2 [3: // |2: skip ] (**) (* simplify line *) #T0 #HT02 #H destruct lapply (pl_sts_step_sn … HT1 … HT02) -T /2 width=3/ ] @@ -150,17 +150,17 @@ lemma pl_sts_fwd_dx_sn_appl_dx: ∀b2,s,r,F1,V2,T2. F1 Ⓡ↦*[(dx:::s)@(sn:::r) ∃∃b1,V1,T1,T0. V1 Ⓡ↦*[r] V2 & T1 Ⓡ↦*[s] T0 & {b1}@V1.T1 = F1. #b2 #s #r #F1 #V2 #T2 #H elim (pl_sts_inv_trans … H) -H #F #HF1 #H -elim (pl_sts_inv_sn_appl_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *) +elim (pl_sts_inv_sn_appl_dx … H …) -H [3: // |2: skip ] (**) (* simplify line *) #b #V #T #HV2 #H destruct -elim (pl_sts_inv_dx_appl_dx … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *) +elim (pl_sts_inv_dx_appl_dx … HF1 …) -HF1 [3: // |2: skip ] (**) (* simplify line *) #T1 #HT1 #H destruct /2 width=7/ qed-. theorem pl_sts_fwd_is_standard: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → is_standard s. #s elim s -s // #p1 * // #p2 #s #IHs #F1 #F2 #H -elim (pl_sts_inv_cons … H ???) -H [4: // |2,3: skip ] #F3 #HF13 #H (**) (* simplify line *) -elim (pl_sts_inv_cons … H ???) [2: // |3,4: skip ] #F4 #HF34 #_ (**) (* simplify line *) +elim (pl_sts_inv_cons … H …) -H [4: // |2,3: skip ] #F3 #HF13 #H (**) (* simplify line *) +elim (pl_sts_inv_cons … H …) [2: // |3,4: skip ] #F4 #HF34 #_ (**) (* simplify line *) lapply (pl_st_fwd_sle … HF13 … HF34) -F1 -F4 /3 width=3/ qed-. @@ -172,7 +172,7 @@ lapply (pl_sts_fwd_is_standard … H) [ #_ @(ex2_2_intro … ◊ ◊) // (**) (* auto needs some help here *) | #p #s #F1 #F #HF1 #HF2 #IHF1 #Hs lapply (is_standard_fwd_cons … Hs) #H - elim (IHF1 ?) // -IHF1 -H #r1 #r2 #Hr1 #H destruct + elim (IHF1 …) // -IHF1 -H #r1 #r2 #Hr1 #H destruct elim (in_whd_or_in_inner p) #Hp [ -Hs -F1 -F -T2 -b2 @(ex2_2_intro … (p::r1) r2) // /2 width=1/ (**) (* auto needs some help here *) @@ -182,17 +182,17 @@ lapply (pl_sts_fwd_is_standard … H) elim (in_inner_inv … Hp) -Hp * #q [3: #IHq ] #Hp (* case 1: dx *) [ -IHq - elim (pl_sts_inv_rc_abst_dx … HF2 ??) -b2 [3: // |2: skip ] (**) (* simplify line *) + elim (pl_sts_inv_rc_abst_dx … HF2 …) -b2 [3: // |2: skip ] (**) (* simplify line *) #b #T #_ #HT -T2 - elim (pl_st_inv_dx … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *) + elim (pl_st_inv_dx … HF1 …) -HF1 [3: // |2: skip ] (**) (* simplify line *) #c #V #T1 #T0 #_ #_ #HT0 -q -T1 -F1 destruct (* case 2: rc *) | destruct -F1 -F -T2 -b2 @(ex2_2_intro … ◊ (q::r2)) // (**) (* auto needs some help here *) (* case 3: sn *) - | elim (pl_sts_inv_rc_abst_dx … HF2 ??) -b2 [3: // |2: skip ] (**) (* simplify line *) + | elim (pl_sts_inv_rc_abst_dx … HF2 …) -b2 [3: // |2: skip ] (**) (* simplify line *) #b #T #_ #HT -T2 - elim (pl_st_inv_sn … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *) + elim (pl_st_inv_sn … HF1 …) -HF1 [3: // |2: skip ] (**) (* simplify line *) #c #V1 #V #T0 #_ #_ #HT0 -c -q -V1 -F1 destruct ] ] @@ -208,7 +208,7 @@ lapply (pl_sts_fwd_is_standard … H) [ #_ @(ex3_3_intro … ◊ ◊ ◊) // (**) (* auto needs some help here *) | #p #s #F1 #F #HF1 #HF2 #IHF1 #Hs lapply (is_standard_fwd_cons … Hs) #H - elim (IHF1 ?) // -IHF1 -H #r1 #r2 #r3 #Hr1 #Hr2 #H destruct + elim (IHF1 …) // -IHF1 -H #r1 #r2 #r3 #Hr1 #Hr2 #H destruct elim (in_whd_or_in_inner p) #Hp [ -Hs -F1 -F -V2 -T2 -b2 @(ex3_3_intro … (p::r1) r2 r3) // /2 width=1/ (**) (* auto needs some help here *) @@ -247,20 +247,20 @@ lemma pl_sred_is_standard_pl_st: ∀p,M,M2. M ↦[p] M2 → ∀F. ⇓F = M → elim (carrier_inv_abst … HF) -HF #b #T #HT #HF destruct elim (pl_sts_fwd_abst_dx … HM1) #r1 #r2 #Hr1 #H destruct elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT - elim (pl_sts_inv_pl_sreds … HM1 ?) // #M0 #_ #H -M1 -Hr1 destruct + elim (pl_sts_inv_pl_sreds … HM1 …) // #M0 #_ #H -M1 -Hr1 destruct >associative_append in Hs; #Hs lapply (is_standard_fwd_append_dx … Hs) -r1 <(map_cons_append … r2 (p::◊)) #H lapply (is_standard_inv_compatible_rc … H) -H #Hp - elim (pl_sts_inv_rc_abst_dx … HT ??) -HT [3: // |2: skip ] #b0 #T0 #HT02 #H (**) (* simplify line *) + elim (pl_sts_inv_rc_abst_dx … HT …) -HT [3: // |2: skip ] #b0 #T0 #HT02 #H (**) (* simplify line *) elim (boolean_inv_abst … (sym_eq … H)) -H #A0 #_ #H #_ -b0 -M0 destruct - elim (IHA12 … HT02 ?) // -r2 -A0 -IHA12 #F2 #HF2 #H + elim (IHA12 … HT02 …) // -r2 -A0 -IHA12 #F2 #HF2 #H @(ex2_intro … ({⊥}𝛌.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *) | #p #B1 #B2 #A #_ #IHB12 #F #HF #s #M1 #HM1 #Hs elim (carrier_inv_appl … HF) -HF #b #V #T #HV #HT #HF destruct elim (pl_sts_fwd_appl_dx … HM1) #r1 #r2 #r3 #Hr1 #_ #H destruct elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT - elim (pl_sts_inv_pl_sreds … HM1 ?) // #M0 #_ #H -M1 -Hr1 destruct + elim (pl_sts_inv_pl_sreds … HM1 …) // #M0 #_ #H -M1 -Hr1 destruct >associative_append in Hs; #Hs lapply (is_standard_fwd_append_dx … Hs) -r1 >associative_append #Hs @@ -269,13 +269,13 @@ lemma pl_sred_is_standard_pl_st: ∀p,M,M2. M ↦[p] M2 → ∀F. ⇓F = M → lapply (is_standard_inv_compatible_sn … H) -H #Hp elim (pl_sts_fwd_dx_sn_appl_dx … HT) -HT #b0 #V0 #T0 #T1 #HV0 #_ #H -T1 -r2 elim (boolean_inv_appl … (sym_eq … H)) -H #B0 #A0 #_ #H #_ #_ -b0 -M0 -T0 destruct - elim (IHB12 … HV0 ?) // -r3 -B0 -IHB12 #G2 #HG2 #H + elim (IHB12 … HV0 …) // -r3 -B0 -IHB12 #G2 #HG2 #H @(ex2_intro … ({⊥}@G2.{⊥}⇕T)) normalize // /2 width=1/ (**) (* auto needs some help here *) | #p #B #A1 #A2 #_ #IHA12 #F #HF #s #M1 #HM1 #Hs elim (carrier_inv_appl … HF) -HF #b #V #T #HV #HT #HF destruct elim (pl_sts_fwd_appl_dx … HM1) #r1 #r2 #r3 #Hr1 #Hr2 #H destruct elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT - elim (pl_sts_inv_pl_sreds … HM1 ?) // #M0 #_ #H -M1 -Hr1 destruct + elim (pl_sts_inv_pl_sreds … HM1 …) // #M0 #_ #H -M1 -Hr1 destruct >associative_append in Hs; #Hs lapply (is_standard_fwd_append_dx … Hs) -r1 >associative_append #Hs @@ -287,22 +287,22 @@ lemma pl_sred_is_standard_pl_st: ∀p,M,M2. M ↦[p] M2 → ∀F. ⇓F = M → lapply (is_whd_is_inner_inv … Hr2) -Hr2 // -H #H destruct lapply (pl_sts_inv_nil … HT ?) -HT // #H elim (boolean_inv_appl … H) -H #B0 #A0 #_ #_ #H #_ -M0 -B0 destruct - elim (IHA12 … A0 ??) -IHA12 [3,5,6: // |2,4: skip ] (* simplify line *) + elim (IHA12 … A0 …) -IHA12 [3,5,6: // |2,4: skip ] (* simplify line *) #F2 #HF2 #H @(ex2_intro … ({b}@V.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *) | <(map_cons_append … r2 (p::◊)) in Hs; #H lapply (is_standard_inv_compatible_dx … H ?) -H /3 width=1/ -Hp #Hp >append_nil in HT; #HT - elim (pl_sts_inv_dx_appl_dx … HT ??) -HT [3: // |2: skip ] (* simplify line *) + elim (pl_sts_inv_dx_appl_dx … HT …) -HT [3: // |2: skip ] (* simplify line *) #T0 #HT0 #H elim (boolean_inv_appl … (sym_eq … H)) -H #B0 #A0 #_ #_ #H #_ -M0 -B0 destruct - elim (IHA12 … HT0 ?) // -r2 -A0 -IHA12 #F2 #HF2 #H + elim (IHA12 … HT0 …) // -r2 -A0 -IHA12 #F2 #HF2 #H @(ex2_intro … ({b}@V.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *) ] | -IHA12 -Hr2 -M0 * #q #r #H destruct lapply (is_standard_fwd_append_dx … Hs) -r2 #Hs lapply (is_standard_fwd_sle … Hs) -r #H - elim (sle_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *) + elim (sle_inv_sn … H …) -H [3: // |2: skip ] (**) (* simplify line *) #q0 #_ #H destruct ] ] @@ -314,7 +314,7 @@ theorem pl_sreds_is_standard_pl_sts: ∀s,M1,M2. M1 ↦*[s] M2 → is_standard s #p #s #M #M2 #_ #HM2 #IHM1 #Hsp lapply (is_standard_fwd_append_sn … Hsp) #Hs elim (IHM1 Hs) -IHM1 -Hs #F #HM1 #H -elim (pl_sred_is_standard_pl_st … HM2 … HM1 ?) -HM2 // -M -Hsp #F2 #HF2 #HFM2 +elim (pl_sred_is_standard_pl_st … HM2 … HM1 …) -HM2 // -M -Hsp #F2 #HF2 #HFM2 lapply (pl_sts_step_dx … HM1 … HF2) -F #H @(ex2_intro … F2) // (**) (* auto needs some help here *) qed-. diff --git a/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma b/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma index e18c1d405..2f93b35af 100644 --- a/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma +++ b/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma @@ -122,11 +122,11 @@ lemma pl_st_inv_pl_sred: ∀p. in_whd p → ∀M1,F2. {⊤}⇑M1 Ⓡ↦[p] F2 ∃∃M2. M1 ↦[p] M2 & {⊤}⇑M2 = F2. #p @(in_whd_ind … p) -p [ #M1 #F2 #H - elim (pl_st_inv_nil … H ?) -H // #V #T #HM1 #H + elim (pl_st_inv_nil … H …) -H // #V #T #HM1 #H elim (boolean_inv_appl … (sym_eq … HM1)) -HM1 #B #N #_ #HB #HN #HM1 elim (boolean_inv_abst … HN) -HN #A #_ #HA #HN destruct /2 width=3/ | #p #_ #IHp #M1 #F2 #H - elim (pl_st_inv_dx … H ??) -H [3: // |2:skip ] #b #V #T1 #T2 #HT12 #HM1 #H (**) (* simplify line *) + elim (pl_st_inv_dx … H …) -H [3: // |2:skip ] #b #V #T1 #T2 #HT12 #HM1 #H (**) (* simplify line *) elim (boolean_inv_appl … (sym_eq … HM1)) -HM1 #B #A #Hb #HB #HA #HM1 destruct elim (IHp … HT12) -IHp -HT12 #C #HAC #H destruct @(ex2_intro … (@B.C)) // /2 width=1/ (**) (* auto needs some help here *) @@ -185,13 +185,13 @@ qed-. theorem pl_st_mono: ∀p. singlevalued … (pl_st p). #p #F #G1 #H elim H -p -F -G1 -[ #V #T #G2 #H elim (pl_st_inv_nil … H ?) -H // +[ #V #T #G2 #H elim (pl_st_inv_nil … H …) -H // #W #U #H #HG2 destruct // -| #b #p #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_rc … H ??) -H [3: // |2: skip ] (**) (* simplify line *) +| #b #p #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_rc … H …) -H [3: // |2: skip ] (**) (* simplify line *) #c #U1 #U2 #HU12 #H #HG2 destruct /3 width=1/ -| #b #p #V1 #V2 #T #_ #IHV12 #G2 #H elim (pl_st_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *) +| #b #p #V1 #V2 #T #_ #IHV12 #G2 #H elim (pl_st_inv_sn … H …) -H [3: // |2: skip ] (**) (* simplify line *) #c #W1 #W2 #U #HW12 #H #HG2 destruct /3 width=1/ -| #b #p #V #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *) +| #b #p #V #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_dx … H …) -H [3: // |2: skip ] (**) (* simplify line *) #c #W #U1 #U2 #HU12 #H #HG2 destruct /3 width=1/ ] qed-. @@ -199,14 +199,14 @@ qed-. theorem pl_st_fwd_sle: ∀p1,F1,F. F1 Ⓡ↦[p1] F → ∀p2,F2. F Ⓡ↦[p2] F2 → p1 ≤ p2. #p1 #F1 #F #H elim H -p1 -F1 -F // -[ #b #p #T1 #T #_ #IHT1 #p2 #F2 #H elim (pl_st_inv_abst … H ???) -H [3: // |2,4: skip ] (**) (* simplify line *) +[ #b #p #T1 #T #_ #IHT1 #p2 #F2 #H elim (pl_st_inv_abst … H …) -H [3: // |2,4: skip ] (**) (* simplify line *) #q #T2 #HT2 #H1 #H2 destruct /3 width=2/ -| #b #p #V1 #V #T #_ #IHV1 #p2 #F2 #H elim (pl_st_inv_appl … H ????) -H [7: // |2,3,4: skip ] * (**) (* simplify line *) +| #b #p #V1 #V #T #_ #IHV1 #p2 #F2 #H elim (pl_st_inv_appl … H …) -H [7: // |2,3,4: skip ] * (**) (* simplify line *) [ #U #H destruct | #q #V2 #H1 #HV2 #H2 destruct /3 width=2/ - | #q #U #_ #H elim (pl_st_inv_empty … H ??) [ // | skip ] (**) (* simplify line *) + | #q #U #_ #H elim (pl_st_inv_empty … H …) [ // | skip ] (**) (* simplify line *) ] -| #b #p #V #T1 #T #HT1 #IHT1 #p2 #F2 #H elim (pl_st_inv_appl … H ????) -H [7: // |2,3,4: skip ] * (**) (* simplify line *) +| #b #p #V #T1 #T #HT1 #IHT1 #p2 #F2 #H elim (pl_st_inv_appl … H …) -H [7: // |2,3,4: skip ] * (**) (* simplify line *) [ #U #_ #H1 #H2 #_ -b -V -F2 -IHT1 elim (pl_st_fwd_abst … HT1 … H2) // -H1 * #q #H elim (pl_st_inv_rc … HT1 … H) -HT1 -H #b #U1 #U2 #_ #_ #H -b -q -T1 -U1 destruct diff --git a/matita/matita/contribs/lambda/paths/path.ma b/matita/matita/contribs/lambda/paths/path.ma index 1993d056b..743ec4c34 100644 --- a/matita/matita/contribs/lambda/paths/path.ma +++ b/matita/matita/contribs/lambda/paths/path.ma @@ -81,7 +81,7 @@ lemma in_inner_ind: ∀R:predicate path. (∀p. in_inner p → R p → R (dx::p)) → ∀p. in_inner p → R p. #R #H1 #H2 #IH #p elim p -p -[ #H elim (H ?) -H // +[ #H elim (H …) -H // | * #p #IHp // #H lapply (in_inner_inv_dx … H) -H /3 width=1/ ] diff --git a/matita/matita/contribs/lambda/paths/standard_order.ma b/matita/matita/contribs/lambda/paths/standard_order.ma index 5ff11ea34..75a3ca97f 100644 --- a/matita/matita/contribs/lambda/paths/standard_order.ma +++ b/matita/matita/contribs/lambda/paths/standard_order.ma @@ -77,7 +77,7 @@ lemma sle_inv_dx: ∀p,q. p ≤ q → ∀q0. dx::q0 = q → in_whd p ∨ ∃∃p0. p0 ≤ q0 & dx::p0 = p. #p #q #H @(star_ind_l … p H) -p [ /3 width=3/ ] #p0 #p #Hp0 #_ #IHpq #q1 #H destruct -elim (IHpq ??) -IHpq [4: // |3: skip ] (**) (* simplify line *) +elim (IHpq …) -IHpq [4: // |3: skip ] (**) (* simplify line *) [ lapply (sprec_fwd_in_whd … Hp0) -Hp0 /3 width=1/ | * #p1 #Hpq1 #H elim (sprec_inv_dx … Hp0 … H) -p [ #H destruct /2 width=1/ @@ -91,7 +91,7 @@ lemma sle_inv_rc: ∀p,q. p ≤ q → ∀p0. rc::p0 = p → ∃q0. sn::q0 = q. #p #q #H elim H -q /3 width=3/ #q #q0 #_ #Hq0 #IHpq #p0 #H destruct -elim (IHpq p0 ?) -IHpq // * +elim (IHpq p0 …) -IHpq // * [ #p1 #Hp01 #H elim (sprec_inv_rc … Hq0 … H) -q * /3 width=3/ /4 width=3/ | #p1 #H elim (sprec_inv_sn … Hq0 … H) -q /3 width=2/ @@ -102,7 +102,7 @@ lemma sle_inv_sn: ∀p,q. p ≤ q → ∀p0. sn::p0 = p → ∃∃q0. p0 ≤ q0 & sn::q0 = q. #p #q #H elim H -q /2 width=3/ #q #q0 #_ #Hq0 #IHpq #p0 #H destruct -elim (IHpq p0 ?) -IHpq // #p1 #Hp01 #H +elim (IHpq p0 …) -IHpq // #p1 #Hp01 #H elim (sprec_inv_sn … Hq0 … H) -q /3 width=3/ qed-. diff --git a/matita/matita/contribs/lambda/paths/standard_trace.ma b/matita/matita/contribs/lambda/paths/standard_trace.ma index edc77df25..f9549d983 100644 --- a/matita/matita/contribs/lambda/paths/standard_trace.ma +++ b/matita/matita/contribs/lambda/paths/standard_trace.ma @@ -49,13 +49,13 @@ qed. lemma is_standard_inv_compatible_sn: ∀s. is_standard (sn:::s) → is_standard s. #s elim s -s // #a1 * // #a2 #s #IHs * #H -elim (sle_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *) +elim (sle_inv_sn … H …) -H [3: // |2: skip ] (**) (* simplify line *) #a #Ha1 #H destruct /3 width=1/ qed-. lemma is_standard_inv_compatible_rc: ∀s. is_standard (rc:::s) → is_standard s. #s elim s -s // #a1 * // #a2 #s #IHs * #H -elim (sle_inv_rc … H ??) -H [4: // |2: skip ] * (**) (* simplify line *) +elim (sle_inv_rc … H …) -H [4: // |2: skip ] * (**) (* simplify line *) [ #a #Ha1 #H destruct /3 width=1/ | #a #H destruct ] @@ -64,9 +64,9 @@ qed-. lemma is_standard_inv_compatible_dx: ∀s. is_standard (dx:::s) → is_inner s → is_standard s. #s elim s -s // #a1 * // #a2 #s #IHs * #H -elim (sle_inv_dx … H ??) -H [4: // |3: skip ] (**) (* simplify line *) +elim (sle_inv_dx … H …) -H [4: // |3: skip ] (**) (* simplify line *) [ * #_ #H1a1 #_ * #H2a1 #_ -IHs - elim (H2a1 ?) -H2a1 -a2 -s // + elim (H2a1 …) -H2a1 -a2 -s // | * #a #Ha2 #H destruct #H * #_ /3 width=1/ qed-. diff --git a/matita/matita/contribs/lambda/paths/trace.ma b/matita/matita/contribs/lambda/paths/trace.ma index 3fdcef3f2..fb042bdf6 100644 --- a/matita/matita/contribs/lambda/paths/trace.ma +++ b/matita/matita/contribs/lambda/paths/trace.ma @@ -69,5 +69,5 @@ lemma is_inner_append: ∀r. is_inner r → ∀s. is_inner s → is_inner (r@s). qed. lemma is_whd_is_inner_inv: ∀s. is_whd s → is_inner s → ◊ = s. -* // #p #s * #H1p #_ * #H2p #_ elim (H2p ?) -H2p // +* // #p #s * #H1p #_ * #H2p #_ elim (H2p …) -H2p // qed-. diff --git a/matita/matita/contribs/lambda/subterms/relocating_substitution.ma b/matita/matita/contribs/lambda/subterms/relocating_substitution.ma index f49a7191d..af5efe023 100644 --- a/matita/matita/contribs/lambda/subterms/relocating_substitution.ma +++ b/matita/matita/contribs/lambda/subterms/relocating_substitution.ma @@ -138,7 +138,7 @@ definition sdsubstable_f_dx: ∀S:Type[0]. (S → ?) → predicate (relation sub lemma lstar_sdsubstable_f_dx: ∀S1,f,S2,R. (∀a. sdsubstable_f_dx S1 f (R a)) → ∀l. sdsubstable_f_dx S1 f (lstar S2 … R l). #S1 #f #S2 #R #HR #l #G #F1 #F2 #H -@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/ +@(lstar_ind_l … l F1 H) -l -F1 // /3 width=3/ qed. (* definition sdsubstable_dx: predicate (relation subterms) ≝ λR. @@ -154,7 +154,7 @@ qed. lemma lstar_sdsubstable_dx: ∀S,R. (∀a. sdsubstable_dx (R a)) → ∀l. sdsubstable_dx (lstar S … R l). #S #R #HR #l #G #F1 #F2 #H -@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/ +@(lstar_ind_l … l F1 H) -l -F1 // /3 width=3/ qed. lemma star_sdsubstable: ∀R. reflexive ? R → diff --git a/matita/matita/contribs/lambda/subterms/relocation.ma b/matita/matita/contribs/lambda/subterms/relocation.ma index 16b681837..0943d3fc2 100644 --- a/matita/matita/contribs/lambda/subterms/relocation.ma +++ b/matita/matita/contribs/lambda/subterms/relocation.ma @@ -240,13 +240,13 @@ qed-. lemma lstar_sliftable: ∀S,R. (∀a. sliftable (R a)) → ∀l. sliftable (lstar S … R l). #S #R #HR #l #h #F1 #F2 #H -@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/ +@(lstar_ind_l … l F1 H) -l -F1 // /3 width=3/ qed. lemma lstar_sdeliftable_sn: ∀S,R. (∀a. sdeliftable_sn (R a)) → ∀l. sdeliftable_sn (lstar S … R l). #S #R #HR #l #h #G1 #G2 #H -@(lstar_ind_l ????????? H) -l -G1 /2 width=3/ +@(lstar_ind_l … l G1 H) -l -G1 /2 width=3/ #a #l #G1 #G #HG1 #_ #IHG2 #d #F1 #HFG1 elim (HR … HG1 … HFG1) -G1 #F #HF1 #HFG elim (IHG2 … HFG) -G /3 width=3/ diff --git a/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma b/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma index 558968e25..2287c6b81 100644 --- a/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma +++ b/matita/matita/contribs/lambda/terms/labeled_sequential_computation.ma @@ -37,7 +37,7 @@ qed-. lemma l_sreds_fwd_mult: ∀S,R. (∀a,M,N. R a M N → M ↦ N) → ∀l,M1,M2. l_sreds S R l M1 M2 → ♯{M2} ≤ ♯{M1} ^ (2 ^ (|l|)). -#S #R #HR #l #M1 #M2 #H @(lstar_ind_l ????????? H) -l -M1 normalize // +#S #R #HR #l #M1 #M2 #H @(lstar_ind_l … l M1 H) -l -M1 normalize // #a #l #M1 #M #HM1 #_ #IHM2 lapply (HR … HM1) -HR -a #HM1 lapply (sred_fwd_mult … HM1) #HM1 diff --git a/matita/matita/contribs/lambda/terms/parallel_reduction.ma b/matita/matita/contribs/lambda/terms/parallel_reduction.ma index 2e082eaaa..b54c4bc57 100644 --- a/matita/matita/contribs/lambda/terms/parallel_reduction.ma +++ b/matita/matita/contribs/lambda/terms/parallel_reduction.ma @@ -111,8 +111,8 @@ qed-. lemma pred_conf1_abst: ∀A. confluent1 … pred A → confluent1 … pred (𝛌.A). #A #IH #M1 #H1 #M2 #H2 -elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #A1 #HA1 #H destruct (**) (* simplify line *) -elim (pred_inv_abst … H2 ??) -H2 [3: // |2: skip ] #A2 #HA2 #H destruct (**) (* simplify line *) +elim (pred_inv_abst … H1 …) -H1 [3: // |2: skip ] #A1 #HA1 #H destruct (**) (* simplify line *) +elim (pred_inv_abst … H2 …) -H2 [3: // |2: skip ] #A2 #HA2 #H destruct (**) (* simplify line *) elim (IH … HA1 … HA2) -A /3 width=3/ qed-. @@ -121,7 +121,7 @@ lemma pred_conf1_appl_beta: ∀B,B1,B2,C,C2,M1. B ⤇ B1 → B ⤇ B2 → 𝛌.C ⤇ M1 → C ⤇ C2 → ∃∃M. @B1.M1 ⤇ M & [↙B2]C2 ⤇ M. #B #B1 #B2 #C #C2 #M1 #IH #HB1 #HB2 #H1 #HC2 -elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #C1 #HC1 #H destruct (**) (* simplify line *) +elim (pred_inv_abst … H1 …) -H1 [3: // |2: skip ] #C1 #HC1 #H destruct (**) (* simplify line *) elim (IH B … HB1 … HB2) -HB1 -HB2 // elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/ qed-. @@ -131,8 +131,8 @@ theorem pred_conf: confluent … pred. [ /2 width=3 by pred_conf1_vref/ | /3 width=4 by pred_conf1_abst/ | #B #A #H #M1 #H1 #M2 #H2 destruct - elim (pred_inv_appl … H1 ???) -H1 [5: // |2,3: skip ] * (**) (* simplify line *) - elim (pred_inv_appl … H2 ???) -H2 [5,10: // |2,3,7,8: skip ] * (**) (* simplify line *) + elim (pred_inv_appl … H1 …) -H1 [5: // |2,3: skip ] * (**) (* simplify line *) + elim (pred_inv_appl … H2 …) -H2 [5,10: // |2,3,7,8: skip ] * (**) (* simplify line *) [ #B2 #A2 #HB2 #HA2 #H2 #B1 #A1 #HB1 #HA1 #H1 destruct elim (IH A … HA1 … HA2) -HA1 -HA2 // elim (IH B … HB1 … HB2) // -A -B /3 width=5/ diff --git a/matita/matita/contribs/lambda/terms/relocating_substitution.ma b/matita/matita/contribs/lambda/terms/relocating_substitution.ma index ebf08b2f7..4f813396f 100644 --- a/matita/matita/contribs/lambda/terms/relocating_substitution.ma +++ b/matita/matita/contribs/lambda/terms/relocating_substitution.ma @@ -145,7 +145,7 @@ qed. lemma lstar_dsubstable_dx: ∀S,R. (∀a. dsubstable_dx (R a)) → ∀l. dsubstable_dx (lstar S … R l). #S #R #HR #l #N #M1 #M2 #H -@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/ +@(lstar_ind_l … l M1 H) -l -M1 // /3 width=3/ qed. lemma star_dsubstable: ∀R. reflexive ? R → diff --git a/matita/matita/contribs/lambda/terms/relocation.ma b/matita/matita/contribs/lambda/terms/relocation.ma index 62da59661..15c7fde8c 100644 --- a/matita/matita/contribs/lambda/terms/relocation.ma +++ b/matita/matita/contribs/lambda/terms/relocation.ma @@ -244,13 +244,13 @@ qed-. lemma lstar_liftable: ∀S,R. (∀a. liftable (R a)) → ∀l. liftable (lstar S … R l). #S #R #HR #l #h #M1 #M2 #H -@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/ +@(lstar_ind_l … l M1 H) -l -M1 // /3 width=3/ qed. lemma lstar_deliftable_sn: ∀S,R. (∀a. deliftable_sn (R a)) → ∀l. deliftable_sn (lstar S … R l). #S #R #HR #l #h #N1 #N2 #H -@(lstar_ind_l ????????? H) -l -N1 /2 width=3/ +@(lstar_ind_l … l N1 H) -l -N1 /2 width=3/ #a #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1 elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN elim (IHN2 … HMN) -N /3 width=3/ diff --git a/matita/matita/contribs/lambda/terms/sequential_computation.ma b/matita/matita/contribs/lambda/terms/sequential_computation.ma index 2fc5afd5a..b248e6027 100644 --- a/matita/matita/contribs/lambda/terms/sequential_computation.ma +++ b/matita/matita/contribs/lambda/terms/sequential_computation.ma @@ -78,7 +78,7 @@ lemma sreds_compatible_beta: ∀B1,B2. B1 ↦* B2 → ∀A1,A2. A1 ↦* A2 → qed. theorem sreds_preds: ∀M1,M2. M1 ↦* M2 → M1 ⤇* M2. -#M1 #M2 #H @(star_ind_l ??????? H) -M1 // +#M1 #M2 #H @(star_ind_l … M1 H) -M1 // #M1 #M #HM1 #_ #IHM2 @(preds_step_sn … IHM2) -M2 /2 width=2/ qed. diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 74a95bb10..d86871963 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -121,7 +121,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse ctx in let m, s, status, t = GrafiteDisambiguate.disambiguate_nterm - status None ctx menv subst (parsed_text,parsed_text_length, + status `XTNone ctx menv subst (parsed_text,parsed_text_length, NotationPt.Cast (t,NotationPt.Implicit `JustOne)) (* XXX use the metasenv, if possible *) in -- 2.39.2