diff options
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 4 | ||||
-rw-r--r-- | plugins/funind/glob_termops.ml | 6 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 2 |
3 files changed, 11 insertions, 1 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 0b929b8ca..f7639d22d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -591,6 +591,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) build_entry_lc env funnames avoid (mkGApp(b,args)) | GRec _ -> user_err Pp.(str "Not handled GRec") + | GProj _ -> user_err Pp.(str "Funind does not support primitive projections") | GProd _ -> user_err Pp.(str "Cannot apply a type") end (* end of the application treatement *) @@ -697,6 +698,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,_) -> build_entry_lc env funnames avoid b + | GProj(_,_) -> user_err Pp.(str "Funind does not support primitive projections") and build_entry_lc_from_case env funname make_discr (el:tomatch_tuples) (brl:Glob_term.cases_clauses) avoid : @@ -1245,7 +1247,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function discrimination ones *) | GSort _ -> params | GHole _ -> params - | GIf _ | GRec _ | GCast _ -> + | GIf _ | GRec _ | GCast _ | GProj _ -> raise (UserError(Some "compute_cst_params", str "Not handled case")) ) gt and compute_cst_params_from_app acc (params,rtl) = diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index be8abb92e..b4ca1073c 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -109,6 +109,7 @@ let change_vars = | GCast(b,c) -> GCast(change_vars mapping b, Miscops.map_cast_type (change_vars mapping) c) + | GProj(p,c) -> GProj(p, change_vars mapping c) ) rt and change_vars_br mapping ((loc,(idl,patl,res)) as br) = let new_mapping = List.fold_right Id.Map.remove idl mapping in @@ -293,6 +294,7 @@ let rec alpha_rt excluded rt = GApp(alpha_rt excluded f, List.map (alpha_rt excluded) args ) + | GProj(p,c) -> GProj(p, alpha_rt excluded c) in new_rt @@ -344,6 +346,7 @@ let is_free_in id = | GHole _ -> false | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t | GCast (b,CastCoerce) -> is_free_in b + | GProj (_,c) -> is_free_in c ) x and is_free_in_br (_,(ids,_,rt)) = (not (Id.List.mem id ids)) && is_free_in rt @@ -437,6 +440,8 @@ let replace_var_by_term x_id term = | GCast(b,c) -> GCast(replace_var_by_pattern b, Miscops.map_cast_type replace_var_by_pattern c) + | GProj(p,c) -> + GProj(p,replace_var_by_pattern c) ) x and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) = if List.exists (fun id -> Id.compare id x_id == 0) idl @@ -540,6 +545,7 @@ let expand_as = | GCases(sty,po,el,brl) -> GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) + | GProj(p,c) -> GProj(p, expand_as map c) ) and expand_as_br map (loc,(idl,cpl,rt)) = (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt)) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 071bab2f3..58154d310 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -215,6 +215,7 @@ let is_rec names = | GCases(_,_,el,brl) -> List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl + | GProj(_,c) -> lookup names c and lookup_br names (_,(idl,_,rt)) = let new_names = List.fold_right Id.Set.remove idl names in lookup new_names rt @@ -779,6 +780,7 @@ let rec add_args id new_args = CAst.map (function | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.") | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.") | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.") + | CProj _ -> user_err Pp.(str "Funind does not support primitive projections") ) exception Stop of Constrexpr.constr_expr |