in
HLog.debug debug; assert false
-(*
-let cic_codomain_of_uri uri =
- (UriManager.string_of_uri uri,
- let term =
- try
- CicUtil.term_of_uri uri
- with exn ->
- assert false
- in
- fun _ _ _ -> term)
-;;
-*)
-
-(*let cic_num_choices = DisambiguateChoices.lookup_num_choices;;*)
-
let __Implicit = "__Implicit__"
let __Closed_Implicit = "__Closed_Implicit__"
(fun l->assert(l = []);CicUtil.term_of_uri (UriManager.uri_of_string uri))
;;
-let cic_mk_implicit b =
+let ncic_mk_choice = function
+ | LexiconAst.Symbol_alias (name, _, dsc) ->
+ if name = __Implicit then
+ dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
+ else if name = __Closed_Implicit then
+ dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
+ else
+ DisambiguateChoices.lookup_symbol_by_dsc
+ ~mk_implicit:(function
+ | true -> NCic.Implicit `Closed
+ | false -> NCic.Implicit `Term)
+ ~mk_appl:(function
+ (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
+ ~term_of_uri:(fun uri ->
+ fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+ name dsc
+ | LexiconAst.Number_alias (_, dsc) ->
+ let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in
+ desc, `Num_interp
+ (fun num ->
+ fst (OCic2NCic.convert_term
+ (UriManager.uri_of_string "cic:/xxx/x.con")
+ (match f with `Num_interp f -> f num | _ -> assert false)))
+ | LexiconAst.Ident_alias (name, uri) ->
+ uri, `Sym_interp
+ (fun l->assert(l = []);
+ let uri = UriManager.uri_of_string uri in
+ fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+;;
+
+
+let mk_implicit b =
match b with
| false ->
LexiconAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
LexiconAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
;;
-let ncic_codomain_of_uri uri =
- (UriManager.string_of_uri uri,
- let term =
- try
- fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri))
- with exn ->
- assert false
- in
- fun _ _ _ -> term)
-;;
-
-let ncic_num_choices _ = (*assert false*) [];;
-let ncic_mk_choice =
- DisambiguateChoices.mk_choice
- ~mk_implicit:(function
- | true -> NCic.Implicit `Closed
- | false -> NCic.Implicit `Term)
- ~mk_appl:(function (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
- ~term_of_uri:(fun uri ->
- fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
-;;
-
let lookup_in_library
interactive_user_uri_choice input_or_locate_uri item
=
?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
~lookup_in_library
~mk_choice:cic_mk_choice
- ~mk_implicit:cic_mk_implicit
+ ~mk_implicit
~description_of_alias:LexiconAst.description_of_alias
~context ~metasenv ~subst:[] (text,prefix_len,term))
in
(CicDisambiguate.disambiguate_term
~lookup_in_library
~mk_choice:cic_mk_choice
- ~mk_implicit:cic_mk_implicit
+ ~mk_implicit
~description_of_alias:LexiconAst.description_of_alias
~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
| None -> raise BaseUriNotSetYet)
| CicNotationPt.Inductive _ -> assert false
| CicNotationPt.Theorem _ -> None in
-(*
+ (*
(match obj with
CicNotationPt.Theorem (_,_,ty,_) ->
(try
(match
NCicDisambiguate.disambiguate_term
- ~lookup_in_library:(lookup_in_library ncic_codomain_of_uri
- ncic_mk_choice ncic_num_choices)
+ ~lookup_in_library:lookup_in_library
+ ~description_of_alias:LexiconAst.description_of_alias
+ ~mk_choice:ncic_mk_choice
+ ~mk_implicit
~context:[] ~metasenv:[] ~subst:[]
- ~aliases:DisambiguateTypes.Environment.empty
- ~universe:(Some DisambiguateTypes.Environment.empty)
+ ~aliases:lexicon_status.LexiconEngine.aliases
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
(text,prefix_len,ty)
with
| [_,metasenv,subst,ty],_ ->
)
| _ -> ()
);
-*)
+ *)
let (diff, metasenv, _, cic, _) =
singleton "third"
(CicDisambiguate.disambiguate_obj
~lookup_in_library
~mk_choice:cic_mk_choice
- ~mk_implicit:cic_mk_implicit
+ ~mk_implicit
~description_of_alias:LexiconAst.description_of_alias
~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri
try
let localise t =
try NCicUntrusted.NCicHash.find localization_tbl t
- with Not_found -> assert false
+ with Not_found ->
+ prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
+ assert false
in
let metasenv, subst, term, _ =
NCicRefiner.typeof metasenv subst context term None ~localise
let interpretate_term
?(create_dummy_ids=false) ~mk_choice ~context ~env ~uri ~is_path ast
- ~localization_tbl
+ ~localization_tbl
=
(* create_dummy_ids shouldbe used only for interpretating patterns *)
assert (uri = None);
let rec aux ~localize loc context = function
+ t ->
+ let res =
+ match t with
| CicNotationPt.AttributedTerm (`Loc loc, term) ->
let res = aux ~localize loc context term in
if localize then NCicUntrusted.NCicHash.add localization_tbl res loc;
| Some (indty_ident, _) ->
(match Disambiguate.resolve ~env ~mk_choice
(Id indty_ident) (`Args []) with
- | NCic.Const r -> r
+ | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
(lazy "The type of the term to be matched is still unknown"))
- | _ ->
+ | t ->
raise (DisambiguateTypes.Invalid_choice
(lazy (loc,"The type of the term to be matched "^
- "is not (co)inductive!"))))
+ "is not (co)inductive: " ^ NCicPp.ppterm
+ ~metasenv:[] ~subst:[] ~context:[] t))))
| None ->
let rec fst_constructor =
function
"because it is an inductive type without constructors "^
"or because all patterns use wildcards")))
in
- (match Disambiguate.resolve ~env ~mk_choice
+(*
+ DisambiguateTypes.Environment.iter
+ (fun k v ->
+ prerr_endline
+ (DisambiguateTypes.string_of_domain_item k ^ " => " ^
+ description_of_alias v)) env;
+*)
+ (match Disambiguate.resolve ~env ~mk_choice
(Id (fst_constructor branches)) (`Args []) with
- | NCic.Const r -> r
+ | NCic.Const (NReference.Ref (_,NReference.Con _) as r) ->
+ let b,_,_,_,_ = NCicEnvironment.get_checked_indtys r in
+ NReference.mk_indty b r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
(lazy "The type of the term to be matched is still unknown"))
- | _ ->
+ | t ->
raise (DisambiguateTypes.Invalid_choice
(lazy (loc,
- "The type of the term to be matched is not (co)inductive!"))))
+ "The type of the term to be matched is not (co)inductive: "
+ ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t))))
in
let _,leftsno,itl,_,indtyp_no =
NCicEnvironment.get_checked_indtys indtype_ref in
| Some t -> aux ~localize loc context t
in
let cic_body = aux ~localize loc (cic_name :: context) body in
- NCic.LetIn (cic_name, cic_def, cic_typ, cic_body)
+ NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
| CicNotationPt.LetRec (_kind, _defs, _body) ->
assert false (*
let context' =
in
NCic.Meta (index, (0, NCic.Ctx cic_subst))
| CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
- | CicNotationPt.Sort `Set -> assert false
+ | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type
+ [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
| CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
[false,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
| CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
Disambiguate.resolve ~env ~mk_choice
(Symbol (symbol, instance)) (`Args [])
| _ -> assert false (* god bless Bologna *)
+
+ in
+ prerr_endline (NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[]
+ res);
+ res
and aux_option ~localize loc context annotation = function
| None -> NCic.Implicit annotation
| Some (CicNotationPt.AttributedTerm (`Loc loc, term)) ->
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
;;
+let _ =
+let mk_type n =
+ if n = 0 then
+ [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+ else
+ [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+in
+let mk_cprop n =
+ if n = 0 then
+ [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+ else
+ [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+in
+ NCicEnvironment.add_constraint true (mk_type 0) (mk_type 1);
+ NCicEnvironment.add_constraint true (mk_cprop 0) (mk_cprop 1);
+ NCicEnvironment.add_constraint true (mk_cprop 0) (mk_type 1);
+ NCicEnvironment.add_constraint true (mk_type 0) (mk_cprop 1);
+ NCicEnvironment.add_constraint false (mk_cprop 0) (mk_type 0);
+ NCicEnvironment.add_constraint false (mk_type 0) (mk_cprop 0);
+;;
+
F.fprintf f "@; @[<v>[ ";
if pl <> [] then
begin
- F.fprintf f "@[<hov 2>%s ⇒@;" (r2s inside_fix (R.mk_constructor 1 r));
+ F.fprintf f "@[<hov 2>%s ⇒@;"
+ (try r2s inside_fix (R.mk_constructor 1 r)
+ with R.IllFormedReference _ -> "#ERROR#");
aux ~toplevel:true ctx (List.hd pl);
F.fprintf f "@]";
ignore(List.fold_left
(fun i t ->
- F.fprintf f "@;| @[<hov 2>%s ⇒@;" (r2s inside_fix (R.mk_constructor i r));
+ F.fprintf f "@;| @[<hov 2>%s ⇒@;"
+ (try r2s inside_fix (R.mk_constructor i r)
+ with R.IllFormedReference _ -> "#ERROR#");
aux ~toplevel:true ctx t;
F.fprintf f "@]";
i+1)
let mk_constructor j = function
| Ref (u, Ind (_,i,l)) ->
reference_of_string (string_of_reference (Ref (u, Con (i,j,l))))
- | _ -> assert false
+ | r ->
+ raise (IllFormedReference (lazy ("NON INDUCTIVE TYPE REFERENCE: " ^
+ string_of_reference r)));
+;;
+let mk_indty b = function
+ | Ref (u, Con (i,_,l)) ->
+ reference_of_string (string_of_reference (Ref (u, Ind (b,i,l))))
+ | r ->
+ raise (IllFormedReference (lazy
+ ("NON INDUCTIVE TYPE CONSTRUCTOR REFERENCE: " ^ string_of_reference r)));
;;
let mk_fix i j = function
(* given the reference of an inductive type, returns the i-th contructor *)
val mk_constructor: int -> reference -> reference
+(* given the reference of an inductive type constructor, returns the indty *)
+val mk_indty: bool -> reference -> reference
val mk_fix: int -> int -> reference -> reference
val mk_cofix: int -> reference -> reference
| _ -> assert false
;;
-let force_to_sort metasenv subst context t =
+let force_to_sort metasenv subst context orig localise t =
match NCicReduction.whd ~subst context t with
| C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as t ->
metasenv, subst, t
in
metasenv, subst, C.Meta (newmeta,(0,C.Irl 0))
| C.Sort _ as t -> metasenv, subst, t
- | _ -> assert false
+ | t ->
+ raise (RefineFailure (lazy
+ (localise orig,
+ "Not a sort: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context t)))
;;
let sort_of_prod
localise metasenv subst context orig_s orig_t (name,s) t (t1, t2)
=
- let metasenv, subst, t1 = force_to_sort metasenv subst context t1 in
+ let metasenv, subst, t1 =
+ force_to_sort metasenv subst context orig_s localise t1 in
let metasenv, subst, t2 =
- force_to_sort metasenv subst ((name,C.Decl s)::context) t2 in
+ force_to_sort metasenv subst ((name,C.Decl s)::context)
+ orig_t localise t2 in
match t1, t2 with
| C.Sort _, C.Sort C.Prop -> metasenv, subst, t2
| C.Sort (C.Type u1), C.Sort (C.Type u2) ->
in
let metasenv, subst, s, ty_s =
typeof_aux metasenv subst context None s in
- let metasenv, subst, _ = force_to_sort metasenv subst context ty_s in
+ let metasenv, subst, _ =
+ force_to_sort metasenv subst context orig_s localise ty_s in
let (metasenv,subst), exp_ty_t =
match exp_s with
| Some exp_s ->
typeof_aux metasenv subst context exp_ty_t t
in
metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t)
- | C.LetIn (n,ty,t,bo) ->
+ | C.LetIn (n,(ty as orig_ty),t,bo) ->
let metasenv, subst, ty, ty_ty =
typeof_aux metasenv subst context None ty in
- let metasenv, subst, _ = force_to_sort metasenv subst context ty_ty in
+ let metasenv, subst, _ =
+ force_to_sort metasenv subst context orig_ty localise ty_ty in
let metasenv, subst, t, _ =
typeof_aux metasenv subst context (Some ty) t in
let context1 = (n, C.Def (t,ty)) :: context in
projects / helm.git / commitdiff