diff options
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/interface/xlate.ml | 1 | ||||
-rw-r--r-- | contrib/subtac/FixSub.v | 10 | ||||
-rw-r--r-- | contrib/subtac/Utils.v | 4 | ||||
-rw-r--r-- | contrib/subtac/subtac_cases.ml | 31 | ||||
-rw-r--r-- | contrib/subtac/subtac_coercion.ml | 6 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.ml | 6 |
6 files changed, 38 insertions, 20 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 522419030..bf5aed32e 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1929,6 +1929,7 @@ let rec xlate_vernac = xlate_sort sort) in CT_ind_scheme (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi)) + | VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme" | VernacSyntacticDefinition (id, c, false, _) -> CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt None) | VernacSyntacticDefinition (id, c, true, _) -> diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v index 0016bfdaf..46121ff18 100644 --- a/contrib/subtac/FixSub.v +++ b/contrib/subtac/FixSub.v @@ -2,13 +2,13 @@ Require Import Wf. Require Import Coq.subtac.Utils. Section Well_founded. - Variable A : Set. + Variable A : Type. Variable R : A -> A -> Prop. Hypothesis Rwf : well_founded R. Section Acc. - Variable P : A -> Set. + Variable P : A -> Type. Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. @@ -20,7 +20,7 @@ Section Well_founded. End Acc. Section FixPoint. - Variable P : A -> Set. + Variable P : A -> Type. Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. @@ -75,13 +75,13 @@ Require Import Wf_nat. Require Import Lt. Section Well_founded_measure. -Variable A : Set. +Variable A : Type. Variable f : A -> nat. Definition R := fun x y => f x < f y. Section FixPoint. -Variable P : A -> Set. +Variable P : A -> Type. Variable F_sub : forall x:A, (forall y: { y : A | f y < f x }, P (proj1_sig y)) -> P x. diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index 34d9f6206..30ecc8ff7 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -66,5 +66,9 @@ Ltac destruct_call f := end. Extraction Inline proj1_sig. +Extract Inductive unit => "unit" [ "()" ]. +Extract Inductive bool => "bool" [ "true" "false" ]. +Extract Inductive sumbool => "bool" [ "true" "false" ]. +Extract Inductive prod => "" [ "" ]. Require Export ProofIrrelevance. diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index cea3fbf51..fd93a115a 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -1187,6 +1187,7 @@ let group_equations pb ind current cstrs mat = let rec generalize_problem pb = function | [] -> pb | i::l -> + trace (str"Generalizing problem"); let d = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in let pb' = generalize_problem pb l in let tomatch = lift_tomatch_stack 1 pb'.tomatch in @@ -1272,10 +1273,11 @@ let build_branch current deps pb eqns const_info = let cur_alias = lift (List.length sign) current in let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in - - sign, + let env' = push_rels sign pb.env in + let pred' = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in + sign, { pb with - env = push_rels sign pb.env; + env = env'; tomatch = List.rev_append currents tomatch; pred = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred; history = history; @@ -1640,14 +1642,13 @@ let constr_of_pat env isevars ty pat = let app = applistc cstr (List.map (lift (List.length args)) params) in let app = applistc app args in (* trace (str "New pattern: " ++ Printer.pr_cases_pattern pat'); *) + let alname = if alias <> Anonymous then alias else Name (id_of_string "anon") in + let al = alname, Some (mkRel 1), lift 1 ty in if alias <> Anonymous then pat', (alias, Some app, ty) :: sign, lift 1 app, n + 1 else pat', sign, app, n in let pat', sign, y, z = typ env ty pat in -(* let prod = it_mkProd_or_LetIn y sign in *) -(* trace (str "Pattern: " ++ Printer.pr_cases_pattern pat ++ str " becomes constr : " ++ *) -(* my_print_constr env prod); *) pat', (sign, y) let mk_refl typ a = mkApp (Lazy.force eq_refl, [| typ; a |]) @@ -1766,9 +1767,12 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs = * A type constraint but no annotation case: it is assumed non dependent. *) -let prepare_predicate_from_tycon loc typing_fun isevars env tomatchs sign tycon = +let prepare_predicate_from_tycon loc typing_fun isevars env tomatchs arsign tycon = (* We extract the signature of the arity *) - let arsign = extract_arity_signature env tomatchs sign in + List.iter + (fun arsign -> + trace (str "arity signature: " ++ my_print_rel_context env arsign)) + arsign; (* let env = List.fold_right push_rels arsign env in *) let allnames = List.rev (List.map (List.map pi1) arsign) in let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in @@ -1823,8 +1827,12 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e None -> let lets, matx = constrs_of_pats typing_fun tycon env isevars matx tomatchs in let matx = List.rev matx in - let env = push_rels lets env in let len = List.length lets in + let sign = + let arsign = extract_arity_signature env tomatchs (List.map snd tomatchl) in + List.map (lift_rel_context len) arsign + in + let env = push_rels lets env in let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in let tycon = lift_tycon len tycon in let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in @@ -1832,9 +1840,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e (* We build the elimination predicate if any and check its consistency *) (* with the type of arguments to match *) - let tmsign = List.map snd tomatchl in - let pred, opred = prepare_predicate_from_tycon loc typing_fun isevars env tomatchs tmsign tycon in - + let pred, opred = prepare_predicate_from_tycon loc typing_fun isevars env tomatchs sign tycon in (* We push the initial terms to match and push their alias to rhs' envs *) (* names of aliases will be recovered from patterns (hence Anonymous here) *) let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in @@ -1883,5 +1889,6 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e (* We check for unused patterns *) List.iter (check_unused_pattern env) matx; inh_conv_coerce_to_tycon loc env isevars j tycon + end diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 16363ac67..f75dd5c39 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -244,15 +244,17 @@ module Coercion = struct coerce (subst1 hdy restT) (succ i) (fun x -> eq_app (co x)) else co in - if Array.length l = Array.length l' then + if Array.length l = Array.length l' then ( + trace (str"Inserting coercion at application"); Some (coerce lam_type 0 (fun x -> x)) - else subco () + ) else subco () | _ -> subco ()) | _, _ -> subco () and subset_coerce env isevars x y = match disc_subset x with Some (u, p) -> + (* trace (str "Inserting projection "); *) let c = coerce_unify env u y in let f x = app_opt c (mkApp ((Lazy.force sig_).proj1, diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 4a1719528..42de8cb89 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -111,8 +111,12 @@ let subst_body prg = subst_deps obls (intset_to (pred (Array.length obls))) prg.prg_body let declare_definition prg = + let body = subst_body prg in + (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++ + my_print_constr (Global.env()) body); + with _ -> ()); let ce = - { const_entry_body = subst_body prg; + { const_entry_body = body; const_entry_type = Some prg.prg_type; const_entry_opaque = false; const_entry_boxed = false} |