open UriManager
module Ast = CicNotationPt
+module NRef = NReference
let debug_print _ = ();;
;;
let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
- assert false;;
-(*
+ ignore (env,item,num,args);
+ assert false
+ (*
try
snd (Environment.find item env) env num args
with Not_found ->
let find_in_context name context =
let rec aux acc = function
| [] -> raise Not_found
- | Cic.Name hd :: _ when hd = name -> acc
+ | hd :: _ when hd = name -> acc
| _ :: tl -> aux (acc + 1) tl
in
aux 1 context
| CicNotationPt.Appl terms ->
NCic.Appl (List.map (aux ~localize loc context) terms)
| CicNotationPt.Binder (binder_kind, (var, typ), body) ->
- let cic_type = aux_option ~localize loc context (Some `Type) typ in
+ let cic_type = aux_option ~localize loc context `Type typ in
let cic_name = cic_name_of_name var in
let cic_body = aux ~localize loc (cic_name :: context) body in
(match binder_kind with
~args:[ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ] ())
| CicNotationPt.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux ~localize loc context term in
- let cic_outtype = aux_option ~localize loc context None outtype in
+ let cic_outtype = aux_option ~localize loc context `Term outtype in
let do_branch ((_, _, args), term) =
let rec do_branch' context = function
| [] -> aux ~localize loc context term
in
do_branch' context args
in
- let indtype_uri, indtype_no =
- if create_dummy_ids then
- (UriManager.uri_of_string "cic:/fake_indty.con", 0)
- else
+ if create_dummy_ids then
+ let branches =
+ List.map
+ (function
+ Ast.Wildcard,term -> ("wildcard",None,[]), term
+ | Ast.Pattern _,_ ->
+ raise (DisambiguateTypes.Invalid_choice
+ (lazy (loc, "Syntax error: the left hand side of a "^
+ "branch pattern must be \"_\"")))
+ ) branches
+ in
+ (*
+ NCic.MutCase (ref, cic_outtype, cic_term,
+ (List.map do_branch branches))
+ *) ignore branches; assert false (* patterns not implemented yet *)
+ else
+ let indtype_ref =
match indty_ident with
| Some (indty_ident, _) ->
(match resolve env (Id indty_ident) () with
- | NCic.Const (NRef.Ref (uri, NRef.Ind (_, tyno))) -> (uri, tyno)
+ | NCic.Const r -> r
| NCic.Implicit _ ->
raise (Disambiguate.Try_again
(lazy "The type of the term to be matched is still unknown"))
| _ ->
raise (DisambiguateTypes.Invalid_choice
- (Some loc,
- lazy "The type of the term to be matched is not (co)inductive!")))
+ (lazy (loc,"The type of the term to be matched "^
+ "is not (co)inductive!"))))
| None ->
let rec fst_constructor =
function
(Ast.Pattern (head, _, _), _) :: _ -> head
| (Ast.Wildcard, _) :: tl -> fst_constructor tl
- | [] -> raise (Invalid_choice (Some loc, lazy "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"))
+ | [] -> raise (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")))
in
(match resolve env (Id (fst_constructor branches)) () with
- | NCic.MutConstruct (indtype_uri, indtype_no, _, _) ->
- (indtype_uri, indtype_no)
+ | NCic.Const r -> r
| NCic.Implicit _ ->
- raise (Disambiguate.Try_again (lazy "The type of the term to be matched
- is still unknown"))
+ raise (Disambiguate.Try_again
+ (lazy "The type of the term to be matched is still unknown"))
| _ ->
- raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
- in
- let branches =
- if create_dummy_ids then
- List.map
- (function
- Ast.Wildcard,term -> ("wildcard",None,[]), term
- | Ast.Pattern _,_ ->
- raise (DisambiguateTypes.Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
- ) branches
- else
- match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
- NCic.InductiveDefinition (il,_,leftsno,_) ->
- let _,_,_,cl =
- try
- List.nth il indtype_no
- with _ -> assert false
- in
- let rec count_prod t =
- match CicReduction.whd [] t with
- NCic.Prod (_, _, t) -> 1 + (count_prod t)
- | _ -> 0
- in
- let rec sort branches cl =
- match cl with
+ raise (DisambiguateTypes.Invalid_choice
+ (lazy (loc,
+ "The type of the term to be matched is not (co)inductive!"))))
+ in
+ let _,leftsno,itl,_,indtyp_no =
+ NCicEnvironment.get_checked_indtys indtype_ref in
+ let _,_,_,cl =
+ try
+ List.nth itl indtyp_no
+ with _ -> assert false in
+ let rec count_prod t =
+ match NCicReduction.whd [] t with
+ NCic.Prod (_, _, t) -> 1 + (count_prod t)
+ | _ -> 0
+ in
+ let rec sort branches cl =
+ match cl with
+ [] ->
+ let rec analyze unused unrecognized useless =
+ function
[] ->
- let rec analyze unused unrecognized useless =
- function
- [] ->
- if unrecognized != [] then
- raise (DisambiguateTypes.Invalid_choice
- (Some loc,
- lazy
- ("Unrecognized constructors: " ^
- String.concat " " unrecognized)))
- else if useless > 0 then
- raise (DisambiguateTypes.Invalid_choice
- (Some loc,
- lazy
- ("The last " ^ string_of_int useless ^
- "case" ^ if useless > 1 then "s are" else " is" ^
- " unused")))
- else
- []
- | (Ast.Wildcard,_)::tl when not unused ->
- analyze true unrecognized useless tl
- | (Ast.Pattern (head,_,_),_)::tl when not unused ->
- analyze unused (head::unrecognized) useless tl
- | _::tl -> analyze unused unrecognized (useless + 1) tl
- in
- analyze false [] 0 branches
- | (name,ty)::cltl ->
- let rec find_and_remove =
+ if unrecognized != [] then
+ raise (DisambiguateTypes.Invalid_choice
+ (lazy
+ (loc,"Unrecognized constructors: " ^
+ String.concat " " unrecognized)))
+ else if useless > 0 then
+ raise (DisambiguateTypes.Invalid_choice
+ (lazy
+ (loc,"The last " ^ string_of_int useless ^
+ "case" ^ if useless > 1 then "s are" else " is" ^
+ " unused")))
+ else
+ []
+ | (Ast.Wildcard,_)::tl when not unused ->
+ analyze true unrecognized useless tl
+ | (Ast.Pattern (head,_,_),_)::tl when not unused ->
+ analyze unused (head::unrecognized) useless tl
+ | _::tl -> analyze unused unrecognized (useless + 1) tl
+ in
+ analyze false [] 0 branches
+ | (_,name,ty)::cltl ->
+ let rec find_and_remove =
+ function
+ [] ->
+ raise
+ (DisambiguateTypes.Invalid_choice
+ (lazy (loc, "Missing case: " ^ name)))
+ | ((Ast.Wildcard, _) as branch :: _) as branches ->
+ branch, branches
+ | (Ast.Pattern (name',_,_),_) as branch :: tl
+ when name = name' ->
+ branch,tl
+ | branch::tl ->
+ let found,rest = find_and_remove tl in
+ found, branch::rest
+ in
+ let branch,tl = find_and_remove branches in
+ 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
+ else
+ raise
+ (DisambiguateTypes.Invalid_choice
+ (lazy (loc,"Wrong number of arguments for " ^ name)))
+ | Ast.Wildcard,term ->
+ let rec mk_lambdas =
function
- [] ->
- raise
- (DisambiguateTypes.Invalid_choice
- (Some loc, lazy ("Missing case: " ^ name)))
- | ((Ast.Wildcard, _) as branch :: _) as branches ->
- branch, branches
- | (Ast.Pattern (name',_,_),_) as branch :: tl
- when name = name' ->
- branch,tl
- | branch::tl ->
- let found,rest = find_and_remove tl in
- found, branch::rest
+ 0 -> term
+ | n ->
+ CicNotationPt.Binder
+ (`Lambda, (CicNotationPt.Ident ("_", None), None),
+ mk_lambdas (n - 1))
in
- let branch,tl = find_and_remove branches in
- 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
- else
- raise
- (DisambiguateTypes.Invalid_choice
- (Some loc,
- lazy ("Wrong number of arguments for " ^ name)))
- | Ast.Wildcard,term ->
- let rec mk_lambdas =
- function
- 0 -> term
- | n ->
- CicNotationPt.Binder
- (`Lambda, (CicNotationPt.Ident ("_", None), None),
- mk_lambdas (n - 1))
- in
- (("wildcard",None,[]),
- mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
- in
- sort branches cl
- | _ -> assert false
- in
- NCic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
- (List.map do_branch branches))
+ (("wildcard",None,[]),
+ mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
+ in
+ let branches = sort branches cl in
+ NCic.Match (indtype_ref, cic_outtype, cic_term,
+ (List.map do_branch branches))
| CicNotationPt.Cast (t1, t2) ->
let cic_t1 = aux ~localize loc context t1 in
let cic_t2 = aux ~localize loc context t2 in
- NCic.Cast (cic_t1, cic_t2)
+ NCic.LetIn ("_",cic_t2,cic_t1, NCic.Rel 1)
| CicNotationPt.LetIn ((name, typ), def, body) ->
let cic_def = aux ~localize loc context def in
let cic_name = cic_name_of_name name in
let cic_typ =
match typ with
- | None -> NCic.Implicit (Some `Type)
+ | None -> NCic.Implicit `Type
| Some t -> aux ~localize loc context t
in
let cic_body = aux ~localize loc (cic_name :: context) body in
NCic.LetIn (cic_name, cic_def, cic_typ, cic_body)
- | CicNotationPt.LetRec (kind, defs, body) ->
+ | CicNotationPt.LetRec (_kind, _defs, _body) ->
+ assert false (*
let context' =
List.fold_left
(fun acc (_, (name, _), _, _) ->
| `AddLetIn cic_body ->
List.fold_right (build_term inductiveFuns) inductiveFuns
cic_body)
+*)
| CicNotationPt.Ident _
| CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
- | CicNotationPt.Ident (name, subst)
- | CicNotationPt.Uri (name, subst) as ast ->
- let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
- (try
- if is_uri ast then raise Not_found;(* don't search the env for URIs *)
- let index = find_in_context name context in
- if subst <> None then
- CicNotationPt.fail loc "Explicit substitutions not allowed here";
- NCic.Rel index
- with Not_found ->
- let cic =
- if is_uri ast then (* we have the URI, build the term out of it *)
- try
- CicUtil.term_of_uri (UriManager.uri_of_string name)
- with UriManager.IllFormedUri _ ->
- CicNotationPt.fail loc "Ill formed URI"
- else
- resolve env (Id name) ()
- in
- let mk_subst uris =
- let ids_to_uris =
- List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
- in
- (match subst with
- | Some subst ->
- List.map
- (fun (s, term) ->
- (try
- List.assoc s ids_to_uris, aux ~localize loc context term
- with Not_found ->
- raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
- subst
- | None -> List.map (fun uri -> uri, NCic.Implicit None) uris)
- in
- (try
- match cic with
- | NCic.Const (uri, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- NCic.Const (uri, mk_subst uris)
- | NCic.Var (uri, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- NCic.Var (uri, mk_subst uris)
- | NCic.MutInd (uri, i, []) ->
- (try
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- NCic.MutInd (uri, i, mk_subst uris)
- with
- CicEnvironment.Object_not_found _ ->
- (* if we are here it is probably the case that during the
- definition of a mutual inductive type we have met an
- occurrence of the type in one of its constructors.
- However, the inductive type is not yet in the environment
- *)
- (*here the explicit_named_substituion is assumed to be of length 0 *)
- NCic.MutInd (uri,i,[]))
- | NCic.MutConstruct (uri, i, j, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- NCic.MutConstruct (uri, i, j, mk_subst uris)
- | NCic.Meta _ | NCic.Implicit _ as t ->
-(*
- debug_print (lazy (sprintf
- "Warning: %s must be instantiated with _[%s] but we do not enforce it"
- (CicPp.ppterm t)
- (String.concat "; "
- (List.map
- (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
- subst))));
-*)
- t
- | _ ->
- raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
- with
- CicEnvironment.CircularDependency _ ->
- raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
- | CicNotationPt.Implicit -> NCic.Implicit None
- | CicNotationPt.UserInput -> NCic.Implicit (Some `Hole)
+ | CicNotationPt.Ident (name, subst) ->
+ assert (subst = None);
+ (try
+ NCic.Rel (find_in_context name context)
+ with Not_found -> resolve env (Id name) ())
+ | CicNotationPt.Uri (name, subst) ->
+ assert (subst = None);
+ (try
+ NCic.Const (NRef.reference_of_string name)
+ with NRef.IllFormedReference _ ->
+ CicNotationPt.fail loc "Ill formed reference")
+ | CicNotationPt.Implicit -> NCic.Implicit `Term
+ | CicNotationPt.UserInput -> assert false (*NCic.Implicit (Some `Hole)
+patterns not implemented *)
| CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
| CicNotationPt.Meta (index, subst) ->
let cic_subst =
- List.map
- (function
- None -> None
- | Some term -> Some (aux ~localize loc context term))
- subst
+ List.map
+ (function None -> assert false| Some t -> aux ~localize loc context t)
+ subst
in
- NCic.Meta (index, cic_subst)
+ NCic.Meta (index, (0, NCic.Ctx cic_subst))
| CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop
- | CicNotationPt.Sort `Set -> NCic.Sort NCic.Set
- | CicNotationPt.Sort (`Type u) -> NCic.Sort (NCic.Type u)
- | CicNotationPt.Sort (`CProp u) -> NCic.Sort (NCic.CProp u)
+ | CicNotationPt.Sort `Set -> assert false
+ | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
+ [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
+ | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
+ [false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"])
| CicNotationPt.Symbol (symbol, instance) ->
resolve env (Symbol (symbol, instance)) ()
| _ -> assert false (* god bless Bologna *)
let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
~localization_tbl
=
- let context = List.map (function None -> NCic.Anonymous | Some (n,_) -> n) context in
+ let context = List.map fst context in
interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
~localization_tbl
;;
let domain_of_term ~context =
- let context = List.map (fun x -> NCic.Name (fst x)) context in
+ let context = List.map (fun name,_ -> Cic.Name name) context in
Disambiguate.domain_of_ast_term ~context
;;
module Make (C : DisambiguateTypes.Callbacks) = struct
module Disambiguator = Disambiguate.Make(C)
- let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
- ?(initial_ugraph = ()) ~aliases ~universe
- (text,prefix_len,term)
+ let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv ~subst
+ ~aliases ~universe ?goal (text,prefix_len,term)
=
let term =
if fresh_instances then CicNotationUtil.freshen_term term else term
in
- let localization_tbl = NCic.NCicHash.create 503 in
- Disambiguator.disambiguate_thing
- ~dbd ~context ~metasenv ~initial_ugraph ~aliases
- ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
- ~domain_of_thing:domain_of_term
- ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
- ~refine_thing:refine_term (text,prefix_len,term)
- ~localization_tbl
+ let localization_tbl = NCicUntrusted.NCicHash.create 503 in
+ let hint =
+ match goal with
+ None -> (fun _ y -> y),(fun x -> x)
+ | Some n ->
+ (fun metasenv y ->
+ let _,_,ty = NCicUtils.lookup_meta n metasenv in
+ NCic.LetIn ("_",ty,y,NCic.Rel 1)),
+ (function
+ | Disambiguate.Ok (t,m,s,ug) ->
+ (match t with
+ | NCic.LetIn ("_",_,y,NCic.Rel 1) -> Disambiguate.Ok (y,m,s,ug)
+ | _ -> assert false)
+ | k -> k)
+ in
+ let res,b =
+ Disambiguator.disambiguate_thing
+ ~dbd ~context ~metasenv ~initial_ugraph:() ~aliases
+ ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
+ ~domain_of_thing:domain_of_term
+ ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
+ ~refine_thing:refine_term (text,prefix_len,term)
+ ~localization_tbl ~hint ~subst
+ in
+ List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
;;
end
projects / helm.git / commitdiff