(pp_term typ) (pp_constructors constructors)
in
fst_typ_pp ^ String.concat "" (List.map pp_type tl))
- | Ast.Theorem (flavour, name, typ, body,_) ->
+ | Ast.Theorem (name, typ, body,(_,flavour,_)) ->
sprintf "%s %s:\n %s\n%s"
(NCicPp.string_of_flavour flavour)
name
type 'term obj =
| Inductive of 'term capture_variable list * 'term inductive_type list
(** parameters, list of loc * mutual inductive types *)
- | Theorem of NCic.def_flavour * string * 'term * 'term option * NCic.def_pragma
- (** flavour, name, type, body
+ | Theorem of string * 'term * 'term option * NCic.c_attr
+ (** name, type, body, attributes
* - name is absent when an unnamed theorem is being proved, tipically in
* interactive usage
* - body is present when its given along with the command, otherwise it
indtypes
in
NotationPt.Inductive (freshen_capture_variables params, indtypes)
- | NotationPt.Theorem (flav, n, t, ty_opt,p) ->
+ | NotationPt.Theorem (n, t, ty_opt, attrs) ->
let ty_opt =
match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
in
- NotationPt.Theorem (flav, n, freshen_term t, ty_opt,p)
+ NotationPt.Theorem (n, freshen_term t, ty_opt, attrs)
| NotationPt.Record (params, n, ty, fields) ->
NotationPt.Record (freshen_capture_variables params, n,
freshen_term ty, freshen_name_ty_b fields)
let domain_of_obj ~context ast =
assert (context = []);
match ast with
- | Ast.Theorem (_,_,ty,bo,_) ->
+ | Ast.Theorem (_,ty,bo,_) ->
domain_of_term [] ty
@ (match bo with
None -> []
use_coercions:bool ->
string_context_of_context:('context -> string option list) ->
initial_ugraph:'ugraph ->
- expty: 'refined_thing option ->
+ expty: 'refined_thing DisambiguateTypes.expected_type ->
mk_implicit:(bool -> 'alias) ->
description_of_alias:('alias -> string) ->
fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
'raw_thing) ->
refine_thing:(
'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
- 'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash ->
+ 'raw_thing -> 'refined_thing DisambiguateTypes.expected_type -> 'ugraph -> localization_tbl:'cichash ->
('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
mk_localization_tbl:(int -> 'cichash) ->
'ast_thing disambiguator_input ->
((DisambiguateTypes.Environment.key * 'alias) list *
'metasenv * 'subst * 'refined_thing * 'ugraph)
list * bool
+
(* $Id$ *)
+type 'a expected_type = [ `XTNone (* unknown *)
+ | `XTSome of 'a (* the given term *)
+ | `XTSort (* any sort *)
+ | `XTInd (* any (co)inductive type *)
+ ]
+
type domain_item =
| Id of string (* literal *)
| Symbol of string * int (* literal, instance num *)
* http://helm.cs.unibo.it/
*)
+type 'a expected_type = [ `XTNone (* unknown *)
+ | `XTSome of 'a (* the given term *)
+ | `XTSort (* any sort *)
+ | `XTInd (* any (co)inductive type *)
+ ]
+
type domain_item =
| Id of string (* literal *)
| Symbol of string * int (* literal, instance num *)
subst:'subst ->
string_context_of_context:('context -> string option list) ->
initial_ugraph:'ugraph ->
- expty: 'refined_thing option ->
+ expty: 'refined_thing DisambiguateTypes.expected_type ->
mk_implicit:(bool -> 'alias) ->
description_of_alias:('alias -> string) ->
fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
'raw_thing) ->
refine_thing:(
'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
- 'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash ->
+ 'raw_thing -> 'refined_thing DisambiguateTypes.expected_type -> 'ugraph -> localization_tbl:'cichash ->
('refined_thing, 'metasenv,'subst,'ugraph) Disambiguate.test_result) ->
mk_localization_tbl:(int -> 'cichash) ->
string * int * 'ast_thing ->
let eval_unification_hint status t n =
let metasenv,subst,status,t =
- GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in
+ GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] ("",0,t) in
assert (metasenv=[]);
let t = NCicUntrusted.apply_subst status subst [] t in
let status = basic_eval_unification_hint (t,n) status in
let o_t = NotationPt.Ident (name,None) in
let metasenv,subst, status,t =
GrafiteDisambiguate.disambiguate_nterm
- status None [] [] [] ("",0,o_t) in
+ status `XTNone [] [] [] ("",0,o_t) in
assert( metasenv = [] && subst = []);
let ty = NCicTypeChecker.typeof status [] [] [] t in
let source, target =
(*prerr_endline (status#ppobj obj);*)
let boxml = NCicElim.mk_elims status obj in
let boxml = boxml @ NCicElim.mk_projections status obj in
- let status = status#set_ng_mode `CommandMode in
+ let status = status#set_ng_mode `CommandMode in
let xxaliases = GrafiteDisambiguate.aliases_for_objs status [uri] in
let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
let status = eval_alias status (mode,xxaliases) in
else
nstatus
with
- | MultiPassDisambiguator.DisambiguationError _
+ | MultiPassDisambiguator.DisambiguationError _ as e ->
+ HLog.warn "error in disambiguating projection/eliminator";
+ status
| NCicTypeChecker.TypeCheckerFailure _ ->
- (*HLog.warn "error in generating projection/eliminator";*)
+ HLog.warn "error in typechecking projection/eliminator";
status
) status boxml in
let _,_,_,_,nobj = obj in
(fun status (name,cpos,arity) ->
try
let metasenv,subst,status,t =
- GrafiteDisambiguate.disambiguate_nterm status None [] [] []
+ GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] []
("",0,NotationPt.Ident (name,None)) in
assert (metasenv = [] && subst = []);
let status, nuris =
else
let status = status#set_ng_mode `ProofMode in
let metasenv,subst,status,indty =
- GrafiteDisambiguate.disambiguate_nterm status None [] [] [] (text,prefix_len,indty) in
+ GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] (text,prefix_len,indty) in
let indtyno, (_,_,tys,_,_),leftno = match indty with
NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) ->
indtyno, NCicEnvironment.get_checked_indtys status r, leftno
let metasenv,subst,status,sort = match sort with
| None -> [],[],status,NCic.Sort NCic.Prop
| Some s ->
- GrafiteDisambiguate.disambiguate_nterm status None [] [] []
+ GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] []
(text,prefix_len,s)
in
assert (metasenv = []);
(status#ppterm ~metasenv ~subst ~context:[] sort))) in
let status = status#set_ng_mode `ProofMode in
let metasenv,subst,status,indty =
- GrafiteDisambiguate.disambiguate_nterm status None [] [] subst
+ GrafiteDisambiguate.disambiguate_nterm status `XTNone [] [] subst
(text,prefix_len,indty) in
let indtyno,(_,leftno,tys,_,_) =
match indty with
(try
let metasenv,subst,status,src =
GrafiteDisambiguate.disambiguate_nterm
- status None ctx [] [] ("",0,src) in
+ status `XTSort ctx [] [] ("",0,src) in
let src = NCicUntrusted.apply_subst status subst [] src in
(* CHECK that the declared pattern matches the abstraction *)
let _ = NCicUnification.unify status metasenv subst ctx ty src in
let status, tgt, arity =
let metasenv,subst,status,tgt =
GrafiteDisambiguate.disambiguate_nterm
- status None [] [] [] ("",0,tgt) in
+ status `XTSort [] [] [] ("",0,tgt) in
let tgt = NCicUntrusted.apply_subst status subst [] tgt in
(* CHECK che sia unificabile mancante *)
let rec count_prod = function
let eval_ncoercion (status: #GrafiteTypes.status) name compose t ty (id,src) tgt =
let metasenv,subst,status,ty =
- GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
+ GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] ("",0,ty) in
assert (metasenv=[]);
let ty = NCicUntrusted.apply_subst status subst [] ty in
let metasenv,subst,status,t =
- GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
+ GrafiteDisambiguate.disambiguate_nterm status (`XTSome ty) [] [] [] ("",0,t) in
assert (metasenv=[]);
let t = NCicUntrusted.apply_subst status subst [] t in
let status, src, tgt, cpos, arity =
| _ -> assert false
in
let body = N.Ident (name,None) in
- (loc, N.Theorem(`Definition, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular))
+ let attrs = `Provided, `Definition, `Regular in
+ (loc, N.Theorem(name, ty, Some (N.LetRec (ind_kind, defs, body)), attrs))
let nmk_rec_corec ind_kind defs loc index =
let loc,t = mk_rec_corec ind_kind defs loc in
IDENT "qed" ; i = index -> G.NQed (loc,i)
| nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
- G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular),true)
+ let attrs = `Provided, nflavour, `Regular in
+ G.NObj (loc, N.Theorem (name, typ, body, attrs),true)
| nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
body = term ->
+ let attrs = `Provided, nflavour, `Regular in
G.NObj (loc,
- N.Theorem(nflavour, name, N.Implicit `JustOne, Some body,`Regular),
+ N.Theorem(name, N.Implicit `JustOne, Some body, attrs),
true)
| IDENT "axiom"; i = index; name = IDENT; SYMBOL ":"; typ = term ->
- G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular),i)
+ let attrs = `Provided, `Axiom, `Regular in
+ G.NObj (loc, N.Theorem (name, typ, None, attrs),i)
| IDENT "discriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
| IDENT "inverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
paramspec = OPT inverter_param_list ;
n, is_ind, ty, List.map (build_constractor lno context) cl
in
match kind with
- | NCic.Constant (_, n, xbo, ty, (_, flavour, pragma)) ->
+ | NCic.Constant (_, n, xbo, ty, attrs) ->
let ty = nast_of_cic ~context:[] ty in
let xbo = match xbo with
| Some bo -> Some (nast_of_cic ~context:[] bo)
| None -> None
in
- N.Theorem (flavour, n, ty, xbo, pragma)
+ N.Theorem (n, ty, xbo, attrs)
| NCic.Inductive (is_ind, lno, itl, (_, `Regular)) ->
let captures, context = build_captures lno itl in
N.Inductive (captures, List.map (build_inductive is_ind lno context) itl)
match obj with
| NotationPt.Inductive (_,(name,_,_,_)::_)
| NotationPt.Record (_,name,_,_) -> name ^ ".ind"
- | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
+ | NotationPt.Theorem (name,_,_,_) -> name ^ ".con"
| NotationPt.Inductive _ -> assert false
in
NUri.uri_of_string (baseuri ^ "/" ^ name)
val disambiguate_nterm :
#status as 'status ->
- NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution ->
+ NCic.term NCicRefiner.expected_type -> NCic.context -> NCic.metasenv -> NCic.substitution ->
NotationPt.term Disambiguate.disambiguator_input ->
NCic.metasenv * NCic.substitution * 'status * NCic.term
(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-open Printf
-
-open DisambiguateTypes
-
+module P = Printf
+module DT = DisambiguateTypes
module Ast = NotationPt
module NRef = NReference
~localization_tbl
=
assert (uri=None);
- debug_print (lazy (sprintf "TEST_INTERPRETATION: %s"
+ debug_print (lazy (P.sprintf "TEST_INTERPRETATION: %s"
(status#ppterm ~metasenv ~subst ~context term)));
try
let localise t =
status#ppterm ~metasenv ~subst ~context term)) ;
Disambiguate.Uncertain loc_msg
| NCicRefiner.RefineFailure loc_msg ->
- debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s"
+ debug_print (lazy (P.sprintf "PRUNED:\nterm%s\nmessage:%s"
(status#ppterm ~metasenv ~subst ~context term) (snd(Lazy.force loc_msg))));
Disambiguate.Ko loc_msg
;;
let refine_obj status metasenv subst _context _uri ~use_coercions obj _ _ugraph
~localization_tbl
=
- (*prerr_endline ((sprintf "TEST_INTERPRETATION: %s" (status#ppobj obj)));*)
+ (*prerr_endline ((P.sprintf "TEST_INTERPRETATION: %s" (status#ppobj obj)));*)
assert (metasenv=[]);
assert (subst=[]);
let localise t =
status#ppobj obj)) ;
Disambiguate.Uncertain loc_msg
| NCicRefiner.RefineFailure loc_msg ->
- debug_print (lazy (sprintf "PRUNED:\nobj: %s\nmessage: %s"
+ debug_print (lazy (P.sprintf "PRUNED:\nobj: %s\nmessage: %s"
(status#ppobj obj) (snd(Lazy.force loc_msg))));
Disambiguate.Ko loc_msg
;;
aux ~localize loc context (NotationPt.Appl (inner @ args))
| NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) ->
let cic_args = List.map (aux ~localize loc context) args in
- Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)
+ Disambiguate.resolve ~mk_choice ~env (DT.Symbol (symb, i)) (`Args cic_args)
| NotationPt.Appl terms ->
NCic.Appl (List.map (aux ~localize loc context) terms)
| NotationPt.Binder (binder_kind, (var, typ), body) ->
| `Pi
| `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
| `Exists ->
- Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", 0))
+ Disambiguate.resolve ~env ~mk_choice (DT.Symbol ("exists", 0))
(`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ]))
| NotationPt.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux ~localize loc context term in
match indty_ident with
| Some (indty_ident, _) ->
(match Disambiguate.resolve ~env ~mk_choice
- (Id indty_ident) (`Args []) with
+ (DT.Id indty_ident) (`Args []) with
| NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
function
(Ast.Pattern (head, _, _), _) :: _ -> head
| (Ast.Wildcard, _) :: tl -> fst_constructor tl
- | [] -> raise (Invalid_choice (lazy (loc,"The type "^
+ | [] -> raise (DT.Invalid_choice (lazy (loc,"The type "^
"of the term to be matched cannot be determined "^
"because it is an inductive type without constructors "^
"or because all patterns use wildcards")))
description_of_alias v)) env;
*)
(match Disambiguate.resolve ~env ~mk_choice
- (Id (fst_constructor branches)) (`Args []) with
+ (DT.Id (fst_constructor branches)) (`Args []) with
| NCic.Const (NReference.Ref (_,NReference.Con _) as r) ->
let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in
NReference.mk_indty b r
with Not_found ->
try NCic.Const (List.assoc name obj_context)
with Not_found ->
- Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
+ Disambiguate.resolve ~env ~mk_choice (DT.Id name) (`Args []))
| NotationPt.Uri (uri, subst) ->
assert (subst = None);
(try
| NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
| NotationPt.UserInput -> NCic.Implicit `Hole
| NotationPt.Num (num, i) ->
- Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
+ Disambiguate.resolve ~env ~mk_choice (DT.Num i) (`Num_arg num)
| NotationPt.Meta (index, subst) ->
let cic_subst =
List.map
[`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
| NotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~env ~mk_choice
- (Symbol (symbol, instance)) (`Args [])
+ (DT.Symbol (symbol, instance)) (`Args [])
| NotationPt.Variable _
| NotationPt.Magic _
| NotationPt.Layout _
interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
let uri = match uri with | None -> assert false | Some u -> u in
match obj with
- | NotationPt.Theorem (flavour, name, ty, bo, pragma) ->
+ | NotationPt.Theorem (name, ty, bo, attrs) ->
+ let _, flavour, _ = attrs in
let ty' =
interpretate_term status
~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty
uri, height, [], [],
(match bo,flavour with
| None,`Axiom ->
- let attrs = `Provided, flavour, pragma in
NCic.Constant ([],name,None,ty',attrs)
| Some _,`Axiom -> assert false
| None,_ ->
- let attrs = `Provided, flavour, pragma in
NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
| Some bo,_ ->
(match bo with
([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
defs
in
- let attrs = `Provided, flavour, pragma in
NCic.Fixpoint (inductive,inductiveFuns,attrs)
| bo ->
let bo =
interpretate_term status
~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
in
- let attrs = `Provided, flavour, pragma in
NCic.Constant ([],name,Some bo,ty',attrs)))
| NotationPt.Inductive (params,tyl) ->
let context,params =
~interpretate_thing:(interpretate_obj status ~mk_choice)
~refine_thing:(refine_obj status)
(text,prefix_len,obj)
- ~mk_localization_tbl ~expty:None
+ ~mk_localization_tbl ~expty:`XTNone
in
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
;;
context:NCic.context ->
metasenv:NCic.metasenv ->
subst:NCic.substitution ->
- expty:NCic.term option ->
+ expty:NCic.term NCicRefiner.expected_type ->
mk_implicit: (bool -> 'alias) ->
description_of_alias:('alias -> string) ->
fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
module C = NCic
module Ref = NReference
+type 'a expected_type = [ `XTNone (* unknown *)
+ | `XTSome of 'a (* the given term *)
+ | `XTSort (* any sort *)
+ | `XTInd (* any (co)inductive type *)
+ ]
+
let debug = ref false;;
let indent = ref "";;
let times = ref [];;
| `Closed ->
let metasenv,subst,expty =
match with_type with
- None -> metasenv,subst,None
- | Some typ ->
+ `XTSort
+ | `XTInd
+ | `XTNone -> metasenv,subst,None
+ | `XTSome typ ->
let (metasenv,subst),typ =
try
NCicMetaSubst.delift status
~unify:(fun m s c t1 t2 ->
try Some (NCicUnification.unify status m s c t1 t2)
with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None)
- metasenv subst context (-1) (0,NCic.Irl 0) typ
+ metasenv subst context (-1) (0,C.Irl 0) typ
with
NCicMetaSubst.MetaSubstFailure _
| NCicMetaSubst.Uncertain _ ->
metasenv,subst,Some typ
in
NCicMetaSubst.mk_meta metasenv [] ?with_type:expty `IsTerm,subst
- | `Type -> NCicMetaSubst.mk_meta metasenv context ?with_type `IsType,subst
- | `Term -> NCicMetaSubst.mk_meta metasenv context ?with_type `IsTerm,subst
+ | `Type ->
+ let with_type = match with_type with `XTSome t -> Some t | _ -> None in
+ NCicMetaSubst.mk_meta metasenv context ?with_type `IsType,subst
+ | `Term ->
+ let with_type = match with_type with `XTSome t -> Some t | _ -> None in
+ NCicMetaSubst.mk_meta metasenv context ?with_type `IsTerm,subst
| `Tagged s ->
+ let with_type = match with_type with `XTSome t -> Some t | _ -> None in
NCicMetaSubst.mk_meta
~attrs:[`Name s] metasenv context ?with_type `IsTerm,subst
| `Vector ->
let force_ty skip_lambda skip_appl metasenv subst context orig t infty expty =
(*D*)inside 'F'; try let rc =
match expty with
- | Some expty ->
+ | `XTSome expty ->
(match t with
| C.Implicit _ -> assert false
| C.Lambda _ when skip_lambda -> metasenv, subst, t, expty
| NCicUnification.Uncertain _
| NCicUnification.UnificationFailure _ as exc ->
try_coercions status ~localise
- metasenv subst context t orig infty (`Type expty) exc)
- | None -> metasenv, subst, t, infty
+ metasenv subst context t orig infty (`XTSome expty) exc)
+ | `XTNone -> metasenv, subst, t, infty
+ | `XTSort ->
+ (match t with
+ | C.Implicit _ -> assert false
+ | _ ->
+ pp (lazy ("forcing infty=any sort: "^
+ (status#ppterm ~metasenv ~subst ~context infty) ^ " === any sort"));
+ force_to_sort status metasenv subst context t orig localise infty)
+ | `XTInd ->
+ (match t with
+ | C.Implicit _ -> assert false
+ | _ ->
+ pp (lazy ("forcing infty=any (co)inductive type: "^
+ (status#ppterm ~metasenv ~subst ~context infty) ^ " === any (co)inductive type"));
+ force_to_inductive status metasenv subst context t orig localise infty)
(*D*)in outside true; rc with exc -> outside false; raise exc
in
let rec typeof_aux metasenv subst context expty =
fun t as orig ->
(*D*)inside 'R'; try let rc =
pp (lazy (status#ppterm ~metasenv ~subst ~context t ^ " ::exp:: " ^
- match expty with None -> "None" | Some e ->
+ match expty with `XTSort -> "Any sort" | `XTInd -> "Any (co)inductive type"
+ | `XTNone -> "None" | `XTSome e ->
status#ppterm ~metasenv ~subst ~context e));
let metasenv, subst, t, infty =
match t with
let (metasenv,_,t,ty),subst =
exp_implicit status ~localise metasenv subst context expty t infos
in
- if expty = None then
- typeof_aux metasenv subst context None t
- else
- metasenv, subst, t, ty
+ (match expty with
+ | `XTSome _ -> metasenv, subst, t, ty
+ | _ -> typeof_aux metasenv subst context expty t)
| C.Meta (n,l) as t ->
let metasenv, ty =
try
| C.Const _ ->
metasenv, subst, t, NCicTypeChecker.typeof status ~subst ~metasenv context t
| C.Prod (name,(s as orig_s),(t as orig_t)) ->
- let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in
+ let metasenv, subst, s, s1 = typeof_aux metasenv subst context `XTSort s in
let metasenv, subst, s, s1 =
force_to_sort status
metasenv subst context s orig_s localise s1 in
let context1 = (name,(C.Decl s))::context in
- let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in
+ let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 `XTSort t in
let metasenv, subst, t, s2 =
force_to_sort status
metasenv subst context1 t orig_t localise s2 in
sort_of_prod status localise metasenv subst
context orig_s orig_t (name,s) t (s1,s2)
in
- metasenv, subst, NCic.Prod(name,s,t), ty
+ metasenv, subst, C.Prod(name,s,t), ty
| C.Lambda (n,(s as orig_s),t) as orig ->
let exp_s, exp_ty_t, force_after =
match expty with
- | None -> None, None, false
- | Some expty ->
+ | `XTSort
+ | `XTInd
+ | `XTNone -> `XTNone, `XTNone, false
+ | `XTSome expty ->
match NCicReduction.whd status ~subst context expty with
- | C.Prod (_,s,t) -> Some s, Some t, false
- | _ -> None, None, true
+ | C.Prod (_,s,t) -> `XTSome s, `XTSome t, false
+ | _ -> `XTNone, `XTNone, true
in
let (metasenv,subst), s =
match exp_s with
- | Some exp_s ->
+ | `XTSome exp_s ->
(* optimized case: implicit and implicitly typed meta
* the optimization prevents proliferation of metas *)
(match s with
(try
pp(lazy("Force source to: "^status#ppterm ~metasenv ~subst
~context exp_s));
- NCicUnification.unify ~test_eq_only:true status metasenv subst context s exp_s,s
+ NCicUnification.unify ~test_eq_only:true status metasenv subst context s exp_s, s
with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf
"Source type %s was expected to be %s" (status#ppterm ~metasenv
~subst ~context s) (status#ppterm ~metasenv ~subst ~context
exp_s))) exc)))
- | None ->
+ | `XTNone
+ | `XTSort
+ | `XTInd ->
let metasenv, subst, s =
check_type status ~localise metasenv subst context s in
(metasenv, subst), s
let metasenv, subst, ty =
check_type status ~localise metasenv subst context ty in
let metasenv, subst, t, _ =
- typeof_aux metasenv subst context (Some ty) t in
+ typeof_aux metasenv subst context (`XTSome ty) t in
let context1 = (n, C.Def (t,ty)) :: context in
let metasenv, subst, expty1 =
match expty with
- | None -> metasenv, subst, None
- | Some x ->
+ | `XTSome x ->
let m, s, x =
NCicUnification.delift_type_wrt_terms
status metasenv subst context1 (NCicSubstitution.lift status 1 x)
[NCicSubstitution.lift status 1 t]
in
- m, s, Some x
+ m, s, `XTSome x
+ | _ -> metasenv, subst, expty
in
let metasenv, subst, bo, bo_ty =
typeof_aux metasenv subst context1 expty1 bo
in
let refine_appl metasenv subst args =
let metasenv, subst, he, ty_he =
- typeof_aux metasenv subst context None he in
+ typeof_aux metasenv subst context `XTNone he in
let metasenv, subst, t, ty =
eat_prods status ~localise force_ty metasenv subst context expty t
orig_he he ty_he args in
metasenv, subst, hbr t, ty
in
- if args = [C.Implicit `Vector] && expty <> None then
+ if args = [C.Implicit `Vector] && expty <> `XTNone then
(* we try here to expand the vector a 0 implicits, but we use
* the expected type *)
try
(* CSC: whd can be useful on he too... *)
(match he with
C.Const (Ref.Ref (uri1,Ref.Con _)) -> (
- match
- HExtlib.map_option (NCicReduction.whd status ~subst context) expty
- with
- Some (C.Appl(C.Const(Ref.Ref (uri2,Ref.Ind _) as ref)::expargs))
+ match expty with
+ | `XTSome expty -> (
+ match NCicReduction.whd status ~subst context expty with
+ C.Appl (C.Const (Ref.Ref (uri2,Ref.Ind _) as ref)::expargs)
when NUri.eq uri1 uri2 ->
(try
let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys status ref in
(C.Implicit `Term :: allargs) allexpargs)
| arg::args ->
let metasenv,subst,arg,_ =
- typeof_aux metasenv subst context None arg in
+ typeof_aux metasenv subst context `XTNone arg in
let metasenv,subst =
NCicUnification.unify status metasenv subst context
arg exparg
| Sys.Break as exn -> raise exn
| _ ->
refine_appl metasenv subst args (* to try coercions *))
- | _ -> refine_appl metasenv subst args)
+ | _ -> refine_appl metasenv subst args)
+ | `XTNone
+ | `XTSort
+ | `XTInd -> refine_appl metasenv subst args)
| _ -> refine_appl metasenv subst args)
| C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
| C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
NCicMetaSubst.saturate status metasenv subst context arity 0 in
let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
let metasenv, subst, term, _ =
- typeof_aux metasenv subst context (Some ind) term in
+ typeof_aux metasenv subst context (`XTSome ind) term in
let parameters, arguments = HExtlib.split_nth leftno args in
let outtype =
match outtype with
| C.Implicit _ as ot ->
let rec aux = function
- | [] -> NCic.Lambda ("_",NCic.Implicit `Type,ot)
- | _::tl -> NCic.Lambda ("_",NCic.Implicit `Type,aux tl)
+ | [] -> C.Lambda ("_",C.Implicit `Type,ot)
+ | _::tl -> C.Lambda ("_",C.Implicit `Type,aux tl)
in
aux arguments
| _ -> outtype
in
let metasenv, subst, outtype, outsort =
- typeof_aux metasenv subst context None outtype in
+ typeof_aux metasenv subst context `XTNone outtype in (* this cannot be `XTSort *)
(* next lines are to do a subst-expansion of the outtype, so
that when it becomes a beta-abstraction, the beta-redex is
if parameters = [] then C.Const r
else C.Appl ((C.Const r)::parameters) in
let metasenv, subst, ind, ind_ty =
- typeof_aux metasenv subst context None ind in
+ typeof_aux metasenv subst context `XTNone ind in (* FG: this cannot be `XTSort *)
let metasenv, subst =
check_allowed_sort_elimination status localise r orig_term metasenv subst
context ind ind_ty outsort
else C.Appl (C.Const cons::parameters)
in
let metasenv, subst, cons, ty_cons =
- typeof_aux metasenv subst context None cons in
+ typeof_aux metasenv subst context `XTNone cons in (* FG: this cannot be `XTInd *)
let ty_branch =
NCicTypeChecker.type_of_branch status
~subst context leftno outtype cons ty_cons in
status#ppterm ~metasenv ~subst ~context p ^ " ::inf:: " ^
status#ppterm ~metasenv ~subst ~context ty_branch ));
let metasenv, subst, p, _ =
- typeof_aux metasenv subst context (Some ty_branch) p in
+ typeof_aux metasenv subst context (`XTSome ty_branch) p in
j-1, metasenv, subst, p :: branches)
pl (List.length pl, metasenv, subst, [])
in
and check_type status ~localise metasenv subst context (ty as orig_ty) =
let metasenv, subst, ty, sort =
- typeof status ~localise metasenv subst context ty None
+ typeof status ~localise metasenv subst context ty `XTSort
in
let metasenv, subst, ty, _ =
force_to_sort status metasenv subst context ty orig_ty localise sort
let cs_subst = NCicSubstitution.subst status ~avoid_beta_redexes:true in
try
(match expty with
- `Type expty ->
+ `XTSome expty ->
pp (lazy "WWW: trying coercions -- preliminary unification");
let metasenv, subst =
NCicUnification.unify status metasenv subst context infty expty
in metasenv, subst, t, expty
- | _ -> raise (Failure "Special case Prod or Sort"))
+ | _ -> raise (Failure "Special case XTProd, XTSort or XTInd"))
with
| exn ->
(* we try with a coercion *)
let rec first exc = function
| [] ->
- pp (lazy "WWW: no more coercions!");
+ pp (lazy "WWW: no more coercions!");
raise (wrap_exc (lazy
let expty =
match expty with
- `Type expty -> status#ppterm ~metasenv ~subst ~context expty
- | `Sort -> "[[sort]]"
- | `Prod -> "[[prod]]" in
- (localise orig_t, Printf.sprintf
+ `XTSome expty -> status#ppterm ~metasenv ~subst ~context expty
+ | `XTSort -> "[[sort]]"
+ | `XTProd -> "[[prod]]"
+ | `XTInd -> "[[ind]]" in
+ (localise orig_t, Printf.sprintf
"The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
(status#ppterm ~metasenv ~subst ~context t)
(status#ppterm ~metasenv ~subst ~context infty)
let metasenv, subst =
NCicUnification.unify status metasenv subst context t meta in
match expty with
- `Type expty ->
+ `XTSome expty ->
pp (lazy ( "UNIFICATION in CTX:\n"^
status#ppcontext ~metasenv ~subst context
^ "\nMENV: " ^
NCicUnification.unify status metasenv subst context newtype expty
in
metasenv, subst, newterm, newtype
- | `Sort ->
+ | `XTSort ->
+ (match NCicReduction.whd status ~subst context newtype with
+ C.Sort _ -> metasenv,subst,newterm,newtype
+ | _ -> first exc tl)
+ | `XTInd ->
(match NCicReduction.whd status ~subst context newtype with
- NCic.Sort _ -> metasenv,subst,newterm,newtype
+ C.Const (Ref.Ref (_, Ref.Ind _)) -> metasenv,subst,newterm,newtype
| _ -> first exc tl)
- | `Prod ->
+ | `XTProd ->
(match NCicReduction.whd status ~subst context newtype with
- NCic.Prod _ -> metasenv,subst,newterm,newtype
+ C.Prod _ -> metasenv,subst,newterm,newtype
| _ -> first exc tl)
with
| NCicUnification.UnificationFailure _ -> first exc tl
try
pp (lazy "WWW: trying coercions -- inner check");
match infty, expty, t with
- (* `Sort|`Prod + Match not implemented *)
- | _,`Type expty, NCic.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) ->
+ (* `XTSort|`XTProd|`XTInd + Match not implemented *)
+ | _,`XTSome expty, C.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 =
let count_pis t =
let rec aux ctx t =
match NCicReduction.whd status ~subst ~delta:max_int ctx t with
- | NCic.Prod (name,src,tgt) ->
- let ctx = (name, (NCic.Decl src)) :: ctx in
+ | C.Prod (name,src,tgt) ->
+ let ctx = (name, (C.Decl src)) :: ctx in
1 + aux ctx tgt
| _ -> 0
in
let rec skip_lambda_delifting t n =
match t,n with
| _,0 -> t
- | NCic.Lambda (_,_,t),n ->
+ | C.Lambda (_,_,t),n ->
pp (lazy ("WWW: failing term? "^ status#ppterm ~subst:[] ~metasenv:[] ~context:[] t));
skip_lambda_delifting
(* substitute dangling indices with a dummy *)
- (NCicSubstitution.subst status (NCic.Sort NCic.Prop) t) (n - 1)
+ (NCicSubstitution.subst status (C.Sort C.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),_) ->
+ | C.Lambda (_,C.Const (Ref.Ref (_,Ref.Ind (_,_,_))),_) -> [],[]
+ | C.Lambda (_,C.Appl
+ (C.Const (Ref.Ref (_,Ref.Ind (_,_,_))) :: args),_) ->
HExtlib.split_nth n args
| _ -> assert false
in
(fun ty ->
List.fold_left
(fun t p -> match t with
- | NCic.Prod (_,_,t) ->
+ | C.Prod (_,_,t) ->
cs_subst p t
| _-> assert false)
ty left_p)
match t,n with
| _,0 ->
let rec mkr n = function
- | [] -> [] | _::tl -> NCic.Rel n :: mkr (n+1) tl
+ | [] -> [] | _::tl -> C.Rel n :: mkr (n+1) tl
in
pp (lazy ("input replace: " ^ status#ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
let bo =
~equality:(fun _ -> NCicRefineUtil.alpha_equivalence status)
~context:ctx
~what:(matched::right_p)
- ~with_what:(NCic.Rel 1::List.rev (mkr 2 right_p))
+ ~with_what:(C.Rel 1::List.rev (mkr 2 right_p))
~where:bo
in
pp (lazy ("output replace: " ^ status#ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
bo
- | NCic.Lambda (name, src, tgt),_ ->
- NCic.Lambda (name, src,
+ | C.Lambda (name, src, tgt),_ ->
+ C.Lambda (name, src,
keep_lambdas_and_put_expty
- ((name, NCic.Decl src)::ctx) tgt (NCicSubstitution.lift status 1 bo)
+ ((name, C.Decl src)::ctx) tgt (NCicSubstitution.lift status 1 bo)
(List.map (NCicSubstitution.lift status 1) right_p) (NCicSubstitution.lift status 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/basics/jmeq/jmeq.ind(1,0,2)")) in
- let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.con(0,1,2)")) in
+ (*let eq = C.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in
+ let eq_refl = C.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*)
+ let eq = C.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.ind(1,0,2)")) in
+ let eq_refl = C.Const (NReference.reference_of_string ("cic:/matita/basics/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) ->
+ | C.Prod (name, src, tgt) ->
let t,k =
aux
- ((name, NCic.Decl src) :: context)
- (NCicSubstitution.lift status 1 outty) (NCic.Rel j::par) (j+1)
+ ((name, C.Decl src) :: context)
+ (NCicSubstitution.lift status 1 outty) (C.Rel j::par) (j+1)
(NCicSubstitution.lift status 1 mty) (NCicSubstitution.lift status 1 m) tgt
in
- NCic.Prod (name, src, t), k
- | NCic.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r) ->
+ C.Prod (name, src, t), k
+ | C.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r) ->
let k =
- let k = NCic.Const(Ref.mk_constructor i r) in
+ let k = C.Const(Ref.mk_constructor i r) in
NCicUntrusted.mk_appl k par
in
(* the type has no parameters, so kty = mty
try NCicTypechecker.typeof ~subst ~metasenv context k
with NCicTypeChecker.TypeCheckerFailure _ -> assert false
in *)
- NCic.Prod ("p",
- NCic.Appl [eq; mty; m; mty; k],
+ C.Prod ("p",
+ C.Appl [eq; mty; m; mty; k],
(NCicSubstitution.lift status 1
(NCicReduction.head_beta_reduce status ~delta:max_int
(NCicUntrusted.mk_appl outty [k])))),[mty,m,mty,k]
- | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r)::pl) ->
+ | C.Appl (C.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
+ let k = C.Const(Ref.mk_constructor i r) in
NCicUntrusted.mk_appl k (left_p@par)
in
let right_p =
try match
NCicTypeChecker.typeof status ~subst ~metasenv context k
with
- | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
+ | C.Appl (C.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) ->
+ | C.Appl (C.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
snd (HExtlib.split_nth leftno args)
| _ -> assert false
in
try NCicTypeChecker.typeof status ~subst ~metasenv context y
with NCicTypeChecker.TypeCheckerFailure _ -> assert false
in
- NCic.Prod ("_", NCic.Appl [eq;xty;x;yty;y],
+ C.Prod ("_", C.Appl [eq;xty;x;yty;y],
NCicSubstitution.lift status 1 tacc), (xty,x,yty,y)::pacc)
(orig_right_p @ [m]) (right_p @ [k])
(NCicReduction.head_beta_reduce status ~delta:max_int
(* if has_rights then
NCicReduction.head_beta_reduce status ~delta:max_int
- (NCic.Appl (outty ::right_p @ [k])),k
+ (C.Appl (outty ::right_p @ [k])),k
else
- NCic.Prod ("p",
- NCic.Appl [eq; mty; m; k],
+ C.Prod ("p",
+ C.Appl [eq; mty; m; k],
(NCicSubstitution.lift status 1
(NCicReduction.head_beta_reduce status ~delta:max_int
- (NCic.Appl (outty ::right_p @ [k]))))),k*)
+ (C.Appl (outty ::right_p @ [k]))))),k*)
| _ -> assert false
in
aux context outty [] 1 mty m 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,
+ | C.Lambda (name,src,bo), C.Prod (_,_,ty) ->
+ C.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],
+ (fun (xty,x,yty,y) (n,acc) -> n+1, C.Lambda ("p" ^ string_of_int n,
+ C.Appl [eq; xty; x; yty; y],
NCicSubstitution.lift status 1 acc)) eqs (1,t))
- (*NCic.Lambda ("p",
- NCic.Appl [eq; mty; m; k],NCicSubstitution.lift status 1 t)*)
+ (*C.Lambda ("p",
+ C.Appl [eq; mty; m; k],NCicSubstitution.lift status 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 status 1 mty) (NCicSubstitution.lift status 1 m) tgt)
+ | C.Lambda (name, src, tgt) ->
+ let context = (name, C.Decl src)::context in
+ C.Lambda (name, src, aux context (NCicSubstitution.lift status 1 mty) (NCicSubstitution.lift status 1 m) tgt)
| t ->
let lhs =
match mty with
- | NCic.Appl (_::params) -> (snd (HExtlib.split_nth lno params))@[m]
+ | C.Appl (_::params) -> (snd (HExtlib.split_nth lno params))@[m]
| _ -> [m]
in
let rhs =
- List.map (fun x -> NCic.Rel x)
+ List.map (fun x -> C.Rel x)
(List.rev (HExtlib.list_seq 1 (rno+2))) in
List.fold_right2
(fun x y acc ->
try NCicTypeChecker.typeof status ~subst ~metasenv context y
with NCicTypeChecker.TypeCheckerFailure _ -> assert false
in
- NCic.Prod
- ("_", NCic.Appl [eq;xty;x;yty;y],
+ C.Prod
+ ("_", C.Appl [eq;xty;x;yty;y],
(NCicSubstitution.lift status 1 acc)))
lhs rhs t
- (* NCic.Prod
- ("_", NCic.Appl [eq;mty;m;NCic.Rel 1],
+ (* C.Prod
+ ("_", C.Appl [eq;mty;m;C.Rel 1],
NCicSubstitution.lift status 1 t)*)
in
aux context mty m new_outty
match
NCicTypeChecker.typeof status ~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 ->
+ | (C.Const (Ref.Ref (_,Ref.Ind (_,_,_))) | C.Meta _) as mty -> [], mty
+ | C.Appl ((C.Const (Ref.Ref (_,Ref.Ind (_,_,_)))|C.Meta _)::args) as mty ->
snd (HExtlib.split_nth leftno args), mty
| _ -> assert false
with NCicTypeChecker.TypeCheckerFailure _ ->
~context ~metasenv ~subst pbo));
let metasenv, subst, pbo, _ =
try_coercions status ~localise menv s context pbo
- orig_t (*??*) infty_pbo (`Type expty_pbo) exc
+ orig_t (*??*) infty_pbo (`XTSome expty_pbo) exc
in
pp
(lazy ("CASE: pbo2: " ^ status#ppterm
List.map
(fun t -> NCicTypeChecker.typeof status ~subst ~metasenv context t) right_p in
let eqs =
- List.map2 (fun x y -> NCic.Appl[eq_refl;x;y]) (right_tys@[mty])
+ List.map2 (fun x y -> C.Appl[eq_refl;x;y]) (right_tys@[mty])
(right_p@[m]) in
- let t = NCic.Appl (NCic.Match(r,new_outty,m,pl) :: eqs)
+ let t = C.Appl (C.Match(r,new_outty,m,pl) :: eqs)
in
metasenv, subst, t, expty (*}}}*)
- | _,`Type expty,NCic.LetIn(name,ty,t,bo) ->
+ | _,`XTSome expty,C.LetIn(name,ty,t,bo) ->
pp (lazy "LETIN");
let name' = mk_fresh_name context name in
- let context_bo = (name', NCic.Def (t,ty)) :: context in
+ let context_bo = (name', C.Def (t,ty)) :: context in
let metasenv, subst, bo2, _ =
try_coercions status ~localise metasenv subst context_bo
bo orig_t (NCicSubstitution.lift status 1 infty)
- (`Type (NCicSubstitution.lift status 1 expty)) exc
+ (`XTSome (NCicSubstitution.lift status 1 expty)) exc
in
- let coerced = NCic.LetIn (name',ty,t,bo2) in
+ let coerced = C.LetIn (name',ty,t,bo2) in
pp (lazy ("LETIN: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced));
metasenv, subst, coerced, expty
- | NCic.Prod (nameprod, src, ty),`Type (NCic.Prod (_, src2, ty2) as expty), _ ->
+ | C.Prod (nameprod, src, ty),`XTSome (C.Prod (_, src2, ty2) as expty), _ ->
(*{{{*) pp (lazy "LAM");
pp (lazy ("LAM: t = " ^ status#ppterm ~metasenv ~subst ~context t));
- let namename = match t with NCic.Lambda (n,_,_) -> n | _ -> nameprod in
+ let namename = match t with C.Lambda (n,_,_) -> n | _ -> nameprod in
let name_con = mk_fresh_name context namename in
- let context_src2 = ((name_con, NCic.Decl src2) :: context) in
+ let context_src2 = ((name_con, C.Decl src2) :: context) in
(* contravariant part: the argument of f:src->ty *)
let metasenv, subst, rel1, _ =
try_coercions status ~localise metasenv subst context_src2
- (NCic.Rel 1) orig_t (NCicSubstitution.lift status 1 src2)
- (`Type (NCicSubstitution.lift status 1 src)) exc
+ (C.Rel 1) orig_t (NCicSubstitution.lift status 1 src2)
+ (`XTSome (NCicSubstitution.lift status 1 src)) 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 status 2 1 bo)
+ | C.Lambda (n,_,bo) -> n, cs_subst rel1 (NCicSubstitution.lift_from status 2 1 bo)
| _ -> name_con, NCicUntrusted.mk_appl (NCicSubstitution.lift status 1 t) [rel1]
in
(* we fix the possible dependency problem in the source ty *)
let ty = cs_subst rel1 (NCicSubstitution.lift_from status 2 1 ty) in
let metasenv, subst, bo, _ =
try_coercions status ~localise metasenv subst context_src2
- bo orig_t ty (`Type ty2) exc
+ bo orig_t ty (`XTSome ty2) exc
in
- let coerced = NCic.Lambda (name_t,src2, bo) in
+ let coerced = C.Lambda (name_t,src2, bo) in
pp (lazy ("LAM: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced));
metasenv, subst, coerced, expty (*}}}*)
| _ -> raise exc
with exc2 ->
let expty =
match expty with
- `Type expty -> expty
- | `Sort ->
- NCic.Sort (NCic.Type
+ `XTSome expty -> expty
+ | `XTSort ->
+ C.Sort (C.Type
(match NCicEnvironment.get_universes () with
| x::_ -> x
| _ -> assert false))
- | `Prod -> NCic.Prod ("_",NCic.Implicit `Type,NCic.Implicit `Type)
+ | `XTProd -> C.Prod ("_",C.Implicit `Type,C.Implicit `Type)
in
pp(lazy("try_coercion " ^
status#ppterm ~metasenv ~subst ~context infty ^ " |---> " ^
RefineFailure msg
in
try_coercions status ~localise metasenv subst context
- t orig_t ty `Sort exn
+ t orig_t ty `XTSort exn
+
+and force_to_inductive status metasenv subst context t orig_t localise ty =
+ try
+ let metasenv, subst, ty =
+ NCicUnification.indfy status (Failure "indfy") metasenv subst context ty in
+ metasenv, subst, t, ty
+ with
+ Failure _ ->
+ let msg =
+ (lazy (localise orig_t,
+ "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
+ " is not a (co)inductive type: " ^ status#ppterm ~metasenv ~subst ~context ty)) in
+ let ty = NCicReduction.whd status ~subst context ty in
+(* prerr_endline ("#### " ^ status#ppterm ~metasenv ~subst ~context ty); *)
+ let exn =
+ if NCicUnification.could_reduce status ~subst context ty then
+ Uncertain msg
+ else
+ RefineFailure msg
+ in
+ raise exn
+(* FG: this should be as follows but the case `XTInd is not imp;emented yet
+ try_coercions status ~localise metasenv subst context
+ t orig_t ty `XTInd exn
+*)
and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s)
t (t1, t2)
pp(lazy("FORCE FINAL APPL: " ^
status#ppterm ~metasenv ~subst ~context res ^
" of type " ^ status#ppterm ~metasenv ~subst ~context ty_he
- ^ " to type " ^ match expty with None -> "None" | Some x ->
+ ^ " to type " ^ match expty with `XTSort -> "Any sort" | `XTInd -> "Any (co)inductive type"
+ | `XTNone -> "None" | `XTSome x ->
status#ppterm ~metasenv ~subst ~context x));
(* whatever the term is, we force the type. in case of ((Lambda..) ?...)
* the application may also be a lambda! *)
force_ty false false metasenv subst context orig_t res ty_he expty
- | NCic.Implicit `Vector::tl ->
+ | C.Implicit `Vector::tl ->
let has_some_more_pis x =
match NCicReduction.whd status ~subst context x with
- | NCic.Meta _ | NCic.Appl (NCic.Meta _::_) -> false
+ | C.Meta _ | C.Appl (C.Meta _::_) -> false
| _ -> true
in
(try
| RefineFailure _ as exc when has_some_more_pis ty_he ->
(try
aux metasenv subst args_so_far he ty_he
- (NCic.Implicit `Term :: NCic.Implicit `Vector :: tl)
+ (C.Implicit `Term :: C.Implicit `Vector :: tl)
with
Uncertain msg | RefineFailure msg -> raise (wrap_exc msg exc))
| RefineFailure msg when not (has_some_more_pis ty_he) ->
match NCicReduction.whd status ~subst context ty_he with
| C.Prod (_,s,t) ->
let metasenv, subst, arg, _ =
- typeof status ~localise metasenv subst context arg (Some s) in
+ typeof status ~localise metasenv subst context arg (`XTSome s) in
let t = NCicSubstitution.subst status ~avoid_beta_redexes:true arg t in
aux metasenv subst (arg :: args_so_far) he t tl
| C.Meta _
| C.Appl (C.Meta _ :: _) as t ->
let metasenv, subst, arg, ty_arg =
- typeof status ~localise metasenv subst context arg None in
+ typeof status ~localise metasenv subst context arg `XTNone in
let name = guess_name status subst context ty_arg in
let metasenv, _, meta, _ =
NCicMetaSubst.mk_meta metasenv
let flex_prod = C.Prod (name, ty_arg, meta) in
(* next line grants that ty_args is a type *)
let metasenv,subst, flex_prod, _ =
- typeof status ~localise metasenv subst context flex_prod None in
+ typeof status ~localise metasenv subst context flex_prod `XTSort in
(*
pp (lazy ( "UNIFICATION in CTX:\n"^
status#ppcontext ~metasenv ~subst context
let metasenv, subst, newhead, newheadty =
try_coercions status ~localise metasenv subst context
(NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty
- `Prod
+ `XTProd
(RefineFailure (lazy (localise orig_he, Printf.sprintf
("The term %s is here applied to %d arguments but expects " ^^
"only %d arguments") (status#ppterm ~metasenv ~subst ~context he)
(HExtlib.list_mapi
(fun (_,_,rno,_,_,_) i ->
let i = len - i - 1 in
- NCic.Const
+ C.Const
(if inductive then NReference.mk_fix i rno ref
else NReference.mk_cofix i ref))
rev_fl)
match bo with
| Some bo ->
let metasenv, subst, bo, ty =
- typeof status ~localise metasenv subst [] bo (Some ty) in
+ typeof status ~localise metasenv subst [] bo (`XTSome ty) in
let height = (* XXX recalculate *) height in
metasenv, subst, Some bo, ty, height
| None -> metasenv, subst, None, ty, 0
List.fold_left
(fun (metasenv,subst,fl) (relevance,name,k,ty,dbo,localise) ->
let metasenv, subst, dbo, ty =
- typeof status ~localise metasenv subst types dbo (Some ty)
+ typeof status ~localise metasenv subst types dbo (`XTSome ty)
in
metasenv, subst, (relevance,name,k,ty,dbo)::fl)
(metasenv, subst, []) rev_fl
(fun (metasenv,subst,res,ctx) (relevance,n,ty,cl) ->
let metasenv, subst, ty =
check_type status ~localise metasenv subst [] ty in
- metasenv,subst,(relevance,n,ty,cl)::res,(n,NCic.Decl ty)::ctx
+ metasenv,subst,(relevance,n,ty,cl)::res,(n,C.Decl ty)::ctx
) (metasenv,subst,[],[]) itl in
let metasenv,subst,itl,_ =
List.fold_left
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
+ | C.Meta _ -> metasenv, subst
+ | C.Implicit _ -> metasenv, subst
+ | C.Appl (C.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
(fun ((metasenv, subst),l) arg ->
NCicUnification.unify status
~test_eq_only:true metasenv subst context arg
- (NCic.Rel (ctxlen - len - l)), l+1
+ (C.Rel (ctxlen - len - l)), l+1
)
((metasenv, subst), 0) lefts
in
NCicSubstitution.psubst status
(fun i ->
if i <= leftno then
- NCic.Rel i
+ C.Rel i
else
- NCic.Const (NReference.reference_of_spec uri
+ C.Const (NReference.reference_of_spec uri
(NReference.Ind (ind,relsno - i,leftno))))
(HExtlib.list_seq 1 (relsno+1))
te in
List.fold_right
(fun (name,decl) te ->
match decl with
- NCic.Decl ty -> NCic.Prod (name,ty,te)
- | NCic.Def (bo,ty) -> NCic.LetIn (name,ty,bo,te)
+ C.Decl ty -> C.Prod (name,ty,te)
+ | C.Def (bo,ty) -> C.LetIn (name,ty,bo,te)
) sx_context_te_rev te
in
metasenv,subst,(k_relev,n,te)::res
exception Uncertain of (Stdpp.location * string) Lazy.t;;
exception AssertFailure of string Lazy.t;;
+type 'a expected_type = [ `XTNone (* unknown *)
+ | `XTSome of 'a (* the given term *)
+ | `XTSort (* any sort *)
+ | `XTInd (* any (co)inductive type *)
+ ]
val typeof :
#NCicCoercion.status ->
?localise:(NCic.term -> Stdpp.location) ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
- NCic.term -> NCic.term option -> (* term, expected type *)
+ NCic.term -> NCic.term expected_type -> (* term, expected type *)
NCic.metasenv * NCic.substitution * NCic.term * NCic.term
(* menv, subst,refined term, type *)
in
metasenv,subst,t
+let indfy status exc metasenv subst context t =
+ let t = NCicReduction.whd status ~subst context t in
+ let metasenv,subst =
+ match t with
+ | NCic.Const (Ref.Ref (_, Ref.Ind _))
+ | NCic.Appl (NCic.Const (Ref.Ref (_, Ref.Ind _))::_) -> metasenv, subst
+(*
+ | NCic.Meta (n,_) ->
+ let attrs, context, ty = NCicUtils.lookup_meta n metasenv in
+ let kind = NCicUntrusted.kind_of_meta attrs in
+ if kind = `IsSort then
+ metasenv,subst
+ else
+ (match ty with
+ | NCic.Implicit (`Typeof _) ->
+ metasenv_to_subst n (`IsSort,[],ty) metasenv subst
+ | ty ->
+ let metasenv,subst,ty = sortfy status exc metasenv subst context ty in
+ metasenv_to_subst n (`IsSort,[],ty) metasenv subst)
+*)
+ | NCic.Implicit _ -> assert false
+ | _ -> raise exc
+ in
+ metasenv,subst,t
+
let tipify status exc metasenv subst context t ty =
let is_type attrs =
match NCicUntrusted.kind_of_meta attrs with
NCic.status -> exn -> NCic.metasenv -> NCic.substitution -> NCic.context ->
NCic.term -> NCic.metasenv * NCic.substitution * NCic.term
+val indfy :#
+ NCic.status -> exn -> NCic.metasenv -> NCic.substitution -> NCic.context ->
+ NCic.term -> NCic.metasenv * NCic.substitution * NCic.term
+
val debug : bool ref
(function x::_ -> x | _ -> assert false) 80
(NotationPres.mpres_of_box boxml)));
*)
+ let attrs = `Generated, `Definition, pragma in
NotationPt.Theorem
- (`Definition,srec_name,
- NotationPt.Implicit `JustOne,Some res,pragma)
+ (srec_name, NotationPt.Implicit `JustOne, Some res, attrs)
;;
let ast_of_sort s =
(function x::_ -> x | _ -> assert false)
80 (NotationPres.render (fun _ -> None)
(TermContentPres.pp_ast res)));*)
+ let attrs = `Generated, `Definition, `Projection in
NotationPt.Theorem
- (`Definition,projname,NotationPt.Implicit `JustOne,Some res,`Projection)
+ (projname, NotationPt.Implicit `JustOne, Some res, attrs)
;;
let mk_projections status (_,_,_,_,obj) =
(* PHASE 2: create the object for the proof of the principle: we'll name it
* "theorem" *)
let status, theorem =
- GrafiteDisambiguate.disambiguate_nobj status ~baseuri
+ let attrs = `Generated, `Theorem, `DiscriminationPrinciple in
+ GrafiteDisambiguate.disambiguate_nobj status ~baseuri
(baseuri ^ name ^ ".def",0,
NotationPt.Theorem
- (`Theorem,name,principle,
- Some (NotationPt.Implicit (`Tagged "inv")),`DiscriminationPrinciple))
+ (name, principle, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
in
let uri,height,nmenv,nsubst,nobj = theorem in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
mk_prods hyplist (mk_appl (mk_id "P"::id_rs))))))
in
let status, theorem =
- GrafiteDisambiguate.disambiguate_nobj status ~baseuri
+ let attrs = `Generated, `Theorem, `InversionPrinciple in
+ GrafiteDisambiguate.disambiguate_nobj status ~baseuri
(baseuri ^ name ^ ".def",0,
NotationPt.Theorem
- (`Theorem,name,theorem,
- Some (NotationPt.Implicit (`Tagged "inv")),`InversionPrinciple))
+ (name,theorem, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
in
let uri,height,nmenv,nsubst,nobj = theorem in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
let disambiguate status context t ty =
let status, expty =
match ty with
- | None -> status, None
- | Some ty ->
- let status, (_,x) = relocate status context ty in status, Some x
+ | `XTSome ty ->
+ let status, (_,x) = relocate status context ty in status, `XTSome x
+ | `XTNone -> status, `XTNone
+ | `XTSort -> status, `XTSort
+ | `XTInd -> status, `XTInd
in
let uri,height,metasenv,subst,obj = status#obj in
let metasenv, subst, status, t =
let status, (_,term) = relocate status ctx term in
let status, expty =
match expty with
- None -> status, None
- | Some e ->
- let status, (_, e) = relocate status ctx e in status, Some e
+ | `XTSome e ->
+ let status, (_, e) = relocate status ctx e in status, `XTSome e
+ | `XTNone -> status, `XTNone
+ | `XTSort -> status, `XTSort
+ | `XTInd -> status, `XTInd
in
let name,height,metasenv,subst,obj = status#obj in
let metasenv,subst,t,ty =
let _,_,metasenv,_,_ = status#obj in
let gname, context, gty = List.assoc i metasenv in
if dorefine then
- let status, (_,t), (_,ty) = refine status context t (Some (context,gty)) in
+ let status, (_,t), (_,ty) = refine status context t (`XTSome (context,gty)) in
to_subst status i (gname,context,t,ty)
else
let status,(_,ty) = typeof status context t in
let _,_,metasenv,_,_ = status#obj in
let gname, context, gty = List.assoc i metasenv in
let ggty = mk_cic_term context gty in
- let status, (_,t) = disambiguate status context t (Some ggty) in
+ let status, (_,t) = disambiguate status context t (`XTSome ggty) in
to_subst status i (gname,context,t,gty)
;;
| NCic.Implicit `Hole, t ->
(match wanted with
| Some wanted ->
- let status', wanted = disambiguate status ctx wanted None in
+ let status', wanted = disambiguate status ctx wanted `XTNone in
pp(lazy("wanted: "^ppterm status' wanted));
let (status',found), t' = match_term status' ctx wanted t in
if found then status',t' else status,t
val mk_cic_term : NCic.context -> NCic.term -> cic_term
val disambiguate:
- #pstatus as 'status -> NCic.context -> tactic_term -> cic_term option ->
+ #pstatus as 'status -> NCic.context -> tactic_term -> cic_term NCicRefiner.expected_type ->
'status * cic_term (* * cic_term XXX *)
val analyse_indty:
val unify:
#pstatus as 'status -> NCic.context -> cic_term -> cic_term -> 'status
val refine:
- #pstatus as 'status -> NCic.context -> cic_term -> cic_term option ->
+ #pstatus as 'status -> NCic.context -> cic_term -> cic_term NCicRefiner.expected_type ->
'status * cic_term * cic_term (* status, term, type *)
val apply_subst:
#pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term
_,_,(None,_,_) -> fail (lazy "No term to generalize")
| txt,txtlen,(Some what,_,_) ->
let status, what =
- disambiguate status (ctx_of goalty) (txt,txtlen,what) None
+ disambiguate status (ctx_of goalty) (txt,txtlen,what) `XTNone
in
status,what,[]
)
let change_tac ~where ~with_what =
let change status t =
- let status, ww = disambiguate status (ctx_of t) with_what None in
+(* FG: `XTSort could be used when we change the whole goal *)
+ let status, ww = disambiguate status (ctx_of t) with_what `XTNone in
let status = unify status (ctx_of t) t ww in
status, ww
in
let analyze_indty_tac ~what indtyref =
distribute_tac (fun (status as orig_status) goal ->
let goalty = get_goalty status goal in
- let status, what = disambiguate status (ctx_of goalty) what None in
+ let status, what = disambiguate status (ctx_of goalty) what `XTInd in
let status, ty_what = typeof status (ctx_of what) what in
let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
let leftno = List.length lefts in
let cases ~what status goal =
let gty = get_goalty status goal in
- let status, what = disambiguate status (ctx_of gty) what None in
+ let status, what = disambiguate status (ctx_of gty) what `XTInd in
let status, ty = typeof status (ctx_of what) what in
let status, (ref, consno, _, _) = analyse_indty status ty in
let status, what = term_of_cic_term status what (ctx_of gty) in
let t =
NCic.Match (ref,NCic.Implicit `Term, what,
HExtlib.mk_list (NCic.Implicit `Term) consno)
- in
+ in
instantiate status goal (mk_cic_term (ctx_of gty) t)
;;
let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
let gty = get_goalty status goal in
let eq status ctx t1 t2 =
- let status,t1 = disambiguate status ctx t1 None in
+ let status,t1 = disambiguate status ctx t1 `XTSort in
let status,t1 = apply_subst status ctx t1 in
let status,t1 = term_of_cic_term status t1 ctx in
let t2 = mk_cic_term ctx t2 in
let is_a_fact_ast status subst metasenv ctx cand =
noprint ~depth:0
(lazy ("checking facts " ^ NotationPp.pp_term status cand));
- let status, t = disambiguate status ctx ("",0,cand) None in
+ let status, t = disambiguate status ctx ("",0,cand) `XTNone in
let status,t = term_of_cic_term status t ctx in
let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
is_a_fact status (mk_cic_term ctx ty)
NCicUnification.unify status metasenv subst ctx gty pty *)
NCicRefiner.typeof
(status#set_coerc_db NCicCoercion.empty_db)
- metasenv subst ctx pt (Some gty)
+ metasenv subst ctx pt (`XTSome gty)
in
noprint (lazy (Printf.sprintf "Refined in %fs"
(Unix.gettimeofday() -. stamp)));
let status,lemmas =
List.fold_left
(fun (status,lemmas) l ->
- let status,l = NTacStatus.disambiguate status ctx l None in
+ let status,l = NTacStatus.disambiguate status ctx l `XTNone in
let status,l = NTacStatus.term_of_cic_term status l ctx in
status,l::lemmas)
(status,[]) lemmas in
let n,h,metasenv,subst,o = status#obj in
let gname, ctx, gty = List.assoc g metasenv in
(* let ggty = mk_cic_term context gty in *)
- let status, t = disambiguate status ctx t None in
+ let status, t = disambiguate status ctx t `XTNone in
let status,t = term_of_cic_term status t ctx in
let _,_,metasenv,subst,_ = status#obj in
let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
let sort_candidates status ctx candidates =
let _,_,metasenv,subst,_ = status#obj in
let branch cand =
- let status,ct = disambiguate status ctx ("",0,cand) None in
+ let status,ct = disambiguate status ctx ("",0,cand) `XTNone in
let status,t = term_of_cic_term status ct ctx in
let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
let res = branch status (mk_cic_term ctx ty) in
| None -> None
| Some l ->
let to_Ast t =
- let status, res = disambiguate status [] t None in
+(* FG: `XTSort here? *)
+ let status, res = disambiguate status [] t `XTNone in
let _,res = term_of_cic_term status res (ctx_of res)
in Ast.NCic res
in Some (List.map to_Ast l)
(* Note: this cannot be in lib because of the missing xoa quantifier *)
lemma lstar_inv_pos: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → 0 < |l| →
∃∃a,ll,b. a::ll = l & R a b1 b & lstar A B R ll b b2.
-#A #B #R #l #b1 #b2 #H @(lstar_ind_l ????????? H) -b1
+#A #B #R #l #b1 #b2 #H @(lstar_ind_l … l b1 H) -l -b1
[ #H elim (lt_refl_false … H)
| #a #ll #b1 #b #Hb1 #Hb2 #_ #_ /2 width=6/ (**) (* auto fail if we do not remove the inductive premise *)
]
| #s #N1 #C1 #C2 #Hs #HN1 #_ #IHC12 #d #M1 #HMN1
elim (pl_sreds_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2
elim (lift_inv_abst … HM2) -HM2 #A1 #HAC1 #HM2 destruct
- elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *)
+ elim (IHC12 …) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *)
@(ex2_intro … (𝛌.A2)) // /2 width=5/
| #s #N1 #D1 #D2 #C1 #C2 #Hs #HN1 #_ #_ #IHD12 #IHC12 #d #M1 #HMN1
elim (pl_sreds_inv_lift … HN1 … HMN1) -N1 #M2 #HM12 #HM2
elim (lift_inv_appl … HM2) -HM2 #B1 #A1 #HBD1 #HAC1 #HM2 destruct
- elim (IHD12 ???) -IHD12 [4: // |2,3: skip ] #B2 #HB12 #HBD2 destruct (**) (* simplify line *)
- elim (IHC12 ???) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *)
+ elim (IHD12 …) -IHD12 [4: // |2,3: skip ] #B2 #HB12 #HBD2 destruct (**) (* simplify line *)
+ elim (IHC12 …) -IHC12 [4: // |2,3: skip ] #A2 #HA12 #HAC2 destruct (**) (* simplify line *)
@(ex2_intro … (@B2.A2)) // /2 width=7/
]
qed-.
lemma dst_step_dx: ∀p,M,M2. M ↦[p] M2 → ∀M1. M1 ⓢ↦* M → M1 ⓢ↦* M2.
#p #M #M2 #H elim H -p -M -M2
[ #B #A #M1 #H
- elim (dst_inv_appl … H ???) -H [4: // |2,3: skip ] #s #B1 #M #Hs #HM1 #HB1 #H (**) (* simplify line *)
- elim (dst_inv_abst … H ??) -H [3: // |2: skip ] #r #A1 #Hr #HM #HA1 (**) (* simplify line *)
+ elim (dst_inv_appl … H …) -H [4: // |2,3: skip ] #s #B1 #M #Hs #HM1 #HB1 #H (**) (* simplify line *)
+ elim (dst_inv_abst … H …) -H [3: // |2: skip ] #r #A1 #Hr #HM #HA1 (**) (* simplify line *)
lapply (pl_sreds_trans … HM1 … (dx:::r) (@B1.𝛌.A1) ?) /2 width=1/ -M #HM1
lapply (pl_sreds_step_dx … HM1 (◊) ([↙B1]A1) ?) -HM1 // #HM1
@(dst_step_sn … HM1) /2 width=1/ /4 width=1/
| #p #A #A2 #_ #IHA2 #M1 #H
- elim (dst_inv_abst … H ??) -H [3: // |2: skip ] /3 width=5/ (**) (* simplify line *)
+ elim (dst_inv_abst … H …) -H [3: // |2: skip ] /3 width=5/ (**) (* simplify line *)
| #p #B #B2 #A #_ #IHB2 #M1 #H
- elim (dst_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *)
+ elim (dst_inv_appl … H …) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *)
| #p #B #A #A2 #_ #IHA2 #M1 #H
- elim (dst_inv_appl … H ???) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *)
+ elim (dst_inv_appl … H …) -H [4: // |2,3: skip ] /3 width=7/ (**) (* simplify line *)
]
qed-.
lemma pl_sreds_dst: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⓢ↦* M2.
-#s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 // /2 width=4 by dst_step_dx/
+#s #M1 #M2 #H @(lstar_ind_r … s M2 H) -s -M2 // /2 width=4 by dst_step_dx/
qed.
lemma dst_inv_pl_sreds_is_standard: ∀M,N. M ⓢ↦* N →
∃∃q,M2. in_whd q & M1 ↦[q] M2 & M2 ⓢ↦* N2.
#p #H @(in_whd_ind … H) -p
[ #N1 #N2 #H1 #M1 #H2
- elim (pl_sred_inv_nil … H1 ?) -H1 // #D #C #HN1 #HN2
+ elim (pl_sred_inv_nil … H1 …) -H1 // #D #C #HN1 #HN2
elim (dst_inv_appl … H2 … HN1) -N1 #s1 #D1 #N #Hs1 #HM1 #HD1 #H
- elim (dst_inv_abst … H ??) -H [3: // |2: skip ] #s2 #C1 #Hs2 #HN #HC1 (**) (* simplify line *)
+ elim (dst_inv_abst … H …) -H [3: // |2: skip ] #s2 #C1 #Hs2 #HN #HC1 (**) (* simplify line *)
lapply (pl_sreds_trans … HM1 … (dx:::s2) (@D1.𝛌.C1) ?) /2 width=1/ -N #HM1
lapply (pl_sreds_step_dx … HM1 (◊) ([↙D1]C1) ?) -HM1 // #HM1
- elim (pl_sreds_inv_pos … HM1 ?) -HM1
+ elim (pl_sreds_inv_pos … HM1 …) -HM1
[2: >length_append normalize in ⊢ (??(??%)); // ]
#q #r #M #Hq #HM1 #HM
lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -s1 -s2 * #Hq #Hr
@(ex3_2_intro … HM1) -M1 // -q
@(dst_step_sn … HM) /2 width=1/
| #p #_ #IHp #N1 #N2 #H1 #M1 #H2
- elim (pl_sred_inv_dx … H1 ??) -H1 [3: // |2: skip ] #D #C1 #C2 #HC12 #HN1 #HN2 (**) (* simplify line *)
+ elim (pl_sred_inv_dx … H1 …) -H1 [3: // |2: skip ] #D #C1 #C2 #HC12 #HN1 #HN2 (**) (* simplify line *)
elim (dst_inv_appl … H2 … HN1) -N1 #s #B #A1 #Hs #HM1 #HBD #HAC1
elim (IHp … HC12 … HAC1) -p -C1 #p #C1 #Hp #HAC1 #HC12
lapply (pl_sreds_step_dx … HM1 (dx::p) (@B.C1) ?) -HM1 /2 width=1/ -A1 #HM1
- elim (pl_sreds_inv_pos … HM1 ?) -HM1
+ elim (pl_sreds_inv_pos … HM1 …) -HM1
[2: >length_append normalize in ⊢ (??(??%)); // ]
#q #r #M #Hq #HM1 #HM
lapply (rewrite_r ?? is_whd … Hq) -Hq /4 width=1/ -p -s * #Hq #Hr
theorem pl_sred_mono: ∀p. singlevalued … (pl_sred p).
#p #M #N1 #H elim H -p -M -N1
-[ #B #A #N2 #H elim (pl_sred_inv_nil … H ?) -H //
+[ #B #A #N2 #H elim (pl_sred_inv_nil … H …) -H //
#D #C #H #HN2 destruct //
-| #p #A1 #A2 #_ #IHA12 #N2 #H elim (pl_sred_inv_rc … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+| #p #A1 #A2 #_ #IHA12 #N2 #H elim (pl_sred_inv_rc … H …) -H [3: // |2: skip ] (**) (* simplify line *)
#C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
-| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (pl_sred_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (pl_sred_inv_sn … H …) -H [3: // |2: skip ] (**) (* simplify line *)
#D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/
-| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (pl_sred_inv_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (pl_sred_inv_dx … H …) -H [3: // |2: skip ] (**) (* simplify line *)
#D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
]
qed-.
| #p #s #F1 #F #HF1 #_ #IHF2 #r #H -b2
elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr
elim (pl_st_inv_rc … HF1 … Hp) -HF1 -p #b1 #T1 #T #HT1 #HF1 #HF destruct
- elim (IHF2 ??) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
+ elim (IHF2 …) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
#b0 #T0 #HT02 #H destruct
lapply (pl_sts_step_sn … HT1 … HT02) -T /2 width=4/
]
| #p #s #F1 #F #HF1 #_ #IHF2 #r #H -b2
elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr
elim (pl_st_inv_sn … HF1 … Hp) -HF1 -p #b1 #V1 #V #T1 #HV1 #HF1 #HF destruct
- elim (IHF2 ??) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
+ elim (IHF2 …) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
#b0 #V0 #T0 #HV02 #H destruct
lapply (pl_sts_step_sn … HV1 … HV02) -V /2 width=5/
]
| #p #s #F1 #F #HF1 #_ #IHF2 #r #H
elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr
elim (pl_st_inv_dx … HF1 … Hp) -HF1 -p #b0 #V0 #T1 #T #HT1 #HF1 #HF destruct
- elim (IHF2 ??) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
+ elim (IHF2 …) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
#T0 #HT02 #H destruct
lapply (pl_sts_step_sn … HT1 … HT02) -T /2 width=3/
]
∃∃b1,V1,T1,T0. V1 Ⓡ↦*[r] V2 & T1 Ⓡ↦*[s] T0 & {b1}@V1.T1 = F1.
#b2 #s #r #F1 #V2 #T2 #H
elim (pl_sts_inv_trans … H) -H #F #HF1 #H
-elim (pl_sts_inv_sn_appl_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+elim (pl_sts_inv_sn_appl_dx … H …) -H [3: // |2: skip ] (**) (* simplify line *)
#b #V #T #HV2 #H destruct
-elim (pl_sts_inv_dx_appl_dx … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *)
+elim (pl_sts_inv_dx_appl_dx … HF1 …) -HF1 [3: // |2: skip ] (**) (* simplify line *)
#T1 #HT1 #H destruct /2 width=7/
qed-.
theorem pl_sts_fwd_is_standard: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → is_standard s.
#s elim s -s // #p1 * //
#p2 #s #IHs #F1 #F2 #H
-elim (pl_sts_inv_cons … H ???) -H [4: // |2,3: skip ] #F3 #HF13 #H (**) (* simplify line *)
-elim (pl_sts_inv_cons … H ???) [2: // |3,4: skip ] #F4 #HF34 #_ (**) (* simplify line *)
+elim (pl_sts_inv_cons … H …) -H [4: // |2,3: skip ] #F3 #HF13 #H (**) (* simplify line *)
+elim (pl_sts_inv_cons … H …) [2: // |3,4: skip ] #F4 #HF34 #_ (**) (* simplify line *)
lapply (pl_st_fwd_sle … HF13 … HF34) -F1 -F4 /3 width=3/
qed-.
[ #_ @(ex2_2_intro … ◊ ◊) // (**) (* auto needs some help here *)
| #p #s #F1 #F #HF1 #HF2 #IHF1 #Hs
lapply (is_standard_fwd_cons … Hs) #H
- elim (IHF1 ?) // -IHF1 -H #r1 #r2 #Hr1 #H destruct
+ elim (IHF1 …) // -IHF1 -H #r1 #r2 #Hr1 #H destruct
elim (in_whd_or_in_inner p) #Hp
[ -Hs -F1 -F -T2 -b2
@(ex2_2_intro … (p::r1) r2) // /2 width=1/ (**) (* auto needs some help here *)
elim (in_inner_inv … Hp) -Hp * #q [3: #IHq ] #Hp
(* case 1: dx *)
[ -IHq
- elim (pl_sts_inv_rc_abst_dx … HF2 ??) -b2 [3: // |2: skip ] (**) (* simplify line *)
+ elim (pl_sts_inv_rc_abst_dx … HF2 …) -b2 [3: // |2: skip ] (**) (* simplify line *)
#b #T #_ #HT -T2
- elim (pl_st_inv_dx … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *)
+ elim (pl_st_inv_dx … HF1 …) -HF1 [3: // |2: skip ] (**) (* simplify line *)
#c #V #T1 #T0 #_ #_ #HT0 -q -T1 -F1 destruct
(* case 2: rc *)
| destruct -F1 -F -T2 -b2
@(ex2_2_intro … ◊ (q::r2)) // (**) (* auto needs some help here *)
(* case 3: sn *)
- | elim (pl_sts_inv_rc_abst_dx … HF2 ??) -b2 [3: // |2: skip ] (**) (* simplify line *)
+ | elim (pl_sts_inv_rc_abst_dx … HF2 …) -b2 [3: // |2: skip ] (**) (* simplify line *)
#b #T #_ #HT -T2
- elim (pl_st_inv_sn … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *)
+ elim (pl_st_inv_sn … HF1 …) -HF1 [3: // |2: skip ] (**) (* simplify line *)
#c #V1 #V #T0 #_ #_ #HT0 -c -q -V1 -F1 destruct
]
]
[ #_ @(ex3_3_intro … ◊ ◊ ◊) // (**) (* auto needs some help here *)
| #p #s #F1 #F #HF1 #HF2 #IHF1 #Hs
lapply (is_standard_fwd_cons … Hs) #H
- elim (IHF1 ?) // -IHF1 -H #r1 #r2 #r3 #Hr1 #Hr2 #H destruct
+ elim (IHF1 …) // -IHF1 -H #r1 #r2 #r3 #Hr1 #Hr2 #H destruct
elim (in_whd_or_in_inner p) #Hp
[ -Hs -F1 -F -V2 -T2 -b2
@(ex3_3_intro … (p::r1) r2 r3) // /2 width=1/ (**) (* auto needs some help here *)
elim (carrier_inv_abst … HF) -HF #b #T #HT #HF destruct
elim (pl_sts_fwd_abst_dx … HM1) #r1 #r2 #Hr1 #H destruct
elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT
- elim (pl_sts_inv_pl_sreds … HM1 ?) // #M0 #_ #H -M1 -Hr1 destruct
+ elim (pl_sts_inv_pl_sreds … HM1 …) // #M0 #_ #H -M1 -Hr1 destruct
>associative_append in Hs; #Hs
lapply (is_standard_fwd_append_dx … Hs) -r1
<(map_cons_append … r2 (p::◊)) #H
lapply (is_standard_inv_compatible_rc … H) -H #Hp
- elim (pl_sts_inv_rc_abst_dx … HT ??) -HT [3: // |2: skip ] #b0 #T0 #HT02 #H (**) (* simplify line *)
+ elim (pl_sts_inv_rc_abst_dx … HT …) -HT [3: // |2: skip ] #b0 #T0 #HT02 #H (**) (* simplify line *)
elim (boolean_inv_abst … (sym_eq … H)) -H #A0 #_ #H #_ -b0 -M0 destruct
- elim (IHA12 … HT02 ?) // -r2 -A0 -IHA12 #F2 #HF2 #H
+ elim (IHA12 … HT02 …) // -r2 -A0 -IHA12 #F2 #HF2 #H
@(ex2_intro … ({⊥}𝛌.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *)
| #p #B1 #B2 #A #_ #IHB12 #F #HF #s #M1 #HM1 #Hs
elim (carrier_inv_appl … HF) -HF #b #V #T #HV #HT #HF destruct
elim (pl_sts_fwd_appl_dx … HM1) #r1 #r2 #r3 #Hr1 #_ #H destruct
elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT
- elim (pl_sts_inv_pl_sreds … HM1 ?) // #M0 #_ #H -M1 -Hr1 destruct
+ elim (pl_sts_inv_pl_sreds … HM1 …) // #M0 #_ #H -M1 -Hr1 destruct
>associative_append in Hs; #Hs
lapply (is_standard_fwd_append_dx … Hs) -r1
>associative_append #Hs
lapply (is_standard_inv_compatible_sn … H) -H #Hp
elim (pl_sts_fwd_dx_sn_appl_dx … HT) -HT #b0 #V0 #T0 #T1 #HV0 #_ #H -T1 -r2
elim (boolean_inv_appl … (sym_eq … H)) -H #B0 #A0 #_ #H #_ #_ -b0 -M0 -T0 destruct
- elim (IHB12 … HV0 ?) // -r3 -B0 -IHB12 #G2 #HG2 #H
+ elim (IHB12 … HV0 …) // -r3 -B0 -IHB12 #G2 #HG2 #H
@(ex2_intro … ({⊥}@G2.{⊥}⇕T)) normalize // /2 width=1/ (**) (* auto needs some help here *)
| #p #B #A1 #A2 #_ #IHA12 #F #HF #s #M1 #HM1 #Hs
elim (carrier_inv_appl … HF) -HF #b #V #T #HV #HT #HF destruct
elim (pl_sts_fwd_appl_dx … HM1) #r1 #r2 #r3 #Hr1 #Hr2 #H destruct
elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT
- elim (pl_sts_inv_pl_sreds … HM1 ?) // #M0 #_ #H -M1 -Hr1 destruct
+ elim (pl_sts_inv_pl_sreds … HM1 …) // #M0 #_ #H -M1 -Hr1 destruct
>associative_append in Hs; #Hs
lapply (is_standard_fwd_append_dx … Hs) -r1
>associative_append #Hs
lapply (is_whd_is_inner_inv … Hr2) -Hr2 // -H #H destruct
lapply (pl_sts_inv_nil … HT ?) -HT // #H
elim (boolean_inv_appl … H) -H #B0 #A0 #_ #_ #H #_ -M0 -B0 destruct
- elim (IHA12 … A0 ??) -IHA12 [3,5,6: // |2,4: skip ] (* simplify line *)
+ elim (IHA12 … A0 …) -IHA12 [3,5,6: // |2,4: skip ] (* simplify line *)
#F2 #HF2 #H
@(ex2_intro … ({b}@V.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *)
| <(map_cons_append … r2 (p::◊)) in Hs; #H
lapply (is_standard_inv_compatible_dx … H ?) -H /3 width=1/ -Hp #Hp
>append_nil in HT; #HT
- elim (pl_sts_inv_dx_appl_dx … HT ??) -HT [3: // |2: skip ] (* simplify line *)
+ elim (pl_sts_inv_dx_appl_dx … HT …) -HT [3: // |2: skip ] (* simplify line *)
#T0 #HT0 #H
elim (boolean_inv_appl … (sym_eq … H)) -H #B0 #A0 #_ #_ #H #_ -M0 -B0 destruct
- elim (IHA12 … HT0 ?) // -r2 -A0 -IHA12 #F2 #HF2 #H
+ elim (IHA12 … HT0 …) // -r2 -A0 -IHA12 #F2 #HF2 #H
@(ex2_intro … ({b}@V.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *)
]
| -IHA12 -Hr2 -M0 * #q #r #H destruct
lapply (is_standard_fwd_append_dx … Hs) -r2 #Hs
lapply (is_standard_fwd_sle … Hs) -r #H
- elim (sle_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+ elim (sle_inv_sn … H …) -H [3: // |2: skip ] (**) (* simplify line *)
#q0 #_ #H destruct
]
]
#p #s #M #M2 #_ #HM2 #IHM1 #Hsp
lapply (is_standard_fwd_append_sn … Hsp) #Hs
elim (IHM1 Hs) -IHM1 -Hs #F #HM1 #H
-elim (pl_sred_is_standard_pl_st … HM2 … HM1 ?) -HM2 // -M -Hsp #F2 #HF2 #HFM2
+elim (pl_sred_is_standard_pl_st … HM2 … HM1 …) -HM2 // -M -Hsp #F2 #HF2 #HFM2
lapply (pl_sts_step_dx … HM1 … HF2) -F
#H @(ex2_intro … F2) // (**) (* auto needs some help here *)
qed-.
∃∃M2. M1 ↦[p] M2 & {⊤}⇑M2 = F2.
#p @(in_whd_ind … p) -p
[ #M1 #F2 #H
- elim (pl_st_inv_nil … H ?) -H // #V #T #HM1 #H
+ elim (pl_st_inv_nil … H …) -H // #V #T #HM1 #H
elim (boolean_inv_appl … (sym_eq … HM1)) -HM1 #B #N #_ #HB #HN #HM1
elim (boolean_inv_abst … HN) -HN #A #_ #HA #HN destruct /2 width=3/
| #p #_ #IHp #M1 #F2 #H
- elim (pl_st_inv_dx … H ??) -H [3: // |2:skip ] #b #V #T1 #T2 #HT12 #HM1 #H (**) (* simplify line *)
+ elim (pl_st_inv_dx … H …) -H [3: // |2:skip ] #b #V #T1 #T2 #HT12 #HM1 #H (**) (* simplify line *)
elim (boolean_inv_appl … (sym_eq … HM1)) -HM1 #B #A #Hb #HB #HA #HM1 destruct
elim (IHp … HT12) -IHp -HT12 #C #HAC #H destruct
@(ex2_intro … (@B.C)) // /2 width=1/ (**) (* auto needs some help here *)
theorem pl_st_mono: ∀p. singlevalued … (pl_st p).
#p #F #G1 #H elim H -p -F -G1
-[ #V #T #G2 #H elim (pl_st_inv_nil … H ?) -H //
+[ #V #T #G2 #H elim (pl_st_inv_nil … H …) -H //
#W #U #H #HG2 destruct //
-| #b #p #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_rc … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+| #b #p #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_rc … H …) -H [3: // |2: skip ] (**) (* simplify line *)
#c #U1 #U2 #HU12 #H #HG2 destruct /3 width=1/
-| #b #p #V1 #V2 #T #_ #IHV12 #G2 #H elim (pl_st_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+| #b #p #V1 #V2 #T #_ #IHV12 #G2 #H elim (pl_st_inv_sn … H …) -H [3: // |2: skip ] (**) (* simplify line *)
#c #W1 #W2 #U #HW12 #H #HG2 destruct /3 width=1/
-| #b #p #V #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+| #b #p #V #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_dx … H …) -H [3: // |2: skip ] (**) (* simplify line *)
#c #W #U1 #U2 #HU12 #H #HG2 destruct /3 width=1/
]
qed-.
theorem pl_st_fwd_sle: ∀p1,F1,F. F1 Ⓡ↦[p1] F →
∀p2,F2. F Ⓡ↦[p2] F2 → p1 ≤ p2.
#p1 #F1 #F #H elim H -p1 -F1 -F //
-[ #b #p #T1 #T #_ #IHT1 #p2 #F2 #H elim (pl_st_inv_abst … H ???) -H [3: // |2,4: skip ] (**) (* simplify line *)
+[ #b #p #T1 #T #_ #IHT1 #p2 #F2 #H elim (pl_st_inv_abst … H …) -H [3: // |2,4: skip ] (**) (* simplify line *)
#q #T2 #HT2 #H1 #H2 destruct /3 width=2/
-| #b #p #V1 #V #T #_ #IHV1 #p2 #F2 #H elim (pl_st_inv_appl … H ????) -H [7: // |2,3,4: skip ] * (**) (* simplify line *)
+| #b #p #V1 #V #T #_ #IHV1 #p2 #F2 #H elim (pl_st_inv_appl … H …) -H [7: // |2,3,4: skip ] * (**) (* simplify line *)
[ #U #H destruct
| #q #V2 #H1 #HV2 #H2 destruct /3 width=2/
- | #q #U #_ #H elim (pl_st_inv_empty … H ??) [ // | skip ] (**) (* simplify line *)
+ | #q #U #_ #H elim (pl_st_inv_empty … H …) [ // | skip ] (**) (* simplify line *)
]
-| #b #p #V #T1 #T #HT1 #IHT1 #p2 #F2 #H elim (pl_st_inv_appl … H ????) -H [7: // |2,3,4: skip ] * (**) (* simplify line *)
+| #b #p #V #T1 #T #HT1 #IHT1 #p2 #F2 #H elim (pl_st_inv_appl … H …) -H [7: // |2,3,4: skip ] * (**) (* simplify line *)
[ #U #_ #H1 #H2 #_ -b -V -F2 -IHT1
elim (pl_st_fwd_abst … HT1 … H2) // -H1 * #q #H
elim (pl_st_inv_rc … HT1 … H) -HT1 -H #b #U1 #U2 #_ #_ #H -b -q -T1 -U1 destruct
(∀p. in_inner p → R p → R (dx::p)) →
∀p. in_inner p → R p.
#R #H1 #H2 #IH #p elim p -p
-[ #H elim (H ?) -H //
+[ #H elim (H …) -H //
| * #p #IHp // #H
lapply (in_inner_inv_dx … H) -H /3 width=1/
]
in_whd p ∨ ∃∃p0. p0 ≤ q0 & dx::p0 = p.
#p #q #H @(star_ind_l … p H) -p [ /3 width=3/ ]
#p0 #p #Hp0 #_ #IHpq #q1 #H destruct
-elim (IHpq ??) -IHpq [4: // |3: skip ] (**) (* simplify line *)
+elim (IHpq …) -IHpq [4: // |3: skip ] (**) (* simplify line *)
[ lapply (sprec_fwd_in_whd … Hp0) -Hp0 /3 width=1/
| * #p1 #Hpq1 #H elim (sprec_inv_dx … Hp0 … H) -p
[ #H destruct /2 width=1/
∃q0. sn::q0 = q.
#p #q #H elim H -q /3 width=3/
#q #q0 #_ #Hq0 #IHpq #p0 #H destruct
-elim (IHpq p0 ?) -IHpq // *
+elim (IHpq p0 …) -IHpq // *
[ #p1 #Hp01 #H
elim (sprec_inv_rc … Hq0 … H) -q * /3 width=3/ /4 width=3/
| #p1 #H elim (sprec_inv_sn … Hq0 … H) -q /3 width=2/
∃∃q0. p0 ≤ q0 & sn::q0 = q.
#p #q #H elim H -q /2 width=3/
#q #q0 #_ #Hq0 #IHpq #p0 #H destruct
-elim (IHpq p0 ?) -IHpq // #p1 #Hp01 #H
+elim (IHpq p0 …) -IHpq // #p1 #Hp01 #H
elim (sprec_inv_sn … Hq0 … H) -q /3 width=3/
qed-.
lemma is_standard_inv_compatible_sn: ∀s. is_standard (sn:::s) → is_standard s.
#s elim s -s // #a1 * // #a2 #s #IHs * #H
-elim (sle_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+elim (sle_inv_sn … H …) -H [3: // |2: skip ] (**) (* simplify line *)
#a #Ha1 #H destruct /3 width=1/
qed-.
lemma is_standard_inv_compatible_rc: ∀s. is_standard (rc:::s) → is_standard s.
#s elim s -s // #a1 * // #a2 #s #IHs * #H
-elim (sle_inv_rc … H ??) -H [4: // |2: skip ] * (**) (* simplify line *)
+elim (sle_inv_rc … H …) -H [4: // |2: skip ] * (**) (* simplify line *)
[ #a #Ha1 #H destruct /3 width=1/
| #a #H destruct
]
lemma is_standard_inv_compatible_dx: ∀s. is_standard (dx:::s) →
is_inner s → is_standard s.
#s elim s -s // #a1 * // #a2 #s #IHs * #H
-elim (sle_inv_dx … H ??) -H [4: // |3: skip ] (**) (* simplify line *)
+elim (sle_inv_dx … H …) -H [4: // |3: skip ] (**) (* simplify line *)
[ * #_ #H1a1 #_ * #H2a1 #_ -IHs
- elim (H2a1 ?) -H2a1 -a2 -s //
+ elim (H2a1 …) -H2a1 -a2 -s //
| * #a #Ha2 #H destruct #H * #_ /3 width=1/
qed-.
qed.
lemma is_whd_is_inner_inv: ∀s. is_whd s → is_inner s → ◊ = s.
-* // #p #s * #H1p #_ * #H2p #_ elim (H2p ?) -H2p //
+* // #p #s * #H1p #_ * #H2p #_ elim (H2p …) -H2p //
qed-.
lemma lstar_sdsubstable_f_dx: ∀S1,f,S2,R. (∀a. sdsubstable_f_dx S1 f (R a)) →
∀l. sdsubstable_f_dx S1 f (lstar S2 … R l).
#S1 #f #S2 #R #HR #l #G #F1 #F2 #H
-@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
+@(lstar_ind_l … l F1 H) -l -F1 // /3 width=3/
qed.
(*
definition sdsubstable_dx: predicate (relation subterms) ≝ λR.
lemma lstar_sdsubstable_dx: ∀S,R. (∀a. sdsubstable_dx (R a)) →
∀l. sdsubstable_dx (lstar S … R l).
#S #R #HR #l #G #F1 #F2 #H
-@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
+@(lstar_ind_l … l F1 H) -l -F1 // /3 width=3/
qed.
lemma star_sdsubstable: ∀R. reflexive ? R →
lemma lstar_sliftable: ∀S,R. (∀a. sliftable (R a)) →
∀l. sliftable (lstar S … R l).
#S #R #HR #l #h #F1 #F2 #H
-@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
+@(lstar_ind_l … l F1 H) -l -F1 // /3 width=3/
qed.
lemma lstar_sdeliftable_sn: ∀S,R. (∀a. sdeliftable_sn (R a)) →
∀l. sdeliftable_sn (lstar S … R l).
#S #R #HR #l #h #G1 #G2 #H
-@(lstar_ind_l ????????? H) -l -G1 /2 width=3/
+@(lstar_ind_l … l G1 H) -l -G1 /2 width=3/
#a #l #G1 #G #HG1 #_ #IHG2 #d #F1 #HFG1
elim (HR … HG1 … HFG1) -G1 #F #HF1 #HFG
elim (IHG2 … HFG) -G /3 width=3/
lemma l_sreds_fwd_mult: ∀S,R. (∀a,M,N. R a M N → M ↦ N) →
∀l,M1,M2. l_sreds S R l M1 M2 →
♯{M2} ≤ ♯{M1} ^ (2 ^ (|l|)).
-#S #R #HR #l #M1 #M2 #H @(lstar_ind_l ????????? H) -l -M1 normalize //
+#S #R #HR #l #M1 #M2 #H @(lstar_ind_l … l M1 H) -l -M1 normalize //
#a #l #M1 #M #HM1 #_ #IHM2
lapply (HR … HM1) -HR -a #HM1
lapply (sred_fwd_mult … HM1) #HM1
lemma pred_conf1_abst: ∀A. confluent1 … pred A → confluent1 … pred (𝛌.A).
#A #IH #M1 #H1 #M2 #H2
-elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #A1 #HA1 #H destruct (**) (* simplify line *)
-elim (pred_inv_abst … H2 ??) -H2 [3: // |2: skip ] #A2 #HA2 #H destruct (**) (* simplify line *)
+elim (pred_inv_abst … H1 …) -H1 [3: // |2: skip ] #A1 #HA1 #H destruct (**) (* simplify line *)
+elim (pred_inv_abst … H2 …) -H2 [3: // |2: skip ] #A2 #HA2 #H destruct (**) (* simplify line *)
elim (IH … HA1 … HA2) -A /3 width=3/
qed-.
B ⤇ B1 → B ⤇ B2 → 𝛌.C ⤇ M1 → C ⤇ C2 →
∃∃M. @B1.M1 ⤇ M & [↙B2]C2 ⤇ M.
#B #B1 #B2 #C #C2 #M1 #IH #HB1 #HB2 #H1 #HC2
-elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #C1 #HC1 #H destruct (**) (* simplify line *)
+elim (pred_inv_abst … H1 …) -H1 [3: // |2: skip ] #C1 #HC1 #H destruct (**) (* simplify line *)
elim (IH B … HB1 … HB2) -HB1 -HB2 //
elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/
qed-.
[ /2 width=3 by pred_conf1_vref/
| /3 width=4 by pred_conf1_abst/
| #B #A #H #M1 #H1 #M2 #H2 destruct
- elim (pred_inv_appl … H1 ???) -H1 [5: // |2,3: skip ] * (**) (* simplify line *)
- elim (pred_inv_appl … H2 ???) -H2 [5,10: // |2,3,7,8: skip ] * (**) (* simplify line *)
+ elim (pred_inv_appl … H1 …) -H1 [5: // |2,3: skip ] * (**) (* simplify line *)
+ elim (pred_inv_appl … H2 …) -H2 [5,10: // |2,3,7,8: skip ] * (**) (* simplify line *)
[ #B2 #A2 #HB2 #HA2 #H2 #B1 #A1 #HB1 #HA1 #H1 destruct
elim (IH A … HA1 … HA2) -HA1 -HA2 //
elim (IH B … HB1 … HB2) // -A -B /3 width=5/
lemma lstar_dsubstable_dx: ∀S,R. (∀a. dsubstable_dx (R a)) →
∀l. dsubstable_dx (lstar S … R l).
#S #R #HR #l #N #M1 #M2 #H
-@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
+@(lstar_ind_l … l M1 H) -l -M1 // /3 width=3/
qed.
lemma star_dsubstable: ∀R. reflexive ? R →
lemma lstar_liftable: ∀S,R. (∀a. liftable (R a)) →
∀l. liftable (lstar S … R l).
#S #R #HR #l #h #M1 #M2 #H
-@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
+@(lstar_ind_l … l M1 H) -l -M1 // /3 width=3/
qed.
lemma lstar_deliftable_sn: ∀S,R. (∀a. deliftable_sn (R a)) →
∀l. deliftable_sn (lstar S … R l).
#S #R #HR #l #h #N1 #N2 #H
-@(lstar_ind_l ????????? H) -l -N1 /2 width=3/
+@(lstar_ind_l … l N1 H) -l -N1 /2 width=3/
#a #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1
elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN
elim (IHN2 … HMN) -N /3 width=3/
qed.
theorem sreds_preds: ∀M1,M2. M1 ↦* M2 → M1 ⤇* M2.
-#M1 #M2 #H @(star_ind_l ??????? H) -M1 //
+#M1 #M2 #H @(star_ind_l … M1 H) -M1 //
#M1 #M #HM1 #_ #IHM2
@(preds_step_sn … IHM2) -M2 /2 width=2/
qed.
ctx in
let m, s, status, t =
GrafiteDisambiguate.disambiguate_nterm
- status None ctx menv subst (parsed_text,parsed_text_length,
+ status `XTNone ctx menv subst (parsed_text,parsed_text_length,
NotationPt.Cast (t,NotationPt.Implicit `JustOne))
(* XXX use the metasenv, if possible *)
in
projects / helm.git / commitdiff