diff options
Diffstat (limited to 'contrib/subtac/subtac_utils.ml')
| -rw-r--r-- | contrib/subtac/subtac_utils.ml | 122 |
1 files changed, 103 insertions, 19 deletions
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index 6c165dad..59c858a6 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -57,7 +57,7 @@ let natind = lazy (init_constant ["Init"; "Datatypes"] "nat") let intind = lazy (init_constant ["ZArith"; "binint"] "Z") let existSind = lazy (init_constant ["Init"; "Specif"] "sigS") -let existS = lazy (build_sigma_set ()) +let existS = lazy (build_sigma_type ()) let prod = lazy (build_prod ()) @@ -118,8 +118,8 @@ let print_args env args = let make_existential loc env isevars c = let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark) c in let (key, args) = destEvar evar in - debug 2 (str "Constructed evar " ++ int key ++ str " applied to args: " ++ - print_args env args); + (try debug 2 (str "Constructed evar " ++ int key ++ str " applied to args: " ++ + print_args env args) with _ -> ()); evar let make_existential_expr loc env c = @@ -160,26 +160,27 @@ open Tactics open Tacticals let build_dependent_sum l = - let rec aux (acc, tac, typ) = function + let rec aux (tac, typ) = function (n, t) :: tl -> let t' = mkLambda (Name n, t, typ) in - trace (str ("treating " ^ string_of_id n) ++ - str "assert: " ++ my_print_constr (Global.env ()) t); + trace (spc () ++ str ("treating evar " ^ string_of_id n)); + (try trace (str " assert: " ++ my_print_constr (Global.env ()) t) + with _ -> ()); let tac' = - tclTHEN (assert_tac true (Name n) t) - (tclTHENLIST - [intros; - (tclTHENSEQ - [tclTRY (constructor_tac (Some 1) 1 - (Rawterm.ImplicitBindings [mkVar n])); - tac]); - ]) + tclTHENS (assert_tac true (Name n) t) + ([intros; + (tclTHENSEQ + [constructor_tac (Some 1) 1 + (Rawterm.ImplicitBindings [mkVar n]); + tac]); + ]) in - aux (mkApp (Lazy.force ex_ind, [| t; t'; |]), tac', t') tl - | [] -> acc, tac, typ + let newt = mkApp (Lazy.force ex_ind, [| t; t'; |]) in + aux (tac', newt) tl + | [] -> tac, typ in match l with - (_, hd) :: tl -> aux (hd, intros, hd) tl + (_, hd) :: tl -> aux (intros, hd) tl | [] -> raise (Invalid_argument "build_dependent_sum") open Proof_type @@ -218,7 +219,8 @@ let and_tac l hook = let and_proof_id, and_goal, and_tac, and_extract = match l with | [] -> raise (Invalid_argument "and_tac: empty list of goals") - | (hdid, x, hdg, hdt) :: tl -> aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl + | (hdid, x, hdg, hdt) :: tl -> + aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl in let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in Command.start_proof and_proofid goal_kind and_goal @@ -238,9 +240,91 @@ let destruct_ex ext ex = try (args.(0), args.(1)) with _ -> assert(false) in - (mk_ex_pi1 dom rng acc) :: aux rng (mk_ex_pi2 dom rng acc) + let pi1 = (mk_ex_pi1 dom rng acc) in + let rng_body = + match kind_of_term rng with + Lambda (_, _, t) -> subst1 pi1 t + | t -> rng + in + pi1 :: aux rng_body (mk_ex_pi2 dom rng acc) | _ -> [acc]) | _ -> [acc] in aux ex ext +let list_mapi f = + let rec aux i = function + hd :: tl -> f i hd :: aux (succ i) tl + | [] -> [] + in aux 0 + +open Rawterm + +let rewrite_cases_aux (loc, po, tml, eqns) = + let tml' = list_mapi (fun i (c, (n, opt)) -> c, + ((match n with + Name id -> (match c with + | RVar (_, id') when id = id' -> + id, (id_of_string (string_of_id id ^ "Heq_id")) + | RVar (_, id') -> + id', id + | _ -> id_of_string (string_of_id id ^ "Heq_id"), id) + | Anonymous -> + let str = "Heq_id" ^ string_of_int i in + id_of_string str, id_of_string (str ^ "'")), + opt)) tml + in + let mkHole = RHole (dummy_loc, InternalHole) in + let mkCoerceCast c = RCast (dummy_loc, c, CastCoerce, mkHole) in + let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)), + [mkHole; c; n]) + in + let eqs_types = + List.map + (fun (c, ((id, id'), _)) -> + let heqid = id_of_string ("Heq" ^ string_of_id id) in + Name heqid, mkeq (RVar (dummy_loc, id')) c) + tml' + in + let po = + List.fold_right + (fun (n,t) acc -> + RProd (dummy_loc, Anonymous, t, acc)) + eqs_types (match po with + Some e -> e + | None -> mkHole) + in + let eqns = + List.map (fun (loc, idl, cpl, c) -> + let c' = + List.fold_left + (fun acc (n, t) -> + RLambda (dummy_loc, n, mkHole, acc)) + c eqs_types + in (loc, idl, cpl, c')) + eqns + in + let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref), + [mkHole; c]) + in + let refls = List.map (fun (c, ((id, _), _)) -> mk_refl_equal (mkCoerceCast c)) tml' in + let tml'' = List.map (fun (c, ((id, id'), opt)) -> c, (Name id', opt)) tml' in + let case = RCases (loc,Some po,tml'',eqns) in + let app = RApp (dummy_loc, case, refls) in +(* let letapp = List.fold_left (fun acc (c, ((id, id'), opt)) -> RLetIn (dummy_loc, Name id, c, acc)) *) +(* app tml' *) +(* in *) + app + +let rec rewrite_cases c = + match c with + RCases _ -> let c' = map_rawconstr rewrite_cases c in + (match c' with + | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w) + | _ -> assert(false)) + | _ -> map_rawconstr rewrite_cases c + +let rewrite_cases env c = + let c' = rewrite_cases c in + let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in + c' |