diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/subtac/subtac.ml | 2 | ||||
| -rw-r--r-- | contrib/subtac/subtac_cases.ml | 175 | ||||
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 9 | ||||
| -rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 6 |
4 files changed, 134 insertions, 58 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index c144f1f9e..4433239f3 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -158,7 +158,7 @@ let start_proof_and_print env isevars idopt k t hook = let subtac (loc, command) = check_required_library ["Coq";"Init";"Datatypes"]; check_required_library ["Coq";"Init";"Specif"]; - check_required_library ["Coq";"Logic";"JMeq"]; + (* check_required_library ["Coq";"Logic";"JMeq"]; *) require_library "Coq.subtac.FixSub"; require_library "Coq.subtac.Utils"; Subtac_obligations.set_default_tactic diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 7096d439e..83e965d0a 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -138,8 +138,6 @@ type rhs = { rhs_env : env; avoid_ids : identifier list; it : rawconstr; - rhs_lift : int; - c_it : constr; } type equation = @@ -719,9 +717,28 @@ let get_names env sign eqns = let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t)) let push_rels_eqn sign eqn = - trace (str "push_rels_eqn: " ++ my_print_rel_context eqn.rhs.rhs_env sign); - {eqn with rhs = {eqn.rhs with rhs_env = push_rels sign eqn.rhs.rhs_env; - rhs_lift = eqn.rhs.rhs_lift - (List.length sign) } } +(* trace (str "push_rels_eqn: " ++ my_print_rel_context eqn.rhs.rhs_env sign ++ *) +(* str " lift is " ++ int eqn.rhs.rhs_lift ++ *) +(* str " branch is " ++ my_print_constr (fst eqn.rhs.c_orig) (snd eqn.rhs.c_orig)); *) +(* let rhs = eqn.rhs in *) +(* let l, c, s, e = *) +(* List.fold_right *) +(* (fun (na, c, t) (itlift, it, sign, env) -> *) +(* (try trace (str "Pushing decl: " ++ pr_rel_decl env (na, c, t) ++ *) +(* str " lift is " ++ int itlift); *) +(* with _ -> trace (str "error in push_rels_eqn")); *) +(* let env' = push_rel (na, c, t) env in *) +(* match sign with *) +(* [] -> (itlift, lift 1 it, sign, env') *) +(* | (na', c, t) :: sign' -> *) +(* if na' = na then *) +(* (pred itlift, it, sign', env') *) +(* else ( *) +(* trace (str "skipping it"); *) +(* (itlift, liftn 1 itlift it, sign, env'))) *) +(* sign (rhs.rhs_lift, rhs.c_it, eqn.rhs.rhs_sign, eqn.rhs.rhs_env) *) +(* in *) + {eqn with rhs = {eqn.rhs with rhs_env = push_rels sign eqn.rhs.rhs_env; } } let push_rels_eqn_with_names sign eqn = let pats = List.rev (list_firstn (List.length sign) eqn.patterns) in @@ -753,20 +770,9 @@ let build_aliases_context env sigma names allpats pats = let allpats = List.map (fun x -> [x]) allpats in insert env [] [] 0 (List.map (fun _ -> []) allpats) allpats (pats, names) -let insert_aliases_rels rhs sign = - let len = List.length sign in - if len = 0 then rhs - else - { rhs with - rhs_env = push_rels sign rhs.rhs_env; - c_it = liftn len rhs.rhs_lift rhs.c_it } - let insert_aliases_eqn sign eqnnames alias_rest eqn = let thissign = List.map2 (fun na (_,c,t) -> (na,c,t)) eqnnames sign in - trace (str "insert aliases: " ++ my_print_rel_context eqn.rhs.rhs_env thissign); - { eqn with - alias_stack = alias_rest; - rhs = insert_aliases_rels eqn.rhs thissign } + push_rels_eqn thissign { eqn with alias_stack = alias_rest; } let insert_aliases env sigma alias eqns = @@ -1160,8 +1166,9 @@ let group_equations pb ind current cstrs mat = | PatVar (_,name) -> (* This is a default clause that we expand *) for i=1 to Array.length cstrs do - let args = make_anonymous_patvars cstrs.(i-1).cs_nargs in - let rest = {rest with tag = lower_pattern_status rest.tag} in + let n = cstrs.(i-1).cs_nargs in + let args = make_anonymous_patvars n in + let rest = {rest with tag = lower_pattern_status rest.tag } in brs.(i-1) <- (args, rest) :: brs.(i-1) done | PatCstr (loc,((_,i)),args,_) -> @@ -1192,10 +1199,11 @@ let build_leaf pb = let tag, rhs = extract_rhs pb in let tycon = match pb.pred with | None -> anomaly "Predicate not found" - | Some (PrCcl typ) -> typ + | Some (PrCcl typ) -> mk_tycon typ | Some _ -> anomaly "not all parameters of pred have been consumed" in - trace (str "In build leaf: env is: " ++ my_print_env rhs.rhs_env); - tag, { uj_val = rhs.c_it; uj_type = tycon } + (try trace (str "In build leaf: env is: " ++ my_print_env rhs.rhs_env) + with _ -> trace (str "Error in build leaf")); + tag, pb.typing_function tycon rhs.rhs_env rhs.it (* Building the sub-problem when all patterns are variables *) let shift_problem (current,t) pb = @@ -1257,7 +1265,6 @@ let build_branch current deps pb eqns const_info = 1 typs' (List.rev dep_sign) in let sign = List.map (fun (na,t) -> mkDeclTomatch na t) typs' in - debug 4 (str "In build branch, add rel context: " ++ Subtac_utils.my_print_rel_context pb.env sign); let ind = appvect ( applist (mkInd (inductive_of_constructor const_info.cs_cstr), @@ -1393,8 +1400,6 @@ let matx_of_eqns env tomatchl eqns = { rhs_env = env; avoid_ids = ids@(ids_of_named_context (named_context env)); it = initial_rhs; - rhs_lift = 0; - c_it = Obj.magic 0; } in { patterns = initial_lpat; tag = RegularPat; @@ -1604,10 +1609,18 @@ let list_mapi f l = in aux 0 l let constr_of_pat env isevars ty pat = - let rec typ env ty = function - | PatVar (_,name) -> - [name, None, ty], mkRel 1, 1 - | PatCstr (_,((_, i) as cstr),args,alias) -> + let rec typ env ty pat = +(* trace (str "Typing pattern " ++ Printer.pr_cases_pattern pat ++ str " in env " ++ *) +(* print_env env); *) + match pat with + | PatVar (l,name) -> + let name = match name with + Name n -> name + | Anonymous -> Name (id_of_string "wildcard") + in +(* trace (str "Treating pattern variable " ++ str (string_of_id (id_of_name name))); *) + PatVar (l, name), [name, None, ty], mkRel 1, 1 + | PatCstr (l,((_, i) as cstr),args,alias) -> let ind = inductive_of_constructor cstr in let IndType (indf, realargs) = find_rectype env (Evd.evars_of !isevars) ty in let ind, params = dest_ind_family indf in @@ -1615,40 +1628,77 @@ let constr_of_pat env isevars ty pat = let ci = cstrs.(i-1) in let nb_args_constr = ci.cs_nargs in assert(nb_args_constr = List.length args); - let args, sign, env, n = - List.fold_left2 - (fun (args, sign, env, n) (na, c, t) ua -> - let sign', arg', n' = typ env t ua in + let patargs, args, sign, env, n = + List.fold_right2 + (fun (na, c, t) ua (patargs, args, sign, env, n) -> + let pat', sign', arg', n' = typ env t ua in let args' = arg' :: List.map (lift n') args in let env' = push_rels sign' env in - (args', sign' @ sign, env', n' + n)) - ([], [], env, 0) ci.cs_args (List.rev args) + (pat' :: patargs, args', sign' @ sign, env', n' + n)) + ci.cs_args (List.rev args) ([], [], [], env, 0) in + let args = List.rev args in + let patargs = List.rev patargs in + let pat' = PatCstr (l, cstr, patargs, alias) in let cstr = mkConstruct ci.cs_cstr in let app = applistc cstr (List.map (lift (List.length args)) params) in - let app = applistc app (List.rev args) in + let app = applistc app args in +(* trace (str "New pattern: " ++ Printer.pr_cases_pattern pat'); *) if alias <> Anonymous then - (alias, Some app, ty) :: sign, lift 1 app, n + 1 - else sign, app, n + pat', (alias, Some app, ty) :: sign, lift 1 app, n + 1 + else pat', sign, app, n in - let x, y, z = typ env ty pat in - let x = List.rev x in - let prod = it_mkProd_or_LetIn y x 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); - - x, y + pat', (sign, y) let mk_refl typ a = mkApp (Lazy.force eq_refl, [| typ; a |]) +let vars_of_ctx = + List.rev_map (fun (na, _, t) -> + match na with + Anonymous -> raise (Invalid_argument "vars_of_ctx") + | Name n -> RVar (dummy_loc, n)) + +(*let build_ineqs eqns pats = + List.fold_left + (fun (sign, c) eqn -> + let acc = fold_left3 + (fun acc prevpat (ppat_sign, ppat_c, ppat_ty) (pat, pat_c) -> + match acc with + None -> None + | Some (sign,len, c) -> + if is_included pat prevpat then + let lens = List.length ppat_sign in + let acc = + (lift_rels lens ppat_sign @ sign, + lens + len, + mkApp (Lazy.force eq_ind, + [| ppat_ty ; ppat_c ; + lift (lens + len) pat_c |]) :: c) + in Some acc + else None) + (sign, c) eqn.patterns eqn.c_patterns pats + in match acc with + None -> (sign, c) + | Some (sign, len, c) -> + it_mkProd_or_LetIn c sign + + ) + ([], []) eqns*) + let constrs_of_pats typing_fun tycon env isevars eqns tomatchs = - List.map - (fun eqn -> + let i = ref 0 in + List.fold_left + (fun (branches, eqns) eqn -> let pats = List.map2 (fun pat (_, ty) -> constr_of_pat env isevars (type_of_tomatch ty) pat) eqn.patterns tomatchs in + let newpatterns, pats = List.split pats in let rhs_rels, signlen = List.fold_left (fun (env, n) (sign,_) -> (sign @ env, List.length sign + n)) ([], 0) pats in @@ -1664,6 +1714,7 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs = ([], 0, signlen) pats tomatchs in let eqs_rels = List.map (fun eq -> Name (id_of_string "H"), None, eq) eqs in +(* let ineqs = build_ineqs eqns newpatterns in *) let rhs_rels' = eqs_rels @ rhs_rels in let rhs_env = push_rels rhs_rels' env in (try trace (str "branch env: " ++ print_env rhs_env) @@ -1673,12 +1724,25 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs = (try trace (str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); with _ -> trace (str "Error in typed branch pretty printing")); - let j' = it_mkLambda_or_LetIn j.uj_val eqs_rels - (*uj_type = it_mkProd_or_LetIn j.uj_type eqs_rels; }*) + let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' + and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in + let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in + let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in + (try trace (str "Branch decl: " ++ pr_rel_decl env branch_decl) + with _ -> trace (str "Error in branch decl pp")); + let branch = + let bref = RVar (dummy_loc, branch_name) in + match vars_of_ctx rhs_rels with + [] -> bref + | l -> RApp (dummy_loc, bref, l) in - let rhs = { eqn.rhs with c_it = j'; rhs_lift = succ signlen } in - { eqn with rhs = rhs }) - eqns + (try trace (str "New branch: " ++ Printer.pr_rawconstr branch) + with _ -> trace (str "Error in new branch pp")); + incr i; + let rhs = { eqn.rhs with it = branch } in + (branch_decl :: branches, + { eqn with patterns = newpatterns; rhs = rhs } :: eqns)) + ([], []) eqns (* liftn_rel_declaration *) @@ -1735,7 +1799,14 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e (* constructors found in patterns *) let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in - let matx = constrs_of_pats typing_fun tycon env isevars matx tomatchs in + 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 matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in + trace (str "New env: " ++ my_print_env env); + let tycon = lift_tycon len tycon in + let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in let args = List.map (fun (tm,ty) -> mk_refl (type_of_tomatch ty) tm) tomatchs in (* We build the elimination predicate if any and check its consistency *) @@ -1761,7 +1832,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e (* We check for unused patterns *) List.iter (check_unused_pattern env) matx; let j = - { uj_val = applistc j.uj_val args; + { uj_val = it_mkLambda_or_LetIn (applistc j.uj_val args) lets; uj_type = opred; } in inh_conv_coerce_to_tycon loc env isevars j tycon diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index a20383688..5d982cf27 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -229,15 +229,18 @@ let update_obls prg obls rem = | l -> let progs = List.map (fun (x,y) -> ProgMap.find x !from_prg, y) prg'.prg_deps in if List.for_all (fun x -> obligations_solved (fst x)) progs then - declare_mutual_definition progs) + (declare_mutual_definition progs; + from_prg := List.fold_left + (fun acc x -> ProgMap.remove (fst x).prg_name acc) !from_prg progs)) let add_definition n b t obls = Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); let prg = init_prog_info n b t [] obls in let obls,_ = prg.prg_obligations in if Array.length obls = 0 then ( - Options.if_verbose ppnl (str "."); - declare_definition prg) + Options.if_verbose ppnl (str "."); + declare_definition prg; + from_prg := ProgMap.remove prg.prg_name !from_prg) else ( let len = Array.length obls in let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index c32971289..9339d7387 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -162,8 +162,10 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* in environment [env], with existential variables [(evars_of isevars)] and *) (* the type constraint tycon *) let rec pretype (tycon : type_constraint) env isevars lvar c = - let _ = Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ - str " with tycon " ++ Evarutil.pr_tycon env tycon) in + let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ + str " with tycon " ++ Evarutil.pr_tycon env tycon) + with _ -> () + in match c with | RRef (loc,ref) -> inh_conv_coerce_to_tycon loc env isevars |