diff options
| -rw-r--r-- | contrib/interface/xlate.ml | 9 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 12 | ||||
| -rw-r--r-- | toplevel/command.ml | 54 | ||||
| -rw-r--r-- | toplevel/command.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
6 files changed, 69 insertions, 13 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index af68c7cf91..fdaa2c5964 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1940,12 +1940,17 @@ let rec xlate_vernac = | VernacScheme [] -> xlate_error "induction scheme" | VernacScheme (lm :: lmi) -> let strip_ind = function - | ((_,id), InductionScheme (depstr, inde, sort)) -> + | (Some (_,id), InductionScheme (depstr, inde, sort)) -> CT_scheme_spec (xlate_ident id, xlate_dep depstr, CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde), xlate_sort sort) - | ((_,id), EqualityScheme _) -> xlate_error "TODO: Scheme Equality" in + | (None, InductionScheme (depstr, inde, sort)) -> + CT_scheme_spec + (xlate_ident (id_of_string ""), xlate_dep depstr, + CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde), + xlate_sort sort) + | (_, EqualityScheme _) -> xlate_error "TODO: Scheme Equality" in CT_ind_scheme (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi)) | VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme" diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c61dfbf63d..b7cde536f7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -285,7 +285,8 @@ GEXTEND Gram ; (* Inductive schemes *) scheme: - [ [ id = identref; ":="; kind = scheme_kind -> (id,kind) ] ] + [ [ kind = scheme_kind -> (None,kind) + | id = identref; ":="; kind = scheme_kind -> (Some id,kind) ] ] ; scheme_kind: [ [ IDENT "Induction"; "for"; ind = global; diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index d44e225b50..4bb7d27520 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -279,15 +279,21 @@ let pr_binders_arg = let pr_and_type_binders_arg bl = pr_binders_arg bl -let pr_onescheme (id,schem) = +let pr_onescheme (idop,schem) = match schem with | InductionScheme (dep,ind,s) -> - hov 0 (pr_lident id ++ str" :=") ++ spc() ++ + (match idop with + | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() + | None -> spc () + ) ++ hov 0 ((if dep then str"Induction for" else str"Minimality for") ++ spc() ++ pr_reference ind) ++ spc() ++ hov 0 (str"Sort" ++ spc() ++ pr_rawsort s) | EqualityScheme ind -> - hov 0 (pr_lident id ++ str" :=") ++ spc() ++ + (match idop with + | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() + | None -> spc() + ) ++ hov 0 (str"Equality for") ++ spc() ++ pr_reference ind diff --git a/toplevel/command.ml b/toplevel/command.ml index d634957ca9..1b8c537b4b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -671,13 +671,54 @@ let build_corecursive l b = interp_recursive IsCoFixpoint fixl b (* 3d| Schemes *) -let rec split_scheme = function +let rec split_scheme l = + let env = Global.env() in + match l with | [] -> [],[] - | (id,t)::q -> let l1,l2 = split_scheme q in + | (Some id,t)::q -> let l1,l2 = split_scheme q in ( match t with | InductionScheme (x,y,z) -> ((id,x,y,z)::l1),l2 - | EqualityScheme x -> l1,((id,x)::l2) + | EqualityScheme x -> l1,(x::l2) ) +(* + if no name has been provided, we build one from the types of the ind +requested +*) + | (None,t)::q -> + let l1,l2 = split_scheme q in + ( match t with + | InductionScheme (x,y,z) -> + let ind = mkInd (Nametab.global_inductive y) in + let sort_of_ind = family_of_sort (Typing.sort_of env Evd.empty ind) +in + let z' = family_of_sort (interp_sort z) in + let suffix = ( + match sort_of_ind with + | InProp -> + if x then (match z' with + | InProp -> "_ind_nodep" + | InSet -> "_rec_nodep" + | InType -> "_rect_nodep") + else ( match z' with + | InProp -> "_ind" + | InSet -> "_rec" + | InType -> "_rect" ) + | _ -> + if x then (match z' with + | InProp -> "_ind" + | InSet -> "_rec" + | InType -> "_rect" ) + else (match z' with + | InProp -> "_ind_nodep" + | InSet -> "_rec_nodep" + | InType -> "_rect_nodep") + ) in + let newid = (string_of_id (Pcoq.coerce_global_to_id y))^suffix in + let newref = (dummy_loc,id_of_string newid) in + ((newref,x,y,z)::l1),l2 + | EqualityScheme x -> l1,(x::l2) + ) + let build_induction_scheme lnamedepindsort = let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort @@ -707,13 +748,16 @@ let build_induction_scheme lnamedepindsort = let build_scheme l = let ischeme,escheme = split_scheme l in +(* we want 1 kind of scheme at a time so we check if the user +tried to declare different schemes at once *) if (ischeme <> []) && (escheme <> []) then error "Do not declare equality and induction scheme at the same time." else ( if ischeme <> [] then build_induction_scheme ischeme; - List.iter ( fun (_,eq)-> let ind = Nametab.global_inductive eq -(* vsiles :This will be replace with the boolean when it will be commited *) + List.iter ( fun indname -> + let ind = Nametab.global_inductive indname +(* vsiles :This will be replace with the boolean eq when it will be commited *) in Pp.msgnl (print_constr (mkInd ind)) ) escheme ) diff --git a/toplevel/command.mli b/toplevel/command.mli index 4bda8a362c..3f7e502850 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -52,7 +52,7 @@ val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit -val build_scheme : (identifier located * scheme ) list -> unit +val build_scheme : (identifier located option * scheme ) list -> unit val build_combined_scheme : identifier located -> identifier located list -> unit diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index efdb710c2a..c1a8625bce 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -203,7 +203,7 @@ type vernac_expr = | VernacInductive of inductive_flag * (inductive_expr * decl_notation) list | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool - | VernacScheme of (lident * scheme) list + | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list (* Gallina extensions *) |