From 412cceb92a1baa75d3d3f78720bfe5b2e261827e Mon Sep 17 00:00:00 2001 From: msozeau Date: Sat, 3 Feb 2007 21:20:22 +0000 Subject: Work on ineqs generation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9590 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/subtac/subtac_cases.ml | 149 +++++++++++++++++++++-------------------- 1 file changed, 76 insertions(+), 73 deletions(-) diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index fbe1ac37b..6da7567c8 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -1651,7 +1651,7 @@ let constr_of_pat env isevars ty pat idents = let pat', sign, y, z, idents = typ env ty pat idents in let c = it_mkProd_or_LetIn y sign in trace (str "Constr_of_pat gives: " ++ my_print_constr env c); - pat', (sign, y), idents + pat', (sign, y, ty), idents let mk_refl typ a = mkApp (Lazy.force eq_refl, [| typ; a |]) @@ -1661,100 +1661,103 @@ let vars_of_ctx = 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) -> +let build_ineqs prevpatterns = () + (* List.fold_left + (fun (sign, c) eqnpats -> + let acc = List.fold_left + (fun acc (ppat_sign, ppat_c, ppat_ty) -> match acc with None -> None - | Some (sign,len, c) -> - if is_included pat prevpat then + | Some (sign, len, n, c) -> +(* if is_included pat prevpat then *) let lens = List.length ppat_sign in + let len' = lens + len in let acc = - (lift_rels lens ppat_sign @ sign, - lens + len, + (lift_rel_context len ppat_sign @ sign, + len', mkApp (Lazy.force eq_ind, [| ppat_ty ; ppat_c ; - lift (lens + len) pat_c |]) :: c) + mkRel (len' + n) |]) :: c) in Some acc - else None) - (sign, c) eqn.patterns eqn.c_patterns pats +(* else None *)) + (sign, c) eqnpats in match acc with None -> (sign, c) | Some (sign, len, c) -> it_mkProd_or_LetIn c sign - ) - ([], []) eqns*) - + ([], []) prevpatterns +*) let constrs_of_pats typing_fun tycon env isevars eqns tomatchs = let i = ref 0 in - List.fold_left - (fun (branches, eqns) eqn -> - let _, newpatterns, pats = - List.fold_right2 (fun pat (_, ty) (idents, newpatterns, pats) -> - let x, y, z = constr_of_pat env isevars (type_of_tomatch ty) pat idents in - (z, x :: newpatterns, y :: pats)) - eqn.patterns tomatchs ([], [], []) - in - let rhs_rels, signlen = - List.fold_left (fun (renv, n) (sign,_) -> + let (x, y, z) = + List.fold_left + (fun (branches, eqns, prevpatterns) eqn -> + let _, newpatterns, pats = + List.fold_right2 (fun pat (_, ty) (idents, newpatterns, pats) -> + let x, y, z = constr_of_pat env isevars (type_of_tomatch ty) pat idents in + (z, x :: newpatterns, y :: pats)) + eqn.patterns tomatchs ([], [], []) + in + let rhs_rels, signlen = + List.fold_left (fun (renv, n) (sign,_,_) -> ((lift_rel_context n sign) @ renv, List.length sign + n)) - ([], 0) pats in - let eqs, _, _ = List.fold_left2 - (fun (eqs, n, slen) (sign, c) (tm, ty) -> - let len = n + signlen in (* Number of already defined equations + signature *) - let csignlen = List.length sign in - let slen' = slen - csignlen in (* Lift to get pattern variables signature *) - let c = liftn (signlen - slen) signlen c in (* Lift to jump over previous ind signatures for pattern variables outside sign - in c (e.g. type arguments of constructors instanciated by variables ) *) - let cstr = lift (slen' + n) c in -(* trace (str "lift " ++ my_print_constr (push_rels sign env) c ++ *) -(* str " by " ++ int ++ str " to get " ++ *) -(* my_print_constr (push_rels sign env) cstr); *) - let app = - mkApp (Lazy.force eq_ind, - [| lift len (type_of_tomatch ty); cstr; lift len tm |]) - in app :: eqs, succ n, slen') - ([], 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) *) -(* with _ -> trace (str "error in print branch env")); *) - let tycon = lift_tycon (List.length eqs + signlen) tycon in - - let j = typing_fun tycon rhs_env eqn.rhs.it in -(* (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++ *) -(* str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); *) -(* with _ -> *) -(* trace (str "Error in typed branch pretty printing")); *) + ([], 0) pats in + let eqs, _, _ = List.fold_left2 + (fun (eqs, n, slen) (sign, c, _) (tm, ty) -> + let len = n + signlen in (* Number of already defined equations + signature *) + let csignlen = List.length sign in + let slen' = slen - csignlen in (* Lift to get pattern variables signature *) + let c = liftn (signlen - slen) signlen c in (* Lift to jump over previous ind signatures for pattern variables outside sign + in c (e.g. type arguments of constructors instanciated by variables ) *) + let cstr = lift (slen' + n) c in + (* trace (str "lift " ++ my_print_constr (push_rels sign env) c ++ *) + (* str " by " ++ int ++ str " to get " ++ *) + (* my_print_constr (push_rels sign env) cstr); *) + let app = + mkApp (Lazy.force eq_ind, + [| lift len (type_of_tomatch ty); cstr; lift len tm |]) + in app :: eqs, succ n, slen') + ([], 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 prevpatterns 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) *) + (* with _ -> trace (str "error in print branch env")); *) + let tycon = lift_tycon (List.length eqs + signlen) tycon in + + let j = typing_fun tycon rhs_env eqn.rhs.it in + (* (try trace (str "in env: " ++ my_print_env rhs_env ++ str"," ++ *) + (* str "Typed branch: " ++ Prettyp.print_judgment rhs_env j); *) + (* with _ -> *) + (* trace (str "Error in typed branch pretty printing")); *) 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 (Name branch_name, Some bbody, btype)) *) -(* with _ -> trace (str "Error in branch decl pp")); *) + (* (try trace (str "Branch decl: " ++ pr_rel_decl env (Name branch_name, Some bbody, btype)) *) + (* 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) + match vars_of_ctx rhs_rels with + [] -> bref + | l -> RApp (dummy_loc, bref, l) in -(* let branch = *) -(* List.fold_left (fun br (eqH, _, t) -> RLambda (dummy_loc, eqH, RHole (dummy_loc, Evd.InternalHole), br)) branch eqs_rels *) -(* in *) -(* (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 - + (* let branch = *) + (* List.fold_left (fun br (eqH, _, t) -> RLambda (dummy_loc, eqH, RHole (dummy_loc, Evd.InternalHole), br)) branch eqs_rels *) + (* in *) + (* (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, + pats :: prevpatterns)) + ([], [], []) eqns + in x, y + (* liftn_rel_declaration *) -- cgit v1.2.3