From fdfdbcda1983c229779a09d77ead5033202bfbc7 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 15 May 2017 12:17:14 +0200 Subject: romega/const_omega : a few improvements (less try with, no gen equality) --- plugins/romega/const_omega.ml | 145 +++++++++++++++++++++--------------------- 1 file changed, 74 insertions(+), 71 deletions(-) (limited to 'plugins/romega') diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index f7eab17df..d7faaac96 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -10,10 +10,10 @@ let module_refl_name = "ReflOmegaCore" let module_refl_path = ["Coq"; "romega"; module_refl_name] type result = - Kvar of string - | Kapp of string * Term.constr list - | Kimp of Term.constr * Term.constr - | Kufo;; + | Kvar of string + | Kapp of string * Term.constr list + | Kimp of Term.constr * Term.constr + | Kufo let meaningful_submodule = [ "Z"; "N"; "Pos" ] @@ -30,19 +30,17 @@ let string_of_global r = let destructurate t = let c, args = Term.decompose_app t in match Term.kind_of_term c, args with - | Term.Const (sp,_), args -> - Kapp (string_of_global (Globnames.ConstRef sp), args) - | Term.Construct (csp,_) , args -> - Kapp (string_of_global (Globnames.ConstructRef csp), args) - | Term.Ind (isp,_), args -> - Kapp (string_of_global (Globnames.IndRef isp), args) - | Term.Var id,[] -> Kvar(Names.Id.to_string id) - | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) - | Term.Prod (Names.Name _,_,_),[] -> - CErrors.error "Omega: Not a quantifier-free goal" - | _ -> Kufo - -exception Destruct + | Term.Const (sp,_), args -> + Kapp (string_of_global (Globnames.ConstRef sp), args) + | Term.Construct (csp,_) , args -> + Kapp (string_of_global (Globnames.ConstructRef csp), args) + | Term.Ind (isp,_), args -> + Kapp (string_of_global (Globnames.IndRef isp), args) + | Term.Var id, [] -> Kvar(Names.Id.to_string id) + | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) + | _ -> Kufo + +exception DestConstApp let dest_const_apply t = let f,args = Term.decompose_app t in @@ -51,8 +49,8 @@ let dest_const_apply t = | Term.Const (sp,_) -> Globnames.ConstRef sp | Term.Construct (csp,_) -> Globnames.ConstructRef csp | Term.Ind (isp,_) -> Globnames.IndRef isp - | _ -> raise Destruct - in Nametab.basename_of_global ref, args + | _ -> raise DestConstApp + in Nametab.basename_of_global ref, args let logic_dir = ["Coq";"Logic";"Decidable"] @@ -262,17 +260,15 @@ type parse_rel = | Riff of Term.constr * Term.constr | Rother -let parse_logic_rel c = - try match destructurate c with - | Kapp("True",[]) -> Rtrue - | Kapp("False",[]) -> Rfalse - | Kapp("not",[t]) -> Rnot t - | Kapp("or",[t1;t2]) -> Ror (t1,t2) - | Kapp("and",[t1;t2]) -> Rand (t1,t2) - | Kimp(t1,t2) -> Rimp (t1,t2) - | Kapp("iff",[t1;t2]) -> Riff (t1,t2) - | _ -> Rother - with e when Logic.catchable_exception e -> Rother +let parse_logic_rel c = match destructurate c with + | Kapp("True",[]) -> Rtrue + | Kapp("False",[]) -> Rfalse + | Kapp("not",[t]) -> Rnot t + | Kapp("or",[t1;t2]) -> Ror (t1,t2) + | Kapp("and",[t1;t2]) -> Rand (t1,t2) + | Kimp(t1,t2) -> Rimp (t1,t2) + | Kapp("iff",[t1;t2]) -> Riff (t1,t2) + | _ -> Rother (* Binary numbers *) @@ -321,20 +317,26 @@ let mult = lazy (z_constant "Z.mul") let opp = lazy (z_constant "Z.opp") let minus = lazy (z_constant "Z.sub") -let recognize t = +let recognize_pos t = let rec loop t = let f,l = dest_const_apply t in match Names.Id.to_string f,l with - "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t)) - | "xO",[t] -> Bigint.mult Bigint.two (loop t) - | "xH",[] -> Bigint.one - | _ -> failwith "not a number" in - let f,l = dest_const_apply t in + | "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t)) + | "xO",[t] -> Bigint.mult Bigint.two (loop t) + | "xH",[] -> Bigint.one + | _ -> raise DestConstApp + in + try Some (loop t) with DestConstApp -> None + +let recognize_Z t = + try + let f,l = dest_const_apply t in match Names.Id.to_string f,l with - "Zpos",[t] -> loop t - | "Zneg",[t] -> Bigint.neg (loop t) - | "Z0",[] -> Bigint.zero - | _ -> failwith "not a number";; + | "Zpos",[t] -> recognize_pos t + | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos t) + | "Z0",[] -> Some Bigint.zero + | _ -> None + with DestConstApp -> None let mk_Z n = if Bigint.equal n Bigint.zero then Lazy.force coq_Z0 @@ -346,38 +348,39 @@ let mk_Z n = let mk = mk_Z let parse_term t = - try match destructurate t with - | Kapp("Z.add",[t1;t2]) -> Tplus (t1,t2) - | Kapp("Z.sub",[t1;t2]) -> Tminus (t1,t2) - | Kapp("Z.mul",[t1;t2]) -> Tmult (t1,t2) - | Kapp("Z.opp",[t]) -> Topp t - | Kapp("Z.succ",[t]) -> Tsucc t - | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one)) - | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> - (try Tnum (recognize t) with e when CErrors.noncritical e -> Tother) - | _ -> Tother - with e when Logic.catchable_exception e -> Tother - -let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c + match destructurate t with + | Kapp("Z.add",[t1;t2]) -> Tplus (t1,t2) + | Kapp("Z.sub",[t1;t2]) -> Tminus (t1,t2) + | Kapp("Z.mul",[t1;t2]) -> Tmult (t1,t2) + | Kapp("Z.opp",[t]) -> Topp t + | Kapp("Z.succ",[t]) -> Tsucc t + | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one)) + | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> + (match recognize_Z t with Some t -> Tnum t | None -> Tother) + | _ -> Tother + +let pf_nf gl c = + EConstr.Unsafe.to_constr + (Tacmach.New.pf_apply Tacred.simpl gl (EConstr.of_constr c)) let parse_rel gl t = - try match destructurate t with - | Kapp("eq",[typ;t1;t2]) - when destructurate (EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr typ))) = Kapp("Z",[]) -> Req (t1,t2) - | Kapp("Zne",[t1;t2]) -> Rne (t1,t2) - | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2) - | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2) - | Kapp("Z.ge",[t1;t2]) -> Rge (t1,t2) - | Kapp("Z.gt",[t1;t2]) -> Rgt (t1,t2) - | _ -> parse_logic_rel t - with e when Logic.catchable_exception e -> Rother - -let is_scalar t = - let rec aux t = match destructurate t with - | Kapp(("Z.add"|"Z.sub"|"Z.mul"),[t1;t2]) -> aux t1 && aux t2 - | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t - | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true - | _ -> false in - try aux t with e when CErrors.noncritical e -> false + match destructurate t with + | Kapp("eq",[typ;t1;t2]) -> + (match destructurate (pf_nf gl typ) with + | Kapp("Z",[]) -> Req (t1,t2) + | _ -> Rother) + | Kapp("Zne",[t1;t2]) -> Rne (t1,t2) + | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2) + | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2) + | Kapp("Z.ge",[t1;t2]) -> Rge (t1,t2) + | Kapp("Z.gt",[t1;t2]) -> Rgt (t1,t2) + | _ -> parse_logic_rel t + +let rec is_scalar t = + match destructurate t with + | Kapp(("Z.add"|"Z.sub"|"Z.mul"),[t1;t2]) -> is_scalar t1 && is_scalar t2 + | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> is_scalar t + | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> Option.has_some (recognize_Z t) + | _ -> false end -- cgit v1.2.3