diff options
author | 2007-02-13 13:48:12 +0000 | |
---|---|---|
committer | 2007-02-13 13:48:12 +0000 | |
commit | 7f076db2a924377e9de3f9a6d838b8c44ed2e16d (patch) | |
tree | e075c526532a227c83d951c9dff8c944ea0c4d15 /contrib/subtac/subtac_command.ml | |
parent | 2a14f39fdfa80b021227396b22e38ed7c35356df (diff) | |
parent | 55ce117e8083477593cf1ff2e51a3641c7973830 (diff) |
Merge commit 'upstream/8.1+dfsg' into 8.1
Diffstat (limited to 'contrib/subtac/subtac_command.ml')
-rw-r--r-- | contrib/subtac/subtac_command.ml | 282 |
1 files changed, 71 insertions, 211 deletions
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index b433af2c..68ab8c46 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -57,7 +57,7 @@ let interp_gen kind isevars env 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 _ -> ()); +(* (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *) let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in evar_nf isevars c' @@ -150,14 +150,6 @@ let collect_non_rec env = in searchrec [] - -let filter_map f l = - let rec aux acc = function - hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl - | None -> aux acc tl) - | [] -> List.rev acc - in aux [] l - let list_of_local_binders l = let rec aux acc = function Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl @@ -176,25 +168,29 @@ let rec gen_rels = function 0 -> [] | n -> mkRel n :: gen_rels (pred n) +let split_args n rel = match list_chop ((List.length rel) - n) rel with + (l1, x :: l2) -> l1, x, l2 + | _ -> assert(false) + 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 prn = Printer.pr_named_context env in - let pr_rel env = Printer.pr_rel_context env in let nc = named_context env in let nc_len = named_context_length nc 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 " : " ++ - Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++ - Ppconstr.pr_constr_expr body) - with _ -> () - 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 " : " ++ *) +(* 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 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 @@ -226,15 +222,14 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = in let argid' = id_of_string (string_of_id argid ^ "'") in let wfarg len = (Name argid', None, - mkSubset (Name argid') argtyp + mkSubset (Name argid') (lift len argtyp) (wf_rel_fun (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 _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 ; @@ -243,32 +238,32 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = mkRel 1 |]) in - (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ()); + (* (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 _ -> ()); +(* (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 _ -> ()); +(* (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 _ -> ()); +(* (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 _ -> ()); +(* (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 _ = *) +(* 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 @@ -292,53 +287,48 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = 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 _ = 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 _ = 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 - (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 _ -> ()); - trace (str "Adding to obligations list"); - Subtac_obligations.add_entry recname evars_def fullctyp evars; - trace (str "Added to obligations list") -(* + (* (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 build_mutrec l boxed = - let sigma = Evd.empty - and env0 = Global.env() - in + let sigma = Evd.empty and env = Global.env () in + let nc = named_context env in + let nc_len = named_context_length nc in let lnameargsardef = - (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*) + (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env protos (f, d))*) 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 *) - let (rec_sign,rec_impls,arityl) = + let (rec_sign,rec_env,rec_impls,arityl) = List.fold_left - (fun (env,impls,arl) ((recname, n, bl,arityc,body),_) -> + (fun (sign,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 arity = interp_type isevars env arityc in let impl = if Impargs.is_implicit_args() - then Impargs.compute_implicits env0 arity + then Impargs.compute_implicits env 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 + ((recname,None,arity) :: sign, Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)) + ([],env,[],[]) lnameargsardef in let arityl = List.rev arityl in let notations = List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) @@ -357,11 +347,11 @@ let build_mutrec l boxed = match info with None -> let def = abstract_constr_expr def bl in - isevars, info, interp_casted_constr isevars rec_sign ~impls:([],rec_impls) + isevars, info, interp_casted_constr isevars rec_env ~impls:([],rec_impls) def arity | Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) -> - let rec_sign = push_rel_context fun_bl rec_sign in - let cstr = interp_casted_constr isevars rec_sign ~impls:([],rec_impls) + let rec_env = push_rel_context fun_bl rec_env in + let cstr = interp_casted_constr isevars rec_env ~impls:([],rec_impls) def intern_arity in isevars, info, it_mkLambda_or_LetIn cstr fun_bl) lnameargsardef arityl @@ -369,162 +359,33 @@ let build_mutrec l boxed = States.unfreeze fs; raise e in States.unfreeze fs; def in - let (lnonrec,(namerec,defrec,arrec,nvrec)) = - collect_non_rec env0 lrecnames recdef arityl nv in - let declare arrec defrec = - let recvec = - Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in - let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in - let rec declare i fi = - (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++ - my_print_constr env0 (recvec.(i))); - with _ -> ()); - let ce = - { const_entry_body = mkFix ((nvrec,i),recdecls); - const_entry_type = Some arrec.(i); - const_entry_opaque = false; - const_entry_boxed = boxed} in - let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint) - in (ConstRef kn) - in - (* declare the recursive definitions *) - let lrefrec = Array.mapi declare namerec in - Options.if_verbose ppnl (recursive_message lrefrec); - - - (*(* The others are declared as normal definitions *) - let var_subst id = (id, Constrintern.global_reference id) in - let _ = - List.fold_left - (fun subst (f,def,t) -> - let ce = { const_entry_body = replace_vars subst def; - const_entry_type = Some t; - const_entry_opaque = false; - const_entry_boxed = boxed } in - let _ = - Declare.declare_constant f (DefinitionEntry ce,IsDefinition Definition) - in - warning ((string_of_id f)^" is non-recursively defined"); - (var_subst f) :: subst) - (List.map var_subst (Array.to_list namerec)) - lnonrec - in*) - List.iter (fun (df,c,scope) -> - Metasyntax.add_notation_interpretation df [] c scope) notations - in - let declare l = - let recvec = Array.of_list l - and arrec = Array.map pi3 arrec - in declare arrec recvec - in + collect_non_rec env lrecnames recdef arityl nv in let recdefs = Array.length defrec in - trace (int recdefs ++ str " recursive definitions"); (* Solve remaining evars *) let rec collect_evars i acc = if i < recdefs then let (isevars, info, def) = defrec.(i) in - let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () 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 isevars = Evd.undefined_evars !isevars in - let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () 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 *) + (* Generalize by the recursive prototypes *) let def = - Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign) + Termops.it_mkNamedLambda_or_LetIn def rec_sign and typ = - Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) + Termops.it_mkNamedProd_or_LetIn typ rec_sign in - let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in - (*let evars_typ = match evars_typ with Some t -> t | None -> assert(false) in*) - (*let fi = id_of_string (string_of_id id ^ "_evars") in*) - (*let ce = - { const_entry_body = evars_def; - const_entry_type = Some evars_typ; - const_entry_opaque = false; - const_entry_boxed = boxed} in - let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Definition) in - definition_message fi; - trace (str (string_of_id fi) ++ str " is defined");*) - let evar_sum = - if evars = [] then None - else ( - (try trace (str "Building evars sum for : "); - List.iter - (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env0 t)) - evars; - with _ -> ()); - let sum = Subtac_utils.build_dependent_sum evars in - (try trace (str "Evars sum: " ++ my_print_constr env0 (snd sum)); - with _ -> ()); - Some sum) - in - collect_evars (succ i) ((id, evars_def, evar_sum) :: acc) + let evars, def = Eterm.eterm_obligations id nc_len evm def (Some typ) in + collect_evars (succ i) ((id, def, typ, evars) :: acc) else acc in let defs = collect_evars 0 [] in - - (* Solve evars then create the definitions *) - let real_evars = - filter_map (fun (id, kn, sum) -> - 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 ++ - str "type: " ++ my_print_constr (Global.env ()) (Global.type_of_global gr)) in - let constant = match gr with Libnames.ConstRef c -> c - | _ -> assert(false) - in - try - (*let value = Environ.constant_value (Global.env ()) constant in*) - let pis = f (mkConst constant) in - (try (trace (str "Accessors: " ++ - List.fold_right (fun (_, _, _, c) acc -> my_print_constr env0 c ++ spc () ++ acc) - pis (mt())); - trace (str "Applied existentials: " ++ - (List.fold_right - (fun (id, kn, sumg, pi) acc -> - let args = Subtac_utils.destruct_ex pi sumg in - my_print_constr env0 (mkApp (kn, Array.of_list args))) - pis (mt ())))) - with _ -> ()); - let rec aux pis acc = function - (id, kn, sum) :: tl -> - (match sum with - None -> aux pis (kn :: acc) tl - | Some (_, sumg) -> - let (id, kn, sumg, pi), pis = List.hd pis, List.tl pis in - let args = Subtac_utils.destruct_ex pi sumg in - let args = - List.map (fun c -> - try Reductionops.whd_betadeltaiota (Global.env ()) Evd.empty c - with Not_found -> - trace (str "Not_found while reducing " ++ - my_print_constr (Global.env ()) c); - c - ) args - in - let _, newdef = decompose_lam_n (recdefs + List.length args) kn in - let constr = Term.substl (mkRel 1 :: List.rev args) newdef in - aux pis (constr :: acc) tl) - | [] -> List.rev acc - in - declare (aux pis [] defs) - with Environ.NotEvaluableConst cer -> - match cer with - Environ.NoBody -> trace (str "Constant has no body") - | Environ.Opaque -> trace (str "Constant is opaque") - ) -*) + Subtac_obligations.add_mutual_definitions (List.rev defs) nvrec + let out_n = function Some n -> n | None -> 0 @@ -544,8 +405,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed errorlabstrm "Subtac_command.build_recursive" (str "Well-founded fixpoints not allowed in mutually recursive blocks")) lnameargsardef - in assert(false) - (*build_mutrec lnameargsardef boxed*) + in build_mutrec lnameargsardef boxed |