diff options
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrextern.ml | 360 | ||||
-rw-r--r-- | interp/constrextern.mli | 49 | ||||
-rw-r--r-- | interp/constrintern.ml | 653 | ||||
-rw-r--r-- | interp/constrintern.mli | 87 | ||||
-rw-r--r-- | interp/coqlib.ml | 285 | ||||
-rw-r--r-- | interp/coqlib.mli | 133 | ||||
-rw-r--r-- | interp/genarg.ml | 185 | ||||
-rw-r--r-- | interp/genarg.mli | 213 | ||||
-rw-r--r-- | interp/modintern.ml | 103 | ||||
-rw-r--r-- | interp/modintern.mli | 24 | ||||
-rw-r--r-- | interp/ppextend.ml | 57 | ||||
-rw-r--r-- | interp/ppextend.mli | 47 | ||||
-rw-r--r-- | interp/symbols.ml | 331 | ||||
-rw-r--r-- | interp/symbols.mli | 77 | ||||
-rw-r--r-- | interp/syntax_def.ml | 72 | ||||
-rw-r--r-- | interp/syntax_def.mli | 23 | ||||
-rw-r--r-- | interp/topconstr.ml | 300 | ||||
-rw-r--r-- | interp/topconstr.mli | 133 |
18 files changed, 3132 insertions, 0 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml new file mode 100644 index 000000000..b9f22ff00 --- /dev/null +++ b/interp/constrextern.ml @@ -0,0 +1,360 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(*i*) +open Pp +open Util +open Univ +open Names +open Nameops +open Term +open Termops +open Inductive +open Sign +open Environ +open Libnames +open Declare +open Impargs +open Topconstr +open Rawterm +open Pattern +open Nametab +(*i*) + +(* Translation from rawconstr to front constr *) + +(**********************************************************************) +(* Parametrization *) + +(* This governs printing of local context of references *) +let print_arguments = ref false + +(* If true, prints local context of evars, whatever print_arguments *) +let print_evar_arguments = ref false + +(* This forces printing of cast nodes *) +let print_casts = ref true + +(* This governs printing of implicit arguments. When + [print_implicits] is on then [print_implicits_explicit_args] tells + how implicit args are printed. If on, implicit args are printed + prefixed by "!" otherwise the function and not the arguments is + prefixed by "!" *) +let print_implicits = ref false +let print_implicits_explicit_args = ref false + +(* This forces printing of coercions *) +let print_coercions = ref false + +(* This forces printing universe names of Type{.} *) +let print_universes = ref false + + +let with_option o f x = + let old = !o in o:=true; + try let r = f x in o := old; r + with e -> o := old; raise e + +let with_arguments f = with_option print_arguments f +let with_casts f = with_option print_casts f +let with_implicits f = with_option print_implicits f +let with_coercions f = with_option print_coercions f +let with_universes f = with_option print_universes f + +(**********************************************************************) +(* conversion of references *) + +let ids_of_ctxt ctxt = + Array.to_list + (Array.map + (function c -> match kind_of_term c with + | Var id -> id + | _ -> + error + "Termast: arbitrary substitution of references not yet implemented") + ctxt) + +let idopt_of_name = function + | Name id -> Some id + | Anonymous -> None + +let extern_evar loc n = warning "No notation for Meta"; CMeta (loc,n) + +let extern_ref r = Qualid (dummy_loc,shortest_qualid_of_global None r) + +(**********************************************************************) +(* conversion of patterns *) + +let rec extern_cases_pattern = function (* loc is thrown away for printing *) + | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id))) + | PatVar (loc,Anonymous) -> CPatAtom (loc, None) + | PatCstr(loc,cstrsp,args,na) -> + let args = List.map extern_cases_pattern args in + let p = CPatCstr (loc,extern_ref (ConstructRef cstrsp),args) in + (match na with + | Name id -> CPatAlias (loc,p,id) + | Anonymous -> p) + +let occur_name na aty = + match na with + | Name id -> occur_var_constr_expr id aty + | Anonymous -> false + +(* Implicit args indexes are in ascending order *) +let explicitize impl f args = + let n = List.length args in + let rec exprec q = function + | a::args, imp::impl when is_status_implicit imp -> + let tail = exprec (q+1) (args,impl) in + let visible = + (!print_implicits & !print_implicits_explicit_args) + or not (is_inferable_implicit n imp) in + if visible then (a,Some q) :: tail else tail + | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl) + | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*) + | [], _ -> [] in + let args = exprec 1 (args,impl) in + if args = [] then f else CApp (dummy_loc, f, args) + +let rec skip_coercion dest_ref (f,args as app) = + if !print_coercions then app + else + try + match dest_ref f with + | Some r -> + (match Classops.hide_coercion r with + | Some n -> + if n >= List.length args then app + else (* We skip a coercion *) + let _,fargs = list_chop n args in + skip_coercion dest_ref (List.hd fargs,List.tl fargs) + | None -> app) + | None -> app + with Not_found -> app + +let extern_app impl f args = + if !print_implicits & not !print_implicits_explicit_args then + CAppExpl (dummy_loc, f, args) + else + explicitize impl (CRef f) args + +let loc = dummy_loc + +let rec extern = function + | RRef (_,ref) -> CRef (extern_ref ref) + + | RVar (_,id) -> CRef (Ident (loc,id)) + + | REvar (_,n) -> extern_evar loc n + + | RMeta (_,n) -> CMeta (loc,n) + + | RApp (_,f,args) -> + let (f,args) = + skip_coercion (function RRef(_,r) -> Some r | _ -> None) (f,args) in + let args = List.map extern args in + (match f with + | REvar (loc,ev) -> extern_evar loc ev (* we drop args *) + | RRef (loc,ref) -> + extern_app (implicits_of_global ref) (extern_ref ref) args + | _ -> explicitize [] (extern f) args) + + | RProd (_,Anonymous,t,c) -> + (* Anonymous product are never factorized *) + CArrow (loc,extern t,extern c) + + | RLetIn (_,na,t,c) -> + CLetIn (loc,(loc,na),extern t,extern c) + + | RProd (_,na,t,c) -> + let t = extern t in + let (idl,c) = factorize_prod t c in + CProdN (loc,[(loc,na)::idl,t],c) + + | RLambda (_,na,t,c) -> + let t = extern t in + let (idl,c) = factorize_lambda t c in + CLambdaN (loc,[(loc,na)::idl,t],c) + + | RCases (_,typopt,tml,eqns) -> + let pred = option_app extern typopt in + let tml = List.map extern tml in + let eqns = List.map extern_eqn eqns in + CCases (loc,pred,tml,eqns) + + | ROrderedCase (_,cs,typopt,tm,bv) -> + let bv = Array.to_list (Array.map extern bv) in + COrderedCase (loc,cs,option_app extern typopt,extern tm,bv) + + | RRec (_,fk,idv,tyv,bv) -> + (match fk with + | RFix (nv,n) -> + let rec split_lambda binds = function + | (0, t) -> (List.rev binds,extern t) + | (n, RLambda (_,na,t,b)) -> + split_lambda (([loc,na],extern t)::binds) (n-1,b) + | _ -> anomaly "extern: ill-formed fixpoint body" in + let rec split_product = function + | (0, t) -> extern t + | (n, RProd (_,na,t,b)) -> split_product (n-1,b) + | _ -> anomaly "extern: ill-formed fixpoint type" in + let listdecl = + Array.mapi + (fun i fi -> + let (lparams,def) = split_lambda [] (nv.(i)+1,bv.(i)) in + let typ = split_product (nv.(i)+1,tyv.(i)) in + (fi, lparams, typ, def)) + idv + in + CFix (loc,(loc,idv.(n)),Array.to_list listdecl) + | RCoFix n -> + let listdecl = + Array.mapi (fun i fi -> (fi,extern tyv.(i),extern bv.(i))) idv + in + CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl)) + + | RSort (_,s) -> + let s = match s with + | RProp _ -> s + | RType (Some _) when !print_universes -> s + | RType _ -> RType None in + CSort (loc,s) + + | RHole (_,e) -> CHole loc + + | RCast (_,c,t) -> CCast (loc,extern c,extern t) + + | RDynamic (_,d) -> CDynamic (loc,d) + +and factorize_prod aty = function + | RProd (_,Name id,ty,c) + when aty = extern ty + & not (occur_var_constr_expr id aty) (*To avoid na in ty escapes scope*) + -> let (nal,c) = factorize_prod aty c in ((loc,Name id)::nal,c) + | c -> ([],extern c) + +and factorize_lambda aty = function + | RLambda (_,na,ty,c) + when aty = extern ty + & not (occur_name na aty) (* To avoid na in ty' escapes scope *) + -> let (nal,c) = factorize_lambda aty c in ((loc,na)::nal,c) + | c -> ([],extern c) + +and extern_eqn (loc,ids,pl,c) = + (loc,List.map extern_cases_pattern pl,extern c) +(* +and extern_numerals r = + on_numeral (fun p -> + match filter p r with + | Some f + +and extern_symbols r = +*) + +let extern_rawconstr = extern + +(******************************************************************) +(* Main translation function from constr -> constr_expr *) + +let extern_constr at_top env t = + let t' = + if !print_casts then t + else Reductionops.local_strong strip_outer_cast t in + let avoid = if at_top then ids_of_context env else [] in + extern (Detyping.detype env avoid (names_of_rel_context env) t') + +(******************************************************************) +(* Main translation function from pattern -> constr_expr *) + +let rec extern_pattern tenv env = function + | PRef ref -> CRef (extern_ref ref) + + | PVar id -> CRef (Ident (loc,id)) + + | PEvar n -> extern_evar loc n + + | PRel n -> + CRef (Ident (loc, + try match lookup_name_of_rel n env with + | Name id -> id + | Anonymous -> + anomaly "ast_of_pattern: index to an anonymous variable" + with Not_found -> + id_of_string ("[REL "^(string_of_int n)^"]"))) + + | PMeta None -> CHole loc + + | PMeta (Some n) -> CMeta (loc,n) + + | PApp (f,args) -> + let (f,args) = + skip_coercion (function PRef r -> Some r | _ -> None) + (f,Array.to_list args) in + let args = List.map (extern_pattern tenv env) args in + (match f with + | PRef ref -> + extern_app (implicits_of_global ref) (extern_ref ref) args + | _ -> explicitize [] (extern_pattern tenv env f) args) + + | PSoApp (n,args) -> + let args = List.map (extern_pattern tenv env) args in + (* [-n] is the trick to embed a so patten into a regular application *) + (* see constrintern.ml and g_constr.ml4 *) + explicitize [] (CMeta (loc,-n)) args + + | PProd (Anonymous,t,c) -> + (* Anonymous product are never factorized *) + CArrow (loc,extern_pattern tenv env t,extern_pattern tenv env c) + + | PLetIn (na,t,c) -> + CLetIn (loc,(loc,na),extern_pattern tenv env t,extern_pattern tenv env c) + + | PProd (na,t,c) -> + let t = extern_pattern tenv env t in + let (idl,c) = factorize_prod_pattern tenv (add_name na env) t c in + CProdN (loc,[(loc,na)::idl,t],c) + + | PLambda (na,t,c) -> + let t = extern_pattern tenv env t in + let (idl,c) = factorize_lambda_pattern tenv (add_name na env) t c in + CLambdaN (loc,[(loc,na)::idl,t],c) + + | PCase (cs,typopt,tm,bv) -> + let bv = Array.to_list (Array.map (extern_pattern tenv env) bv) in + COrderedCase + (loc,cs,option_app (extern_pattern tenv env) typopt, + extern_pattern tenv env tm,bv) + + | PFix f -> extern (Detyping.detype tenv [] env (mkFix f)) + + | PCoFix c -> extern (Detyping.detype tenv [] env (mkCoFix c)) + + | PSort s -> + let s = match s with + | RProp _ -> s + | RType (Some _) when !print_universes -> s + | RType _ -> RType None in + CSort (loc,s) + +and factorize_prod_pattern tenv env aty = function + | PProd (Name id as na,ty,c) + when aty = extern_pattern tenv env ty + & not (occur_var_constr_expr id aty) (*To avoid na in ty escapes scope*) + -> let (nal,c) = factorize_prod_pattern tenv (na::env) aty c in + ((loc,Name id)::nal,c) + | c -> ([],extern_pattern tenv env c) + +and factorize_lambda_pattern tenv env aty = function + | PLambda (na,ty,c) + when aty = extern_pattern tenv env ty + & not (occur_name na aty) (* To avoid na in ty' escapes scope *) + -> let (nal,c) = factorize_lambda_pattern tenv (add_name na env) aty c + in ((loc,na)::nal,c) + | c -> ([],extern_pattern tenv env c) diff --git a/interp/constrextern.mli b/interp/constrextern.mli new file mode 100644 index 000000000..cfa00c006 --- /dev/null +++ b/interp/constrextern.mli @@ -0,0 +1,49 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ *) + +(*i*) +open Names +open Term +open Termops +open Sign +open Environ +open Libnames +open Nametab +open Rawterm +open Pattern +open Topconstr +(*i*) + +(* Translation of pattern, cases pattern, rawterm and term into syntax + trees for printing *) + +val extern_cases_pattern : cases_pattern -> cases_pattern_expr +val extern_rawconstr : rawconstr -> constr_expr +val extern_pattern : env -> names_context -> constr_pattern -> constr_expr + +(* If [b=true] in [extern_constr b env c] then the variables in the first + level of quantification clashing with the variables in [env] are renamed *) + +val extern_constr : bool -> env -> constr -> constr_expr +val extern_ref : global_reference -> reference + +(* For debugging *) +val print_implicits : bool ref +val print_casts : bool ref +val print_arguments : bool ref +val print_evar_arguments : bool ref +val print_coercions : bool ref +val print_universes : bool ref + +val with_casts : ('a -> 'b) -> 'a -> 'b +val with_implicits : ('a -> 'b) -> 'a -> 'b +val with_arguments : ('a -> 'b) -> 'a -> 'b +val with_coercions : ('a -> 'b) -> 'a -> 'b +val with_universes : ('a -> 'b) -> 'a -> 'b diff --git a/interp/constrintern.ml b/interp/constrintern.ml new file mode 100644 index 000000000..2ce1a4db0 --- /dev/null +++ b/interp/constrintern.ml @@ -0,0 +1,653 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Pp +open Util +open Options +open Names +open Nameops +open Libnames +open Impargs +open Rawterm +open Pattern +open Pretyping +open Topconstr +open Nametab +open Symbols + +type implicits_env = (identifier * Impargs.implicits_list) list + +let interning_grammar = ref false + +let for_grammar f x = + interning_grammar := true; + let a = f x in + interning_grammar := false; + a + +(**********************************************************************) +(* Internalisation errors *) + +type internalisation_error = + | VariableCapture of identifier + | WrongExplicitImplicit + | NegativeMetavariable + | NotAConstructor of reference + | UnboundFixName of bool * identifier + | NonLinearPattern of identifier + | BadPatternsNumber of int * int + | BadExplicitationNumber of int * int option + +exception InternalisationError of loc * internalisation_error + +let explain_variable_capture id = + str "The variable " ++ pr_id id ++ str " occurs in its type" + +let explain_wrong_explicit_implicit = + str "Found an explicitely given implicit argument but was expecting" ++ + fnl () ++ str "a regular one" + +let explain_negative_metavariable = + str "Metavariable numbers must be positive" + +let explain_not_a_constructor ref = + str "Unknown constructor: " ++ pr_reference ref + +let explain_unbound_fix_name is_cofix id = + str "The name" ++ spc () ++ pr_id id ++ + spc () ++ str "is not bound in the corresponding" ++ spc () ++ + str (if is_cofix then "co" else "") ++ str "fixpoint definition" + +let explain_non_linear_pattern id = + str "The variable " ++ pr_id id ++ str " is bound several times in pattern" + +let explain_bad_patterns_number n1 n2 = + let s = if n1 > 1 then "s" else "" in + str "Expecting " ++ int n1 ++ str " pattern" ++ str s ++ str " but found " + ++ int n2 + +let explain_bad_explicitation_number n po = + let s = match po with + | None -> "a regular argument" + | Some p -> string_of_int p in + str "Bad explicitation number: found " ++ int n ++ + str" but was expecting " ++ str s + +let explain_internalisation_error = function + | VariableCapture id -> explain_variable_capture id + | WrongExplicitImplicit -> explain_wrong_explicit_implicit + | NegativeMetavariable -> explain_negative_metavariable + | NotAConstructor ref -> explain_not_a_constructor ref + | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id + | NonLinearPattern id -> explain_non_linear_pattern id + | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 + | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po + +(**********************************************************************) +(* Dump of globalization (to be used by coqdoc) *) + +let add_glob loc ref = +(*i + let sp = Nametab.sp_of_global (Global.env ()) ref in + let dir,_ = repr_path sp in + let rec find_module d = + try + let qid = let dir,id = split_dirpath d in make_qualid dir id in + let _ = Nametab.locate_loaded_library qid in d + with Not_found -> find_module (dirpath_prefix d) + in + let s = string_of_dirpath (find_module dir) in + i*) + let sp = Nametab.sp_of_global None ref in + let id = let _,id = repr_path sp in string_of_id id in + let dp = string_of_dirpath (Declare.library_part ref) in + dump_string (Printf.sprintf "R%d %s.%s\n" (fst loc) dp id) + +(**********************************************************************) +(* Discriminating between bound variables and global references *) + +(* [vars1] is a set of name to avoid (used for the tactic language); + [vars2] is the set of global variables, env is the set of variables + abstracted until this point *) + +(* Is it a bound variables? *) +let intern_var (env,impls,_) (vars1,vars2) loc id = + let imps, args_scopes = + (* Is [id] bound in *) + if Idset.mem id env or List.mem id vars1 + then + try List.assoc id impls, [] + with Not_found -> [], [] + else + (* Is [id] a section variable *) + let _ = Sign.lookup_named id vars2 in + (* Car Fixpoint met les fns définies temporairement comme vars de sect *) + try + let ref = VarRef id in + implicits_of_global ref, find_arguments_scope ref + with _ -> [], [] + in RVar (loc, id), imps, args_scopes + +(* Is it a global reference or a syntactic definition? *) +let intern_qualid env vars loc qid = + try match Nametab.extended_locate qid with + | TrueGlobal ref -> + if !dump then add_glob loc ref; + RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref + | SyntacticDef sp -> + (Syntax_def.search_syntactic_definition loc sp),[],[] + with Not_found -> + error_global_not_found_loc loc qid + +let intern_reference env lvar = function + | Qualid (loc, qid) -> + intern_qualid env lvar loc qid + | Ident (loc, id) -> + (* For old ast syntax compatibility *) + if (string_of_id id).[0] = '$' then RVar (loc,id),[],[] else + (* End old ast syntax compatibility *) + try intern_var env lvar loc id + with Not_found -> + try intern_qualid env lvar loc (make_short_qualid id) + with e -> + (* Extra allowance for grammars *) + if !interning_grammar then begin + if_verbose warning ("Could not globalize " ^ (string_of_id id)); + RVar (loc, id), [], [] + end + else raise e + +let apply_scope_env (ids,impls,scopes as env) = function + | [] -> env, [] + | (Some sc)::scl -> (ids,impls,sc::scopes), scl + | None::scl -> env, scl + +(**********************************************************************) +(* Cases *) + +(* Check linearity of pattern-matching *) +let rec has_duplicate = function + | [] -> None + | x::l -> if List.mem x l then (Some x) else has_duplicate l + +let loc_of_lhs lhs = + join_loc (cases_pattern_loc (List.hd lhs)) (cases_pattern_loc (list_last lhs)) + +let check_linearity lhs ids = + match has_duplicate ids with + | Some id -> + raise (InternalisationError (loc_of_lhs lhs,NonLinearPattern id)) + | None -> + () + +(* Warns if some pattern variable starts with uppercase *) +let check_uppercase loc ids = +(* A quoi ça sert ? Pour l'extraction vers ML ? Maintenant elle est externe + let is_uppercase_var v = + match (string_of_id v).[0] with 'A'..'Z' -> true | _ -> false + in + let warning_uppercase loc uplid = + let vars = h 0 (prlist_with_sep pr_coma pr_id uplid) in + let (s1,s2) = if List.length uplid = 1 then (" ","s ") else ("s "," ") in + warn (str ("the variable"^s1) ++ vars ++ + str (" start"^s2^"with an upper case letter in pattern")) in + let uplid = List.filter is_uppercase_var ids in + if uplid <> [] then warning_uppercase loc uplid +*) + () + +(* Match the number of pattern against the number of matched args *) +let check_number_of_pattern loc n l = + let p = List.length l in + if n<>p then raise (InternalisationError (loc,BadPatternsNumber (n,p))) + +(* Manage multiple aliases *) + + (* [merge_aliases] returns the sets of all aliases encountered at this + point and a substitution mapping extra aliases to the first one *) +let merge_aliases (ids,subst as aliases) id = + ids@[id], if ids=[] then subst else (id, List.hd ids)::subst + +let alias_of = function + | ([],_) -> Anonymous + | (id::_,_) -> Name id + +let message_redundant_alias (id1,id2) = + if_verbose warning + ("Alias variable "^(string_of_id id1)^" is merged with "^(string_of_id id2)) + +(* Differentiating between constructors and matching variables *) +type pattern_qualid_kind = + | ConstrPat of constructor + | VarPat of identifier + +let find_constructor ref = + let (loc,qid) = qualid_of_reference ref in + try match extended_locate qid with + | SyntacticDef sp -> + (match Syntax_def.search_syntactic_definition loc sp with + | RRef (_,(ConstructRef c as x)) -> + if !dump then add_glob loc x; + c + | _ -> + raise (InternalisationError (loc,NotAConstructor ref))) + | TrueGlobal r -> + let rec unf = function + | ConstRef cst -> + (try + let v = Environ.constant_value (Global.env()) cst in + unf (reference_of_constr v) + with + Environ.NotEvaluableConst _ | Not_found -> + raise (InternalisationError (loc,NotAConstructor ref))) + | ConstructRef c -> + if !dump then add_glob loc r; + c + | _ -> raise (InternalisationError (loc,NotAConstructor ref)) + in unf r + with Not_found -> + raise (InternalisationError (loc,NotAConstructor ref)) + +let find_pattern_variable = function + | Ident (loc,id) -> id + | Qualid (loc,_) as x -> raise (InternalisationError(loc,NotAConstructor x)) + +let maybe_constructor ref = + try ConstrPat (find_constructor ref) + with InternalisationError _ -> VarPat (find_pattern_variable ref) + +let rec intern_cases_pattern scopes aliases = function + | CPatAlias (loc, p, id) -> + let aliases' = merge_aliases aliases id in + intern_cases_pattern scopes aliases' p + | CPatCstr (loc, head, pl) -> + let c = find_constructor head in + let (idsl,pl') = + List.split (List.map (intern_cases_pattern scopes ([],[])) pl) + in + (aliases::(List.flatten idsl), PatCstr (loc,c,pl',alias_of aliases)) + | CPatNumeral (loc, n) -> + ([aliases], + Symbols.interp_numeral_as_pattern loc n (alias_of aliases) scopes) + | CPatDelimiters (_, sc, e) -> + intern_cases_pattern (sc::scopes) aliases e + | CPatAtom (loc, Some head) -> + (match maybe_constructor head with + | ConstrPat c -> + ([aliases], PatCstr (loc,c,[],alias_of aliases)) + | VarPat id -> + let aliases = merge_aliases aliases id in + ([aliases], PatVar (loc,alias_of aliases))) + | CPatAtom (loc, None) -> + ([aliases], PatVar (loc,alias_of aliases)) + +(**********************************************************************) +(* Fix and CoFix *) + +let rec intern_fix = function + | [] -> ([],[],[],[]) + | (fi, bl, c, t)::rest-> + let ni = List.length (List.flatten (List.map fst bl)) - 1 in + let (lf,ln,lc,lt) = intern_fix rest in + (fi::lf, ni::ln, + CProdN (dummy_loc, bl, c)::lc, + CLambdaN (dummy_loc, bl, t)::lt) + +let rec intern_cofix = function + | [] -> ([],[],[]) + | (fi, c, t)::rest -> + let (lf,lc,lt) = intern_cofix rest in + (fi::lf, c::lc, t::lt) + +(**********************************************************************) +(* Utilities for binders *) + +let check_capture loc ty = function + | Name id when occur_var_constr_expr id ty -> + raise (InternalisationError (loc,VariableCapture id)) + | _ -> + () + +let locate_if_isevar loc id = function + | RHole _ -> RHole (loc, AbstractionType id) + | x -> x + +(**********************************************************************) +(* Utilities for application *) + +let set_hole_implicit i = function + | RRef (loc,r) -> (loc,ImplicitArg (r,i)) + | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i)) + | _ -> anomaly "Only refs have implicits" + +(**********************************************************************) +(* Syntax extensions *) + +let coerce_to_id = function + | CRef (Ident (_,id)) -> id + | c -> + user_err_loc (constr_loc c, "subst_rawconstr", + str"This expression should be a simple identifier") + +let traverse_binder id (subst,(ids,impls,scopes as env)) = + try + let id' = coerce_to_id (List.assoc id subst) in + id', (subst,(Idset.add id' ids,impls,scopes)) + with Not_found -> + id, (List.remove_assoc id subst,env) + +let rec subst_rawconstr loc interp (subst,env as senv) = function + | AVar id -> + let a = try List.assoc id subst + with Not_found -> CRef (Ident (dummy_loc,id)) in + interp env a + | t -> + map_aconstr_with_binders_loc loc traverse_binder + (subst_rawconstr loc interp) senv t + +(**********************************************************************) +(* Main loop *) + +let internalise sigma env allow_soapp lvar c = + let rec intern (ids,impls,scopes as env) = function + | CRef ref as x -> + let (c,imp,subscopes) = intern_reference env lvar ref in + (match intern_impargs c env imp subscopes [] with + | [] -> c + | l -> RApp (constr_loc x, c, l)) + | CFix (loc, (locid,iddef), ldecl) -> + let (lf,ln,lc,lt) = intern_fix ldecl in + let n = + try + (list_index iddef lf) -1 + with Not_found -> + raise (InternalisationError (locid,UnboundFixName (false,iddef))) + in + let ids' = List.fold_right Idset.add lf ids in + let defl = Array.of_list (List.map (intern (ids',impls,scopes)) lt) in + let arityl = Array.of_list (List.map (intern env) lc) in + RRec (loc,RFix (Array.of_list ln,n), Array.of_list lf, arityl, defl) + | CCoFix (loc, (locid,iddef), ldecl) -> + let (lf,lc,lt) = intern_cofix ldecl in + let n = + try + (list_index iddef lf) -1 + with Not_found -> + raise (InternalisationError (locid,UnboundFixName (true,iddef))) + in + let ids' = List.fold_right Idset.add lf ids in + let defl = Array.of_list (List.map (intern (ids',impls,scopes)) lt) in + let arityl = Array.of_list (List.map (intern env) lc) in + RRec (loc,RCoFix n, Array.of_list lf, arityl, defl) + | CArrow (loc,c1,c2) -> + RProd (loc, Anonymous, intern env c1, intern env c2) + | CProdN (loc,[],c2) -> + intern env c2 + | CProdN (loc,(nal,ty)::bll,c2) -> + iterate_prod loc env ty (CProdN (loc, bll, c2)) nal + | CLambdaN (loc,[],c2) -> + intern env c2 + | CLambdaN (loc,(nal,ty)::bll,c2) -> + iterate_lam loc env ty (CLambdaN (loc, bll, c2)) nal + | CLetIn (loc,(_,na),c1,c2) -> + RLetIn (loc, na, intern env c1, + intern (name_fold Idset.add na ids,impls,scopes) c2) + | CNotation (loc,ntn,args) -> + subst_rawconstr loc intern (args,env) + (Symbols.interp_notation ntn scopes) + | CNumeral (loc, n) -> + Symbols.interp_numeral loc n scopes + | CDelimiters (loc, sc, e) -> + intern (ids,impls,sc::scopes) e + | CAppExpl (loc, ref, args) -> + let (f,_,args_scopes) = intern_reference env lvar ref in + RApp (loc, f, intern_args env args_scopes args) + | CApp (loc, f, args) -> + let (c, impargs, args_scopes) = + match f with + | CRef ref -> intern_reference env lvar ref + | _ -> (intern env f, [], []) + in + RApp (loc, c, intern_impargs c env impargs args_scopes args) + | CCases (loc, po, tms, eqns) -> + RCases (loc, option_app (intern env) po, + List.map (intern env) tms, + List.map (intern_eqn (List.length tms) env) eqns) + | COrderedCase (loc, tag, po, c, cl) -> + ROrderedCase (loc, tag, option_app (intern env) po, intern env c, + Array.of_list (List.map (intern env) cl)) + | CHole loc -> + RHole (loc, QuestionMark) + | CMeta (loc, n) when n >=0 or allow_soapp -> + RMeta (loc, n) + | CMeta (loc, _) -> + raise (InternalisationError (loc,NegativeMetavariable)) + | CSort (loc, s) -> + RSort(loc,s) + | CCast (loc, c1, c2) -> + RCast (loc,intern env c1,intern env c2) + + | CGrammar (loc,c,subst) -> + subst_rawconstr loc intern (subst,env) c + + | CDynamic (loc,d) -> RDynamic (loc,d) + + and intern_eqn n (ids,impls,scopes as env) (loc,lhs,rhs) = + let (idsl_substl_list,pl) = + List.split (List.map (intern_cases_pattern scopes ([],[])) lhs) in + let idsl, substl = List.split (List.flatten idsl_substl_list) in + let eqn_ids = List.flatten idsl in + let subst = List.flatten substl in + (* Linearity implies the order in ids is irrelevant *) + check_linearity lhs eqn_ids; + check_uppercase loc eqn_ids; + check_number_of_pattern loc n pl; + let rhs = replace_vars_constr_expr subst rhs in + List.iter message_redundant_alias subst; + let env_ids = List.fold_right Idset.add eqn_ids ids in + (loc, eqn_ids,pl,intern (env_ids,impls,scopes) rhs) + + and iterate_prod loc2 (ids,impls,scopes as env) ty body = function + | (loc1,na)::nal -> + if nal <> [] then check_capture loc1 ty na; + let ids' = name_fold Idset.add na ids in + let body = iterate_prod loc2 (ids',impls,scopes) ty body nal in + RProd (join_loc loc1 loc2, na, intern env ty, body) + | [] -> intern env body + + and iterate_lam loc2 (ids,impls,scopes as env) ty body = function + | (loc1,na)::nal -> + if nal <> [] then check_capture loc1 ty na; + let ids' = name_fold Idset.add na ids in + let body = iterate_lam loc2 (ids',impls,scopes) ty body nal in + let ty = locate_if_isevar loc1 na (intern env ty) in + RLambda (join_loc loc1 loc2, na, ty, body) + | [] -> intern env body + + and intern_impargs c env l subscopes args = + let rec aux n l subscopes args = + let (enva,subscopes') = apply_scope_env env subscopes in + match (l,args) with + | (imp::l', (a,Some j)::args') -> + if is_status_implicit imp & j>=n then + if j=n then + (intern enva a)::(aux (n+1) l' subscopes' args') + else + (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args) + else + let e = if is_status_implicit imp then Some n else None in + raise + (InternalisationError(constr_loc a,BadExplicitationNumber (j,e))) + | (imp::l',(a,None)::args') -> + if is_status_implicit imp then + (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args) + else + (intern enva a)::(aux (n+1) l' subscopes' args') + | ([],args) -> intern_tailargs env subscopes args + | (_::l',[]) -> + if List.for_all is_status_implicit l then + (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes args) + else [] + in + aux 1 l subscopes args + + and intern_tailargs env subscopes = function + | (a,Some _)::args' -> + raise (InternalisationError (constr_loc a, WrongExplicitImplicit)) + | (a,None)::args -> + let (enva,subscopes) = apply_scope_env env subscopes in + (intern enva a) :: (intern_tailargs env subscopes args) + | [] -> [] + + and intern_args env subscopes = function + | [] -> [] + | a::args -> + let (enva,subscopes) = apply_scope_env env subscopes in + (intern enva a) :: (intern_args env subscopes args) + + in + try + intern env c + with + InternalisationError (loc,e) -> + user_err_loc (loc,"internalize",explain_internalisation_error e) + +(**************************************************************************) +(* Functions to translate constr_expr into rawconstr *) +(**************************************************************************) + +let extract_ids env = + List.fold_right Idset.add + (Termops.ids_of_rel_context (Environ.rel_context env)) + Idset.empty + +let interp_rawconstr_gen sigma env impls allow_soapp lvar c = + internalise sigma (extract_ids env, impls, Symbols.current_scopes ()) + allow_soapp (lvar,Environ.named_context env) c + +let interp_rawconstr sigma env c = + interp_rawconstr_gen sigma env [] false [] c + +let interp_rawconstr_with_implicits sigma env impls c = + interp_rawconstr_gen sigma env impls false [] c + +(* The same as interp_rawconstr but with a list of variables which must not be + globalized *) + +let interp_rawconstr_wo_glob sigma env lvar c = + interp_rawconstr_gen sigma env [] false lvar c + +(*********************************************************************) +(* Functions to parse and interpret constructions *) + +let interp_constr sigma env c = + understand sigma env (interp_rawconstr sigma env c) + +let interp_openconstr sigma env c = + understand_gen_tcc sigma env [] [] None (interp_rawconstr sigma env c) + +let interp_casted_openconstr sigma env c typ = + understand_gen_tcc sigma env [] [] (Some typ) (interp_rawconstr sigma env c) + +let interp_type sigma env c = + understand_type sigma env (interp_rawconstr sigma env c) + +let interp_type_with_implicits sigma env impls c = + understand_type sigma env (interp_rawconstr_with_implicits sigma env impls c) + +let judgment_of_rawconstr sigma env c = + understand_judgment sigma env (interp_rawconstr sigma env c) + +let type_judgment_of_rawconstr sigma env c = + understand_type_judgment sigma env (interp_rawconstr sigma env c) + +(* To retype a list of key*constr with undefined key *) +let retype_list sigma env lst = + List.fold_right (fun (x,csr) a -> + try (x,Retyping.get_judgment_of env sigma csr)::a with + | Anomaly _ -> a) lst [] + +(* List.map (fun (x,csr) -> (x,Retyping.get_judgment_of env sigma csr)) lst*) + +(* Interprets a constr according to two lists *) +(* of instantiations (variables and metas) *) +(* Note: typ is retyped *) +let interp_constr_gen sigma env lvar lmeta c exptyp = + let c = interp_rawconstr_gen sigma env [] false (List.map fst lvar) c + and rtype lst = retype_list sigma env lst in + understand_gen sigma env (rtype lvar) (rtype lmeta) exptyp c;; + +(*Interprets a casted constr according to two lists of instantiations + (variables and metas)*) +let interp_openconstr_gen sigma env lvar lmeta c exptyp = + let c = interp_rawconstr_gen sigma env [] false (List.map fst lvar) c + and rtype lst = retype_list sigma env lst in + understand_gen_tcc sigma env (rtype lvar) (rtype lmeta) exptyp c;; + +let interp_casted_constr sigma env c typ = + understand_gen sigma env [] [] (Some typ) (interp_rawconstr sigma env c) + +(* To process patterns, we need a translation without typing at all. *) + +let rec pat_of_raw metas vars lvar = function + | RVar (_,id) -> + (try PRel (list_index (Name id) vars) + with Not_found -> + try List.assoc id lvar + with Not_found -> PVar id) + | RMeta (_,n) -> + metas := n::!metas; PMeta (Some n) + | RRef (_,r) -> + PRef r + (* Hack pour ne pas réécrire une interprétation complète des patterns*) + | RApp (_, RMeta (_,n), cl) when n<0 -> + PSoApp (- n, List.map (pat_of_raw metas vars lvar) cl) + | RApp (_,c,cl) -> + PApp (pat_of_raw metas vars lvar c, + Array.of_list (List.map (pat_of_raw metas vars lvar) cl)) + | RLambda (_,na,c1,c2) -> + PLambda (na, pat_of_raw metas vars lvar c1, + pat_of_raw metas (na::vars) lvar c2) + | RProd (_,na,c1,c2) -> + PProd (na, pat_of_raw metas vars lvar c1, + pat_of_raw metas (na::vars) lvar c2) + | RLetIn (_,na,c1,c2) -> + PLetIn (na, pat_of_raw metas vars lvar c1, + pat_of_raw metas (na::vars) lvar c2) + | RSort (_,s) -> + PSort s + | RHole _ -> + PMeta None + | RCast (_,c,t) -> + if_verbose warning "Cast not taken into account in constr pattern"; + pat_of_raw metas vars lvar c + | ROrderedCase (_,st,po,c,br) -> + PCase (st,option_app (pat_of_raw metas vars lvar) po, + pat_of_raw metas vars lvar c, + Array.map (pat_of_raw metas vars lvar) br) + | r -> + let loc = loc_of_rawconstr r in + user_err_loc (loc,"pattern_of_rawconstr", str "Not supported pattern") + +let pattern_of_rawconstr lvar c = + let metas = ref [] in + let p = pat_of_raw metas [] lvar c in + (!metas,p) + +let interp_constrpattern_gen sigma env lvar c = + let c = interp_rawconstr_gen sigma env [] true (List.map fst lvar) c in + let nlvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) lvar in + pattern_of_rawconstr nlvar c + +let interp_constrpattern sigma env c = + interp_constrpattern_gen sigma env [] c + +let interp_aconstr a = + aconstr_of_rawconstr (interp_rawconstr Evd.empty (Global.env()) a) diff --git a/interp/constrintern.mli b/interp/constrintern.mli new file mode 100644 index 000000000..ce8c6f5ee --- /dev/null +++ b/interp/constrintern.mli @@ -0,0 +1,87 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ *) + +(*i*) +open Names +open Term +open Sign +open Evd +open Environ +open Libnames +open Rawterm +open Pattern +open Coqast +open Topconstr +(*i*) + +(*s Translation from front abstract syntax of term to untyped terms (rawconstr) + + The translation performs: + + - resolution of names : + - check all variables are bound + - make absolute the references to global objets + - resolution of symbolic notations using scopes + - insert existential variables for implicit arguments +*) + +type implicits_env = (identifier * Impargs.implicits_list) list + +(* Interprets global names, including syntactic defs and section variables *) +val interp_rawconstr : evar_map -> env -> constr_expr -> rawconstr +val interp_rawconstr_gen : evar_map -> env -> implicits_env -> + bool -> identifier list -> constr_expr -> rawconstr + +(*s Composing the translation with typing *) +val interp_constr : evar_map -> env -> constr_expr -> constr +val interp_casted_constr : evar_map -> env -> constr_expr -> types -> constr +val interp_type : evar_map -> env -> constr_expr -> types +val interp_openconstr : evar_map -> env -> constr_expr -> evar_map * constr +val interp_casted_openconstr : + evar_map -> env -> constr_expr -> constr -> evar_map * constr + +(* [interp_type_with_implicits] extends [interp_type] by allowing + implicits arguments in the ``rel'' part of [env]; the extra + argument associates a list of implicit positions to identifiers + declared in the rel_context of [env] *) +val interp_type_with_implicits : + evar_map -> env -> implicits_env -> constr_expr -> types + +(*s Build a judgement from *) +val judgment_of_rawconstr : evar_map -> env -> constr_expr -> unsafe_judgment +val type_judgment_of_rawconstr : + evar_map -> env -> constr_expr -> unsafe_type_judgment + +(* Interprets a constr according to two lists of instantiations (variables and + metas), possibly casting it*) +val interp_constr_gen : + evar_map -> env -> (identifier * constr) list -> + (int * constr) list -> constr_expr -> constr option -> constr + +(* Interprets a constr according to two lists of instantiations (variables and + metas), possibly casting it, and turning unresolved evar into metas*) +val interp_openconstr_gen : + evar_map -> env -> (identifier * constr) list -> + (int * constr) list -> constr_expr -> constr option -> evar_map * constr + +(* Interprets constr patterns according to a list of instantiations + (variables)*) +val interp_constrpattern_gen : + evar_map -> env -> (identifier * constr) list -> constr_expr -> + int list * constr_pattern + +val interp_constrpattern : + evar_map -> env -> constr_expr -> int list * constr_pattern + +(* Interprets into a abbreviatable constr *) +val interp_aconstr : constr_expr -> aconstr + +(* Globalization leak for Grammar *) +val for_grammar : ('a -> 'b) -> 'a -> 'b diff --git a/interp/coqlib.ml b/interp/coqlib.ml new file mode 100644 index 000000000..d06f6ac52 --- /dev/null +++ b/interp/coqlib.ml @@ -0,0 +1,285 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Util +open Names +open Term +open Libnames +open Declare +open Pattern +open Nametab + +let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) +let coq_id = id_of_string "Coq" +let init_id = id_of_string "Init" +let arith_id = id_of_string "Arith" +let datatypes_id = id_of_string "Datatypes" + +let logic_module = make_dir ["Coq";"Init";"Logic"] +let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"] +let datatypes_module = make_dir ["Coq";"Init";"Datatypes"] +let arith_module = make_dir ["Coq";"Arith";"Arith"] + +(* TODO: temporary hack *) +let make_path dir id = Libnames.encode_kn dir id + +let nat_path = make_path datatypes_module (id_of_string "nat") + +let glob_nat = IndRef (nat_path,0) + +let path_of_O = ((nat_path,0),1) +let path_of_S = ((nat_path,0),2) +let glob_O = ConstructRef path_of_O +let glob_S = ConstructRef path_of_S + +let eq_path = make_path logic_module (id_of_string "eq") +let eqT_path = make_path logic_type_module (id_of_string "eqT") + +let glob_eq = IndRef (eq_path,0) +let glob_eqT = IndRef (eqT_path,0) + +let reference dir s = + let dir = make_dir ("Coq"::"Init"::[dir]) in + let id = id_of_string s in + try + Nametab.absolute_reference (Libnames.make_path dir id) + with Not_found -> + anomaly ("Coqlib: cannot find "^(string_of_qualid (make_qualid dir id))) + +let constant dir s = constr_of_reference (reference dir s) + +type coq_sigma_data = { + proj1 : constr; + proj2 : constr; + elim : constr; + intro : constr; + typ : constr } + +type 'a delayed = unit -> 'a + +let build_sigma_set () = + { proj1 = constant "Specif" "projS1"; + proj2 = constant "Specif" "projS2"; + elim = constant "Specif" "sigS_rec"; + intro = constant "Specif" "existS"; + typ = constant "Specif" "sigS" } + +let build_sigma_type () = + { proj1 = constant "Specif" "projT1"; + proj2 = constant "Specif" "projT2"; + elim = constant "Specif" "sigT_rec"; + intro = constant "Specif" "existT"; + typ = constant "Specif" "sigT" } + +(* Equalities *) +type coq_leibniz_eq_data = { + eq : constr delayed; + ind : constr delayed; + rrec : constr delayed option; + rect : constr delayed option; + congr: constr delayed; + sym : constr delayed } + +let constant dir id = lazy (constant dir id) + +(* Equality on Set *) +let coq_eq_eq = constant "Logic" "eq" +let coq_eq_ind = constant "Logic" "eq_ind" +let coq_eq_rec = constant "Logic" "eq_rec" +let coq_eq_rect = constant "Logic" "eq_rect" +let coq_eq_congr = constant "Logic" "f_equal" +let coq_eq_sym = constant "Logic" "sym_eq" +let coq_f_equal2 = constant "Logic" "f_equal2" + +let build_coq_eq_data = { + eq = (fun () -> Lazy.force coq_eq_eq); + ind = (fun () -> Lazy.force coq_eq_ind); + rrec = Some (fun () -> Lazy.force coq_eq_rec); + rect = Some (fun () -> Lazy.force coq_eq_rect); + congr = (fun () -> Lazy.force coq_eq_congr); + sym = (fun () -> Lazy.force coq_eq_sym) } + +let build_coq_eq = build_coq_eq_data.eq +let build_coq_f_equal2 () = Lazy.force coq_f_equal2 + +(* Specif *) +let coq_sumbool = constant "Specif" "sumbool" + +let build_coq_sumbool () = Lazy.force coq_sumbool + +(* Equality on Type *) +let coq_eqT_eq = constant "Logic_Type" "eqT" +let coq_eqT_ind = constant "Logic_Type" "eqT_ind" +let coq_eqT_congr =constant "Logic_Type" "congr_eqT" +let coq_eqT_sym = constant "Logic_Type" "sym_eqT" + +let build_coq_eqT_data = { + eq = (fun () -> Lazy.force coq_eqT_eq); + ind = (fun () -> Lazy.force coq_eqT_ind); + rrec = None; + rect = None; + congr = (fun () -> Lazy.force coq_eqT_congr); + sym = (fun () -> Lazy.force coq_eqT_sym) } + +let build_coq_eqT = build_coq_eqT_data.eq +let build_coq_sym_eqT = build_coq_eqT_data.sym + +(* Equality on Type as a Type *) +let coq_idT_eq = constant "Logic_Type" "identityT" +let coq_idT_ind = constant "Logic_Type" "identityT_ind" +let coq_idT_rec = constant "Logic_Type" "identityT_rec" +let coq_idT_rect = constant "Logic_Type" "identityT_rect" +let coq_idT_congr = constant "Logic_Type" "congr_idT" +let coq_idT_sym = constant "Logic_Type" "sym_idT" + +let build_coq_idT_data = { + eq = (fun () -> Lazy.force coq_idT_eq); + ind = (fun () -> Lazy.force coq_idT_ind); + rrec = Some (fun () -> Lazy.force coq_idT_rec); + rect = Some (fun () -> Lazy.force coq_idT_rect); + congr = (fun () -> Lazy.force coq_idT_congr); + sym = (fun () -> Lazy.force coq_idT_sym) } + +(* Empty Type *) +let coq_EmptyT = constant "Logic_Type" "EmptyT" + +(* Unit Type and its unique inhabitant *) +let coq_UnitT = constant "Logic_Type" "UnitT" +let coq_IT = constant "Logic_Type" "IT" + +(* The False proposition *) +let coq_False = constant "Logic" "False" + +(* The True proposition and its unique proof *) +let coq_True = constant "Logic" "True" +let coq_I = constant "Logic" "I" + +(* Connectives *) +let coq_not = constant "Logic" "not" +let coq_and = constant "Logic" "and" +let coq_or = constant "Logic" "or" +let coq_ex = constant "Logic" "ex" + +(* Runtime part *) +let build_coq_EmptyT () = Lazy.force coq_EmptyT +let build_coq_UnitT () = Lazy.force coq_UnitT +let build_coq_IT () = Lazy.force coq_IT + +let build_coq_True () = Lazy.force coq_True +let build_coq_I () = Lazy.force coq_I + +let build_coq_False () = Lazy.force coq_False +let build_coq_not () = Lazy.force coq_not +let build_coq_and () = Lazy.force coq_and +let build_coq_or () = Lazy.force coq_or +let build_coq_ex () = Lazy.force coq_ex + +(****************************************************************************) +(* Patterns *) +(* This needs to have interp_constrpattern available ... +let parse_astconstr s = + try + Pcoq.parse_string Pcoq.Constr.constr_eoi s + with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) -> + error "Syntax error : not a construction" + +let parse_pattern s = + Constrintern.interp_constrpattern Evd.empty (Global.env()) (parse_astconstr s) + +let coq_eq_pattern = + lazy (snd (parse_pattern "(Coq.Init.Logic.eq ?1 ?2 ?3)")) +let coq_eqT_pattern = + lazy (snd (parse_pattern "(Coq.Init.Logic_Type.eqT ?1 ?2 ?3)")) +let coq_idT_pattern = + lazy (snd (parse_pattern "(Coq.Init.Logic_Type.identityT ?1 ?2 ?3)")) +let coq_existS_pattern = + lazy (snd (parse_pattern "(Coq.Init.Specif.existS ?1 ?2 ?3 ?4)")) +let coq_existT_pattern = + lazy (snd (parse_pattern "(Coq.Init.Specif.existT ?1 ?2 ?3 ?4)")) +let coq_not_pattern = + lazy (snd (parse_pattern "(Coq.Init.Logic.not ?)")) +let coq_imp_False_pattern = + lazy (snd (parse_pattern "? -> Coq.Init.Logic.False")) +let coq_imp_False_pattern = + lazy (snd (parse_pattern "? -> Coq.Init.Logic.False")) +let coq_eqdec_partial_pattern + lazy (snd (parse_pattern "(sumbool (eq ?1 ?2 ?3) ?4)")) +let coq_eqdec_pattern + lazy (snd (parse_pattern "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}")) +*) + +(* The following is less readable but does not depend on parsing *) +let coq_eq_ref = lazy (reference "Logic" "eq") +let coq_eqT_ref = lazy (reference "Logic_Type" "eqT") +let coq_idT_ref = lazy (reference "Logic_Type" "identityT") +let coq_existS_ref = lazy (reference "Specif" "existS") +let coq_existT_ref = lazy (reference "Specif" "existT") +let coq_not_ref = lazy (reference "Logic" "not") +let coq_False_ref = lazy (reference "Logic" "False") +let coq_sumbool_ref = lazy (reference "Specif" "sumbool") +let coq_sig_ref = lazy (reference "Specif" "sig") + +(* Pattern "(sig ?1 ?2)" *) +let coq_sig_pattern = + lazy (PApp (PRef (Lazy.force coq_sig_ref), + [| PMeta (Some 1); PMeta (Some 2) |])) + +(* Patterns "(eq ?1 ?2 ?3)", "(eqT ?1 ?2 ?3)" and "(idT ?1 ?2 ?3)" *) +let coq_eq_pattern_gen eq = + lazy (PApp(PRef (Lazy.force eq), Array.init 3 (fun i -> PMeta (Some (i+1))))) +let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref +let coq_eqT_pattern = coq_eq_pattern_gen coq_eqT_ref +let coq_idT_pattern = coq_eq_pattern_gen coq_idT_ref + +(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *) +let coq_ex_pattern_gen ex = + lazy (PApp(PRef (Lazy.force ex), Array.init 4 (fun i -> PMeta (Some (i+1))))) +let coq_existS_pattern = coq_ex_pattern_gen coq_existS_ref +let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref + +(* Patterns "~ ?" and "? -> False" *) +let coq_not_pattern = lazy(PApp(PRef (Lazy.force coq_not_ref), [|PMeta None|])) +let imp a b = PProd (Anonymous, a, b) +let coq_imp_False_pattern = + lazy (imp (PMeta None) (PRef (Lazy.force coq_False_ref))) + +(* Pattern "(sumbool (eq ?1 ?2 ?3) ?4)" *) +let coq_eqdec_partial_pattern = + lazy + (PApp + (PRef (Lazy.force coq_sumbool_ref), + [| Lazy.force coq_eq_pattern; PMeta (Some 4) |])) + +(* The expected form of the goal for the tactic Decide Equality *) + +(* Pattern "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}" *) +(* i.e. "(x,y:?1)(sumbool (eq ?1 x y) ~(eq ?1 x y))" *) +let x = Name (id_of_string "x") +let y = Name (id_of_string "y") +let coq_eqdec_pattern = + lazy + (PProd (x, PMeta (Some 1), PProd (y, PMeta (Some 1), + PApp (PRef (Lazy.force coq_sumbool_ref), + [| PApp (PRef (Lazy.force coq_eq_ref), + [| PMeta (Some 1); PRel 2; PRel 1 |]); + PApp (PRef (Lazy.force coq_not_ref), + [|PApp (PRef (Lazy.force coq_eq_ref), + [| PMeta (Some 1); PRel 2; PRel 1 |])|]) |])))) + +let build_coq_eq_pattern () = Lazy.force coq_eq_pattern +let build_coq_eqT_pattern () = Lazy.force coq_eqT_pattern +let build_coq_idT_pattern () = Lazy.force coq_idT_pattern +let build_coq_existS_pattern () = Lazy.force coq_existS_pattern +let build_coq_existT_pattern () = Lazy.force coq_existT_pattern +let build_coq_not_pattern () = Lazy.force coq_not_pattern +let build_coq_imp_False_pattern () = Lazy.force coq_imp_False_pattern +let build_coq_eqdec_partial_pattern () = Lazy.force coq_eqdec_partial_pattern +let build_coq_eqdec_pattern () = Lazy.force coq_eqdec_pattern +let build_coq_sig_pattern () = Lazy.force coq_sig_pattern diff --git a/interp/coqlib.mli b/interp/coqlib.mli new file mode 100644 index 000000000..dbe99e399 --- /dev/null +++ b/interp/coqlib.mli @@ -0,0 +1,133 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(*i*) +open Names +open Libnames +open Nametab +open Term +open Pattern +(*i*) + +(*s This module collects the global references, constructions and + patterns of the standard library used in ocaml files *) + +(*s Global references *) + +(* Modules *) +val logic_module : dir_path +val logic_type_module : dir_path + +(* Natural numbers *) +val glob_nat : global_reference +val path_of_O : constructor +val path_of_S : constructor +val glob_O : global_reference +val glob_S : global_reference + +(* Equality *) +val glob_eq : global_reference +val glob_eqT : global_reference + +(*s Constructions and patterns related to Coq initial state are unknown + at compile time. Therefore, we can only provide methods to build + them at runtime. This is the purpose of the [constr delayed] and + [constr_pattern delayed] types. Objects of this time needs to be + applied to [()] to get the actual constr or pattern at runtime *) + +type 'a delayed = unit -> 'a + +(*s For Equality tactics *) +type coq_sigma_data = { + proj1 : constr; + proj2 : constr; + elim : constr; + intro : constr; + typ : constr } + +val build_sigma_set : unit -> coq_sigma_data +val build_sigma_type : unit -> coq_sigma_data + +type coq_leibniz_eq_data = { + eq : constr delayed; + ind : constr delayed; + rrec : constr delayed option; + rect : constr delayed option; + congr: constr delayed; + sym : constr delayed } + +val build_coq_eq_data : coq_leibniz_eq_data +val build_coq_eqT_data : coq_leibniz_eq_data +val build_coq_idT_data : coq_leibniz_eq_data + +val build_coq_f_equal2 : constr delayed +val build_coq_eqT : constr delayed +val build_coq_sym_eqT : constr delayed + +(* Empty Type *) +val build_coq_EmptyT : constr delayed + +(* Unit Type and its unique inhabitant *) +val build_coq_UnitT : constr delayed +val build_coq_IT : constr delayed + +(* Specif *) +val build_coq_sumbool : constr delayed + +(*s Connectives *) +(* The False proposition *) +val build_coq_False : constr delayed + +(* The True proposition and its unique proof *) +val build_coq_True : constr delayed +val build_coq_I : constr delayed + +(* Negation *) +val build_coq_not : constr delayed + +(* Conjunction *) +val build_coq_and : constr delayed + +(* Disjunction *) +val build_coq_or : constr delayed + +(* Existential quantifier *) +val build_coq_ex : constr delayed + +(**************************** Patterns ************************************) +(* ["(eq ?1 ?2 ?3)"] *) +val build_coq_eq_pattern : constr_pattern delayed + +(* ["(eqT ?1 ?2 ?3)"] *) +val build_coq_eqT_pattern : constr_pattern delayed + +(* ["(identityT ?1 ?2 ?3)"] *) +val build_coq_idT_pattern : constr_pattern delayed + +(* ["(existS ?1 ?2 ?3 ?4)"] *) +val build_coq_existS_pattern : constr_pattern delayed + +(* ["(existT ?1 ?2 ?3 ?4)"] *) +val build_coq_existT_pattern : constr_pattern delayed + +(* ["(not ?)"] *) +val build_coq_not_pattern : constr_pattern delayed + +(* ["? -> False"] *) +val build_coq_imp_False_pattern : constr_pattern delayed + +(* ["(sumbool (eq ?1 ?2 ?3) ?4)"] *) +val build_coq_eqdec_partial_pattern : constr_pattern delayed + +(* ["! (x,y:?1). (sumbool (eq ?1 x y) ~(eq ?1 x y))"] *) +val build_coq_eqdec_pattern : constr_pattern delayed + +(* ["(sig ?1 ?2)"] *) +val build_coq_sig_pattern : constr_pattern delayed diff --git a/interp/genarg.ml b/interp/genarg.ml new file mode 100644 index 000000000..b25908b42 --- /dev/null +++ b/interp/genarg.ml @@ -0,0 +1,185 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Util +open Names +open Nametab +open Rawterm +open Topconstr + +type argument_type = + (* Basic types *) + | BoolArgType + | IntArgType + | IntOrVarArgType + | StringArgType + | PreIdentArgType + | IdentArgType + | RefArgType + (* Specific types *) + | SortArgType + | ConstrArgType + | ConstrMayEvalArgType + | QuantHypArgType + | TacticArgType + | CastedOpenConstrArgType + | ConstrWithBindingsArgType + | RedExprArgType + | List0ArgType of argument_type + | List1ArgType of argument_type + | OptArgType of argument_type + | PairArgType of argument_type * argument_type + | ExtraArgType of string + +type 'a or_var = ArgArg of 'a | ArgVar of identifier located + +(* Dynamics but tagged by a type expression *) + +type ('a,'b) generic_argument = argument_type * Obj.t + +let dyntab = ref ([] : string list) + +type ('a,'b,'c) abstract_argument_type = argument_type + +let create_arg s = + if List.mem s !dyntab then + anomaly ("Genarg.create: already declared generic argument " ^ s); + dyntab := s :: !dyntab; + let t = ExtraArgType s in + (t,t) + +let exists_argtype s = List.mem s !dyntab + +type open_constr = Evd.evar_map * Term.constr +(*type open_rawconstr = Coqast.t*) +type open_rawconstr = constr_expr + +let rawwit_bool = BoolArgType +let wit_bool = BoolArgType + +let rawwit_int = IntArgType +let wit_int = IntArgType + +let rawwit_int_or_var = IntOrVarArgType +let wit_int_or_var = IntOrVarArgType + +let rawwit_string = StringArgType +let wit_string = StringArgType + +let rawwit_ident = IdentArgType +let wit_ident = IdentArgType + +let rawwit_pre_ident = PreIdentArgType +let wit_pre_ident = PreIdentArgType + +let rawwit_ref = RefArgType +let wit_ref = RefArgType + +let rawwit_quant_hyp = QuantHypArgType +let wit_quant_hyp = QuantHypArgType + +let rawwit_sort = SortArgType +let wit_sort = SortArgType + +let rawwit_constr = ConstrArgType +let wit_constr = ConstrArgType + +let rawwit_constr_may_eval = ConstrMayEvalArgType +let wit_constr_may_eval = ConstrMayEvalArgType + +let rawwit_tactic = TacticArgType +let wit_tactic = TacticArgType + +let rawwit_casted_open_constr = CastedOpenConstrArgType +let wit_casted_open_constr = CastedOpenConstrArgType + +let rawwit_constr_with_bindings = ConstrWithBindingsArgType +let wit_constr_with_bindings = ConstrWithBindingsArgType + +let rawwit_red_expr = RedExprArgType +let wit_red_expr = RedExprArgType + +let wit_list0 t = List0ArgType t + +let wit_list1 t = List1ArgType t + +let wit_opt t = OptArgType t + +let wit_pair t1 t2 = PairArgType (t1,t2) + +let in_gen t o = (t,Obj.repr o) +let out_gen t (t',o) = if t = t' then Obj.magic o else failwith "out_gen" +let genarg_tag (s,_) = s + +let fold_list0 f = function + | (List0ArgType t as u, l) -> + List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l) + | _ -> failwith "Genarg: not a list0" + +let fold_list1 f = function + | (List1ArgType t as u, l) -> + List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l) + | _ -> failwith "Genarg: not a list1" + +let fold_opt f a = function + | (OptArgType t as u, l) -> + (match Obj.magic l with + | None -> a + | Some x -> f (in_gen t x)) + | _ -> failwith "Genarg: not a opt" + +let fold_pair f = function + | (PairArgType (t1,t2) as u, l) -> + let (x1,x2) = Obj.magic l in + f (in_gen t1 x1) (in_gen t2 x2) + | _ -> failwith "Genarg: not a pair" + +let app_list0 f = function + | (List0ArgType t as u, l) -> + let o = Obj.magic l in + (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o)) + | _ -> failwith "Genarg: not a list0" + +let app_list1 f = function + | (List1ArgType t as u, l) -> + let o = Obj.magic l in + (u, Obj.repr (List.map (fun x -> out_gen t (f (in_gen t x))) o)) + | _ -> failwith "Genarg: not a list1" + +let app_opt f = function + | (OptArgType t as u, l) -> + let o = Obj.magic l in + (u, Obj.repr (option_app (fun x -> out_gen t (f (in_gen t x))) o)) + | _ -> failwith "Genarg: not an opt" + +let app_pair f1 f2 = function + | (PairArgType (t1,t2) as u, l) -> + let (o1,o2) = Obj.magic l in + let o1 = out_gen t1 (f1 (in_gen t1 o1)) in + let o2 = out_gen t2 (f2 (in_gen t2 o2)) in + (u, Obj.repr (o1,o2)) + | _ -> failwith "Genarg: not a pair" + +let or_var_app f = function + | ArgArg x -> ArgArg (f x) + | ArgVar _ as x -> x + +let smash_var_app t f g = function + | ArgArg x -> f x + | ArgVar (_,id) -> + let (u, _ as x) = g id in + if t <> u then failwith "Genarg: a variable bound to a wrong type"; + x + +let unquote x = x + +type an_arg_of_this_type = Obj.t + +let in_generic t x = (t, Obj.repr x) diff --git a/interp/genarg.mli b/interp/genarg.mli new file mode 100644 index 000000000..f1246b2cc --- /dev/null +++ b/interp/genarg.mli @@ -0,0 +1,213 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Util +open Names +open Term +open Libnames +open Rawterm +open Topconstr + +type 'a or_var = ArgArg of 'a | ArgVar of identifier located + +type open_constr = Evd.evar_map * Term.constr +type open_rawconstr = constr_expr + + +(* The route of a generic argument, from parsing to evaluation + + parsing in_raw out_raw + char stream ----> rawtype ----> rawconstr generic_argument ----> + | + | interp + V + type <---- constr generic_argument <---- + out in + +To distinguish between the uninterpreted (raw) and the interpreted +worlds, we annotate the type generic_argument by a phantom argument +which is either constr_expr or constr (actually we add also a second +argument raw_tactic_expr and tactic, but this is only for technical +reasons, because these types are undefined at the type of compilation +of Genarg). + +Transformation for each type : +tag f raw open type cooked closed type + +BoolArgType bool bool +IntArgType int int +IntOrVarArgType int or_var int +StringArgType string (parsed w/ "") string +IdentArgType identifier identifier +PreIdentArgType string (parsed w/o "") string +RefArgType reference global_reference +ConstrArgType constr_expr constr +ConstrMayEvalArgType constr_expr may_eval constr +QuantHypArgType quantified_hypothesis quantified_hypothesis +TacticArgType raw_tactic_expr tactic +CastedOpenConstrArgType constr_expr open_constr +ConstrWithBindingsArgType constr_expr with_bindings constr with_bindings +List0ArgType of argument_type +List1ArgType of argument_type +OptArgType of argument_type +ExtraArgType of string '_a '_b +*) + +type ('a,'co,'ta) abstract_argument_type + +val rawwit_bool : (bool,'co,'ta) abstract_argument_type +val wit_bool : (bool,'co,'ta) abstract_argument_type + +val rawwit_int : (int,'co,'ta) abstract_argument_type +val wit_int : (int,'co,'ta) abstract_argument_type + +val rawwit_int_or_var : (int or_var,'co,'ta) abstract_argument_type +val wit_int_or_var : (int or_var,'co,'ta) abstract_argument_type + +val rawwit_string : (string,'co,'ta) abstract_argument_type +val wit_string : (string,'co,'ta) abstract_argument_type + +val rawwit_ident : (identifier,'co,'ta) abstract_argument_type +val wit_ident : (identifier,'co,'ta) abstract_argument_type + +val rawwit_pre_ident : (string,'co,'ta) abstract_argument_type +val wit_pre_ident : (string,'co,'ta) abstract_argument_type + +val rawwit_ref : (reference,constr_expr,'ta) abstract_argument_type +val wit_ref : (global_reference,constr,'ta) abstract_argument_type + +val rawwit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type +val wit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type + +val rawwit_sort : (rawsort,constr_expr,'ta) abstract_argument_type +val wit_sort : (sorts,constr,'ta) abstract_argument_type + +val rawwit_constr : (constr_expr,constr_expr,'ta) abstract_argument_type +val wit_constr : (constr,constr,'ta) abstract_argument_type + +val rawwit_constr_may_eval : (constr_expr may_eval,constr_expr,'ta) abstract_argument_type +val wit_constr_may_eval : (constr,constr,'ta) abstract_argument_type + +val rawwit_casted_open_constr : (open_rawconstr,constr_expr,'ta) abstract_argument_type +val wit_casted_open_constr : (open_constr,constr,'ta) abstract_argument_type + +val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) abstract_argument_type +val wit_constr_with_bindings : (constr with_bindings,constr,'ta) abstract_argument_type + +val rawwit_red_expr : ((constr_expr,reference or_metanum) red_expr_gen,constr_expr,'ta) abstract_argument_type +val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,constr,'ta) abstract_argument_type + +(* TODO: transformer tactic en extra arg *) +val rawwit_tactic : ('ta,constr_expr,'ta) abstract_argument_type +val wit_tactic : ('ta,constr,'ta) abstract_argument_type + +val wit_list0 : + ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type + +val wit_list1 : + ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type + +val wit_opt : + ('a,'co,'ta) abstract_argument_type -> ('a option,'co,'ta) abstract_argument_type + +val wit_pair : + ('a,'co,'ta) abstract_argument_type -> + ('b,'co,'ta) abstract_argument_type -> + ('a * 'b,'co,'ta) abstract_argument_type + +(* 'a generic_argument = (Sigma t:type. t[constr/'a]) *) +type ('a,'b) generic_argument + +val fold_list0 : + (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c + +val fold_list1 : + (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c + +val fold_opt : + (('a,'b) generic_argument -> 'c) -> 'c -> ('a,'b) generic_argument -> 'c + +val fold_pair : + (('a,'b) generic_argument -> ('a,'b) generic_argument -> 'c) -> + ('a,'b) generic_argument -> 'c + +(* [app_list0] fails if applied to an argument not of tag [List0 t] + for some [t]; it's the responsability of the caller to ensure it *) + +val app_list0 : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> +('a,'b) generic_argument -> ('c,'d) generic_argument + +val app_list1 : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> +('a,'b) generic_argument -> ('c,'d) generic_argument + +val app_opt : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> +('a,'b) generic_argument -> ('c,'d) generic_argument + +val app_pair : + (('a,'b) generic_argument -> ('c,'d) generic_argument) -> + (('a,'b) generic_argument -> ('c,'d) generic_argument) + -> ('a,'b) generic_argument -> ('c,'d) generic_argument + +(* Manque l'ordre supérieur, on aimerait ('co,'ta) 'a; manque aussi le + polymorphism, on aimerait que 'b et 'c restent polymorphes à l'appel + de create *) +val create_arg : string -> + ('rawa,'rawco,'rawta) abstract_argument_type + * ('a,'co,'ta) abstract_argument_type + +val exists_argtype : string -> bool + +type argument_type = + (* Basic types *) + | BoolArgType + | IntArgType + | IntOrVarArgType + | StringArgType + | PreIdentArgType + | IdentArgType + | RefArgType + (* Specific types *) + | SortArgType + | ConstrArgType + | ConstrMayEvalArgType + | QuantHypArgType + | TacticArgType + | CastedOpenConstrArgType + | ConstrWithBindingsArgType + | RedExprArgType + | List0ArgType of argument_type + | List1ArgType of argument_type + | OptArgType of argument_type + | PairArgType of argument_type * argument_type + | ExtraArgType of string + +val genarg_tag : ('a,'b) generic_argument -> argument_type + +val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type + +(* We'd like + + [in_generic: !b:type, !a:argument_type -> (f a) -> b generic_argument] + + with f a = b if a is Constr, f a = c if a is Tactic, otherwise f a = |a| + + in_generic is not typable; we replace the second argument by an absurd + type (with no introduction rule) +*) +type an_arg_of_this_type + +val in_generic : + argument_type -> an_arg_of_this_type -> ('a,'b) generic_argument + +val in_gen : + ('a,'co,'ta) abstract_argument_type -> 'a -> ('co,'ta) generic_argument +val out_gen : + ('a,'co,'ta) abstract_argument_type -> ('co,'ta) generic_argument -> 'a + diff --git a/interp/modintern.ml b/interp/modintern.ml new file mode 100644 index 000000000..8a0c8e545 --- /dev/null +++ b/interp/modintern.ml @@ -0,0 +1,103 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Pp +open Util +open Names +open Entries +open Libnames +open Topconstr +open Constrintern + +let rec make_mp mp = function + [] -> mp + | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl + +(* +(* Since module components are not put in the nametab we try to locate +the module prefix *) +exception BadRef + +let lookup_qualid (modtype:bool) qid = + let rec make_mp mp = function + [] -> mp + | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl + in + let rec find_module_prefix dir n = + if n<0 then raise Not_found; + let dir',dir'' = list_chop n dir in + let id',dir''' = + match dir'' with + | hd::tl -> hd,tl + | _ -> anomaly "This list should not be empty!" + in + let qid' = make_qualid dir' id' in + try + match Nametab.locate qid' with + | ModRef mp -> mp,dir''' + | _ -> raise BadRef + with + Not_found -> find_module_prefix dir (pred n) + in + try Nametab.locate qid + with Not_found -> + let (dir,id) = repr_qualid qid in + let pref_mp,dir' = find_module_prefix dir (List.length dir - 1) in + let mp = + List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir' + in + if modtype then + ModTypeRef (make_ln mp (label_of_id id)) + else + ModRef (MPdot (mp,label_of_id id)) + +*) + +(* Search for the head of [qid] in [binders]. + If found, returns the module_path/kernel_name created from the dirpath + and the basename. Searches Nametab otherwise. +*) + +let lookup_module (loc,qid) = + try + Nametab.locate_module qid + with + | Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid) + +let lookup_modtype (loc,qid) = + try + Nametab.locate_modtype qid + with + | Not_found -> + Modops.error_not_a_modtype_loc loc (string_of_qualid qid) + +let transl_with_decl env = function + | CWith_Module (id,qid) -> + With_Module (id,lookup_module qid) + | CWith_Definition (id,c) -> + With_Definition (id,interp_constr Evd.empty env c) + +let rec interp_modtype env = function + | CMTEident qid -> + MTEident (lookup_modtype qid) + | CMTEwith (mty,decl) -> + let mty = interp_modtype env mty in + let decl = transl_with_decl env decl in + MTEwith(mty,decl) + + +let rec interp_modexpr env = function + | CMEident qid -> + MEident (lookup_module qid) + | CMEapply (me1,me2) -> + let me1 = interp_modexpr env me1 in + let me2 = interp_modexpr env me2 in + MEapply(me1,me2) + diff --git a/interp/modintern.mli b/interp/modintern.mli new file mode 100644 index 000000000..2f9935674 --- /dev/null +++ b/interp/modintern.mli @@ -0,0 +1,24 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +(*i*) +open Declarations +open Environ +open Entries +open Topconstr +(*i*) + +(* Module expressions and module types are interpreted relatively to + eventual functor or funsig arguments. *) + +val interp_modtype : env -> module_type_ast -> module_type_entry + +val interp_modexpr : env -> module_ast -> module_expr + diff --git a/interp/ppextend.ml b/interp/ppextend.ml new file mode 100644 index 000000000..e2e60dc15 --- /dev/null +++ b/interp/ppextend.ml @@ -0,0 +1,57 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ *) + +(*i*) +open Pp +open Util +open Names +(*i*) + +(*s Pretty-print. *) + +(* Dealing with precedences *) + +type precedence = int + +type parenRelation = L | E | Any | Prec of precedence + +type tolerability = precedence * parenRelation + +type ppbox = + | PpHB of int + | PpHOVB of int + | PpHVB of int + | PpVB of int + | PpTB + +type ppcut = + | PpBrk of int * int + | PpTbrk of int * int + | PpTab + | PpFnl + +let ppcmd_of_box = function + | PpHB n -> h n + | PpHOVB n -> hov n + | PpHVB n -> hv n + | PpVB n -> v n + | PpTB -> t + +let ppcmd_of_cut = function + | PpTab -> tab () + | PpFnl -> fnl () + | PpBrk(n1,n2) -> brk(n1,n2) + | PpTbrk(n1,n2) -> tbrk(n1,n2) + +type unparsing = + | UnpMetaVar of identifier * tolerability + | UnpTerminal of string + | UnpBox of ppbox * unparsing list + | UnpCut of ppcut diff --git a/interp/ppextend.mli b/interp/ppextend.mli new file mode 100644 index 000000000..890422de8 --- /dev/null +++ b/interp/ppextend.mli @@ -0,0 +1,47 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ *) + +(*i*) +open Pp +open Names +(*i*) + +(*s Pretty-print. *) + +(* Dealing with precedences *) + +type precedence = int + +type parenRelation = L | E | Any | Prec of precedence + +type tolerability = precedence * parenRelation + +type ppbox = + | PpHB of int + | PpHOVB of int + | PpHVB of int + | PpVB of int + | PpTB + +type ppcut = + | PpBrk of int * int + | PpTbrk of int * int + | PpTab + | PpFnl + +val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds + +val ppcmd_of_cut : ppcut -> std_ppcmds + +type unparsing = + | UnpMetaVar of identifier * tolerability + | UnpTerminal of string + | UnpBox of ppbox * unparsing list + | UnpCut of ppcut diff --git a/interp/symbols.ml b/interp/symbols.ml new file mode 100644 index 000000000..c6eff9ab9 --- /dev/null +++ b/interp/symbols.ml @@ -0,0 +1,331 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(*i*) +open Util +open Pp +open Bignat +open Names +open Nametab +open Summary +open Rawterm +open Topconstr +open Ppextend +(*i*) + +(*s A scope is a set of notations; it includes + + - a set of ML interpreters/parsers for positive (e.g. 0, 1, 15, ...) and + negative numbers (e.g. -0, -2, -13, ...). These interpreters may + fail if a number has no interpretation in the scope (e.g. there is + no interpretation for negative numbers in [nat]); interpreters both for + terms and patterns can be set; these interpreters are in permanent table + [numeral_interpreter_tab] + - a set of ML printers for expressions denoting numbers parsable in + this scope (permanently declared in [Esyntax.primitive_printer_tab]) + - a set of interpretations for infix (more generally distfix) notations + - an optional pair of delimiters which, when occurring in a syntactic + expression, set this scope to be the current scope +*) + +(**********************************************************************) +(* Scope of symbols *) + +type level = precedence * precedence list +type delimiters = string * string +type scope = { + notations: (aconstr * level) Stringmap.t; + delimiters: delimiters option +} +type scopes = scope_name list + +(* Scopes table: scope_name -> symbol_interpretation *) +let scope_map = ref Stringmap.empty + +let empty_scope = { + notations = Stringmap.empty; + delimiters = None +} + +let default_scope = "core_scope" + +let _ = Stringmap.add default_scope empty_scope !scope_map + +let scope_stack = ref [default_scope] + +let current_scopes () = !scope_stack + +(* TODO: push nat_scope, z_scope, ... in scopes summary *) + +(**********************************************************************) +(* Interpreting numbers (not in summary because functional objects) *) + +type numeral_interpreter_name = string +type numeral_interpreter = + (loc -> bigint -> rawconstr) + * (loc -> bigint -> name -> cases_pattern) option + +let numeral_interpreter_tab = + (Hashtbl.create 17 : (numeral_interpreter_name,numeral_interpreter)Hashtbl.t) + +let declare_numeral_interpreter sc t = + Hashtbl.add numeral_interpreter_tab sc t + +let lookup_numeral_interpreter s = + try + Hashtbl.find numeral_interpreter_tab s + with Not_found -> + error ("No interpretation for numerals in scope "^s) + +(* For loading without opening *) +let declare_scope scope = + try let _ = Stringmap.find scope !scope_map in () + with Not_found -> +(* Options.if_verbose message ("Creating scope "^scope);*) + scope_map := Stringmap.add scope empty_scope !scope_map + +let find_scope scope = + try Stringmap.find scope !scope_map + with Not_found -> error ("Scope "^scope^" is not declared") + +let check_scope sc = let _ = find_scope sc in () + +let declare_delimiters scope dlm = + let sc = find_scope scope in + if sc.delimiters <> None && Options.is_verbose () then + warning ("Overwriting previous delimiters in "^scope); + let sc = { sc with delimiters = Some dlm } in + scope_map := Stringmap.add scope sc !scope_map + +(* The mapping between notations and production *) + +let declare_notation nt scope (c,prec as info) = + let sc = find_scope scope in + if Stringmap.mem nt sc.notations && Options.is_verbose () then + warning ("Notation "^nt^" is already used in scope "^scope); + let sc = { sc with notations = Stringmap.add nt info sc.notations } in + scope_map := Stringmap.add scope sc !scope_map + +let rec find_interpretation f = function + | scope::scopes -> + (try f (find_scope scope) + with Not_found -> find_interpretation f scopes) + | [] -> raise Not_found + +let rec interp_notation ntn scopes = + let f scope = fst (Stringmap.find ntn scope.notations) in + try find_interpretation f scopes + with Not_found -> anomaly ("Unknown interpretation for notation "^ntn) + +let find_notation_with_delimiters scope = + match (Stringmap.find scope !scope_map).delimiters with + | Some dlm -> Some (Some dlm) + | None -> None + +let rec find_notation_without_delimiters ntn_scope ntn = function + | scope::scopes -> + (* Is the expected printer attached to the most recently open scope? *) + if scope = ntn_scope then + Some None + else + (* If the most recently open scope has a printer for this pattern + but not the expected one then we need delimiters *) + if Stringmap.mem ntn (Stringmap.find scope !scope_map).notations then + find_notation_with_delimiters ntn_scope + else + find_notation_without_delimiters ntn_scope ntn scopes + | [] -> + find_notation_with_delimiters ntn_scope + +let find_notation ntn_scope ntn scopes = + match + find_notation_without_delimiters ntn_scope ntn scopes + with + | None -> None + | Some None -> Some (None,scopes) + | Some x -> Some (x,ntn_scope::scopes) + +let exists_notation_in_scope scope prec ntn r = + try Stringmap.find ntn (Stringmap.find scope !scope_map).notations = (r,prec) + with Not_found -> false + +let exists_notation_prec prec nt sc = + try snd (Stringmap.find nt sc.notations) = prec with Not_found -> false + +let exists_notation prec nt = + Stringmap.fold (fun scn sc b -> b or exists_notation_prec prec nt sc) + !scope_map false + +(* We have to print delimiters; look for the more recent defined one *) +(* Do we need to print delimiters? To know it, we look for a numeral *) +(* printer available in the current stack of scopes *) +let find_numeral_with_delimiters scope = + match (Stringmap.find scope !scope_map).delimiters with + | Some dlm -> Some (Some dlm) + | None -> None + +let rec find_numeral_without_delimiters printer_scope = function + | scope :: scopes -> + (* Is the expected printer attached to the most recently open scope? *) + if scope = printer_scope then + Some None + else + (* If the most recently open scope has a printer for numerals + but not the expected one then we need delimiters *) + if not (Hashtbl.mem numeral_interpreter_tab scope) then + find_numeral_without_delimiters printer_scope scopes + else + find_numeral_with_delimiters printer_scope + | [] -> + (* Can we switch to [scope]? Yes if it has defined delimiters *) + find_numeral_with_delimiters printer_scope + +let find_numeral_printer printer_scope scopes = + match + find_numeral_without_delimiters printer_scope scopes + with + | None -> None + | Some None -> Some (None,scopes) + | Some x -> Some (x,printer_scope::scopes) + +(* This is the map associating the scope a numeral printer belongs to *) +(* +let numeral_printer_map = ref (Stringmap.empty : scope_name Stringmap.t) +*) + +let rec interp_numeral loc n = function + | scope :: scopes -> + (try fst (lookup_numeral_interpreter scope) loc n + with Not_found -> interp_numeral loc n scopes) + | [] -> + user_err_loc (loc,"interp_numeral", + str "No interpretation for numeral " ++ pr_bigint n) + +let rec interp_numeral_as_pattern loc n name = function + | scope :: scopes -> + (try + match snd (lookup_numeral_interpreter scope) with + | None -> raise Not_found + | Some g -> g loc n name + with Not_found -> interp_numeral_as_pattern loc n name scopes) + | [] -> + user_err_loc (loc,"interp_numeral_as_pattern", + str "No interpretation for numeral " ++ pr_bigint n) + +(* Exportation of scopes *) +let cache_scope (_,sc) = + check_scope sc; + scope_stack := sc :: !scope_stack + +let subst_scope (_,subst,sc) = sc + +open Libobject + +let (inScope,outScope) = + declare_object {(default_object "SCOPE") with + cache_function = cache_scope; + open_function = (fun i o -> if i=1 then cache_scope o); + subst_function = subst_scope; + classify_function = (fun (_,o) -> Substitute o); + export_function = (fun x -> Some x) } + +let open_scope sc = Lib.add_anonymous_leaf (inScope sc) + + +(* Special scopes associated to arguments of a global reference *) + +open Libnames + +module RefOrdered = + struct + type t = global_reference + let compare = Pervasives.compare + end + +module Refmap = Map.Make(RefOrdered) + +let arguments_scope = ref Refmap.empty + +let cache_arguments_scope (_,(r,scl)) = + List.iter (option_iter check_scope) scl; + arguments_scope := Refmap.add r scl !arguments_scope + +let subst_arguments_scope (_,subst,(r,scl)) = (subst_global subst r,scl) + +let (inArgumentsScope,outArgumentsScope) = + declare_object {(default_object "ARGUMENTS-SCOPE") with + cache_function = cache_arguments_scope; + open_function = (fun i o -> if i=1 then cache_arguments_scope o); + subst_function = subst_arguments_scope; + classify_function = (fun (_,o) -> Substitute o); + export_function = (fun x -> Some x) } + +let declare_arguments_scope r scl = + Lib.add_anonymous_leaf (inArgumentsScope (r,scl)) + +let find_arguments_scope r = + try Refmap.find r !arguments_scope + with Not_found -> [] + +(* Printing *) + +let pr_delimiters = function + | None -> str "No delimiters" + | Some (l,r) -> str "Delimiters are " ++ str l ++ str " and " ++ str r + +let pr_notation prraw ntn r = + str ntn ++ str " stands for " ++ prraw r + +let pr_named_scope prraw scope sc = + str "Scope " ++ str scope ++ fnl () + ++ pr_delimiters sc.delimiters ++ fnl () + ++ Stringmap.fold + (fun ntn (r,_) strm -> pr_notation prraw ntn r ++ fnl () ++ strm) + sc.notations (mt ()) + +let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope) + +let pr_scopes prraw = + Stringmap.fold + (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm) + !scope_map (mt ()) + +(* Synchronisation with reset *) + +let freeze () = (!scope_map, !scope_stack, !arguments_scope) + +let unfreeze (scm,scs,asc) = + scope_map := scm; + scope_stack := scs; + arguments_scope := asc + +let init () = () +(* + scope_map := Strinmap.empty; + scope_stack := Stringmap.empty +*) + +let _ = + declare_summary "symbols" + { freeze_function = freeze; + unfreeze_function = unfreeze; + init_function = init; + survive_section = false } + + +let printing_rules = + ref (Stringmap.empty : (unparsing list * precedence) Stringmap.t) + +let declare_printing_rule ntn unpl = + printing_rules := Stringmap.add ntn unpl !printing_rules + +let find_notation_printing_rule ntn = + try Stringmap.find ntn !printing_rules + with Not_found -> anomaly ("No printing rule found for "^ntn) diff --git a/interp/symbols.mli b/interp/symbols.mli new file mode 100644 index 000000000..3c082b2ce --- /dev/null +++ b/interp/symbols.mli @@ -0,0 +1,77 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(*i*) +open Util +open Pp +open Bignat +open Names +open Nametab +open Rawterm +open Topconstr +open Ppextend +(*i*) + +(*s A numeral interpreter is the pair of an interpreter for _integer_ + numbers in terms and an optional interpreter in pattern, if + negative numbers are not supported, the interpreter must fail with + an appropriate error message *) + +type numeral_interpreter_name = string +type numeral_interpreter = + (loc -> bigint -> rawconstr) + * (loc -> bigint -> name -> cases_pattern) option + +(* A scope is a set of interpreters for symbols + optional + interpreter and printers for integers + optional delimiters *) + +type level = precedence * precedence list +type delimiters = string * string +type scope +type scopes = scope_name list + +val default_scope : scope_name +val current_scopes : unit -> scopes +val open_scope : scope_name -> unit +val declare_scope : scope_name -> unit + +(* Declare delimiters for printing *) +val declare_delimiters : scope_name -> delimiters -> unit + +(* Declare, interpret, and look for a printer for numeral *) +val declare_numeral_interpreter : + numeral_interpreter_name -> numeral_interpreter -> unit +val interp_numeral : loc -> bigint -> scopes -> rawconstr +val interp_numeral_as_pattern : loc -> bigint -> name -> scopes ->cases_pattern +val find_numeral_printer : string -> scopes -> + (delimiters option * scopes) option + +(* Declare, interpret, and look for a printer for symbolic notations *) +val declare_notation : notation -> scope_name -> aconstr * level -> unit +val interp_notation : notation -> scopes -> aconstr +val find_notation : scope_name -> notation -> scopes -> + (delimiters option * scopes) option +val exists_notation_in_scope : + scope_name -> level -> notation -> aconstr -> bool +val exists_notation : level -> notation -> bool + +(* Declare and look for scopes associated to arguments of a global ref *) +open Libnames +val declare_arguments_scope: global_reference -> scope_name option list -> unit +val find_arguments_scope : global_reference -> scope_name option list + +(* Printing scopes *) +val pr_scope : (aconstr -> std_ppcmds) -> scope_name -> std_ppcmds +val pr_scopes : (aconstr -> std_ppcmds) -> std_ppcmds + + +val declare_printing_rule : notation -> unparsing list * precedence -> unit +val find_notation_printing_rule : notation -> unparsing list * precedence + diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml new file mode 100644 index 000000000..a49352da3 --- /dev/null +++ b/interp/syntax_def.ml @@ -0,0 +1,72 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Util +open Pp +open Names +open Libnames +open Topconstr +open Libobject +open Lib +open Nameops + +(* Syntactic definitions. *) + +let syntax_table = ref (KNmap.empty : aconstr KNmap.t) + +let _ = Summary.declare_summary + "SYNTAXCONSTANT" + { Summary.freeze_function = (fun () -> !syntax_table); + Summary.unfreeze_function = (fun ft -> syntax_table := ft); + Summary.init_function = (fun () -> syntax_table := KNmap.empty); + Summary.survive_section = false } + +let add_syntax_constant kn c = + syntax_table := KNmap.add kn c !syntax_table + +let cache_syntax_constant ((sp,kn),c) = + if Nametab.exists_cci sp then + errorlabstrm "cache_syntax_constant" + (pr_id (basename sp) ++ str " already exists"); + add_syntax_constant kn c; + Nametab.push_syntactic_definition (Nametab.Until 1) sp kn + +let load_syntax_constant i ((sp,kn),c) = + if Nametab.exists_cci sp then + errorlabstrm "cache_syntax_constant" + (pr_id (basename sp) ++ str " already exists"); + add_syntax_constant kn c; + Nametab.push_syntactic_definition (Nametab.Until i) sp kn + +let open_syntax_constant i ((sp,kn),c) = + Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn + +let subst_syntax_constant ((sp,kn),subst,c) = + subst_aconstr subst c + +let classify_syntax_constant (_,c) = Substitute c + +let (in_syntax_constant, out_syntax_constant) = + declare_object {(default_object "SYNTAXCONSTANT") with + cache_function = cache_syntax_constant; + load_function = load_syntax_constant; + open_function = open_syntax_constant; + subst_function = subst_syntax_constant; + classify_function = classify_syntax_constant; + export_function = (fun x -> Some x) } + +let declare_syntactic_definition id c = + let _ = add_leaf id (in_syntax_constant c) in () + +let rec set_loc loc _ a = + map_aconstr_with_binders_loc loc (fun id e -> (id,e)) (set_loc loc) () a + +let search_syntactic_definition loc kn = + set_loc loc () (KNmap.find kn !syntax_table) diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli new file mode 100644 index 000000000..f4600d8db --- /dev/null +++ b/interp/syntax_def.mli @@ -0,0 +1,23 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +(*i*) +open Names +open Topconstr +open Rawterm +(*i*) + +(* Syntactic definitions. *) + +val declare_syntactic_definition : identifier -> aconstr -> unit + +val search_syntactic_definition : loc -> kernel_name -> rawconstr + + diff --git a/interp/topconstr.ml b/interp/topconstr.ml new file mode 100644 index 000000000..8569c414b --- /dev/null +++ b/interp/topconstr.ml @@ -0,0 +1,300 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(*i*) +open Pp +open Util +open Names +open Nameops +open Libnames +open Rawterm +open Term +(*i*) + + +(* This is the subtype of rawconstr allowed in syntactic extensions *) +type aconstr = + | ARef of global_reference + | AVar of identifier + | AApp of aconstr * aconstr list + | ALambda of name * aconstr * aconstr + | AProd of name * aconstr * aconstr + | ALetIn of name * aconstr * aconstr + | AOldCase of case_style * aconstr option * aconstr * aconstr array + | ASort of rawsort + | AHole of hole_kind + | AMeta of int + | ACast of aconstr * aconstr + +let name_app f e = function + | Name id -> let (id, e) = f id e in (Name id, e) + | Anonymous -> Anonymous, e + +let map_aconstr_with_binders_loc loc g f e = function + | AVar (id) -> RVar (loc,id) + | AApp (a,args) -> RApp (loc,f e a, List.map (f e) args) + | ALambda (na,ty,c) -> + let na,e = name_app g e na in RLambda (loc,na,f e ty,f e c) + | AProd (na,ty,c) -> + let na,e = name_app g e na in RProd (loc,na,f e ty,f e c) + | ALetIn (na,b,c) -> + let na,e = name_app g e na in RLetIn (loc,na,f e b,f e c) + | AOldCase (b,tyopt,tm,bv) -> + ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv) + | ACast (c,t) -> RCast (loc,f e c,f e t) + | ASort x -> RSort (loc,x) + | AHole x -> RHole (loc,x) + | AMeta n -> RMeta (loc,n) + | ARef x -> RRef (loc,x) + +let rec subst_aconstr subst raw = + match raw with + | ARef ref -> + let ref' = subst_global subst ref in + if ref' == ref then raw else + ARef ref' + + | AVar _ -> raw + + | AApp (r,rl) -> + let r' = subst_aconstr subst r + and rl' = list_smartmap (subst_aconstr subst) rl in + if r' == r && rl' == rl then raw else + AApp(r',rl') + + | ALambda (n,r1,r2) -> + let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in + if r1' == r1 && r2' == r2 then raw else + ALambda (n,r1',r2') + + | AProd (n,r1,r2) -> + let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in + if r1' == r1 && r2' == r2 then raw else + AProd (n,r1',r2') + + | ALetIn (n,r1,r2) -> + let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in + if r1' == r1 && r2' == r2 then raw else + ALetIn (n,r1',r2') + + | AOldCase (b,ro,r,ra) -> + let ro' = option_smartmap (subst_aconstr subst) ro + and r' = subst_aconstr subst r + and ra' = array_smartmap (subst_aconstr subst) ra in + if ro' == ro && r' == r && ra' == ra then raw else + AOldCase (b,ro',r',ra') + + | AMeta _ | ASort _ -> raw + + | AHole (ImplicitArg (ref,i)) -> + let ref' = subst_global subst ref in + if ref' == ref then raw else + AHole (ImplicitArg (ref',i)) + | AHole ( (AbstractionType _ | QuestionMark | CasesType | + InternalHole | TomatchTypeParameter _)) -> raw + + | ACast (r1,r2) -> + let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in + if r1' == r1 && r2' == r2 then raw else + ACast (r1',r2') + +let rec aux = function + | RVar (_,id) -> AVar id + | RApp (_,g,args) -> AApp (aux g, List.map aux args) + | RLambda (_,na,ty,c) -> ALambda (na,aux ty,aux c) + | RProd (_,na,ty,c) -> AProd (na,aux ty,aux c) + | RLetIn (_,na,b,c) -> ALetIn (na,aux b,aux c) + | ROrderedCase (_,b,tyopt,tm,bv) -> + AOldCase (b,option_app aux tyopt,aux tm, Array.map aux bv) + | RCast (_,c,t) -> ACast (aux c,aux t) + | RSort (_,s) -> ASort s + | RHole (_,w) -> AHole w + | RRef (_,r) -> ARef r + | RMeta (_,n) -> AMeta n + | RDynamic _ | RRec _ | RCases _ | REvar _ -> + error "Fixpoints, cofixpoints, existential variables and pattern-matching not \ +allowed in abbreviatable expressions" + +let aconstr_of_rawconstr = aux + +(*s Concrete syntax for terms *) + +type scope_name = string + +type notation = string + +type explicitation = int + +type cases_pattern_expr = + | CPatAlias of loc * cases_pattern_expr * identifier + | CPatCstr of loc * reference * cases_pattern_expr list + | CPatAtom of loc * reference option + | CPatNumeral of loc * Bignat.bigint + | CPatDelimiters of loc * scope_name * cases_pattern_expr + +type constr_expr = + | CRef of reference + | CFix of loc * identifier located * fixpoint_expr list + | CCoFix of loc * identifier located * cofixpoint_expr list + | CArrow of loc * constr_expr * constr_expr + | CProdN of loc * (name located list * constr_expr) list * constr_expr + | CLambdaN of loc * (name located list * constr_expr) list * constr_expr + | CLetIn of loc * name located * constr_expr * constr_expr + | CAppExpl of loc * reference * constr_expr list + | CApp of loc * constr_expr * (constr_expr * explicitation option) list + | CCases of loc * constr_expr option * constr_expr list * + (loc * cases_pattern_expr list * constr_expr) list + | COrderedCase of loc * case_style * constr_expr option * constr_expr + * constr_expr list + | CHole of loc + | CMeta of loc * int + | CSort of loc * rawsort + | CCast of loc * constr_expr * constr_expr + | CNotation of loc * notation * (identifier * constr_expr) list + | CGrammar of loc * aconstr * (identifier * constr_expr) list + | CNumeral of loc * Bignat.bigint + | CDelimiters of loc * scope_name * constr_expr + | CDynamic of loc * Dyn.t + +and fixpoint_binder = name located list * constr_expr + +and fixpoint_expr = identifier * fixpoint_binder list * constr_expr * constr_expr + +and cofixpoint_expr = identifier * constr_expr * constr_expr + +let constr_loc = function + | CRef (Ident (loc,_)) -> loc + | CRef (Qualid (loc,_)) -> loc + | CFix (loc,_,_) -> loc + | CCoFix (loc,_,_) -> loc + | CArrow (loc,_,_) -> loc + | CProdN (loc,_,_) -> loc + | CLambdaN (loc,_,_) -> loc + | CLetIn (loc,_,_,_) -> loc + | CAppExpl (loc,_,_) -> loc + | CApp (loc,_,_) -> loc + | CCases (loc,_,_,_) -> loc + | COrderedCase (loc,_,_,_,_) -> loc + | CHole loc -> loc + | CMeta (loc,_) -> loc + | CSort (loc,_) -> loc + | CCast (loc,_,_) -> loc + | CNotation (loc,_,_) -> loc + | CGrammar (loc,_,_) -> loc + | CNumeral (loc,_) -> loc + | CDelimiters (loc,_,_) -> loc + | CDynamic _ -> dummy_loc + +let cases_pattern_loc = function + | CPatAlias (loc,_,_) -> loc + | CPatCstr (loc,_,_) -> loc + | CPatAtom (loc,_) -> loc + | CPatNumeral (loc,_) -> loc + | CPatDelimiters (loc,_,_) -> loc + +let replace_vars_constr_expr l t = + if l = [] then t else failwith "replace_constr_expr: TODO" + +let occur_var_constr_ref id = function + | Ident (loc,id') -> id = id' + | Qualid _ -> false + +let rec occur_var_constr_expr id = function + | CRef r -> occur_var_constr_ref id r + | CArrow (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b + | CAppExpl (loc,r,l) -> + occur_var_constr_ref id r or List.exists (occur_var_constr_expr id) l + | CApp (loc,f,l) -> + occur_var_constr_expr id f or + List.exists (fun (a,_) -> occur_var_constr_expr id a) l + | CProdN (_,l,b) -> occur_var_binders id b l + | CLambdaN (_,l,b) -> occur_var_binders id b l + | CLetIn (_,na,a,b) -> occur_var_binders id b [[na],a] + | CCast (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b + | CNotation (_,_,l) -> List.exists (fun (_,x) -> occur_var_constr_expr id x) l + | CGrammar (loc,_,l) -> List.exists (fun (_,x) -> occur_var_constr_expr id x)l + | CDelimiters (loc,_,a) -> occur_var_constr_expr id a + | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ -> false + | CCases (loc,_,_,_) + | COrderedCase (loc,_,_,_,_) + | CFix (loc,_,_) + | CCoFix (loc,_,_) -> + Pp.warning "Capture check in multiple binders not done"; false + +and occur_var_binders id b = function + | (idl,a)::l -> + occur_var_constr_expr id a or + (not (List.mem (Name id) (snd (List.split idl))) + & occur_var_binders id b l) + | [] -> occur_var_constr_expr id b + +let mkIdentC id = CRef (Ident (dummy_loc, id)) +let mkRefC r = CRef r +let mkAppC (f,l) = CApp (dummy_loc, f, List.map (fun x -> (x,None)) l) +let mkCastC (a,b) = CCast (dummy_loc,a,b) +let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b) +let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b) +let mkProdC (idl,a,b) = CProdN (dummy_loc,[idl,a],b) + +(* Used in correctness and interface *) + +let map_binders f g e bl = + (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) + let h (nal,t) (e,bl) = + (List.fold_right (fun (_,na) -> name_fold g na) nal e,(nal,f e t)::bl) in + List.fold_right h bl (e,[]) + +let map_constr_expr_with_binders f g e = function + | CArrow (loc,a,b) -> CArrow (loc,f e a,f e b) + | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l) + | CApp (loc,a,l) -> CApp (loc,f e a,List.map (fun (a,i) -> (f e a,i)) l) + | CProdN (loc,bl,b) -> + let (e,bl) = map_binders f g e bl in CProdN (loc,bl,f e b) + | CLambdaN (loc,bl,b) -> + let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b) + | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b) + | CCast (loc,a,b) -> CCast (loc,f e a,f e b) + | CNotation (loc,n,l) -> CNotation (loc,n,List.map (fun (x,t) ->(x,f e t)) l) + | CGrammar (loc,r,l) -> CGrammar (loc,r,List.map (fun (x,t) ->(x,f e t)) l) + | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a) + | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ | CRef _ as x -> x + | CCases (loc,po,a,bl) -> + (* TODO: apply g on the binding variables in pat... *) + (* hard because no syntactic diff between a constructor and a var *) + let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in + CCases (loc,option_app (f e) po,List.map (f e) a,bl) + | COrderedCase (loc,s,po,a,bl) -> + COrderedCase (loc,s,option_app (f e) po,f e a,List.map (f e) bl) + | CFix (loc,id,dl) -> + let k (id,bl,t,d) = + let (e,bl) = map_binders f g e bl in (id,bl,f e t,f e d) in + CFix (loc,id,List.map k dl) + | CCoFix (loc,id,dl) -> + CCoFix (loc,id,List.map (fun (id,t,d) -> (id,f e t,f e d)) dl) + +(* For binders parsing *) + +type local_binder = + | LocalRawDef of name located * constr_expr + | LocalRawAssum of name located list * constr_expr + +(* Concrete syntax for modules and modules types *) + +type with_declaration_ast = + | CWith_Module of identifier * qualid located + | CWith_Definition of identifier * constr_expr + +type module_type_ast = + | CMTEident of qualid located + | CMTEwith of module_type_ast * with_declaration_ast + +type module_ast = + | CMEident of qualid located + | CMEapply of module_ast * module_ast diff --git a/interp/topconstr.mli b/interp/topconstr.mli new file mode 100644 index 000000000..72845f896 --- /dev/null +++ b/interp/topconstr.mli @@ -0,0 +1,133 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(*i*) +open Pp +open Util +open Names +open Libnames +open Rawterm +open Term +(*i*) + +(*s This is the subtype of rawconstr allowed in syntactic extensions *) +(* No location since intended to be substituted at any place of a text *) +(* Complex expressions such as fixpoints, cofixpoints and pattern-matching *) +(* are excluded; non global expressions such as existential variables also *) + +type aconstr = + | ARef of global_reference + | AVar of identifier + | AApp of aconstr * aconstr list + | ALambda of name * aconstr * aconstr + | AProd of name * aconstr * aconstr + | ALetIn of name * aconstr * aconstr + | AOldCase of case_style * aconstr option * aconstr * aconstr array + | ASort of rawsort + | AHole of hole_kind + | AMeta of int + | ACast of aconstr * aconstr + +val map_aconstr_with_binders_loc : loc -> + (identifier -> 'a -> identifier * 'a) -> + ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr + +val subst_aconstr : Names.substitution -> aconstr -> aconstr + +val aconstr_of_rawconstr : rawconstr -> aconstr + +(*s Concrete syntax for terms *) + +type scope_name = string + +type notation = string + +type explicitation = int + +type cases_pattern_expr = + | CPatAlias of loc * cases_pattern_expr * identifier + | CPatCstr of loc * reference * cases_pattern_expr list + | CPatAtom of loc * reference option + | CPatNumeral of loc * Bignat.bigint + | CPatDelimiters of loc * scope_name * cases_pattern_expr + +type constr_expr = + | CRef of reference + | CFix of loc * identifier located * fixpoint_expr list + | CCoFix of loc * identifier located * cofixpoint_expr list + | CArrow of loc * constr_expr * constr_expr + | CProdN of loc * (name located list * constr_expr) list * constr_expr + | CLambdaN of loc * (name located list * constr_expr) list * constr_expr + | CLetIn of loc * name located * constr_expr * constr_expr + | CAppExpl of loc * reference * constr_expr list + | CApp of loc * constr_expr * (constr_expr * explicitation option) list + | CCases of loc * constr_expr option * constr_expr list * + (loc * cases_pattern_expr list * constr_expr) list + | COrderedCase of loc * case_style * constr_expr option * constr_expr + * constr_expr list + | CHole of loc + | CMeta of loc * int + | CSort of loc * rawsort + | CCast of loc * constr_expr * constr_expr + | CNotation of loc * notation * (identifier * constr_expr) list + | CGrammar of loc * aconstr * (identifier * constr_expr) list + | CNumeral of loc * Bignat.bigint + | CDelimiters of loc * scope_name * constr_expr + | CDynamic of loc * Dyn.t + +and fixpoint_binder = name located list * constr_expr + +and fixpoint_expr = identifier * fixpoint_binder list * constr_expr * constr_expr + +and cofixpoint_expr = identifier * constr_expr * constr_expr + +val constr_loc : constr_expr -> loc + +val cases_pattern_loc : cases_pattern_expr -> loc + +val replace_vars_constr_expr : + (identifier * identifier) list -> constr_expr -> constr_expr + +val occur_var_constr_expr : identifier -> constr_expr -> bool + +val mkIdentC : identifier -> constr_expr +val mkRefC : reference -> constr_expr +val mkAppC : constr_expr * constr_expr list -> constr_expr +val mkCastC : constr_expr * constr_expr -> constr_expr +val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr +val mkLetInC : name located * constr_expr * constr_expr -> constr_expr +val mkProdC : name located list * constr_expr * constr_expr -> constr_expr + +(* Used in correctness and interface; absence of var capture not guaranteed *) +(* in pattern-matching clauses and in binders of the form [x,y:T(x)] *) + +val map_constr_expr_with_binders : + ('a -> constr_expr -> constr_expr) -> + (identifier -> 'a -> 'a) -> 'a -> constr_expr -> constr_expr + +(* For binders parsing *) + +type local_binder = + | LocalRawDef of name located * constr_expr + | LocalRawAssum of name located list * constr_expr + +(* Concrete syntax for modules and modules types *) + +type with_declaration_ast = + | CWith_Module of identifier * qualid located + | CWith_Definition of identifier * constr_expr + +type module_type_ast = + | CMTEident of qualid located + | CMTEwith of module_type_ast * with_declaration_ast + +type module_ast = + | CMEident of qualid located + | CMEapply of module_ast * module_ast |