From 4325281db7a89cdc42be395362886d48d7c96987 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 21 Nov 2008 17:58:08 +0000 Subject: [PATCH] ... --- .../ng_disambiguation/nDisambiguate.ml | 382 ++++++++---------- .../ng_disambiguation/nDisambiguate.mli | 3 + 2 files changed, 172 insertions(+), 213 deletions(-) diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.ml b/helm/software/components/ng_disambiguation/nDisambiguate.ml index d350a7f23..514e2f781 100644 --- a/helm/software/components/ng_disambiguation/nDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nDisambiguate.ml @@ -31,6 +31,7 @@ open DisambiguateTypes open UriManager module Ast = CicNotationPt +module NRef = NReference let debug_print _ = ();; @@ -64,8 +65,9 @@ let refine_term metasenv subst context uri term _ ~localization_tbl = ;; 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 -> @@ -77,7 +79,7 @@ let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ? 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 @@ -100,7 +102,7 @@ let interpretate_term | 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 @@ -112,7 +114,7 @@ let interpretate_term ~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 @@ -128,144 +130,147 @@ let interpretate_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, _), _, _) -> @@ -360,102 +365,37 @@ let interpretate_term | `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 *) @@ -468,34 +408,50 @@ let interpretate_term 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 diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.mli b/helm/software/components/ng_disambiguation/nDisambiguate.mli index 8637e214b..279e54b78 100644 --- a/helm/software/components/ng_disambiguation/nDisambiguate.mli +++ b/helm/software/components/ng_disambiguation/nDisambiguate.mli @@ -6,11 +6,14 @@ val disambiguate_term : dbd:HSql.dbd -> context:NCic.context -> metasenv:NCic.metasenv -> + subst:NCic.substitution -> aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> + ?goal: int -> CicNotationPt.term Disambiguate.disambiguator_input -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * NCic.metasenv * (* new metasenv *) + NCic.substitution * NCic.term) list * (* disambiguated term *) bool end -- 2.39.2