=
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
projects / helm.git / commitdiff