From: Enrico Tassi Date: Fri, 2 Oct 2009 17:58:08 +0000 (+0000) Subject: fixed bug in coercion application, input/output swapped in unification X-Git-Tag: make_still_working~3393 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=63b86fce8a75490b957e7301517b9006f58321b6;p=helm.git fixed bug in coercion application, input/output swapped in unification --- diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index c82919f4d..896403d94 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -321,9 +321,9 @@ 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 (`MutualDefinition, name, typ, body) -> + | Ast.Theorem (`MutualDefinition, name, typ, body,_) -> sprintf "<>" - | Ast.Theorem (flavour, name, typ, body) -> + | Ast.Theorem (flavour, name, typ, body,_) -> sprintf "%s %s:\n %s\n%s" (pp_flavour flavour) name diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml index 0480c3d26..4e9da0424 100644 --- a/helm/software/components/acic_content/cicNotationPt.ml +++ b/helm/software/components/acic_content/cicNotationPt.ml @@ -177,7 +177,7 @@ 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 Cic.object_flavour * string * 'term * 'term option + | Theorem of Cic.object_flavour * string * 'term * 'term option * NCic.def_pragma (** flavour, name, type, body * - name is absent when an unnamed theorem is being proved, tipically in * interactive usage diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml index 4e5917a15..0c8abce50 100644 --- a/helm/software/components/acic_content/cicNotationUtil.ml +++ b/helm/software/components/acic_content/cicNotationUtil.ml @@ -406,11 +406,11 @@ let freshen_obj obj = indtypes in CicNotationPt.Inductive (freshen_capture_variables params, indtypes) - | CicNotationPt.Theorem (flav, n, t, ty_opt) -> + | CicNotationPt.Theorem (flav, n, t, ty_opt,p) -> let ty_opt = match ty_opt with None -> None | Some ty -> Some (freshen_term ty) in - CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt) + CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt,p) | CicNotationPt.Record (params, n, ty, fields) -> CicNotationPt.Record (freshen_capture_variables params, n, freshen_term ty, freshen_name_ty_b fields) diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index c465315d4..45fbe756a 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -174,7 +174,7 @@ let mk_record types lpsno fields = let mk_statement flavour name t v = let name = match name with Some name -> name | None -> assert false in - let obj = N.Theorem (flavour, name, t, v) in + let obj = N.Theorem (flavour, name, t, v, `Regular) in G.Executable (floc, G.Command (floc, G.Obj (floc, obj))) let mk_qed = diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml index db305e5d5..91839e209 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml @@ -618,7 +618,7 @@ let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in Cic.InductiveDefinition (tyl,[],List.length params,[`Class (`Record field_names)]) - | CicNotationPt.Theorem (flavour, name, ty, bo) -> + | CicNotationPt.Theorem (flavour, name, ty, bo, _pragma) -> let attrs = [`Flavour flavour] in let ty' = interpretate_term [] env None false ty in (match bo,flavour with diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml index 354a73783..52411d6ed 100644 --- a/helm/software/components/disambiguation/disambiguate.ml +++ b/helm/software/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/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 494701d2d..ea5afab4c 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -747,6 +747,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let obj = uri,height,[],[],obj_kind in let old_status = status in let status = NCicLibrary.add_obj status obj in +(* prerr_endline (NCicPp.ppobj obj); *) HLog.message ("New object: " ^ NUri.string_of_uri uri); (try (*prerr_endline (NCicPp.ppobj obj);*) diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 6b5dfca61..b53d6ea3f 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -628,7 +628,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) = match obj with | CicNotationPt.Inductive (_,(name,_,_,_)::_) | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind" - | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con" + | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con" | CicNotationPt.Inductive _ -> assert false in UriManager.uri_of_string (baseuri ^ "/" ^ name) @@ -770,7 +770,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = match obj with | CicNotationPt.Inductive (_,(name,_,_,_)::_) | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind" - | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con" + | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con" | CicNotationPt.Inductive _ -> assert false in UriManager.uri_of_string (baseuri ^ "/" ^ name) diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 2fbfe4179..0fc42291d 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -95,7 +95,7 @@ let mk_rec_corec ind_kind defs loc = else `MutualDefinition in - (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body)))) + (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular)) let nmk_rec_corec ind_kind defs loc = let loc,t = mk_rec_corec ind_kind defs loc in @@ -797,12 +797,12 @@ EXTEND IDENT "nqed" -> G.NQed loc | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - G.NObj (loc, N.Theorem (nflavour, name, typ, body)) + G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular)) | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); body = term -> - G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body)) + G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular)) | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term -> - G.NObj (loc, N.Theorem (`Axiom, name, typ, None)) + G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular)) | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ; paramspec = OPT inverter_param_list ; outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> @@ -856,16 +856,16 @@ EXTEND typ = term; SYMBOL <:unicode> ; newname = IDENT -> G.Obj (loc, N.Theorem - (`Variant,name,typ,Some (N.Ident (newname, None)))) + (`Variant,name,typ,Some (N.Ident (newname, None)), `Regular)) | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - G.Obj (loc, N.Theorem (flavour, name, typ, body)) + G.Obj (loc, N.Theorem (flavour, name, typ, body,`Regular)) | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); body = term -> G.Obj (loc, - N.Theorem (flavour, name, N.Implicit `JustOne, Some body)) + N.Theorem (flavour, name, N.Implicit `JustOne, Some body,`Regular)) | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term -> - G.Obj (loc, N.Theorem (`Axiom, name, typ, None)) + G.Obj (loc, N.Theorem (`Axiom, name, typ, None, `Regular)) | LETCOREC ; defs = let_defs -> mk_rec_corec `CoInductive defs loc | LETREC ; defs = let_defs -> diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index ff74d233a..1e88c3714 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -435,7 +435,7 @@ let interpretate_obj 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 - | CicNotationPt.Theorem (flavour, name, ty, bo) -> + | CicNotationPt.Theorem (flavour, name, ty, bo, pragma) -> let ty' = interpretate_term ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty @@ -444,11 +444,11 @@ let interpretate_obj uri, height, [], [], (match bo,flavour with | None,`Axiom -> - let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in + let attrs = `Provided, new_flavour_of_flavour flavour, pragma in NCic.Constant ([],name,None,ty',attrs) | Some _,`Axiom -> assert false | None,_ -> - let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in + let attrs = `Provided, new_flavour_of_flavour flavour, pragma in NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs) | Some bo,_ -> (match bo with @@ -485,14 +485,14 @@ let interpretate_obj ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body)) defs in - let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in + let attrs = `Provided, new_flavour_of_flavour flavour, pragma in NCic.Fixpoint (inductive,inductiveFuns,attrs) | bo -> let bo = interpretate_term ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo in - let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in + let attrs = `Provided, new_flavour_of_flavour flavour, pragma in NCic.Constant ([],name,Some bo,ty',attrs))) | CicNotationPt.Inductive (params,tyl) -> let context,params = diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 33677cb42..f608acc15 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -255,6 +255,35 @@ let ppsubst ~formatter ~metasenv subst = ppsubst ~formatter ~metasenv ~subst subst ;; +let string_of_generated = function + | `Generated -> "Generated" + | `Provided -> "Provided" +;; + +let string_of_flavour = function + | `Definition -> "Definition" + | `Fact -> "Fact" + | `Lemma -> "Lemma" + | `Theorem -> "Theorem" + | `Corollary -> "Corollary" + | `Example -> "Example" +;; + +let string_of_pragma = function + | `Coercion _arity -> "Coercion _" + | `Elim _sort -> "Elim _" + | `Projection -> "Projection" + | `InversionPrinciple -> "InversionPrinciple" + | `Variant -> "Variant" + | `Local -> "Local" + | `Regular -> "Regular" +;; + +let string_of_fattrs (g,f,p) = + String.concat "," + [ string_of_generated g; string_of_flavour f; string_of_pragma p ] +;; + let ppobj ~formatter (u,_,metasenv, subst, o) = F.fprintf formatter "metasenv:\n"; ppmetasenv ~formatter ~subst metasenv; @@ -263,7 +292,7 @@ let ppobj ~formatter (u,_,metasenv, subst, o) = (*ppsubst subst ~formatter ~metasenv;*) F.fprintf formatter "..."; F.fprintf formatter "\n"; match o with - | NCic.Fixpoint (b, fl, _) -> + | NCic.Fixpoint (b, fl, attrs) -> F.fprintf formatter "{%s}@\n@[" (NUri.string_of_uri u); F.fprintf formatter "@[%s"(if b then "let rec " else "let corec "); HExtlib.list_iter_sep @@ -274,7 +303,8 @@ let ppobj ~formatter (u,_,metasenv, subst, o) = F.fprintf formatter "@]@;@[:=@;"; ppterm ~formatter ~metasenv ~subst ~context:[] ~inside_fix:true bo; F.fprintf formatter "@]") fl; - F.fprintf formatter "@]" + F.fprintf formatter "@; %s" (string_of_fattrs attrs); + F.fprintf formatter "@]" | NCic.Inductive (b, leftno,tyl, _) -> F.fprintf formatter "{%s} with %d fixed params@\n@[@[%s" (NUri.string_of_uri u) leftno diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli index c260e8c61..3b4cffb6d 100644 --- a/helm/software/components/ng_kernel/nCicPp.mli +++ b/helm/software/components/ng_kernel/nCicPp.mli @@ -36,3 +36,34 @@ val ppmetasenv: val ppsubst: metasenv:NCic.metasenv -> NCic.substitution -> string val ppobj: NCic.obj -> string + +(* variants that use a formatter +module Format : sig + val ppterm: + formatter:Format.formatter -> + context:NCic.context -> + subst:NCic.substitution -> + metasenv:NCic.metasenv -> + ?margin:int -> + ?inside_fix:bool -> + NCic.term -> unit + + val ppcontext: + ?sep:string -> + formatter:Format.formatter -> + subst:NCic.substitution -> + metasenv:NCic.metasenv -> + NCic.context -> unit + + val ppmetasenv: + formatter:Format.formatter -> + subst:NCic.substitution -> NCic.metasenv -> unit + + val ppsubst: + formatter:Format.formatter -> + metasenv:NCic.metasenv -> NCic.substitution -> unit + + val ppobj: + formatter:Format.formatter -> NCic.obj -> unit +end +*) diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index 1e7432724..771568018 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -168,17 +168,20 @@ let clean_or_fix_dependent_abstrations ctx t = aux (List.map fst ctx) t ;; -let rec fire_projection_redex () = function +let rec fire_projection_redex on_args = function | C.Meta _ as t -> t | C.Appl(C.Const(Ref.Ref(_,Ref.Fix(fno,rno,_)) as r)::args as ol)as ot-> - let l = List.map (fire_projection_redex ()) ol in + let l= if on_args then List.map (fire_projection_redex true) ol else ol in let t = if l == ol then ot else C.Appl l in let ifl,(_,_,pragma),_ = NCicEnvironment.get_checked_fixes_or_cofixes r in let conclude () = - let l' = HExtlib.sharing_map (fire_projection_redex ()) l in - if l == l' then t else C.Appl l' + if on_args then + let l' = HExtlib.sharing_map (fire_projection_redex true) l in + if l == l' then t else C.Appl l' + else + t (* ot is the same *) in - if (*pragma <> `Projection ||*) List.length args <= rno then conclude () + if pragma <> `Projection || List.length args <= rno then conclude () else (match List.nth args rno with | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) -> @@ -187,15 +190,18 @@ let rec fire_projection_redex () = function (match NCicReduction.head_beta_reduce ~delta:max_int t with | C.Match (_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat])-> let _,kargs = HExtlib.split_nth leftno kargs in - NCicReduction.head_beta_reduce - ~delta:max_int (C.Appl (pat :: kargs)) + fire_projection_redex false + (NCicReduction.head_beta_reduce + ~delta:max_int (C.Appl (pat :: kargs))) | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat]) :: args) -> let _,kargs = HExtlib.split_nth leftno kargs in - NCicReduction.head_beta_reduce - ~delta:max_int (C.Appl (pat :: kargs @ args)) + fire_projection_redex false + (NCicReduction.head_beta_reduce + ~delta:max_int (C.Appl (pat :: kargs @ args))) | _ -> conclude ()) | _ -> conclude ()) - | t -> NCicUtils.map (fun _ _ -> ()) () fire_projection_redex t + | t when on_args -> NCicUtils.map (fun _ x -> x) true fire_projection_redex t + | t -> t ;; let apply_subst ?(fix_projections=false) subst context t = @@ -217,7 +223,7 @@ let apply_subst ?(fix_projections=false) subst context t = apply_subst subst () (NCicSubstitution.lift n t)) l)))) | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t in - (if fix_projections then fire_projection_redex () else fun x -> x) + (if fix_projections then fire_projection_redex true else fun x -> x) (clean_or_fix_dependent_abstrations context (apply_subst subst () t)) ;; diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml index 4117c4ffa..b493edb6a 100644 --- a/helm/software/components/ng_tactics/nCicElim.ml +++ b/helm/software/components/ng_tactics/nCicElim.ml @@ -42,7 +42,7 @@ let mk_appl = | l -> CicNotationPt.Appl l ;; -let mk_elim uri leftno it (outsort,suffix) = +let mk_elim uri leftno it (outsort,suffix) pragma = let _,ind_name,ty,cl = it in let srec_name = ind_name ^ "_" ^ suffix in let rec_name = mk_id srec_name in @@ -150,7 +150,8 @@ let mk_elim uri leftno it (outsort,suffix) = (CicNotationPres.mpres_of_box boxml))); *) CicNotationPt.Theorem - (`Definition,srec_name,CicNotationPt.Implicit `JustOne,Some res) + (`Definition,srec_name, + CicNotationPt.Implicit `JustOne,Some res,pragma) ;; let ast_of_sort s = @@ -177,7 +178,7 @@ let ast_of_sort s = let mk_elims (uri,_,_,_,obj) = match obj with NCic.Inductive (true,leftno,[itl],_) -> - List.map (fun s -> mk_elim uri leftno itl (ast_of_sort s)) + List.map (fun s -> mk_elim uri leftno itl (ast_of_sort s) (`Elim s)) (NCic.Prop:: List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ())) | _ -> [] @@ -290,7 +291,7 @@ let mk_projection leftno tyname consname consty (projname,_,_) i = 80 (CicNotationPres.render (fun _ -> None) (TermContentPres.pp_ast res)));*) CicNotationPt.Theorem - (`Definition,projname,CicNotationPt.Implicit `JustOne,Some res) + (`Definition,projname,CicNotationPt.Implicit `JustOne,Some res,`Projection) ;; let mk_projections (_,_,_,_,obj) = diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml index a93e7f513..f70999315 100644 --- a/helm/software/components/ng_tactics/nInversion.ml +++ b/helm/software/components/ng_tactics/nInversion.ml @@ -130,7 +130,8 @@ let mk_inverter name it leftno ?selection outsort status baseuri = let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri (baseuri ^ name ^ ".def", - 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some (CicNotationPt.Implicit (`Tagged "inv")))) in + 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some + (CicNotationPt.Implicit (`Tagged "inv")),`Regular)) in let uri,height,nmenv,nsubst,nobj = theorem in let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in let status = status#set_obj theorem in diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml index 244cd1d72..c63fca741 100644 --- a/helm/software/components/tptp_grafite/tptp2grafite.ml +++ b/helm/software/components/tptp_grafite/tptp2grafite.ml @@ -354,7 +354,7 @@ let convert_ast ng statements context = function (mk_ident universe,Some (PT.Sort (`Type (CicUniv.fresh ())))), convert_formula fv false context f) in - let o = PT.Theorem (`Theorem,name,f,None) in + let o = PT.Theorem (`Theorem,name,f,None,`Regular) in (statements @ [ GA.Executable(floc,GA.Command(floc, (*if ng then GA.NObj (floc,o) else*) GA.Obj(floc,o))); ] @