oCic2NCic.cmi: nUri.cmi nReference.cmi nCic.cmo
nCic2OCic.cmi: nUri.cmi nReference.cmi nCic.cmo
nCicLibrary.cmi: nUri.cmi nCic.cmo
-nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo
nCicPp.cmi: nCic.cmo
+nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo
nCicReduction.cmi: nCic.cmo
nCicTypeChecker.cmi: nUri.cmi nCic.cmo
nCicUntrusted.cmi: nCic.cmo
nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi
nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nCic2OCic.cmi nCicLibrary.cmi
nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nCic2OCic.cmx nCicLibrary.cmi
+nCicPp.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmo nCicPp.cmi
+nCicPp.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx nCicPp.cmi
nCicEnvironment.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmo \
nCicEnvironment.cmi
nCicEnvironment.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx \
nCicEnvironment.cmi
-nCicPp.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmo nCicPp.cmi
-nCicPp.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx nCicPp.cmi
nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
nCicEnvironment.cmi nCic.cmo nCicReduction.cmi
nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \
nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx nCicEnvironment.cmx \
nCic.cmx nCicTypeChecker.cmi
-nCicUntrusted.cmo: nReference.cmi nCic.cmo nCicUntrusted.cmi
-nCicUntrusted.cmx: nReference.cmx nCic.cmx nCicUntrusted.cmi
+nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi nCic.cmo \
+ nCicUntrusted.cmi
+nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx nCic.cmx \
+ nCicUntrusted.cmi
nReference.cmi: nUri.cmi
nCicUtils.cmi: nCic.cmx
+nCicPp.cmi: nCic.cmx
nCicSubstitution.cmi: nCic.cmx
oCic2NCic.cmi: nUri.cmi nReference.cmi nCic.cmx
nCic2OCic.cmi: nUri.cmi nReference.cmi nCic.cmx
nCicLibrary.cmi: nUri.cmi nCic.cmx
nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx
-nCicPp.cmi: nCic.cmx
nCicReduction.cmi: nCic.cmx
nCicTypeChecker.cmi: nUri.cmi nCic.cmx
nCicUntrusted.cmi: nCic.cmx
nReference.cmx: nUri.cmx nReference.cmi
nCicUtils.cmo: nReference.cmi nCic.cmx nCicUtils.cmi
nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi
+nCicPp.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmx nCicPp.cmi
+nCicPp.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx nCicPp.cmi
nCicSubstitution.cmo: nReference.cmi nCicUtils.cmi nCic.cmx \
nCicSubstitution.cmi
nCicSubstitution.cmx: nReference.cmx nCicUtils.cmx nCic.cmx \
nCicEnvironment.cmi
nCicEnvironment.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx \
nCicEnvironment.cmi
-nCicPp.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmx nCicPp.cmi
-nCicPp.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx nCicPp.cmi
nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
nCicEnvironment.cmi nCic.cmx nCicReduction.cmi
nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \
nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx nCicEnvironment.cmx \
nCic.cmx nCicTypeChecker.cmi
-nCicUntrusted.cmo: nReference.cmi nCic.cmx nCicUntrusted.cmi
-nCicUntrusted.cmx: nReference.cmx nCic.cmx nCicUntrusted.cmi
+nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi nCic.cmx \
+ nCicUntrusted.cmi
+nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx nCic.cmx \
+ nCicUntrusted.cmi
oCic2NCic.mli \
nCic2OCic.mli \
nCicLibrary.mli \
- nCicEnvironment.mli \
nCicPp.mli \
+ nCicEnvironment.mli \
nCicReduction.mli \
nCicTypeChecker.mli \
nCicUntrusted.mli
prerr_endline (HelmLogger.string_of_html_msg html_msg));
CicParser.impredicative_set := false;
NCicTypeChecker.set_logger logger;
- NCicPp.set_ppterm NCicPp.trivial_pp_term;
Helm_registry.load_from "conf.xml";
let alluris =
try
(* $Id$ *)
-let ppterm =
- ref (fun ~context:_ ~subst:_ ~metasenv:_ ?inside_fix _ ->
- ignore (inside_fix) ; "Please, set a pp callback")
-;;
-
-let set_ppterm f = ppterm := f;;
-
-let ppterm ~context ~subst ~metasenv ?inside_fix t =
- !ppterm ~context ~subst ~metasenv ?inside_fix t
-;;
-
module C = NCic
module R = NReference
with NCicLibrary.ObjectNotFound _ -> R.string_of_reference r
;;
-let trivial_pp_term ~context ~subst:_ ~metasenv:_ ?(inside_fix=false) t =
+let ppterm ~context ~subst ~metasenv:_ ?(inside_fix=false) t =
let buff = Buffer.create 100 in
let f = Format.formatter_of_buffer buff in
let module F = Format in
if not toplevel then F.fprintf f ")";
F.fprintf f "@]"
| C.Implicit _ -> F.fprintf f "?"
+ | C.Meta (n,lc) when List.mem_assoc n subst ->
+ let _,_,t,_ = List.assoc n subst in
+ aux ctx (NCicSubstitution.subst_meta lc t)
| C.Meta (n,(shift,C.Irl len)) ->
F.fprintf f "?%d(%d,%d)" n shift len
| C.Meta (n,(shift,C.Ctx l)) ->
F.fprintf f "?%d(%d,[" n shift;
- List.iter (fun x -> aux ctx x; F.fprintf f ",") l;
+ if List.length l > 0 then
+ begin
+ aux ctx (List.hd l);
+ List.iter (fun x -> F.fprintf f ",";aux ctx x) (List.tl l);
+ end;
F.fprintf f "])"
| C.Sort C.Prop -> F.fprintf f "Prop"
| C.Sort (C.Type []) -> F.fprintf f "IllFormedUniverse"
(* $Id$ *)
-val set_ppterm:
- (context:NCic.context ->
- subst:NCic.substitution ->
- metasenv:NCic.metasenv ->
- ?inside_fix:bool ->
- NCic.term -> string) -> unit
-
val ppterm:
context:NCic.context ->
subst:NCic.substitution ->
metasenv:NCic.metasenv ->
NCic.context -> string
-val trivial_pp_term:
- context:NCic.context ->
- subst:NCic.substitution ->
- metasenv:NCic.metasenv ->
- ?inside_fix:bool ->
- NCic.term -> string
-
val ppobj: NCic.obj -> string
let (===) x y = Pervasives.compare x y = 0 ;;
+let get_relevance = ref (fun ~subst:_ _ _ -> assert false);;
+
+let set_get_relevance f = get_relevance := f;;
+
(* t1, t2 must be well-typed *)
-let are_convertible ?(subst=[]) get_exact_relev =
+let are_convertible ?(subst=[]) =
let rec aux test_eq_only context t1 t2 =
let alpha_eq test_eq_only t1 t2 =
if t1 === t2 then
tl1 tl2 true relevance
with Invalid_argument _ -> false
| HExtlib.FailureAt fail ->
- let relevance = get_exact_relev ~subst context hd1 tl1 in
+ let relevance = !get_relevance ~subst context hd1 tl1 in
let _,relevance = HExtlib.split_nth fail relevance in
let b,relevance = (match relevance with
| [] -> assert false
| (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
aux test_eq_only context hd1 hd2 &&
- let relevance = get_exact_relev ~subst context hd1 tl1 in
+ let relevance = !get_relevance ~subst context hd1 tl1 in
(try
HExtlib.list_forall_default3
(fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
NCic.context -> NCic.term ->
NCic.term
+val set_get_relevance :
+ (subst:NCic.substitution ->
+ NCic.context -> NCic.term -> NCic.term list -> bool list) -> unit
+
val are_convertible :
?subst:NCic.substitution ->
- (subst:NCic.substitution ->
- NCic.context -> NCic.term -> NCic.term list -> bool list) ->
NCic.context -> NCic.term -> NCic.term -> bool
let lift_from k n =
let rec liftaux k = function
| C.Rel m as t -> if m < k then t else C.Rel (m + n)
- | C.Meta (i,(m,l)) as t when k <= m ->
- if n = 0 then t else C.Meta (i,(m+n,l))
+ | C.Meta (i,(m,l)) when k <= m+1 -> C.Meta (i,(m+n,l))
| C.Meta (_,(m,C.Irl l)) as t when k > l + m -> t
| C.Meta (i,(m,l)) ->
let lctx = NCicUtils.expand_local_context l in
else lift_from from n t
;;
+
(* subst t1 t2 *)
(* substitutes [t1] for [Rel 1] in [t2] *)
(* if avoid_beta_redexes is true (default: false) no new beta redexes *)
| C.LetIn (n,ty,t,bo) ->
let ty_t = typeof_aux context t in
let _ = typeof_aux context ty in
- if not (R.are_convertible ~subst get_relevance context ty_t ty) then
+ if not (R.are_convertible ~subst context ty_t ty) then
raise
(TypeCheckerFailure
(lazy (Printf.sprintf
let ty_branch =
type_of_branch ~subst context leftno outtype cons ty_cons 0
in
- j+1, R.are_convertible ~subst get_relevance context ty_p ty_branch,
+ j+1, R.are_convertible ~subst context ty_p ty_branch,
ty_p, ty_branch
else
j,false,old_p_ty,old_exp_p_ty
(_,C.Decl t1), (_,C.Decl t2)
| (_,C.Def (t1,_)), (_,C.Def (t2,_))
| (_,C.Def (_,t1)), (_,C.Decl t2) ->
- if not (R.are_convertible ~subst get_relevance tl t1 t2) then
+ if not (R.are_convertible ~subst tl t1 t2) then
raise
(TypeCheckerFailure
(lazy (Printf.sprintf
with Failure _ -> t)
| _ -> t
in
- if not (R.are_convertible ~subst get_relevance context optimized_t ct)
+ if not (R.are_convertible ~subst context optimized_t ct)
then
raise
(TypeCheckerFailure
(PP.ppterm ~subst ~metasenv ~context t))))
| t, (_,C.Decl ct) ->
let type_t = typeof_aux context t in
- if not (R.are_convertible ~subst get_relevance context type_t ct) then
+ if not (R.are_convertible ~subst context type_t ct) then
raise (TypeCheckerFailure
(lazy (Printf.sprintf
("Not well typed metavariable local context: "^^
let arity2 = R.whd ~subst context arity2 in
match arity1,arity2 with
| C.Prod (name,so1,de1), C.Prod (_,so2,de2) ->
- if not (R.are_convertible ~subst get_relevance context so1 so2) then
+ if not (R.are_convertible ~subst context so1 so2) then
raise (TypeCheckerFailure (lazy (Printf.sprintf
"In outtype: expected %s, found %s"
(PP.ppterm ~subst ~metasenv ~context so1)
aux ((name, C.Decl so1)::context)
(mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2
| C.Sort _, C.Prod (name,so,ta) ->
- if not (R.are_convertible ~subst get_relevance context so ind) then
+ if not (R.are_convertible ~subst context so ind) then
raise (TypeCheckerFailure (lazy (Printf.sprintf
"In outtype: expected %s, found %s"
(PP.ppterm ~subst ~metasenv ~context ind)
| (arg, ty_arg)::tl ->
match R.whd ~subst context ty_he with
| C.Prod (_,s,t) ->
- if R.are_convertible ~subst get_relevance context ty_arg s then
+ if R.are_convertible ~subst context ty_arg s then
aux (S.subst ~avoid_beta_redexes:true arg t) tl
else
raise
let convertible =
match item1,item2 with
(n1,C.Decl ty1),(n2,C.Decl ty2) ->
- n1 = n2 && R.are_convertible ~subst get_relevance context ty1 ty2
+ n1 = n2 && R.are_convertible ~subst context ty1 ty2
| (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
n1 = n2
- && R.are_convertible ~subst get_relevance context ty1 ty2
- && R.are_convertible ~subst get_relevance context bo1 bo2
+ && R.are_convertible ~subst context ty1 ty2
+ && R.are_convertible ~subst context bo1 bo2
| _,_ -> false
in
if not convertible then
| name,C.Def (te,ty) ->
ignore (typeof ~metasenv ~subst:[] context ty);
let ty' = typeof ~metasenv ~subst:[] context te in
- if not (R.are_convertible ~subst get_relevance context ty' ty) then
+ if not (R.are_convertible ~subst context ty' ty) then
raise (AssertFailure (lazy (Printf.sprintf (
"the type of the definiens for %s in the context is not "^^
"convertible with the declared one.\n"^^
typecheck_context ~metasenv ~subst context;
ignore (typeof ~metasenv ~subst context ty);
let ty' = typeof ~metasenv ~subst context bo in
- if not (R.are_convertible ~subst get_relevance context ty' ty) then
+ if not (R.are_convertible ~subst context ty' ty) then
raise (AssertFailure (lazy (Printf.sprintf (
"the type of the definiens for %d in the substitution is not "^^
"convertible with the declared one.\n"^^
| C.Constant (relevance,_,Some te,ty,_) ->
let _ = typeof ~subst ~metasenv [] ty in
let ty_te = typeof ~subst ~metasenv [] te in
- if not (R.are_convertible ~subst get_relevance [] ty_te ty) then
+ if not (R.are_convertible ~subst [] ty_te ty) then
raise (TypeCheckerFailure (lazy (Printf.sprintf (
"the type of the body is not convertible with the declared one.\n"^^
"inferred type:\n%s\nexpected type:\n%s")
in
List.iter2 (fun (_,_,x,ty,_) bo ->
let ty_bo = typeof ~subst ~metasenv types bo in
- if not (R.are_convertible ~subst get_relevance types ty_bo ty)
+ if not (R.are_convertible ~subst types ty_bo ty)
then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))
else
if inductive then begin
typecheck_obj obj)
;;
+let _ = NCicReduction.set_get_relevance get_relevance;;
+
(* EOF *)
let _ =
Helm_registry.load_from "conf.xml";
CicParser.impredicative_set := false;
- NCicPp.set_ppterm NCicPp.trivial_pp_term;
let u = UriManager.uri_of_string Sys.argv.(1) in
let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph u in
prerr_endline "VECCHIO";
match ity with
| NCic.Appl [eq;t;a;b] ->
NCic.Appl [eq;t;NCicReduction.whd ~delta:0 ctx a;b]
- | t -> t
+ | t -> NCicReduction.whd ~delta:0 ctx t
in
+(*
prerr_endline
(Printf.sprintf "%s == %s"
(NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
(NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty));
+*)
let metasenv, subst =
try
- prerr_endline ("INIZIO: " ^ NUri.string_of_uri u);
+(* prerr_endline ("INIZIO: " ^ NUri.string_of_uri u); *)
NCicUnification.unify menv [] ctx ity sty
with
| NCicUnification.Uncertain msg
(NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
(NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty));
[], []
+ | Sys.Break -> [],[]
in
- if (NCicReduction.are_convertible
- ~subst (fun ~subst:_ _ _ _ ->[]) ctx ity sty)
+ if (NCicReduction.are_convertible ~subst ctx ity sty)
then
prerr_endline ("OK: " ^ NUri.string_of_uri u)
else
let inside c = indent := !indent ^ String.make 1 c;;
let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
-let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ s);;
+(*
+let pp s =
+ prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ s);;
+*)
+
+let pp _ = ();;
let rec beta_expand num test_eq_only swap metasenv subst context t arg =
let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
and beta_expand_many test_equality_only swap metasenv subst context t args =
(*D*) inside 'B'; try let rc =
pp (String.concat ", " (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
- args) ^ " in " ^ NCicPp.ppterm ~metasenv ~subst ~context t);
+ args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t);
let _, subst, metasenv, hd =
List.fold_right
(fun arg (num,subst,metasenv,t) ->
num+1,subst,metasenv,t)
args (1,subst,metasenv,t)
in
+ pp ("Head syntesized by b-exp: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context hd);
metasenv, subst, hd
(*D*) in outside (); rc with exn -> outside (); raise exn
^ NCicPp.ppterm ~metasenv ~subst ~context ty_t);
let metasenv, subst = unify test_eq_only metasenv subst context lty ty_t in
let (metasenv, subst), t =
- NCicMetaSubst.delift metasenv subst context n lc t
+ try NCicMetaSubst.delift metasenv subst context n lc t
+ with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
+ | NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg)
in
(* Unifying the types may have already instantiated n. *)
try
| _ -> raise (uncert_exc metasenv subst context t1 t2)
(*D*) in outside(); rc with exn -> outside (); raise exn
in
- let height_of is_whd = function
+ let height_of = function
| NCic.Const (Ref.Ref (_,Ref.Def h))
| NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
| NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
| NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h, false
- | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> max_int, true
-(* | NCic.Rel _ -> 1, WRONG *)
- | _ when is_whd -> 0, false
- | _ -> max_int, false
+ | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> 0, true
+ | _ -> 0, false
in
- let small_delta_step is_whd (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
- let h1, flex1 = height_of is_whd t1 in
- let h2, flex2 = height_of is_whd t2 in
- let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
- NCicReduction.reduce_machine ~delta ~subst context m1,
- NCicReduction.reduce_machine ~delta ~subst context m2,
- if is_whd && flex1 && flex2 then 0 else delta
+ let put_in_whd m1 m2 =
+ NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
+ NCicReduction.reduce_machine ~delta:max_int ~subst context m2,
+ false (* not in normal form *)
+ in
+ let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
+ let h1, flex1 = height_of t1 in
+ let h2, flex2 = height_of t2 in
+ let delta =
+ if flex1 then max 0 (h2 - 1) else
+ if flex2 then max 0 (h1 - 1) else
+ if h1 = h2 then max 0 (h1 -1) else min h1 h2
+ in
+ pp ("DELTA STEP TO: " ^ string_of_int delta);
+ let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in
+ let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in
+ m1', m2', (m1' == m1 && m2' == m2) || delta = 0
+ (* if we have as heads two Fix of height n>0, they may or may not
+ * reduce, depending on their rec argument... we thus check if
+ * something changed or not. This relies on the reduction machine
+ * preserving the original machine if it performs no action *)
in
let rec unif_machines metasenv subst =
function
- | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
+ | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),are_normal) ->
(*D*) inside 'M'; try let rc =
- pp ((if delta > 100 then "∞" else string_of_int delta) ^ " " ^
+ pp ((if are_normal then "*" else " ") ^ " " ^
NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
" === " ^
NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2));
try
let t1 = NCicReduction.from_stack t1 in
let t2 = NCicReduction.from_stack t2 in
- unif_machines metasenv subst
- (small_delta_step true t1 t2)
+ unif_machines metasenv subst (put_in_whd t1 t2)
with UnificationFailure _ | Uncertain _ when not b ->
metasenv, subst
in
(NCicReduction.unwind (k2,e2,t2,List.rev l2))
in
try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
- with UnificationFailure _ | Uncertain _ when delta > 0 ->
+ with UnificationFailure _ | Uncertain _ when not are_normal ->
(*
let delta = delta - 1 in
let red = NCicReduction.reduce_machine ~delta ~subst context in
*)
- unif_machines metasenv subst (small_delta_step true m1 m2)
+ unif_machines metasenv subst (small_delta_step m1 m2)
(*D*) in outside(); rc with exn -> outside (); raise exn
in
try fo_unif test_eq_only metasenv subst t1 t2
with UnificationFailure msg | Uncertain msg as exn ->
try
unif_machines metasenv subst
- (small_delta_step false (0,[],t1,[]) (0,[],t2,[]))
+ (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
with
| UnificationFailure _ -> raise (UnificationFailure msg)
| Uncertain _ -> raise exn
projects / helm.git / commitdiff