aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/funind/rawterm_to_relation.ml355
-rw-r--r--contrib/funind/rawtermops.ml24
-rw-r--r--contrib/funind/rawtermops.mli4
3 files changed, 233 insertions, 150 deletions
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index a60a4f4fc..ba60f49ed 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -9,11 +9,11 @@ open Util
open Rawtermops
let observe strm =
- if Tacinterp.get_debug () <> Tactic_debug.DebugOff && false
+ if Tacinterp.get_debug () <> Tactic_debug.DebugOff
then Pp.msgnl strm
else ()
let observennl strm =
- if Tacinterp.get_debug () <> Tactic_debug.DebugOff &&false
+ if Tacinterp.get_debug () <> Tactic_debug.DebugOff
then Pp.msg strm
else ()
@@ -295,7 +295,7 @@ let pr_name = function
(**********************************************************************)
(* [build_constructors_of_type] construct the array of pattern of its inductive argument*)
-let build_constructors_of_type msg ind' argl =
+let build_constructors_of_type ind' argl =
let (mib,ind) = Inductive.lookup_mind_specif (Global.env()) ind' in
let npar = mib.Declarations.mind_nparams in
Array.mapi (fun i _ ->
@@ -324,15 +324,6 @@ let build_constructors_of_type msg ind' argl =
)
ind.Declarations.mind_consnames
-(* construction of the branches from an inductive*)
-let find_constructors_of_raw_type msg t argl : Rawterm.cases_pattern array =
- let ind,args = raw_decompose_app t in
- match ind with
- | RRef(_,IndRef ind') ->
- build_constructors_of_type msg ind' argl
- | _ -> error msg
-
-
(* [find_type_of] very naive attempts to discover the type of an if or a letin *)
let rec find_type_of nb b =
let f,_ = raw_decompose_app b in
@@ -371,6 +362,60 @@ let rec find_type_of nb b =
(* Main functions *)
(******************)
+
+
+let raw_push_named (na,raw_value,raw_typ) env =
+ match na with
+ | Anonymous -> env
+ | Name id ->
+ let value = Util.option_map (Pretyping.Default.understand Evd.empty env) raw_value in
+ let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in
+ Environ.push_named (id,value,typ) env
+
+
+let add_pat_variables pat typ env : Environ.env =
+ let rec add_pat_variables env pat typ : Environ.env =
+ observe (str "new rel env := " ++ Printer.pr_rel_context_of env);
+
+ match pat with
+ | PatVar(_,na) -> Environ.push_rel (na,None,typ) env
+ | PatCstr(_,c,patl,na) ->
+ let Inductiveops.IndType(indf,indargs) =
+ try Inductiveops.find_rectype env Evd.empty typ
+ with Not_found -> assert false
+ in
+ let constructors = Inductiveops.get_constructors env indf in
+ let constructor : Inductiveops.constructor_summary = List.find (fun cs -> cs.Inductiveops.cs_cstr = c) (Array.to_list constructors) in
+ let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
+ List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
+ in
+ let new_env = add_pat_variables env pat typ in
+ let res =
+ fst (
+ Sign.fold_rel_context
+ (fun (na,v,t) (env,ctxt) ->
+ match na with
+ | Anonymous -> assert false
+ | Name id ->
+ let new_t = substl ctxt t in
+ let new_v = option_map (substl ctxt) v in
+ observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
+ str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
+ str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
+ option_fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
+ option_fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
+ );
+ (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt)
+ )
+ (Environ.rel_context new_env)
+ ~init:(env,[])
+ )
+ in
+ observe (str "new var env := " ++ Printer.pr_named_context_of res);
+ res
+
+
+
(* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return)
of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the
corresponding graphs.
@@ -403,8 +448,8 @@ let rec find_type_of nb b =
*)
-let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
-(* Pp.msgnl (str " Entering : " ++ Printer.pr_rawconstr rt); *)
+let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return =
+ observe (str " Entering : " ++ Printer.pr_rawconstr rt);
match rt with
| RRef _ | RVar _ | REvar _ | RPatVar _ | RSort _ | RHole _ ->
(* do nothing (except changing type of course) *)
@@ -414,8 +459,8 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
let args_res : (rawconstr list) build_entry_return =
List.fold_right (* create the arguments lists of constructors and combine them *)
(fun arg ctxt_argsl ->
- let arg_res = build_entry_lc funnames ctxt_argsl.to_avoid arg in
- combine_results combine_args arg_res ctxt_argsl
+ let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in
+ combine_results combine_args arg_res ctxt_argsl
)
args
(mk_result [] [] avoid)
@@ -430,6 +475,9 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
a pseudo value "v1 ... vn".
The "value" of this branch is then simply [res]
*)
+ let rt_as_constr = Pretyping.Default.understand Evd.empty env rt in
+ let rt_typ = Typing.type_of env Evd.empty rt_as_constr in
+ let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in
let res = fresh_id args_res.to_avoid "res" in
let new_avoid = res::args_res.to_avoid in
let res_rt = mkRVar res in
@@ -437,7 +485,7 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
List.map
(fun arg_res ->
let new_hyps =
- [Prod (Name res),mkRHole ();
+ [Prod (Name res),res_raw_type;
Prod Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)]
in
{context = arg_res.context@new_hyps; value = res_rt }
@@ -481,6 +529,7 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
| _ -> n,b,avoid
in
build_entry_lc
+ env
funnames
avoid
(mkRLetIn(new_n,t,mkRApp(new_b,args)))
@@ -489,7 +538,7 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
we first compute the result from the case and
then combine each of them with each of args one
*)
- let f_res = build_entry_lc funnames args_res.to_avoid f in
+ let f_res = build_entry_lc env funnames args_res.to_avoid f in
combine_results combine_app f_res args_res
| RDynamic _ ->error "Not handled RDynamic"
| RCast(_,b,_,_) ->
@@ -498,7 +547,7 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
WARNING: We need to restart since [b] itself should be an application term
*)
- build_entry_lc funnames avoid (mkRApp(b,args))
+ build_entry_lc env funnames avoid (mkRApp(b,args))
| RRec _ -> error "Not handled RRec"
| RProd _ -> error "Cannot apply a type"
end (* end of the application treatement *)
@@ -509,13 +558,14 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
then the one corresponding to the type
and combine the two result
*)
- let b_res = build_entry_lc funnames avoid b in
- let t_res = build_entry_lc funnames avoid t in
+ let t_res = build_entry_lc env funnames avoid t in
let new_n =
match n with
| Name _ -> n
| Anonymous -> Name (Indfun_common.fresh_id [] "_x")
in
+ let new_env = raw_push_named (new_n,None,t) env in
+ let b_res = build_entry_lc new_env funnames avoid b in
combine_results (combine_lam new_n) t_res b_res
| RProd(_,n,t,b) ->
(* we first compute the list of constructor
@@ -523,106 +573,88 @@ let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return =
then the one corresponding to the type
and combine the two result
*)
- let b_res = build_entry_lc funnames avoid b in
- let t_res = build_entry_lc funnames avoid t in
+ let t_res = build_entry_lc env funnames avoid t in
+ let new_env = raw_push_named (n,None,t) env in
+ let b_res = build_entry_lc new_env funnames avoid b in
combine_results (combine_prod n) t_res b_res
- | RLetIn(_,n,t,b) ->
+ | RLetIn(_,n,v,b) ->
(* we first compute the list of constructor
corresponding to the body of the function,
then the one corresponding to the value [t]
and combine the two result
*)
- let b_res = build_entry_lc funnames avoid b in
- let t_res = build_entry_lc funnames avoid t in
- combine_results (combine_letin n) t_res b_res
+ let v_res = build_entry_lc env funnames avoid v in
+ let v_as_constr = Pretyping.Default.understand Evd.empty env v in
+ let v_type = Typing.type_of env Evd.empty v_as_constr in
+ let new_env =
+ match n with
+ Anonymous -> env
+ | Name id -> Environ.push_named (id,Some v_as_constr,v_type) env
+ in
+ let b_res = build_entry_lc new_env funnames avoid b in
+ combine_results (combine_letin n) v_res b_res
| RCases(_,_,el,brl) ->
(* we create the discrimination function
and treat the case itself
*)
let make_discr = make_discr_match brl in
- build_entry_lc_from_case funnames make_discr el brl avoid
+ build_entry_lc_from_case env funnames make_discr el brl avoid
| RIf(_,b,(na,e_option),lhs,rhs) ->
- (* Same as RCases but we need to compute the branches *)
- begin
- match b with
- | RCast(_,b,_,t) ->
- let msg = "If construction must be used with cast" in
- let case_pat = find_constructors_of_raw_type msg t [] in
- assert (Array.length case_pat = 2);
- let brl =
- list_map_i
- (fun i x -> (dummy_loc,[],[case_pat.(i)],x))
- 0
- [lhs;rhs]
- in
- let match_expr =
- mkRCases(None,[(b,(Anonymous,None))],brl)
- in
-(* Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *)
- build_entry_lc funnames avoid match_expr
- | _ ->
- try
- let ind = find_type_of 2 b in
- let case_pat = build_constructors_of_type (str "") ind [] in
- let brl =
- list_map_i
- (fun i x -> (dummy_loc,[],[case_pat.(i)],x))
- 0
- [lhs;rhs]
- in
- let match_expr =
- mkRCases(None,[(b,(Anonymous,None))],brl)
- in
- (* Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *)
- build_entry_lc funnames avoid match_expr
- with Invalid_argument s ->
- let msg = "If construction must be used with cast : "^ s in
- error msg
-
- end
+ let b_as_constr = Pretyping.Default.understand Evd.empty env b in
+ let b_typ = Typing.type_of env Evd.empty b_as_constr in
+ let (ind,_) =
+ try Inductiveops.find_inductive env Evd.empty b_typ
+ with Not_found ->
+ errorlabstrm "" (str "Cannot find the inductive associated to " ++
+ Printer.pr_rawconstr b ++ str " in " ++
+ Printer.pr_rawconstr rt ++ str ". try again with a cast")
+ in
+ let case_pats = build_constructors_of_type ind [] in
+ assert (Array.length case_pats = 2);
+ let brl =
+ list_map_i
+ (fun i x -> (dummy_loc,[],[case_pats.(i)],x))
+ 0
+ [lhs;rhs]
+ in
+ let match_expr =
+ mkRCases(None,[(b,(Anonymous,None))],brl)
+ in
+ (* Pp.msgnl (str "new case := " ++ Printer.pr_rawconstr match_expr); *)
+ build_entry_lc env funnames avoid match_expr
| RLetTuple(_,nal,_,b,e) ->
- begin
- (* Same as RCases but we need to compute the branches *)
- let nal_as_rawconstr =
- List.map
- (function
- Name id -> mkRVar id
+ begin
+ let nal_as_rawconstr =
+ List.map
+ (function
+ Name id -> mkRVar id
| Anonymous -> mkRHole ()
)
- nal
+ nal
in
- match b with
- | RCast(_,b,_,t) ->
- let case_pat =
- find_constructors_of_raw_type
- "LetTuple construction must be used with cast" t nal_as_rawconstr in
- assert (Array.length case_pat = 1);
- let br =
- (dummy_loc,[],[case_pat.(0)],e)
- in
- let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in
- build_entry_lc funnames avoid match_expr
- | _ ->
- try
- let ind = find_type_of 1 b in
- let case_pat =
- build_constructors_of_type
- (str "LetTuple construction must be used with cast") ind nal_as_rawconstr in
- let br =
- (dummy_loc,[],[case_pat.(0)],e)
- in
- let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in
- build_entry_lc funnames avoid match_expr
- with Invalid_argument s ->
- let msg = "LetTuple construction must be used with cast : "^ s in
- error msg
-
+ let b_as_constr = Pretyping.Default.understand Evd.empty env b in
+ let b_typ = Typing.type_of env Evd.empty b_as_constr in
+ let (ind,_) =
+ try Inductiveops.find_inductive env Evd.empty b_typ
+ with Not_found ->
+ errorlabstrm "" (str "Cannot find the inductive associated to " ++
+ Printer.pr_rawconstr b ++ str " in " ++
+ Printer.pr_rawconstr rt ++ str ". try again with a cast")
+ in
+ let case_pats = build_constructors_of_type ind nal_as_rawconstr in
+ assert (Array.length case_pats = 1);
+ let br =
+ (dummy_loc,[],[case_pats.(0)],e)
+ in
+ let match_expr = mkRCases(None,[b,(Anonymous,None)],[br]) in
+ build_entry_lc env funnames avoid match_expr
+
end
| RRec _ -> error "Not handled RRec"
| RCast(_,b,_,_) ->
- build_entry_lc funnames avoid b
+ build_entry_lc env funnames avoid b
| RDynamic _ -> error "Not handled RDynamic"
-and build_entry_lc_from_case funname make_discr
+and build_entry_lc_from_case env funname make_discr
(el:tomatch_tuple)
(brl:Rawterm.cases_clauses) avoid :
rawconstr build_entry_return =
@@ -640,15 +672,26 @@ and build_entry_lc_from_case funname make_discr
let case_resl =
List.fold_right
(fun (case_arg,_) ctxt_argsl ->
- let arg_res = build_entry_lc funname avoid case_arg in
+ let arg_res = build_entry_lc env funname avoid case_arg in
combine_results combine_args arg_res ctxt_argsl
)
el
(mk_result [] [] avoid)
in
+ (****** The next works only if the match is not dependent ****)
+ let types =
+ List.map (fun (case_arg,_) ->
+ let case_arg_as_constr = Pretyping.Default.understand Evd.empty env case_arg in
+ Typing.type_of env Evd.empty case_arg_as_constr
+ ) el
+ in
let results =
List.map
- (build_entry_lc_from_case_term funname (make_discr (List.map fst el)) [] brl case_resl.to_avoid)
+ (build_entry_lc_from_case_term
+ env types
+ funname (make_discr (List.map fst el))
+ [] brl
+ case_resl.to_avoid)
case_resl.result
in
{
@@ -657,7 +700,7 @@ and build_entry_lc_from_case funname make_discr
List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results
}
-and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avoid
+and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid
matched_expr =
match brl with
| [] -> (* computed_branches *) {result = [];to_avoid = avoid}
@@ -668,18 +711,26 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
(* building a list of precondition stating that we are not in this branch
(will be used in the following recursive calls)
*)
+ let new_env = List.fold_right2 add_pat_variables patl types env in
let not_those_patterns : (identifier list -> rawconstr -> rawconstr) list =
- List.map
- (fun pat ->
+ List.map2
+ (fun pat typ ->
fun avoid pat'_as_term ->
let renamed_pat,_,_ = alpha_pat avoid pat in
let pat_ids = get_pattern_id renamed_pat in
- List.fold_right
- (fun id acc -> mkRProd (Name id,mkRHole (),acc))
+ let env_with_pat_ids = add_pat_variables pat typ new_env in
+ List.fold_right
+ (fun id acc ->
+ let typ_of_id = Typing.type_of env_with_pat_ids Evd.empty (mkVar id) in
+ let raw_typ_of_id =
+ Detyping.detype false [] (Termops.names_of_rel_context env_with_pat_ids) typ_of_id
+ in
+ mkRProd (Name id,raw_typ_of_id,acc))
pat_ids
(raw_make_neq pat'_as_term (pattern_to_term renamed_pat))
)
patl
+ types
in
(* Checking if we can be in this branch
(will be used in the following recursive calls)
@@ -695,6 +746,8 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
*)
let brl'_res =
build_entry_lc_from_case_term
+ env
+ types
funname
make_discr
((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent)
@@ -712,22 +765,30 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
let those_pattern_preconds =
(List.flatten
(
- List.map2
- (fun pat e ->
+ list_map3
+ (fun pat e typ_as_constr ->
let this_pat_ids = ids_of_pat pat in
+ let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr in
let pat_as_term = pattern_to_term pat in
List.fold_right
(fun id acc ->
if Idset.mem id this_pat_ids
- then (Prod (Name id),mkRHole ())::acc
+ then (Prod (Name id),
+ let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in
+ let raw_typ_of_id =
+ Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_of_id
+ in
+ raw_typ_of_id
+ )::acc
else acc
)
idl
- [(Prod Anonymous,raw_make_eq pat_as_term e)]
+ [(Prod Anonymous,raw_make_eq ~typ pat_as_term e)]
)
patl
matched_expr.value
+ types
)
)
@
@@ -738,13 +799,13 @@ and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avo
List.for_all (fun x -> x) unif) patterns_to_prevent
then
let i = List.length patterns_to_prevent in
- [(Prod Anonymous,make_discr i )]
+ [(Prod Anonymous,make_discr i )]
else
[]
)
in
(* We compute the result of the value returned by the branch*)
- let return_res = build_entry_lc funname new_avoid return in
+ let return_res = build_entry_lc new_env funname new_avoid return in
(* and combine it with the preconds computed for this branch *)
let this_branch_res =
List.map
@@ -796,7 +857,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
assert false
end
| RApp(_,RRef(_,eq_as_ref),[_;RVar(_,id);rt])
- when eq_as_ref = Lazy.force Coqlib.coq_eq_ref
+ when eq_as_ref = Lazy.force Coqlib.coq_eq_ref && n = Anonymous
->
let is_in_b = is_free_in id b in
let _keep_eq =
@@ -997,14 +1058,34 @@ let build_inductive
let relnames = Array.map mk_rel_id funnames in
let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in
(* Construction of the pseudo constructors *)
- let resa = Array.map (build_entry_lc funnames_as_set []) rta in
+ let env =
+ Array.fold_right
+ (fun id env ->
+ Environ.push_named (id,None,Typing.type_of env Evd.empty (Tacinterp.constr_of_id env id)) env
+ )
+ funnames
+ (Global.env ())
+ in
+ let resa = Array.map (build_entry_lc env funnames_as_set []) rta in
(* and of the real constructors*)
let constr i res =
List.map
(function result (* (args',concl') *) ->
let rt = compose_raw_context result.context result.value in
let nb_args = List.length funsargs.(i) in
-(* Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
+(* let old_implicit_args = Impargs.is_implicit_args () *)
+(* and old_strict_implicit_args = Impargs.is_strict_implicit_args () *)
+(* and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in *)
+(* let old_rawprint = !Options.raw_print in *)
+(* Options.raw_print := true; *)
+(* Impargs.make_implicit_args false; *)
+(* Impargs.make_strict_implicit_args false; *)
+(* Impargs.make_contextual_implicit_args false; *)
+(* Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
+(* Impargs.make_implicit_args old_implicit_args; *)
+(* Impargs.make_strict_implicit_args old_strict_implicit_args; *)
+(* Impargs.make_contextual_implicit_args old_contextual_implicit_args; *)
+(* Options.raw_print := old_rawprint; *)
fst (
rebuild_cons nb_args relnames.(i)
[]
@@ -1096,26 +1177,26 @@ let build_inductive
in
let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in
let rel_inds = Array.to_list ext_rel_constructors in
- let _ =
- observe (
- str "Inductive" ++ spc () ++
- prlist_with_sep
- (fun () -> fnl ()++spc () ++ str "with" ++ spc ())
- (function ((_,id),_,params,ar,constr) ->
- Ppconstr.pr_id id ++ spc () ++
- Ppconstr.pr_binders params ++ spc () ++
- str ":" ++ spc () ++
- Ppconstr.pr_lconstr_expr ar ++ spc () ++
- prlist_with_sep
- (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ())
- (function (_,((_,id),t)) ->
- Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++
- Ppconstr.pr_lconstr_expr t)
- constr
- )
- rel_inds
- )
- in
+(* let _ = *)
+(* Pp.msgnl (\* observe *\) ( *)
+(* str "Inductive" ++ spc () ++ *)
+(* prlist_with_sep *)
+(* (fun () -> fnl ()++spc () ++ str "with" ++ spc ()) *)
+(* (function ((_,id),_,params,ar,constr) -> *)
+(* Ppconstr.pr_id id ++ spc () ++ *)
+(* Ppconstr.pr_binders params ++ spc () ++ *)
+(* str ":" ++ spc () ++ *)
+(* Ppconstr.pr_lconstr_expr ar ++ spc () ++ str ":=" ++ *)
+(* prlist_with_sep *)
+(* (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ()) *)
+(* (function (_,((_,id),t)) -> *)
+(* Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++ *)
+(* Ppconstr.pr_lconstr_expr t) *)
+(* constr *)
+(* ) *)
+(* rel_inds *)
+(* ) *)
+(* in *)
let old_implicit_args = Impargs.is_implicit_args ()
and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index 96b0e1eb7..204249f1d 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -18,7 +18,7 @@ let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
let mkRSort s = RSort(dummy_loc,s)
let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
-
+let mkRCast(b,t) = RCast(dummy_loc,b,CastCoerce,t)
(*
Some basic functions to decompose rawconstrs
@@ -49,8 +49,8 @@ let raw_decompose_app =
(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *)
-let raw_make_eq t1 t2 =
- mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[mkRHole ();t2;t1])
+let raw_make_eq ?(typ= mkRHole ()) t1 t2 =
+ mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1])
(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *)
let raw_make_neq t1 t2 =
@@ -386,30 +386,32 @@ let is_free_in id =
-let rec pattern_to_term = function
+let rec pattern_to_term = function
| PatVar(loc,Anonymous) -> assert false
- | PatVar(loc,Name id) ->
+ | PatVar(loc,Name id) ->
mkRVar id
- | PatCstr(loc,constr,patternl,_) ->
- let cst_narg =
+ | PatCstr(loc,constr,patternl,_) ->
+ let cst_narg =
Inductiveops.mis_constructor_nargs_env
(Global.env ())
constr
in
- let implicit_args =
- Array.to_list
- (Array.init
+ let implicit_args =
+ Array.to_list
+ (Array.init
(cst_narg - List.length patternl)
(fun _ -> mkRHole ())
)
in
- let patl_as_term =
+ let patl_as_term =
List.map pattern_to_term patternl
in
mkRApp(mkRRef(Libnames.ConstructRef constr),
implicit_args@patl_as_term
)
+
+
let replace_var_by_term x_id term =
let rec replace_var_by_pattern rt =
match rt with
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index 4df239e32..aa3554850 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -25,7 +25,7 @@ val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr
val mkRCases : rawconstr option * tomatch_tuple * cases_clauses -> rawconstr
val mkRSort : rawsort -> rawconstr
val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *)
-
+val mkRCast : rawconstr* rawconstr -> rawconstr
(*
Some basic functions to decompose rawconstrs
These are analogous to the ones constrs
@@ -36,7 +36,7 @@ val raw_decompose_app : rawconstr -> rawconstr*(rawconstr list)
(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *)
-val raw_make_eq : rawconstr -> rawconstr -> rawconstr
+val raw_make_eq : ?typ:rawconstr -> rawconstr -> rawconstr -> rawconstr
(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *)
val raw_make_neq : rawconstr -> rawconstr -> rawconstr
(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 08:46:09 +0000