From 84a5fc74efc30a2b2fca18726cf988edd356353e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 25 Sep 2008 15:39:26 +0000 Subject: [PATCH 1/1] beta expand --- .../components/ng_refiner/nCicUnification.ml | 226 ++++-------------- 1 file changed, 47 insertions(+), 179 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 29851b5d4..fa3ba4988 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -44,201 +44,69 @@ let eta_reduce after_beta_expansion after_beta_expansion_body = try match before_beta_expansion,after_beta_expansion_body with - Cic.Appl l, Cic.Appl l' -> - let rec all_but_last check_last = - function - [] -> assert false - | [Cic.Rel 1] -> [] + | NCic.Appl l1, NCic.Appl l2 -> + let rec all_but_last check_last = function + | [] -> assert false + | [NCic.Rel 1] -> [] | [_] -> if check_last then raise WrongShape else [] | he::tl -> he::(all_but_last check_last tl) in - let all_but_last check_last l = + let all_but_last check_last l = match all_but_last check_last l with - [] -> assert false - | [he] -> he - | l -> Cic.Appl l - in - let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in - let all_but_last = all_but_last false l in - (* here we should test alpha-equivalence; however we know by - construction that here alpha_equivalence is equivalent to = *) - if t = all_but_last then - all_but_last - else - after_beta_expansion - | _,_ -> after_beta_expansion - with - WrongShape -> after_beta_expansion + | [] -> assert false + | [he] -> he + | l -> NCic.Appl l + in + let t = + NCicSubstitution.subst (NCic.Sort NCic.Prop) (all_but_last true l2) in + let all_but_last = all_but_last false l in + if t = all_but_last then all_but_last else after_beta_expansion + | _ -> after_beta_expansion + with WrongShape -> after_beta_expansion +;; -let rec beta_expand num test_equality_only metasenv subst context t arg ugraph = - let module S = CicSubstitution in - let module C = Cic in -let foo () = - let rec aux metasenv subst n context t' ugraph = +let rec beta_expand num test_equality_only metasenv subst context t arg = + let rec aux (n,context as k) (metasenv, subst as acc) t' = try - - let subst,metasenv,ugraph1 = - fo_unif_subst test_equality_only subst context metasenv - (CicSubstitution.lift n arg) t' ugraph - + let metasenv, subst = + unify (* test_equality_only *) metasenv subst context + (NCicSubstitution.lift n arg) t' in - subst,metasenv,C.Rel (1 + n),ugraph1 - with - Uncertain _ - | UnificationFailure _ -> + (metasenv, subst), C.Rel (1 + n) + with Uncertain _ | UnificationFailure _ -> match t' with - | C.Rel m -> subst,metasenv, - (if m <= n then C.Rel m else C.Rel (m+1)),ugraph - | C.Var (uri,exp_named_subst) -> - let subst,metasenv,exp_named_subst',ugraph1 = - aux_exp_named_subst metasenv subst n context exp_named_subst ugraph - in - subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1 - | C.Meta (i,l) -> - (* andrea: in general, beta_expand can create badly typed - terms. This happens quite seldom in practice, UNLESS we - iterate on the local context. For this reason, we renounce - to iterate and just lift *) - let l = - List.map - (function - Some t -> Some (CicSubstitution.lift 1 t) - | None -> None) l in - subst, metasenv, C.Meta (i,l), ugraph - | C.Sort _ - | C.Implicit _ as t -> subst,metasenv,t,ugraph - | C.Cast (te,ty) -> - let subst,metasenv,te',ugraph1 = - aux metasenv subst n context te ugraph in - let subst,metasenv,ty',ugraph2 = - aux metasenv subst n context ty ugraph1 in - (* TASSI: sure this is in serial? *) - subst,metasenv,(C.Cast (te', ty')),ugraph2 - | C.Prod (nn,s,t) -> - let subst,metasenv,s',ugraph1 = - aux metasenv subst n context s ugraph in - let subst,metasenv,t',ugraph2 = - aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t - ugraph1 - in - (* TASSI: sure this is in serial? *) - subst,metasenv,(C.Prod (nn, s', t')),ugraph2 - | C.Lambda (nn,s,t) -> - let subst,metasenv,s',ugraph1 = - aux metasenv subst n context s ugraph in - let subst,metasenv,t',ugraph2 = - aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1 - in - (* TASSI: sure this is in serial? *) - subst,metasenv,(C.Lambda (nn, s', t')),ugraph2 - | C.LetIn (nn,s,ty,t) -> - let subst,metasenv,s',ugraph1 = - aux metasenv subst n context s ugraph in - let subst,metasenv,ty',ugraph1 = - aux metasenv subst n context ty ugraph in - let subst,metasenv,t',ugraph2 = - aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t - ugraph1 - in - (* TASSI: sure this is in serial? *) - subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2 - | C.Appl l -> - let subst,metasenv,revl',ugraph1 = - List.fold_left - (fun (subst,metasenv,appl,ugraph) t -> - let subst,metasenv,t',ugraph1 = - aux metasenv subst n context t ugraph in - subst,metasenv,(t'::appl),ugraph1 - ) (subst,metasenv,[],ugraph) l - in - subst,metasenv,(C.Appl (List.rev revl')),ugraph1 - | C.Const (uri,exp_named_subst) -> - let subst,metasenv,exp_named_subst',ugraph1 = - aux_exp_named_subst metasenv subst n context exp_named_subst ugraph - in - subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1 - | C.MutInd (uri,i,exp_named_subst) -> - let subst,metasenv,exp_named_subst',ugraph1 = - aux_exp_named_subst metasenv subst n context exp_named_subst ugraph - in - subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1 - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let subst,metasenv,exp_named_subst',ugraph1 = - aux_exp_named_subst metasenv subst n context exp_named_subst ugraph - in - subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1 - | C.MutCase (sp,i,outt,t,pl) -> - let subst,metasenv,outt',ugraph1 = - aux metasenv subst n context outt ugraph in - let subst,metasenv,t',ugraph2 = - aux metasenv subst n context t ugraph1 in - let subst,metasenv,revpl',ugraph3 = - List.fold_left - (fun (subst,metasenv,pl,ugraph) t -> - let subst,metasenv,t',ugraph1 = - aux metasenv subst n context t ugraph in - subst,metasenv,(t'::pl),ugraph1 - ) (subst,metasenv,[],ugraph2) pl - in - subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3 - (* TASSI: not sure this is serial *) - | C.Fix (i,fl) -> -(*CSC: not implemented - let tylen = List.length fl in - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo)) - fl - in - C.Fix (i, substitutedfl) -*) - subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph - | C.CoFix (i,fl) -> -(*CSC: not implemented - let tylen = List.length fl in - let substitutedfl = - List.map - (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo)) - fl - in - C.CoFix (i, substitutedfl) + | NCic.Rel m -> + (metasenv, subst), if m <= n then NCic.Rel m else NCic.Rel (m+1) + (* andrea: in general, beta_expand can create badly typed + terms. This happens quite seldom in practice, UNLESS we + iterate on the local context. For this reason, we renounce + to iterate and just lift *) + | NCic.Meta (i,(shift,lc)) -> + (metasenv,subst), NCic.Meta (i,(shift+1,lc)) + | t -> + NCicUntrusted.map_term_fold_a + (fun e (n,ctx) -> n+i,e::ctx) k aux acc t -*) - subst,metasenv,(CicSubstitution.lift 1 t'), ugraph - - and aux_exp_named_subst metasenv subst n context ens ugraph = - List.fold_right - (fun (uri,t) (subst,metasenv,l,ugraph) -> - let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in - subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph) in - let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in - let fresh_name = - FreshNamesGenerator.mk_fresh_name ~subst - metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty - in - let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in - let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in - subst, metasenv, t'', ugraph2 -in profiler_beta_expand.HExtlib.profile foo () - + let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in + let fresh_name = "Hbeta" ^ string_of_int num in + let (metasenv,subst), t = aux (0, context) (metasenv, subst) t in + let t = eta_reduce (C.Lambda (fresh_name,argty,t)) t t in + metasenv, subst, t and beta_expand_many test_equality_only metasenv subst context t args ugraph = - let _,subst,metasenv,hd,ugraph = + let _, subst, metasenv, hd = List.fold_right - (fun arg (num,subst,metasenv,t,ugraph) -> - let subst,metasenv,t,ugraph1 = - beta_expand num test_equality_only - metasenv subst context t arg ugraph + (fun arg (num,subst,metasenv,t) -> + let subst, metasenv, t = + beta_expand num test_equality_only metasenv subst context t arg in - num+1,subst,metasenv,t,ugraph1 - ) args (1,subst,metasenv,t,ugraph) + num+1,subst,metasenv,t) + args (1,subst,metasenv,t) in - subst,metasenv,hd,ugraph - - + metasenv, subst, hd -let rec instantiate test_eq_only metasenv subst context n lc t swap = +and instantiate test_eq_only metasenv subst context n lc t swap = let unif m s c t1 t2 = if swap then unify m s c t2 t1 else unify m s c t1 t2 in -- 2.39.2