summaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_command.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac/subtac_command.ml')
-rw-r--r--contrib/subtac/subtac_command.ml282
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 02:18:15 +0000