let hbr t =
if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t
in
- let refine_appl metasenv subst args =
+ let refine_appl () =
let metasenv, subst, he, ty_he =
typeof_aux metasenv subst context None he in
let metasenv, subst, t, ty =
let metasenv, subst, he, ty_he =
typeof_aux metasenv subst context expty he in
metasenv, subst, hbr he, ty_he
- with Uncertain _ | RefineFailure _ -> refine_appl metasenv subst args
- else
- (* CSC: whd can be useful on he too... *)
- (match he with
- C.Const (Ref.Ref (uri1,Ref.Con _)) -> (
- match
- HExtlib.map_option (NCicReduction.whd ~subst context) expty
- with
- Some (C.Appl(C.Const(Ref.Ref (uri2,Ref.Ind _) as ref)::expargs))
- when NUri.eq uri1 uri2 ->
- (try
- let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys ref in
- let leftexpargs,_ = HExtlib.split_nth leftno expargs in
- let rec instantiate metasenv subst revargs args =
- function
- [] ->
- (* some checks are re-done here, but it would be complex
- to avoid them (e.g. we did not check yet that the
- constructor is a constructor for that inductive type)*)
- refine_appl metasenv subst ((List.rev revargs)@args)
- | (exparg::expargs) as allexpargs ->
- match args with
- [] -> raise (Failure "Not enough args")
- | (C.Implicit `Vector::args) as allargs ->
- (try
- instantiate metasenv subst revargs args allexpargs
- with
- Sys.Break as exn -> raise exn
- | _ ->
- instantiate metasenv subst revargs
- (C.Implicit `Term :: allargs) allexpargs)
- | arg::args ->
- let metasenv,subst,arg,_ =
- typeof_aux metasenv subst context None arg in
- let metasenv,subst =
- NCicUnification.unify rdb metasenv subst context
- arg exparg
- in
- instantiate metasenv subst(arg::revargs) args expargs
- in
- instantiate metasenv subst [] args leftexpargs
- with
- | Sys.Break as exn -> raise exn
- | _ ->
- refine_appl metasenv subst args (* to try coercions *))
- | _ -> refine_appl metasenv subst args)
- | _ -> refine_appl metasenv subst args)
+ with Uncertain _ | RefineFailure _ -> refine_appl ()
+ else refine_appl ()
| C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
| C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
outtype,(term as orig_term),pl) as orig ->
~localise
metasenv subst context t orig_t infty expty perform_unification exc
=
- let cs_subst = NCicSubstitution.subst ~avoid_beta_redexes:true in
- try
- pp (lazy "WWW: trying coercions -- preliminary unification");
- let metasenv, subst =
- NCicUnification.unify rdb metasenv subst context infty expty
- in metasenv, subst, t, expty
- with
- | exn ->
(* we try with a coercion *)
let rec first exc = function
- | [] ->
- pp (lazy "WWW: no more coercions!");
+ | [] ->
raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
"The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
(NCicPp.ppterm ~metasenv ~subst ~context t)
with
| NCicUnification.UnificationFailure _ -> first exc tl
| NCicUnification.Uncertain _ as exc -> first exc tl
- in
-
- try
- pp (lazy "WWW: trying coercions -- inner check");
- match infty, expty, t with
- | _,_, NCic.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) ->
- (*{{{*) pp (lazy "CASE");
- (* {{{ helper functions *)
- let get_cl_and_left_p refit outty =
- match refit with
- | NReference.Ref (uri, NReference.Ind (_,tyno,leftno)) ->
- let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys r in
- let _, _, ty, cl = List.nth itl tyno in
- let constructorsno = List.length cl in
- let count_pis t =
- let rec aux ctx t =
- match NCicReduction.whd ~subst ~delta:max_int ctx t with
- | NCic.Prod (name,src,tgt) ->
- let ctx = (name, (NCic.Decl src)) :: ctx in
- 1 + aux ctx tgt
- | _ -> 0
- in
- aux [] t
- in
- let rec skip_lambda_delifting t n =
- match t,n with
- | _,0 -> t
- | NCic.Lambda (_,_,t),n ->
- pp (lazy ("WWW: failing term? "^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:[] t));
- skip_lambda_delifting
- (* substitute dangling indices with a dummy *)
- (NCicSubstitution.subst (NCic.Sort NCic.Prop) t) (n - 1)
- | _ -> assert false
- in
- let get_l_r_p n = function
- | NCic.Lambda (_,NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))),_) -> [],[]
- | NCic.Lambda (_,NCic.Appl
- (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))) :: args),_) ->
- HExtlib.split_nth n args
- | _ -> assert false
- in
- let pis = count_pis ty in
- let rno = pis - leftno in
- let t = skip_lambda_delifting outty rno in
- let left_p, _ = get_l_r_p leftno t in
- let instantiate_with_left cl =
- List.map
- (fun ty ->
- List.fold_left
- (fun t p -> match t with
- | NCic.Prod (_,_,t) ->
- cs_subst p t
- | _-> assert false)
- ty left_p)
- cl
- in
- let cl = instantiate_with_left (List.map (fun (_,_,x) -> x) cl) in
- cl, left_p, leftno, rno
- | _ -> raise exn
- in
- let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
- match t,n with
- | _,0 ->
- let rec mkr n = function
- | [] -> [] | _::tl -> NCic.Rel n :: mkr (n+1) tl
- in
- pp (lazy ("input replace: " ^ NCicPp.ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
- let bo =
- NCicRefineUtil.replace_lifting
- ~equality:(fun _ -> NCicRefineUtil.alpha_equivalence)
- ~context:ctx
- ~what:(matched::right_p)
- ~with_what:(NCic.Rel 1::List.rev (mkr 2 right_p))
- ~where:bo
- in
- pp (lazy ("output replace: " ^ NCicPp.ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
- bo
- | NCic.Lambda (name, src, tgt),_ ->
- NCic.Lambda (name, src,
- keep_lambdas_and_put_expty
- ((name, NCic.Decl src)::ctx) tgt (NCicSubstitution.lift 1 bo)
- (List.map (NCicSubstitution.lift 1) right_p) (NCicSubstitution.lift 1 matched) (n-1))
- | _ -> assert false
- in
- (*let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in
- let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*)
- let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.ind(1,0,2)")) in
- let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.con(0,1,2)")) in
- let add_params
- metasenv subst context cty outty mty m i
- =
- let rec aux context outty par j mty m = function
- | NCic.Prod (name, src, tgt) ->
- let t,k =
- aux
- ((name, NCic.Decl src) :: context)
- (NCicSubstitution.lift 1 outty) (NCic.Rel j::par) (j+1)
- (NCicSubstitution.lift 1 mty) (NCicSubstitution.lift 1 m) tgt
- in
- NCic.Prod (name, src, t), k
- | NCic.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r) ->
- let k =
- let k = NCic.Const(Ref.mk_constructor i r) in
- NCicUntrusted.mk_appl k par
- in
- (* the type has no parameters, so kty = mty
- let kty =
- try NCicTypechecker.typeof ~subst ~metasenv context k
- with NCicTypeChecker.TypeCheckerFailure _ -> assert false
- in *)
- NCic.Prod ("p",
- NCic.Appl [eq; mty; m; mty; k],
- (NCicSubstitution.lift 1
- (NCicReduction.head_beta_reduce ~delta:max_int
- (NCicUntrusted.mk_appl outty [k])))),[mty,m,mty,k]
- | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r)::pl) ->
- let left_p,right_p = HExtlib.split_nth leftno pl in
- let has_rights = right_p <> [] in
- let k =
- let k = NCic.Const(Ref.mk_constructor i r) in
- NCicUntrusted.mk_appl k (left_p@par)
- in
- let right_p =
- try match
- NCicTypeChecker.typeof ~subst ~metasenv context k
- with
- | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
- snd (HExtlib.split_nth leftno args)
- | _ -> assert false
- with NCicTypeChecker.TypeCheckerFailure _-> assert false
- in
- let orig_right_p =
- match mty with
- | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
- snd (HExtlib.split_nth leftno args)
- | _ -> assert false
- in
- List.fold_right2
- (fun x y (tacc,pacc) ->
- let xty =
- try NCicTypeChecker.typeof ~subst ~metasenv context x
- with NCicTypeChecker.TypeCheckerFailure _ -> assert false
- in
- let yty =
- try NCicTypeChecker.typeof ~subst ~metasenv context y
- with NCicTypeChecker.TypeCheckerFailure _ -> assert false
- in
- NCic.Prod ("_", NCic.Appl [eq;xty;x;yty;y],
- NCicSubstitution.lift 1 tacc), (xty,x,yty,y)::pacc)
- (orig_right_p @ [m]) (right_p @ [k])
- (NCicReduction.head_beta_reduce ~delta:max_int
- (NCicUntrusted.mk_appl outty (right_p@[k])), [])
-
- (* if has_rights then
- NCicReduction.head_beta_reduce ~delta:max_int
- (NCic.Appl (outty ::right_p @ [k])),k
- else
- NCic.Prod ("p",
- NCic.Appl [eq; mty; m; k],
- (NCicSubstitution.lift 1
- (NCicReduction.head_beta_reduce ~delta:max_int
- (NCic.Appl (outty ::right_p @ [k]))))),k*)
- | _ -> assert false
- in
- aux context outty [] 1 mty m cty
- in
- let add_lambda_for_refl_m pbo eqs cty =
- (* k lives in the right context *)
- (* if rno <> 0 then pbo else *)
- let rec aux = function
- | NCic.Lambda (name,src,bo), NCic.Prod (_,_,ty) ->
- NCic.Lambda (name,src,
- (aux (bo,ty)))
- | t,_ -> snd (List.fold_right
- (fun (xty,x,yty,y) (n,acc) -> n+1, NCic.Lambda ("p" ^ string_of_int n,
- NCic.Appl [eq; xty; x; yty; y],
- NCicSubstitution.lift 1 acc)) eqs (1,t))
- (*NCic.Lambda ("p",
- NCic.Appl [eq; mty; m; k],NCicSubstitution.lift 1 t)*)
- in
- aux (pbo,cty)
- in
- let add_pi_for_refl_m context new_outty mty m lno rno =
- (*if rno <> 0 then new_outty else*)
- let rec aux context mty m = function
- | NCic.Lambda (name, src, tgt) ->
- let context = (name, NCic.Decl src)::context in
- NCic.Lambda (name, src, aux context (NCicSubstitution.lift 1 mty) (NCicSubstitution.lift 1 m) tgt)
- | t ->
- let lhs =
- match mty with
- | NCic.Appl (_::params) -> (snd (HExtlib.split_nth lno params))@[m]
- | _ -> [m]
- in
- let rhs =
- List.map (fun x -> NCic.Rel x)
- (List.rev (HExtlib.list_seq 1 (rno+2))) in
- List.fold_right2
- (fun x y acc ->
- let xty =
- try NCicTypeChecker.typeof ~subst ~metasenv context x
- with NCicTypeChecker.TypeCheckerFailure _ -> assert false
- in
- let yty =
- try NCicTypeChecker.typeof ~subst ~metasenv context y
- with NCicTypeChecker.TypeCheckerFailure _ -> assert false
- in
- NCic.Prod
- ("_", NCic.Appl [eq;xty;x;yty;y],
- (NCicSubstitution.lift 1 acc)))
- lhs rhs t
- (* NCic.Prod
- ("_", NCic.Appl [eq;mty;m;NCic.Rel 1],
- NCicSubstitution.lift 1 t)*)
- in
- aux context mty m new_outty
- in (* }}} end helper functions *)
- (* constructors types with left params already instantiated *)
- let outty = NCicUntrusted.apply_subst subst context outty in
- let cl, left_p, leftno,rno =
- get_cl_and_left_p r outty
- in
- let right_p, mty =
- try
- match
- NCicTypeChecker.typeof ~subst ~metasenv context m
- with
- | (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))) | NCic.Meta _) as mty -> [], mty
- | NCic.Appl ((NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))|NCic.Meta _)::args) as mty ->
- snd (HExtlib.split_nth leftno args), mty
- | _ -> assert false
- with NCicTypeChecker.TypeCheckerFailure _ ->
- raise (AssertFailure(lazy "already ill-typed matched term"))
- in
- let mty = NCicUntrusted.apply_subst subst context mty in
- let outty = NCicUntrusted.apply_subst subst context outty in
- let expty = NCicUntrusted.apply_subst subst context expty in
- let new_outty =
- keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
- in
- pp
- (lazy ("CASE: new_outty: " ^ NCicPp.ppterm
- ~context ~metasenv ~subst new_outty));
- let _,pl,subst,metasenv =
- List.fold_right2
- (fun cty pbo (i, acc, s, menv) ->
- pp (lazy ("begin iteration"));
- (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
- * (new_)outty right_par (K_i left_par k_par) *)
- let infty_pbo, _ =
- add_params menv s context cty outty mty m i in
- pp
- (lazy ("CASE: infty_pbo: "^ NCicPp.ppterm
- ~context ~metasenv ~subst infty_pbo));
- let expty_pbo, eqs = (* k is (K_i left_par k_par) *)
- add_params menv s context cty new_outty mty m i in
- pp
- (lazy ("CASE: expty_pbo: "^ NCicPp.ppterm
- ~context ~metasenv ~subst expty_pbo));
- let pbo = add_lambda_for_refl_m pbo eqs cty in
- pp
- (lazy ("CASE: pbo: " ^ NCicPp.ppterm
- ~context ~metasenv ~subst pbo));
- let metasenv, subst, pbo, _ =
- try_coercions rdb ~localise menv s context pbo
- orig_t (*??*) infty_pbo expty_pbo perform_unification exc
- in
- pp
- (lazy ("CASE: pbo2: " ^ NCicPp.ppterm
- ~context ~metasenv ~subst pbo));
- (i-1, pbo::acc, subst, metasenv))
- cl pl (List.length pl, [], subst, metasenv)
- in
- (*let metasenv, subst =
- try
- NCicUnification.unify rdb metasenv subst context outty new_outty
- with _ -> raise (RefineFailure (lazy (localise orig_t, "try_coercions")))
- in*)
- let new_outty = add_pi_for_refl_m context new_outty mty m leftno rno in
- pp (lazy ("CASE: new_outty: " ^ (NCicPp.ppterm
- ~metasenv ~subst ~context new_outty)));
- let right_tys =
- List.map
- (fun t -> NCicTypeChecker.typeof ~subst ~metasenv context t) right_p in
- let eqs =
- List.map2 (fun x y -> NCic.Appl[eq_refl;x;y]) (right_tys@[mty])
- (right_p@[m]) in
- let t = NCic.Appl (NCic.Match(r,new_outty,m,pl) :: eqs)
- in
- metasenv, subst, t, expty (*}}}*)
- | NCic.Prod (nameprod, src, ty),NCic.Prod (_, src2, ty2), _ ->
- let rec mk_fresh_name ctx firstch n =
- let candidate = (String.make 1 firstch) ^ (string_of_int n) in
- if (List.for_all (fun (s,_) -> s <> candidate) ctx) then candidate
- else mk_fresh_name ctx firstch (n+1)
- in
- (*{{{*) pp (lazy "LAM");
- pp (lazy ("LAM: t = " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
- let name_con = mk_fresh_name context 'c' 0
- (*FreshNamesGenerator.mk_fresh_name
- ~subst metasenv context ~typ:src2 Cic.Anonymous*)
- in
- let context_src2 = ((name_con, NCic.Decl src2) :: context) in
- (* contravariant part: the argument of f:src->ty *)
- let metasenv, subst, rel1, _ =
- try_coercions rdb ~localise metasenv subst context_src2
- (NCic.Rel 1) orig_t (NCicSubstitution.lift 1 src2)
- (NCicSubstitution.lift 1 src) perform_unification exc
- in
- (* covariant part: the result of f(c x); x:src2; (c x):src *)
- let name_t, bo =
- match t with
- | NCic.Lambda (n,_,bo) -> n, cs_subst rel1 (NCicSubstitution.lift_from 2 1 bo)
- | _ -> name_con, NCicUntrusted.mk_appl (NCicSubstitution.lift 1 t) [rel1]
- in
- (* we fix the possible dependency problem in the source ty *)
- let ty = cs_subst rel1 (NCicSubstitution.lift_from 2 1 ty) in
- let metasenv, subst, bo, _ =
- try_coercions rdb ~localise metasenv subst context_src2
- bo orig_t ty ty2 perform_unification exc
- in
- let coerced = NCic.Lambda (name_t,src2, bo) in
- pp (lazy ("LAM: coerced = " ^ NCicPp.ppterm ~metasenv ~subst ~context coerced));
- metasenv, subst, coerced, expty (*}}}*)
- | _ -> raise exc
- with exc2 ->
+ in
pp(lazy("try_coercion " ^
NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |---> " ^
NCicPp.ppterm ~metasenv ~subst ~context expty));
;;
let undebruijnate inductive ref t rev_fl =
- let len = List.length rev_fl in
NCicSubstitution.psubst (fun x -> x)
- (HExtlib.list_mapi
+ (List.rev (HExtlib.list_mapi
(fun (_,_,rno,_,_,_) i ->
- let i = len - i - 1 in
NCic.Const
(if inductive then NReference.mk_fix i rno ref
else NReference.mk_cofix i ref))
- rev_fl)
+ rev_fl))
t
;;
metasenv,subst,item1::context
) (metasenv,subst,tys) sx_context_ty_rev sx_context_te_rev
with Invalid_argument "List.fold_left2" -> assert false in
- let metasenv, subst =
- let rec aux context (metasenv,subst) = function
- | NCic.Meta _ -> metasenv, subst
- | NCic.Implicit _ -> metasenv, subst
- | NCic.Appl (NCic.Rel i :: args) as t
- when i > List.length context - len ->
- let lefts, _ = HExtlib.split_nth leftno args in
- let ctxlen = List.length context in
- let (metasenv, subst), _ =
- List.fold_left
- (fun ((metasenv, subst),l) arg ->
- NCicUnification.unify rdb
- ~test_eq_only:true metasenv subst context arg
- (NCic.Rel (ctxlen - len - l)), l+1
- )
- ((metasenv, subst), 0) lefts
- in
- metasenv, subst
- | t -> NCicUtils.fold (fun e c -> e::c) context aux
- (metasenv,subst) t
- in
- aux context (metasenv,subst) te
- in
let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in
(match
NCicReduction.whd ~subst context con_sort,
projects / helm.git / blobdiff