Merge pull request Deducteam#149 from Deducteam/api-get-rule

Add a way to get a function definition

kernel/signature.ml

@@ -218,6 +218,10 @@ let get_dtree sg rule_filter l cst =
       try Dtree.of_rules rules'
       with Dtree.DtreeError e -> raise (SignatureError (CannotBuildDtree e))
 
+let get_rules sg lc cst =
+  match (get_infos sg lc cst).rule_opt_info with
+  | None -> []
+  | Some (rs,_) -> rs
 
 (******************************************************************************)
 

kernel/signature.mli

@@ -54,6 +54,9 @@ val get_dtree           : t -> (Rule.rule_name -> bool) option -> loc -> name ->
     with [cst] inside the environment [sg]. When filter is specified, it is used
     to select only the corresponding set of rules  *)
 
+val get_rules           : t -> loc -> name -> rule_infos list
+(** [get_rules sg lc cst] returns a list of rules that defines the symbol. *)
+
 val add_declaration     : t -> loc -> ident -> staticity -> term -> unit
 (** [add_declaration sg l id st ty] declares the symbol [id] of type [ty]
     and staticity [st] in the environment [sg]. *)