(* for demo to reduce the number of interpretations *)
(true, `Library, true);
]
+ else if !debug then
+ [ (true, `Multi, true); ]
else
[ (true, `Mono, false);
(true, `Multi, false);
let occurrences = ref 0 in
let rec aux k _ = function
| C.Rel m when m = n+k -> incr occurrences
- | C.Rel m -> ()
+ | C.Rel _m -> ()
| C.Implicit _ -> ()
| C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
| C.Meta (mno,(s,l)) ->
aux 0 () t;
!occurrences
;;
+
+exception Found_variable
+
+let looks_closed t =
+ let rec aux k _ = function
+ | C.Rel m when k < m -> raise Found_variable
+ | C.Rel _m -> ()
+ | C.Implicit _ -> ()
+ | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
+ | C.Meta _ -> raise Found_variable
+ | t -> NCicUtils.fold (fun _ k -> k + 1) k aux () t
+ in
+ try aux 0 () t; true with Found_variable -> false
+;;
val count_occurrences :
subst:NCic.substitution -> int -> NCic.term -> int
+(* quick, but with false negatives (since no ~subst), check for closed terms *)
+val looks_closed : NCic.term -> bool
lb
in
let rec aux (context,k,in_scope) (metasenv, subst as ms) t =
+ (* XXX if t is closed, we should just terminate. Speeds up hints! *)
+ if NCicUntrusted.looks_closed t then ms, t
+ else
match unify_list in_scope metasenv subst context k t with
| Some x -> x
| None ->
let time2 = Unix.gettimeofday () in
let time1 =
match !times with time1::tl -> times := tl; time1 | [] -> assert false in
- prerr_endline ("}}} " ^ string_of_float (time2 -. time1));
+ prerr_endline ("}}} " ^ !indent ^ " " ^ string_of_float (time2 -. time1));
(match exc_opt with
| Some e -> prerr_endline ("exception raised: " ^ Printexc.to_string e)
| None -> ());
| Uncertain _ as exn -> raise exn
| _ -> assert false
in
+ let fo_unif_heads_and_cont_or_unwind_and_hints
+ test_eq_only metasenv subst m1 m2 cont hm1 hm2
+ =
+ let ms, continuation =
+ (* calling the continuation inside the outermost try is an option
+ and makes unification stronger, but looks not frequent to me
+ that heads unify but not the arguments and that an hints can fix
+ that *)
+ try fo_unif test_eq_only metasenv subst m1 m2, cont
+ with
+ | UnificationFailure _
+ | KeepReducing _ | Uncertain _ as exn ->
+ let (t1,norm1),(t2,norm2) = hm1, hm2 in
+ match
+ try_hints metasenv subst
+ (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
+ with
+ | Some x -> x, fun x -> x
+ | None ->
+ match exn with
+ | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
+ | UnificationFailure _ | Uncertain _ as exn -> raise exn
+ | _ -> assert false
+ in
+ continuation ms
+ in
let height_of = function
| NCic.Const (Ref.Ref (_,Ref.Def h))
| NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
match t1 with
| C.Const r -> NCicEnvironment.get_relevance r
| _ -> [] *) in
- let unif_from_stack t1 t2 b metasenv subst =
+ let unif_from_stack (metasenv, subst) (t1, t2, b) =
try
let t1 = NCicReduction.from_stack ~delta:max_int t1 in
let t2 = NCicReduction.from_stack ~delta:max_int t2 in
NCicReduction.unwind (k2,e2,t2,List.rev l2),
todo
in
- let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
+ let check_stack l1 l2 r =
+ match t1, t2 with
+ | NCic.Meta _, _ | _, NCic.Meta _ ->
+ (NCicReduction.unwind (k1,e1,t1,s1)),
+ (NCicReduction.unwind (k2,e2,t2,s2)),[]
+ | _ -> check_stack l1 l2 r []
+ in
+ let hh1,hh2,todo = check_stack (List.rev s1) (List.rev s2) relevance in
try
- let metasenv,subst =
- fo_unif_w_hints test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) in
- List.fold_left
- (fun (metasenv,subst) (x1,x2,r) ->
- unif_from_stack x1 x2 r metasenv subst
- ) (metasenv,subst) todo
+ fo_unif_heads_and_cont_or_unwind_and_hints
+ test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
+ (fun ms -> List.fold_left unif_from_stack ms todo)
+ m1 m2
with
| KeepReducing _ -> assert false
| KeepReducingThis _ ->
@; //;##]
nqed.
-STOP
-
(* theorem 16: 1 *)
alias symbol "pc" (instance 13) = "cat lang".
alias symbol "in_pl" (instance 23) = "in_pl".
alias symbol "in_pl" (instance 5) = "in_pl".
alias symbol "eclose" (instance 21) = "eclose".
-ntheorem bull_cup : ∀S:Alpha. ∀e:pitem S. 𝐋\p (•e) = 𝐋\p e ∪ 𝐋 .|e|.
+ntheorem bull_cup : ∀S:Alpha. ∀e:pitem S. 𝐋\p (•e) = 𝐋\p e ∪ 𝐋 |e|.
#S e; nelim e; //;
- ##[ #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl, or_intror;
- ##| #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl; *;
+ ##[ #a; napply ext_set; #w; @; *; /3/ by or_introl, or_intror;
+ ##| #a; napply ext_set; #w; @; *; /3/ by or_introl; *;
##| #e1 e2 IH1 IH2;
- nchange in ⊢ (??(??(%))?) with (•e1 ⊙ 〈e2,false〉);
- nrewrite > (odot_dot_aux S (•e1) 〈e2,false〉 IH2);
- nrewrite > (IH1 …); nrewrite > (cup_dotD …);
- nrewrite > (cupA …); nrewrite > (cupC ?? (𝐋\p ?) …);
- nchange in match (𝐋\p 〈?,?〉) with (𝐋\p e2 ∪ {}); nrewrite > (cup0 …);
- nrewrite < (erase_dot …); nrewrite < (cupA …); //;
+ nchange in match (•(e1·e2)) with (•e1 ⊙ 〈e2,false〉);
+ napply (.=_1 (odot_dot_aux ?? 〈e2,false〉 IH2));
+ napply (.=_1 (IH1 ╪_1 #) ╪_1 #);
+ napply (.=_1 (cup_dotD …) ╪_1 #);
+ napply (.=_1 (cupA …));
+ napply (.=_1 # ╪_1 ((erase_dot ???)^-1 ╪_1 (cup0 ??)));
+ napply (.=_1 # ╪_1 (cupC…));
+ napply (.=_1 (cupA …)^-1);
+ //;
##| #e1 e2 IH1 IH2;
- nchange in match (•(?+?)) with (•e1 ⊕ •e2); nrewrite > (oplus_cup …);
- nrewrite > (IH1 …); nrewrite > (IH2 …); nrewrite > (cupA …);
- nrewrite > (cupC ? (𝐋\p e2)…);nrewrite < (cupA ??? (𝐋\p e2)…);
- nrewrite > (cupC ?? (𝐋\p e2)…); nrewrite < (cupA …);
- nrewrite < (erase_plus …); //.
+ nchange in match (•(?+?)) with (•e1 ⊕ •e2);
+ napply (.=_1 (oplus_cup …));
+ napply (.=_1 IH1 ╪_1 IH2);
+ napply (.=_1 (cupA …));
+ napply (.=_1 # ╪_1 (# ╪_1 (cupC…)));
+ napply (.=_1 # ╪_1 (cupA ????)^-1);
+ napply (.=_1 # ╪_1 (cupC…));
+ napply (.=_1 (cupA ????)^-1);
+ napply (.=_1 # ╪_1 (erase_plus ???)^-1);
+ //;
##| #e; nletin e' ≝ (\fst (•e)); nletin b' ≝ (\snd (•e)); #IH;
- nchange in match (𝐋\p ?) with (𝐋\p 〈e'^*,true〉);
+ nchange in match (𝐋\p ?) with (𝐋\p 〈e'^*,true〉);
nchange in match (𝐋\p ?) with (𝐋\p (e'^* ) ∪ {[ ]});
- nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 .|e'|^* );
+STOP
+ nchange in match (𝐋\p (pk ? e')) with (𝐋\p e' · 𝐋 |e'|^* );
nrewrite > (erase_bull…e);
nrewrite > (erase_star …);
nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 .|e| - ϵ b')); ##[##2:
nrewrite > (cup_dotD…); nrewrite > (cupA…);
nrewrite > (?: ((?·?)∪{[]} = 𝐋 .|e^*|)); //;
nchange in match (𝐋 .|e^*|) with ((𝐋. |e|)^* ); napply sub_dot_star;##]
- nqed.
+nqed.
(* theorem 16: 3 *)
nlemma odot_dot:
projects / helm.git / commitdiff