let debug_print _ = ();;
let cic_name_of_name = function
- | Ast.Ident (n, None) -> n
+ | Ast.Ident (n,_) -> n
| _ -> assert false
;;
(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) ->
+ NCic.Implicit `Term
| 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)
| `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body)
| `Pi
| `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
- | `Exists ->
- Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", 0))
- (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ]))
+ | `Exists -> assert false)
+ (*Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", None))
+ (`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
let cic_outtype = aux_option ~localize loc context `Term outtype in
else
let indtype_ref =
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
- | 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))))
+ | Some (_,Some r) -> r
+ | Some (_, None) ->
+ raise (Disambiguate.Try_again
+ (lazy "The type of the term to be matched is still unknown"))
| None ->
let rec fst_constructor =
function
- (Ast.Pattern (head, _, _), _) :: _ -> head
+ (Ast.Pattern (head, href, _), _) :: _ ->
+ head, HExtlib.map_option NReference.string_of_reference href
| (Ast.Wildcard, _) :: tl -> fst_constructor tl
| [] -> raise (Invalid_choice (lazy (loc,"The type "^
"of the term to be matched cannot be determined "^
0 -> term
| n ->
NotationPt.Binder
- (`Lambda, (NotationPt.Ident ("_", None), None),
+ (`Lambda, (NotationPt.Ident ("_", `Ambiguous), None),
mk_lambdas (n - 1))
in
(("wildcard",None,[]),
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.Ident (name, subst) ->
- assert (subst = None);
- (try
- NCic.Rel (find_in_context name context)
- with Not_found ->
- try NCic.Const (List.assoc name obj_context)
- with Not_found ->
- Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
- | NotationPt.Uri (uri, subst) ->
- assert (subst = None);
+ | NotationPt.Ident (name, `Rel) ->
+ (try NCic.Rel (find_in_context name context)
+ with Not_found ->
+ (try NCic.Const (List.assoc name obj_context)
+ with Not_found -> assert false)) (* bug in initialize_ast *)
+ | NotationPt.Ident (name, `Ambiguous) ->
+ (try NCic.Const (List.assoc name obj_context)
+ with Not_found -> NCic.Implicit `Closed)
+ (* Disambiguate.resolve ~env ~mk_choice (Id (name,None)) (`Args [])) *)
+ | NotationPt.Ident (name, `Uri uri) ->
(try
NCic.Const (NReference.reference_of_string uri)
with NRef.IllFormedReference _ ->
| 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.Meta (index, subst) ->
;;
let ncic_name_of_ident = function
- | Ast.Ident (name, None) -> name
+ | Ast.Ident (name,_) -> name
| _ -> assert false
;;
NCic.Inductive (true,leftno,tyl,attrs)
;;
+let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names t =
+ (* ast_of_alias_spec is duplicate in Disambiguate *)
+ let ast_of_alias_spec t alias = match (t,alias) with
+ | _, GrafiteAst.Ident_alias (id,uri) -> Ast.Ident(id,`Uri uri)
+ | _, GrafiteAst.Symbol_alias (sym,uri,desc) -> Ast.Symbol (sym,Some (uri,desc))
+ | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
+ | _ -> assert false
+ 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)
+ in
+ let init_vars ~local_names vars =
+ (*
+ List.fold_right (fun (n,ty) (nacc,tyacc) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) vars (local_names,[])
+ *)
+ let a,b = List.fold_left (fun (nacc,tyacc) (n,ty) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) (local_names,[]) vars
+ in a, List.rev b
+ in
+ 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')
+ in
+ let mk_alias = function
+ | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
+ | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
+ | Ast.Num _ -> DisambiguateTypes.Num None
+ | _ -> 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)
+ | Ast.Ident (id,`Rel) -> init ~local_names (Ast.Ident (id,`Ambiguous))
+ | Ast.Ident (_,`Ambiguous)
+ | Ast.Num (_,None)
+ | Ast.Symbol (_,None) ->
+ let choices = lookup_choices (mk_alias t) in
+ if List.length choices <> 1 then t
+ else ast_of_alias_spec t (List.hd choices)
+ | Ast.AttributedTerm (a,u) -> Ast.AttributedTerm (a, init ~local_names u)
+ | Ast.Appl tl -> Ast.Appl (List.map (init ~local_names) tl)
+ | Ast.Binder (k,(n,ty),body) ->
+ let n' = cic_name_of_name n in
+ let ty' = HExtlib.map_option (init ~local_names) ty in
+ let body' = init ~local_names:(n'::local_names) body in
+ Ast.Binder (k,(n,ty'),body')
+ | Ast.Case (t,ity,oty,pl) ->
+ let t' = init ~local_names t in
+ let oty' = HExtlib.map_option (init ~local_names) oty in
+ let pl' =
+ 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')
+ | 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
+ let ty' = HExtlib.map_option (init ~local_names) ty in
+ let u' = init ~local_names u in
+ let v' = init ~local_names:(n'::local_names) v in
+ Ast.LetIn ((n,ty'),u',v')
+ | Ast.LetRec (ik,l,t) ->
+ let recfuns =
+ List.fold_right (fun (_,(n,_),_,_) acc ->
+ cic_name_of_name n::acc) l [] in
+ let l' = List.map (fun (vl,(n,ty),u,m) ->
+ let ln',vl' = init_vars ~local_names vl in
+ let ty' = HExtlib.map_option (init ~local_names:ln') ty in
+ let ln'' = recfuns@ln' in
+ let u' = init ~local_names:ln'' u in
+ vl',(n,ty'),u',m) l in
+ let t' = init ~local_names:(recfuns@local_names) t in
+ Ast.LetRec (ik,l',t') (* XXX: t??? *)
+ | t -> t
+;;
+
+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
+ let init_vars ~local_names vars =
+ let a,b = List.fold_left (fun (nacc,tyacc) (n,ty) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) (local_names,[]) vars
+ in a, List.rev b
+ (*List.fold_right (fun (n,ty) (nacc,tyacc) ->
+ (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
+ ) vars (local_names,[])*)
+ in
+
+ match o with
+ | Ast.Inductive (ls,itl) ->
+ let ln,ls' = init_vars ~local_names:[] ls in
+ let indtys =
+ List.fold_right
+ (fun (name,_,_,_) acc -> name::acc) itl [] in
+ let itl' = List.map
+ (fun (name,isind,ty,cl) ->
+ let ty' = init ~local_names:ln ty in
+ let cl' =
+ List.map (fun (cname,cty) ->
+ cname, init ~local_names:(indtys@ln) cty) cl
+ in
+ name,isind,ty',cl') itl
+ 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)
+ | 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 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 local_names = List.map (fun (n,_) -> n) context in
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 status)
+ ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status)
~passes:(MultiPassDisambiguator.passes ())
~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
- ~refine_thing:(refine_term status) (text,prefix_len,term)
+ ~refine_thing:(refine_term status)
+ (text,prefix_len,
+ (initialize_ast ~universe ~lookup_in_library ~local_names term))
+ ~visit:Disambiguate.bfvisit
~mk_localization_tbl ~expty ~subst
in
- List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
+ List.map (function (a,b,c,d,_) -> term,a,b,c,d) res, b
;;
+
let disambiguate_obj (status: #NCicCoercion.status)
~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
~string_context_of_context:(List.map (fun (x,_) -> Some x))
~universe
~uri:(Some uri)
- ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status))
+ ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status)) ~pp_term:(NotationPp.pp_term status)
~passes:(MultiPassDisambiguator.passes ())
~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,obj)
+ (text,prefix_len,(initialize_obj ~universe ~lookup_in_library obj))
+ ~visit:Disambiguate.bfvisit_obj
~mk_localization_tbl ~expty:None
in
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
projects / helm.git / blobdiff