diff options
Diffstat (limited to 'plugins/romega/const_omega.ml')
-rw-r--r-- | plugins/romega/const_omega.ml | 65 |
1 files changed, 38 insertions, 27 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index fb45e816..21b0f78b 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -1,7 +1,7 @@ (************************************************************************* PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D + Author: Pierre Crégut - France Télécom R&D Licence : LGPL version 2.1 *************************************************************************) @@ -19,27 +19,27 @@ let meaningful_submodule = [ "Z"; "N"; "Pos" ] let string_of_global r = let dp = Nametab.dirpath_of_global r in - let prefix = match Names.repr_dirpath dp with + let prefix = match Names.DirPath.repr dp with | [] -> "" | m::_ -> - let s = Names.string_of_id m in - if List.mem s meaningful_submodule then s^"." else "" + let s = Names.Id.to_string m in + if Util.String.List.mem s meaningful_submodule then s^"." else "" in - prefix^(Names.string_of_id (Nametab.basename_of_global r)) + prefix^(Names.Id.to_string (Nametab.basename_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 (Libnames.ConstRef sp), args) - | Term.Construct csp , args -> - Kapp (string_of_global (Libnames.ConstructRef csp), args) - | Term.Ind isp, args -> - Kapp (string_of_global (Libnames.IndRef isp), args) - | Term.Var id,[] -> Kvar(Names.string_of_id id) + | 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 _,_,_),[] -> - Util.error "Omega: Not a quantifier-free goal" + Errors.error "Omega: Not a quantifier-free goal" | _ -> Kufo exception Destruct @@ -48,9 +48,9 @@ let dest_const_apply t = let f,args = Term.decompose_app t in let ref = match Term.kind_of_term f with - | Term.Const sp -> Libnames.ConstRef sp - | Term.Construct csp -> Libnames.ConstructRef csp - | Term.Ind isp -> Libnames.IndRef isp + | 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 @@ -71,7 +71,6 @@ let z_constant = Coqlib.gen_constant_in_modules "Omega" z_module let bin_constant = Coqlib.gen_constant_in_modules "Omega" bin_module (* Logic *) -let coq_eq = lazy(init_constant "eq") let coq_refl_equal = lazy(init_constant "eq_refl") let coq_and = lazy(init_constant "and") let coq_not = lazy(init_constant "not") @@ -211,19 +210,31 @@ let rec mk_nat = function (* Lists *) -let coq_cons = lazy (constant "cons") -let coq_nil = lazy (constant "nil") +let mkListConst c = + let r = + Coqlib.gen_reference "" ["Init";"Datatypes"] c + in + let inst = + if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|] + else fun _ -> Univ.Instance.empty + in + fun u -> Term.mkConstructU (Globnames.destConstructRef r, inst u) + +let coq_cons univ typ = Term.mkApp (mkListConst "cons" univ, [|typ|]) +let coq_nil univ typ = Term.mkApp (mkListConst "nil" univ, [|typ|]) -let mk_list typ l = +let mk_list univ typ l = let rec loop = function - | [] -> - Term.mkApp (Lazy.force coq_nil, [|typ|]) + | [] -> coq_nil univ typ | (step :: l) -> - Term.mkApp (Lazy.force coq_cons, [|typ; step; loop l |]) in + Term.mkApp (coq_cons univ typ, [| step; loop l |]) in loop l -let mk_plist l = mk_list Term.mkProp l +let mk_plist = + let type1lev = Universes.new_univ_level (Global.current_dirpath ()) in + fun l -> mk_list type1lev Term.mkProp l +let mk_list = mk_list Univ.Level.set let mk_shuffle_list l = mk_list (Lazy.force coq_t_fusion) l @@ -297,13 +308,13 @@ let coq_Zneg = lazy (bin_constant "Zneg") let recognize t = let rec loop t = let f,l = dest_const_apply t in - match Names.string_of_id f,l with + 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 - match Names.string_of_id f,l with + match Names.Id.to_string f,l with "Zpos",[t] -> loop t | "Zneg",[t] -> Bigint.neg (loop t) | "Z0",[] -> Bigint.zero @@ -353,7 +364,7 @@ let parse_rel gl t = 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.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 |