diff options
Diffstat (limited to 'contrib/subtac/subtac_command.ml')
-rw-r--r-- | contrib/subtac/subtac_command.ml | 271 |
1 files changed, 203 insertions, 68 deletions
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index b09228c0..c738d7a6 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -117,7 +117,8 @@ let interp_context sigma env params = let list_chop_hd i l = match list_chop i l with | (l1,x::l2) -> (l1,x,l2) - | _ -> assert false + | (x :: [], l2) -> ([], x, []) + | _ -> assert(false) let collect_non_rec env = let rec searchrec lnonrec lnamerec ldefrec larrec nrec = @@ -173,82 +174,189 @@ let list_of_local_binders l = | [] -> List.rev acc in aux [] l -let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed = +let lift_binders k n l = + let rec aux n = function + | (id, t, c) :: tl -> (id, option_map (liftn k n) t, liftn k n c) :: aux (pred n) tl + | [] -> [] + in aux n l + +let rec gen_rels = function + 0 -> [] + | n -> mkRel n :: gen_rels (pred n) + +let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = + let sigma = Evd.empty in + let isevars = ref (Evd.create_evar_defs sigma) in + let env = Global.env() in + let pr c = my_print_constr env c in + let prr = Printer.pr_rel_context env in + let pr_rel env = Printer.pr_rel_context env in + let _ = + try debug 2 (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ + Ppconstr.pr_binders bl ++ str " : " ++ + Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++ + Ppconstr.pr_constr_expr body) + with _ -> () + in + let env', binders_rel = interp_context isevars env bl in + let after, ((argname, _, argtyp) as arg), before = list_chop_hd (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 envwf = push_rel_context before env in + let wf_rel, measure_fn = + let rconstr = interp_constr isevars envwf r in + if measure then + let lt_rel = constr_of_global (Lazy.force lt_ref) in + let name s = Name (id_of_string s) in + mkLambda (name "x", argtyp, + mkLambda (name "y", argtyp, + mkApp (lt_rel, + [| mkApp (rconstr, [| mkRel 2 |]) ; + mkApp (rconstr, [| mkRel 1 |]) |]))), + Some rconstr + else rconstr, 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, + mkSubset (Name argid') argtyp + (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|]))) + in + let top_bl = after @ (arg :: before) in + let intern_bl = after @ (wfarg 1 :: arg :: before) in + 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 + (try debug 2 (str "Intern bl: " ++ prr intern_bl) with _ -> ()); + let proj = (Lazy.force sig_).Coqlib.proj1 in + let projection = + mkApp (proj, [| argtyp ; + (mkLambda (Name argid', argtyp, + (mkApp (wf_rel, [|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_before_env = push_rel_context before env in + let intern_fun_bl = after @ [wfarg 1] in + (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 + let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in + let fun_bl = after @ (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 () ++ + str "Intern body " ++ pr intern_body_lam) + with _ -> () + in + let _impl = + if Impargs.is_implicit_args() + then Impargs.compute_implicits top_env top_arity + else [] + in + let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in + let fix_def = + match measure_fn with + None -> + mkApp (constr_of_reference (Lazy.force fix_sub_ref), + [| argtyp ; + wf_rel ; + make_existential dummy_loc 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 |]) + in + let def_appl = applist (fix_def, gen_rels (after_length + 1)) in + let def = it_mkLambda_or_LetIn def_appl binders_rel in + let typ = it_mkProd_or_LetIn top_arity binders_rel in + debug 2 (str "Constructed def"); + debug 2 (my_print_constr intern_before_env def); + debug 2 (str "Type: " ++ my_print_constr env typ); + let fullcoqc = Evarutil.nf_isevar !isevars def in + let fullctyp = Evarutil.nf_isevar !isevars typ in + let _ = try trace (str "After evar normalization: " ++ spc () ++ + str "Coq term: " ++ my_print_constr env fullcoqc ++ spc () + ++ str "Coq type: " ++ my_print_constr env fullctyp) + with _ -> () + in + let evm = non_instanciated_map env isevars in + let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in + let evars_def, evars_typ, evars = Eterm.eterm_term evm fullcoqc (Some fullctyp) in + let evars_typ = out_some evars_typ in + (try trace (str "Building evars sum for : "); + List.iter + (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) + evars; + with _ -> ()); + let (sum_tac, sumg) = Subtac_utils.build_dependent_sum evars in + (try trace (str "Evars sum: " ++ my_print_constr env sumg); + trace (str "Evars type: " ++ my_print_constr env evars_typ); + with _ -> ()); + let proofid = id_of_string (string_of_id recname ^ "_evars_proof") in + Command.start_proof proofid goal_proof_kind sumg + (fun strength gr -> + debug 2 (str "Proof finished"); + let def = constr_of_global gr in + let args = Subtac_utils.destruct_ex def sumg in + let _, newdef = decompose_lam_n (List.length args) evars_def in + let constr = Term.substl (List.rev args) newdef in + debug 2 (str "Applied existentials : " ++ my_print_constr env constr); + let ce = + { const_entry_body = constr; + const_entry_type = Some fullctyp; + const_entry_opaque = false; + const_entry_boxed = boxed} + in + let _constant = Declare.declare_constant + recname (DefinitionEntry ce,IsDefinition Definition) + in + definition_message recname); + trace (str "Started existentials proof"); + Pfedit.by sum_tac; + trace (str "Applied sum tac") + +let build_mutrec l boxed = let sigma = Evd.empty and env0 = Global.env() in let lnameargsardef = (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*) - lnameargsardef + l in let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef in - (* Build the recursive context and notations for the recursive types *) + (* Build the recursive context and notations for the recursive types *) let (rec_sign,rec_impls,arityl) = List.fold_left - (fun (env,impls,arl) ((recname,(n, ro),bl,arityc,body),_) -> - let isevars = ref (Evd.create_evar_defs sigma) in - match ro with - CStructRec -> - let arityc = Command.generalize_constr_expr arityc bl in - let arity = interp_type isevars env0 arityc in - let impl = - if Impargs.is_implicit_args() - then Impargs.compute_implicits env0 arity - else [] in - let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in - (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl) - | CWfRec r -> - let n = out_some n in - let _ = - try trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ - Ppconstr.pr_binders bl ++ str " : " ++ - Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++ - Ppconstr.pr_constr_expr body) - with _ -> () - in - let env', binders_rel = interp_context isevars env0 bl in - let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in - let argid = match argname with Name n -> n | _ -> assert(false) in - let after' = List.map (fun (n, c, t) -> (n, option_map (lift 1) c, lift 1 t)) after in - let envwf = push_rel_context before env0 in - let wf_rel = interp_constr isevars envwf r in - let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in - let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| argtyp; wf_rel; mkRel 1 |])) in - let argid' = id_of_string (string_of_id argid ^ "'") in - let before_length, after_length = List.length before, List.length after in - let full_length = before_length + 1 + after_length in - let wfarg len = (Name argid, None, - mkSubset (Name argid') argtyp - (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|]))) - in - let new_bl = after' @ (accarg :: arg :: before) - and intern_bl = after @ (wfarg (before_length + 1) :: before) - in - let intern_env = push_rel_context intern_bl env0 in - let env' = push_rel_context new_bl env0 in - let arity = interp_type isevars intern_env arityc in - let intern_arity = it_mkProd_or_LetIn arity intern_bl in - let arity' = interp_type isevars env' arityc in - let arity' = it_mkProd_or_LetIn arity' new_bl in - let fun_bl = after @ ((Name recname, None, intern_arity) :: arg :: before) in - let _ = - let pr c = my_print_constr env c in - let prr = Printer.pr_rel_context env in - try trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++ - str "Intern bl" ++ prr intern_bl ++ spc () ++ - str "Extern bl" ++ prr new_bl ++ spc () ++ - str "Intern arity: " ++ pr intern_arity) - with _ -> () - in - let impl = - if Impargs.is_implicit_args() - then Impargs.compute_implicits intern_env arity' - else [] in - let impls' = (recname,([],impl,compute_arguments_scope arity'))::impls in - (Environ.push_named (recname,None,arity') env, impls', - (isevars, Some (full_length - n, argtyp, wf_rel, fun_bl, intern_bl, intern_arity), arity')::arl)) + (fun (env,impls,arl) ((recname, n, bl,arityc,body),_) -> + let isevars = ref (Evd.create_evar_defs sigma) in + let arityc = Command.generalize_constr_expr arityc bl in + let arity = interp_type isevars env0 arityc in + let impl = + if Impargs.is_implicit_args() + then Impargs.compute_implicits env0 arity + else [] in + let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in + (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)) (env0,[],[]) lnameargsardef in let arityl = List.rev arityl in let notations = @@ -283,7 +391,6 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed let (lnonrec,(namerec,defrec,arrec,nvrec)) = collect_non_rec env0 lrecnames recdef arityl nv in - let nvrec' = Array.map (function (Some n,_) -> n | _ -> 0) nvrec in(* ignore rec order *) let declare arrec defrec = let recvec = Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in @@ -293,7 +400,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed my_print_constr env0 (recvec.(i))); with _ -> ()); let ce = - { const_entry_body = mkFix ((nvrec',i),recdecls); + { const_entry_body = mkFix ((nvrec,i),recdecls); const_entry_type = Some arrec.(i); const_entry_opaque = false; const_entry_boxed = boxed} in @@ -384,6 +491,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed match sum with Some (sumtac, sumg) -> Some (id, kn, sumg, sumtac) | None -> None) defs in + match real_evars with + [] -> declare (List.rev_map (fun (id, c, _) -> + snd (decompose_lam_n recdefs c)) defs) + | l -> + Subtac_utils.and_tac real_evars (fun f _ gr -> let _ = trace (str "Got a proof of: " ++ pr_global gr ++ @@ -431,5 +543,28 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed Environ.NoBody -> trace (str "Constant has no body") | Environ.Opaque -> trace (str "Constant is opaque") ) + +let out_n = function + Some n -> n + | None -> 0 + +let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed = + match lnameargsardef with + | ((id, (n, CWfRec r), bl, typ, body), no) :: [] -> + build_wellfounded (id, out_n n, bl, typ, body) r false no boxed + | ((id, (n, CMeasureRec r), bl, typ, body), no) :: [] -> + build_wellfounded (id, out_n n, bl, typ, body) r true no boxed + | l -> + let lnameargsardef = + List.map (fun ((id, (n, ro), bl, typ, body), no) -> + match ro with + CStructRec -> (id, out_n n, bl, typ, body), no + | CWfRec _ | CMeasureRec _ -> + errorlabstrm "Subtac_command.build_recursive" + (str "Well-founded fixpoints not allowed in mutually recursive blocks")) + lnameargsardef + in + build_mutrec lnameargsardef boxed; + assert(false) |