diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-21 19:02:56 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-21 19:02:56 +0100 |
commit | 4b0fe4e09d547f0e6ee98da3fd6f7a134e51f3fd (patch) | |
tree | 9550d5b99c9023c9c0ad84d2d7b89e05f344348b /plugins/funind | |
parent | 2f13806f10b2781f84417014c8018097c8e8b2ad (diff) | |
parent | 2aff5c40ba9b40b4e0188b799dde6f31585e356b (diff) |
Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 8 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 34 |
2 files changed, 22 insertions, 20 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index f7639d22d..693ab464d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1295,8 +1295,8 @@ let rec rebuild_return_type rt = CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t') | Constrexpr.CLetIn(na,v,t,t') -> CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') - | _ -> CAst.make ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous], - Constrexpr.Default Decl_kinds.Explicit, rt], + | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([Loc.tag Anonymous], + Constrexpr.Default Decl_kinds.Explicit, rt)], CAst.make @@ Constrexpr.CSort(GType [])) let do_build_inductive @@ -1356,7 +1356,7 @@ let do_build_inductive acc) | None -> CAst.make @@ Constrexpr.CProdN - ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], acc ) ) @@ -1423,7 +1423,7 @@ let do_build_inductive acc) | None -> CAst.make @@ Constrexpr.CProdN - ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], + ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], acc ) ) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 58154d310..96e4a94d3 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -591,11 +591,11 @@ and rebuild_nal aux bk bl' nal typ = match nal,typ with | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ | [], _ -> rebuild_bl aux bl' typ - | na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } -> + | na::nal,{ CAst.v = CProdN(CLocalAssum(na'::nal',bk',nal't)::rest,typ') } -> if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na') then let assum = CLocalAssum([na],bk,nal't) in - let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in + let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in rebuild_nal (assum::aux) bk @@ -604,7 +604,7 @@ and rebuild_nal aux bk bl' nal typ = (CAst.make @@ CProdN(new_rest,typ')) else let assum = CLocalAssum([na'],bk,nal't) in - let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in + let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in rebuild_nal (assum::aux) bk @@ -731,10 +731,14 @@ let rec add_args id new_args = CAst.map (function end | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.") | CProdN(nal,b1) -> - CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, + CProdN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) + | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t) + | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal, add_args id new_args b1) | CLambdaN(nal,b1) -> - CLambdaN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, + CLambdaN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) + | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t) + | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal, add_args id new_args b1) | CLetIn(na,b1,t,b2) -> CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) @@ -793,7 +797,7 @@ let rec chop_n_arrow n t = then t (* If we have already removed all the arrows then return the type *) else (* If not we check the form of [t] *) match t.CAst.v with - | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible : + | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, two results are possible : either we need to discard more than the number of arrows contained in this product declaration then we just recall [chop_n_arrow] on the remaining number of arrow to chop and [t'] we discard it and @@ -805,7 +809,7 @@ let rec chop_n_arrow n t = let new_n = let rec aux (n:int) = function [] -> n - | (nal,k,t'')::nal_ta' -> + | CLocalAssum(nal,k,t'')::nal_ta' -> let nal_l = List.length nal in if n >= nal_l then @@ -813,9 +817,10 @@ let rec chop_n_arrow n t = else let new_t' = CAst.make @@ Constrexpr.CProdN( - ((snd (List.chop n nal)),k,t'')::nal_ta',t') + CLocalAssum((snd (List.chop n nal)),k,t'')::nal_ta',t') in raise (Stop new_t') + | _ -> anomaly (Pp.str "Not enough products.") in aux n nal_ta' in @@ -828,16 +833,13 @@ let rec chop_n_arrow n t = let rec get_args b t : Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr = match b.CAst.v with - | Constrexpr.CLambdaN ((nal_ta), b') -> + | Constrexpr.CLambdaN (CLocalAssum(nal,k,ta) as d::rest, b') -> begin - let n = - (List.fold_left (fun n (nal,_,_) -> - n+List.length nal) 0 nal_ta ) - in - let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in - (List.map (fun (nal,k,ta) -> - (Constrexpr.CLocalAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' + let n = List.length nal in + let nal_tas,b'',t'' = get_args (CAst.make ?loc:b.CAst.loc @@ Constrexpr.CLambdaN (rest,b')) (chop_n_arrow n t) in + d :: nal_tas, b'',t'' end + | Constrexpr.CLambdaN ([], b) -> [],b,t | _ -> [],b,t |