open Printf
open DisambiguateTypes
-open UriManager
module Ast = NotationPt
module NRef = NReference
-let debug_print s = prerr_endline (Lazy.force s);;
-let debug_print _ = ();;
-
-let reference_of_oxuri = ref (fun _ -> assert false);;
-let set_reference_of_oxuri f = reference_of_oxuri := f;;
+let debug = ref false;;
+let debug_print s = if !debug then prerr_endline (Lazy.force s);;
let cic_name_of_name = function
| Ast.Ident (n, None) -> n
| _ -> (NCic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
;;
-let refine_term
- metasenv subst context uri ~rdb ~use_coercions term expty _ ~localization_tbl=
+let refine_term (status: #NCicCoercion.status) metasenv subst context uri ~use_coercions term expty _
+ ~localization_tbl
+=
assert (uri=None);
debug_print (lazy (sprintf "TEST_INTERPRETATION: %s"
- (NCicPp.ppterm ~metasenv ~subst ~context term)));
+ (status#ppterm ~metasenv ~subst ~context term)));
try
let localise t =
try NCicUntrusted.NCicHash.find localization_tbl t
with Not_found ->
- prerr_endline ("NOT LOCALISED" ^ NCicPp.ppterm ~metasenv ~subst ~context t);
+ prerr_endline ("NOT LOCALISED" ^ status#ppterm ~metasenv ~subst ~context t);
(*assert false*) HExtlib.dummy_floc
in
let metasenv, subst, term, _ =
NCicRefiner.typeof
- (rdb#set_coerc_db
- (if use_coercions then rdb#coerc_db else NCicCoercion.empty_db))
+ (status#set_coerc_db
+ (if use_coercions then status#coerc_db else NCicCoercion.empty_db))
metasenv subst context term expty ~localise
in
Disambiguate.Ok (term, metasenv, subst, ())
with
| NCicRefiner.Uncertain loc_msg ->
debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force loc_msg) ^ "] " ^
- NCicPp.ppterm ~metasenv ~subst ~context term)) ;
+ status#ppterm ~metasenv ~subst ~context term)) ;
Disambiguate.Uncertain loc_msg
| NCicRefiner.RefineFailure loc_msg ->
debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s"
- (NCicPp.ppterm ~metasenv ~subst ~context term) (snd(Lazy.force loc_msg))));
+ (status#ppterm ~metasenv ~subst ~context term) (snd(Lazy.force loc_msg))));
Disambiguate.Ko loc_msg
;;
-let refine_obj
- ~rdb metasenv subst _context _uri
- ~use_coercions obj _ _ugraph ~localization_tbl
+let refine_obj status metasenv subst _context _uri ~use_coercions obj _ _ugraph
+ ~localization_tbl
=
+ (*prerr_endline ((sprintf "TEST_INTERPRETATION: %s" (status#ppobj obj)));*)
assert (metasenv=[]);
assert (subst=[]);
let localise t =
try
let obj =
NCicRefiner.typeof_obj
- (rdb#set_coerc_db
- (if use_coercions then rdb#coerc_db
+ (status#set_coerc_db
+ (if use_coercions then status#coerc_db
else NCicCoercion.empty_db))
obj ~localise
in
with
| NCicRefiner.Uncertain loc_msg ->
debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force loc_msg) ^ "] " ^
- NCicPp.ppobj obj)) ;
+ status#ppobj obj)) ;
Disambiguate.Uncertain loc_msg
| NCicRefiner.RefineFailure loc_msg ->
debug_print (lazy (sprintf "PRUNED:\nobj: %s\nmessage: %s"
- (NCicPp.ppobj obj) (snd(Lazy.force loc_msg))));
+ (status#ppobj obj) (snd(Lazy.force loc_msg))));
Disambiguate.Ko loc_msg
;;
in
aux 1 context
-let interpretate_term_and_interpretate_term_option
- ?(create_dummy_ids=false)
- ~obj_context ~mk_choice ~env ~uri ~is_path ~localization_tbl
+let interpretate_term_and_interpretate_term_option (status: #NCic.status)
+ ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~uri ~is_path
+ ~localization_tbl
=
(* create_dummy_ids shouldbe used only for interpretating patterns *)
assert (uri = None);
NCicUntrusted.NCicHash.add localization_tbl res loc;
res
| NotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
- | NotationPt.Appl (NotationPt.Appl inner :: args) ->
- aux ~localize loc context (NotationPt.Appl (inner @ args))
| NotationPt.Appl
- (NotationPt.AttributedTerm (att,(NotationPt.Appl inner))::args)->
+ (NotationPt.AttributedTerm (att, inner)::args)->
aux ~localize loc context
- (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
Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)
raise (DisambiguateTypes.Invalid_choice
(lazy (loc, "Syntax error: the left hand side of a "^
"branch pattern must be \"_\"")))
- ) branches
+ ) branches in
+ let indtype_ref =
+ NReference.reference_of_string "cic:/fake_indty.ind(0,0,0)"
in
- (*
- 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
| t ->
raise (DisambiguateTypes.Invalid_choice
(lazy (loc,"The type of the term to be matched "^
- "is not (co)inductive: " ^ NCicPp.ppterm
+ "is not (co)inductive: " ^ status#ppterm
~metasenv:[] ~subst:[] ~context:[] t))))
| None ->
let rec fst_constructor =
(match Disambiguate.resolve ~env ~mk_choice
(Id (fst_constructor branches)) (`Args []) with
| NCic.Const (NReference.Ref (_,NReference.Con _) as r) ->
- let b,_,_,_,_ = NCicEnvironment.get_checked_indtys r in
+ let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in
NReference.mk_indty b r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
raise (DisambiguateTypes.Invalid_choice
(lazy (loc,
"The type of the term to be matched is not (co)inductive: "
- ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t))))
+ ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] t))))
in
let _,leftsno,itl,_,indtyp_no =
- NCicEnvironment.get_checked_indtys indtype_ref in
+ NCicEnvironment.get_checked_indtys status indtype_ref in
let _,_,_,cl =
try
List.nth itl indtyp_no
with _ -> assert false in
let rec count_prod t =
- match NCicReduction.whd ~subst:[] [] t with
+ match NCicReduction.whd status ~subst:[] [] t with
NCic.Prod (_, _, t) -> 1 + (count_prod t)
| _ -> 0
in
| NotationPt.Uri (uri, subst) ->
assert (subst = None);
(try
- NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri))
+ NCic.Const (NReference.reference_of_string uri)
with NRef.IllFormedReference _ ->
NotationPt.fail loc "Ill formed reference")
| NotationPt.NRef nref -> NCic.Const nref
- | NotationPt.NCic t ->
- let context = (* to make metas_of_term happy *)
- List.map (fun x -> x,NCic.Decl (NCic.Implicit `Type)) context in
- assert(NCicUntrusted.metas_of_term [] context t = []); t
+ | NotationPt.NCic t -> t
| NotationPt.Implicit `Vector -> NCic.Implicit `Vector
| NotationPt.Implicit `JustOne -> NCic.Implicit `Term
| NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
(fun ~context -> aux_option ~localize:true HExtlib.dummy_floc context)
;;
-let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
- ~obj_context ~localization_tbl ~mk_choice
+let interpretate_term status ?(create_dummy_ids=false) ~context ~env ~uri
+ ~is_path ast ~obj_context ~localization_tbl ~mk_choice
=
let context = List.map fst context in
fst
- (interpretate_term_and_interpretate_term_option
- ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path ~localization_tbl)
+ (interpretate_term_and_interpretate_term_option status
+ ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path
+ ~localization_tbl)
~context ast
;;
-let interpretate_term_option
- ?(create_dummy_ids=false) ~context ~env ~uri ~is_path
- ~localization_tbl ~mk_choice ~obj_context
+let interpretate_term_option status ?(create_dummy_ids=false) ~context ~env ~uri
+ ~is_path ~localization_tbl ~mk_choice ~obj_context
=
let context = List.map fst context in
snd
- (interpretate_term_and_interpretate_term_option
- ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path ~localization_tbl)
+ (interpretate_term_and_interpretate_term_option status
+ ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path
+ ~localization_tbl)
~context
;;
-let disambiguate_path path =
+let disambiguate_path status path =
let localization_tbl = NCicUntrusted.NCicHash.create 23 in
fst
- (interpretate_term_and_interpretate_term_option
+ (interpretate_term_and_interpretate_term_option status
~obj_context:[] ~mk_choice:(fun _ -> assert false)
~create_dummy_ids:true ~env:DisambiguateTypes.Environment.empty
~uri:None ~is_path:true ~localization_tbl) ~context:[] path
;;
-let new_flavour_of_flavour = function
- | `Definition -> `Definition
- | `MutualDefinition -> `Definition
- | `Fact -> `Fact
- | `Lemma -> `Lemma
- | `Remark -> `Example
- | `Theorem -> `Theorem
- | `Variant -> `Corollary
- | `Axiom -> `Fact
-;;
-
let ncic_name_of_ident = function
| Ast.Ident (name, None) -> name
| _ -> assert false
;;
-let interpretate_obj
+let interpretate_obj status
(* ?(create_dummy_ids=false) *)
~context ~env ~uri ~is_path obj ~localization_tbl ~mk_choice
=
match obj with
| NotationPt.Theorem (flavour, name, ty, bo, pragma) ->
let ty' =
- interpretate_term
+ interpretate_term status
~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty
in
let height = (* XXX calculate *) 0 in
uri, height, [], [],
(match bo,flavour with
| None,`Axiom ->
- let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+ let attrs = `Provided, flavour, pragma in
NCic.Constant ([],name,None,ty',attrs)
| Some _,`Axiom -> assert false
| None,_ ->
- let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+ let attrs = `Provided, flavour, pragma in
NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
| Some bo,_ ->
(match bo with
NotationPt.Binder (kind, var, t)) params t
in
let cic_body =
- interpretate_term
+ interpretate_term status
~obj_context ~context ~env ~uri:None ~is_path:false
(add_binders `Lambda body)
in
let cic_type =
- interpretate_term_option
+ interpretate_term_option status
~obj_context:[]
~context ~env ~uri:None ~is_path:false `Type
(HExtlib.map_option (add_binders `Pi) typ)
([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
defs
in
- let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+ let attrs = `Provided, flavour, pragma in
NCic.Fixpoint (inductive,inductiveFuns,attrs)
| bo ->
let bo =
- interpretate_term
+ interpretate_term status
~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
in
- let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
+ let attrs = `Provided, flavour, pragma in
NCic.Constant ([],name,Some bo,ty',attrs)))
| NotationPt.Inductive (params,tyl) ->
let context,params =
| Some t -> t in
let name = cic_name_of_name name in
let t =
- interpretate_term ~obj_context:[] ~context ~env ~uri:None
+ interpretate_term status ~obj_context:[] ~context ~env ~uri:None
~is_path:false t
in
(name,NCic.Decl t)::context,(name,t)::res
(fun (name,_,ty,cl) ->
let ty' =
add_params
- (interpretate_term ~obj_context:[] ~context ~env ~uri:None
+ (interpretate_term status ~obj_context:[] ~context ~env ~uri:None
~is_path:false ty) in
let cl' =
List.map
(fun (name,ty) ->
let ty' =
add_params
- (interpretate_term ~obj_context ~context ~env ~uri:None
+ (interpretate_term status ~obj_context ~context ~env ~uri:None
~is_path:false ty) in
let relevance = [] in
relevance,name,ty'
| Some t -> t in
let name = cic_name_of_name name in
let t =
- interpretate_term ~obj_context:[] ~context ~env ~uri:None
+ interpretate_term status ~obj_context:[] ~context ~env ~uri:None
~is_path:false t
in
(name,NCic.Decl t)::context,(name,t)::res
let leftno = List.length params in
let ty' =
add_params
- (interpretate_term ~obj_context:[] ~context ~env ~uri:None
+ (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
List.fold_left
(fun (context,res) (name,ty,_coercion,_arity) ->
let ty =
- interpretate_term ~obj_context ~context ~env ~uri:None
+ interpretate_term status ~obj_context ~context ~env ~uri:None
~is_path:false ty in
let context' = (name,NCic.Decl ty)::context in
context',(name,ty)::res
NCic.Inductive (true,leftno,tyl,attrs)
;;
-let disambiguate_term ~context ~metasenv ~subst ~expty
- ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
- ~aliases ~universe ~rdb ~lookup_in_library
- (text,prefix_len,term)
- =
+let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst
+ ~expty ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
+ ~aliases ~universe ~lookup_in_library (text,prefix_len,term)
+=
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
let res,b =
MultiPassDisambiguator.disambiguate_thing
~context ~metasenv ~initial_ugraph:() ~aliases
~mk_implicit ~description_of_alias ~fix_instance
~string_context_of_context:(List.map (fun (x,_) -> Some x))
- ~universe ~uri:None ~pp_thing:NotationPp.pp_term
+ ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status)
~passes:(MultiPassDisambiguator.passes ())
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
- ~interpretate_thing:(interpretate_term ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
- ~refine_thing:(refine_term ~rdb) (text,prefix_len,term)
+ ~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
+ ~refine_thing:(refine_term status) (text,prefix_len,term)
~mk_localization_tbl ~expty ~subst
in
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
;;
-let disambiguate_obj
+let disambiguate_obj (status: #NCicCoercion.status)
~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
- ~aliases ~universe ~rdb ~lookup_in_library ~uri
- (text,prefix_len,obj)
+ ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
=
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
let res,b =
~string_context_of_context:(List.map (fun (x,_) -> Some x))
~universe
~uri:(Some uri)
- ~pp_thing:(NotationPp.pp_obj NotationPp.pp_term)
+ ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status))
~passes:(MultiPassDisambiguator.passes ())
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
- ~interpretate_thing:(interpretate_obj ~mk_choice)
- ~refine_thing:(refine_obj ~rdb)
+ ~interpretate_thing:(interpretate_obj status ~mk_choice)
+ ~refine_thing:(refine_obj status)
(text,prefix_len,obj)
~mk_localization_tbl ~expty:None
in
projects / helm.git / blobdiff