diff options
Diffstat (limited to 'contrib/subtac/subtac_command.ml')
| -rw-r--r-- | contrib/subtac/subtac_command.ml | 109 |
1 files changed, 66 insertions, 43 deletions
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 68ab8c46..86139039 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -56,7 +56,6 @@ let interp_gen kind isevars env ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in - let c' = Subtac_utils.rewrite_cases env c' in (* (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *) let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in evar_nf isevars c' @@ -178,10 +177,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let env = Global.env() in let nc = named_context env in let nc_len = named_context_length nc in -(* let pr c = my_print_constr env c in *) -(* let prr = Printer.pr_rel_context env in *) -(* let prn = Printer.pr_named_context env in *) -(* let pr_rel env = Printer.pr_rel_context env in *) + let pr c = my_print_constr env c in + let prr = Printer.pr_rel_context env in + let _prn = Printer.pr_named_context env in + let _pr_rel env = Printer.pr_rel_context env in (* let _ = *) (* try debug 2 (str "In named context: " ++ prn (named_context env) ++ str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ *) (* Ppconstr.pr_binders bl ++ str " : " ++ *) @@ -193,40 +192,42 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let after, ((argname, _, argtyp) as arg), before = split_args (succ n) binders_rel in let before_length, after_length = List.length before, List.length after in let argid = match argname with Name n -> n | _ -> assert(false) in - let _liftafter = lift_binders 1 after_length after in + let liftafter = lift_binders 1 after_length after in let envwf = push_rel_context before env in let wf_rel, wf_rel_fun, measure_fn = let rconstr_body, rconstr = let app = mkAppC (r, [mkIdentC (id_of_name argname)]) in let env = push_rel_context [arg] envwf in let capp = interp_constr isevars env app in - capp, mkLambda (argname, argtyp, capp) + capp, mkLambda (argname, argtyp, capp) in + trace (str"rconstr_body: " ++ pr rconstr_body); if measure then let lt_rel = constr_of_global (Lazy.force lt_ref) in let name s = Name (id_of_string s) in - let wf_rel_fun = - (fun x y -> - mkApp (lt_rel, [| subst1 x rconstr_body; - subst1 y rconstr_body |])) - in + let wf_rel_fun lift x y = (* lift to before_env *) + trace (str"lifter rconstr_body:" ++ pr (liftn lift 2 rconstr_body)); + mkApp (lt_rel, [| subst1 x (liftn lift 2 rconstr_body); + subst1 y (liftn lift 2 rconstr_body) |]) + in let wf_rel = mkLambda (name "x", argtyp, mkLambda (name "y", lift 1 argtyp, - wf_rel_fun (mkRel 2) (mkRel 1))) + wf_rel_fun 0 (mkRel 2) (mkRel 1))) in wf_rel, wf_rel_fun , Some rconstr - else rconstr, (fun x y -> mkApp (rconstr, [|x; y|])), None + else rconstr, (fun lift x y -> mkApp (rconstr, [|x; y|])), None in let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |]) in let argid' = id_of_string (string_of_id argid ^ "'") in - let wfarg len = (Name argid', None, + let wfarg len = (Name argid', None, mkSubset (Name argid') (lift len argtyp) - (wf_rel_fun (mkRel 1) (mkRel (len + 1)))) + (wf_rel_fun (succ len) (mkRel 1) (mkRel (len + 1)))) in let top_bl = after @ (arg :: before) in - let intern_bl = after @ (wfarg 1 :: arg :: before) in + let intern_bl = liftafter @ (wfarg 1 :: arg :: before) in + (try trace (str "Intern bl: " ++ prr intern_bl) with _ -> ()); let top_env = push_rel_context top_bl env in let _intern_env = push_rel_context intern_bl env in let top_arity = interp_type isevars top_env arityc in @@ -234,36 +235,45 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let projection = mkApp (proj, [| argtyp ; (mkLambda (Name argid', argtyp, - (wf_rel_fun (mkRel 1) (mkRel 3)))) ; + (wf_rel_fun 1 (mkRel 1) (mkRel 3)))) ; mkRel 1 |]) in - (* (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ()); *) - let intern_arity = substnl [projection] after_length top_arity in -(* (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ()); *) + let intern_arity = it_mkProd_or_LetIn top_arity after in + (try trace (str "After length: " ++ int after_length ++ str "Top env: " ++ prr top_bl ++ spc () ++ str "Top arity: " ++ my_print_constr top_env top_arity); + trace (str "Before lifting arity: " ++ my_print_constr env top_arity) with _ -> ()); + (* Top arity is in top_env = after :: arg :: before *) +(* let intern_arity' = liftn 1 (succ after_length) top_arity in (\* arity in after :: wfarg :: arg :: before *\) *) +(* (try trace (str "projection: " "After lifting arity: " ++ my_print_constr env intern_arity' ++ spc ()); *) +(* trace (str "Intern env: " ++ prr intern_bl ++ str "intern_arity': " ++ my_print_constr _intern_env intern_arity') with _ -> ()); *) + let intern_arity = substl [projection] intern_arity in (* substitute the projection of wfarg for arg *) + (try trace (str "Top arity after subst: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); +(* let intern_arity = liftn 1 (succ after_length) intern_arity in (\* back in after :: wfarg :: arg :: before (ie, jump over arg) *\) *) +(* (try trace (str "Top arity after subst and lift: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); *) let intern_before_env = push_rel_context before env in - let intern_fun_bl = after @ [wfarg 1] in +(* let intern_fun_bl = liftafter @ [wfarg 1] in (\* FixMe dependencies *\) *) (* (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ()); *) - let intern_fun_arity = intern_arity in -(* (try debug 2 (str "Intern fun arity: " ++ *) -(* my_print_constr intern_env intern_fun_arity) with _ -> ()); *) - let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in + (try trace (str "Intern arity: " ++ + my_print_constr _intern_env intern_arity) with _ -> ()); + let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in + (try trace (str "Intern fun arity product: " ++ + my_print_constr (push_rel_context [arg] intern_before_env) intern_fun_arity_prod) with _ -> ()); let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in - let fun_bl = after @ (intern_fun_binder :: [arg]) in + let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in (* (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ()); *) let fun_env = push_rel_context fun_bl intern_before_env in let fun_arity = interp_type isevars fun_env arityc in let intern_body = interp_casted_constr isevars fun_env body fun_arity in let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in -(* let _ = *) -(* try debug 2 (str "Fun bl: " ++ prr fun_bl ++ spc () ++ *) -(* str "Intern bl" ++ prr intern_bl ++ spc () ++ *) -(* str "Top bl" ++ prr top_bl ++ spc () ++ *) -(* str "Intern arity: " ++ pr intern_arity ++ *) -(* str "Top arity: " ++ pr top_arity ++ spc () ++ *) + let _ = + try trace ((* str "Fun bl: " ++ prr fun_bl ++ spc () ++ *) + str "Intern bl" ++ prr intern_bl ++ spc ()) +(* str "Top bl" ++ prr top_bl ++ spc () ++ *) +(* str "Intern arity: " ++ pr intern_arity ++ *) +(* str "Top arity: " ++ pr top_arity ++ spc () ++ *) (* str "Intern body " ++ pr intern_body_lam) *) -(* with _ -> () *) -(* in *) + with _ -> () + in let _impl = if Impargs.is_implicit_args() then Impargs.compute_implicits top_env top_arity @@ -276,13 +286,16 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = mkApp (constr_of_reference (Lazy.force fix_sub_ref), [| argtyp ; wf_rel ; - make_existential dummy_loc intern_before_env isevars wf_proof ; + make_existential dummy_loc ~opaque:false intern_before_env isevars wf_proof ; prop ; intern_body_lam |]) | Some f -> - mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), - [| argtyp ; f ; prop ; - intern_body_lam |]) + lift (succ after_length) + (mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), + [| argtyp ; + f ; + prop ; + intern_body_lam |])) in let def_appl = applist (fix_def, gen_rels (after_length + 1)) in let def = it_mkLambda_or_LetIn def_appl binders_rel in @@ -294,15 +307,22 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = (* ++ str "Coq type: " ++ my_print_constr env fullctyp) *) (* with _ -> () *) (* in *) - let evm = non_instanciated_map env isevars in + let evm = evars_of_term (Evd.evars_of !isevars) Evd.empty fullctyp in + let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in + let evm = non_instanciated_map env isevars evm in + (* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *) - let evars, evars_def = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in + let evars, evars_def = Eterm.eterm_obligations recname nc_len !isevars evm 0 fullcoqc (Some fullctyp) in (* (try trace (str "Generated obligations : "); *) (* Array.iter *) (* (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *) (* evars; *) (* with _ -> ()); *) Subtac_obligations.add_definition recname evars_def fullctyp evars + +let nf_evar_context isevars ctx = + List.map (fun (n, b, t) -> + (n, option_map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx let build_mutrec l boxed = let sigma = Evd.empty and env = Global.env () in @@ -368,10 +388,13 @@ let build_mutrec l boxed = let (isevars, info, def) = defrec.(i) in (* let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in *) let def = evar_nf isevars def in + let x, y, typ = arrec.(i) in + let typ = evar_nf isevars typ in + arrec.(i) <- (x, y, typ); + let rec_sign = nf_evar_context !isevars rec_sign in let isevars = Evd.undefined_evars !isevars in (* let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in *) let evm = Evd.evars_of isevars in - let _, _, typ = arrec.(i) in let id = namerec.(i) in (* Generalize by the recursive prototypes *) let def = @@ -379,7 +402,7 @@ let build_mutrec l boxed = and typ = Termops.it_mkNamedProd_or_LetIn typ rec_sign in - let evars, def = Eterm.eterm_obligations id nc_len evm def (Some typ) in + let evars, def = Eterm.eterm_obligations id nc_len isevars evm recdefs def (Some typ) in collect_evars (succ i) ((id, def, typ, evars) :: acc) else acc in |