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=false) ~obj_context ~mk_choice ~env ~universe ~uri ~is_path
~localization_tbl
=
+ let _ = (mk_choice : GrafiteAst.alias_spec -> NCic.term
+ DisambiguateTypes.codomain_item) in
(* create_dummy_ids shouldbe used only for interpretating patterns *)
assert (uri = None);
(NotationPt.AttributedTerm (att,(NotationPt.Appl inner))::args)->
aux ~localize loc context
(NotationPt.AttributedTerm (att,NotationPt.Appl (inner @ args)))
- | NotationPt.Appl (NotationPt.Symbol (symb, None) :: args) ->
+ | NotationPt.Appl (NotationPt.Symbol (symb, None) :: args)
+ | NotationPt.Appl
+ (NotationPt.AttributedTerm (_,NotationPt.Symbol (symb,None))::args) ->
NCic.Implicit `Term
- | NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) ->
+ | NotationPt.Appl (NotationPt.Symbol (symb, Some(uri,desc)) :: args)
+ | NotationPt.Appl (NotationPt.AttributedTerm
+ (_,NotationPt.Symbol (symb,Some (uri,desc)))::args) ->
let cic_args = List.map (aux ~localize loc context) args in
- Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)
+ (try
+ prerr_endline ("interpr Appl/Sym: " ^ symb);
+ let interpr = Some (GrafiteAst.Symbol_alias (symb, uri, desc)) in
+ Disambiguate.resolve ~mk_choice ~env ~universe (loc (*, Symbol symb*))
+ interpr (`Args cic_args)
+ with Failure err ->
+ prerr_endline ("resolve of " ^ symb ^ " failed: " ^ err);
+ assert false)
| NotationPt.Appl terms ->
NCic.Appl (List.map (aux ~localize loc context) terms)
| NotationPt.Binder (binder_kind, (var, typ), body) ->
raise (Disambiguate.Try_again
(lazy "The type of the term to be matched is still unknown"))
| None ->
- let rec fst_constructor =
+ let rec fst_constructor concrete_pat_found =
function
- (Ast.Pattern (head, href, _), _) :: _ ->
- head, HExtlib.map_option NReference.string_of_reference href
- | (Ast.Wildcard, _) :: tl -> fst_constructor tl
+ | (Ast.Pattern (_, None,_),_)::tl -> fst_constructor true tl
+ | (Ast.Pattern (head, Some href, _), _) :: _ ->
+ head, href
+ | (Ast.Wildcard, _) :: tl -> fst_constructor concrete_pat_found tl
+ | [] when concrete_pat_found -> raise (Disambiguate.Try_again
+ (lazy "The type of the term to be matched is still unknown"))
| [] -> raise (Invalid_choice (lazy (loc,"The type "^
"of the term to be matched cannot be determined "^
"because it is an inductive type without constructors "^
(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 (NReference.Ref (_,NReference.Con _) as r) ->
- let b,_,_,_,_= NCicEnvironment.get_checked_indtys status 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: "
- ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] t))))
+ let kname,href = fst_constructor false branches in
+ let b,_,_,_,_ = NCicEnvironment.get_checked_indtys status href
+ in
+ NReference.mk_indty b href
in
let _,leftsno,itl,_,indtyp_no =
NCicEnvironment.get_checked_indtys status indtype_ref in
NCic.Prod (_, _, t) -> 1 + (count_prod t)
| _ -> 0
in
- let rec sort branches cl =
+ let rec sort cno branches cl =
match cl with
[] ->
let rec analyze unused unrecognized useless =
(lazy (loc, "Missing case: " ^ name)))
| ((Ast.Wildcard, _) as branch :: _) as branches ->
branch, branches
+ | (Ast.Pattern (name',Some href,_),_) as branch :: tl ->
+ prerr_endline
+ (Printf.sprintf "analysis of %s and %s" name name');
+ (match href with
+ | NReference.Ref (curi, (NReference.Con (n,cno',_))) ->
+ (* check che la curi corrisponda alla uri del tipo induttivo *)
+ let this_indty = NReference.mk_indty true href in
+ if indtype_ref <> this_indty then
+ (prerr_endline "fail1";
+ raise (DisambiguateTypes.Invalid_choice
+ (lazy (loc, Printf.sprintf
+ "Malformed pattern matching: the matching type is %s, but constructor %s belongs to type %s."
+ (NReference.string_of_reference indtype_ref)
+ (NReference.string_of_reference href)
+ (NReference.string_of_reference this_indty)))))
+ else
+ if cno = cno' then (prerr_endline "ok";branch, tl)
+ else
+ (prerr_endline (Printf.sprintf "skip %d %d" cno cno');
+ let found,rest = find_and_remove tl in
+ found, branch::rest)
+ | _ ->
+ (prerr_endline "fail2";
+ raise
+ (DisambiguateTypes.Invalid_choice
+ (lazy (loc,"Malformed pattern: found " ^
+ (NReference.string_of_reference href) ^
+ " which is not a type constructor.")))))
| (Ast.Pattern (name',_,_),_) as branch :: tl
when name = name' ->
branch,tl
match branch with
Ast.Pattern (name,y,args),term ->
if List.length args = count_prod ty - leftsno then
- ((name,y,args),term)::sort tl cltl
+ ((name,y,args),term)::sort (cno+1) tl cltl
else
raise
(DisambiguateTypes.Invalid_choice
mk_lambdas (n - 1))
in
(("wildcard",None,[]),
- mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
+ mk_lambdas (count_prod ty - leftsno)) :: sort (cno+1) tl cltl
in
- let branches = sort branches cl in
+ let branches = sort 1 branches cl in
NCic.Match (indtype_ref, cic_outtype, cic_term,
(List.map do_branch branches))
| NotationPt.Cast (t1, t2) ->
| NotationPt.Implicit `JustOne -> NCic.Implicit `Term
| NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
| NotationPt.UserInput -> NCic.Implicit `Hole
- | NotationPt.Num (num, None) -> NCic.Implicit `Closed
- | NotationPt.Num (num, i) ->
- Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
+ | NotationPt.Num (num, i) ->
+ let i = HExtlib.map_option
+ (fun (uri,desc) -> GrafiteAst.Number_alias (uri,desc)) i in
+ Disambiguate.resolve ~env ~universe ~mk_choice (loc(*,Num*)) i (`Num_arg num)
| NotationPt.Meta (index, subst) ->
let cic_subst =
List.map
| NotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
[`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
| NotationPt.Symbol (symbol, instance) ->
- Disambiguate.resolve ~env ~mk_choice
- (Symbol (symbol, instance)) (`Args [])
+ let instance = HExtlib.map_option
+ (fun (uri,desc) -> GrafiteAst.Symbol_alias (symbol, uri, desc))
+ instance
+ in
+ Disambiguate.resolve ~env ~universe ~mk_choice
+ (loc (*,Symbol symbol*)) instance (`Args [])
| NotationPt.Variable _
| NotationPt.Magic _
| NotationPt.Layout _
(fun ~context -> aux_option ~localize:true HExtlib.dummy_floc context)
;;
-let interpretate_term status ?(create_dummy_ids=false) ~context ~env ~uri
+let interpretate_term status ?(create_dummy_ids=false) ~context ~env ~universe ~uri
~is_path ast ~obj_context ~localization_tbl ~mk_choice
=
let context = List.map fst context in
fst
(interpretate_term_and_interpretate_term_option status
- ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path
+ ~obj_context ~mk_choice ~create_dummy_ids ~env ~universe ~uri ~is_path
~localization_tbl)
~context ast
;;
-let interpretate_term_option status ?(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
+ ~universe ~uri ~is_path ~localization_tbl ~mk_choice ~obj_context
=
let context = List.map fst context in
snd
(interpretate_term_and_interpretate_term_option status
- ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path
+ ~obj_context ~mk_choice ~create_dummy_ids ~env ~universe ~uri ~is_path
~localization_tbl)
~context
;;
fst
(interpretate_term_and_interpretate_term_option status
~obj_context:[] ~mk_choice:(fun _ -> assert false)
- ~create_dummy_ids:true ~env:DisambiguateTypes.Environment.empty
+ ~create_dummy_ids:true ~env:DisambiguateTypes.InterprEnv.empty
+ ~universe:DisambiguateTypes.Environment.empty
~uri:None ~is_path:true ~localization_tbl) ~context:[] path
;;
let interpretate_obj status
(* ?(create_dummy_ids=false) *)
- ~context ~env ~uri ~is_path obj ~localization_tbl ~mk_choice
+ ~context ~env ~universe ~uri ~is_path obj ~localization_tbl ~mk_choice
=
assert (context = []);
assert (is_path = false);
| NotationPt.Theorem (flavour, name, ty, bo, pragma) ->
let ty' =
interpretate_term status
- ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty
+ ~obj_context:[] ~context:[] ~env ~universe ~uri:None ~is_path:false ty
in
let height = (* XXX calculate *) 0 in
uri, height, [], [],
in
let cic_body =
interpretate_term status
- ~obj_context ~context ~env ~uri:None ~is_path:false
+ ~obj_context ~context ~env ~universe ~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
+ ~context ~env ~universe ~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))
| bo ->
let bo =
interpretate_term status
- ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
+ ~obj_context:[] ~context:[] ~env ~universe ~uri:None ~is_path:false bo
in
let attrs = `Provided, flavour, pragma in
NCic.Constant ([],name,Some bo,ty',attrs)))
| Some t -> t in
let name = cic_name_of_name name in
let t =
- interpretate_term status ~obj_context:[] ~context ~env ~uri:None
+ interpretate_term status ~obj_context:[] ~context ~env ~universe ~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 status ~obj_context:[] ~context ~env ~uri:None
+ (interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None
~is_path:false ty) in
let cl' =
List.map
(fun (name,ty) ->
let ty' =
add_params
- (interpretate_term status ~obj_context ~context ~env ~uri:None
+ (interpretate_term status ~obj_context ~context ~env ~universe ~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 status ~obj_context:[] ~context ~env ~uri:None
+ interpretate_term status ~obj_context:[] ~context ~env ~universe ~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 status ~obj_context:[] ~context ~env ~uri:None
+ (interpretate_term status ~obj_context:[] ~context ~env ~universe ~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 status ~obj_context ~context ~env ~uri:None
+ interpretate_term status ~obj_context ~context ~env ~universe ~uri:None
~is_path:false ty in
let context' = (name,NCic.Decl ty)::context in
context',(name,ty)::res
| Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
| _ -> assert false
in
+ let lookup_choices =
+ fun item ->
+ (*match universe with
+ | None ->
+ lookup_in_library
+ interactive_user_uri_choice
+ input_or_locate_uri item
+ | Some e ->
+ (try Environment.find item e
+ with Not_found -> [])
+*)
+ (try
+ let res = Environment.find item universe in
+ let id = match item with
+ | DisambiguateTypes.Id id -> id
+ | DisambiguateTypes.Symbol _ -> "SYM"
+ | DisambiguateTypes.Num _ -> "NUM"
+ in
+ prerr_endline (Printf.sprintf "lookup_choices of %s returns length %d" id
+ (List.length res));
+ res
+ with Not_found -> [])
+ in
let init = initialize_ast ~universe ~lookup_in_library in
let init_var ~local_names (n,ty) =
(n,HExtlib.map_option (init ~local_names) ty)
let init_pattern ~local_names = function
| Ast.Wildcard as t -> local_names,t
| Ast.Pattern (c,uri,vars) ->
- (* XXX verificare ordine *)
let ln',vars' = init_vars ~local_names vars in
- ln',Ast.Pattern (c,uri,vars')
+ let uri' = match uri with
+ | Some _ -> uri
+ | None ->
+ let choices = lookup_choices (DisambiguateTypes.Id c) in
+ if List.length choices <> 1 then None
+ else (match (List.hd choices) with
+ | GrafiteAst.Ident_alias (_,u) ->
+ Some (NReference.reference_of_string u)
+ | _ -> assert false)
+ in
+ ln',Ast.Pattern (c,uri',vars')
in
let mk_alias = function
- | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
- | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
- | Ast.Num _ -> DisambiguateTypes.Num None
+ | Ast.Ident (id,_) -> DisambiguateTypes.Id id
+ | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol sym
+ | Ast.Num _ -> DisambiguateTypes.Num
| _ -> assert false
in
- let lookup_choices =
- fun item ->
- (*match universe with
- | None ->
- lookup_in_library
- interactive_user_uri_choice
- input_or_locate_uri item
- | Some e ->
- (try Environment.find item e
- with Not_found -> [])
-*)
- (try
- let res = Environment.find item universe in
- let id = match item with
- | DisambiguateTypes.Id (id,None) -> id ^ "?"
- | DisambiguateTypes.Id (id,_) -> id ^ "!"
- | DisambiguateTypes.Symbol _ -> "SYM"
- | DisambiguateTypes.Num _ -> "NUM"
- in
- prerr_endline (Printf.sprintf "lookup_choices of %s returns length %d" id
- (List.length res));
- res
- with Not_found -> [])
- in
match t with
| Ast.Ident (id,(`Ambiguous|`Rel))
when List.mem id local_names -> Ast.Ident (id,`Rel)
List.map (fun (p,u) ->
let ns,p' = init_pattern ~local_names p in
p',init ~local_names:ns u) pl in
- Ast.Case (t',ity,oty',pl')
+ let ity' = HExtlib.map_option
+ (fun (ity_id,href) ->
+ let href' = match href with
+ | None ->
+ let choices = lookup_choices (DisambiguateTypes.Id ity_id) in
+ if List.length choices <> 1 then None
+ else (match (List.hd choices) with
+ | GrafiteAst.Ident_alias (_,u) ->
+ Some (NReference.reference_of_string u)
+ | _ -> assert false)
+ | Some _ -> href
+ in (ity_id,href')) ity
+ in Ast.Case (t',ity',oty',pl')
| Ast.Cast (u,v) -> Ast.Cast (init ~local_names u,init ~local_names v)
| Ast.LetIn ((n,ty),u,v) ->
let n' = cic_name_of_name n in
| t -> t
;;
-let initialize_obj ~universe ~lookup_in_library o =
+let initialize_obj ~universe ~lookup_in_library o =
let init = initialize_ast ~universe ~lookup_in_library in
let init_var ~local_names (n,ty) =
(n,HExtlib.map_option (init ~local_names) ty)
in
Ast.Inductive (ls',itl')
| Ast.Theorem (flav,n,ty,bo,p) ->
- Ast.Theorem (flav,n,init ~local_names:[] ty,
- HExtlib.map_option (init ~local_names:[]) bo,p)
+ let ty' = init ~local_names:[] ty in
+ let bo' = HExtlib.map_option (init ~local_names:[]) bo in
+ Ast.Theorem (flav,n,ty',bo',p)
| Ast.Record (ls,n,ty,fl) ->
let ln,ls' = init_vars ~local_names:[] ls in
let ty' = init ~local_names:ln ty in
- let fl' = List.map (fun (fn,fty,b,i) ->
- fn,init ~local_names:ln fty,b,i) fl in
- Ast.Record (ls,n,ty',fl')
+ let _,fl' = List.fold_left (fun (ln0,fl0) (fn,fty,b,i) ->
+ (fn::ln0,(fn,init ~local_names:ln0 fty,b,i)::fl0)) (ln,[]) fl
+ in
+ let fl' = List.rev fl' in
+ Ast.Record (ls',n,ty',fl')
;;
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 _ = (aliases : GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t) in
let local_names = List.map (fun (n,_) -> n) context in
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
let res,b =
~visit:Disambiguate.bfvisit
~mk_localization_tbl ~expty ~subst
in
- List.map (function (a,b,c,d,_) -> term,a,b,c,d) res, b
+ List.map (function (t,a,b,c,_) -> t,a,b,c) res, b
;;
=
let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
let res,b =
+ let obj' = initialize_obj ~universe ~lookup_in_library obj in
MultiPassDisambiguator.disambiguate_thing
~freshen_thing:NotationUtil.freshen_obj
~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
~interpretate_thing:(interpretate_obj status ~mk_choice)
~refine_thing:(refine_obj status)
- (text,prefix_len,(initialize_obj ~universe ~lookup_in_library obj))
+ (text,prefix_len,obj')
~visit:Disambiguate.bfvisit_obj
~mk_localization_tbl ~expty:None
in
- List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
+ List.map (function (o,a,b,c,_) -> o,a,b,c) res, b
;;
(*
let _ =
projects / helm.git / blobdiff