From 6b9a9124d3bd24fe9305df613547139f6f609c60 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Aug 2017 16:15:57 +0200 Subject: Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr. The motivations are: - To reflect the concrete syntax more closely. - To factorize the different places where "contexts" are internalized: before this patch, there is a different treatment of `Definition f '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack to interpret `Definition f `pat := c : t`. With the patch, the fix to avoid seeing a variable named `pat` works for both `fun 'x => ...` and `Definition f 'x := ...`. The drawbacks are: - Counterpart to reflecting the concrete syntax more closerly, there are more redundancies in the syntax. For instance, the case `CLetIn (na,b,t,c)` can appears also in the form `CProdN (CLocalDef (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`. - Changes in the API, hence adaptation of plugins referring to `constr_expr` needed. --- printing/ppconstr.ml | 68 ++------------------------------------------------- printing/ppconstr.mli | 8 ------ 2 files changed, 2 insertions(+), 74 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 1146b42a0..c58d9eb9a 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -394,68 +394,6 @@ let tag_var = tag Tag.variable if is_open then pr_delimited_binders pr_com_at sep pr_c else pr_undelimited_binders sep pr_c - let rec extract_prod_binders = let open CAst in function - (* | CLetIn (loc,na,b,c) as x -> - let bl,c = extract_prod_binders c in - if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) - | { v = CProdN ([],c) } -> - extract_prod_binders c - | { loc; v = CProdN ([[_,Name id],bk,t], - { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} ) } - when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) -> - let bl,c = extract_prod_binders b in - CLocalPattern (loc, (p,None)) :: bl, c - | { loc; v = CProdN ((nal,bk,t)::bl,c) } -> - let bl,c = extract_prod_binders (CAst.make ?loc @@ CProdN(bl,c)) in - CLocalAssum (nal,bk,t) :: bl, c - | c -> [], c - - let rec extract_lam_binders ce = let open CAst in match ce.v with - (* | CLetIn (loc,na,b,c) as x -> - let bl,c = extract_lam_binders c in - if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) - | CLambdaN ([],c) -> - extract_lam_binders c - | CLambdaN ([[_,Name id],bk,t], - { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} ) - when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) -> - let bl,c = extract_lam_binders b in - CLocalPattern (ce.loc,(p,None)) :: bl, c - | CLambdaN ((nal,bk,t)::bl,c) -> - let bl,c = extract_lam_binders (CAst.make ?loc:ce.loc @@ CLambdaN(bl,c)) in - CLocalAssum (nal,bk,t) :: bl, c - | _ -> [], ce - - let split_lambda = CAst.with_loc_val (fun ?loc -> function - | CLambdaN ([[na],bk,t],c) -> (na,t,c) - | CLambdaN (([na],bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN(bl,c)) - | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN((nal,bk,t)::bl,c)) - | _ -> anomaly (Pp.str "ill-formed fixpoint body.") - ) - - let rename na na' t c = - match (na,na') with - | (_,Name id), (_,Name id') -> - (na',t,replace_vars_constr_expr (Id.Map.singleton id id') c) - | (_,Name id), (_,Anonymous) -> (na,t,c) - | _ -> (na',t,c) - - let split_product na' = CAst.with_loc_val (fun ?loc -> function - | CProdN ([[na],bk,t],c) -> rename na na' t c - | CProdN (([na],bk,t)::bl,c) -> rename na na' t (CAst.make ?loc @@ CProdN(bl,c)) - | CProdN ((na::nal,bk,t)::bl,c) -> - rename na na' t (CAst.make ?loc @@ CProdN((nal,bk,t)::bl,c)) - | _ -> anomaly (Pp.str "ill-formed fixpoint body.") - ) - - let rec split_fix n typ def = - if Int.equal n 0 then ([],typ,def) - else - let (na,_,def) = split_lambda def in - let (na,t,typ) = split_product na typ in - let (bl,typ,def) = split_fix (n-1) typ def in - (CLocalAssum ([na],default_binder_kind,t)::bl,typ,def) - let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = let pr_body = if dangling_with_for then pr_dangling else pr in @@ -574,8 +512,7 @@ let tag_var = tag Tag.variable (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix), lfix ) - | CProdN _ -> - let (bl,a) = extract_prod_binders a in + | CProdN (bl,a) -> return ( hov 0 ( hov 2 (pr_delimited_binders pr_forall spc @@ -583,8 +520,7 @@ let tag_var = tag Tag.variable str "," ++ pr spc ltop a), lprod ) - | CLambdaN _ -> - let (bl,a) = extract_lam_binders a in + | CLambdaN (bl,a) -> return ( hov 0 ( hov 2 (pr_delimited_binders pr_fun spc diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 1320cce9b..158906dd2 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -17,14 +17,6 @@ open Names open Misctypes open Notation_term -val extract_lam_binders : - constr_expr -> local_binder_expr list * constr_expr -val extract_prod_binders : - constr_expr -> local_binder_expr list * constr_expr -val split_fix : - int -> constr_expr -> constr_expr -> - local_binder_expr list * constr_expr * constr_expr - val prec_less : precedence -> tolerability -> bool val pr_tight_coma : unit -> Pp.t -- cgit v1.2.3