(* $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
"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))
match indty_ident with
| Some (indty_ident, _) ->
(match Disambiguate.resolve ~env ~mk_choice
- (Id indty_ident) (`Args []) with
- | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
+ (DT.Id indty_ident) (`Args []) with
+ | 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"))
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
- | NCic.Const (NReference.Ref (_,NReference.Con _) as r) ->
+ (DT.Id (fst_constructor branches)) (`Args []) with
+ | 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
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
- 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
| 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
- | 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
- 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 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
~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
;;