aux 1 context
let interpretate_term_and_interpretate_term_option (status: #NCic.status)
- ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~uri ~is_path
+ ~create_dummy_ids ~obj_context ~mk_choice ~env ~uri ~is_path
~localization_tbl
=
(* create_dummy_ids shouldbe used only for interpretating patterns *)
"branch pattern must be \"_\"")))
) branches in
let indtype_ref =
- NReference.reference_of_string "cic:/fake_indty.ind(0,0,0)"
+ let uri = NUri.uri_of_string "cic:/matita/dummy/indty.ind" in
+ NRef.reference_of_spec uri (NRef.Ind (true,1,1))
in
NCic.Match (indtype_ref, cic_outtype, cic_term,
(List.map do_branch branches))
| Some (indty_ident, _) ->
(match Disambiguate.resolve ~env ~mk_choice
(DT.Id indty_ident) (`Args []) with
- | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
+ | NCic.Const (NRef.Ref (_,NRef.Ind _) as r) -> r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
(lazy "The type of the term to be matched is still unknown"))
*)
(match Disambiguate.resolve ~env ~mk_choice
(DT.Id (fst_constructor branches)) (`Args []) with
- | NCic.Const (NReference.Ref (_,NReference.Con _) as r) ->
+ | NCic.Const (NRef.Ref (_,NRef.Con _) as r) ->
let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in
- NReference.mk_indty b r
+ NRef.mk_indty b r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
(lazy "The type of the term to be matched is still unknown"))
in
let cic_body = aux ~localize loc (cic_name :: context) body in
NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
- | NotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
| NotationPt.Ident _
| NotationPt.Uri _
| NotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
| NotationPt.Uri (uri, subst) ->
assert (subst = None);
(try
- NCic.Const (NReference.reference_of_string uri)
+ NCic.Const (NRef.reference_of_string uri)
with NRef.IllFormedReference _ ->
NotationPt.fail loc "Ill formed reference")
| NotationPt.NRef nref -> NCic.Const nref
| None,_ ->
NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
| Some bo,_ ->
- (match bo with
- | NotationPt.LetRec (kind, defs, _) ->
- let inductive = kind = `Inductive in
- let _,obj_context =
- List.fold_left
- (fun (i,acc) (_,(name,_),_,k) ->
- (i+1,
- (ncic_name_of_ident name, NReference.reference_of_spec uri
- (if inductive then NReference.Fix (i,k,0)
- else NReference.CoFix i)) :: acc))
- (0,[]) defs
- in
- let inductiveFuns =
- List.map
- (fun (params, (name, typ), body, decr_idx) ->
- let add_binders kind t =
- List.fold_right
- (fun var t ->
- NotationPt.Binder (kind, var, t)) params t
- in
- let cic_body =
- interpretate_term status
- ~obj_context ~context ~env ~uri:None ~is_path:false
- (add_binders `Lambda body)
- in
- let cic_type =
- interpretate_term_option status
- ~obj_context:[]
- ~context ~env ~uri:None ~is_path:false `Type
- (HExtlib.map_option (add_binders `Pi) typ)
- in
- ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
- defs
- in
- NCic.Fixpoint (inductive,inductiveFuns,attrs)
- | bo ->
- let bo =
- interpretate_term status
- ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
- in
- NCic.Constant ([],name,Some bo,ty',attrs)))
- | NotationPt.Inductive (params,tyl) ->
+ let bo =
+ interpretate_term status
+ ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
+ in
+ NCic.Constant ([],name,Some bo,ty',attrs))
+ | NotationPt.Inductive (params,tyl,source) ->
let context,params =
let context,res =
List.fold_left
List.fold_left
(fun (i,res) (name,_,_,_) ->
let nref =
- NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno))
+ NRef.reference_of_spec uri (NRef.Ind (inductive,i,leftno))
in
i+1,(name,nref)::res)
(0,[]) tyl) in
) tyl
in
let height = (* XXX calculate *) 0 in
- let attrs = `Provided, `Regular in
+ let attrs = source, `Regular in
uri, height, [], [],
NCic.Inductive (inductive,leftno,tyl,attrs)
- | NotationPt.Record (params,name,ty,fields) ->
+ | NotationPt.Record (params,name,ty,fields,source) ->
let context,params =
let context,res =
List.fold_left
(interpretate_term status ~obj_context:[] ~context ~env ~uri:None
~is_path:false ty) in
let nref =
- NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
+ NRef.reference_of_spec uri (NRef.Ind (true,0,leftno)) in
let obj_context = [name,nref] in
let fields' =
snd (
let tyl = [relevance,name,ty',[relevance,"mk_" ^ name,con']] in
let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
let height = (* XXX calculate *) 0 in
- let attrs = `Provided, `Record field_names in
+ let attrs = source, `Record field_names in
uri, height, [], [],
NCic.Inductive (true,leftno,tyl,attrs)
+ | NotationPt.LetRec (kind, defs, attrs) ->
+ let inductive = kind = `Inductive in
+ let _,obj_context =
+ List.fold_left
+ (fun (i,acc) (_,(name,_),_,k) ->
+ (i+1,
+ (ncic_name_of_ident name, NRef.reference_of_spec uri
+ (if inductive then NRef.Fix (i,k,0)
+ else NRef.CoFix i)) :: acc))
+ (0,[]) defs
+ in
+ let inductiveFuns =
+ List.map
+ (fun (params, (name, typ), body, decr_idx) ->
+ let add_binders kind t =
+ List.fold_right
+ (fun var t ->
+ NotationPt.Binder (kind, var, t)) params t
+ in
+ let cic_body =
+ interpretate_term status
+ ~obj_context ~context ~env ~uri:None ~is_path:false
+ (add_binders `Lambda body)
+ in
+ let cic_type =
+ interpretate_term_option status
+ ~obj_context:[]
+ ~context ~env ~uri:None ~is_path:false `Type
+ (HExtlib.map_option (add_binders `Pi) typ)
+ in
+ ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
+ defs
+ in
+ let height = (* XXX calculate *) 0 in
+ uri, height, [], [],
+ NCic.Fixpoint (inductive,inductiveFuns,attrs)
;;
let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst
projects / helm.git / blobdiff