let cic_name_of_name = function
| Ast.Ident (n, None) -> n
let cic_name_of_name = function
| Ast.Ident (n, None) -> n
status#ppterm ~metasenv ~subst ~context term)) ;
Disambiguate.Uncertain loc_msg
| NCicRefiner.RefineFailure loc_msg ->
status#ppterm ~metasenv ~subst ~context term)) ;
Disambiguate.Uncertain loc_msg
| NCicRefiner.RefineFailure loc_msg ->
NCicUntrusted.NCicHash.add localization_tbl res loc;
res
| NotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
NCicUntrusted.NCicHash.add localization_tbl res loc;
res
| NotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
- (NotationPt.AttributedTerm (att,NotationPt.Appl (inner @ args)))
+ (NotationPt.AttributedTerm (att,NotationPt.Appl (inner :: args)))
+ | NotationPt.Appl (NotationPt.Appl inner :: args) ->
+ 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
| NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) ->
let cic_args = List.map (aux ~localize loc context) args in
| NotationPt.Appl terms ->
NCic.Appl (List.map (aux ~localize loc context) terms)
| NotationPt.Binder (binder_kind, (var, typ), body) ->
| NotationPt.Appl terms ->
NCic.Appl (List.map (aux ~localize loc context) terms)
| NotationPt.Binder (binder_kind, (var, typ), body) ->
(`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
(`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
raise (DisambiguateTypes.Invalid_choice
(lazy (loc, "Syntax error: the left hand side of a "^
"branch pattern must be \"_\"")))
raise (DisambiguateTypes.Invalid_choice
(lazy (loc, "Syntax error: the left hand side of a "^
"branch pattern must be \"_\"")))
- (*
- NCic.MutCase (ref, cic_outtype, cic_term,
- (List.map do_branch branches))
- *) ignore branches; assert false (* patterns not implemented yet *)
+ NCic.Match (indtype_ref, cic_outtype, cic_term,
+ (List.map do_branch branches))
else
let indtype_ref =
match indty_ident with
| Some (indty_ident, _) ->
(match Disambiguate.resolve ~env ~mk_choice
else
let indtype_ref =
match indty_ident with
| Some (indty_ident, _) ->
(match Disambiguate.resolve ~env ~mk_choice
| NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
| 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
function
(Ast.Pattern (head, _, _), _) :: _ -> head
| (Ast.Wildcard, _) :: tl -> fst_constructor tl
"of the term to be matched cannot be determined "^
"because it is an inductive type without constructors "^
"or because all patterns use wildcards")))
"of the term to be matched cannot be determined "^
"because it is an inductive type without constructors "^
"or because all patterns use wildcards")))
| NCic.Const (NReference.Ref (_,NReference.Con _) as r) ->
let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in
NReference.mk_indty b r
| NCic.Const (NReference.Ref (_,NReference.Con _) as r) ->
let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in
NReference.mk_indty b r
| NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
| NotationPt.UserInput -> NCic.Implicit `Hole
| NotationPt.Num (num, i) ->
| NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
| NotationPt.UserInput -> NCic.Implicit `Hole
| NotationPt.Num (num, i) ->
[`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
| NotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~env ~mk_choice
[`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
| NotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~env ~mk_choice
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
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
NCic.Constant ([],name,None,ty',attrs)
| Some _,`Axiom -> assert false
| None,_ ->
NCic.Constant ([],name,None,ty',attrs)
| Some _,`Axiom -> assert false
| None,_ ->
NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
| Some bo,_ ->
(match bo with
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
([],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.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 context,params =
NCic.Constant ([],name,Some bo,ty',attrs)))
| NotationPt.Inductive (params,tyl) ->
let context,params =
in
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
;;
in
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
;;