-requires="helm-content_pres helm-ng_library helm-cic_disambiguation camlp5.gramlib"
+requires="helm-content_pres helm-ng_library camlp5.gramlib"
version="0.0.1"
archive(byte)="lexicon.cma"
archive(native)="lexicon.cmxa"
-requires="helm-whelp helm-acic_content helm-ng_refiner helm-disambiguation helm-cic_disambiguation"
+requires="helm-acic_content helm-ng_refiner helm-disambiguation"
version="0.0.1"
archive(byte)="ng_disambiguation.cma"
archive(native)="ng_disambiguation.cmxa"
-requires="helm-cic_proof_checking helm-library helm-metadata"
+requires="helm-cic_proof_checking helm-library"
version="0.0.1"
archive(byte)="ng_kernel.cma"
archive(native)="ng_kernel.cmxa"
-requires="helm-extlib helm-cic_proof_checking helm-cic_unification helm-whelp"
+requires="helm-extlib helm-cic_proof_checking helm-cic_unification"
version="0.0.1"
archive(byte)="tactics.cma"
archive(native)="tactics.cmxa"
+++ /dev/null
-requires="helm-metadata"
-version="0.0.1"
-archive(byte)="whelp.cma"
-archive(native)="whelp.cmxa"
acic_content \
grafite \
cic_unification \
- whelp \
tactics \
acic_procedural \
disambiguation \
- cic_disambiguation \
ng_kernel \
ng_refiner \
ng_disambiguation \
+++ /dev/null
-cicDisambiguate.cmi:
-disambiguateChoices.cmi:
-cicDisambiguate.cmo: cicDisambiguate.cmi
-cicDisambiguate.cmx: cicDisambiguate.cmi
-disambiguateChoices.cmo: disambiguateChoices.cmi
-disambiguateChoices.cmx: disambiguateChoices.cmi
-number_notation.cmo: disambiguateChoices.cmi
-number_notation.cmx: disambiguateChoices.cmx
+++ /dev/null
-cicDisambiguate.cmi:
-disambiguateChoices.cmi:
-cicDisambiguate.cmo: cicDisambiguate.cmi
-cicDisambiguate.cmx: cicDisambiguate.cmi
-disambiguateChoices.cmo: disambiguateChoices.cmi
-disambiguateChoices.cmx: disambiguateChoices.cmi
-number_notation.cmo: disambiguateChoices.cmi
-number_notation.cmx: disambiguateChoices.cmx
+++ /dev/null
-PACKAGE = cic_disambiguation
-NOTATIONS = number
-INTERFACE_FILES = \
- cicDisambiguate.mli \
- disambiguateChoices.mli
-IMPLEMENTATION_FILES = \
- $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \
- $(patsubst %,%_notation.ml,$(NOTATIONS))
-
-all:
-
-clean:
-distclean:
- rm -f macro_table.dump
-
-include ../../Makefile.defs
-include ../Makefile.common
-
-OCAMLARCHIVEOPTIONS += -linkall
-
+++ /dev/null
-(*
-Copyright (C) 1999-2006, HELM Team.
-
-This file is part of HELM, an Hypertextual, Electronic
-Library of Mathematics, developed at the Computer Science
-Department, University of Bologna, Italy.
-
-HELM is free software; you can redistribute it and/or
-modify it under the terms of the GNU General Public License
-as published by the Free Software Foundation; either version 2
-of the License, or (at your option) any later version.
-
-HELM is distributed in the hope that it will be useful,
-but WITHOUT ANY WARRANTY; without even the implied warranty of
-MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-GNU General Public License for more details.
-
-You should have received a copy of the GNU General Public License
-along with this program; if not, write to the Free Software
-Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
-02110-1301 USA.
-
-For details, see the HELM web site: http://helm.cs.unibo.it/
-*)
-
-open Printf
-module Ast = CicNotationPt
-
-let debug = false
-let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
-
-let rec string_context_of_context =
- List.map
- (function
- | Cic.Name n -> Some n
- | Cic.Anonymous -> Some "_")
-;;
-
-let refine_term metasenv subst context uri ~use_coercions
- term expty ugraph ~localization_tbl =
-(* if benchmark then incr actual_refinements; *)
- assert (uri=None);
- debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
- let saved_use_coercions = !CicRefine.insert_coercions in
- try
- CicRefine.insert_coercions := use_coercions;
- let term =
- match expty with
- | None -> term
- | Some ty -> Cic.Cast(term,ty)
- in
- let term', _, metasenv',ugraph1 =
- CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl
- in
- let term' =
- match expty, term' with
- | None,_ -> term'
- | Some _,Cic.Cast (term',_) -> term'
- | _ -> assert false
- in
- CicRefine.insert_coercions := saved_use_coercions;
- (Disambiguate.Ok (term', metasenv',[],ugraph1))
- with
- exn ->
- CicRefine.insert_coercions := saved_use_coercions;
- let rec process_exn loc =
- function
- HExtlib.Localized (loc,exn) -> process_exn loc exn
- | CicRefine.Uncertain msg ->
- debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
- Disambiguate.Uncertain (lazy (loc,Lazy.force msg))
- | CicRefine.RefineFailure msg ->
- debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
- (CicPp.ppterm term) (Lazy.force msg)));
- Disambiguate.Ko (lazy (loc,Lazy.force msg))
- | exn -> raise exn
- in
- process_exn Stdpp.dummy_loc exn
-
-let refine_obj metasenv subst context uri ~use_coercions obj _ ugraph
- ~localization_tbl =
- assert (context = []);
- assert (metasenv = []);
- assert (subst = []);
- debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
- let saved_use_coercions = !CicRefine.insert_coercions in
- try
- CicRefine.insert_coercions := use_coercions;
- let obj', metasenv,ugraph =
- CicRefine.typecheck metasenv uri obj ~localization_tbl
- in
- CicRefine.insert_coercions := saved_use_coercions;
- (Disambiguate.Ok (obj', metasenv,[],ugraph))
- with
- exn ->
- CicRefine.insert_coercions := saved_use_coercions;
- let rec process_exn loc =
- function
- HExtlib.Localized (loc,exn) -> process_exn loc exn
- | CicRefine.Uncertain msg ->
- debug_print (lazy ("UNCERTAIN!!! [" ^
- (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
- Disambiguate.Uncertain (lazy (loc,Lazy.force msg))
- | CicRefine.RefineFailure msg ->
- debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
- (CicPp.ppobj obj) (Lazy.force msg))) ;
- Disambiguate.Ko (lazy (loc,Lazy.force msg))
- | exn -> raise exn
- in
- process_exn Stdpp.dummy_loc exn
-;;
-
-let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
- ~is_path ast ~localization_tbl ~obj_context
-=
- (* create_dummy_ids shouldbe used only for interpretating patterns *)
- assert (uri = None);
- let rec aux ~localize loc context = function
- | CicNotationPt.AttributedTerm (`Loc loc, term) ->
- let res = aux ~localize loc context term in
- if localize then Cic.CicHash.add localization_tbl res loc;
- res
- | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
- | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
- let cic_args = List.map (aux ~localize loc context) args in
- Disambiguate.resolve ~mk_choice ~env
- (DisambiguateTypes.Symbol (symb, i)) (`Args cic_args)
- | CicNotationPt.Appl terms ->
- Cic.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_name = CicNotationUtil.cic_name_of_name var in
- let cic_body = aux ~localize loc (cic_name :: context) body in
- (match binder_kind with
- | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
- | `Pi
- | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
- | `Exists ->
- Disambiguate.resolve ~mk_choice ~env
- (DisambiguateTypes.Symbol ("exists", 0))
- (`Args [ cic_type; Cic.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 do_branch ((head, _, args), term) =
- let rec do_branch' context = function
- | [] -> aux ~localize loc context term
- | (name, typ) :: tl ->
- let cic_name = CicNotationUtil.cic_name_of_name name in
- let cic_body = do_branch' (cic_name :: context) tl in
- let typ =
- match typ with
- | None -> Cic.Implicit (Some `Type)
- | Some typ -> aux ~localize loc context typ
- in
- Cic.Lambda (cic_name, typ, cic_body)
- 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
- match indty_ident with
- | Some (indty_ident, _) ->
- (match
- Disambiguate.resolve ~mk_choice ~env
- (DisambiguateTypes.Id indty_ident) (`Args [])
- with
- | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
- | Cic.Implicit _ ->
- raise (Disambiguate.Try_again
- (lazy "The type of the term to be matched
- is still unknown"))
- | _ ->
- raise (DisambiguateTypes.Invalid_choice (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 (DisambiguateTypes.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 Disambiguate.resolve ~mk_choice ~env
- (DisambiguateTypes.Id (fst_constructor branches))
- (`Args []) with
- | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
- (indtype_uri, indtype_no)
- | Cic.Implicit _ ->
- raise (Disambiguate.Try_again (lazy "The type of the term to be matched
- is still unknown"))
- | _ ->
- raise (DisambiguateTypes.Invalid_choice (lazy (loc,"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 (lazy (loc, "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
- Cic.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
- Cic.Prod (_, _, t) -> 1 + (count_prod t)
- | _ -> 0
- in
- let rec sort branches cl =
- match cl with
- [] ->
- let rec analyze unused unrecognized useless =
- function
- [] ->
- 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
- 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
- Cic.MutCase (indtype_uri, indtype_no, 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
- Cic.Cast (cic_t1, cic_t2)
- | CicNotationPt.LetIn ((name, typ), def, body) ->
- let cic_def = aux ~localize loc context def in
- let cic_name = CicNotationUtil.cic_name_of_name name in
- let cic_typ =
- match typ with
- | None -> Cic.Implicit (Some `Type)
- | Some t -> aux ~localize loc context t
- in
- let cic_body = aux ~localize loc (cic_name :: context) body in
- Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
- | CicNotationPt.LetRec (kind, defs, body) ->
- let context' =
- List.fold_left
- (fun acc (_, (name, _), _, _) ->
- CicNotationUtil.cic_name_of_name name :: acc)
- context defs
- in
- let cic_body =
- let unlocalized_body = aux ~localize:false loc context' body in
- match unlocalized_body with
- Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
- | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->
- (try
- let l' =
- List.map
- (function t ->
- let t',subst,metasenv =
- CicMetaSubst.delift_rels [] [] (List.length defs) t
- in
- assert (subst=[]);
- assert (metasenv=[]);
- t') l
- in
- (* We can avoid the LetIn. But maybe we need to recompute l'
- so that it is localized *)
- if localize then
- match body with
- CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
- (* since we avoid the letin, the context has no
- * recfuns in it *)
- let l' = List.map (aux ~localize loc context) l in
- `AvoidLetIn (n,l')
- | _ -> assert false
- else
- `AvoidLetIn (n,l')
- with
- CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
- if localize then
- `AddLetIn (aux ~localize loc context' body)
- else
- `AddLetIn unlocalized_body)
- | _ ->
- if localize then
- `AddLetIn (aux ~localize loc context' body)
- else
- `AddLetIn unlocalized_body
- in
- let inductiveFuns =
- List.map
- (fun (params, (name, typ), body, decr_idx) ->
- let add_binders kind t =
- List.fold_right
- (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
- in
- let cic_body =
- aux ~localize loc context' (add_binders `Lambda body) in
- let typ =
- match typ with
- Some typ -> typ
- | None-> CicNotationPt.Implicit `JustOne in
- let cic_type =
- aux_option ~localize loc context (Some `Type)
- (Some (add_binders `Pi typ)) in
- let name =
- match CicNotationUtil.cic_name_of_name name with
- | Cic.Anonymous ->
- CicNotationPt.fail loc
- "Recursive functions cannot be anonymous"
- | Cic.Name name -> name
- in
- (name, decr_idx, cic_type, cic_body))
- defs
- in
- let fix_or_cofix n =
- match kind with
- `Inductive -> Cic.Fix (n,inductiveFuns)
- | `CoInductive ->
- let coinductiveFuns =
- List.map
- (fun (name, _, typ, body) -> name, typ, body)
- inductiveFuns
- in
- Cic.CoFix (n,coinductiveFuns)
- in
- let counter = ref ~-1 in
- let build_term funs (var,_,ty,_) t =
- incr counter;
- Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
- in
- (match cic_body with
- `AvoidLetInNoAppl n ->
- let n' = List.length inductiveFuns - n in
- fix_or_cofix n'
- | `AvoidLetIn (n,l) ->
- let n' = List.length inductiveFuns - n in
- Cic.Appl (fix_or_cofix n'::l)
- | `AddLetIn cic_body ->
- List.fold_right (build_term inductiveFuns) inductiveFuns
- cic_body)
- | CicNotationPt.Ident _
- | CicNotationPt.Uri _
- | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
- | CicNotationPt.NCic _ -> assert false
- | CicNotationPt.NRef _ -> assert false
- | 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 =
- Disambiguate.find_in_context name (string_context_of_context context)
- in
- if subst <> None then
- CicNotationPt.fail loc "Explicit substitutions not allowed here";
- Cic.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
- try
- List.assoc name obj_context
- with
- Not_found ->
- Disambiguate.resolve ~mk_choice ~env
- (DisambiguateTypes.Id name) (`Args [])
- 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 (DisambiguateTypes.Invalid_choice (lazy (loc, "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, Cic.Implicit None) uris)
- in
- (try
- match cic with
- | Cic.Const (uri, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- Cic.Const (uri, mk_subst uris)
- | Cic.Var (uri, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- Cic.Var (uri, mk_subst uris)
- | Cic.MutInd (uri, i, []) ->
- (try
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- Cic.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 *)
- Cic.MutInd (uri,i,[]))
- | Cic.MutConstruct (uri, i, j, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- let uris = CicUtil.params_of_obj o in
- Cic.MutConstruct (uri, i, j, mk_subst uris)
- | Cic.Meta _ | Cic.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 (DisambiguateTypes.Invalid_choice (lazy (loc, "??? Can this happen?")))
- with
- CicEnvironment.CircularDependency _ ->
- raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
- | CicNotationPt.Implicit `Vector -> assert false
- | CicNotationPt.Implicit (`JustOne | `Tagged _) -> Cic.Implicit None
- | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
- | CicNotationPt.Num (num, i) ->
- Disambiguate.resolve ~mk_choice ~env
- (DisambiguateTypes.Num i) (`Num_arg num)
- | CicNotationPt.Meta (index, subst) ->
- let cic_subst =
- List.map
- (function
- None -> None
- | Some term -> Some (aux ~localize loc context term))
- subst
- in
- Cic.Meta (index, cic_subst)
- | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
- | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
- | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
- | CicNotationPt.Sort (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
- | CicNotationPt.Sort (`NCProp _) -> Cic.Sort (Cic.CProp (CicUniv.fresh ()))
- | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
- | CicNotationPt.Symbol (symbol, instance) ->
- Disambiguate.resolve ~mk_choice ~env
- (DisambiguateTypes.Symbol (symbol, instance)) (`Args [])
- | CicNotationPt.Variable _
- | CicNotationPt.Magic _
- | CicNotationPt.Layout _
- | CicNotationPt.Literal _ -> assert false (* god bless Bologna *)
- and aux_option ~localize loc context annotation = function
- | None -> Cic.Implicit annotation
- | Some term -> aux ~localize loc context term
- in
- aux ~localize:true HExtlib.dummy_floc context ast
-
-let interpretate_path ~context path =
- let localization_tbl = Cic.CicHash.create 23 in
- (* here we are throwing away useful localization informations!!! *)
- fst (
- interpretate_term ~mk_choice:(fun _ -> assert false) ~create_dummy_ids:true
- ~context ~env:DisambiguateTypes.Environment.empty ~uri:None ~is_path:true
- path ~localization_tbl ~obj_context:[], localization_tbl)
-
-let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj
- ~localization_tbl
-=
- assert (context = []);
- assert (is_path = false);
- let interpretate_term ?(obj_context=[]) =
- interpretate_term ~mk_choice ~localization_tbl ~obj_context in
- match obj with
- | CicNotationPt.Inductive (params,tyl) ->
- let uri = match uri with Some uri -> uri | None -> assert false in
- let context,params =
- let context,res =
- List.fold_left
- (fun (context,res) (name,t) ->
- let t =
- match t with
- None -> CicNotationPt.Implicit `JustOne
- | Some t -> t in
- let name = CicNotationUtil.cic_name_of_name name in
- name::context,(name, interpretate_term context env None false t)::res
- ) ([],[]) params
- in
- context,List.rev res in
- let add_params =
- List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
- let obj_context =
- snd (
- List.fold_left
- (*here the explicit_named_substituion is assumed to be of length 0 *)
- (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res)
- (0,[]) tyl) in
- let tyl =
- List.map
- (fun (name,b,ty,cl) ->
- let ty' = add_params (interpretate_term context env None false ty) in
- let cl' =
- List.map
- (fun (name,ty) ->
- let ty' =
- add_params
- (interpretate_term ~obj_context ~context ~env ~uri:None
- ~is_path:false ty)
- in
- name,ty'
- ) cl
- in
- name,b,ty',cl'
- ) tyl
- in
- Cic.InductiveDefinition (tyl,[],List.length params,[])
- | CicNotationPt.Record (params,name,ty,fields) ->
- let uri = match uri with Some uri -> uri | None -> assert false in
- let context,params =
- let context,res =
- List.fold_left
- (fun (context,res) (name,t) ->
- let t =
- match t with
- None -> CicNotationPt.Implicit `JustOne
- | Some t -> t in
- let name = CicNotationUtil.cic_name_of_name name in
- name::context,(name, interpretate_term context env None false t)::res
- ) ([],[]) params
- in
- context,List.rev res in
- let add_params =
- List.fold_right
- (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
- let ty' = add_params (interpretate_term context env None false ty) in
- let fields' =
- snd (
- List.fold_left
- (fun (context,res) (name,ty,_coercion,arity) ->
- let context' = Cic.Name name :: context in
- context',(name,interpretate_term context env None false ty)::res
- ) (context,[]) fields) in
- let concl =
- (*here the explicit_named_substituion is assumed to be of length 0 *)
- let mutind = Cic.MutInd (uri,0,[]) in
- if params = [] then mutind
- else
- Cic.Appl
- (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
- let con =
- List.fold_left
- (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
- concl fields' in
- let con' = add_params con in
- let tyl = [name,true,ty',["mk_" ^ name,con']] in
- let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
- Cic.InductiveDefinition
- (tyl,[],List.length params,[`Class (`Record field_names)])
- | CicNotationPt.Theorem (flavour, name, ty, bo, _pragma) ->
- let attrs = [`Flavour flavour] in
- let ty' = interpretate_term [] env None false ty in
- (match bo,flavour with
- None,`Axiom ->
- Cic.Constant (name,None,ty',[],attrs)
- | Some bo,`Axiom -> assert false
- | None,_ ->
- Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
- | Some bo,_ ->
- let bo' = Some (interpretate_term [] env None false bo) in
- Cic.Constant (name,bo',ty',[],attrs))
-;;
-
-let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
- ~is_path ast ~localization_tbl
-=
- let context =
- List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context
- in
- interpretate_term ~mk_choice ~create_dummy_ids ~context ~env ~uri ~is_path
- ast ~localization_tbl ~obj_context:[]
-;;
-
-let string_context_of_context =
- List.map (function None -> None | Some (Cic.Name n,_) -> Some n | Some
- (Cic.Anonymous,_) -> Some "_");;
-
-let disambiguate_term ~context ~metasenv ~subst ~expty
- ?(initial_ugraph = CicUniv.oblivion_ugraph)
- ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
- ~aliases ~universe ~lookup_in_library (text,prefix_len,term)
-=
- let mk_localization_tbl x = Cic.CicHash.create x in
- MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
- ~initial_ugraph ~aliases ~string_context_of_context
- ~universe ~lookup_in_library ~mk_implicit ~description_of_alias
- ~fix_instance
- ~uri:None ~pp_thing:CicNotationPp.pp_term
- ~domain_of_thing:Disambiguate.domain_of_term
- ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
- ~refine_thing:refine_term (text,prefix_len,term)
- ~mk_localization_tbl
- ~expty
- ~freshen_thing:CicNotationUtil.freshen_term
- ~passes:(MultiPassDisambiguator.passes ())
-
-let disambiguate_obj ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
- ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
-=
- let mk_localization_tbl x = Cic.CicHash.create x in
- MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
- ~aliases ~universe ~uri ~string_context_of_context
- ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
- ~domain_of_thing:Disambiguate.domain_of_obj
- ~lookup_in_library ~mk_implicit ~description_of_alias ~fix_instance
- ~initial_ugraph:CicUniv.empty_ugraph
- ~interpretate_thing:(interpretate_obj ~mk_choice)
- ~refine_thing:refine_obj
- ~mk_localization_tbl
- ~expty:None
- ~passes:(MultiPassDisambiguator.passes ())
- ~freshen_thing:CicNotationUtil.freshen_obj
- (text,prefix_len,obj)
+++ /dev/null
-(*
- *
-Copyright (C) 1999-2006, HELM Team.
-
-This file is part of HELM, an Hypertextual, Electronic
-Library of Mathematics, developed at the Computer Science
-Department, University of Bologna, Italy.
-
-HELM is free software; you can redistribute it and/or
-modify it under the terms of the GNU General Public License
-as published by the Free Software Foundation; either version 2
-of the License, or (at your option) any later version.
-
-HELM is distributed in the hope that it will be useful,
-but WITHOUT ANY WARRANTY; without even the implied warranty of
-MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-GNU General Public License for more details.
-
-You should have received a copy of the GNU General Public License
-along with this program; if not, write to the Free Software
-Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
-02110-1301 USA.
-
-For details, see the HELM web site: http://helm.cs.unibo.it/
-*)
-
-val interpretate_path :
- context:Cic.name list -> CicNotationPt.term -> Cic.term
-
-val disambiguate_term :
- context:Cic.context ->
- metasenv:Cic.metasenv ->
- subst:Cic.substitution ->
- expty:Cic.term option ->
- ?initial_ugraph:CicUniv.universe_graph ->
- mk_implicit:(bool -> 'alias) ->
- description_of_alias:('alias -> string) ->
- fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
- mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
- aliases:'alias DisambiguateTypes.Environment.t ->
- universe:'alias list DisambiguateTypes.Environment.t option ->
- lookup_in_library:(
- DisambiguateTypes.interactive_user_uri_choice_type ->
- DisambiguateTypes.input_or_locate_uri_type ->
- DisambiguateTypes.Environment.key ->
- 'alias list) ->
- CicNotationPt.term Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item * 'alias) list *
- Cic.metasenv *
- Cic.substitution *
- Cic.term*
- CicUniv.universe_graph) list *
- bool
-
-val disambiguate_obj :
- mk_implicit:(bool -> 'alias) ->
- description_of_alias:('alias -> string) ->
- fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
- mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) ->
- aliases:'alias DisambiguateTypes.Environment.t ->
- universe:'alias list DisambiguateTypes.Environment.t option ->
- lookup_in_library:(
- DisambiguateTypes.interactive_user_uri_choice_type ->
- DisambiguateTypes.input_or_locate_uri_type ->
- DisambiguateTypes.Environment.key ->
- 'alias list) ->
- uri:UriManager.uri option -> (* required only for inductive types *)
- CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input ->
- ((DisambiguateTypes.domain_item * 'alias) list *
- Cic.metasenv *
- Cic.substitution *
- Cic.obj *
- CicUniv.universe_graph) list *
- bool
+++ /dev/null
-(* Copyright (C) 2004, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-open Printf
-
-open DisambiguateTypes
-
-exception Choice_not_found of string Lazy.t
-
-let num_choices = ref []
-let nnum_choices = ref []
-
-let add_num_choice choice = num_choices := choice :: !num_choices
-let nadd_num_choice choice = nnum_choices := choice :: !nnum_choices
-
-let has_description dsc = (fun x -> fst x = dsc)
-
-let lookup_num_choices () = !num_choices
-
-let lookup_num_by_dsc dsc =
- try
- List.find (has_description dsc) !num_choices
- with Not_found -> raise (Choice_not_found (lazy ("Num with dsc " ^ dsc)))
-
-let nlookup_num_by_dsc dsc =
- try
- List.find (has_description dsc) !nnum_choices
- with Not_found -> raise (Choice_not_found (lazy ("Num with dsc " ^ dsc)))
-
-let mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref (dsc, args, appl_pattern)=
- dsc,
- `Sym_interp
- (fun cic_args ->
- let env',rest =
- let names =
- List.map (function CicNotationPt.IdentArg (_, name) -> name) args
- in
- let rec combine_with_rest l1 l2 =
- match l1,l2 with
- _::_,[] -> raise (Invalid_argument "combine_with_rest")
- | [],rest -> [],rest
- | he1::tl1,he2::tl2 ->
- let l,rest = combine_with_rest tl1 tl2 in
- (he1,he2)::l,rest
- in
- try
- combine_with_rest names cic_args
- with Invalid_argument _ ->
- raise (Invalid_choice (lazy (Stdpp.dummy_loc,
- "The notation " ^ dsc ^ " expects more arguments")))
- in
- let combined =
- TermAcicContent.instantiate_appl_pattern
- ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env' appl_pattern
- in
- match rest with
- [] -> combined
- | _::_ -> mk_appl (combined::rest))
-
-let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref symbol dsc =
- let interpretations = TermAcicContent.lookup_interpretations ~sorted:false symbol in
- try
- mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref
- (List.find (fun (dsc', _, _) -> dsc = dsc') interpretations)
- with TermAcicContent.Interpretation_not_found | Not_found ->
- raise (Choice_not_found (lazy (sprintf "Symbol %s, dsc %s" symbol dsc)))
-
-let cic_lookup_symbol_by_dsc = lookup_symbol_by_dsc
- ~mk_implicit:(function
- | true -> Cic.Implicit (Some `Type)
- | false -> Cic.Implicit None)
- ~mk_appl:(function (Cic.Appl l)::tl -> Cic.Appl (l@tl) | l -> Cic.Appl l)
- ~term_of_uri:CicUtil.term_of_uri ~term_of_nref:(fun _ -> assert false)
-;;
+++ /dev/null
-(* Copyright (C) 2004, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-open DisambiguateTypes
-
-(** {2 Choice registration low-level interface} *)
-
- (** raised by lookup_XXXX below *)
-exception Choice_not_found of string Lazy.t
-
- (** register a new number choice *)
-val add_num_choice: Cic.term codomain_item -> unit
-
- (** register a new number choice *)
-val nadd_num_choice: NCic.term codomain_item -> unit
-
-(** {2 Choices lookup}
- * for user defined aliases *)
-
-val lookup_num_choices: unit -> Cic.term codomain_item list
-
- (** @param dsc description (1st component of codomain_item) *)
-val lookup_num_by_dsc: string -> Cic.term codomain_item
-
- (** @param dsc description (1st component of codomain_item) *)
-val nlookup_num_by_dsc: string -> NCic.term codomain_item
-
- (** @param symbol symbol as per AST
- * @param dsc description (1st component of codomain_item)
- *)
-val lookup_symbol_by_dsc:
- mk_appl: ('term list -> 'term) ->
- mk_implicit: (bool -> 'term) ->
- term_of_uri: (UriManager.uri -> 'term) ->
- term_of_nref: (NReference.reference -> 'term) ->
- string -> string -> 'term codomain_item
-
-val cic_lookup_symbol_by_dsc:
- string -> string -> Cic.term codomain_item
-
-val mk_choice:
- mk_appl: ('term list -> 'term) ->
- mk_implicit: (bool -> 'term) ->
- term_of_uri: (UriManager.uri -> 'term) ->
- term_of_nref: (NReference.reference -> 'term) ->
- string * CicNotationPt.argument_pattern list *
- CicNotationPt.cic_appl_pattern ->
- 'term codomain_item
-
+++ /dev/null
-
-Input Should be parsed as Derived constraint
- on precedence
---------------------------------------------------------------------------------
-\lambda x.x y \lambda x.(x y) lambda > apply
-S x = y (= (S x) y) apply > infix operators
-\forall x.x=x (\forall x.(= x x)) infix operators > binders
-\lambda x.x \to x \lambda. (x \to x) \to > \lambda
---------------------------------------------------------------------------------
-
-Precedence total order:
-
- apply > infix operators > to > binders
-
-where binders are all binders except lambda (i.e. \forall, \pi, \exists)
-
-to test:
-
-./test_parser term << EOT
- \lambda x.x y
- S x = y
- \forall x.x=x
- \lambda x.x \to x
-EOT
-
-should respond with:
-
- \lambda x.(x y)
- (eq (S x) y)
- \forall x.(eq x x)
- \lambda x.(x \to x)
-
+++ /dev/null
-(* Copyright (C) 2004, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-module C = Cic
-module Obj = LibraryObjects
-module DT = DisambiguateTypes
-
-let error msg =
- raise (DT.Invalid_choice (lazy (Stdpp.dummy_loc, msg)))
-
-let build_nat o s str =
- let n = int_of_string str in
- if n < 0 then error (str ^ " is not a valid natural number number") else
- let rec aux n = if n = 0 then o () else s (aux (pred n)) in
- aux n
-
-let interp_natural_number num =
- let nat_URI = match Obj.nat_URI () with
- | Some uri -> uri
- | None -> error "no default natural numbers"
- in
- let o () = C.MutConstruct (nat_URI,0,1,[]) in
- let s t = C.Appl [C.MutConstruct (nat_URI,0,2,[]); t] in
- build_nat o s num
-
-let _ =
- DisambiguateChoices.add_num_choice
- ("natural number", `Num_interp interp_natural_number);
- DisambiguateChoices.add_num_choice
- ("Coq natural number",
- `Num_interp (fun num -> HelmLibraryObjects.build_nat (int_of_string num)));
- DisambiguateChoices.add_num_choice
- ("real number",
- `Num_interp (fun num -> HelmLibraryObjects.build_real (int_of_string num)));
- DisambiguateChoices.add_num_choice
- ("binary positive number",
- `Num_interp (fun num ->
- let num = int_of_string num in
- if num = 0 then
- error "0 is not a valid positive number"
- else
- HelmLibraryObjects.build_bin_pos num));
- DisambiguateChoices.add_num_choice
- ("binary integer number",
- `Num_interp (fun num ->
- let num = int_of_string num in
- if num = 0 then
- HelmLibraryObjects.BinInt.z0
- else if num > 0 then
- Cic.Appl [
- HelmLibraryObjects.BinInt.zpos;
- HelmLibraryObjects.build_bin_pos num ]
- else
- assert false))
+++ /dev/null
-alias id foo = cic:/a.con
-alias id bar = cic:/b.con
-alias symbol "plus" (instance 0) = "real plus"
-alias symbol "plus" (instance 1) = "natural plus"
-alias num (instance 0) = "real number"
-alias num (instance 1) = "natural number"
+++ /dev/null
-\forall n. \forall m. n + m = n
+++ /dev/null
-[\lambda x:nat.
- [\lambda y:nat. Set]
- match x:nat with [ O \Rightarrow nat | (S x) \Rightarrow bool ]]
-match (S O):nat with
-[ O \Rightarrow O
-| (S x) \Rightarrow false ]
-
-[\lambda z:nat. \lambda h:(le O z). (eq nat O O)]
-match (le_n O): le with
-[ le_n \Rightarrow (refl_equal nat O)
-| (le_S x y) \Rightarrow (refl_equal nat O) ]
-
-[\lambda z:nat. \lambda h:(le (plus (plus O O) (plus O O)) z). (eq nat (plus (plus O O) (plus O O)) (plus (plus O O) (plus O O)))]
-match (le_n (plus (plus O O) (plus O O))): le with
-[ le_n \Rightarrow (refl_equal nat (plus (plus O O) (plus O O)))
-| (le_S x y) \Rightarrow (refl_equal nat (plus (plus O O) (plus O O))) ]
-
-(*
-[\lambda z:nat. \lambda h:(le 1 z). (le 0 z)]
-match (le_S 2 (le_n 1)): le with
-[ le_n \Rightarrow (le_S 1 (le_n 0))
-| (le_S x y) \Rightarrow y ]
-*)
-
-[\lambda z:nat. \lambda h:(le 0 z). (le 0 (S z))]
-match (le_S 0 0 (le_n 0)): le with
-[ le_n \Rightarrow (le_S 0 0 (le_n 0))
-| (le_S x y) \Rightarrow (le_S 0 (S x) (le_S 0 x y)) ]
-
-
-[\lambda x:bool. nat]
-match true:bool with
-[ true \Rightarrow O
-| false \Rightarrow (S O) ]
-
-[\lambda x:nat. nat]
-match O:nat with
-[ O \Rightarrow O
-| (S x) \Rightarrow (S (S x)) ]
-
-[\lambda x:list. list]
-match nil:list with
-[ nil \Rightarrow nil
-| (cons x y) \Rightarrow (cons x y) ]
-
-\lambda x:False.
- [\lambda h:False. True]
- match x:False with []
-
status, `Old [] (*CSC: TO BE FIXED *)
| GrafiteAst.Set (loc, name, value) -> status, `Old []
(* GrafiteTypes.set_option status name value,[] *)
- | GrafiteAst.Obj (loc,obj) ->
- let ext,name =
- match obj with
- Cic.Constant (name,_,_,_,_)
- | Cic.CurrentProof (name,_,_,_,_,_) -> ".con",name
- | Cic.InductiveDefinition (types,_,_,_) ->
- ".ind",
- (match types with (name,_,_,_)::_ -> name | _ -> assert false)
- | _ -> assert false in
- let buri = status#baseuri in
- let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ext) in
- let obj = CicRefine.pack_coercion_obj obj in
- let metasenv = GrafiteTypes.get_proof_metasenv status in
- match obj with
- | Cic.CurrentProof (_,metasenv',bo,ty,_, attrs) ->
- let name = UriManager.name_of_uri uri in
- if not(CicPp.check name ty) then
- HLog.warn ("Bad name: " ^ name);
- if opts.do_heavy_checks then
- begin
- let dbd = LibraryDb.instance () in
- let similar = Whelp.match_term ~dbd ty in
- let similar_len = List.length similar in
- if similar_len> 30 then
- (HLog.message
- ("Duplicate check will compare your theorem with " ^
- string_of_int similar_len ^
- " theorems, this may take a while."));
- let convertible =
- List.filter (
- fun u ->
- let t = CicUtil.term_of_uri u in
- let ty',g =
- CicTypeChecker.type_of_aux'
- metasenv' [] t CicUniv.oblivion_ugraph
- in
- fst(CicReduction.are_convertible [] ty' ty g))
- similar
- in
- (match convertible with
- | [] -> ()
- | x::_ ->
- HLog.warn
- ("Theorem already proved: " ^ UriManager.string_of_uri x ^
- "\nPlease use a variant."));
- end;
- let _subst = [] in
- let initial_proof = (Some uri, metasenv', _subst, lazy bo, ty, attrs) in
- let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
- status#set_proof_status
- (GrafiteTypes.Incomplete_proof
- { GrafiteTypes.proof = initial_proof; stack = initial_stack }),
- `Old []
- | _ ->
- if metasenv <> [] then
- raise (GrafiteTypes.Command_error (
- "metasenv not empty while giving a definition with body: " ^
- CicMetaSubst.ppmetasenv [] metasenv));
- let status, lemmas = add_obj uri obj status in
- let status,new_lemmas = add_coercions_of_lemmas lemmas status in
- status#set_proof_status GrafiteTypes.No_proof,
- `Old (uri::new_lemmas@lemmas)
+ | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false
in
match status#proof_status with
GrafiteTypes.Intermediate _ ->
let __Implicit = "__Implicit__"
let __Closed_Implicit = "__Closed_Implicit__"
-let cic_mk_choice = function
- | LexiconAst.Symbol_alias (name, _, dsc) ->
- if name = __Implicit then
- dsc, `Sym_interp (fun _ -> Cic.Implicit None)
- else if name = __Closed_Implicit then
- dsc, `Sym_interp (fun _ -> Cic.Implicit (Some `Closed))
- else
- DisambiguateChoices.cic_lookup_symbol_by_dsc name dsc
- | LexiconAst.Number_alias (_, dsc) ->
- DisambiguateChoices.lookup_num_by_dsc dsc
- | LexiconAst.Ident_alias (name, uri) ->
- uri, `Sym_interp
- (fun l->assert(l = []);CicUtil.term_of_uri (UriManager.uri_of_string uri))
-;;
-
let ncic_mk_choice = function
| LexiconAst.Symbol_alias (name, _, dsc) ->
if name = __Implicit then
| false -> NCic.Implicit `Term)
~mk_appl:(function
(NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
- ~term_of_uri:(fun uri ->
- fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+ ~term_of_uri:(fun _ -> assert false)
~term_of_nref:(fun nref -> NCic.Const nref)
name dsc
| LexiconAst.Number_alias (_, dsc) ->
- (try
- let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
- desc, `Num_interp
- (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
- with
- DisambiguateChoices.Choice_not_found _ ->
- let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in
- desc, `Num_interp
- (fun num ->
- fst (OCic2NCic.convert_term
- (UriManager.uri_of_string "cic:/xxx/x.con")
- (match f with `Num_interp f -> f num | _ -> assert false))))
+ let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in
+ desc, `Num_interp
+ (fun num -> match f with `Num_interp f -> f num | _ -> assert false)
| LexiconAst.Ident_alias (name, uri) ->
uri, `Sym_interp
(fun l->assert(l = []);
LexiconAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
;;
-let lookup_in_library
- interactive_user_uri_choice input_or_locate_uri item
-=
- let mk_ident_alias id u =
- LexiconAst.Ident_alias (id,UriManager.string_of_uri u)
- in
- let mk_num_alias instance =
- List.map
- (fun dsc,_ -> LexiconAst.Number_alias (instance,dsc))
- (DisambiguateChoices.lookup_num_choices())
- in
- let mk_symbol_alias symb ino (dsc, _,_) =
- LexiconAst.Symbol_alias (symb,ino,dsc)
- in
- let dbd = LibraryDb.instance () in
- let choices_of_id id =
- let uris = Whelp.locate ~dbd id in
- match uris with
- | [] ->
- (match
- (input_or_locate_uri
- ~title:("URI matching \"" ^ id ^ "\" unknown.")
- ?id:(Some id) ())
- with
- | None -> []
- | Some uri -> [uri])
- | [uri] -> [uri]
- | _ ->
- interactive_user_uri_choice ~selection_mode:`MULTIPLE
- ?ok:(Some "Try selected.")
- ?enable_button_for_non_vars:(Some true)
- ~title:"Ambiguous input."
- ~msg: ("Ambiguous input \"" ^ id ^
- "\". Please, choose one or more interpretations:")
- ~id
- uris
- in
- match item with
- | DisambiguateTypes.Id id ->
- let uris = choices_of_id id in
- List.map (mk_ident_alias id) uris
- | DisambiguateTypes.Symbol (symb, ino) ->
- (try
- List.map (mk_symbol_alias symb ino)
- (TermAcicContent.lookup_interpretations symb)
- with
- TermAcicContent.Interpretation_not_found -> [])
- | DisambiguateTypes.Num instance -> mk_num_alias instance
-;;
-
let nlookup_in_library
interactive_user_uri_choice input_or_locate_uri item
=
let references = NCicLibrary.resolve id in
List.map
(fun u -> LexiconAst.Ident_alias (id,NReference.string_of_reference u)
- ) references @
- lookup_in_library interactive_user_uri_choice input_or_locate_uri item
+ ) references
with
- NCicEnvironment.ObjectNotFound _ ->
- lookup_in_library interactive_user_uri_choice input_or_locate_uri item)
- | _ -> lookup_in_library interactive_user_uri_choice input_or_locate_uri item
+ NCicEnvironment.ObjectNotFound _ -> [])
+ | _ -> []
;;
let fix_instance item l =
;;
- (** @param term not meaningful when context is given *)
-let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv
-term =
- let lexicon_status = !lexicon_status_ref in
- let (diff, metasenv, subst, cic, _) =
- singleton "first"
- (CicDisambiguate.disambiguate_term
- ~aliases:lexicon_status#lstatus.LexiconEngine.aliases
- ~expty ~universe:(Some lexicon_status#lstatus.LexiconEngine.multi_aliases)
- ~lookup_in_library
- ~mk_choice:cic_mk_choice
- ~mk_implicit ~fix_instance
- ~description_of_alias:LexiconAst.description_of_alias
- ~context ~metasenv ~subst:[] (text,prefix_len,term))
- in
- let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
- lexicon_status_ref := lexicon_status;
- metasenv,(*subst,*) cic
-;;
-
let disambiguate_nterm expty estatus context metasenv subst thing
=
let diff, metasenv, subst, cic =
;;
- (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
- * rationale: lazy_term will be invoked in different context to obtain a term,
- * each invocation will disambiguate the term and can add aliases. Once all
- * disambiguations have been performed, the first returned function can be
- * used to obtain the resulting aliases *)
-let disambiguate_lazy_term expty text prefix_len lexicon_status_ref term =
- (fun context metasenv ugraph ->
- let lexicon_status = !lexicon_status_ref in
- let (diff, metasenv, _, cic, ugraph) =
- singleton "second"
- (CicDisambiguate.disambiguate_term
- ~lookup_in_library
- ~mk_choice:cic_mk_choice
- ~mk_implicit ~fix_instance
- ~description_of_alias:LexiconAst.description_of_alias
- ~initial_ugraph:ugraph ~aliases:lexicon_status#lstatus.LexiconEngine.aliases
- ~universe:(Some lexicon_status#lstatus.LexiconEngine.multi_aliases)
- ~context ~metasenv ~subst:[]
- (text,prefix_len,term) ~expty) in
- let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
- lexicon_status_ref := lexicon_status;
- cic, metasenv, ugraph)
-;;
-
-let disambiguate_pattern
- text prefix_len lexicon_status_ref (wanted, hyp_paths, goal_path)
-=
- let interp path =CicDisambiguate.interpretate_path [] path in
- let goal_path = HExtlib.map_option interp goal_path in
- let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
- let wanted =
- match wanted with
- None -> None
- | Some wanted ->
- let wanted =
- disambiguate_lazy_term None text prefix_len lexicon_status_ref wanted
- in
- Some wanted
- in
- (wanted, hyp_paths, goal_path)
-;;
-
type pattern =
CicNotationPt.term Disambiguate.disambiguator_input option *
(string * NCic.term) list * NCic.term option
;;
let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
- | `Unfold (Some t) ->
- let t =
- disambiguate_lazy_term None text prefix_len lexicon_status_ref t in
- `Unfold (Some t)
+ | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
| `Normalize
| `Simpl
| `Unfold None
metasenv, `Auto params
;;
-let rec disambiguate_tactic
- lexicon_status_ref context metasenv goal (text,prefix_len,tactic)
-=
- let disambiguate_term_hint =
- let _,_,expty =
- List.find (fun (x,_,_) -> Some x = goal) metasenv
- in
- disambiguate_term (Some expty) text prefix_len lexicon_status_ref in
- let disambiguate_term =
- disambiguate_term None text prefix_len lexicon_status_ref in
- let disambiguate_pattern =
- disambiguate_pattern text prefix_len lexicon_status_ref in
- let disambiguate_reduction_kind =
- disambiguate_reduction_kind text prefix_len lexicon_status_ref in
- let disambiguate_lazy_term =
- disambiguate_lazy_term None text prefix_len lexicon_status_ref in
- let disambiguate_tactic metasenv tac =
- disambiguate_tactic lexicon_status_ref context metasenv goal (text,prefix_len,tac)
- in
- let disambiguate_auto_params m p =
- disambiguate_auto_params disambiguate_term m context p
- in
- match tactic with
- (* Higher order tactics *)
- | GrafiteAst.Progress (loc,tac) ->
- let metasenv,tac = disambiguate_tactic metasenv tac in
- metasenv,GrafiteAst.Progress (loc,tac)
- | GrafiteAst.Solve (loc,tacl) ->
- let metasenv,tacl =
- List.fold_right
- (fun tac (metasenv,tacl) ->
- let metasenv,tac = disambiguate_tactic metasenv tac in
- metasenv,tac::tacl
- ) tacl (metasenv,[])
- in
- metasenv,GrafiteAst.Solve (loc,tacl)
- | GrafiteAst.Try (loc,tac) ->
- let metasenv,tac = disambiguate_tactic metasenv tac in
- metasenv,GrafiteAst.Try (loc,tac)
- | GrafiteAst.First (loc,tacl) ->
- let metasenv,tacl =
- List.fold_right
- (fun tac (metasenv,tacl) ->
- let metasenv,tac = disambiguate_tactic metasenv tac in
- metasenv,tac::tacl
- ) tacl (metasenv,[])
- in
- metasenv,GrafiteAst.First (loc,tacl)
- | GrafiteAst.Seq (loc,tacl) ->
- let metasenv,tacl =
- List.fold_right
- (fun tac (metasenv,tacl) ->
- let metasenv,tac = disambiguate_tactic metasenv tac in
- metasenv,tac::tacl
- ) tacl (metasenv,[])
- in
- metasenv,GrafiteAst.Seq (loc,tacl)
- | GrafiteAst.Repeat (loc,tac) ->
- let metasenv,tac = disambiguate_tactic metasenv tac in
- metasenv,GrafiteAst.Repeat (loc,tac)
- | GrafiteAst.Do (loc,n,tac) ->
- let metasenv,tac = disambiguate_tactic metasenv tac in
- metasenv,GrafiteAst.Do (loc,n,tac)
- | GrafiteAst.Then (loc,tac,tacl) ->
- let metasenv,tac = disambiguate_tactic metasenv tac in
- let metasenv,tacl =
- List.fold_right
- (fun tac (metasenv,tacl) ->
- let metasenv,tac = disambiguate_tactic metasenv tac in
- metasenv,tac::tacl
- ) tacl (metasenv,[])
- in
- metasenv,GrafiteAst.Then (loc,tac,tacl)
- (* First order tactics *)
- | GrafiteAst.Absurd (loc, term) ->
- let metasenv,cic = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.Absurd (loc, cic)
- | GrafiteAst.Apply (loc, term) ->
- let metasenv,cic = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.Apply (loc, cic)
- | GrafiteAst.ApplyRule (loc, term) ->
- let metasenv,cic = disambiguate_term_hint context metasenv term in
- metasenv,GrafiteAst.ApplyRule (loc, cic)
- | GrafiteAst.ApplyP (loc, term) ->
- let metasenv,cic = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.ApplyP (loc, cic)
- | GrafiteAst.ApplyS (loc, term, params) ->
- let metasenv, params = disambiguate_auto_params metasenv params in
- let metasenv,cic = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.ApplyS (loc, cic, params)
- | GrafiteAst.Assumption loc ->
- metasenv,GrafiteAst.Assumption loc
- | GrafiteAst.AutoBatch (loc,params) ->
- let metasenv, params = disambiguate_auto_params metasenv params in
- metasenv,GrafiteAst.AutoBatch (loc,params)
- | GrafiteAst.Cases (loc, what, pattern, idents) ->
- let metasenv,what = disambiguate_term context metasenv what in
- let pattern = disambiguate_pattern pattern in
- metasenv,GrafiteAst.Cases (loc, what, pattern, idents)
- | GrafiteAst.Change (loc, pattern, with_what) ->
- let with_what = disambiguate_lazy_term with_what in
- let pattern = disambiguate_pattern pattern in
- metasenv,GrafiteAst.Change (loc, pattern, with_what)
- | GrafiteAst.Clear (loc,id) ->
- metasenv,GrafiteAst.Clear (loc,id)
- | GrafiteAst.ClearBody (loc,id) ->
- metasenv,GrafiteAst.ClearBody (loc,id)
- | GrafiteAst.Compose (loc, t1, t2, times, spec) ->
- let metasenv,t1 = disambiguate_term context metasenv t1 in
- let metasenv,t2 =
- match t2 with
- | None -> metasenv, None
- | Some t2 ->
- let m, t2 = disambiguate_term context metasenv t2 in
- m, Some t2
- in
- metasenv, GrafiteAst.Compose (loc, t1, t2, times, spec)
- | GrafiteAst.Constructor (loc,n) ->
- metasenv,GrafiteAst.Constructor (loc,n)
- | GrafiteAst.Contradiction loc ->
- metasenv,GrafiteAst.Contradiction loc
- | GrafiteAst.Cut (loc, ident, term) ->
- let metasenv,cic = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.Cut (loc, ident, cic)
- | GrafiteAst.Decompose (loc, names) ->
- metasenv,GrafiteAst.Decompose (loc, names)
- | GrafiteAst.Demodulate (loc, params) ->
- let metasenv, params = disambiguate_auto_params metasenv params in
- metasenv,GrafiteAst.Demodulate (loc, params)
- | GrafiteAst.Destruct (loc, Some terms) ->
- let map term (metasenv, terms) =
- let metasenv, term = disambiguate_term context metasenv term in
- metasenv, term :: terms
- in
- let metasenv, terms = List.fold_right map terms (metasenv, []) in
- metasenv, GrafiteAst.Destruct(loc, Some terms)
- | GrafiteAst.Destruct (loc, None) ->
- metasenv,GrafiteAst.Destruct(loc,None)
- | GrafiteAst.Exact (loc, term) ->
- let metasenv,cic = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.Exact (loc, cic)
- | GrafiteAst.Elim (loc, what, Some using, pattern, specs) ->
- let metasenv,what = disambiguate_term context metasenv what in
- let metasenv,using = disambiguate_term context metasenv using in
- let pattern = disambiguate_pattern pattern in
- metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, specs)
- | GrafiteAst.Elim (loc, what, None, pattern, specs) ->
- let metasenv,what = disambiguate_term context metasenv what in
- let pattern = disambiguate_pattern pattern in
- metasenv,GrafiteAst.Elim (loc, what, None, pattern, specs)
- | GrafiteAst.ElimType (loc, what, Some using, specs) ->
- let metasenv,what = disambiguate_term context metasenv what in
- let metasenv,using = disambiguate_term context metasenv using in
- metasenv,GrafiteAst.ElimType (loc, what, Some using, specs)
- | GrafiteAst.ElimType (loc, what, None, specs) ->
- let metasenv,what = disambiguate_term context metasenv what in
- metasenv,GrafiteAst.ElimType (loc, what, None, specs)
- | GrafiteAst.Exists loc ->
- metasenv,GrafiteAst.Exists loc
- | GrafiteAst.Fail loc ->
- metasenv,GrafiteAst.Fail loc
- | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
- let pattern = disambiguate_pattern pattern in
- let term = disambiguate_lazy_term term in
- let red_kind = disambiguate_reduction_kind red_kind in
- metasenv,GrafiteAst.Fold (loc, red_kind, term, pattern)
- | GrafiteAst.FwdSimpl (loc, hyp, names) ->
- metasenv,GrafiteAst.FwdSimpl (loc, hyp, names)
- | GrafiteAst.Fourier loc ->
- metasenv,GrafiteAst.Fourier loc
- | GrafiteAst.Generalize (loc,pattern,ident) ->
- let pattern = disambiguate_pattern pattern in
- metasenv,GrafiteAst.Generalize (loc,pattern,ident)
- | GrafiteAst.IdTac loc ->
- metasenv,GrafiteAst.IdTac loc
- | GrafiteAst.Intros (loc, specs) ->
- metasenv,GrafiteAst.Intros (loc, specs)
- | GrafiteAst.Inversion (loc, term) ->
- let metasenv,term = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.Inversion (loc, term)
- | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
- let f term (metasenv, to_what) =
- let metasenv, term = disambiguate_term context metasenv term in
- metasenv, term :: to_what
- in
- let metasenv, to_what = List.fold_right f to_what (metasenv, []) in
- let metasenv, what = disambiguate_term context metasenv what in
- metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
- | GrafiteAst.Left loc ->
- metasenv,GrafiteAst.Left loc
- | GrafiteAst.LetIn (loc, term, name) ->
- let metasenv,term = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.LetIn (loc,term,name)
- | GrafiteAst.Reduce (loc, red_kind, pattern) ->
- let pattern = disambiguate_pattern pattern in
- let red_kind = disambiguate_reduction_kind red_kind in
- metasenv,GrafiteAst.Reduce(loc, red_kind, pattern)
- | GrafiteAst.Reflexivity loc ->
- metasenv,GrafiteAst.Reflexivity loc
- | GrafiteAst.Replace (loc, pattern, with_what) ->
- let pattern = disambiguate_pattern pattern in
- let with_what = disambiguate_lazy_term with_what in
- metasenv,GrafiteAst.Replace (loc, pattern, with_what)
- | GrafiteAst.Rewrite (loc, dir, t, pattern, names) ->
- let metasenv,term = disambiguate_term context metasenv t in
- let pattern = disambiguate_pattern pattern in
- metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern, names)
- | GrafiteAst.Right loc ->
- metasenv,GrafiteAst.Right loc
- | GrafiteAst.Ring loc ->
- metasenv,GrafiteAst.Ring loc
- | GrafiteAst.Split loc ->
- metasenv,GrafiteAst.Split loc
- | GrafiteAst.Symmetry loc ->
- metasenv,GrafiteAst.Symmetry loc
- | GrafiteAst.Transitivity (loc, term) ->
- let metasenv,cic = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.Transitivity (loc, cic)
- (* Nuovi casi *)
- | GrafiteAst.Assume (loc, id, term) ->
- let metasenv,cic = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.Assume (loc, id, cic)
- | GrafiteAst.Suppose (loc, term, id, term') ->
- let metasenv,cic = disambiguate_term context metasenv term in
- let metasenv,cic' =
- match term' with
- None -> metasenv,None
- | Some t ->
- let metasenv,t = disambiguate_term context metasenv t in
- metasenv,Some t in
- metasenv,GrafiteAst.Suppose (loc, cic, id, cic')
- | GrafiteAst.Bydone (loc,just) ->
- let metasenv,just =
- disambiguate_just disambiguate_term context metasenv just
- in
- metasenv,GrafiteAst.Bydone (loc, just)
- | GrafiteAst.We_need_to_prove (loc,term,id,term') ->
- let metasenv,cic = disambiguate_term context metasenv term in
- let metasenv,cic' =
- match term' with
- None -> metasenv,None
- | Some t ->
- let metasenv,t = disambiguate_term context metasenv t in
- metasenv,Some t in
- metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic')
- | GrafiteAst.By_just_we_proved (loc,just,term',id,term'') ->
- let metasenv,just =
- disambiguate_just disambiguate_term context metasenv just in
- let metasenv,cic' = disambiguate_term context metasenv term' in
- let metasenv,cic'' =
- match term'' with
- None -> metasenv,None
- | Some t ->
- let metasenv,t = disambiguate_term context metasenv t in
- metasenv,Some t in
- metasenv,GrafiteAst.By_just_we_proved (loc,just,cic',id,cic'')
- | GrafiteAst.We_proceed_by_cases_on (loc, term, term') ->
- let metasenv,cic = disambiguate_term context metasenv term in
- let metasenv,cic' = disambiguate_term context metasenv term' in
- metasenv,GrafiteAst.We_proceed_by_cases_on (loc, cic, cic')
- | GrafiteAst.We_proceed_by_induction_on (loc, term, term') ->
- let metasenv,cic = disambiguate_term context metasenv term in
- let metasenv,cic' = disambiguate_term context metasenv term' in
- metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic')
- | GrafiteAst.Byinduction (loc, term, id) ->
- let metasenv,cic = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.Byinduction(loc, cic, id)
- | GrafiteAst.Thesisbecomes (loc, term) ->
- let metasenv,cic = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.Thesisbecomes (loc, cic)
- | GrafiteAst.ExistsElim (loc, just, id1, term1, id2, term2) ->
- let metasenv,just =
- disambiguate_just disambiguate_term context metasenv just in
- let metasenv,cic' = disambiguate_term context metasenv term1 in
- let cic''= disambiguate_lazy_term term2 in
- metasenv,GrafiteAst.ExistsElim(loc, just, id1, cic', id2, cic'')
- | GrafiteAst.AndElim (loc, just, id, term1, id1, term2) ->
- let metasenv,just =
- disambiguate_just disambiguate_term context metasenv just in
- let metasenv,cic'= disambiguate_term context metasenv term1 in
- let metasenv,cic''= disambiguate_term context metasenv term2 in
- metasenv,GrafiteAst.AndElim(loc, just, id, cic', id1, cic'')
- | GrafiteAst.Case (loc, id, params) ->
- let metasenv,params' =
- List.fold_right
- (fun (id,term) (metasenv,params) ->
- let metasenv,cic = disambiguate_term context metasenv term in
- metasenv,(id,cic)::params
- ) params (metasenv,[])
- in
- metasenv,GrafiteAst.Case(loc, id, params')
- | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) ->
- let metasenv,cic =
- match term1 with
- None -> metasenv,None
- | Some (start,t) ->
- let metasenv,t = disambiguate_term context metasenv t in
- metasenv,Some (start,t) in
- let metasenv,cic'= disambiguate_term context metasenv term2 in
- let metasenv,cic'' =
- match term3 with
- | `SolveWith term ->
- let metasenv,term = disambiguate_term context metasenv term in
- metasenv, `SolveWith term
- | `Auto params ->
- let metasenv, params = disambiguate_auto_params metasenv params in
- metasenv,`Auto params
- | `Term t ->
- let metasenv,t = disambiguate_term context metasenv t in
- metasenv,`Term t
- | `Proof as t -> metasenv,t in
- metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)
-
-let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
- let uri =
- let baseuri =
- match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
- in
- let name =
- match obj with
- | CicNotationPt.Inductive (_,(name,_,_,_)::_)
- | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
- | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
- | CicNotationPt.Inductive _ -> assert false
- in
- UriManager.uri_of_string (baseuri ^ "/" ^ name)
- in
-(*
- let _try_new cic =
- (NCicLibrary.clear_cache ();
- NCicEnvironment.invalidate ();
- OCic2NCic.clear ();
- let graph =
- match cic with
- | Some (Cic.CurrentProof (_,metasenv, _, ty,_,_)) ->
- let _, ugraph =
- CicTypeChecker.type_of_aux' metasenv [] ty CicUniv.empty_ugraph
- in
- ugraph
- | Some (Cic.Constant (_,_, ty,_,_)) ->
- let _, ugraph =
- CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph
- in
- ugraph
- | _ -> CicUniv.empty_ugraph
- in
-
-(*
- prerr_endline "PRIMA COERCIONS";
- let _,l = CicUniv.do_rank graph in
- List.iter (fun k ->
- prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int
- (CicUniv.get_rank k))) l;
-*)
-
- let graph =
- List.fold_left
- (fun graph (_,_,l) ->
- List.fold_left
- (fun graph (uri,_,_) ->
- let _,g = CicTypeChecker.typecheck uri in
- CicUniv.merge_ugraphs ~base_ugraph:graph ~increment:(g,uri))
- graph l)
- graph (CoercDb.to_list (CoercDb.dump ()))
- in
- ignore(CicUniv.do_rank graph);
-
-
-(*
- prerr_endline "DOPO COERCIONS";
- let _,l = CicUniv.do_rank graph in
- List.iter (fun k ->
- prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int
- (CicUniv.get_rank k))) l;
-*)
-
-
- prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE";
- let time = Unix.gettimeofday () in
- (try
- (match
- NCicDisambiguate.disambiguate_obj
- ~rdb:estatus
- ~lookup_in_library:nlookup_in_library
- ~description_of_alias:LexiconAst.description_of_alias
- ~mk_choice:ncic_mk_choice
- ~mk_implicit
- ~uri:(OCic2NCic.nuri_of_ouri uri)
- ~aliases:estatus#lstatus.LexiconEngine.aliases
- ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
- (text,prefix_len,obj)
- with
- | [_,_,_,obj],_ ->
- let time = Unix.gettimeofday () -. time in
-(* NCicTypeChecker.typecheck_obj obj; *)
- prerr_endline ("NUOVA DISAMBIGUAZIONE OK: "^ string_of_float time);
-(*
- let obj =
- let u,i,m,_,o = obj in
- u,i,m,[],o
- in
-*)
- prerr_endline (NCicPp.ppobj obj)
- | _ ->
- prerr_endline ("NUOVA DISAMBIGUAZIONE AMBIGUO!!!!!!!!! "))
- with
- | MultiPassDisambiguator.DisambiguationError (_,s) ->
- prerr_endline ("ERRORE NUOVA DISAMBIGUAZIONE ("
- ^UriManager.string_of_uri uri^
- "):\n" ^
- String.concat "\n"
- (List.map (fun _,_,x,_ -> snd (Lazy.force x)) (List.flatten s)))
-(* | exn -> prerr_endline (Printexc.to_string exn) *)
- )
- )
- in
-*)
-
-
- try
-(* let time = Unix.gettimeofday () in *)
-
-
- let (diff, metasenv, _, cic, _) =
- singleton "third"
- (CicDisambiguate.disambiguate_obj
- ~lookup_in_library
- ~mk_choice:cic_mk_choice
- ~mk_implicit ~fix_instance
- ~description_of_alias:LexiconAst.description_of_alias
- ~aliases:estatus#lstatus.LexiconEngine.aliases
- ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
- ~uri:(Some uri)
- (text,prefix_len,obj))
- in
-
-
-(*
- let time = Unix.gettimeofday () -. time in
- prerr_endline ("VECCHIA DISAMBIGUAZIONE ("^
- UriManager.string_of_uri uri ^"): " ^ string_of_float time);
-*)
-(* try_new (Some cic); *)
-
-
- let estatus = LexiconEngine.set_proof_aliases estatus diff in
- estatus, metasenv, cic
-
- with
- | Sys.Break as exn -> raise exn
- | exn ->
-(* try_new None; *)
- raise exn
-;;
-
let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
let uri =
let baseuri =
let estatus = LexiconEngine.set_proof_aliases estatus diff in
estatus, cic
;;
-
let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)=
match cmd with
- | GrafiteAst.Index(loc,key,uri) ->
- let lexicon_status_ref = ref estatus in
- let disambiguate_term =
- disambiguate_term None text prefix_len lexicon_status_ref [] in
- let disambiguate_term_option metasenv =
- function
- None -> metasenv,None
- | Some t ->
- let metasenv,t = disambiguate_term metasenv t in
- metasenv, Some t
- in
- let metasenv,key = disambiguate_term_option metasenv key in
- !lexicon_status_ref,metasenv,GrafiteAst.Index(loc,key,uri)
+ | GrafiteAst.Index(loc,key,uri) -> (* MATITA 1.0 *) assert false
| GrafiteAst.Select (loc,uri) ->
estatus, metasenv, GrafiteAst.Select(loc,uri)
| GrafiteAst.Pump(loc,i) ->
estatus, metasenv, GrafiteAst.Pump(loc,i)
- | GrafiteAst.PreferCoercion (loc,t) ->
- let lexicon_status_ref = ref estatus in
- let disambiguate_term =
- disambiguate_term None text prefix_len lexicon_status_ref [] in
- let metasenv,t = disambiguate_term metasenv t in
- !lexicon_status_ref, metasenv, GrafiteAst.PreferCoercion (loc,t)
- | GrafiteAst.Coercion (loc,t,b,a,s) ->
- let lexicon_status_ref = ref estatus in
- let disambiguate_term =
- disambiguate_term None text prefix_len lexicon_status_ref [] in
- let metasenv,t = disambiguate_term metasenv t in
- !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
- | GrafiteAst.Inverter (loc,n,indty,params) ->
- let lexicon_status_ref = ref estatus in
- let disambiguate_term =
- disambiguate_term None text prefix_len lexicon_status_ref [] in
- let metasenv,indty = disambiguate_term metasenv indty in
- !lexicon_status_ref, metasenv, GrafiteAst.Inverter (loc,n,indty,params)
+ | GrafiteAst.PreferCoercion (loc,t) -> (* MATITA 1.0 *) assert false
+ | GrafiteAst.Coercion (loc,t,b,a,s) -> (* MATITA 1.0 *) assert false
+ | GrafiteAst.Inverter (loc,n,indty,params) -> (* MATITA 1.0 *) assert false
| GrafiteAst.Default _
| GrafiteAst.Drop _
| GrafiteAst.Include _
| GrafiteAst.Qed _
| GrafiteAst.Set _ as cmd ->
estatus,metasenv,cmd
- | GrafiteAst.Obj (loc,obj) ->
- let estatus,metasenv,obj =
- disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj)in
- estatus, metasenv, GrafiteAst.Obj (loc,obj)
- | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ->
- let lexicon_status_ref = ref estatus in
- let disambiguate_term =
- disambiguate_term None text prefix_len lexicon_status_ref [] in
- let disambiguate_term_option metasenv =
- function
- None -> metasenv,None
- | Some t ->
- let metasenv,t = disambiguate_term metasenv t in
- metasenv, Some t
- in
- let metasenv,a = disambiguate_term metasenv a in
- let metasenv,aeq = disambiguate_term metasenv aeq in
- let metasenv,refl = disambiguate_term_option metasenv refl in
- let metasenv,sym = disambiguate_term_option metasenv sym in
- let metasenv,trans = disambiguate_term_option metasenv trans in
- !lexicon_status_ref, metasenv,
- GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
-
-let disambiguate_macro
- lexicon_status_ref metasenv context (text,prefix_len, macro)
-=
- let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref in
- let disambiguate_reduction_kind =
- disambiguate_reduction_kind text prefix_len lexicon_status_ref in
- match macro with
- | GrafiteAst.Check (loc,term) ->
- let metasenv,term = disambiguate_term context metasenv term in
- metasenv,GrafiteAst.Check (loc,term)
- | GrafiteAst.Eval (loc,kind,term) ->
- let metasenv, term = disambiguate_term context metasenv term in
- let kind = disambiguate_reduction_kind kind in
- metasenv,GrafiteAst.Eval (loc,kind,term)
- | GrafiteAst.AutoInteractive (loc, params) ->
- let metasenv, params =
- disambiguate_auto_params disambiguate_term metasenv context params in
- metasenv, GrafiteAst.AutoInteractive (loc, params)
- | GrafiteAst.Hint _
- | GrafiteAst.Inline _ as macro ->
- metasenv,macro
+ | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false
+ | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> (* MATITA 1.0 *) assert false
(Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string)
GrafiteAst.tactic
-val disambiguate_tactic:
- LexiconEngine.status ref ->
- Cic.context ->
- Cic.metasenv -> int option ->
- tactic Disambiguate.disambiguator_input ->
- Cic.metasenv * lazy_tactic
-
val disambiguate_command:
LexiconEngine.status as 'status ->
?baseuri:string ->
((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
'status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
-val disambiguate_macro:
- LexiconEngine.status ref ->
- Cic.metasenv ->
- Cic.context ->
- ((CicNotationPt.term,CicNotationPt.term) GrafiteAst.macro) Disambiguate.disambiguator_input ->
- Cic.metasenv * (Cic.term,Cic.lazy_term) GrafiteAst.macro
-
val disambiguate_nterm :
NCic.term option ->
(#NEstatus.status as 'status) ->
nCicDisambiguate.cmi:
+disambiguateChoices.cmo: disambiguateChoices.cmi
+disambiguateChoices.cmx: disambiguateChoices.cmi
nCicDisambiguate.cmo: nCicDisambiguate.cmi
nCicDisambiguate.cmx: nCicDisambiguate.cmi
nnumber_notation.cmo:
INTERFACE_FILES = nCicDisambiguate.mli
IMPLEMENTATION_FILES = \
+ disambiguateChoices.ml \
$(INTERFACE_FILES:%.mli=%.ml) nnumber_notation.ml
EXTRA_OBJECTS_TO_INSTALL =
EXTRA_OBJECTS_TO_CLEAN =
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+open Printf
+
+open DisambiguateTypes
+
+exception Choice_not_found of string Lazy.t
+
+let num_choices = ref []
+let nnum_choices = ref []
+
+let add_num_choice choice = num_choices := choice :: !num_choices
+let nadd_num_choice choice = nnum_choices := choice :: !nnum_choices
+
+let has_description dsc = (fun x -> fst x = dsc)
+
+let lookup_num_choices () = !num_choices
+
+let lookup_num_by_dsc dsc =
+ try
+ List.find (has_description dsc) !num_choices
+ with Not_found -> raise (Choice_not_found (lazy ("Num with dsc " ^ dsc)))
+
+let nlookup_num_by_dsc dsc =
+ try
+ List.find (has_description dsc) !nnum_choices
+ with Not_found -> raise (Choice_not_found (lazy ("Num with dsc " ^ dsc)))
+
+let mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref (dsc, args, appl_pattern)=
+ dsc,
+ `Sym_interp
+ (fun cic_args ->
+ let env',rest =
+ let names =
+ List.map (function CicNotationPt.IdentArg (_, name) -> name) args
+ in
+ let rec combine_with_rest l1 l2 =
+ match l1,l2 with
+ _::_,[] -> raise (Invalid_argument "combine_with_rest")
+ | [],rest -> [],rest
+ | he1::tl1,he2::tl2 ->
+ let l,rest = combine_with_rest tl1 tl2 in
+ (he1,he2)::l,rest
+ in
+ try
+ combine_with_rest names cic_args
+ with Invalid_argument _ ->
+ raise (Invalid_choice (lazy (Stdpp.dummy_loc,
+ "The notation " ^ dsc ^ " expects more arguments")))
+ in
+ let combined =
+ TermAcicContent.instantiate_appl_pattern
+ ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env' appl_pattern
+ in
+ match rest with
+ [] -> combined
+ | _::_ -> mk_appl (combined::rest))
+
+let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref symbol dsc =
+ let interpretations = TermAcicContent.lookup_interpretations ~sorted:false symbol in
+ try
+ mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref
+ (List.find (fun (dsc', _, _) -> dsc = dsc') interpretations)
+ with TermAcicContent.Interpretation_not_found | Not_found ->
+ raise (Choice_not_found (lazy (sprintf "Symbol %s, dsc %s" symbol dsc)))
+
+let cic_lookup_symbol_by_dsc = lookup_symbol_by_dsc
+ ~mk_implicit:(function
+ | true -> Cic.Implicit (Some `Type)
+ | false -> Cic.Implicit None)
+ ~mk_appl:(function (Cic.Appl l)::tl -> Cic.Appl (l@tl) | l -> Cic.Appl l)
+ ~term_of_uri:CicUtil.term_of_uri ~term_of_nref:(fun _ -> assert false)
+;;
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open DisambiguateTypes
+
+(** {2 Choice registration low-level interface} *)
+
+ (** raised by lookup_XXXX below *)
+exception Choice_not_found of string Lazy.t
+
+ (** register a new number choice *)
+val add_num_choice: Cic.term codomain_item -> unit
+
+ (** register a new number choice *)
+val nadd_num_choice: NCic.term codomain_item -> unit
+
+(** {2 Choices lookup}
+ * for user defined aliases *)
+
+val lookup_num_choices: unit -> Cic.term codomain_item list
+
+ (** @param dsc description (1st component of codomain_item) *)
+val lookup_num_by_dsc: string -> Cic.term codomain_item
+
+ (** @param dsc description (1st component of codomain_item) *)
+val nlookup_num_by_dsc: string -> NCic.term codomain_item
+
+ (** @param symbol symbol as per AST
+ * @param dsc description (1st component of codomain_item)
+ *)
+val lookup_symbol_by_dsc:
+ mk_appl: ('term list -> 'term) ->
+ mk_implicit: (bool -> 'term) ->
+ term_of_uri: (UriManager.uri -> 'term) ->
+ term_of_nref: (NReference.reference -> 'term) ->
+ string -> string -> 'term codomain_item
+
+val cic_lookup_symbol_by_dsc:
+ string -> string -> Cic.term codomain_item
+
+val mk_choice:
+ mk_appl: ('term list -> 'term) ->
+ mk_implicit: (bool -> 'term) ->
+ term_of_uri: (UriManager.uri -> 'term) ->
+ term_of_nref: (NReference.reference -> 'term) ->
+ string * CicNotationPt.argument_pattern list *
+ CicNotationPt.cic_appl_pattern ->
+ 'term codomain_item
+
let fwd_simpl_tac
?(mk_fresh_name_callback = FNG.mk_fresh_name ~subst:[])
~dbd hyp =
+assert false (* MATITA 1.0
let lapply_tac to_what lemma =
lapply_tac ~mk_fresh_name_callback ~how_many:1 ~to_what:[to_what] lemma
in
PET.apply_tactic tac status
in
PET.mk_tactic fwd_simpl_tac
+ *)
+++ /dev/null
-whelp.cmi:
-fwdQueries.cmi:
-whelp.cmo: whelp.cmi
-whelp.cmx: whelp.cmi
-fwdQueries.cmo: fwdQueries.cmi
-fwdQueries.cmx: fwdQueries.cmi
+++ /dev/null
-whelp.cmi:
-fwdQueries.cmi:
-whelp.cmo: whelp.cmi
-whelp.cmx: whelp.cmi
-fwdQueries.cmo: fwdQueries.cmi
-fwdQueries.cmx: fwdQueries.cmi
+++ /dev/null
-PACKAGE = whelp
-
-INTERFACE_FILES = \
- whelp.mli \
- fwdQueries.mli \
- $(NULL)
-
-IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
-
-include ../../Makefile.defs
-include ../Makefile.common
+++ /dev/null
-(* Copyright (C) 2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-(* fwd_simpl ****************************************************************)
-
-let rec filter_map_n f n = function
- | [] -> []
- | hd :: tl ->
- match f n hd with
- | None -> filter_map_n f (succ n) tl
- | Some hd -> hd :: filter_map_n f (succ n) tl
-
-let get_uri t =
- let aux = function
- | Cic.Appl (hd :: tl) -> Some (CicUtil.uri_of_term hd, tl)
- | hd -> Some (CicUtil.uri_of_term hd, [])
- in
- try aux t with
- | Invalid_argument "uri_of_term" -> None
-
-let get_metadata t =
- let f n t =
- match get_uri t with
- | None -> None
- | Some (uri, _) -> Some (n, uri)
- in
- match get_uri t with
- | None -> None
- | Some (uri, args) -> Some (uri, filter_map_n f 1 args)
-
-let debug_metadata = function
- | None -> ()
- | Some (outer, inners) ->
- let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n (UriManager.string_of_uri uri) in
- Printf.eprintf "\n%s: %s\n" "fwd" (UriManager.string_of_uri outer);
- List.iter f inners; prerr_newline ()
-
-let fwd_simpl ~dbd t =
- let map inners row =
- match row.(0), row.(1), row.(2) with
- | Some source, Some inner, Some index ->
- source,
- List.mem
- (int_of_string index, (UriManager.uri_of_string inner)) inners
- | _ -> "", false
- in
- let rec rank ranks (source, ok) =
- match ranks, ok with
- | [], false -> [source, 0]
- | [], true -> [source, 1]
- | (uri, i) :: tl, false when uri = source -> (uri, 0) :: tl
- | (uri, 0) :: tl, true when uri = source -> (uri, 0) :: tl
- | (uri, i) :: tl, true when uri = source -> (uri, succ i) :: tl
- | hd :: tl, _ -> hd :: rank tl (source, ok)
- in
- let compare (_, x) (_, y) = compare x y in
- let filter n (uri, rank) =
- if rank > 0 then Some (UriManager.uri_of_string uri) else None
- in
- let metadata = get_metadata t in debug_metadata metadata;
- match metadata with
- | None -> []
- | Some (outer, inners) ->
- let select = "source, h_inner, h_index" in
- let from = "genLemma" in
- let where =
- Printf.sprintf "h_outer = \"%s\""
- (HSql.escape HSql.Library dbd (UriManager.string_of_uri outer)) in
- let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in
- let result = HSql.exec HSql.Library dbd query in
- let lemmas = HSql.map ~f:(map inners) result in
- let ranked = List.fold_left rank [] lemmas in
- let ordered = List.rev (List.fast_sort compare ranked) in
- filter_map_n filter 0 ordered
-
-(* get_decomposables ********************************************************)
-
-let decomposables ~dbd =
- let map row = match row.(0) with
- | None -> None
- | Some str ->
- match CicUtil.term_of_uri (UriManager.uri_of_string str) with
- | Cic.MutInd (uri, typeno, _) -> Some (uri, Some typeno)
- | Cic.Const (uri, _) -> Some (uri, None)
- | _ ->
- raise (UriManager.IllFormedUri str)
- in
- let select, from = "source", "decomposables" in
- let query = Printf.sprintf "SELECT %s FROM %s" select from in
- let decomposables = HSql.map ~f:map (HSql.exec HSql.Library dbd query) in
- filter_map_n (fun _ x -> x) 0 decomposables
+++ /dev/null
-(* Copyright (C) 2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-val fwd_simpl: dbd:HSql.dbd -> Cic.term -> UriManager.uri list
-val decomposables: dbd:HSql.dbd -> (UriManager.uri * int option) list
-
+++ /dev/null
-(* Copyright (C) 2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-open Printf
-
-let nonvar uri = not (UriManager.uri_is_var uri)
-
- (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for
- * the "like" operator (which uses '%' and '_'). Does not support escaping. *)
-let sqlpat_of_shellglob =
- let star_RE, qmark_RE, percent_RE, uscore_RE =
- Pcre.regexp "\\*", Pcre.regexp "\\?", Pcre.regexp "%", Pcre.regexp "_"
- in
- fun shellglob ->
- Pcre.replace ~rex:star_RE ~templ:"%"
- (Pcre.replace ~rex:qmark_RE ~templ:"_"
- (Pcre.replace ~rex:percent_RE ~templ:"\\%"
- (Pcre.replace ~rex:uscore_RE ~templ:"\\_"
- shellglob)))
-
-let locate ~(dbd:HSql.dbd) ?(vars = false) pat =
- let escape dbtype dbd s = HSql.escape dbtype dbd s in
- let sql_pat = sqlpat_of_shellglob pat in
- let query dbtype tbl =
- sprintf
- ("SELECT source FROM %s WHERE value LIKE \"%s\" "
- ^^ HSql.escape_string_for_like dbtype dbd)
- tbl (escape dbtype dbd sql_pat)
- in
- let tbls =
- [HSql.User, MetadataTypes.name_tbl ();
- HSql.Library, MetadataTypes.library_name_tbl;
- HSql.Legacy, MetadataTypes.library_name_tbl]
- in
- let map cols =
- match cols.(0) with
- | Some s -> UriManager.uri_of_string s | _ -> assert false
- in
- let result =
- List.fold_left
- (fun acc (dbtype,tbl) ->
- acc @ HSql.map ~f:map (HSql.exec dbtype dbd (query dbtype tbl)))
- [] tbls
- in
- List.filter nonvar result
-
-let match_term ~(dbd:HSql.dbd) ty =
-(* debug_print (lazy (CicPp.ppterm ty)); *)
- let metadata = MetadataExtractor.compute ~body:None ~ty in
- let constants_no =
- MetadataConstraints.UriManagerSet.cardinal (MetadataConstraints.constants_of ty)
- in
- let full_card, diff =
- if CicUtil.is_meta_closed ty then
- Some (MetadataConstraints.Eq constants_no), None
- else
- let diff_no =
- let (hyp_constants, concl_constants) =
- (* collect different constants in hypotheses and conclusions *)
- List.fold_left
- (fun ((hyp, concl) as acc) metadata ->
- match (metadata: MetadataTypes.metadata) with
- | `Sort _ | `Rel _ -> acc
- | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _)
- when not (List.mem uri concl) -> (hyp, uri :: concl)
- | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _)
- when not (List.mem uri hyp) -> (uri :: hyp, concl)
- | `Obj _ -> acc)
- ([], [])
- metadata
- in
- List.length hyp_constants - List.length concl_constants
- in
- let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in
- let diff =
- if MetadataExtractor.IntSet.equal concl_metas hyp_metas then
- Some (MetadataConstraints.Eq diff_no)
- else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then
- Some (MetadataConstraints.Gt (diff_no - 1))
- else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then
- Some (MetadataConstraints.Lt (diff_no + 1))
- else
- None
- in
- None, diff
- in
- let constraints = List.map MetadataTypes.constr_of_metadata metadata in
- MetadataConstraints.at_least ~dbd ?full_card ?diff constraints
-
-let fill_with_dummy_constants t =
- let rec aux i types =
- function
- Cic.Lambda (n,s,t) ->
- let dummy_uri =
- UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)^".con") in
- (aux (i+1) (s::types)
- (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t))
- | t -> t,types
- in
- let t,types = aux 0 [] t in
- t, List.rev types
-
-let instance ~dbd t =
- let t',types = fill_with_dummy_constants t in
- let metadata = MetadataExtractor.compute ~body:None ~ty:t' in
-(* List.iter
- (fun x ->
- debug_print
- (lazy (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))))
- metadata; *)
- let no_concl = MetadataDb.count_distinct `Conclusion metadata in
- let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in
- let no_full = MetadataDb.count_distinct `Statement metadata in
- let is_dummy = function
- | `Obj(s, _) -> (String.sub (UriManager.string_of_uri s) 0 10) <> "cic:/dummy"
- | _ -> true
- in
- let rec look_for_dummy_main = function
- | [] -> None
- | `Obj(s,`MainConclusion (Some (MetadataTypes.Eq d)))::_
- when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") ->
- let s = UriManager.string_of_uri s in
- let len = String.length s in
- let dummy_index = int_of_string (String.sub s 11 (len-15)) in
- let dummy_type = List.nth types dummy_index in
- Some (d,dummy_type)
- | _::l -> look_for_dummy_main l
- in
- match (look_for_dummy_main metadata) with
- | None->
-(* debug_print (lazy "Caso None"); *)
- (* no dummy in main position *)
- let metadata = List.filter is_dummy metadata in
- let constraints = List.map MetadataTypes.constr_of_metadata metadata in
- let concl_card = Some (MetadataConstraints.Eq no_concl) in
- let full_card = Some (MetadataConstraints.Eq no_full) in
- let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
- MetadataConstraints.at_least ~dbd ?concl_card ?full_card ?diff
- constraints
- | Some (depth, dummy_type) ->
-(* debug_print
- (lazy (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type))); *)
- (* a dummy in main position *)
- let metadata_for_dummy_type =
- MetadataExtractor.compute ~body:None ~ty:dummy_type in
- (* Let us skip this for the moment
- let main_of_dummy_type =
- look_for_dummy_main metadata_for_dummy_type in *)
- let metadata = List.filter is_dummy metadata in
- let constraints = List.map MetadataTypes.constr_of_metadata metadata in
- let metadata_for_dummy_type =
- List.filter is_dummy metadata_for_dummy_type in
- let metadata_for_dummy_type, depth' =
- (* depth' = the depth of the A -> A -> Prop *)
- List.fold_left (fun (acc,dep) c ->
- match c with
- | `Sort (s,`MainConclusion (Some (MetadataTypes.Eq i))) ->
- (`Sort (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
- | `Obj (s,`MainConclusion (Some (MetadataTypes.Eq i))) ->
- (`Obj (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
- | `Rel (`MainConclusion (Some (MetadataTypes.Eq i))) ->
- (`Rel (`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
- | _ -> (c::acc,dep)) ([],0) metadata_for_dummy_type
- in
- let constraints_for_dummy_type =
- List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in
- (* start with the dummy constant in main conlusion *)
- let from = ["refObj as table0"] in (* XXX table hardcoded *)
- let where =
- [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos;
- sprintf "table0.h_depth >= %d" depth] in
- let (n,from,where) =
- List.fold_left
- (MetadataConstraints.add_constraint ~start:2)
- (2,from,where) constraints in
- let concl_card = Some (MetadataConstraints.Eq no_concl) in
- let full_card = Some (MetadataConstraints.Eq no_full) in
- let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
- let (n,from,where) =
- MetadataConstraints.add_all_constr
- (n,from,where) concl_card full_card diff in
- (* join with the constraints over the type of the constant *)
- let where =
- (sprintf "table0.h_occurrence = table%d.source" n)::where in
- let where =
- sprintf "table0.h_depth - table%d.h_depth = %d"
- n (depth - depth')::where
- in
- (* XXX performed only in library and legacy not user *)
- let (m,from,where) =
- List.fold_left
- (MetadataConstraints.add_constraint ~start:n)
- (n,from,where) constraints_for_dummy_type
- in
- MetadataConstraints.exec HSql.Library ~dbd (m,from,where)
- @
- MetadataConstraints.exec HSql.Legacy ~dbd (m,from,where)
-
-let elim ~dbd uri =
- let constraints =
- [`Rel [`MainConclusion None];
- `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Ge 1))]);
- `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]);
- `Obj (uri,[`InHypothesis]);
- ]
- in
- MetadataConstraints.at_least ~rating:`Hits ~dbd constraints
-
+++ /dev/null
-(* Copyright (C) 2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-val locate: dbd:HSql.dbd -> ?vars:bool -> string -> UriManager.uri list
-val elim: dbd:HSql.dbd -> UriManager.uri -> UriManager.uri list
-val instance: dbd:HSql.dbd -> Cic.term -> UriManager.uri list
-val match_term: dbd:HSql.dbd -> Cic.term -> UriManager.uri list
-
FINDLIB_COMREQUIRES="\
helm-disambiguation \
-helm-cic_disambiguation \
helm-grafite \
helm-grafite_engine \
helm-tptp_grafite \
let debug = false ;;
let debug_print = if debug then prerr_endline else ignore ;;
-let disambiguate_tactic text prefix_len lexicon_status_ref grafite_status goal tac =
- let metasenv,tac =
- GrafiteDisambiguate.disambiguate_tactic
- lexicon_status_ref
- (GrafiteTypes.get_proof_context grafite_status goal)
- (GrafiteTypes.get_proof_metasenv grafite_status) (Some goal)
- tac
- in
- GrafiteTypes.set_metasenv metasenv grafite_status,tac
-
let disambiguate_command lexicon_status_ref grafite_status cmd =
let baseuri = grafite_status#baseuri in
let lexicon_status,metasenv,cmd =
lexicon_status_ref := lexicon_status;
GrafiteTypes.set_metasenv metasenv grafite_status,cmd
-let disambiguate_macro lexicon_status_ref grafite_status macro context =
- let metasenv,macro =
- GrafiteDisambiguate.disambiguate_macro
- lexicon_status_ref
- (GrafiteTypes.get_proof_metasenv grafite_status)
- context macro
- in
- GrafiteTypes.set_metasenv metasenv grafite_status,macro
-
let eval_macro_screenshot (status : GrafiteTypes.status) name =
let _,_,metasenv,subst,_ = status#obj in
let sequent = List.hd metasenv in
status, `Old []
| ast ->
GrafiteEngine.eval_ast
- ~disambiguate_tactic:(disambiguate_tactic text prefix_len lexicon_status_ref)
+ ~disambiguate_tactic:((* MATITA 1.0*) fun _ -> assert false)
~disambiguate_command:(disambiguate_command lexicon_status_ref)
- ~disambiguate_macro:(disambiguate_macro lexicon_status_ref)
+ ~disambiguate_macro:((* MATITA 1.0*) fun _ -> assert false)
?do_heavy_checks status (text,prefix_len,ast)
in
let new_status =
projects / helm.git / commitdiff