From: Stefano Zacchiroli Date: Wed, 4 Feb 2004 09:42:58 +0000 (+0000) Subject: - sorted domain which hopefully avoids exponential explosion X-Git-Tag: V_0_2_3~79 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f67ef877debe15f14da063eff415fd1748b33e54;p=helm.git - sorted domain which hopefully avoids exponential explosion - ported to CicAst --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index b2b714975..657eb5485 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -75,15 +75,14 @@ let find_in_environment name context = let interpretate ~context ~env ast = let rec aux loc context = function - | CicTextualParser2Ast.AttributedTerm (`Loc loc, term) -> + | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term - | CicTextualParser2Ast.AttributedTerm (_, term) -> aux loc context term - | CicTextualParser2Ast.Appl terms -> - Cic.Appl (List.map (aux loc context) terms) - | CicTextualParser2Ast.Appl_symbol (symb, i, args) -> + | CicAst.AttributedTerm (_, term) -> aux loc context term + | CicAst.Appl (CicAst.Symbol (symb, i) :: args) -> let cic_args = List.map (aux loc context) args in resolve env (Symbol (symb, i)) ~args:cic_args () - | CicTextualParser2Ast.Binder (binder_kind, (var, typ), body) -> + | CicAst.Appl terms -> Cic.Appl (List.map (aux loc context) terms) + | CicAst.Binder (binder_kind, (var, typ), body) -> let cic_type = aux_option loc context typ in let cic_body = aux loc (var :: context) body in (match binder_kind with @@ -92,7 +91,7 @@ let interpretate ~context ~env ast = | `Exists -> resolve env (Symbol ("exists", 0)) ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ()) - | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) -> + | CicAst.Case (term, indty_ident, outtype, branches) -> let cic_term = aux loc context term in let cic_outtype = aux_option loc context outtype in let do_branch ((head, args), term) = @@ -117,7 +116,7 @@ let interpretate ~context ~env ast = in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) - | CicTextualParser2Ast.LetIn ((name, typ), def, body) -> + | CicAst.LetIn ((name, typ), def, body) -> let cic_def = aux loc context def in let cic_def = match typ with @@ -126,7 +125,7 @@ let interpretate ~context ~env ast = in let cic_body = aux loc (name :: context) body in Cic.LetIn (name, cic_def, cic_body) - | CicTextualParser2Ast.LetRec (kind, defs, body) -> + | CicAst.LetRec (kind, defs, body) -> let context' = List.fold_left (fun acc ((name, _), _, _) -> name :: acc) context defs @@ -166,7 +165,7 @@ let interpretate ~context ~env ast = Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic)) in List.fold_right (build_term inductiveFuns) inductiveFuns cic_body - | CicTextualParser2Ast.Ident (name, subst) -> + | CicAst.Ident (name, subst) -> (* TODO hanlde explicit substitutions *) (try let index = find_in_environment name context in @@ -175,42 +174,43 @@ let interpretate ~context ~env ast = "Explicit substitutions not allowed here"; Cic.Rel index with Not_found -> resolve env (Id name) ()) - | CicTextualParser2Ast.Num (num, i) -> resolve env (Num i) ~num () - | CicTextualParser2Ast.Meta (index, subst) -> + | CicAst.Implicit -> Cic.Implicit + | CicAst.Num (num, i) -> resolve env (Num i) ~num () + | CicAst.Meta (index, subst) -> let cic_subst = List.map (function None -> None | Some term -> Some (aux loc context term)) subst in Cic.Meta (index, cic_subst) - | CicTextualParser2Ast.Sort `Prop -> Cic.Sort Cic.Prop - | CicTextualParser2Ast.Sort `Set -> Cic.Sort Cic.Set - | CicTextualParser2Ast.Sort `Type -> Cic.Sort Cic.Type - | CicTextualParser2Ast.Sort `CProp -> Cic.Sort Cic.CProp + | CicAst.Sort `Prop -> Cic.Sort Cic.Prop + | CicAst.Sort `Set -> Cic.Sort Cic.Set + | CicAst.Sort `Type -> Cic.Sort Cic.Type + | CicAst.Sort `CProp -> Cic.Sort Cic.CProp + | CicAst.Symbol (symbol, instance) -> + resolve env (Symbol (symbol, instance)) () and aux_option loc context = function | None -> Cic.Implicit | Some term -> aux loc context term in match ast with - | CicTextualParser2Ast.AttributedTerm (`Loc loc, term) -> aux loc context term + | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term | _ -> assert false let domain_of_term ~context ast = + (* "aux" keeps domain in reverse order and doesn't care about duplicates. + * Domain item more in deep in the list will be processed first. + *) let rec aux loc context = function - | CicTextualParser2Ast.AttributedTerm (`Loc loc, term) -> - aux loc context term - | CicTextualParser2Ast.AttributedTerm (_, term) -> aux loc context term - | CicTextualParser2Ast.Appl terms -> - List.fold_left (fun dom term -> Domain.union dom (aux loc context term)) - Domain.empty terms - | CicTextualParser2Ast.Appl_symbol (symb, i, args) -> - List.fold_left (fun dom term -> Domain.union dom (aux loc context term)) - (Domain.singleton (Symbol (symb, i))) args - | CicTextualParser2Ast.Binder (_, (var, typ), body) -> + | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term + | CicAst.AttributedTerm (_, term) -> aux loc context term + | CicAst.Appl terms -> + List.fold_left (fun dom term -> aux loc context term @ dom) [] terms + | CicAst.Binder (_, (var, typ), body) -> let type_dom = aux_option loc context typ in let body_dom = aux loc (var :: context) body in - Domain.union type_dom body_dom - | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) -> + body_dom @ type_dom + | CicAst.Case (term, indty_ident, outtype, branches) -> let term_dom = aux loc context term in let outtype_dom = aux_option loc context outtype in let do_branch ((head, args), term) = @@ -220,27 +220,21 @@ let domain_of_term ~context ast = (name :: cont, (match typ with | None -> dom - | Some typ -> Domain.union dom (aux loc cont typ)))) - (context, Domain.empty) args + | Some typ -> aux loc cont typ @ dom))) + (context, []) args in - Domain.union (aux loc term_context term) args_domain + args_domain @ aux loc term_context term in let branches_dom = - List.fold_left (fun dom branch -> Domain.union dom (do_branch branch)) - Domain.empty branches + List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches in - Domain.add (Id indty_ident) - (Domain.union outtype_dom (Domain.union term_dom branches_dom)) - | CicTextualParser2Ast.LetIn ((var, typ), body, where) -> + branches_dom @ outtype_dom @ term_dom @ [ Id indty_ident ] + | CicAst.LetIn ((var, typ), body, where) -> let body_dom = aux loc context body in - let type_dom = - match typ with - | None -> Domain.empty - | Some typ -> aux loc context typ - in + let type_dom = aux_option loc context typ in let where_dom = aux loc (var :: context) where in - Domain.union (Domain.union body_dom where_dom) type_dom - | CicTextualParser2Ast.LetRec (kind, defs, where) -> + where_dom @ type_dom @ body_dom + | CicAst.LetRec (kind, defs, where) -> let context' = List.fold_left (fun acc ((var, typ), _, _) -> var :: acc) context defs @@ -249,33 +243,69 @@ let domain_of_term ~context ast = let defs_dom = List.fold_left (fun dom ((_, typ), body, _) -> - Domain.union (aux loc context' body) (aux_option loc context typ)) - Domain.empty defs + aux loc context' body @ aux_option loc context typ) + [] defs in - Domain.union where_dom defs_dom - | CicTextualParser2Ast.Ident (name, subst) -> + where_dom @ defs_dom + | CicAst.Ident (name, subst) -> (* TODO hanlde explicit substitutions *) (try let index = find_in_environment name context in if subst <> [] then CicTextualParser2.fail loc "Explicit substitutions not allowed here"; - Domain.empty - with Not_found -> Domain.singleton (Id name)) - | CicTextualParser2Ast.Num (num, i) -> Domain.singleton (Num i) - | CicTextualParser2Ast.Meta (index, local_context) -> - List.fold_left - (fun dom term -> Domain.union dom (aux_option loc context term)) - Domain.empty local_context - | CicTextualParser2Ast.Sort _ -> Domain.empty + [] + with Not_found -> [ Id name ]) + | CicAst.Implicit -> [] + | CicAst.Num (num, i) -> [ Num i ] + | CicAst.Meta (index, local_context) -> + List.fold_left (fun dom term -> aux_option loc context term @ dom) [] + local_context + | CicAst.Sort _ -> [] + | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ] + and aux_option loc context = function - | None -> Domain.empty + | None -> [] | Some t -> aux loc context t in + + (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *) + let rev_uniq = + let module SortedItem = + struct + type t = DisambiguateTypes.domain_item + let compare = Pervasives.compare + end + in + let module Set = Set.Make (SortedItem) in + fun l -> + let rev_l = List.rev l in + let (_, uniq_rev_l) = + List.fold_left + (fun (members, rev_l) elt -> + if Set.mem elt members then + (members, rev_l) + else + Set.add elt members, elt :: rev_l) + (Set.empty, []) rev_l + in + List.rev uniq_rev_l + in + match ast with - | CicTextualParser2Ast.AttributedTerm (`Loc loc, term) -> aux loc context term + | CicAst.AttributedTerm (`Loc loc, term) -> rev_uniq (aux loc context term) | _ -> assert false + + (* dom1 \ dom2 *) +let domain_diff dom1 dom2 = +(* let domain_diff = Domain.diff *) + let is_in_dom2 = + List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt')) + (fun _ -> false) dom2 + in + List.filter (fun elt -> not (is_in_dom2 elt)) dom1 + module Make (C: Callbacks) = struct let choices_of_id mqi_handle id = @@ -320,10 +350,6 @@ module Make (C: Callbacks) = let disambiguate_term mqi_handle context metasenv term ~aliases:current_env = - let current_dom = (* TODO temporary, remove ASAP *) - Environment.fold (fun item _ dom -> Domain.add item dom) - current_env Domain.empty - in debug_print "NEW DISAMBIGUATE INPUT"; let disambiguate_context = (* cic context -> disambiguate context *) List.map @@ -333,7 +359,10 @@ module Make (C: Callbacks) = let term_dom = domain_of_term ~context:disambiguate_context term in debug_print (sprintf "DISAMBIGUATION DOMAIN: %s" (string_of_domain term_dom)); - let todo_dom = Domain.diff term_dom current_dom in + let current_dom = + Environment.fold (fun item _ dom -> item :: dom) current_env [] + in + let todo_dom = domain_diff term_dom current_dom in (* (2) lookup function for any item (Id/Symbol/Num) *) let lookup_choices = let id_choices = Hashtbl.create 1023 in @@ -357,10 +386,10 @@ module Make (C: Callbacks) = *) let test_env current_env todo_dom = let filled_env = - Domain.fold - (fun item env -> + List.fold_left + (fun env item -> Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env) - todo_dom current_env + current_env todo_dom in try let cic_term = @@ -373,36 +402,34 @@ module Make (C: Callbacks) = in (* (4) build all possible interpretations *) let rec aux current_env todo_dom = - if Domain.is_empty todo_dom then - match test_env current_env Domain.empty with - | Ok (term, metasenv) -> [ current_env, term, metasenv ] - | Ko | Uncertain -> [] - else - let item = Domain.choose todo_dom in - let remaining_dom = Domain.remove item todo_dom in - debug_print (sprintf "CHOOSED ITEM: %s" (string_of_domain_item item)); - let choices = lookup_choices item in - let rec filter = function - | [] -> [] - | codomain_item :: tl -> - debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ; - let new_env = Environment.add item codomain_item current_env in - (match test_env new_env remaining_dom with - | Ok (term, metasenv) -> - (if Domain.is_empty remaining_dom then - [ new_env, term, metasenv ] - else - aux new_env remaining_dom) - @ filter tl - | Uncertain -> - (if Domain.is_empty remaining_dom then - [] - else - aux new_env remaining_dom) - @ filter tl - | Ko -> filter tl) - in - filter choices + match todo_dom with + | [] -> + (match test_env current_env [] with + | Ok (term, metasenv) -> [ current_env, term, metasenv ] + | Ko | Uncertain -> []) + | item :: remaining_dom -> + debug_print (sprintf "CHOOSED ITEM: %s" + (string_of_domain_item item)); + let choices = lookup_choices item in + let rec filter = function + | [] -> [] + | codomain_item :: tl -> + debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ; + let new_env = + Environment.add item codomain_item current_env + in + (match test_env new_env remaining_dom with + | Ok (term, metasenv) -> + (match remaining_dom with + | [] -> [ new_env, term, metasenv ] + | _ -> aux new_env remaining_dom) @ filter tl + | Uncertain -> + (match remaining_dom with + | [] -> [] + | _ -> aux new_env remaining_dom) @ filter tl + | Ko -> filter tl) + in + filter choices in let (choosed_env, choosed_term, choosed_metasenv) = match aux current_env todo_dom with @@ -421,7 +448,7 @@ module Make (C: Callbacks) = fst (Environment.find domain_item env) in (descr_of_domain_item domain_item, description)) - (Domain.elements term_dom)) + term_dom) l in let choosed = C.interactive_interpretation_choice choices in diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index 13d3adc6f..0e05413b8 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -35,7 +35,7 @@ module Make (C : Callbacks) : MQIConn.handle -> Cic.context -> Cic.metasenv -> - CicTextualParser2Ast.term -> + CicAst.term -> aliases:environment -> (* previous interpretation status *) environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *)